From 60f01f46ba232ed6416054f0a6115cb2a9b70b4e Mon Sep 17 00:00:00 2001 From: OszkarSemerath Date: Sat, 10 Jun 2017 19:05:05 +0200 Subject: Migrating Additional projects --- .../.classpath | 9 + .../.gitignore | 4 + .../.project | 34 + .../.settings/org.eclipse.core.resources.prefs | 2 + .../.settings/org.eclipse.jdt.core.prefs | 7 + .../META-INF/MANIFEST.MF | 27 + .../build.properties | 6 + .../plugin.xml | 398 ++++++++ .../plugin.xml_gen | 398 ++++++++ .../inf/dslreasoner/ui/SmtLanguageUiModule.java | 15 + .../SmtLanguageProposalProvider.xtend | 12 + .../SmtLanguageDescriptionLabelProvider.xtend | 24 + .../ui/labeling/SmtLanguageLabelProvider.xtend | 29 + .../outline/SmtLanguageOutlineTreeProvider.xtend | 13 + .../ui/quickfix/SmtLanguageQuickfixProvider.xtend | 26 + .../.classpath | 9 + .../.gitignore | 4 + ...hu.bme.mit.inf.dslreasoner.smt.language).launch | 17 + .../.project | 34 + .../.settings/org.eclipse.core.resources.prefs | 2 + .../.settings/org.eclipse.jdt.core.prefs | 7 + .../META-INF/MANIFEST.MF | 37 + .../build.properties | 7 + .../model/generated/SmtLanguage.ecore | 304 ++++++ .../model/generated/SmtLanguage.genmodel | 238 +++++ .../plugin.xml | 16 + .../plugin.xml_gen | 16 + .../mit/inf/dslreasoner/GenerateSmtLanguage.mwe2 | 133 +++ .../hu/bme/mit/inf/dslreasoner/SmtLanguage.xtext | 222 ++++ .../inf/dslreasoner/SmtLanguageRuntimeModule.java | 11 + .../dslreasoner/SmtLanguageStandaloneSetup.java | 16 + .../formatting/SmtLanguageFormatter.xtend | 34 + .../generator/SmtLanguageGenerator.xtend | 24 + .../scoping/SmtLanguageScopeProvider.xtend | 138 +++ .../validation/SmtLanguageValidator.xtend | 24 + .../.classpath | 8 + .../.gitignore | 4 + .../.project | 34 + .../.settings/org.eclipse.jdt.core.prefs | 7 + .../META-INF/MANIFEST.MF | 12 + .../build.properties | 5 + .../Logic2SMT_TypeMapperInterpretation.xtend | 36 + .../dslreasoner/smt/reasoner/Logic2SmtMapper.xtend | 1055 ++++++++++++++++++++ .../smt/reasoner/Logic2SmtMapperTrace.xtend | 23 + .../Logic2SmtMapper_UnfoldingSupport.xtend | 33 + .../smt/reasoner/Logic2Smt_TypeMapper.xtend | 38 + .../Logic2Smt_TypeMapper_FilteredTypes.xtend | 501 ++++++++++ ...Logic2Smt_TypeMapper_FilteredTypesSimple.xtend_ | 463 +++++++++ .../reasoner/Logic2Smt_TypeMapper_Horizontal.xtend | 63 ++ .../inf/dslreasoner/smt/reasoner/SMTSolver.xtend | 49 + .../dslreasoner/smt/reasoner/Smt2LogicMapper.xtend | 71 ++ .../smt/reasoner/SmtModelInterpretation.xtend | 167 ++++ .../smt/reasoner/SmtSolverConfiguration.xtend | 9 + .../smt/reasoner/TransformedSubterm.xtend | 183 ++++ .../dslreasoner/smt/reasoner/TypeDescriptor.xtend | 44 + .../smt/reasoner/builder/SmtModelQueryEngine.xtend | 314 ++++++ .../smt/reasoner/builder/SmtSolverHandler.xtend | 64 ++ 57 files changed, 5480 insertions(+) create mode 100644 Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language.ui/.classpath create mode 100644 Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language.ui/.gitignore create mode 100644 Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language.ui/.project create mode 100644 Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language.ui/.settings/org.eclipse.core.resources.prefs create mode 100644 Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language.ui/.settings/org.eclipse.jdt.core.prefs create mode 100644 Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language.ui/META-INF/MANIFEST.MF create mode 100644 Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language.ui/build.properties create mode 100644 Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language.ui/plugin.xml create mode 100644 Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language.ui/plugin.xml_gen create mode 100644 Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language.ui/src/hu/bme/mit/inf/dslreasoner/ui/SmtLanguageUiModule.java create mode 100644 Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language.ui/src/hu/bme/mit/inf/dslreasoner/ui/contentassist/SmtLanguageProposalProvider.xtend create mode 100644 Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language.ui/src/hu/bme/mit/inf/dslreasoner/ui/labeling/SmtLanguageDescriptionLabelProvider.xtend create mode 100644 Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language.ui/src/hu/bme/mit/inf/dslreasoner/ui/labeling/SmtLanguageLabelProvider.xtend create mode 100644 Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language.ui/src/hu/bme/mit/inf/dslreasoner/ui/outline/SmtLanguageOutlineTreeProvider.xtend create mode 100644 Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language.ui/src/hu/bme/mit/inf/dslreasoner/ui/quickfix/SmtLanguageQuickfixProvider.xtend create mode 100644 Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/.classpath create mode 100644 Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/.gitignore create mode 100644 Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/.launch/Generate Language Infrastructure (hu.bme.mit.inf.dslreasoner.smt.language).launch create mode 100644 Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/.project create mode 100644 Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/.settings/org.eclipse.core.resources.prefs create mode 100644 Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/.settings/org.eclipse.jdt.core.prefs create mode 100644 Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/META-INF/MANIFEST.MF create mode 100644 Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/build.properties create mode 100644 Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/model/generated/SmtLanguage.ecore create mode 100644 Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/model/generated/SmtLanguage.genmodel create mode 100644 Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/plugin.xml create mode 100644 Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/plugin.xml_gen create mode 100644 Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/GenerateSmtLanguage.mwe2 create mode 100644 Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/SmtLanguage.xtext create mode 100644 Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/SmtLanguageRuntimeModule.java create mode 100644 Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/SmtLanguageStandaloneSetup.java create mode 100644 Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/formatting/SmtLanguageFormatter.xtend create mode 100644 Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/generator/SmtLanguageGenerator.xtend create mode 100644 Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/scoping/SmtLanguageScopeProvider.xtend create mode 100644 Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/validation/SmtLanguageValidator.xtend create mode 100644 Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/.classpath create mode 100644 Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/.gitignore create mode 100644 Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/.project create mode 100644 Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/.settings/org.eclipse.jdt.core.prefs create mode 100644 Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/META-INF/MANIFEST.MF create mode 100644 Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/build.properties create mode 100644 Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2SMT_TypeMapperInterpretation.xtend create mode 100644 Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2SmtMapper.xtend create mode 100644 Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2SmtMapperTrace.xtend create mode 100644 Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2SmtMapper_UnfoldingSupport.xtend create mode 100644 Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2Smt_TypeMapper.xtend create mode 100644 Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2Smt_TypeMapper_FilteredTypes.xtend create mode 100644 Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2Smt_TypeMapper_FilteredTypesSimple.xtend_ create mode 100644 Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2Smt_TypeMapper_Horizontal.xtend create mode 100644 Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/SMTSolver.xtend create mode 100644 Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Smt2LogicMapper.xtend create mode 100644 Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/SmtModelInterpretation.xtend create mode 100644 Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/SmtSolverConfiguration.xtend create mode 100644 Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/TransformedSubterm.xtend create mode 100644 Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/TypeDescriptor.xtend create mode 100644 Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/builder/SmtModelQueryEngine.xtend create mode 100644 Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/builder/SmtSolverHandler.xtend (limited to 'Solvers/SMT-Solver') diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language.ui/.classpath b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language.ui/.classpath new file mode 100644 index 00000000..1287f96c --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language.ui/.classpath @@ -0,0 +1,9 @@ + + + + + + + + + diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language.ui/.gitignore b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language.ui/.gitignore new file mode 100644 index 00000000..8ae4e44d --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language.ui/.gitignore @@ -0,0 +1,4 @@ +/bin/ +/src-gen/ +/vql-gen/ +/xtend-gen/ diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language.ui/.project b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language.ui/.project new file mode 100644 index 00000000..94d225bf --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language.ui/.project @@ -0,0 +1,34 @@ + + + hu.bme.mit.inf.dslreasoner.smt.language.ui + + + + + + org.eclipse.jdt.core.javabuilder + + + + + org.eclipse.pde.ManifestBuilder + + + + + org.eclipse.pde.SchemaBuilder + + + + + org.eclipse.xtext.ui.shared.xtextBuilder + + + + + + org.eclipse.jdt.core.javanature + org.eclipse.pde.PluginNature + org.eclipse.xtext.ui.shared.xtextNature + + diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language.ui/.settings/org.eclipse.core.resources.prefs b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language.ui/.settings/org.eclipse.core.resources.prefs new file mode 100644 index 00000000..4824b802 --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language.ui/.settings/org.eclipse.core.resources.prefs @@ -0,0 +1,2 @@ +eclipse.preferences.version=1 +encoding/=UTF-8 diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language.ui/.settings/org.eclipse.jdt.core.prefs b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language.ui/.settings/org.eclipse.jdt.core.prefs new file mode 100644 index 00000000..295926d9 --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language.ui/.settings/org.eclipse.jdt.core.prefs @@ -0,0 +1,7 @@ +eclipse.preferences.version=1 +org.eclipse.jdt.core.compiler.codegen.inlineJsrBytecode=enabled +org.eclipse.jdt.core.compiler.codegen.targetPlatform=1.8 +org.eclipse.jdt.core.compiler.compliance=1.8 +org.eclipse.jdt.core.compiler.problem.assertIdentifier=error +org.eclipse.jdt.core.compiler.problem.enumIdentifier=error +org.eclipse.jdt.core.compiler.source=1.8 diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language.ui/META-INF/MANIFEST.MF b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language.ui/META-INF/MANIFEST.MF new file mode 100644 index 00000000..ba28b7ef --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language.ui/META-INF/MANIFEST.MF @@ -0,0 +1,27 @@ +Manifest-Version: 1.0 +Bundle-ManifestVersion: 2 +Bundle-Name: hu.bme.mit.inf.dslreasoner.smt.language.ui +Bundle-Vendor: My Company +Bundle-Version: 1.0.0.qualifier +Bundle-SymbolicName: hu.bme.mit.inf.dslreasoner.smt.language.ui; singleton:=true +Bundle-ActivationPolicy: lazy +Require-Bundle: hu.bme.mit.inf.dslreasoner.smt.language;visibility:=reexport, + org.eclipse.xtext.ui, + org.eclipse.ui.editors;bundle-version="3.5.0", + org.eclipse.ui.ide;bundle-version="3.5.0", + org.eclipse.xtext.ui.shared, + org.eclipse.ui, + org.eclipse.xtext.builder, + org.antlr.runtime, + org.eclipse.xtext.common.types.ui, + org.eclipse.xtext.ui.codetemplates.ui, + org.eclipse.compare, + org.eclipse.xtext.xbase.lib +Import-Package: org.apache.log4j, + org.eclipse.xtext.xbase.lib +Bundle-RequiredExecutionEnvironment: J2SE-1.5 +Export-Package: hu.bme.mit.inf.dslreasoner.ui.quickfix, + hu.bme.mit.inf.dslreasoner.ui.contentassist, + hu.bme.mit.inf.dslreasoner.ui.contentassist.antlr, + hu.bme.mit.inf.dslreasoner.ui.internal +Bundle-Activator: hu.bme.mit.inf.dslreasoner.ui.internal.SmtLanguageActivator diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language.ui/build.properties b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language.ui/build.properties new file mode 100644 index 00000000..31255ed0 --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language.ui/build.properties @@ -0,0 +1,6 @@ +source.. = src/,\ + src-gen/,\ + xtend-gen/ +bin.includes = META-INF/,\ + .,\ + plugin.xml \ No newline at end of file diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language.ui/plugin.xml b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language.ui/plugin.xml new file mode 100644 index 00000000..2602c957 --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language.ui/plugin.xml @@ -0,0 +1,398 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language.ui/plugin.xml_gen b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language.ui/plugin.xml_gen new file mode 100644 index 00000000..4edb0697 --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language.ui/plugin.xml_gen @@ -0,0 +1,398 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language.ui/src/hu/bme/mit/inf/dslreasoner/ui/SmtLanguageUiModule.java b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language.ui/src/hu/bme/mit/inf/dslreasoner/ui/SmtLanguageUiModule.java new file mode 100644 index 00000000..371ccec5 --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language.ui/src/hu/bme/mit/inf/dslreasoner/ui/SmtLanguageUiModule.java @@ -0,0 +1,15 @@ +/* + * generated by Xtext + */ +package hu.bme.mit.inf.dslreasoner.ui; + +import org.eclipse.ui.plugin.AbstractUIPlugin; + +/** + * Use this class to register components to be used within the IDE. + */ +public class SmtLanguageUiModule extends hu.bme.mit.inf.dslreasoner.ui.AbstractSmtLanguageUiModule { + public SmtLanguageUiModule(AbstractUIPlugin plugin) { + super(plugin); + } +} diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language.ui/src/hu/bme/mit/inf/dslreasoner/ui/contentassist/SmtLanguageProposalProvider.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language.ui/src/hu/bme/mit/inf/dslreasoner/ui/contentassist/SmtLanguageProposalProvider.xtend new file mode 100644 index 00000000..b00cbdfa --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language.ui/src/hu/bme/mit/inf/dslreasoner/ui/contentassist/SmtLanguageProposalProvider.xtend @@ -0,0 +1,12 @@ +/* + * generated by Xtext + */ +package hu.bme.mit.inf.dslreasoner.ui.contentassist + +import hu.bme.mit.inf.dslreasoner.ui.contentassist.AbstractSmtLanguageProposalProvider + +/** + * see http://www.eclipse.org/Xtext/documentation.html#contentAssist on how to customize content assistant + */ +class SmtLanguageProposalProvider extends AbstractSmtLanguageProposalProvider { +} diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language.ui/src/hu/bme/mit/inf/dslreasoner/ui/labeling/SmtLanguageDescriptionLabelProvider.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language.ui/src/hu/bme/mit/inf/dslreasoner/ui/labeling/SmtLanguageDescriptionLabelProvider.xtend new file mode 100644 index 00000000..1aa3189f --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language.ui/src/hu/bme/mit/inf/dslreasoner/ui/labeling/SmtLanguageDescriptionLabelProvider.xtend @@ -0,0 +1,24 @@ +/* +* generated by Xtext +*/ +package hu.bme.mit.inf.dslreasoner.ui.labeling + +//import org.eclipse.xtext.resource.IEObjectDescription + +/** + * Provides labels for a IEObjectDescriptions and IResourceDescriptions. + * + * see http://www.eclipse.org/Xtext/documentation.html#labelProvider + */ +class SmtLanguageDescriptionLabelProvider extends org.eclipse.xtext.ui.label.DefaultDescriptionLabelProvider { + + // Labels and icons can be computed like this: + +// override text(IEObjectDescription ele) { +// ele.name.toString +// } +// +// override image(IEObjectDescription ele) { +// ele.EClass.name + '.gif' +// } +} diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language.ui/src/hu/bme/mit/inf/dslreasoner/ui/labeling/SmtLanguageLabelProvider.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language.ui/src/hu/bme/mit/inf/dslreasoner/ui/labeling/SmtLanguageLabelProvider.xtend new file mode 100644 index 00000000..3d26adea --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language.ui/src/hu/bme/mit/inf/dslreasoner/ui/labeling/SmtLanguageLabelProvider.xtend @@ -0,0 +1,29 @@ +/* +* generated by Xtext +*/ +package hu.bme.mit.inf.dslreasoner.ui.labeling + +import com.google.inject.Inject + +/** + * Provides labels for a EObjects. + * + * see http://www.eclipse.org/Xtext/documentation.html#labelProvider + */ +class SmtLanguageLabelProvider extends org.eclipse.xtext.ui.label.DefaultEObjectLabelProvider { + + @Inject + new(org.eclipse.emf.edit.ui.provider.AdapterFactoryLabelProvider delegate) { + super(delegate); + } + + // Labels and icons can be computed like this: + +// def text(Greeting ele) { +// 'A greeting to ' + ele.name +// } +// +// def image(Greeting ele) { +// 'Greeting.gif' +// } +} diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language.ui/src/hu/bme/mit/inf/dslreasoner/ui/outline/SmtLanguageOutlineTreeProvider.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language.ui/src/hu/bme/mit/inf/dslreasoner/ui/outline/SmtLanguageOutlineTreeProvider.xtend new file mode 100644 index 00000000..3ad5725a --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language.ui/src/hu/bme/mit/inf/dslreasoner/ui/outline/SmtLanguageOutlineTreeProvider.xtend @@ -0,0 +1,13 @@ +/* +* generated by Xtext +*/ +package hu.bme.mit.inf.dslreasoner.ui.outline + +/** + * Customization of the default outline structure. + * + * see http://www.eclipse.org/Xtext/documentation.html#outline + */ +class SmtLanguageOutlineTreeProvider extends org.eclipse.xtext.ui.editor.outline.impl.DefaultOutlineTreeProvider { + +} diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language.ui/src/hu/bme/mit/inf/dslreasoner/ui/quickfix/SmtLanguageQuickfixProvider.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language.ui/src/hu/bme/mit/inf/dslreasoner/ui/quickfix/SmtLanguageQuickfixProvider.xtend new file mode 100644 index 00000000..7fae2761 --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language.ui/src/hu/bme/mit/inf/dslreasoner/ui/quickfix/SmtLanguageQuickfixProvider.xtend @@ -0,0 +1,26 @@ +/* +* generated by Xtext +*/ +package hu.bme.mit.inf.dslreasoner.ui.quickfix + +//import org.eclipse.xtext.ui.editor.quickfix.Fix +//import org.eclipse.xtext.ui.editor.quickfix.IssueResolutionAcceptor +//import org.eclipse.xtext.validation.Issue + +/** + * Custom quickfixes. + * + * see http://www.eclipse.org/Xtext/documentation.html#quickfixes + */ +class SmtLanguageQuickfixProvider extends org.eclipse.xtext.ui.editor.quickfix.DefaultQuickfixProvider { + +// @Fix(MyDslValidator::INVALID_NAME) +// def capitalizeName(Issue issue, IssueResolutionAcceptor acceptor) { +// acceptor.accept(issue, 'Capitalize name', 'Capitalize the name.', 'upcase.png') [ +// context | +// val xtextDocument = context.xtextDocument +// val firstLetter = xtextDocument.get(issue.offset, 1) +// xtextDocument.replace(issue.offset, 1, firstLetter.toUpperCase) +// ] +// } +} diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/.classpath b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/.classpath new file mode 100644 index 00000000..1287f96c --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/.classpath @@ -0,0 +1,9 @@ + + + + + + + + + diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/.gitignore b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/.gitignore new file mode 100644 index 00000000..8ae4e44d --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/.gitignore @@ -0,0 +1,4 @@ +/bin/ +/src-gen/ +/vql-gen/ +/xtend-gen/ diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/.launch/Generate Language Infrastructure (hu.bme.mit.inf.dslreasoner.smt.language).launch b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/.launch/Generate Language Infrastructure (hu.bme.mit.inf.dslreasoner.smt.language).launch new file mode 100644 index 00000000..e448edbe --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/.launch/Generate Language Infrastructure (hu.bme.mit.inf.dslreasoner.smt.language).launch @@ -0,0 +1,17 @@ + + + + + + + + + + + + + + + + + diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/.project b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/.project new file mode 100644 index 00000000..b4b09620 --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/.project @@ -0,0 +1,34 @@ + + + hu.bme.mit.inf.dslreasoner.smt.language + + + + + + org.eclipse.jdt.core.javabuilder + + + + + org.eclipse.pde.ManifestBuilder + + + + + org.eclipse.pde.SchemaBuilder + + + + + org.eclipse.xtext.ui.shared.xtextBuilder + + + + + + org.eclipse.jdt.core.javanature + org.eclipse.pde.PluginNature + org.eclipse.xtext.ui.shared.xtextNature + + diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/.settings/org.eclipse.core.resources.prefs b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/.settings/org.eclipse.core.resources.prefs new file mode 100644 index 00000000..4824b802 --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/.settings/org.eclipse.core.resources.prefs @@ -0,0 +1,2 @@ +eclipse.preferences.version=1 +encoding/=UTF-8 diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/.settings/org.eclipse.jdt.core.prefs b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/.settings/org.eclipse.jdt.core.prefs new file mode 100644 index 00000000..295926d9 --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/.settings/org.eclipse.jdt.core.prefs @@ -0,0 +1,7 @@ +eclipse.preferences.version=1 +org.eclipse.jdt.core.compiler.codegen.inlineJsrBytecode=enabled +org.eclipse.jdt.core.compiler.codegen.targetPlatform=1.8 +org.eclipse.jdt.core.compiler.compliance=1.8 +org.eclipse.jdt.core.compiler.problem.assertIdentifier=error +org.eclipse.jdt.core.compiler.problem.enumIdentifier=error +org.eclipse.jdt.core.compiler.source=1.8 diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/META-INF/MANIFEST.MF b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/META-INF/MANIFEST.MF new file mode 100644 index 00000000..ec8f78ce --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/META-INF/MANIFEST.MF @@ -0,0 +1,37 @@ +Manifest-Version: 1.0 +Bundle-ManifestVersion: 2 +Bundle-Name: hu.bme.mit.inf.dslreasoner.smt.language +Bundle-Vendor: My Company +Bundle-Version: 1.0.0.qualifier +Bundle-SymbolicName: hu.bme.mit.inf.dslreasoner.smt.language; singleton:=true +Bundle-ActivationPolicy: lazy +Require-Bundle: org.eclipse.xtext;visibility:=reexport, + org.eclipse.xtext.xbase;resolution:=optional;visibility:=reexport, + org.eclipse.xtext.generator;resolution:=optional, + org.apache.commons.logging;bundle-version="1.0.4";resolution:=optional, + org.eclipse.emf.codegen.ecore;resolution:=optional, + org.eclipse.emf.mwe.utils;resolution:=optional, + org.eclipse.emf.mwe2.launch;resolution:=optional, + org.eclipse.xtext.util, + org.eclipse.emf.ecore, + org.eclipse.emf.common, + org.antlr.runtime, + org.eclipse.xtext.common.types, + org.objectweb.asm;bundle-version="[5.0.1,6.0.0)";resolution:=optional, + org.eclipse.xtext.xbase.lib +Import-Package: org.apache.log4j, + org.eclipse.xtext.xbase.lib +Bundle-RequiredExecutionEnvironment: J2SE-1.5 +Export-Package: hu.bme.mit.inf.dslreasoner, + hu.bme.mit.inf.dslreasoner.services, + hu.bme.mit.inf.dslreasoner.smtLanguage, + hu.bme.mit.inf.dslreasoner.smtLanguage.impl, + hu.bme.mit.inf.dslreasoner.smtLanguage.util, + hu.bme.mit.inf.dslreasoner.serializer, + hu.bme.mit.inf.dslreasoner.parser.antlr, + hu.bme.mit.inf.dslreasoner.parser.antlr.internal, + hu.bme.mit.inf.dslreasoner.validation, + hu.bme.mit.inf.dslreasoner.scoping, + hu.bme.mit.inf.dslreasoner.generator, + hu.bme.mit.inf.dslreasoner.formatting + diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/build.properties b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/build.properties new file mode 100644 index 00000000..07a42688 --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/build.properties @@ -0,0 +1,7 @@ +source.. = src/,\ + src-gen/,\ + xtend-gen/ +bin.includes = model/,\ + META-INF/,\ + .,\ + plugin.xml \ No newline at end of file diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/model/generated/SmtLanguage.ecore b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/model/generated/SmtLanguage.ecore new file mode 100644 index 00000000..e49cb530 --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/model/generated/SmtLanguage.ecore @@ -0,0 +1,304 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/model/generated/SmtLanguage.genmodel b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/model/generated/SmtLanguage.genmodel new file mode 100644 index 00000000..500f4dae --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/model/generated/SmtLanguage.genmodel @@ -0,0 +1,238 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/plugin.xml b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/plugin.xml new file mode 100644 index 00000000..fea6dabe --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/plugin.xml @@ -0,0 +1,16 @@ + + + + + + + + + + + + + diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/plugin.xml_gen b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/plugin.xml_gen new file mode 100644 index 00000000..3665b60a --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/plugin.xml_gen @@ -0,0 +1,16 @@ + + + + + + + + + + + + + diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/GenerateSmtLanguage.mwe2 b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/GenerateSmtLanguage.mwe2 new file mode 100644 index 00000000..e27dbd64 --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/GenerateSmtLanguage.mwe2 @@ -0,0 +1,133 @@ +module hu.bme.mit.inf.dslreasoner.GenerateSmtLanguage + +import org.eclipse.emf.mwe.utils.* +import org.eclipse.xtext.generator.* +import org.eclipse.xtext.ui.generator.* + +var grammarURI = "classpath:/hu/bme/mit/inf/dslreasoner/SmtLanguage.xtext" +var fileExtensions = "smt2" +var projectName = "hu.bme.mit.inf.dslreasoner.smt.language" +var runtimeProject = "../${projectName}" +var generateXtendStub = true +var encoding = "UTF-8" + +Workflow { + bean = StandaloneSetup { + scanClassPath = true + platformUri = "${runtimeProject}/.." + // The following two lines can be removed, if Xbase is not used. + registerGeneratedEPackage = "org.eclipse.xtext.xbase.XbasePackage" + registerGenModelFile = "platform:/resource/org.eclipse.xtext.xbase/model/Xbase.genmodel" + } + + component = DirectoryCleaner { + directory = "${runtimeProject}/src-gen" + } + + component = DirectoryCleaner { + directory = "${runtimeProject}/model/generated" + } + + component = DirectoryCleaner { + directory = "${runtimeProject}.ui/src-gen" + } + + component = DirectoryCleaner { + directory = "${runtimeProject}.tests/src-gen" + } + + component = Generator { + pathRtProject = runtimeProject + pathUiProject = "${runtimeProject}.ui" + //pathTestProject = "${runtimeProject}.tests" + projectNameRt = projectName + projectNameUi = "${projectName}.ui" + encoding = encoding + language = auto-inject { + uri = grammarURI + + // Java API to access grammar elements (required by several other fragments) + fragment = grammarAccess.GrammarAccessFragment auto-inject {} + + // generates Java API for the generated EPackages + fragment = ecore.EMFGeneratorFragment auto-inject {} + + // the old serialization component + // fragment = parseTreeConstructor.ParseTreeConstructorFragment auto-inject {} + + // serializer 2.0 + fragment = serializer.SerializerFragment auto-inject { + generateStub = false + } + + // a custom ResourceFactory for use with EMF + fragment = resourceFactory.ResourceFactoryFragment auto-inject {} + + // The antlr parser generator fragment. + fragment = parser.antlr.XtextAntlrGeneratorFragment auto-inject { + // options = { + // backtrack = true + // } + } + + // Xtend-based API for validation + fragment = validation.ValidatorFragment auto-inject { + // composedCheck = "org.eclipse.xtext.validation.ImportUriValidator" + // composedCheck = "org.eclipse.xtext.validation.NamesAreUniqueValidator" + } + + // old scoping and exporting API + // fragment = scoping.ImportURIScopingFragment auto-inject {} + // fragment = exporting.SimpleNamesFragment auto-inject {} + + // scoping and exporting API + fragment = scoping.ImportNamespacesScopingFragment auto-inject {} + fragment = exporting.QualifiedNamesFragment auto-inject {} + fragment = builder.BuilderIntegrationFragment auto-inject {} + + // generator API + fragment = generator.GeneratorFragment auto-inject {} + + // formatter API + fragment = formatting.FormatterFragment auto-inject {} + + // labeling API + fragment = labeling.LabelProviderFragment auto-inject {} + + // outline API + fragment = outline.OutlineTreeProviderFragment auto-inject {} + fragment = outline.QuickOutlineFragment auto-inject {} + + // quickfix API + fragment = quickfix.QuickfixProviderFragment auto-inject {} + + // content assist API + fragment = contentAssist.ContentAssistFragment auto-inject {} + + // generates a more lightweight Antlr parser and lexer tailored for content assist + fragment = parser.antlr.XtextAntlrUiGeneratorFragment auto-inject {} + + // generates junit test support classes into Generator#pathTestProject + //fragment = junit.Junit4Fragment auto-inject {} + + // rename refactoring + fragment = refactoring.RefactorElementNameFragment auto-inject {} + + // provides the necessary bindings for java types integration + fragment = types.TypesGeneratorFragment auto-inject {} + + // generates the required bindings only if the grammar inherits from Xbase + fragment = xbase.XbaseGeneratorFragment auto-inject {} + + // generates the required bindings only if the grammar inherits from Xtype + fragment = xbase.XtypeGeneratorFragment auto-inject {} + + // provides a preference page for template proposals + fragment = templates.CodetemplatesGeneratorFragment auto-inject {} + + // provides a compare view + fragment = compare.CompareFragment auto-inject {} + } + } +} + diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/SmtLanguage.xtext b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/SmtLanguage.xtext new file mode 100644 index 00000000..320e1cfe --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/SmtLanguage.xtext @@ -0,0 +1,222 @@ +grammar hu.bme.mit.inf.dslreasoner.SmtLanguage with org.eclipse.xtext.common.Terminals + +generate smtLanguage "http://www.bme.hu/mit/inf/dslreasoner/SmtLanguage" + +import "http://www.eclipse.org/emf/2002/Ecore" as ecore + +SMTDocument: + input=SMTInput + ( + '--------------' + output=SMTOutput + )?; + +SMTInput: + (options += SMTOption)* + ( + typeDeclarations+=SMTType | + functionDeclarations+=SMTFunctionDeclaration | + functionDefinition+=SMTFunctionDefinition | + assertions += SMTAssertion + )* + satCommand = SMTSatCommand + getModelCommand = SMTGetModelCommand; + +SMTOutput:( + (satResult = SMTResult + getModelResult = SMTResult) | 'timeout' {SMTOutput}) + statistics=SMTStatisticsSection?; + +////////////////////////////////// +// SMT terminals +////////////////////////////////// + +terminal SL_COMMENT : ';' !('\n'|'\r')* ('\r'? '\n')?; + +terminal ID : ('a'..'z'|'A'..'Z'|'_') ('a'..'z'|'A'..'Z'|'_'|'-'|'!'|'0'..'9')*; +// ('a'..'z'|'A'..'Z'|'_'/*|'+'|'-'|'/'|'*'|'='|'%'|'?'|'!'|'.'|'$'|'~'|'&'/*|'^'*/|'<'|'>'/*|'@'*/) +// ('a'..'z'|'A'..'Z'|'_'/*|'+'|'-'|'/'|'*'|'='|'%'|'?'|'!'|'.'|'$'|'~'|'&'/*|'^'|*/'<'|'>'/*|'@'*/|'0'..'9')* +SMTID: ID; + +terminal PROPERTYNAME : ':' + ID; +terminal REAL returns ecore::EBigDecimal: INT '.' INT; + +////////////////////////////////// +// Options +////////////////////////////////// +SMTOption: '(' 'set-option' name = PROPERTYNAME value = SMTAtomicTerm ')'; + +////////////////////////////////// +// Type declarations +////////////////////////////////// +SMTType: SMTEnumeratedTypeDeclaration | SMTSetTypeDeclaration; + +SMTEnumLiteral: name = SMTID; +SMTEnumeratedTypeDeclaration: '(' 'declare-datatypes' '(' ')' '(' '(' name = SMTID elements+=SMTEnumLiteral+ ')' ')' ')'; +SMTSetTypeDeclaration: '(' 'declare-sort' name = SMTID ')'; + +SMTTypeReference: SMTComplexTypeReference | SMTPrimitiveTypeReference; +SMTComplexTypeReference: referred = [SMTType]; +SMTPrimitiveTypeReference: SMTIntTypeReference | SMTBoolTypeReference | SMTRealTypeReference; + +SMTIntTypeReference: {SMTIntTypeReference} "Int"; +SMTBoolTypeReference: {SMTBoolTypeReference} "Bool"; +SMTRealTypeReference: {SMTRealTypeReference} "Real"; + +////////////////////////////////// +// Functions and constants +////////////////////////////////// + +SMTFunctionDeclaration: '(' 'declare-fun' name = SMTID '(' parameters+=SMTTypeReference* ')' range = SMTTypeReference ')'; + +/*DeclaredFunctionDefinition: + '(' 'define-fun' declaration=[Function] '(' parameters+=SortedVariable* ')' range = TypeReference value = Term ')';*/ + +SMTFunctionDefinition: + '(' 'define-fun' name=SMTID '(' parameters+=SMTSortedVariable* ')' range = SMTTypeReference value = SMTTerm ')'; + + +////////////////////////////////// +// Expressions +////////////////////////////////// +SMTTerm: + SMTSymbolicValue| + SMTAtomicTerm | + SMTBoolOperation | + SMTIntOperation | + SMTITE | + SMTLet | + SMTRelation | + SMTQuantifiedExpression; + +SMTSymbolicDeclaration: SMTFunctionDeclaration | SMTFunctionDefinition | SMTSortedVariable | SMTEnumLiteral | SMTInlineConstantDefinition; + +SMTSymbolicValue: + '(' symbolicReference = [SMTSymbolicDeclaration] ( parameterSubstitutions += SMTTerm )+ ')' | + symbolicReference = [SMTSymbolicDeclaration]; + +SMTAtomicTerm: SMTIntLiteral | SMTBoolLiteral | SMTRealLiteral; +SMTIntLiteral: value=INT; +BOOLEANTERMINAL returns ecore::EBoolean: 'true' | 'false'; +SMTBoolLiteral: value=BOOLEANTERMINAL; +SMTRealLiteral: value=REAL; + +// Quantified operations +SMTSortedVariable: '(' name = SMTID range = SMTTypeReference ')'; +//QuantifiedVariableValue: variable = [QuantifiedVariable]; + +SMTQuantifiedExpression: SMTExists | SMTForall; +SMTExists: '(' 'exists' '(' (quantifiedVariables += SMTSortedVariable)+ ')' + (expression=SMTTerm | ('(' '!' expression = SMTTerm ':pattern' '(' pattern = SMTTerm ')' ')')) ')' +; +SMTForall: '(' 'forall' '(' (quantifiedVariables += SMTSortedVariable)+ ')' + (expression=SMTTerm | ('(' '!' expression = SMTTerm ':pattern' '(' pattern = SMTTerm ')' ')')) ')' +; + +// Boolean operations +SMTBoolOperation: SMTAnd | SMTOr | SMTImpl | SMTNot | SMTIff; +SMTAnd: '(' 'and' operands+=SMTTerm+ ')'; +SMTOr: '(' 'or' operands+=SMTTerm+ ')'; +SMTImpl: '(' '=>' leftOperand=SMTTerm rightOperand=SMTTerm ')'; +SMTNot: '(' 'not' operand=SMTTerm ')'; +SMTIff: '(' 'iff' leftOperand=SMTTerm rightOperand=SMTTerm ')'; + +// If-then-else +SMTITE: '(' 'ite' condition = SMTTerm if=SMTTerm else = SMTTerm ')'; + +//Let +SMTLet: '(' 'let' '(' (inlineConstantDefinitions+=SMTInlineConstantDefinition)+ ')' term=SMTTerm ')'; +SMTInlineConstantDefinition: + '(' name=SMTID definition=SMTTerm ')' +; + +// Relations +SMTRelation: SMTEquals | SMTDistinct | SMTLT | SMTMT | SMTLEQ | SMTMEQ; +SMTEquals: '(' '=' leftOperand=SMTTerm rightOperand=SMTTerm ')'; +SMTDistinct: '(' 'distinct' operands+=SMTTerm+ ')'; +SMTLT: '(' '<' leftOperand=SMTTerm rightOperand=SMTTerm ')'; +SMTMT: '(' '>' leftOperand=SMTTerm rightOperand=SMTTerm ')'; +SMTLEQ: '(' '<=' leftOperand=SMTTerm rightOperand=SMTTerm ')'; +SMTMEQ: '(' '>=' leftOperand=SMTTerm rightOperand=SMTTerm ')'; + +// Int operations +SMTIntOperation: SMTPlus | SMTMinus | SMTMultiply | SMTDivison | SMTDiv | SMTMod; +SMTPlus: '(' '+' leftOperand=SMTTerm rightOperand=SMTTerm ')'; +SMTMinus: '(' '-' leftOperand=SMTTerm (rightOperand=SMTTerm)? ')'; +SMTMultiply: '(' '*' leftOperand=SMTTerm rightOperand=SMTTerm ')'; +SMTDivison: '(' '/' leftOperand=SMTTerm rightOperand=SMTTerm ')'; +SMTDiv: '(' 'div' leftOperand=SMTTerm rightOperand=SMTTerm ')'; +SMTMod: '(' 'mod' leftOperand=SMTTerm rightOperand=SMTTerm ')'; + +////////////////////////////////// +// Assertion +////////////////////////////////// +SMTAssertion: '(' 'assert' value=SMTTerm ')'; +SMTCardinalityConstraint: + '(' 'forall' '(' '(' ID type=SMTTypeReference ')' ')' + (('(' 'or'('(' '=' ID elements+=SMTSymbolicValue ')')* ')') | // With multiple element + ('(' '=' ID elements+=SMTSymbolicValue ')')) //With single element + ')' +; + +////////////////////////////////// +// Goals +////////////////////////////////// +SMTSatCommand: SMTSimpleSatCommand | SMTComplexSatCommand; +SMTSimpleSatCommand : '(' 'check-sat' {SMTSimpleSatCommand} ')'; +SMTComplexSatCommand: '(' 'check-sat-using' method = SMTReasoningTactic ')'; +SMTGetModelCommand: '(' 'get-model' {SMTGetModelCommand} ')'; + +SMTReasoningTactic: SMTBuiltinTactic | SMTReasoningCombinator; +SMTBuiltinTactic: name = ID; +SMTReasoningCombinator: + SMTAndThenCombinator | SMTOrElseCombinator | SMTParOrCombinator | SMTParThenCombinator | SMTTryForCombinator | + SMTIfCombinator | SMTWhenCombinator | SMTFailIfCombinator | SMTUsingParamCombinator +; +// executes the given tactics sequencially. +SMTAndThenCombinator: '(' 'and-then' (tactics+=SMTReasoningTactic)+ ')'; +// tries the given tactics in sequence until one of them succeeds. +SMTOrElseCombinator: '(' 'or-else' (tactics+=SMTReasoningTactic)+ ')'; +// executes the given tactics in parallel until one of them succeeds. +SMTParOrCombinator: '(' 'par-or' (tactics+=SMTReasoningTactic)+ ')'; +// executes tactic1 and then tactic2 to every subgoal produced by tactic1. All subgoals are processed in parallel. +SMTParThenCombinator: '(' 'par-then' preProcessingTactic=SMTReasoningTactic paralellyPostpricessingTactic = SMTReasoningTactic ')'; +// excutes the given tactic for at most milliseconds, it fails if the execution takes more than milliseconds. +SMTTryForCombinator: '(' 'try-for' tactic=SMTReasoningTactic time=INT ')'; +// if evaluates to true, then execute the first tactic. Otherwise execute the second. +SMTIfCombinator: '(' 'if' probe=ReasoningProbe ifTactic=SMTReasoningTactic elseTactic=SMTReasoningTactic ')'; +// shorthand for (if skip). +SMTWhenCombinator: '(' 'when' probe=ReasoningProbe tactic=SMTReasoningTactic ')'; +// fail if evaluates to true. +SMTFailIfCombinator: '(' 'fail-if' probe=ReasoningProbe ')'; +//executes the given tactic using the given attributes, where ::= . ! is a syntax sugar for using-params. +SMTUsingParamCombinator: '(' ('using-params' | '!') tactic=SMTReasoningTactic (parameters+=ReasoningTacticParameter)* ')'; + +ReasoningProbe: name=ID; +ReasoningTacticParameter: name=PROPERTYNAME value=SMTAtomicTerm; + +////////////////////////////////// +// Result +////////////////////////////////// + +SMTResult: SMTUnsupportedResult | SMTSatResult | SMTModelResult | SMTErrorResult; +SMTErrorResult: '(' 'error' message = STRING ')'; +SMTUnsupportedResult: 'unsupported' ';' command=ID; +SMTSatResult: sat?='sat' | unsat?='unsat' | unknown?='unknown'; +SMTModelResult: {SMTModelResult} '(' 'model' + ( + newFunctionDeclarations+=SMTFunctionDeclaration | + typeDefinitions+=SMTCardinalityConstraint | + newFunctionDefinitions+=SMTFunctionDefinition + )* + ')'; + +////////////////////////////////// +// Statistics +////////////////////////////////// +//IntOrReal returns ecore::EDouble: INT | REAL; + +SMTStatisticValue: SMTStatisticIntValue | SMTStatisticDoubleValue; +SMTStatisticIntValue: name = PROPERTYNAME value=INT; +SMTStatisticDoubleValue: name = PROPERTYNAME value = REAL; +SMTStatisticsSection: '(' {SMTStatisticsSection} values += SMTStatisticValue* ')'; \ No newline at end of file diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/SmtLanguageRuntimeModule.java b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/SmtLanguageRuntimeModule.java new file mode 100644 index 00000000..dabb0c29 --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/SmtLanguageRuntimeModule.java @@ -0,0 +1,11 @@ +/* + * generated by Xtext + */ +package hu.bme.mit.inf.dslreasoner; + +/** + * Use this class to register components to be used at runtime / without the Equinox extension registry. + */ +public class SmtLanguageRuntimeModule extends hu.bme.mit.inf.dslreasoner.AbstractSmtLanguageRuntimeModule { + +} diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/SmtLanguageStandaloneSetup.java b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/SmtLanguageStandaloneSetup.java new file mode 100644 index 00000000..ed297373 --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/SmtLanguageStandaloneSetup.java @@ -0,0 +1,16 @@ +/* +* generated by Xtext +*/ +package hu.bme.mit.inf.dslreasoner; + +/** + * Initialization support for running Xtext languages + * without equinox extension registry + */ +public class SmtLanguageStandaloneSetup extends SmtLanguageStandaloneSetupGenerated{ + + public static void doSetup() { + new SmtLanguageStandaloneSetup().createInjectorAndDoEMFRegistration(); + } +} + diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/formatting/SmtLanguageFormatter.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/formatting/SmtLanguageFormatter.xtend new file mode 100644 index 00000000..9e3e3943 --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/formatting/SmtLanguageFormatter.xtend @@ -0,0 +1,34 @@ +package hu.bme.mit.inf.dslreasoner.formatting + +import org.eclipse.xtext.formatting.impl.AbstractDeclarativeFormatter +import org.eclipse.xtext.formatting.impl.FormattingConfig +import hu.bme.mit.inf.dslreasoner.services.SmtLanguageGrammarAccess + + +/** + * This class contains custom formatting description. + * + * see : http://www.eclipse.org/Xtext/documentation.html#formatting + * on how and when to use it + * + * Also see {@link org.eclipse.xtext.xtext.XtextFormattingTokenSerializer} as an example + */ +class SmtLanguageFormatter extends AbstractDeclarativeFormatter { + +// @Inject extension SmtLanguageGrammarAccess + + override protected void configureFormatting(FormattingConfig c) { + val f = getGrammarAccess as SmtLanguageGrammarAccess + c.setAutoLinewrap(100000); + for(pair : f.findKeywordPairs("(",")")) { + c.setNoSpace().after(pair.getFirst()); + c.setNoSpace().before(pair.getSecond()); + } + c.setLinewrap.after(f.SMTAssertionRule) + c.setLinewrap.after(f.SMTFunctionDeclarationRule) + c.setLinewrap.after(f.SMTFunctionDefinitionRule) + c.setLinewrap.after(f.SMTEnumeratedTypeDeclarationRule) + c.setLinewrap.after(f.SMTSetTypeDeclarationRule) + c.setLinewrap.after(f.SMTOptionRule) + } +} diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/generator/SmtLanguageGenerator.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/generator/SmtLanguageGenerator.xtend new file mode 100644 index 00000000..e61c082e --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/generator/SmtLanguageGenerator.xtend @@ -0,0 +1,24 @@ +/* + * generated by Xtext + */ +package hu.bme.mit.inf.dslreasoner.generator + +import org.eclipse.emf.ecore.resource.Resource +import org.eclipse.xtext.generator.IGenerator +import org.eclipse.xtext.generator.IFileSystemAccess + +/** + * Generates code from your model files on save. + * + * see http://www.eclipse.org/Xtext/documentation.html#TutorialCodeGeneration + */ +class SmtLanguageGenerator implements IGenerator { + + override void doGenerate(Resource resource, IFileSystemAccess fsa) { +// fsa.generateFile('greetings.txt', 'People to greet: ' + +// resource.allContents +// .filter(typeof(Greeting)) +// .map[name] +// .join(', ')) + } +} diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/scoping/SmtLanguageScopeProvider.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/scoping/SmtLanguageScopeProvider.xtend new file mode 100644 index 00000000..e93e0543 --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/scoping/SmtLanguageScopeProvider.xtend @@ -0,0 +1,138 @@ +/* + * generated by Xtext + */ +package hu.bme.mit.inf.dslreasoner.scoping + +import java.util.Set +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSortedVariable +import org.eclipse.emf.ecore.EObject +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTQuantifiedExpression +import java.util.Collections +import java.util.HashSet +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTInlineConstantDefinition +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTLet +import java.util.Collection +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDefinition +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSymbolicValue +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTDocument +import org.eclipse.xtext.scoping.IScope +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSymbolicDeclaration +import org.eclipse.emf.ecore.EReference +import java.util.HashMap +import java.util.Map +import org.eclipse.xtext.scoping.Scopes +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTModelResult +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTComplexTypeReference +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTEnumLiteral +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTEnumeratedTypeDeclaration +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDeclaration + +/** + * This class contains custom scoping description. + * + * see : http://www.eclipse.org/Xtext/documentation.html#scoping + * on how and when to use it + * + */ +class SmtLanguageScopeProvider extends org.eclipse.xtext.scoping.impl.AbstractDeclarativeScopeProvider { + /** + * Search for the first instance of containerType up in the containment hierarchy. + * @param containerType + * @param from + * @return + */ + @SuppressWarnings("unchecked") + def private ContainerType getTop(Class containerType, EObject from){ + var actualLevel = from.eContainer(); + while(actualLevel!=null){ + if(containerType.isInstance(actualLevel)) { return actualLevel as ContainerType} + else { actualLevel = actualLevel.eContainer() } + } + return null; + } + + def private Set getQuantifiedVariables(EObject from) { + //The most inner quantified variables are in this expression: + val quantifiedExpression = getTop(typeof(SMTQuantifiedExpression), from); + if(quantifiedExpression==null) return Collections.emptySet(); + + //The variables can be referred by a symbolic reference + val Set result = new HashSet(quantifiedExpression.getQuantifiedVariables()); + //The variables can defined in an outer quantifier + result.addAll(getQuantifiedVariables(quantifiedExpression)); + //println(result.map[name].join(",")) + return result; + } + + def private Set getInlineConstantDefinitions(EObject from) { + //The most inner quantified variables are in this expression: + val let = getTop(typeof(SMTLet), from); + if(let==null) return Collections.emptySet(); + + //The variables can be referred by a symbolic reference + val result = new HashSet(let.getInlineConstantDefinitions()); + //The variables can defined in an outer quantifier + result.addAll(getInlineConstantDefinitions(let)); + return result; + } + + def private Collection getParameters(SMTSymbolicValue from) { + val functionDefinition = getTop(typeof(SMTFunctionDefinition), from); + if(functionDefinition!=null) { + return functionDefinition.getParameters(); + } + else return Collections.emptySet(); + } + + def private Set getFiniteElements(SMTSymbolicValue value) { + val Set result = new HashSet(); + val document = getTop(typeof(SMTDocument),value) + for(type : document.input.getTypeDeclarations().filter(typeof(SMTEnumeratedTypeDeclaration))) { + result.addAll(type.getElements()); + } + return result; + } + + def private Set getFunctions(SMTSymbolicValue value) { + val document = getTop(typeof(SMTDocument),value); + val input = document.input + var SMTModelResult output = null; + if(document.output != null && document.output.getModelResult instanceof SMTModelResult) { + output = document.output.getModelResult as SMTModelResult + } + + val Map declarations = new HashMap + val Set definitions =new HashSet + + input.functionDeclarations.forEach[declarations.put(it.name,it)] + if(output != null) { + output.newFunctionDeclarations.forEach[declarations.put(it.name,it)] + } + input.functionDefinition.filter[!declarations.containsKey(it.name)].forEach[definitions += it] + if(output != null) { + output.newFunctionDefinitions.filter[!declarations.containsKey(it.name)].forEach[definitions += it] + } + + val referrables = new HashSet; + referrables.addAll(declarations.values) + referrables.addAll(definitions) + return referrables + } + + def public IScope scope_SMTSymbolicValue_symbolicReference(SMTSymbolicValue value, EReference ref) { + val Set referrables = new HashSet; + + referrables.addAll(value.getFiniteElements) + referrables.addAll(value.getParameters) + referrables.addAll(value.getFunctions) + referrables.addAll(value.getQuantifiedVariables) + referrables.addAll(value.getInlineConstantDefinitions) + + return Scopes.scopeFor(referrables); + } + + // Any type defined in the input section can be referred. + def public IScope scope_SMTComplexTypeReference_referred(SMTComplexTypeReference reference, EReference ref){ + return Scopes.scopeFor(getTop(typeof(SMTDocument),reference).input.typeDeclarations) + } +} diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/validation/SmtLanguageValidator.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/validation/SmtLanguageValidator.xtend new file mode 100644 index 00000000..2ae6130f --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.language/src/hu/bme/mit/inf/dslreasoner/validation/SmtLanguageValidator.xtend @@ -0,0 +1,24 @@ +/* + * generated by Xtext + */ +package hu.bme.mit.inf.dslreasoner.validation +//import org.eclipse.xtext.validation.Check + +/** + * Custom validation rules. + * + * see http://www.eclipse.org/Xtext/documentation.html#validation + */ +class SmtLanguageValidator extends AbstractSmtLanguageValidator { + +// public static val INVALID_NAME = 'invalidName' +// +// @Check +// def checkGreetingStartsWithCapital(Greeting greeting) { +// if (!Character.isUpperCase(greeting.name.charAt(0))) { +// warning('Name should start with a capital', +// MyDslPackage.Literals.GREETING__NAME, +// INVALID_NAME) +// } +// } +} diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/.classpath b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/.classpath new file mode 100644 index 00000000..7e444723 --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/.classpath @@ -0,0 +1,8 @@ + + + + + + + + diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/.gitignore b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/.gitignore new file mode 100644 index 00000000..8ae4e44d --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/.gitignore @@ -0,0 +1,4 @@ +/bin/ +/src-gen/ +/vql-gen/ +/xtend-gen/ diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/.project b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/.project new file mode 100644 index 00000000..00f0576a --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/.project @@ -0,0 +1,34 @@ + + + hu.bme.mit.inf.dslreasoner.smt.reasoner + + + + + + org.eclipse.xtext.ui.shared.xtextBuilder + + + + + org.eclipse.jdt.core.javabuilder + + + + + org.eclipse.pde.ManifestBuilder + + + + + org.eclipse.pde.SchemaBuilder + + + + + + org.eclipse.pde.PluginNature + org.eclipse.jdt.core.javanature + org.eclipse.xtext.ui.shared.xtextNature + + diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/.settings/org.eclipse.jdt.core.prefs b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/.settings/org.eclipse.jdt.core.prefs new file mode 100644 index 00000000..295926d9 --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/.settings/org.eclipse.jdt.core.prefs @@ -0,0 +1,7 @@ +eclipse.preferences.version=1 +org.eclipse.jdt.core.compiler.codegen.inlineJsrBytecode=enabled +org.eclipse.jdt.core.compiler.codegen.targetPlatform=1.8 +org.eclipse.jdt.core.compiler.compliance=1.8 +org.eclipse.jdt.core.compiler.problem.assertIdentifier=error +org.eclipse.jdt.core.compiler.problem.enumIdentifier=error +org.eclipse.jdt.core.compiler.source=1.8 diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/META-INF/MANIFEST.MF b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/META-INF/MANIFEST.MF new file mode 100644 index 00000000..a7f26476 --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/META-INF/MANIFEST.MF @@ -0,0 +1,12 @@ +Manifest-Version: 1.0 +Bundle-ManifestVersion: 2 +Bundle-Name: Solver +Bundle-SymbolicName: hu.bme.mit.inf.dslreasoner.smt.reasoner +Bundle-Version: 1.0.0.qualifier +Bundle-RequiredExecutionEnvironment: JavaSE-1.8 +Require-Bundle: hu.bme.mit.inf.dslreasoner.smt.language;bundle-version="1.0.0", + hu.bme.mit.inf.dslreasoner.logic.model;bundle-version="1.0.0", + org.eclipse.viatra.query.runtime;bundle-version="1.5.0", + org.eclipse.viatra.query.runtime.base.itc;bundle-version="1.5.0", + org.eclipse.viatra.query.tooling.core;bundle-version="1.5.0" +Export-Package: hu.bme.mit.inf.dslreasoner.smt.reasoner diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/build.properties b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/build.properties new file mode 100644 index 00000000..d6c49e5c --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/build.properties @@ -0,0 +1,5 @@ +source.. = src/,\ + xtend-gen/ +output.. = bin/ +bin.includes = META-INF/,\ + . diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2SMT_TypeMapperInterpretation.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2SMT_TypeMapperInterpretation.xtend new file mode 100644 index 00000000..44708f44 --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2SMT_TypeMapperInterpretation.xtend @@ -0,0 +1,36 @@ +package hu.bme.mit.inf.dslreasoner.smt.reasoner + +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSymbolicDeclaration +import java.util.List +import java.util.Map +import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* + +class Logic2SMT_TypeMapperInterpretation { + + val Map> type2Elements + val Map logic2smt + val Map smt2logic + + public new( + Map> type2Elements, + Map logic2smt, + Map smt2logic) { + this.type2Elements = type2Elements + this.logic2smt = logic2smt + this.smt2logic = smt2logic + } + + public def getElements(Type type) { + return type2Elements.get(type) + } + + public def ValueType logicElement2Smt(DefinedElement element) { + return element.lookup(this.logic2smt) + } + + public def smtElement2Logic(SMTSymbolicDeclaration element) { + return element.lookup(this.smt2logic) + } +} diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2SmtMapper.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2SmtMapper.xtend new file mode 100644 index 00000000..aad43716 --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2SmtMapper.xtend @@ -0,0 +1,1055 @@ +package hu.bme.mit.inf.dslreasoner.smt.reasoner + +import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput +import hu.bme.mit.inf.dslreasoner.logic.model.builder.TypeScopes +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Assertion +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolLiteral +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDefinition +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Distinct +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Divison +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Equals +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Exists +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Forall +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Function +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDefinition +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IfThenElse +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Iff +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Impl +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.InstanceOf +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntLiteral +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntTypeReference +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LessOrEqualThan +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LessThan +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Minus +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Mod +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.MoreOrEqualThan +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.MoreThan +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Multiply +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Not +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Or +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Plus +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.QuantifiedExpression +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealLiteral +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTAnd +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTAssertion +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTBoolTypeReference +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTComplexTypeReference +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTDocument +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTInput +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTIntTypeReference +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTOr +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTQuantifiedExpression +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTRealTypeReference +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTReasoningTactic +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSortedVariable +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSymbolicValue +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTTerm +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTType +import hu.bme.mit.inf.dslreasoner.smtLanguage.SmtLanguageFactory +import java.util.ArrayList +import java.util.HashMap +import java.util.LinkedHashMap +import java.util.LinkedList +import java.util.List +import java.util.Map +import org.eclipse.emf.ecore.EObject +import org.eclipse.emf.ecore.util.EcoreUtil +import org.eclipse.xtend.lib.annotations.Accessors +import org.eclipse.xtext.xbase.lib.Functions.Function0 +import org.eclipse.xtext.xbase.lib.Functions.Function1 +import org.eclipse.xtext.xbase.lib.Functions.Function2 +import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDefinition +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy +import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder + +class Logic2SmtMapper{ + val extension SmtLanguageFactory factory = SmtLanguageFactory.eINSTANCE + val Logic2SmtMapper_UnfoldingSupport unfolder = new Logic2SmtMapper_UnfoldingSupport + @Accessors val Logic2Smt_TypeMapper typeMapper; + + LogicProblemBuilder b + + new(Logic2Smt_TypeMapper typeMapper) { + this.typeMapper = typeMapper + } + + public def TracedOutput transformProblem(LogicProblem problem, TypeScopes scope, SMTReasoningTactic strategy) { + val documentInput = createSMTInput => [getModelCommand = createSMTGetModelCommand] + if(strategy == null) documentInput.satCommand = createSMTSimpleSatCommand + else documentInput.satCommand = createSMTComplexSatCommand => [it.method = EcoreUtil.copy(strategy)] + + val document = createSMTDocument => [input = documentInput] + val trace = new Logic2SmtMapperTrace => [ + it.forwardMapper = this + it.problem = problem + ] + // Trafo + this.typeMapper.transformTypes(documentInput,problem,trace, scope) + problem.functions.filter(FunctionDeclaration).forEach[it.transformFunctionDeclaration(documentInput,trace)] + problem.functions.filter(FunctionDefinition) .forEach[it.transformFunctionDefinition(documentInput,trace)] + problem.relations.filter(RelationDeclaration).forEach[it.transformRelationDeclaration(documentInput,trace)] + problem.relations.filter(RelationDefinition) .forEach[it.transformRelationDefinition(documentInput,trace)] + problem.constants.filter(ConstantDeclaration).forEach[it.transformConstantDeclaration(documentInput,trace)] + problem.constants.filter(ConstantDefinition) .forEach[it.transformConstantDefinition(documentInput,trace)] + + problem.relations.filter(RelationDefinition).forEach[it.transformRelationDefinition_definition(documentInput,trace)] + documentInput.assertions += problem.assertions.map[transformAssertion(trace)] + // End trafo + + document.input.assertions.forEach[it.value.nameAllUnnamedVariable] + document.input.functionDefinition.forEach[it.value.nameAllUnnamedVariable] + document.cleanDocument + return new TracedOutput(document,trace) + } + + private def toID(String name) {name.split("\\s+").join("!") } + + private def nameAllUnnamedVariable(SMTTerm root) { + var index = 1 + val unnamedVariables = root.eAllContents.filter(SMTSortedVariable).filter[it.name == null].toList + for(unnamedVariable : unnamedVariables) { + unnamedVariable.name = '''var«index++»''' + } + } + +// def protected maxIntegerRageDefiniton(SMTInput documentInput) { +// val upperlimit = createSMTFunctionDeclaration +// } + + def dispatch protected List transformTypeReference(BoolTypeReference boolTypeReference, Logic2SmtMapperTrace trace) { + return #[new TypeConstraint(createSMTBoolTypeReference,null)] + } + def dispatch protected List transformTypeReference(IntTypeReference intTypeReference, Logic2SmtMapperTrace trace) { + return #[new TypeConstraint(createSMTIntTypeReference,null)] + } + def dispatch protected List transformTypeReference(RealTypeReference realTypeReference, Logic2SmtMapperTrace trace) { + return #[new TypeConstraint(createSMTRealTypeReference,null)] + } + def dispatch protected List transformTypeReference(ComplexTypeReference complexTypeReference, Logic2SmtMapperTrace trace) { + return typeMapper.transformTypeReference(complexTypeReference.referred,trace) + } + + /////////////////////////////////////////////////////// + // Definitions + /////////////////////////////////////////////////////// + + def transformFunctionDeclaration(FunctionDeclaration function, SMTInput input, Logic2SmtMapperTrace trace) { + val parameterTypeCombinations = unfolder.getPermutations(function.parameters.map[x|transformTypeReference(x,trace)]) + val rangeTypeCombinations = function.range.transformTypeReference(trace) + + if(rangeTypeCombinations.size == 1) { + val rangeType = rangeTypeCombinations.head + // Map it as function + var index = 1 + for(combination : parameterTypeCombinations) { + val nameWithIndex = if (parameterTypeCombinations.size > 1) + toID('''function «function.name.toID» «index++»''') + else + toID('''function «function.name.toID»''') + + createFunctionDeclaration(function,nameWithIndex,combination,rangeType,true, input,trace) + } + } else { + // Map it as a relation + var index = 1 + for(combination : parameterTypeCombinations) { + val type2function = new HashMap + for(rangeType : rangeTypeCombinations) { + val nameWithIndex = toID('''function «function.name.toID» «index++»''') + val f = createFunctionDeclaration(function,nameWithIndex,combination,rangeType,false,input,trace) + type2function.put(rangeType,f) + } + // for all rangeTypes, there is + // 1. at least one range type that satisfies the relation + input.assertions+=createSMTAssertion => [ + it.value = createSMTForall => [f| + var paramIndex = 1 + for(param : combination) { + val paramName = '''p«paramIndex++»''' + val variable = createSMTSortedVariable => [ + it.name = paramName + it.range = param.type + ] + f.quantifiedVariables += variable + } + f.expression = createSMTOr => [ + operands+=rangeTypeCombinations.map[t| + createSMTExists => [ + val v = createSMTSortedVariable => [ + it.name = "r" + it.range = EcoreUtil.copy(t.type) + ] + it.quantifiedVariables += v + it.expression = createSMTSymbolicValue => [ + it.symbolicReference = type2function.get(t) + it.parameterSubstitutions += f.quantifiedVariables.map[fv| + createSMTSymbolicValue => [it.symbolicReference = fv] + ] + it.parameterSubstitutions += createSMTSymbolicValue => [it.symbolicReference = v] + ] + ] + ] + ] + ] + ] + // 2. at most one range type that satisfies the relation + // TODO a + } + } + } + + private def createFunctionDeclaration( + Function function, + String nameWithIndex, + List combination, + TypeConstraint rangeType, + boolean useFunction, + SMTInput input, + Logic2SmtMapperTrace trace + ) { + val smtFunction = if(useFunction) { + createSMTFunctionDeclaration => [ + it.name = nameWithIndex + it.parameters += combination.map[it.type] + it.range = rangeType.type + ] + } else { + createSMTFunctionDeclaration => [ + it.name = nameWithIndex + it.parameters += combination.map[it.type] + it.parameters += rangeType.type + it.range = createSMTBoolTypeReference + ] + } + + val descriptor = new Descriptor((combination+#[rangeType]).toList.map[ + TypeDescriptor.createFromTypeReference(it.type)],function) + trace.functionMap.put(descriptor,smtFunction) + input.functionDeclarations += smtFunction + trace.functionUnfolding.put(function,#[descriptor]) + + if(!useFunction) { + input.assertions += createSMTAssertion => [ + it.value = createSMTForall => [f| + var pi = 0 + for(param : combination) { + val variable = createSMTSortedVariable + variable.name = "p"+pi.toString + variable.range = EcoreUtil.copy(combination.get(pi).type) + f.quantifiedVariables+=variable + pi++ + } + val resultParam1 = createSMTSortedVariable => [ + it.name = "res1" + it.range = EcoreUtil.copy(rangeType.type) + ] + f.quantifiedVariables+=resultParam1 + val resultParam2 = createSMTSortedVariable => [ + it.name = "res2" + it.range = EcoreUtil.copy(rangeType.type) + ] + f.quantifiedVariables+=resultParam2 + f.expression = createSMTImpl => [ + it.leftOperand = createSMTAnd => [ + it.operands += createSMTSymbolicValue => [ + it.symbolicReference = smtFunction + it.parameterSubstitutions += (0.. [it.symbolicReference = f.quantifiedVariables.get(x)]] + it.parameterSubstitutions += createSMTSymbolicValue => [it.symbolicReference = resultParam1] + ] + it.operands += createSMTSymbolicValue => [ + it.symbolicReference = smtFunction + it.parameterSubstitutions += (0.. [it.symbolicReference = f.quantifiedVariables.get(x)]] + it.parameterSubstitutions += createSMTSymbolicValue => [it.symbolicReference = resultParam2] + ] + ] + it.rightOperand = createSMTEquals => [ + it.leftOperand = createSMTSymbolicValue => [it.symbolicReference = resultParam1] + it.rightOperand = createSMTSymbolicValue => [it.symbolicReference = resultParam2] + ] + ] + ] + ] + } + + if(rangeType.constraint != null) { + input.assertions += createSMTAssertion => [ + it.value = createSMTForall => [f| + var pi = 0 + for(param : combination) { + val variable = createSMTSortedVariable + variable.name = "p"+pi.toString + variable.range = EcoreUtil.copy(combination.get(pi).type) + f.quantifiedVariables+=variable + pi++ + } + val resultParam = createSMTSortedVariable => [ + it.name = "res" + it.range = EcoreUtil.copy(rangeType.type) + ] + f.quantifiedVariables += resultParam + f.expression = createSMTImpl => [ + it.leftOperand = if(useFunction) + { + createSMTEquals => [ + leftOperand = createSMTSymbolicValue => [ + it.symbolicReference = smtFunction + it.parameterSubstitutions += (0.. [it.symbolicReference = f.quantifiedVariables.get(x)] + ] + ] + rightOperand = createSMTSymbolicValue => [it.symbolicReference = resultParam] + ] + } else { + createSMTSymbolicValue => [ + it.symbolicReference = smtFunction + it.parameterSubstitutions += (0.. [it.symbolicReference = f.quantifiedVariables.get(x)]] + it.parameterSubstitutions += createSMTSymbolicValue => [it.symbolicReference = resultParam] + ] + } + it.rightOperand = rangeType.constraint.apply(resultParam) + ] + ] + ] + } + return smtFunction + } + + def transformFunctionDefinition(FunctionDefinition function, SMTInput input, Logic2SmtMapperTrace trace) { + throw new UnsupportedOperationException("TODO: auto-generated method stub") + } + + def protected transformRelationDeclaration(RelationDeclaration relation, SMTInput input, Logic2SmtMapperTrace trace) { + val parameterTypeCombinations = unfolder.getPermutations(relation.parameters.map[x|transformTypeReference(x,trace)]) + var relationIndex = 1 + val unfolding = new ArrayList(parameterTypeCombinations.size) + for(parameterTypeCombination : parameterTypeCombinations) { + /// Create a name for the relation + val nameWithIndex = if (parameterTypeCombinations.size > 1) + toID('''relation «relation.name.toID» «relationIndex++»''') + else + toID('''relation «relation.name.toID»''') + + // Adding an unfolded relation + val smtRelation = createSMTFunctionDeclaration => [ + name = nameWithIndex + parameters+= parameterTypeCombination.map[typeConstraint | EcoreUtil.copy(typeConstraint.type)] + range = createSMTBoolTypeReference + ] + val Descriptor descriptor = new Descriptor(parameterTypeCombination.map[ + TypeDescriptor.createFromTypeReference(it.type)],relation) + trace.relationMap.put(descriptor,smtRelation) + input.functionDeclarations += smtRelation + unfolding += descriptor + + // If there is a type constraint + if(parameterTypeCombination.exists[it.constraint != null]) { + // create a constraint that specifies that the relation contains elemenents with the required properties + val and = createSMTAnd + val rel = createSMTSymbolicValue => [it.symbolicReference = smtRelation] + val forall = createSMTForall => [ + it.expression = createSMTImpl => [ + it.leftOperand = rel + it.rightOperand = and + ] + ] + var paramIndex = 0 + for(param : parameterTypeCombination) { + val paramName = '''p«paramIndex++»''' + val variable = createSMTSortedVariable => [ + it.name = paramName + it.range = param.type + ] + forall.quantifiedVariables += variable + rel.parameterSubstitutions += createSMTSymbolicValue => [it.symbolicReference = variable] + if(param.constraint != null) { + and.operands+=param.constraint.apply(variable) + } + } + input.assertions += createSMTAssertion => [ + it.value = forall + ] + } + } + trace.relationUnfolding.put(relation,unfolding) + } + def protected transformRelationDefinition(RelationDefinition relation, SMTInput input, Logic2SmtMapperTrace trace) { + val parameterTypeCombinations = unfolder.getPermutations(relation.variables.map[x|transformTypeReference(x.range,trace)]).toList + var relationIndex = 1 + val unfolding = new ArrayList(parameterTypeCombinations.size) + for(parameterTypeCombination : parameterTypeCombinations) { + /// Create a name for the relation + val nameWithIndex = if (parameterTypeCombinations.size > 1) + toID('''relation «relation.name.toID» «relationIndex++»''') + else + toID('''relation «relation.name.toID»''') + + // creating an unfolded relation + val smtRelation = createSMTFunctionDefinition => [ + name = nameWithIndex + range = createSMTBoolTypeReference + ] + /* + // adding variables as parameters + val Map variables = new HashMap + var paramIndex = 0 + val constraintList = new LinkedList + for(param : parameterTypeCombination) { + val paramName = relation.variables.get(paramIndex).name.toID + val variable = createSMTSortedVariable => [ + it.name = paramName + it.range = param.type + ] + + smtRelation.parameters+=variable + variables.put(relation.variables.get(paramIndex),variable) + if(param.constraint != null) { + constraintList+=param.constraint.apply(variable) + } + paramIndex++ + } + val definition = transformTerm(relation.value,trace,variables) + if(constraintList.empty) { + smtRelation.value = definition.expectLogic.value + } else if(constraintList.size == 1) { + smtRelation.value = createSMTAnd => [ + it.operands += constraintList.head + it.operands += definition.expectLogic.value + ] + } else { + smtRelation.value = createSMTAnd => [ + it.operands += createSMTAnd => [operands += constraintList] + it.operands += definition.expectLogic.value + ] + } + */ + // + val Descriptor descriptor = new Descriptor(parameterTypeCombination.map[ + TypeDescriptor.createFromTypeReference(it.type)],relation) + trace.relationMap.put(descriptor,smtRelation) + input.functionDefinition += smtRelation + unfolding += descriptor + } + trace.relationUnfolding.put(relation,unfolding) + } + def transformRelationDefinition_definition(RelationDefinition relation, SMTInput input, Logic2SmtMapperTrace trace) { + val parameterTypeCombinations = unfolder.getPermutations(relation.variables.map[x|transformTypeReference(x.range,trace)]).toList + for(parameterTypeCombination : parameterTypeCombinations) { + val Descriptor descriptor = new Descriptor(parameterTypeCombination.map[ + TypeDescriptor.createFromTypeReference(it.type)],relation) + val smtRelation = descriptor.lookup(trace.relationMap) as SMTFunctionDefinition + + // adding variables as parameters + val Map variables = new HashMap + var paramIndex = 0 + val constraintList = new LinkedList + for(param : parameterTypeCombination) { + val paramName = relation.variables.get(paramIndex).name.toID + val variable = createSMTSortedVariable => [ + it.name = paramName + it.range = param.type + ] + + smtRelation.parameters+=variable + variables.put(relation.variables.get(paramIndex),variable) + if(param.constraint != null) { + constraintList+=param.constraint.apply(variable) + } + paramIndex++ + } + val definition = transformTerm(relation.value,trace,variables) + if(constraintList.empty) { + smtRelation.value = definition.expectLogic.value + } else if(constraintList.size == 1) { + smtRelation.value = createSMTAnd => [ + it.operands += constraintList.head + it.operands += definition.expectLogic.value + ] + } else { + smtRelation.value = createSMTAnd => [ + it.operands += createSMTAnd => [operands += constraintList] + it.operands += definition.expectLogic.value + ] + } + } + } + + def transformConstantDeclaration(ConstantDeclaration constant,SMTInput input, Logic2SmtMapperTrace trace) { + throw new UnsupportedOperationException("TODO: auto-generated method stub") + } + + def transformConstantDefinition(ConstantDefinition constant, SMTInput input, Logic2SmtMapperTrace trace) { + throw new UnsupportedOperationException("TODO: auto-generated method stub") + } + + + def protected SMTAssertion transformAssertion(Assertion assertion, Logic2SmtMapperTrace trace) { + val a = assertion.value.transformTerm(trace,emptyMap) + createSMTAssertion => [value = a.expectLogic.value] + } + + /////////////////////////////////////////////////////// + // Logic -> Logic value transformation + /////////////////////////////////////////////////////// + + /////////////////////////////////////////////////////// + // Literals + /////////////////////////////////////////////////////// + def dispatch protected TransformedSubterm transformTerm(BoolLiteral literal, Logic2SmtMapperTrace trace, Map variables) { + new LogicSubterm(createSMTBoolLiteral => [value = literal.value]) } + def dispatch protected TransformedSubterm transformTerm(IntLiteral literal, Logic2SmtMapperTrace trace, Map variables) { + if(literal.value>=0) { new NumericSubterm(#[],#[],createSMTIntLiteral => [value = literal.value])} + else {new NumericSubterm(#[],#[],createSMTMinus => [ leftOperand = (createSMTIntLiteral => [value = - (literal.value) ] ) ]) } } + def dispatch protected TransformedSubterm transformTerm(RealLiteral literal, Logic2SmtMapperTrace trace, Map variables) { + new NumericSubterm(#[],#[],createSMTRealLiteral => [value = literal.value]) } + + /////////////////////////////////////////////////////// + // NumericOperators + /////////////////////////////////////////////////////// + def dispatch protected TransformedSubterm transformTerm(Plus plus, Logic2SmtMapperTrace trace, Map variables) { + return transformBinaryNumericOperator( + plus.leftOperand,plus.rightOperand, + [l,r|createSMTPlus => [ leftOperand = l rightOperand = r ]], + trace,variables) + } + def dispatch protected TransformedSubterm transformTerm(Minus minus, Logic2SmtMapperTrace trace, Map variables) { + return transformBinaryNumericOperator( + minus.leftOperand,minus.rightOperand, + [l,r|createSMTMinus => [ leftOperand = l rightOperand = r ]], + trace,variables) + } + def dispatch protected TransformedSubterm transformTerm(Multiply multiply, Logic2SmtMapperTrace trace, Map variables) { + return transformBinaryNumericOperator( + multiply.leftOperand,multiply.rightOperand, + [l,r|createSMTMultiply => [ leftOperand = l rightOperand = r ]], + trace,variables) + } + def dispatch protected TransformedSubterm transformTerm(Divison div, Logic2SmtMapperTrace trace, Map variables) { + return transformBinaryNumericOperator( + div.leftOperand,div.rightOperand, + [l,r|createSMTDiv => [ leftOperand = l rightOperand = r ]], + trace,variables) + } + def dispatch protected TransformedSubterm transformTerm(Mod mod, Logic2SmtMapperTrace trace, Map variables) { + return transformBinaryNumericOperator( + mod.leftOperand,mod.rightOperand, + [l,r|createSMTMod => [ leftOperand = l rightOperand = r ]], + trace,variables) + } + + def protected TransformedSubterm transformBinaryNumericOperator( + Term leftOperand, + Term rightOperand, + Function2 combinator, + Logic2SmtMapperTrace trace, Map variables) + { + val left = leftOperand. transformTerm(trace,variables).expectNumber.getPossibleValues + val right = rightOperand.transformTerm(trace,variables).expectNumber.getPossibleValues + val values = new ArrayList(left.size * right.size) + for(combination : TransformedSubterm.allCombinations(left,right)) { + val l = combination.get(0) + val r = combination.get(1) + values += new SubtermOption( + #[l,r],#[],#[], + combinator.apply(l.expression, r.expression), + TypeDescriptor.numericTypeDescriptor_Instance + ) + } + return new NumericSubterm(values) + } + + /////////////////////////////////////////////////////// + // LogicOperators + /////////////////////////////////////////////////////// + def dispatch protected TransformedSubterm transformTerm(Not not, Logic2SmtMapperTrace trace, Map variables) { + val operand = not.operand.transformTerm(trace,variables).expectLogic + new LogicSubterm(createSMTNot => [operand = operand.value]) } + def dispatch protected TransformedSubterm transformTerm(And and, Logic2SmtMapperTrace trace, Map variables) { + transformBinaryLogicOperator2(and.operands,[x|createSMTAnd => [operands += x]],trace,variables) } + def dispatch protected TransformedSubterm transformTerm(Or or, Logic2SmtMapperTrace trace, Map variables) { + transformBinaryLogicOperator2(or.operands,[x|createSMTOr => [operands += x]],trace,variables) } + def dispatch protected TransformedSubterm transformTerm(Impl impl, Logic2SmtMapperTrace trace, Map variables) { + transformBinaryLogicOperator1(impl.leftOperand,impl.rightOperand,[l,r|createSMTImpl =>[leftOperand = l rightOperand = r]],trace,variables) } + def dispatch protected TransformedSubterm transformTerm(Iff iff, Logic2SmtMapperTrace trace, Map variables) { + transformBinaryLogicOperator1(iff.leftOperand,iff.rightOperand,[l,r|createSMTIff => [leftOperand = l rightOperand = r]],trace,variables)} + + /** + * Logic combinator with two values + */ + def protected transformBinaryLogicOperator1( + Term leftOperand, Term rightOperand, + Function2 combinator, + Logic2SmtMapperTrace trace, Map variables) { + val left = leftOperand.transformTerm(trace,variables).expectLogic + val right = rightOperand.transformTerm(trace,variables).expectLogic + return new LogicSubterm(combinator.apply(left.value, right.value)) + } + /** + * Logic combinator with multiple values + */ + def protected transformBinaryLogicOperator2( + Iterable operands, + Function1,SMTTerm> combinator, + Logic2SmtMapperTrace trace, Map variables) { + val smtOperands = operands.map[transformTerm(trace,variables).expectLogic.value] + return new LogicSubterm(combinator.apply(smtOperands)) + } + + /////////////////////////////////////////////////////// + // Numeric -> Logic + /////////////////////////////////////////////////////// + def dispatch protected TransformedSubterm transformTerm(MoreThan moreThan, Logic2SmtMapperTrace trace, Map variables) { + transformNumericComparison(moreThan.leftOperand,moreThan.rightOperand, [l,r|createSMTMT => [ leftOperand = l rightOperand = r ]],trace,variables)} + def dispatch protected TransformedSubterm transformTerm(LessThan lessThan, Logic2SmtMapperTrace trace, Map variables) { + transformNumericComparison(lessThan.leftOperand,lessThan.rightOperand, [l,r|createSMTLT => [ leftOperand = l rightOperand = r ]],trace,variables)} + def dispatch protected TransformedSubterm transformTerm(MoreOrEqualThan moreThan, Logic2SmtMapperTrace trace, Map variables) { + transformNumericComparison(moreThan.leftOperand,moreThan.rightOperand, [l,r|createSMTMEQ => [ leftOperand = l rightOperand = r ]],trace,variables)} + def dispatch protected TransformedSubterm transformTerm(LessOrEqualThan lessThan, Logic2SmtMapperTrace trace, Map variables) { + transformNumericComparison(lessThan.leftOperand,lessThan.rightOperand, [l,r|createSMTLEQ => [ leftOperand = l rightOperand = r ]],trace,variables)} + + def protected transformNumericComparison(Term leftOperand, Term rightOperand, Function2 combinator, Logic2SmtMapperTrace trace, Map variables){ + val left = leftOperand.transformTerm(trace,variables).getPossibleValues + val right = rightOperand.transformTerm(trace,variables).getPossibleValues + val values = new ArrayList(left.size * right.size) + for(combination : TransformedSubterm.allCombinations(left,right)) { + val l = combination.get(0) + val r = combination.get(1) + values += LogicSubterm::resolveToLogic(#[l,r],combinator.apply(l.expression, r.expression)) + } + val res = createSMTOr =>[operands += values] + return new LogicSubterm(res) + } + + /////////////////////////////////////////////////////// + // Equals and Distinct + /////////////////////////////////////////////////////// + + def dispatch protected TransformedSubterm transformTerm(Equals equals, Logic2SmtMapperTrace trace, Map variables) { + val left = equals.leftOperand.transformTerm(trace,variables) + val rightX = equals.rightOperand.transformTerm(trace,variables) + if(left instanceof LogicSubterm) { + val right = rightX.expectLogic + new LogicSubterm(createSMTEquals => [ + leftOperand = left.value + rightOperand = right.value ]) + } else if(left instanceof NumericSubterm) { + val right = rightX.expectNumber + val leftOperands = left.possibleValues + val rightOperands = right.possibleValues + val values = new ArrayList(leftOperands.size * rightOperands.size) + for(combination : TransformedSubterm.allCombinations(left.possibleValues,right.possibleValues)) { + val l = combination.get(0) + val r = combination.get(1) + values += TransformedSubterm.resolveToLogic(#[l,r], + createSMTEquals => [ + leftOperand = combination.get(0).expression + rightOperand = combination.get(1).expression]) + } + return new LogicSubterm(createSMTOr =>[operands += values]) + } else if(left instanceof ComplexSubterm){ + val right = rightX as ComplexSubterm + + val values = new LinkedList + for(combination : TransformedSubterm.allCombinations(left.possibleValues,right.possibleValues)) { + val l = combination.get(0) + val r = combination.get(1) + if(l.type.complexType == r.type.complexType) { + values += TransformedSubterm.resolveToLogic(#[l,r],createSMTEquals => [ + leftOperand = l.expression + rightOperand = r.expression ]) + } /*else dont add*/ + } + + if(values.size == 0) { + return new LogicSubterm(createSMTBoolLiteral => [it.value = false]) + } else if(values.size == 1) { + return new LogicSubterm(values.head) + } else { + return new LogicSubterm(createSMTOr => [operands += values]) + } + } + } + + def dispatch protected TransformedSubterm transformTerm(Distinct distinct, Logic2SmtMapperTrace trace, Map variables) { + val o = distinct.operands.map[transformTerm(trace,variables)] + if(o.empty) { + throw new IllegalArgumentException('''empty distinct''') + } else if(o.size == 1) { + // 1 element is always distinct + new LogicSubterm(createSMTBoolLiteral => [it.value = true]) + } else { + val head = o.head + if(head instanceof LogicSubterm) { + return new LogicSubterm(createSMTDistinct => [ + it.operands += o.map[expectLogic.value]]) + } else if(head instanceof NumericSubterm) { + val numbers = o.map[expectNumber.possibleValues] + val distincts = new LinkedList + for(combination : TransformedSubterm.allCombinations(numbers)) { + distincts += LogicSubterm::resolveToLogic(combination,createSMTDistinct => [operands += combination.map[it.expression]]) + } + new LogicSubterm(createSMTOr => [it.operands += distincts]) + } else { + val objects = o.map[possibleValues] + val distincts = new LinkedList + for(combination : TransformedSubterm.allCombinations(objects)) { + val Map> type2Terms = new LinkedHashMap; + for(param:combination) { + val type = param.type.complexType + val value = param + var LinkedList list; + if(type2Terms.containsKey(type)) { + list = type2Terms.get(type) + } else { + list = new LinkedList + type2Terms.put(type,list) + } + list+=value + } + + val groups = type2Terms.values.map[elementList| + if(elementList.size == 1) return null + else return LogicSubterm.resolveToLogic(elementList,createSMTDistinct => [it.operands += elementList.map[expression]]) + ].filterNull + if(groups.empty) { + // One of the group is trivially satisfied + return new LogicSubterm(createSMTBoolLiteral => [it.value = true]) + } else { + val and = createSMTAnd => [operands += groups] + distincts.add(and) + } + } + if(distincts.size == 1) { + return new LogicSubterm(distincts.head) + } else { + return new LogicSubterm(createSMTOr => [it.operands += distincts]) + } + } + } + } + + /////////////////////////////////////////////////////// + // Quantifiers + /////////////////////////////////////////////////////// + + def dispatch protected TransformedSubterm transformTerm(Forall forall, Logic2SmtMapperTrace trace, Map variables) { + new LogicSubterm(transformQuantifiedExpression(forall,trace,variables, + [createSMTForall], + [q|createSMTAnd=>[operands+=q]], + [precondition,expression|createSMTImpl=>[leftOperand=precondition rightOperand=expression]])) + } + def dispatch protected TransformedSubterm transformTerm(Exists exists, Logic2SmtMapperTrace trace, Map variables) { + new LogicSubterm(transformQuantifiedExpression(exists,trace,variables, + [createSMTExists], + [q|createSMTOr=>[operands+=q]], + [precondition,expression|createSMTAnd=>[operands+=precondition operands+=expression]])) + } + + def protected SMTTerm transformQuantifiedExpression( + QuantifiedExpression q, Logic2SmtMapperTrace trace, Map variables, + Function0 constructor, + Function1,SMTTerm> combinator, + Function2 preconditionCombinator + ) { + val permutations = unfolder.getPermutations(q.quantifiedVariables.map[it.range.transformTypeReference(trace)]) + val ArrayList unfoldedQuantification = new ArrayList(permutations.size) + + for(permutation : permutations) { + val allVariables = new HashMap(variables) + val newSMTVariables = new ArrayList(q.quantifiedVariables.size) + val typePrecondition = new ArrayList(q.quantifiedVariables.size) + + for(variableIndex: 0.. [ + name = logicVariable.name.toID + range = elementInPermutation.type + ] + allVariables.put(logicVariable, newSMTVariable) + newSMTVariables+=newSMTVariable + if(elementInPermutation.constraint != null) { + typePrecondition += elementInPermutation.constraint.apply(newSMTVariable) + } + } + + val expressionOfQuantifiedFormula = + if(typePrecondition.isEmpty) + q.expression.transformTerm(trace,allVariables).expectLogic.value + else if(typePrecondition.size == 1) + preconditionCombinator.apply( + typePrecondition.head, + q.expression.transformTerm(trace,allVariables).expectLogic.value) + else + preconditionCombinator.apply( + createSMTAnd => [it.operands += typePrecondition], + q.expression.transformTerm(trace,allVariables).expectLogic.value) + + unfoldedQuantification += constructor.apply => [ + quantifiedVariables += newSMTVariables + expression = expressionOfQuantifiedFormula + ] + +// if(newSMTVariables.exists[it.range == null]) { +// println(newSMTVariables.filter[it.range == null].map[name]) +// } + } + + if(permutations.size == 1) return unfoldedQuantification.head + else return combinator.apply(unfoldedQuantification) + } + + /////////////////////////////////////////////////////// + // If - Then - Else + /////////////////////////////////////////////////////// + def dispatch protected TransformedSubterm transformTerm(IfThenElse ite, Logic2SmtMapperTrace trace, Map variables) { + val condition = ite.condition.transformTerm(trace,variables).expectLogic.value + val positiveTerm = ite.ifTrue.transformTerm(trace,variables) + val positives = positiveTerm.possibleValues + val negativeTerm = ite.ifFalse.transformTerm(trace,variables) + val negatives = negativeTerm.possibleValues + // Simple ITE + if(positives.size == 1 && negatives.size == 1 && positives.head.type == negatives.head.type) { + val t = positives.head.type + if(t.isLogic) { + return new LogicSubterm(createSMTITE => [ + it.condition = condition + it.^if = positives.head.expression + it.^else = negatives.head.expression]) + } else if(t.isNumeric) { + return new NumericSubterm( + (positives.head.variables + negatives.head.variables).toList, + (positives.head.preconditions + negatives.head.preconditions).toList, + createSMTITE => [ + it.condition = condition + it.^if = positives.head.expression + it.^else = negatives.head.expression + ]) + } else { + return new ComplexSubterm( + (positives.head.variables + negatives.head.variables).toList, + (positives.head.preconditions + negatives.head.preconditions).toList, + createSMTITE => [ + it.condition = condition + it.^if = positives.head.expression + it.^else = negatives.head.expression], + t + ) + } + // else the ite need to be unfolded + } else { + if(positiveTerm instanceof LogicSubterm) { + throw new AssertionError('''If the subterm has logic value it should be transformed as "Simple ITE""''') + } else if (positiveTerm instanceof NumericSubterm){ + return new NumericSubterm(unfoldIte(positives, condition, negatives)) + } else { + return new ComplexSubterm(unfoldIte(positives, condition, negatives)) + } + } + } + + private def List unfoldIte(List positives, SMTTerm condition, List negatives) { + (positives.map[ + new SubtermOption(#[it],#[],#[condition],it.expression,it.type) + ] + + negatives.map[ + new SubtermOption(#[it],#[],#[createSMTNot => [it.operand = condition]],it.expression,it.type) + ]).toList + } + + /////////////////////////////////////////////////////// + // instanceof + /////////////////////////////////////////////////////// + + def dispatch protected TransformedSubterm transformTerm(InstanceOf i, Logic2SmtMapperTrace trace, Map variables) { + val value = i.value.transformTerm(trace,variables) + val range = i.range + if(range instanceof BoolTypeReference) { + return new LogicSubterm(createSMTBoolLiteral=>[it.value = (value instanceof LogicSubterm)]) + } else if(range instanceof IntTypeReference || range instanceof RealTypeReference) { + return new LogicSubterm(createSMTBoolLiteral=>[it.value = (value instanceof NumericSubterm)]) + } else { + val requestedTypes = this.typeMapper.transformTypeReference((range as ComplexTypeReference).referred,trace) + val possileValues = value.possibleValues + val options = new ArrayList(requestedTypes.size) + for(typeConstraint : requestedTypes) { + val possibleValue = possileValues.filter[it.type.complexType == (typeConstraint.type as SMTComplexTypeReference).referred].head + if(possibleValue != null) { + val x = if(typeConstraint.constraint != null ) { + if(possibleValue.expression instanceof SMTSymbolicValue && (possibleValue.expression as SMTSymbolicValue).symbolicReference instanceof SMTSortedVariable) { + val referred = (possibleValue.expression as SMTSymbolicValue).symbolicReference as SMTSortedVariable + typeConstraint.constraint.apply(referred) + } else { + createSMTForall => [ + val v = createSMTSortedVariable => [it.range = EcoreUtil.copy(typeConstraint.type)] + it.quantifiedVariables += v + it.expression = createSMTImpl => [ + leftOperand = createSMTEquals => [ + it.leftOperand = possibleValue.expression + it.rightOperand = createSMTSymbolicValue => [it.symbolicReference = v] + ] + rightOperand = typeConstraint.constraint.apply(v) + ] + ] + } + } else if(typeConstraint.constraint == null) { + createSMTBoolLiteral => [it.value = true] + } + options += LogicSubterm::resolveToLogic(#[possibleValue],x) + } + } + + if(options.size == 0) { + return new LogicSubterm(createSMTBoolLiteral=>[it.value = false]) + } else if(options.size == 1) { + return new LogicSubterm(options.head) + } else { + return new LogicSubterm(createSMTOr => [it.operands += options]) + } + } + + } + + /////////////////////////////////////////////////////// + // SymbolicReference + /////////////////////////////////////////////////////// + + def dispatch protected TransformedSubterm transformTerm(SymbolicValue symbolicValue, Logic2SmtMapperTrace trace, Map variables) { + val referred = symbolicValue.symbolicReference + val params = symbolicValue.parameterSubstitutions + return transformSymbolicReference(referred,params,trace,variables) + } + + def dispatch protected TransformedSubterm transformSymbolicReference(Relation referred, List parameterSubstitution, Logic2SmtMapperTrace trace, Map variables) { + val parameters = parameterSubstitution.map[transformTerm(it,trace,variables)] + val list = new LinkedList + for(combination : TransformedSubterm.allCombinations(parameters.map[it.possibleValues])) { + val descriptor = new Descriptor(combination.map[it.type],referred) + val targetRelation = descriptor.lookup(trace.relationMap) + if(targetRelation == null) { + throw new AssertionError('''target relation should not be null (yet)''') + + } else { + list += TransformedSubterm.resolveToLogic(combination,createSMTSymbolicValue => [ + it.symbolicReference = targetRelation + it.parameterSubstitutions += combination.map[it.expression] + ]) + } + } + + if(list.size == 1) { + return new LogicSubterm(list.head) + } else { + return new LogicSubterm(createSMTOr => [ operands += list ]) + } + } + + + def dispatch protected TransformedSubterm transformSymbolicReference(Function referred, List parameterSubstitution, Logic2SmtMapperTrace trace, Map variables) { + throw new UnsupportedOperationException + } + + def dispatch protected TransformedSubterm transformSymbolicReference(Variable referred, List parameterSubstitution, Logic2SmtMapperTrace trace, Map variables) { + if(!variables.containsKey(referred)) { + val container = referred.eContainer + println("X" + container) + for(v : variables.keySet) { + println(v) + println("in " +v.eContainer) + } + return null + } + val v = referred.lookup(variables) + + val expression = createSMTSymbolicValue => [it.symbolicReference = v] + if(v.range instanceof SMTBoolTypeReference) { + return new LogicSubterm(expression) + } else if(v.range instanceof SMTIntTypeReference || v.range instanceof SMTRealTypeReference) { + return new NumericSubterm(#[],#[],expression) + } else { + return new ComplexSubterm(#[],#[],expression, + new TypeDescriptor((v.range as SMTComplexTypeReference).referred)); + } + } + + def dispatch protected TransformedSubterm transformSymbolicReference(DefinedElement referred, List parameterSubstitution, Logic2SmtMapperTrace trace, Map variables) { + this.typeMapper.transformSymbolicReference(referred,trace) + } + + def dispatch protected TransformedSubterm transformSymbolicReference(Void referred, List parameterSubstitution, Logic2SmtMapperTrace trace, Map variables) { + throw new NullPointerException('''unfilled symbolic reference!''') + } + + /////////// + + /*def transformContainment(SMTDocument document, ContainmentHierarchy h, Logic2SmtMapperTrace trace) { + val containmentRelation_oo = createSMTFunctionDefinition=>[ + it.name="containment!oo" + it.range=createSMTBoolTypeReference + val child = createSMTSortedVariable => [ + it.name = + ] + ] + }*/ + + /////////// + + def cleanDocument(SMTDocument document) { + val content = document.eAllContents.toList + for(object:content) { + for(containmentReference : object.eClass.EAllReferences.filter[containment]) { + val child = object.eGet(containmentReference) { + if(child!=null) { + if(containmentReference.isMany) { + val list = child as List + for(index : 0.. [it.value = false] + } else return null + } + def private dispatch replaceWith(SMTAnd and) { + if(and.operands.empty) { + return createSMTBoolLiteral => [it.value = true] + } else return null + } + def private dispatch replaceWith(EObject object) { + null + } +} \ No newline at end of file diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2SmtMapperTrace.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2SmtMapperTrace.xtend new file mode 100644 index 00000000..69111a11 --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2SmtMapperTrace.xtend @@ -0,0 +1,23 @@ +package hu.bme.mit.inf.dslreasoner.smt.reasoner + +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Constant +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Function +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSymbolicDeclaration +import java.util.HashMap +import java.util.List +import java.util.Map + +class Logic2SmtMapperTrace { + public var LogicProblem problem + public var Logic2SmtMapper forwardMapper + public var Logic2Smt_TypeMapperTrace typeMapperTrace + + public val Map>> relationUnfolding = new HashMap + public val Map,SMTSymbolicDeclaration> relationMap = new HashMap + public val Map>> functionUnfolding = new HashMap + public val Map,SMTSymbolicDeclaration> functionMap = new HashMap + public val Map>> constantUnfolding = new HashMap + public val Map,SMTSymbolicDeclaration> constantMap = new HashMap +} \ No newline at end of file diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2SmtMapper_UnfoldingSupport.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2SmtMapper_UnfoldingSupport.xtend new file mode 100644 index 00000000..8c2d5dad --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2SmtMapper_UnfoldingSupport.xtend @@ -0,0 +1,33 @@ +package hu.bme.mit.inf.dslreasoner.smt.reasoner + +//import hu.bme.mit.inf.dslreasoner.smtLanguage.SmtLanguageFactory +import java.util.ArrayList +import java.util.List + +class Logic2SmtMapper_UnfoldingSupport { + //val extension SmtLanguageFactory factory = SmtLanguageFactory.eINSTANCE + + def List> getPermutations(List> lists) { + if(lists.size == 1) { + val elements = lists.head + val result = new ArrayList(elements.size) + for(element: elements){ + result.add(#[element.copy]) + } + return result + } else { + val permuteThis = lists.head + val withThat = getPermutations(lists.tail.toList) + val result = new ArrayList(permuteThis.size*withThat.size) + for(h:permuteThis) { + for(t:withThat) { + val l = new ArrayList(withThat.size+1) + l+=h.copy + l.addAll(t.map[copy]) + result.add(l) + } + } + return result + } + } +} \ No newline at end of file diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2Smt_TypeMapper.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2Smt_TypeMapper.xtend new file mode 100644 index 00000000..71cfd0e0 --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2Smt_TypeMapper.xtend @@ -0,0 +1,38 @@ +package hu.bme.mit.inf.dslreasoner.smt.reasoner + +import hu.bme.mit.inf.dslreasoner.logic.model.builder.TypeScopes +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTDocument +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTInput +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSortedVariable +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTTerm +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTTypeReference +import java.util.List +import org.eclipse.emf.ecore.util.EcoreUtil +import org.eclipse.xtend.lib.annotations.Data +import org.eclipse.xtext.xbase.lib.Functions.Function1 + +interface Logic2Smt_TypeMapper { + def void transformTypes( + SMTInput document, LogicProblem problem, Logic2SmtMapperTrace trace, TypeScopes scopes) + + def List transformTypeReference(Type type, Logic2SmtMapperTrace trace) + def TransformedSubterm transformSymbolicReference(DefinedElement referred, Logic2SmtMapperTrace trace) + def Logic2SMT_TypeMapperInterpretation getTypeInterpretation(LogicProblem problem,SMTDocument document,SmtModelInterpretation interpretation, Logic2SmtMapperTrace trace) +} + +@Data +class TypeConstraint { + SMTTypeReference type + Function1 constraint + + def public copy() { + return new TypeConstraint(EcoreUtil.copy(this.type),this.constraint) + } +} + +interface Logic2Smt_TypeMapperTrace{ + def Logic2Smt_TypeMapperTrace copy(SMTInput newModel) +} \ No newline at end of file diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2Smt_TypeMapper_FilteredTypes.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2Smt_TypeMapper_FilteredTypes.xtend new file mode 100644 index 00000000..c9bafa6c --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2Smt_TypeMapper_FilteredTypes.xtend @@ -0,0 +1,501 @@ +package hu.bme.mit.inf.dslreasoner.smt.reasoner + +import hu.bme.mit.inf.dslreasoner.logic.model.builder.TypeScopes +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem +import hu.bme.mit.inf.dslreasoner.logic.model.patterns.PossibleDynamicTypeMatcher +import hu.bme.mit.inf.dslreasoner.logic.model.patterns.SupertypeStarMatcher +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTComplexTypeReference +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTDocument +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTEnumLiteral +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTEnumeratedTypeDeclaration +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDeclaration +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDefinition +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTInput +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTModelResult +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSetTypeDeclaration +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSymbolicDeclaration +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTTerm +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTType +import hu.bme.mit.inf.dslreasoner.smtLanguage.SmtLanguageFactory +import java.util.ArrayList +import java.util.HashMap +import java.util.LinkedList +import java.util.List +import java.util.Map +import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine +import org.eclipse.viatra.query.runtime.emf.EMFScope +import org.eclipse.xtext.xbase.lib.Functions.Function0 +import org.eclipse.xtext.xbase.lib.Functions.Function1 + +import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* + +class Logic2Smt_TypeMapperTrace_FilteredTypes implements Logic2Smt_TypeMapperTrace{ + public var Map independentClasses = new HashMap + /** + * SMT type for the new objects + */ + public var SMTType newObjects + /** + * SMT type for the existing objects + */ + public var SMTEnumeratedTypeDeclaration oldObjects + /** + * existing element -> SMT literal map + */ + public var Map elementMap = new HashMap + + public var SMTEnumeratedTypeDeclaration oldObjectTypes + public var Map oldObjectTypeMap = new HashMap + public var SMTFunctionDefinition oldObjectTypeFunction + public var Map oldObjectTypePredicates = new HashMap + + public var SMTEnumeratedTypeDeclaration newObjectTypes + public var Map newObjectTypeMap = new HashMap + public var SMTFunctionDeclaration newObjectTypeFunction + public var Map newObjectTypePredicates = new HashMap + + override copy(SMTInput newModel) { + val a = this + val b = new Logic2Smt_TypeMapperTrace_FilteredTypes + + b.independentClasses = a.independentClasses.copyMap(newModel.typeDeclarations,[name]) + + b.newObjects = newModel.typeDeclarations.filter[it.name == a.newObjects.name].head + b.oldObjects = newModel.typeDeclarations.filter[it.name == a.oldObjects.name].head as SMTEnumeratedTypeDeclaration + b.elementMap = a.elementMap.copyMap(b.oldObjects.elements,[name]) + + b.oldObjectTypes = newModel.typeDeclarations.filter[it.name == a.newObjects.name].head as SMTEnumeratedTypeDeclaration + b.oldObjectTypeMap = a.oldObjectTypeMap.copyMap(b.oldObjectTypes.elements,[name]) + b.oldObjectTypeFunction = newModel.functionDefinition.filter[it.name == a.oldObjectTypeFunction.name].head + b.oldObjectTypePredicates = a.oldObjectTypePredicates.copyMap(newModel.functionDefinition,[name]) + + b.newObjectTypes = newModel.typeDeclarations.filter[it.name == a.newObjectTypes.name].head as SMTEnumeratedTypeDeclaration + b.newObjectTypeMap = a.newObjectTypeMap.copyMap(b.newObjectTypes.elements,[name]) + b.newObjectTypeFunction = newModel.functionDeclarations.filter[it.name == a.newObjectTypeFunction.name].head + b.newObjectTypePredicates = a.newObjectTypePredicates.copyMap(newModel.functionDefinition,[name]) + + return b + } +} + +class Logic2Smt_TypeMapper_FilteredTypes implements Logic2Smt_TypeMapper { + val extension SmtLanguageFactory factory = SmtLanguageFactory.eINSTANCE + val LogiclanguageFactory factory2 = LogiclanguageFactory.eINSTANCE + + private def toID(List names) {names.join("!") } + private def toID(String name) {name.split("\\s+").toID} + + override transformTypes(SMTInput document, LogicProblem problem, Logic2SmtMapperTrace trace, TypeScopes scopes) { + val typeTrace = new Logic2Smt_TypeMapperTrace_FilteredTypes + trace.typeMapperTrace = typeTrace + val engine = ViatraQueryEngine.on(new EMFScope(problem)) + + val independentTypes = problem.types.filter(TypeDefinition).filter[isIndependentType] + + val connectedTypes = problem.types.filter[!isIndependentType] + val connectedElements = problem.elements.filter[!isIndependentElement] + + val connectedTypesWithoutDefintypesWithoutDefinedSupertype = connectedTypes.filter(TypeDeclaration).filter[!hasDefinedSupertype].toList + val hasOldElements = !connectedElements.empty + val hasNewElements = !connectedTypesWithoutDefintypesWithoutDefinedSupertype.empty + + // 0. map the simple types + this.transformIndependentTypes(independentTypes,trace) + + // 1. Has old elements => create supertype for it + if(hasOldElements) { + this.transformDefinedElements(connectedElements, trace,document) + } + // 2. Has new types => create a supertype for it + if(hasNewElements) { + this.transformUndefinedElements(scopes,trace,document) + } + // 3. Adding type definitions of the types + // 3.1: Type definition to old elements + if(hasOldElements) { + this.transformOldTypes(connectedTypes, connectedElements, trace, document, engine) + } + // 3.2: Type definition to new elements + if(hasNewElements) { + this.transformNewTypes(connectedTypesWithoutDefintypesWithoutDefinedSupertype,trace,document,engine); + } + } + + private def isIndependentType(Type t) { + val res = (t instanceof TypeDefinition) && t.supertypes.empty && t.subtypes.empty + return res + } + private def isIndependentElement(DefinedElement e) { + val types = e.definedInType + return types.size == 1 && types.head.isIndependentType + } + + protected def transformIndependentTypes(Iterable types,Logic2SmtMapperTrace trace) { + for(type: types) { + val independentSMTType = createSMTEnumeratedTypeDeclaration => [ + name = toID(#["oldType",type.name]) + ] + trace.typeTrace.independentClasses.put(type,independentSMTType) + for(element : type.elements) { + val enumLiteral = createSMTEnumLiteral => [it.name = toID(#["oldElement",element.name])] + independentSMTType.elements += enumLiteral + trace.typeTrace.elementMap.put(element,enumLiteral) + } + } + } + + protected def transformDefinedElements(Iterable oldElements, Logic2SmtMapperTrace trace, SMTInput document) { + val List literals = new ArrayList(oldElements.size) + for(element : oldElements) { + val elementName ='''oldElement «element.name»''' + val literal = createSMTEnumLiteral => [name = elementName.toID] + literals += literal + trace.typeTrace.elementMap.put(element,literal) + } + trace.typeTrace.oldObjects = createSMTEnumeratedTypeDeclaration => + [name = "oldObjects" it.elements += literals] + document.typeDeclarations += trace.typeTrace.oldObjects + } + + protected def transformUndefinedElements(TypeScopes scopes, Logic2SmtMapperTrace trace, SMTInput document) { + var SMTType newObjects + if(scopes.maxNewElements == -1) { + newObjects = createSMTSetTypeDeclaration => [ + name = "newObjects" + ] + } else { + val newElements = new ArrayList(scopes.maxNewElements) + for(index : (1.. [ + name = #["newElement",index.toString].toID + ] + newElements += literal + } + newObjects = createSMTEnumeratedTypeDeclaration => [ + name = "newObjects" + it.elements += newElements + ] + } + trace.typeTrace.newObjects = newObjects + document.typeDeclarations += newObjects + } + + protected def transformOldTypes(Iterable oldTypes,Iterable oldElements, Logic2SmtMapperTrace trace, SMTInput document, ViatraQueryEngine engine) { + val possibleTypeMatcher = PossibleDynamicTypeMatcher.on(engine) + val supertypeStarMatcher = SupertypeStarMatcher.on(engine) +// val possibleTypes = new LinkedList +// if(hasDefinedElement) possibleTypes += typesWithDefinedSupertype +// if(hasUndefinedElement) possibleTypes += typesWithoutDefinedSupertype +// val possibleConcreteTypes = possibleTypes.filter[!it.isIsAbstract] +// val possibleConcreteTypes = possibleTypeMatcher.allValuesOfdynamic + + // 3.1.1. cretate a type for old types + val possibleConcreteTypeLiterals = new ArrayList() + for(possibleConcreteType: oldTypes.filter[!isIsAbstract]) { + val typeName = '''oldType «possibleConcreteType.name»''' + val literal = createSMTEnumLiteral => [name = typeName.toID] + trace.typeTrace.oldObjectTypeMap.put(possibleConcreteType,literal) + possibleConcreteTypeLiterals+=literal + } + val oldObjectTypes = createSMTEnumeratedTypeDeclaration => [ + it.name = "oldTypes" + it.elements += possibleConcreteTypeLiterals + ] + trace.typeTrace.oldObjectTypes = oldObjectTypes + document.typeDeclarations += oldObjectTypes + + // 3.1.2 for each object, create a constant for its possible dynamic type + val Map possibleTypesOfElement = new HashMap + val Map onlyPossibleType = new HashMap + for(object: oldElements) { + val types = possibleTypeMatcher.getAllValuesOfdynamic(null,object) + if(types.size == 1) { + onlyPossibleType.put(object,types.head) + } else { // including 0 or more than 1 + // create a constant declaration + val typeOfObjectConstant = createSMTFunctionDeclaration => [ + it.name = toID(#["typeDecisions",toID(object.name)]) + it.range = createSMTComplexTypeReference => [ + it.referred = trace.typeTrace.oldObjectTypes + ] + ] + document.functionDeclarations += typeOfObjectConstant + possibleTypesOfElement.put(object,typeOfObjectConstant) + // add assertions to the constant to select valid values + document.assertions += createSMTAssertion => [ + val options = types.map[type | createSMTEquals => [ + it.leftOperand = createSMTSymbolicValue => [it.symbolicReference = typeOfObjectConstant] + it.rightOperand = createSMTSymbolicValue => [it.symbolicReference = type.lookup(trace.typeTrace.oldObjectTypeMap)] + ]] + it.value = if(options.empty) { + createSMTBoolLiteral => [it.value = false] + } else { + createSMTOr=>[operands += options] + } + ] + } + } + + // 3.1.2 create a function: old elements -> old types + val oldTypeFunction = createSMTFunctionDefinition => [ + it.name = "oldTypeFunction" + val o = createSMTSortedVariable => [ + it.name = "o" + it.range= createSMTComplexTypeReference => [it.referred = trace.typeTrace.oldObjects] + ] + it.parameters += o + it.range = createSMTComplexTypeReference => [it.referred = trace.typeTrace.oldObjectTypes] + it.value = unfoldITE(oldElements, + [createSMTSymbolicValue => [it.symbolicReference = o]], + [DefinedElement e | createSMTSymbolicValue => [it.symbolicReference = e.lookup(trace.typeTrace.elementMap)]], + [DefinedElement e | + if(onlyPossibleType.containsKey(e)) { + return createSMTSymbolicValue => [ + symbolicReference = e.lookup(onlyPossibleType).lookup(trace.typeTrace.oldObjectTypeMap) ] + } else { + return createSMTSymbolicValue => [ + symbolicReference = e.lookup(possibleTypesOfElement) + ] + } + ] + ) + ] + trace.typeTrace.oldObjectTypeFunction = oldTypeFunction + document.functionDefinition += oldTypeFunction + + // 3.1.3 create a predicate for each type: old object -> {true, false} + for(oldType: oldTypes) { + val oldTypePredicate = createSMTFunctionDefinition + oldTypePredicate.name = toID(#["oldTypePredicate",oldType.name.toID]) + val param = createSMTSortedVariable => [ + name = "o" + range = createSMTComplexTypeReference => [referred = trace.typeTrace.oldObjects] + ] + oldTypePredicate.parameters += param + oldTypePredicate.range = createSMTBoolTypeReference + val values = new LinkedList + for(concreteSupbtype : supertypeStarMatcher.getAllValuesOfsubtype(oldType).filter[!isIsAbstract]) { + val typeOfO = createSMTSymbolicValue => [ + it.symbolicReference = oldTypeFunction + it.parameterSubstitutions += createSMTSymbolicValue => [it.symbolicReference = param] + ] + val valueOfConcreteSupbtype = createSMTSymbolicValue => [ + it.symbolicReference = concreteSupbtype.lookup(trace.typeTrace.oldObjectTypeMap) + ] + values += createSMTEquals => [ + it.leftOperand = typeOfO + it.rightOperand = valueOfConcreteSupbtype + ] + } + oldTypePredicate.value = createSMTOr=>[it.operands +=values] + + document.functionDefinition += oldTypePredicate + trace.typeTrace.oldObjectTypePredicates.put(oldType,oldTypePredicate) + } + } + + protected def transformNewTypes( + Iterable typesWithoutDefinedSupertype, + Logic2SmtMapperTrace trace, SMTInput document, ViatraQueryEngine engine) + { + val supertypeStarMatcher = SupertypeStarMatcher.on(engine) + val possibleTypes = typesWithoutDefinedSupertype + val possibleConcreteTypes = possibleTypes.filter[!it.isIsAbstract].toList + + // 3.2.1. cretate a type for new types + val possibleConcreteTypeLiterals = new ArrayList() + for(possibleConcreteType: possibleConcreteTypes) { + val typeName = '''newType «possibleConcreteType.name»''' + val literal = createSMTEnumLiteral => [name = typeName.toID] + trace.typeTrace.newObjectTypeMap.put(possibleConcreteType,literal) + possibleConcreteTypeLiterals+=literal + } + val newObjectTypes = createSMTEnumeratedTypeDeclaration => [ + it.name = "newTypes" + it.elements += possibleConcreteTypeLiterals + ] + trace.typeTrace.newObjectTypes = newObjectTypes + document.typeDeclarations += newObjectTypes + + // 3.2.2 create a function: new elements -> new types + val newTypeFunction = createSMTFunctionDeclaration => [ + it.name = "newTypeFunction" + it.parameters += createSMTComplexTypeReference => [it.referred = trace.typeTrace.newObjects] + it.range = createSMTComplexTypeReference => [it.referred = trace.typeTrace.newObjectTypes] + ] + trace.typeTrace.newObjectTypeFunction = newTypeFunction + document.functionDeclarations += newTypeFunction + + // 3.1.3 create a predicate for each type: new type -> {true, false} + for(newType: possibleTypes) { + val newTypePredicate = createSMTFunctionDefinition + newTypePredicate.name = toID(#["newTypePredicate",newType.name.toID]) + val param = createSMTSortedVariable => [ + name = "o" + range = createSMTComplexTypeReference => [referred = trace.typeTrace.newObjects] + ] + newTypePredicate.parameters += param + newTypePredicate.range = createSMTBoolTypeReference + val values = new LinkedList + for(concreteSupbtype : supertypeStarMatcher.getAllValuesOfsubtype(newType).filter[!isIsAbstract]) { + if(possibleConcreteTypes.contains(concreteSupbtype)) { + val typeOfO = createSMTSymbolicValue => [ + it.symbolicReference = newTypeFunction + it.parameterSubstitutions += createSMTSymbolicValue => [it.symbolicReference = param] + ] + if(!trace.typeTrace.newObjectTypeMap.containsKey(concreteSupbtype)) { + println("gebasz") + } + val valueOfConcreteSupbtype = createSMTSymbolicValue => [ + it.symbolicReference = concreteSupbtype.lookup(trace.typeTrace.newObjectTypeMap) + ] + values+= createSMTEquals => [ + it.leftOperand = typeOfO + it.rightOperand = valueOfConcreteSupbtype + ] + } + } + newTypePredicate.value = createSMTOr=>[it.operands +=values] + + document.functionDefinition += newTypePredicate + trace.typeTrace.newObjectTypePredicates.put(newType,newTypePredicate) + } + } + + private def Logic2Smt_TypeMapperTrace_FilteredTypes getTypeTrace(Logic2SmtMapperTrace trace) { + val typeTrace = trace.typeMapperTrace + if(typeTrace instanceof Logic2Smt_TypeMapperTrace_FilteredTypes) { + return typeTrace + } else { + throw new IllegalArgumentException('''Unknown trace type: «typeTrace.class.name»''') + } + } + + private def boolean hasDefinedSupertype(Type type) { + if(type instanceof TypeDefinition) { + return true + } else { + if(type.supertypes.empty) return false + else return type.supertypes.exists[it.hasDefinedSupertype] + } + } + + def private SMTTerm unfoldITE(Iterable options, Function0 input, Function1 conditionOfOption, Function1 outputForOption) { + if(options.size == 1) { + return outputForOption.apply(options.head) + } else { + return createSMTITE => [ + it.condition = createSMTEquals => [ + leftOperand = input.apply + rightOperand = conditionOfOption.apply(options.head) + ] + it.^if = outputForOption.apply(options.head) + it.^else = unfoldITE(options.tail,input,conditionOfOption,outputForOption) + ] + } + } + + override transformSymbolicReference(DefinedElement referred,Logic2SmtMapperTrace trace) { + val x = referred.lookup(trace.typeTrace.elementMap) + new ComplexSubterm(#[],#[], + createSMTSymbolicValue => [it.symbolicReference = x], + new TypeDescriptor(x.eContainer as SMTEnumeratedTypeDeclaration) + ) + } + + override transformTypeReference(Type type, Logic2SmtMapperTrace trace) { + val list = new ArrayList + + if(trace.typeTrace.oldObjectTypePredicates.containsKey(type)) { + list += new TypeConstraint( + createSMTComplexTypeReference => [it.referred = trace.typeTrace.oldObjects], + [x|createSMTSymbolicValue => [ + it.symbolicReference = trace.typeTrace.oldObjectTypePredicates.get(type) + it.parameterSubstitutions += createSMTSymbolicValue => [it.symbolicReference = x]]] + ) + } + if(trace.typeTrace.newObjectTypePredicates.containsKey(type)) { + list += new TypeConstraint( + createSMTComplexTypeReference => [it.referred = trace.typeTrace.newObjects], + [x|createSMTSymbolicValue => [ + it.symbolicReference = trace.typeTrace.newObjectTypePredicates.get(type) + it.parameterSubstitutions += createSMTSymbolicValue => [it.symbolicReference = x]]] + ) + } + if(trace.typeTrace.independentClasses.containsKey(type)) { + list += new TypeConstraint( + createSMTComplexTypeReference => [it.referred = type.lookup(trace.typeTrace.independentClasses)], + null + ) + } + + if(list.empty) throw new AssertionError('''Typereference to type is «type.name» empty''') + if(list.exists[it.type == null]){ + throw new AssertionError('''Typereference to null!''') + } + return list + } + + override getTypeInterpretation(LogicProblem problem, SMTDocument document, SmtModelInterpretation interpretation, Logic2SmtMapperTrace trace) { + val model = document.output.getModelResult as SMTModelResult + val newTypeDec = trace.typeTrace.newObjects + var List newElements = null + + if(newTypeDec instanceof SMTSetTypeDeclaration) { + val newElementType = model.typeDefinitions.filter[ + (it.type as SMTComplexTypeReference).referred == newTypeDec + ].head + newElements = newElementType.elements.map[new ValueType(new TypeDescriptor(newTypeDec),it.symbolicReference)] + } else if(newTypeDec instanceof SMTEnumeratedTypeDeclaration) { + newElements = newTypeDec.elements.map[new ValueType(new TypeDescriptor(newTypeDec),it)] + } else throw new IllegalArgumentException('''Unknown type : «newTypeDec.class.name»''') + + val Map logic2smt = new HashMap + val Map smt2logic = new HashMap + + var index = 1; + for(newElement : newElements) { + val n = '''new «index++»''' + val logic = factory2.createDefinedElement => [it.name = n] + logic2smt.put(logic,newElement) + smt2logic.put(newElement.value as SMTSymbolicDeclaration,logic) + } + for(oldElement : problem.elements) { + val declaration = trace.typeTrace.oldObjectTypeMap.get(oldElement) + logic2smt.put(oldElement,new ValueType(new TypeDescriptor(trace.typeTrace.oldObjects),declaration)) + smt2logic.put(declaration,oldElement) + } + + val engine = ViatraQueryEngine.on(new EMFScope(problem)) + val supertypeStarMatcher = SupertypeStarMatcher.on(engine) + + val type2Elements = (trace.typeTrace.oldObjectTypeMap.keySet + + trace.typeTrace.newObjectTypeMap.keySet) + .toInvertedMap[new LinkedList] + + val inverseOldTypeMap = trace.typeTrace.oldObjectTypeMap.bijectiveInverse + for(oldElement: trace.typeTrace.elementMap.values) { + val type = interpretation.queryEngine.resolveFunctionDefinition( + trace.typeTrace.oldObjectTypeFunction,#[oldElement]) as SMTEnumLiteral + val dynamicType = type.lookup(inverseOldTypeMap) + val supertypes = supertypeStarMatcher.getAllValuesOfsupertype(dynamicType) + supertypes.forEach[type2Elements.get(it) += oldElement.lookup(smt2logic)] + } + + val inverseNewTypeMap = trace.typeTrace.newObjectTypeMap.bijectiveInverse + for(newElement: newElements.map[value as SMTSymbolicDeclaration]) { + val type = interpretation.queryEngine.resolveFunctionDeclaration( + trace.typeTrace.newObjectTypeFunction,#[newElement]) as SMTEnumLiteral + val dynamicType = type.lookup(inverseNewTypeMap) + val supertypes = supertypeStarMatcher.getAllValuesOfsupertype(dynamicType) + supertypes.forEach[type2Elements.get(it) += newElement.lookup(smt2logic)] + } + + return new Logic2SMT_TypeMapperInterpretation(type2Elements,logic2smt,smt2logic) + } +} \ No newline at end of file diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2Smt_TypeMapper_FilteredTypesSimple.xtend_ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2Smt_TypeMapper_FilteredTypesSimple.xtend_ new file mode 100644 index 00000000..79fc38e6 --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2Smt_TypeMapper_FilteredTypesSimple.xtend_ @@ -0,0 +1,463 @@ +package hu.bme.mit.inf.dslreasoner.smt.reasoner + +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTType +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type +import java.util.HashMap +import java.util.Map +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTInput +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDefinition +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTEnumLiteral +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTEnumeratedTypeDeclaration +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement +import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem +import hu.bme.mit.inf.dslreasoner.logic.model.builder.TypeScopes +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTDocument +import hu.bme.mit.inf.dslreasoner.smtLanguage.SmtLanguageFactory +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory +import java.util.List +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition +import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine +import org.eclipse.viatra.query.runtime.emf.EMFScope + +class Logic2Smt_TypeMapperTrace_FilteredTypesSimple implements Logic2Smt_TypeMapperTrace{ + public var Map independentClasses = new HashMap + /** + * SMT type for the new objects + */ + public var SMTEnumeratedTypeDeclaration objects + /** + * existing element -> SMT literal map + */ + public var Map elementMap = new HashMap + + public var SMTEnumeratedTypeDeclaration objectTypes + public var Map objectTypeMap = new HashMap + public var SMTFunctionDefinition objectTypeFunction + public var Map objectTypePredicates = new HashMap + + override copy(SMTInput newModel) { + val a = this + val b = new Logic2Smt_TypeMapperTrace_FilteredTypesSimple + + b.independentClasses = a.independentClasses.copyMap(newModel.typeDeclarations,[name]) + + b.objects = newModel.typeDeclarations.filter[it.name == a.objects.name].head as SMTEnumeratedTypeDeclaration + b.elementMap = a.elementMap.copyMap(b.objects.elements,[name]) + + b.objectTypes = newModel.typeDeclarations.filter[it.name == a.objects.name].head as SMTEnumeratedTypeDeclaration + b.objectTypeMap = a.objectTypeMap.copyMap(b.objectTypes.elements,[name]) + b.objectTypeFunction = newModel.functionDefinition.filter[it.name == a.objectTypeFunction.name].head + b.objectTypePredicates = a.objectTypePredicates.copyMap(newModel.functionDefinition,[name]) + + return b + } +} + +class Logic2Smt_TypeMapper_FilteredTypesSimple implements Logic2Smt_TypeMapper{ + val extension SmtLanguageFactory factory = SmtLanguageFactory.eINSTANCE + val LogiclanguageFactory factory2 = LogiclanguageFactory.eINSTANCE + + private def toID(List names) {names.join("!") } + private def toID(String name) {name.split("\\s+").toID} + + override transformTypes(SMTInput document, LogicProblem problem, Logic2SmtMapperTrace trace, TypeScopes scopes) { + val typeTrace = new Logic2Smt_TypeMapperTrace_FilteredTypes + trace.typeMapperTrace = typeTrace + val engine = ViatraQueryEngine.on(new EMFScope(problem)) + + val independentTypes = problem.types.filter(TypeDefinition).filter[isIndependentType] + + val connectedTypes = problem.types.filter[!isIndependentType] + val connectedElements = problem.elements.filter[!isIndependentElement] + + // 0. map the simple types + this.transformIndependentTypes(independentTypes,trace) + + // 1. Has old elements => create supertype for it + + this.transformDefinedElements(connectedElements, trace,document) + this.transformUndefinedElements(scopes,trace,document) + + + this.transforTypes(connectedTypes, connectedElements, trace, document, engine) + // 3.2: Type definition to new elements + if(hasNewElements) { + this.transformNewTypes(connectedTypesWithoutDefintypesWithoutDefinedSupertype,trace,document,engine); + } + } + + private def isIndependentType(Type t) { + val res = (t instanceof TypeDefinition) && t.supertypes.empty && t.subtypes.empty + return res + } + private def isIndependentElement(DefinedElement e) { + val types = e.definedInType + return types.size == 1 && types.head.isIndependentType + } + + protected def transformIndependentTypes(Iterable types,Logic2SmtMapperTrace trace) { + for(type: types) { + val independentSMTType = createSMTEnumeratedTypeDeclaration => [ + name = toID(#["oldType",type.name]) + ] + trace.typeTrace.independentClasses.put(type,independentSMTType) + for(element : type.elements) { + val enumLiteral = createSMTEnumLiteral => [it.name = toID(#["oldElement",element.name])] + independentSMTType.elements += enumLiteral + trace.typeTrace.elementMap.put(element,enumLiteral) + } + } + } + + protected def transformDefinedElements(Iterable oldElements, Logic2SmtMapperTrace trace, SMTInput document) { + val List literals = new ArrayList(oldElements.size) + for(element : oldElements) { + val elementName ='''oldElement «element.name»''' + val literal = createSMTEnumLiteral => [name = elementName.toID] + literals += literal + trace.typeTrace.elementMap.put(element,literal) + } + trace.typeTrace.oldObjects = createSMTEnumeratedTypeDeclaration => + [name = "oldObjects" it.elements += literals] + document.typeDeclarations += trace.typeTrace.oldObjects + } + + protected def transformUndefinedElements(TypeScopes scopes, Logic2SmtMapperTrace trace, SMTInput document) { + var SMTType newObjects + if(scopes.maxNewElements == -1) { + newObjects = createSMTSetTypeDeclaration => [ + name = "newObjects" + ] + } else { + val newElements = new ArrayList(scopes.maxNewElements) + for(index : (1.. [ + name = #["newElement",index.toString].toID + ] + newElements += literal + } + newObjects = createSMTEnumeratedTypeDeclaration => [ + name = "newObjects" + it.elements += newElements + ] + } + trace.typeTrace.newObjects = newObjects + document.typeDeclarations += newObjects + } + + protected def transformOldTypes(Iterable oldTypes,Iterable oldElements, Logic2SmtMapperTrace trace, SMTInput document, ViatraQueryEngine engine) { + val possibleTypeMatcher = PossibleDynamicTypeMatcher.on(engine) + val supertypeStarMatcher = SupertypeStarMatcher.on(engine) +// val possibleTypes = new LinkedList +// if(hasDefinedElement) possibleTypes += typesWithDefinedSupertype +// if(hasUndefinedElement) possibleTypes += typesWithoutDefinedSupertype +// val possibleConcreteTypes = possibleTypes.filter[!it.isIsAbstract] +// val possibleConcreteTypes = possibleTypeMatcher.allValuesOfdynamic + + // 3.1.1. cretate a type for old types + val possibleConcreteTypeLiterals = new ArrayList() + for(possibleConcreteType: oldTypes.filter[!isIsAbstract]) { + val typeName = '''oldType «possibleConcreteType.name»''' + val literal = createSMTEnumLiteral => [name = typeName.toID] + trace.typeTrace.oldObjectTypeMap.put(possibleConcreteType,literal) + possibleConcreteTypeLiterals+=literal + } + val oldObjectTypes = createSMTEnumeratedTypeDeclaration => [ + it.name = "oldTypes" + it.elements += possibleConcreteTypeLiterals + ] + trace.typeTrace.oldObjectTypes = oldObjectTypes + document.typeDeclarations += oldObjectTypes + + // 3.1.2 for each object, create a constant for its possible dynamic type + val Map possibleTypesOfElement = new HashMap + val Map onlyPossibleType = new HashMap + for(object: oldElements) { + val types = possibleTypeMatcher.getAllValuesOfdynamic(null,object) + if(types.size == 1) { + onlyPossibleType.put(object,types.head) + } else { // including 0 or more than 1 + // create a constant declaration + val typeOfObjectConstant = createSMTFunctionDeclaration => [ + it.name = toID(#["typeDecisions",toID(object.name)]) + it.range = createSMTComplexTypeReference => [ + it.referred = trace.typeTrace.oldObjectTypes + ] + ] + document.functionDeclarations += typeOfObjectConstant + possibleTypesOfElement.put(object,typeOfObjectConstant) + // add assertions to the constant to select valid values + document.assertions += createSMTAssertion => [ + val options = types.map[type | createSMTEquals => [ + it.leftOperand = createSMTSymbolicValue => [it.symbolicReference = typeOfObjectConstant] + it.rightOperand = createSMTSymbolicValue => [it.symbolicReference = type.lookup(trace.typeTrace.oldObjectTypeMap)] + ]] + it.value = if(options.empty) { + createSMTBoolLiteral => [it.value = false] + } else { + createSMTOr=>[operands += options] + } + ] + } + } + + // 3.1.2 create a function: old elements -> old types + val oldTypeFunction = createSMTFunctionDefinition => [ + it.name = "oldTypeFunction" + val o = createSMTSortedVariable => [ + it.name = "o" + it.range= createSMTComplexTypeReference => [it.referred = trace.typeTrace.oldObjects] + ] + it.parameters += o + it.range = createSMTComplexTypeReference => [it.referred = trace.typeTrace.oldObjectTypes] + it.value = unfoldITE(oldElements, + [createSMTSymbolicValue => [it.symbolicReference = o]], + [DefinedElement e | createSMTSymbolicValue => [it.symbolicReference = e.lookup(trace.typeTrace.elementMap)]], + [DefinedElement e | + if(onlyPossibleType.containsKey(e)) { + return createSMTSymbolicValue => [ + symbolicReference = e.lookup(onlyPossibleType).lookup(trace.typeTrace.oldObjectTypeMap) ] + } else { + return createSMTSymbolicValue => [ + symbolicReference = e.lookup(possibleTypesOfElement) + ] + } + ] + ) + ] + trace.typeTrace.oldObjectTypeFunction = oldTypeFunction + document.functionDefinition += oldTypeFunction + + // 3.1.3 create a predicate for each type: old object -> {true, false} + for(oldType: oldTypes) { + val oldTypePredicate = createSMTFunctionDefinition + oldTypePredicate.name = toID(#["oldTypePredicate",oldType.name.toID]) + val param = createSMTSortedVariable => [ + name = "o" + range = createSMTComplexTypeReference => [referred = trace.typeTrace.oldObjects] + ] + oldTypePredicate.parameters += param + oldTypePredicate.range = createSMTBoolTypeReference + val values = new LinkedList + for(concreteSupbtype : supertypeStarMatcher.getAllValuesOfsubtype(oldType).filter[!isIsAbstract]) { + val typeOfO = createSMTSymbolicValue => [ + it.symbolicReference = oldTypeFunction + it.parameterSubstitutions += createSMTSymbolicValue => [it.symbolicReference = param] + ] + val valueOfConcreteSupbtype = createSMTSymbolicValue => [ + it.symbolicReference = concreteSupbtype.lookup(trace.typeTrace.oldObjectTypeMap) + ] + values += createSMTEquals => [ + it.leftOperand = typeOfO + it.rightOperand = valueOfConcreteSupbtype + ] + } + oldTypePredicate.value = createSMTOr=>[it.operands +=values] + + document.functionDefinition += oldTypePredicate + trace.typeTrace.oldObjectTypePredicates.put(oldType,oldTypePredicate) + } + } + + protected def transformNewTypes( + Iterable typesWithoutDefinedSupertype, + Logic2SmtMapperTrace trace, SMTInput document, ViatraQueryEngine engine) + { + val supertypeStarMatcher = SupertypeStarMatcher.on(engine) + val possibleTypes = typesWithoutDefinedSupertype + val possibleConcreteTypes = possibleTypes.filter[!it.isIsAbstract].toList + + // 3.2.1. cretate a type for new types + val possibleConcreteTypeLiterals = new ArrayList() + for(possibleConcreteType: possibleConcreteTypes) { + val typeName = '''newType «possibleConcreteType.name»''' + val literal = createSMTEnumLiteral => [name = typeName.toID] + trace.typeTrace.newObjectTypeMap.put(possibleConcreteType,literal) + possibleConcreteTypeLiterals+=literal + } + val newObjectTypes = createSMTEnumeratedTypeDeclaration => [ + it.name = "newTypes" + it.elements += possibleConcreteTypeLiterals + ] + trace.typeTrace.newObjectTypes = newObjectTypes + document.typeDeclarations += newObjectTypes + + // 3.2.2 create a function: new elements -> new types + val newTypeFunction = createSMTFunctionDeclaration => [ + it.name = "newTypeFunction" + it.parameters += createSMTComplexTypeReference => [it.referred = trace.typeTrace.newObjects] + it.range = createSMTComplexTypeReference => [it.referred = trace.typeTrace.newObjectTypes] + ] + trace.typeTrace.newObjectTypeFunction = newTypeFunction + document.functionDeclarations += newTypeFunction + + // 3.1.3 create a predicate for each type: new type -> {true, false} + for(newType: possibleTypes) { + val newTypePredicate = createSMTFunctionDefinition + newTypePredicate.name = toID(#["newTypePredicate",newType.name.toID]) + val param = createSMTSortedVariable => [ + name = "o" + range = createSMTComplexTypeReference => [referred = trace.typeTrace.newObjects] + ] + newTypePredicate.parameters += param + newTypePredicate.range = createSMTBoolTypeReference + val values = new LinkedList + for(concreteSupbtype : supertypeStarMatcher.getAllValuesOfsubtype(newType).filter[!isIsAbstract]) { + if(possibleConcreteTypes.contains(concreteSupbtype)) { + val typeOfO = createSMTSymbolicValue => [ + it.symbolicReference = newTypeFunction + it.parameterSubstitutions += createSMTSymbolicValue => [it.symbolicReference = param] + ] + if(!trace.typeTrace.newObjectTypeMap.containsKey(concreteSupbtype)) { + println("gebasz") + } + val valueOfConcreteSupbtype = createSMTSymbolicValue => [ + it.symbolicReference = concreteSupbtype.lookup(trace.typeTrace.newObjectTypeMap) + ] + values+= createSMTEquals => [ + it.leftOperand = typeOfO + it.rightOperand = valueOfConcreteSupbtype + ] + } + } + newTypePredicate.value = createSMTOr=>[it.operands +=values] + + document.functionDefinition += newTypePredicate + trace.typeTrace.newObjectTypePredicates.put(newType,newTypePredicate) + } + } + + private def Logic2Smt_TypeMapperTrace_FilteredTypes getTypeTrace(Logic2SmtMapperTrace trace) { + val typeTrace = trace.typeMapperTrace + if(typeTrace instanceof Logic2Smt_TypeMapperTrace_FilteredTypes) { + return typeTrace + } else { + throw new IllegalArgumentException('''Unknown trace type: «typeTrace.class.name»''') + } + } + + private def boolean hasDefinedSupertype(Type type) { + if(type instanceof TypeDefinition) { + return true + } else { + if(type.supertypes.empty) return false + else return type.supertypes.exists[it.hasDefinedSupertype] + } + } + + def private SMTTerm unfoldITE(Iterable options, Function0 input, Function1 conditionOfOption, Function1 outputForOption) { + if(options.size == 1) { + return outputForOption.apply(options.head) + } else { + return createSMTITE => [ + it.condition = createSMTEquals => [ + leftOperand = input.apply + rightOperand = conditionOfOption.apply(options.head) + ] + it.^if = outputForOption.apply(options.head) + it.^else = unfoldITE(options.tail,input,conditionOfOption,outputForOption) + ] + } + } + + override transformSymbolicReference(DefinedElement referred,Logic2SmtMapperTrace trace) { + val x = referred.lookup(trace.typeTrace.elementMap) + new ComplexSubterm(#[],#[], + createSMTSymbolicValue => [it.symbolicReference = x], + new TypeDescriptor(x.eContainer as SMTEnumeratedTypeDeclaration) + ) + } + + override transformTypeReference(Type type, Logic2SmtMapperTrace trace) { + val list = new ArrayList + + if(trace.typeTrace.oldObjectTypePredicates.containsKey(type)) { + list += new TypeConstraint( + createSMTComplexTypeReference => [it.referred = trace.typeTrace.oldObjects], + [x|createSMTSymbolicValue => [ + it.symbolicReference = trace.typeTrace.oldObjectTypePredicates.get(type) + it.parameterSubstitutions += createSMTSymbolicValue => [it.symbolicReference = x]]] + ) + } + if(trace.typeTrace.newObjectTypePredicates.containsKey(type)) { + list += new TypeConstraint( + createSMTComplexTypeReference => [it.referred = trace.typeTrace.newObjects], + [x|createSMTSymbolicValue => [ + it.symbolicReference = trace.typeTrace.newObjectTypePredicates.get(type) + it.parameterSubstitutions += createSMTSymbolicValue => [it.symbolicReference = x]]] + ) + } + if(trace.typeTrace.independentClasses.containsKey(type)) { + list += new TypeConstraint( + createSMTComplexTypeReference => [it.referred = type.lookup(trace.typeTrace.independentClasses)], + null + ) + } + + if(list.empty) throw new AssertionError('''Typereference to type is «type.name» empty''') + if(list.exists[it.type == null]){ + throw new AssertionError('''Typereference to null!''') + } + return list + } + + override getTypeInterpretation(LogicProblem problem, SMTDocument document, SmtModelInterpretation interpretation, Logic2SmtMapperTrace trace) { + val model = document.output.getModelResult as SMTModelResult + val newTypeDec = trace.typeTrace.newObjects + var List newElements = null + + if(newTypeDec instanceof SMTSetTypeDeclaration) { + val newElementType = model.typeDefinitions.filter[ + (it.type as SMTComplexTypeReference).referred == newTypeDec + ].head + newElements = newElementType.elements.map[new ValueType(new TypeDescriptor(newTypeDec),it.symbolicReference)] + } else if(newTypeDec instanceof SMTEnumeratedTypeDeclaration) { + newElements = newTypeDec.elements.map[new ValueType(new TypeDescriptor(newTypeDec),it)] + } else throw new IllegalArgumentException('''Unknown type : «newTypeDec.class.name»''') + + val Map logic2smt = new HashMap + val Map smt2logic = new HashMap + + var index = 1; + for(newElement : newElements) { + val n = '''new «index++»''' + val logic = factory2.createDefinedElement => [it.name = n] + logic2smt.put(logic,newElement) + smt2logic.put(newElement.value as SMTSymbolicDeclaration,logic) + } + for(oldElement : problem.elements) { + val declaration = trace.typeTrace.oldObjectTypeMap.get(oldElement) + logic2smt.put(oldElement,new ValueType(new TypeDescriptor(trace.typeTrace.oldObjects),declaration)) + smt2logic.put(declaration,oldElement) + } + + val engine = ViatraQueryEngine.on(new EMFScope(problem)) + val supertypeStarMatcher = SupertypeStarMatcher.on(engine) + + val type2Elements = (trace.typeTrace.oldObjectTypeMap.keySet + + trace.typeTrace.newObjectTypeMap.keySet) + .toInvertedMap[new LinkedList] + + val inverseOldTypeMap = trace.typeTrace.oldObjectTypeMap.bijectiveInverse + for(oldElement: trace.typeTrace.elementMap.values) { + val type = interpretation.queryEngine.resolveFunctionDefinition( + trace.typeTrace.oldObjectTypeFunction,#[oldElement]) as SMTEnumLiteral + val dynamicType = type.lookup(inverseOldTypeMap) + val supertypes = supertypeStarMatcher.getAllValuesOfsupertype(dynamicType) + supertypes.forEach[type2Elements.get(it) += oldElement.lookup(smt2logic)] + } + + val inverseNewTypeMap = trace.typeTrace.newObjectTypeMap.bijectiveInverse + for(newElement: newElements.map[value as SMTSymbolicDeclaration]) { + val type = interpretation.queryEngine.resolveFunctionDeclaration( + trace.typeTrace.newObjectTypeFunction,#[newElement]) as SMTEnumLiteral + val dynamicType = type.lookup(inverseNewTypeMap) + val supertypes = supertypeStarMatcher.getAllValuesOfsupertype(dynamicType) + supertypes.forEach[type2Elements.get(it) += newElement.lookup(smt2logic)] + } + + return new Logic2SMT_TypeMapperInterpretation(type2Elements,logic2smt,smt2logic) + } + +} \ No newline at end of file diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2Smt_TypeMapper_Horizontal.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2Smt_TypeMapper_Horizontal.xtend new file mode 100644 index 00000000..a5abbb44 --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2Smt_TypeMapper_Horizontal.xtend @@ -0,0 +1,63 @@ +package hu.bme.mit.inf.dslreasoner.smt.reasoner + +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTInput +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem +import hu.bme.mit.inf.dslreasoner.logic.model.builder.TypeScopes +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTDocument +import java.util.List +import hu.bme.mit.inf.dslreasoner.smtLanguage.SmtLanguageFactory +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition + +class Logic2Smt_TypeMapperTrace_Horizontal implements Logic2Smt_TypeMapperTrace{ + + override copy(SMTInput newModel) { + throw new UnsupportedOperationException("TODO: auto-generated method stub") + } +} + +class Logic2Smt_TypeMapper_Horizontal implements Logic2Smt_TypeMapper { + val extension SmtLanguageFactory factory = SmtLanguageFactory.eINSTANCE + + private def toID(List names) {names.join("!") } + + override transformTypes(SMTInput document, LogicProblem problem, Logic2SmtMapperTrace trace, TypeScopes scopes) { + val typeTrace = new Logic2Smt_TypeMapperTrace_Horizontal + trace.typeMapperTrace = typeTrace + + // mapping of known elements + + } + + private def Logic2Smt_TypeMapperTrace_Horizontal getTypeTrace(Logic2SmtMapperTrace trace) { + val typeTrace = trace.typeMapperTrace + if(typeTrace instanceof Logic2Smt_TypeMapperTrace_Horizontal) { + return typeTrace + } else { + throw new IllegalArgumentException('''Unknown trace type: «typeTrace.class.name»''') + } + } + + private def boolean hasDefinedSupertype(Type type) { + if(type instanceof TypeDefinition) { + return true + } else { + if(type.supertypes.empty) return false + else return type.supertypes.exists[it.hasDefinedSupertype] + } + } + + override transformTypeReference(Type type, Logic2SmtMapperTrace trace) { + throw new UnsupportedOperationException("TODO: auto-generated method stub") + } + + override transformSymbolicReference(DefinedElement referred, Logic2SmtMapperTrace trace) { + throw new UnsupportedOperationException("TODO: auto-generated method stub") + } + + override getTypeInterpretation(LogicProblem problem, SMTDocument document, SmtModelInterpretation interpretation, Logic2SmtMapperTrace trace) { + throw new UnsupportedOperationException("TODO: auto-generated method stub") + } + +} \ No newline at end of file diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/SMTSolver.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/SMTSolver.xtend new file mode 100644 index 00000000..d371b89e --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/SMTSolver.xtend @@ -0,0 +1,49 @@ +package hu.bme.mit.inf.dslreasoner.smt.reasoner + +import hu.bme.mit.inf.dslreasoner.SmtLanguageStandaloneSetupGenerated +import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner +import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem +import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult +import hu.bme.mit.inf.dslreasoner.smt.reasoner.builder.SmtSolverHandler +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTDocument +import hu.bme.mit.inf.dslreasoner.smtLanguage.SmtLanguagePackage +import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace +import org.eclipse.emf.ecore.util.EcoreUtil + +class SMTSolver extends LogicReasoner{ + + public new() { + SmtLanguagePackage.eINSTANCE.eClass + val x = new SmtLanguageStandaloneSetupGenerated + x.createInjectorAndDoEMFRegistration + } + + val forwardMapper = new Logic2SmtMapper(new Logic2Smt_TypeMapper_FilteredTypes); + val backMapper = new Smt2LogicMapper; + val handler = new SmtSolverHandler + + override solve(LogicProblem problem, LogicSolverConfiguration configuration, ReasonerWorkspace workspace) { + if(configuration instanceof SmtSolverConfiguration) { + val transformationStart = System.currentTimeMillis + val transformationResult = forwardMapper.transformProblem(problem,configuration.typeScopes,configuration.strategy) + val SMTDocument inputModel= transformationResult.output + val trace = transformationResult.trace + val input = workspace.writeModel(inputModel,"problem.smt2") + val transformationTime = System.currentTimeMillis-transformationStart + val solverTimeStart = System.currentTimeMillis + handler.callSolver(input,configuration) + val solverTime = System.currentTimeMillis - solverTimeStart + val outputModel = workspace.reloadModel(typeof(SMTDocument), "problem.smt2") + EcoreUtil.resolveAll(outputModel) + workspace.deactivateModel("problem.smt2") + return backMapper.transformOutput(problem,outputModel.output,trace, transformationTime, solverTime) + } else throw new IllegalArgumentException('''The configuration have to be an «SmtSolverConfiguration.simpleName»!''') + } + + override getInterpretation(ModelResult modelResult) { + val representation = modelResult.representation as SMTDocument + val trace = modelResult.trace as Logic2SmtMapperTrace + return new SmtModelInterpretation(trace.problem,representation,trace.forwardMapper,trace) + } +} \ No newline at end of file diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Smt2LogicMapper.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Smt2LogicMapper.xtend new file mode 100644 index 00000000..cbabc7b0 --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Smt2LogicMapper.xtend @@ -0,0 +1,71 @@ +package hu.bme.mit.inf.dslreasoner.smt.reasoner + +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTOutput +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTStatisticsSection +import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTStatisticIntValue +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTStatisticDoubleValue +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTErrorResult +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSatResult +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTUnsupportedResult +import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException +import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTStatisticValue +import java.math.BigDecimal + +class Smt2LogicMapper { + val extension LogicresultFactory resultFactory = LogicresultFactory.eINSTANCE + + public def transformOutput(LogicProblem problem, SMTOutput output, Logic2SmtMapperTrace trace, long transformationTime, long solverTime) { + val satResult = output.satResult + if(satResult === null) { // Timeout + return createInsuficientResourcesResult => [ init(problem,output,transformationTime,solverTime) it.resourceName = "time"] + } else { + if(satResult instanceof SMTErrorResult) { + return createErrorResult => [init(problem,output,transformationTime,solverTime) message = satResult.message] + } else if(satResult instanceof SMTUnsupportedResult) { + return createUndecidableResult => [init(problem,output,transformationTime,solverTime)] + } else if(satResult instanceof SMTSatResult) { + if(satResult.sat) { + return createModelResult => [ + init(problem,output,transformationTime,solverTime) + representation += output.eContainer + it.trace = trace + ] + } else if(satResult.unsat) { + return createInconsistencyResult => [init(problem,output,transformationTime,solverTime)] + } else if(satResult.unknown) { + return createUndecidableResult => [init(problem,output,transformationTime,solverTime)] + } + } else throw new LogicReasonerException("The solver resulted with unknown result.") + } + } + + private def init(LogicResult result,LogicProblem problem, SMTOutput output, long transformationTime, long solverTime) { + result.problem = problem + result.statistics = output.statistics.transformStatistics(transformationTime,solverTime) + } + + protected def transformStatistics(SMTStatisticsSection section, long transformationTime, long solverTime) { + createStatistics => [ + it.transformationTime = transformationTime.intValue + it.solverTime = solverTime.intValue + + val memorySection = section.values.filter[it.name==":memory"].head + if(memorySection != null) { + it.solverMemory = ((memorySection as SMTStatisticDoubleValue).value.add(BigDecimal.valueOf(0.5))).intValue + } + entries += section.values.map[transformEntry] + ] + } + + protected def dispatch transformEntry(SMTStatisticIntValue entry) { + createIntStatisticEntry => [name = entry.exportName value = entry.value] } + protected def dispatch transformEntry(SMTStatisticDoubleValue entry) { + createRealStatisticEntry => [name = entry.exportName value = entry.value.doubleValue] } + + private def exportName(SMTStatisticValue value) { + return value.name.replaceFirst(":","") + } +} \ No newline at end of file diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/SmtModelInterpretation.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/SmtModelInterpretation.xtend new file mode 100644 index 00000000..fb0739ab --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/SmtModelInterpretation.xtend @@ -0,0 +1,167 @@ +package hu.bme.mit.inf.dslreasoner.smt.reasoner + +import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicModelInterpretation +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem +import hu.bme.mit.inf.dslreasoner.smt.reasoner.builder.SmtModelQueryEngine +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTDocument +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTInput +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSymbolicDeclaration +import org.eclipse.xtend.lib.annotations.Accessors +import org.eclipse.xtend.lib.annotations.Data + +import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDeclaration + +@Data +class ValueType { + TypeDescriptor descriptor + Object value +} + +class SmtModelInterpretation implements LogicModelInterpretation { + //val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE + @Accessors(PUBLIC_GETTER) val SmtModelQueryEngine queryEngine; + + // Trace info + val Logic2SmtMapperTrace newTrace; + val Logic2SMT_TypeMapperInterpretation typeInterpretation + + /** + * Creates a model builder which queries a logic structure. + * @param document The whole SMT2 document. + * @param trace The trace of the [Logic problem -> SMT problem] mapping + */ + new(LogicProblem problem, SMTDocument document, Logic2SmtMapper forwardMapper, Logic2SmtMapperTrace forwardTrace) { + //document.input.typeDeclarations.forEach[typeNames.put(it.name,it)] + + this.queryEngine = new SmtModelQueryEngine(document) + this.newTrace = initialiseNewTrace(document,forwardTrace) + this.typeInterpretation = forwardMapper.typeMapper.getTypeInterpretation(problem,document,this,newTrace) + } + + /** + * Creates a new trace from the logic model to the new smt file by using the old trace. + */ + def protected Logic2SmtMapperTrace initialiseNewTrace(SMTDocument document, Logic2SmtMapperTrace oldTrace) { + val i = document.input + + val res = new Logic2SmtMapperTrace => [ typeMapperTrace = oldTrace.typeMapperTrace.copy(i) ] + + for(entry : oldTrace.relationUnfolding.entrySet) { + val rel = entry.key + val descriptors = entry.value.map[old | + new Descriptor( + old.parameterTypes.map[copyTypeDescriptor(i)], + old.relation) + ] + res.relationUnfolding.put(rel,descriptors) + } + + for(entry : oldTrace.relationMap.entrySet) { + val desc = new Descriptor( + entry.key.parameterTypes.map[copyTypeDescriptor(i)], + entry.key.relation) + val fun = i.functionDeclarations.filter[it.name == entry.value.name].head + res.relationMap.put(desc,fun) + } + + return res + } + + def private copyTypeDescriptor(TypeDescriptor original, SMTInput i) { + if(original.complexType == null) return original + else { + val newType = i.typeDeclarations.filter[it.name == original.complexType.name].head + new TypeDescriptor(newType) + } + } + + /*def protected initialiseTypes(SMTDocument document) { + val model = document.output.getModelResult as SMTModelResult + val smtUndefinedType2LogicType = this.newTrace.typeDeclarationMap.bijectiveInverse + + for(cardinalityConstraint : model.typeDefinitions) { + val targetType = (cardinalityConstraint.type as SMTComplexTypeReference).referred as SMTSetTypeDeclaration + val List elementCollection = new LinkedList + for(element : cardinalityConstraint.elements.map[symbolicReference]) { + if(element instanceof SMTFunctionDeclaration) { + val definedElementRepresentation = createDefinedElement => [name += element.name.split("!")] + newElement2Constants.put(definedElementRepresentation,element) + newConstants2Elements.put(element,definedElementRepresentation) + } else{ + throw new UnsupportedOperationException( + "Unresolvable reference in cardinality constraint: " + element.class.name + ": " + element.name) + } + } + undefinedTypeDefinitions.put(targetType.lookup(smtUndefinedType2LogicType),elementCollection); + } + }*/ + + def private dispatch ValueType logicLiteral2SmtLiteral(Integer literal) { + new ValueType(TypeDescriptor::numericTypeDescriptor_Instance, literal) + } + def private dispatch ValueType logicLiteral2SmtLiteral(Boolean literal) { + new ValueType(TypeDescriptor::logicTypeDescriptor_Instance, literal) + } + def private dispatch ValueType logicLiteral2SmtLiteral(DefinedElement literal) { + this.typeInterpretation.logicElement2Smt(literal) + } + +// def private dispatch Object smt2Literal2LogicLiteral(Integer literal) { literal } +// def private dispatch Object smt2Literal2LogicLiteral(Boolean literal) { literal } +// def private dispatch Object smt2Literal2LogicLiteral(SMTSymbolicDeclaration literal) { +// this.typeInterpretation.smtElement2Logic(literal) +// } + + override getElements(Type type) { + return this.typeInterpretation.getElements(type) + } + + override getInterpretation(FunctionDeclaration function, Object[] parameterSubstitution) { + /*queryEngine.resolveFunctionDeclaration( + function.lookup(newTrace.functionDeclarationMap), + parameterSubstitution.map[logicLiteral2SmtLiteral] + ).smt2Literal2LogicLiteral*/ + throw new UnsupportedOperationException + } + + override getInterpretation(RelationDeclaration relation, Object[] parameterSubstitution) { + val transformedParameters = parameterSubstitution.map[logicLiteral2SmtLiteral] + + val smtFunction = new Descriptor( + transformedParameters.map[descriptor], + relation) + .lookup(newTrace.relationMap) + + val result = queryEngine.resolveFunctionDeclaration( + smtFunction as SMTFunctionDeclaration, + transformedParameters.map[value] + ) as Boolean + + return result + } + + override getInterpretation(ConstantDeclaration constant) { + /*queryEngine.resolveFunctionDeclaration( + constant.lookup(newTrace.constantDeclarationMap), + Collections.EMPTY_LIST + ).smt2Literal2LogicLiteral*/ + throw new UnsupportedOperationException + } + + override getMaximalInteger() { + 100 + //throw new UnsupportedOperationException("TODO: auto-generated method stub") + } + + override getMinimalInteger() { + -100 + //throw new UnsupportedOperationException("TODO: auto-generated method stub") + } +} \ No newline at end of file diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/SmtSolverConfiguration.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/SmtSolverConfiguration.xtend new file mode 100644 index 00000000..2a926cb6 --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/SmtSolverConfiguration.xtend @@ -0,0 +1,9 @@ +package hu.bme.mit.inf.dslreasoner.smt.reasoner + +import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTReasoningTactic + +class SmtSolverConfiguration extends LogicSolverConfiguration{ + public boolean fixRandomSeed = false + public SMTReasoningTactic strategy = null +} diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/TransformedSubterm.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/TransformedSubterm.xtend new file mode 100644 index 00000000..48952288 --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/TransformedSubterm.xtend @@ -0,0 +1,183 @@ +package hu.bme.mit.inf.dslreasoner.smt.reasoner + +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSortedVariable +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSymbolicValue +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTTerm +import hu.bme.mit.inf.dslreasoner.smtLanguage.SmtLanguageFactory +import java.util.ArrayList +import java.util.List +import java.util.Map +import org.eclipse.emf.ecore.EObject +import org.eclipse.emf.ecore.util.EcoreUtil +import org.eclipse.xtend.lib.annotations.Data +import java.util.HashMap +import java.util.LinkedList + +abstract class TransformedSubterm { + val static extension SmtLanguageFactory factory = SmtLanguageFactory.eINSTANCE + def LogicSubterm expectLogic() + def NumericSubterm expectNumber() + + def List getPossibleValues() + + public static def List> allCombinations(List... possibleValues) { + return allCombinations(possibleValues.toList) + } + public static def List> allCombinations(Iterable> possibleValues) { + if(possibleValues.size == 1) { + return possibleValues.head.map[x|#[x.copy]] + } else { + val head = possibleValues.head + val tails = possibleValues.tail.allCombinations + val res = new ArrayList(tails.size * head.size) + for(headElement : head) { + for(tail : tails) { + val combination = new ArrayList(tail.size+1) + combination.add(headElement) + combination.addAll(tail.map[copy]) + res.add(combination) + } + } + return res + } + } + + public static def resolveToLogic(List subterms, SMTTerm value) { + val allDefinitions = subterms.map[it.variables].flatten + val allPreconditions = subterms.map[it.preconditions].flatten + val preconditionedExpression = if(allPreconditions.empty) { + value + } else { + createSMTAnd => [it.operands += allPreconditions it.operands += value] + } + val quantifiedExpression = if(allDefinitions.empty) { + preconditionedExpression + } else { + createSMTForall => [ + it.quantifiedVariables += allDefinitions + it.expression = preconditionedExpression] + } + return quantifiedExpression + } +} + +@Data class SubtermOption { + List variables + List preconditions + SMTTerm expression + TypeDescriptor type + + public new( + List variables, + List preconditions, + SMTTerm expression, + TypeDescriptor type) + { + this.variables = variables + this.preconditions = preconditions + this.expression = expression + this.type = type + } + + public new( + List previousSubterms, + List newVariables, + List newPreconditions, + SMTTerm newExpression, + TypeDescriptor newType) + { + val old2New = new HashMap + variables = new LinkedList + for(variable : previousSubterms.map[getVariables].flatten) { + val newVariable = EcoreUtil.copy(variable) + old2New.put(variable,newVariable) + variables+=newVariable + } + + preconditions = new LinkedList + preconditions += previousSubterms.map[getPreconditions].flatten.map[x|EcoreUtil.copy(x)] + preconditions += newPreconditions.map[x|EcoreUtil.copy(x)] + preconditions.forEach[relinkAllVariableReference(old2New)] + + expression = EcoreUtil.copy(newExpression) + relinkAllVariableReference(expression,old2New) + + type = newType + } + + public def copy() { + val old2New = variables.toInvertedMap[EcoreUtil.copy(it)] + val newPreconditions = preconditions.map[EcoreUtil.copy(it)] + newPreconditions.forEach[it.relinkAllVariableReference(old2New)] + val newExpression = EcoreUtil.copy(expression) + return new SubtermOption(variables.map[old2New.get(it)],newPreconditions,newExpression,type) + } + + def private relinkAllVariableReference(EObject root,Map map) { + if(root instanceof SMTSymbolicValue) root.relinkVariableReference(map) + root.eAllContents().filter(SMTSymbolicValue).forEach[relinkVariableReference(map)] + } + def private relinkVariableReference(SMTSymbolicValue target,Map map) { + if(map.containsKey(target.symbolicReference)) { + target.symbolicReference = map.get(target.symbolicReference) + } + } +} + +@Data +class LogicSubterm extends TransformedSubterm{ + + SMTTerm value + override expectLogic() {return this} + override expectNumber() { throw new AssertionError("A term is not a number") } + + public new(SMTTerm expression) + { + this.value = expression + } + override getPossibleValues() { + #[new SubtermOption(#[],#[],value,TypeDescriptor::logicTypeDescriptor_Instance)] + } +} + +@Data +class NumericSubterm extends TransformedSubterm { + List values + + public new( + List variables, + List preconditions, + SMTTerm expression) { + this.values = #[new SubtermOption(variables,preconditions,expression,TypeDescriptor.numericTypeDescriptor_Instance)] + } + public new(List values) { + this.values = values + } + + override expectLogic() { throw new AssertionError("A term is not a logic value") } + override expectNumber() { return this } + + override getPossibleValues() { + values + } +} + +@Data +class ComplexSubterm extends TransformedSubterm { + List options + override expectLogic() { throw new AssertionError("A term is not a logic value") } + override expectNumber() { throw new AssertionError("A term is not a number") } + public new(List variables, + List preconditions, + SMTTerm expression, + TypeDescriptor type) + { + this.options = #[new SubtermOption(variables,preconditions,expression,type)] + } + public new(List subterms) { + this.options = subterms + } + override getPossibleValues() { + this.options + } +} diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/TypeDescriptor.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/TypeDescriptor.xtend new file mode 100644 index 00000000..1aa5cf04 --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/TypeDescriptor.xtend @@ -0,0 +1,44 @@ +package hu.bme.mit.inf.dslreasoner.smt.reasoner + +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTBoolTypeReference +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTComplexTypeReference +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTIntTypeReference +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTRealTypeReference +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTType +import java.util.List +import org.eclipse.xtend.lib.annotations.Accessors +import org.eclipse.xtend.lib.annotations.Data + +@Data +class Descriptor { + List parameterTypes + T relation +} + +@Data +class TypeDescriptor { + val boolean logic + val boolean numeric + val SMTType complexType + + @Accessors(PUBLIC_GETTER) + static val LogicTypeDescriptor_Instance = new TypeDescriptor(true,false,null) + @Accessors(PUBLIC_GETTER) + static val NumericTypeDescriptor_Instance = new TypeDescriptor(false,true,null) + + private new(boolean logic, boolean numeric, SMTType complexType) { + this.logic = logic + this.numeric = numeric + this.complexType = complexType + } + public new(SMTType complexType) { + this.logic = false + this.numeric = false + this.complexType = complexType + } + + def static dispatch createFromTypeReference(SMTBoolTypeReference ref) { return TypeDescriptor::LogicTypeDescriptor_Instance} + def static dispatch createFromTypeReference(SMTIntTypeReference ref) { return TypeDescriptor::NumericTypeDescriptor_Instance} + def static dispatch createFromTypeReference(SMTRealTypeReference ref) { return TypeDescriptor::NumericTypeDescriptor_Instance} + def static dispatch createFromTypeReference(SMTComplexTypeReference ref) { return new TypeDescriptor(false,false,ref.referred)} +} \ No newline at end of file diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/builder/SmtModelQueryEngine.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/builder/SmtModelQueryEngine.xtend new file mode 100644 index 00000000..a259d103 --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/builder/SmtModelQueryEngine.xtend @@ -0,0 +1,314 @@ +package hu.bme.mit.inf.dslreasoner.smt.reasoner.builder + +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTAnd +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTBoolLiteral +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTBoolTypeReference +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTComplexTypeReference +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTDocument +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTEnumLiteral +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTEnumeratedTypeDeclaration +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTEquals +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDeclaration +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDefinition +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTITE +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTInput +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTIntLiteral +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTIntTypeReference +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTMinus +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTModelResult +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTOutput +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSortedVariable +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSymbolicValue +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTTerm +import java.util.HashMap +import java.util.List +import java.util.Map + +class SmtModelQueryEngine { + private Map functionDeclarationToDefinitions = + new HashMap + + private val SMTInput input; + private val SMTOutput output + + new(SMTDocument model) { + val nameToFunctionDefiniton = new HashMap + input = model.input + var SMTModelResult modelResult = null + + output = model.output + if(output!=null) { + val result = output.getModelResult + if(result instanceof SMTModelResult) { + modelResult = result as SMTModelResult + } + } + + input.functionDefinition. + forEach[x|nameToFunctionDefiniton.put(x.name,x)] + if(modelResult!=null) + modelResult.newFunctionDefinitions. + forEach[x|nameToFunctionDefiniton.put(x.name,x)] + + input.functionDeclarations. + forEach[x|functionDeclarationToDefinitions.put(x,x.name.lookup(nameToFunctionDefiniton))] + if(modelResult!=null) + modelResult.newFunctionDeclarations. + forEach[x|functionDeclarationToDefinitions.put(x,x.name.lookup(nameToFunctionDefiniton))] + } + + def protected VALUE_TYPE lookup(KEY_TYPE key, Map map) { + return map.get(key) + } + + def protected dispatch getDefaultValue(SMTIntTypeReference reference) { 0 } + def protected dispatch getDefaultValue(SMTBoolTypeReference reference) { false } + def protected dispatch getDefaultValue(SMTComplexTypeReference reference) { + val type = reference.referred + if(type instanceof SMTEnumeratedTypeDeclaration) return type.elements.head + else { + val definition = (output.getModelResult as SMTModelResult).typeDefinitions.filter[it.type == type].head + return definition.elements.head + } + } + + def protected isTerminal( + SMTTerm term, + Map substitution) + { + /* + * An undefined function is a terminal. + */ + if(term instanceof SMTSymbolicValue) { + val symbolicValue = term as SMTSymbolicValue + + if(symbolicValue.symbolicReference instanceof SMTFunctionDeclaration) + { + val function = symbolicValue.symbolicReference as SMTFunctionDeclaration; + val hasDefinition = functionDeclarationToDefinitions.get(function) != null + return ! hasDefinition + } + else return false + } + /* + * A finite element is a terminal. + */ + else if(term instanceof SMTEnumLiteral) + return true + else return false + } + def protected resolveTerminal( + SMTTerm terminal, + Map substitution) + { + if(terminal instanceof SMTEnumLiteral) { + return terminal; + } + else if(terminal instanceof SMTSymbolicValue) { + val symbolicValue = terminal as SMTSymbolicValue + if(symbolicValue.symbolicReference instanceof SMTFunctionDeclaration) + { + val function = symbolicValue.symbolicReference as SMTFunctionDeclaration; + return function + } + } + } + + def public Object resolveFunctionDeclaration( + SMTFunctionDeclaration declaration, + List params) + { + + val definition = declaration.lookup(functionDeclarationToDefinitions) + if(definition == null) return declaration.range.defaultValue + else return definition.resolveFunctionDefinition(params) + } + def public Object resolveFunctionDefinition( + SMTFunctionDefinition definition, + List params) + { + if(params.nullOrEmpty && definition.parameters.nullOrEmpty) { + return definition.resolveFunctionDefinition(emptyMap) + } + else if(params.size!=definition.parameters.size) + throw new IllegalArgumentException( + "Incorrect number of parameters!") + else { + val substitution = new HashMap + if(! definition.parameters.nullOrEmpty) { + for(i : 0..definition.parameters.size-1) { + substitution.put( + definition.parameters.get(i), + params.get(i)) + } + } + val result=definition.resolveFunctionDefinition(substitution) + //System::out.println(definition.name+"("+params.map[toString] + ") = " + result) + return result + } + } + def protected Object resolveFunctionDefinition( + SMTFunctionDefinition definition, + Map substitution) + { + definition.value.resolveValue(substitution) + } + + def protected isBoolLiteral(SMTTerm term, Map substitution) { + term instanceof SMTBoolLiteral + } + def protected resolveBoolLiteral(SMTTerm boolValue, Map substitution) { + return (boolValue as SMTBoolLiteral).^value + } + + def protected isIntLiteral(SMTTerm term, Map substitution) { + term instanceof SMTIntLiteral || + (term instanceof SMTMinus && (term as SMTMinus).rightOperand==null) + } + def protected resolveIntLiteral(SMTTerm intValue, Map substitution) { + if(intValue instanceof SMTIntLiteral) return (intValue as SMTIntLiteral).^value + else return -((intValue as SMTMinus).leftOperand as SMTIntLiteral).value + } + + def protected isParameterValue( + SMTTerm term, + Map substitution) + { + if(term instanceof SMTSymbolicValue) { + return substitution.containsKey((term as SMTSymbolicValue).symbolicReference) + } + else return false + } + def protected Object resolveParameterValue( + SMTTerm term, + Map substitution) + { + return substitution.get((term as SMTSymbolicValue).symbolicReference); + } + + def protected isITE( + SMTTerm term, + Map substitution) + { + return term instanceof SMTITE; + } + def protected resolveITE( + SMTTerm term, + Map substitution) + { + val ite = term as SMTITE + val condition = ite.condition.resolveValue(substitution) as Boolean + + if(condition){ + return resolveValue(ite.^if,substitution) + }else{ + return resolveValue(ite.^else,substitution) + } + } + + def protected isAnd(SMTTerm term, Map substitution) { + term instanceof SMTAnd + } + def protected resolveAnd(SMTTerm term, Map substitution) { + val and = term as SMTAnd + for(operand : and.operands) { + val operandValue = operand.resolveValue(substitution) as Boolean + if(!operandValue) return false + } + return true + } + + def protected isEquals( + SMTTerm operand, + Map substitution) + { + return operand instanceof SMTEquals + } + def protected resolveEquals(SMTTerm term, Map substitution){ + val equals = term as SMTEquals + val left = equals.leftOperand.resolveValue(substitution) + val right = equals.rightOperand.resolveValue(substitution) + val res = left.equals(right) + return res + } + + def protected isFiniteElementReference(SMTTerm term, Map substitution) { + if(term instanceof SMTSymbolicValue) { + if((term as SMTSymbolicValue).symbolicReference instanceof SMTEnumLiteral) { + return true + } + } + return false; + } + def protected resolveFiniteElementReference(SMTTerm term, Map substitution) { + (term as SMTSymbolicValue).symbolicReference + } + + def protected isFunctionCall(SMTTerm term, Map substitution) { + if(term instanceof SMTSymbolicValue) { + val functionCall = (term as SMTSymbolicValue).symbolicReference + return functionCall instanceof SMTFunctionDeclaration || functionCall instanceof SMTFunctionDefinition + } + return false; + } + def protected resolveFunctionCall(SMTTerm term, Map substitution) { + if(term.isTerminal(substitution)) + { + return term.resolveTerminal(substitution); + } + else{ + val functionCall = term as SMTSymbolicValue + var SMTFunctionDefinition calledFunction; + var SMTFunctionDeclaration calledDeclaration; + if(functionCall.symbolicReference instanceof SMTFunctionDeclaration) { + calledDeclaration = functionCall.symbolicReference as SMTFunctionDeclaration + calledFunction = functionCall.symbolicReference.lookup(functionDeclarationToDefinitions)} + else { + calledDeclaration = null; + calledFunction = functionCall.symbolicReference as SMTFunctionDefinition + } + + val newSubstitution = new HashMap + if(! calledFunction.parameters.nullOrEmpty) { + for(i : 0..calledFunction.parameters.size-1) { + newSubstitution.put( + calledFunction.parameters.get(i), + functionCall.parameterSubstitutions.get(i).resolveValue(substitution) + ) + } + } + return calledFunction.resolveFunctionDefinition(newSubstitution) + } + } + + def protected Object resolveValue( + SMTTerm value, + Map substitution) + { + if(value instanceof SMTSymbolicValue){ + (value as SMTSymbolicValue).symbolicReference + } + + if(value.isTerminal(substitution)) { + return value.resolveTerminal(substitution) + }else if(value.isBoolLiteral(substitution)){ + return resolveBoolLiteral(value, substitution) + }else if(value.isIntLiteral(substitution)){ + return resolveIntLiteral(value, substitution) + }else if(value.isParameterValue(substitution)) { + return resolveParameterValue(value,substitution) + }else if(value.isITE(substitution)){ + return resolveITE(value, substitution) + }else if(value.isAnd(substitution)) { + return resolveAnd(value,substitution) + }else if(value.isEquals(substitution)) { + return resolveEquals(value,substitution) + }else if(value.isFiniteElementReference(substitution)) { + return resolveFiniteElementReference(value,substitution) + }else if(value.isFunctionCall(substitution)) { + return resolveFunctionCall(value,substitution) + }else{ + throw new IllegalArgumentException("Can not resolve this term: " + value) + } + } +} \ No newline at end of file diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/builder/SmtSolverHandler.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/builder/SmtSolverHandler.xtend new file mode 100644 index 00000000..38ae1dae --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/builder/SmtSolverHandler.xtend @@ -0,0 +1,64 @@ +package hu.bme.mit.inf.dslreasoner.smt.reasoner.builder + +import org.eclipse.emf.common.util.URI +import java.io.InputStream +import java.io.IOException +import java.io.FileWriter +import java.io.File +import java.io.BufferedReader +import java.io.InputStreamReader +import org.eclipse.emf.common.CommonPlugin +import hu.bme.mit.inf.dslreasoner.smt.reasoner.SmtSolverConfiguration + +class SmtSolverException extends Exception{ + new(String s) { super(s) } + new(String s, Exception e) { super(s,e) } +} + +class SmtSolverHandler { + public def callSolver(URI resourceURI, SmtSolverConfiguration configuration) { + val URI smtUri = CommonPlugin.resolve(resourceURI) + val File smtFile = new File(smtUri.toFileString()) + + val params = + '''/smt2 /st« + IF configuration.runtimeLimit != SmtSolverConfiguration::Unlimited» /T:«configuration.runtimeLimit»«ENDIF»« + IF configuration.memoryLimit != SmtSolverConfiguration::Unlimited» /memory:«configuration.memoryLimit»«ENDIF»« + IF configuration.fixRandomSeed» /rs:0«ENDIF + » «smtFile.path»''' + + val Runtime runTime = Runtime.getRuntime() + + try { + val process = runTime.exec(configuration.solverPath + " " + params) + + val FileWriter writer = new FileWriter(smtFile,true) + writer.append("\n--------------\n") + appendStream(writer, process.getInputStream()) + printStream(process.getErrorStream()) + writer.close + } catch (IOException e) { + throw new SmtSolverException( + "Error during the input/output handling of the reasoner.", e) + } + + return resourceURI + } + + def private void printStream(InputStream inputStream) throws IOException { + val BufferedReader input = new BufferedReader(new InputStreamReader(inputStream)) + var int line = -1 + while ((line = input.read()) != -1) { + System.out.print(line as char) + } + input.close() + } + + def private appendStream(FileWriter writer, InputStream inputStream) throws IOException { + val BufferedReader input = new BufferedReader(new InputStreamReader(inputStream)) + var int line = -1 + while ((line = input.read()) != -1) { + writer.append(line as char) + } + } +} \ No newline at end of file -- cgit v1.2.3-54-g00ecf