From 20f131a3f09edf8e1455f20b4f486629147e7eff Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Tue, 15 Jan 2019 12:44:33 -0500 Subject: Initial workspace setup --- .../.classpath | 9 + .../.gitignore | 1 + .../.project | 34 ++ .../.settings/org.eclipse.jdt.core.prefs | 7 + .../META-INF/MANIFEST.MF | 17 + .../build.properties | 4 + .../vampire/reasoner/queries/signatureQueries.vql | 1 + .../vampire/reasoner/queries/typeQueries.vql | 1 + .../reasoner/VampireAnalyzerConfiguration.xtend | 22 + .../vampire/reasoner/VampireSolver.xtend | 102 +++++ .../builder/Logic2VampireLanguageMapper.xtend | 386 ++++++++++++++++++ .../builder/Logic2VampireLanguageMapperTrace.xtend | 39 ++ ...ogic2VampireLanguageMapper_ConstantMapper.xtend | 42 ++ ...ogic2VampireLanguageMapper_RelationMapper.xtend | 183 +++++++++ .../Logic2VampireLanguageMapper_Support.xtend | 148 +++++++ .../Logic2VampireLanguageMapper_TypeMapper.xtend | 19 + ...guageMapper_TypeMapperTrace_FilteredTypes.xtend | 21 + ...reLanguageMapper_TypeMapper_FilteredTypes.xtend | 158 ++++++++ ...ireModelInterpretation_TypeInterpretation.xtend | 5 + ...retation_TypeInterpretation_FilteredTypes.xtend | 5 + .../.VampireAnalyzerConfiguration.xtendbin | Bin 0 -> 2685 bytes .../vampire/reasoner/.VampireSolver.xtendbin | Bin 0 -> 5463 bytes .../ecse/dslreasoner/vampire/reasoner/.gitignore | 4 + .../vampire/reasoner/TypeMappingTechnique.java | 6 + .../vampire/reasoner/VampireBackendSolver.java | 5 + .../vampire/reasoner/VampireSolver.java | 80 ++++ .../reasoner/VampireSolverConfiguration.java | 10 + .../builder/.Logic2VampireLanguageMapper.xtendbin | Bin 0 -> 17674 bytes .../.Logic2VampireLanguageMapperTrace.xtendbin | Bin 0 -> 3140 bytes ...c2VampireLanguageMapper_ConstantMapper.xtendbin | Bin 0 -> 3164 bytes ...c2VampireLanguageMapper_RelationMapper.xtendbin | Bin 0 -> 8247 bytes .../.Logic2VampireLanguageMapper_Support.xtendbin | Bin 0 -> 9398 bytes ...Logic2VampireLanguageMapper_TypeMapper.xtendbin | Bin 0 -> 3224 bytes ...geMapper_TypeMapperTrace_FilteredTypes.xtendbin | Bin 0 -> 2742 bytes ...anguageMapper_TypeMapper_FilteredTypes.xtendbin | Bin 0 -> 9278 bytes ...ModelInterpretation_TypeInterpretation.xtendbin | Bin 0 -> 1490 bytes ...ation_TypeInterpretation_FilteredTypes.xtendbin | Bin 0 -> 1691 bytes .../vampire/reasoner/builder/.gitignore | 11 + .../builder/Logic2VampireLanguageMapper.java | 442 +++++++++++++++++++++ .../builder/Logic2VampireLanguageMapperTrace.java | 34 ++ ...Logic2VampireLanguageMapper_ConstantMapper.java | 34 ++ ...Logic2VampireLanguageMapper_RelationMapper.java | 296 ++++++++++++++ .../Logic2VampireLanguageMapper_Support.java | 242 +++++++++++ .../Logic2VampireLanguageMapper_TypeMapper.java | 25 ++ ...ogic2VampireLanguageMapper_TypeMapperTrace.java | 5 + ...nguageMapper_TypeMapperTrace_FilteredTypes.java | 21 + ...ireLanguageMapper_TypeMapper_FilteredTypes.java | 287 +++++++++++++ ...pireModelInterpretation_TypeInterpretation.java | 5 + ...pretation_TypeInterpretation_FilteredTypes.java | 7 + 49 files changed, 2718 insertions(+) create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/.classpath create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/.gitignore create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/.project create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/.settings/org.eclipse.jdt.core.prefs create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/META-INF/MANIFEST.MF create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/build.properties create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/queries/ca/mcgill/ecse/dslreasoner/vampire/reasoner/queries/signatureQueries.vql create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/queries/ca/mcgill/ecse/dslreasoner/vampire/reasoner/queries/typeQueries.vql create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ConstantMapper.xtend create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtend create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation_TypeInterpretation.xtend create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtend create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.gitignore create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/TypeMappingTechnique.java create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireBackendSolver.java create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.java create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolverConfiguration.java create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtendbin create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtendbin create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.gitignore create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ConstantMapper.java create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapperTrace.java create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.java create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.java create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation_TypeInterpretation.java create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation_TypeInterpretation_FilteredTypes.java (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner') diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/.classpath b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/.classpath new file mode 100644 index 00000000..a1e0140b --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/.classpath @@ -0,0 +1,9 @@ + + + + + + + + + diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/.gitignore b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/.gitignore new file mode 100644 index 00000000..ae3c1726 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/.gitignore @@ -0,0 +1 @@ +/bin/ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/.project b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/.project new file mode 100644 index 00000000..2221f39c --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/.project @@ -0,0 +1,34 @@ + + + ca.mcgill.ecse.dslreasoner.vampire.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/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/.settings/org.eclipse.jdt.core.prefs b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/.settings/org.eclipse.jdt.core.prefs new file mode 100644 index 00000000..295926d9 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.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/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/META-INF/MANIFEST.MF b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/META-INF/MANIFEST.MF new file mode 100644 index 00000000..2eb4f151 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/META-INF/MANIFEST.MF @@ -0,0 +1,17 @@ +Manifest-Version: 1.0 +Bundle-ManifestVersion: 2 +Bundle-Name: Reasoner +Bundle-SymbolicName: ca.mcgill.ecse.dslreasoner.vampire.reasoner;singleton:=true +Bundle-Version: 1.0.0.qualifier +Automatic-Module-Name: ca.mcgill.ecse.dslreasoner.vampire.reasoner +Bundle-RequiredExecutionEnvironment: JavaSE-1.8 +Require-Bundle: org.eclipse.xtend.lib, + hu.bme.mit.inf.dslreasoner.logic.model;bundle-version="1.0.0", + hu.bme.mit.inf.dslreasoner.ecore2logic;bundle-version="1.0.0", + ca.mcgill.ecse.dslreasoner.vampire.language;bundle-version="1.0.0", + org.eclipse.viatra.query.runtime;bundle-version="2.1.0", + org.eclipse.viatra.query.runtime.base.itc;bundle-version="2.1.0" +Export-Package: ca.mcgill.ecse.dslreasoner.vampire.reasoner, + ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder + + diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/build.properties b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/build.properties new file mode 100644 index 00000000..41eb6ade --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/build.properties @@ -0,0 +1,4 @@ +source.. = src/ +output.. = bin/ +bin.includes = META-INF/,\ + . diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/queries/ca/mcgill/ecse/dslreasoner/vampire/reasoner/queries/signatureQueries.vql b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/queries/ca/mcgill/ecse/dslreasoner/vampire/reasoner/queries/signatureQueries.vql new file mode 100644 index 00000000..754b5ac7 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/queries/ca/mcgill/ecse/dslreasoner/vampire/reasoner/queries/signatureQueries.vql @@ -0,0 +1 @@ +package ca.mcgill.ecse.dslreasoner.vampire.reasoner.queries \ No newline at end of file diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/queries/ca/mcgill/ecse/dslreasoner/vampire/reasoner/queries/typeQueries.vql b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/queries/ca/mcgill/ecse/dslreasoner/vampire/reasoner/queries/typeQueries.vql new file mode 100644 index 00000000..754b5ac7 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/queries/ca/mcgill/ecse/dslreasoner/vampire/reasoner/queries/typeQueries.vql @@ -0,0 +1 @@ +package ca.mcgill.ecse.dslreasoner.vampire.reasoner.queries \ No newline at end of file diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend new file mode 100644 index 00000000..27e00ccf --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend @@ -0,0 +1,22 @@ +package ca.mcgill.ecse.dslreasoner.vampire.reasoner + +import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration + +class VampireSolverConfiguration extends LogicSolverConfiguration { + + public var int symmetry = 0 // by default + //choose needed backend solver +// public var VampireBackendSolver solver = VampireBackendSolver.SAT4J + public var boolean writeToFile = false +} + + +enum VampireBackendSolver { + //add needed things +} + + +enum TypeMappingTechnique { + //default + FilteredTypes +} \ No newline at end of file diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend new file mode 100644 index 00000000..64484b88 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend @@ -0,0 +1,102 @@ +package ca.mcgill.ecse.dslreasoner.vampire.reasoner + +import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetupGenerated +import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner +import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException +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 ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage +import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace +import java.io.PrintWriter +import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetup +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapper +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes + +class VampireSolver extends LogicReasoner{ + + new() { + VampireLanguagePackage.eINSTANCE.eClass + val x = new VampireLanguageStandaloneSetupGenerated + VampireLanguageStandaloneSetup::doSetup() + } + + val Logic2VampireLanguageMapper forwardMapper = new Logic2VampireLanguageMapper(new Logic2VampireLanguageMapper_TypeMapper_FilteredTypes) +// //not for now +// val VampireHandler handler = new VampireHandler +// val Vampire2LogicMapper backwardMapper = new Vampire2LogicMapper + + val fileName = "problem.tptp" + + override solve(LogicProblem problem, LogicSolverConfiguration configuration, ReasonerWorkspace workspace) throws LogicReasonerException { + val vampireConfig = configuration.asConfig + + // Start: Logic -> Vampire mapping + val transformationStart = System.currentTimeMillis + //TODO + val result = forwardMapper.transformProblem(problem,vampireConfig) + val vampireProblem = result.output + val forwardTrace = result.trace + + var String fileURI = null; + var String vampireCode = null; + if(vampireConfig.writeToFile) { + fileURI = workspace.writeModel(vampireProblem,fileName).toFileString + } else { + vampireCode = workspace.writeModelToString(vampireProblem,fileName) + } + val transformationTime = System.currentTimeMillis - transformationStart + // Finish: Logic -> Vampire mapping + + //Creates a file containing the tptp code after transformation + val out = new PrintWriter("output/files/vampireCode.tptp") + out.println(vampireCode) + out.close() + + + /* + * not for now -> Start: Solving Alloy problem + * + // Start: Solving Alloy problem + val solverStart = System.currentTimeMillis + val result2 = handler.callSolver(alloyProblem,workspace,alloyConfig,fileURI,alloyCode) + val logicResult = backwardMapper.transformOutput(problem,configuration.solutionScope.numberOfRequiredSolution,result2,forwardTrace,transformationTime) + val solverFinish = System.currentTimeMillis-solverStart + // Finish: Solving Alloy problem + + if(vampireConfig.writeToFile) workspace.deactivateModel(fileName) + + return logicResult + */ + + return null // for now + } + + def asConfig(LogicSolverConfiguration configuration){ + if(configuration instanceof VampireSolverConfiguration) { + return configuration + } else { + throw new IllegalArgumentException('''The configuration have to be an «VampireSolverConfiguration.simpleName»!''') + } + } + +// /* +// * not for now +// * + override getInterpretations(ModelResult modelResult) { + //val answers = (modelResult.representation as MonitoredAlloySolution).aswers.map[key] +// val sols = modelResult.representation// as List +// //val res = answers.map +// sols.map[ +// new VampireModelInterpretation( +// forwardMapper.typeMapper.typeInterpreter, +// it as A4Solution, +// forwardMapper, +// modelResult.trace as Logic2AlloyLanguageMapperTrace +// ) +// ] + } +// */ + +} \ No newline at end of file diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend new file mode 100644 index 00000000..5ec15541 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend @@ -0,0 +1,386 @@ +package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder + +import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput +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.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.FunctionDeclaration +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDefinition +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.Not +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Or +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealLiteral +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation +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 ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel +import java.util.Collections +import java.util.HashMap +import java.util.List +import java.util.Map +import org.eclipse.xtend.lib.annotations.Accessors + +import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* + +class Logic2VampireLanguageMapper { + private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE + private val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support; + @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_ConstantMapper constantMapper = new Logic2VampireLanguageMapper_ConstantMapper( + this) + @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_RelationMapper relationMapper = new Logic2VampireLanguageMapper_RelationMapper( + this) + @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_TypeMapper typeMapper + + public new(Logic2VampireLanguageMapper_TypeMapper typeMapper) { + this.typeMapper = typeMapper + } + + public def TracedOutput transformProblem(LogicProblem problem, + VampireSolverConfiguration configuration) { + // create model bases + // TODO + val initialComment = createVLSComment => [ + it.comment = "%This is an initial Test Comment \r" + ] + + val specification = createVampireModel => [ + it.comments += initialComment + ] + + val trace = new Logic2VampireLanguageMapperTrace => [ + it.specification = specification + +// it.incQueryEngine = viatraQueryEngine.on(new EMFScope(problem)) + ] + + // call mappers + if (!problem.types.isEmpty) { + typeMapper.transformTypes(problem.types, problem.elements, this, trace) + } + + trace.constantDefinitions = problem.collectConstantDefinitions + trace.relationDefinitions = problem.collectRelationDefinitions + + problem.relations.forEach[this.relationMapper.transformRelation(it, trace)] + + // only transforms definitions + // problem.constants.filter(ConstantDefinition).forEach[this.constantMapper.transformConstant(it, trace)] + problem.constants.filter(ConstantDefinition).forEach [ + this.constantMapper.transformConstantDefinitionSpecification(it, trace) + ] + + // ////////////////// + // Transform Assertions + // ////////////////// + for (assertion : problem.assertions) { + transformAssertion(assertion, trace) + } + + return new TracedOutput(specification, trace) + } + + // End of transformProblem + // //////////// + // Type References + // //////////// + def dispatch protected VLSTerm transformTypeReference(BoolTypeReference boolTypeReference, + Logic2VampireLanguageMapperTrace trace) { + // TODO, Not Now + // return createALSReference => [ it.referred = support.getBooleanType(trace) ] + } + + // //////////// + // Collectors + // //////////// + // exact Same as for Alloy + private def collectConstantDefinitions(LogicProblem problem) { + val res = new HashMap + problem.constants.filter(ConstantDefinition).filter[it.defines !== null].forEach [ + res.put(it.defines, it) + ] + return res + } + + private def collectRelationDefinitions(LogicProblem problem) { + val res = new HashMap + problem.relations.filter(RelationDefinition).filter[it.defines !== null].forEach [ + res.put(it.defines, it) + ] + return res + } + + // //////////// + // Assertions + Terms + // //////////// + def protected transformAssertion(Assertion assertion, Logic2VampireLanguageMapperTrace trace) { + val res = createVLSFofFormula => [ + it.name = support.toID(assertion.name) + // below is temporary solution + it.fofRole = "axiom" + it.fofFormula = assertion.value.transformTerm(trace, Collections.EMPTY_MAP) + // it.annotation = nothing + ] + trace.specification.formulas += res + } + + def dispatch protected VLSTerm transformTerm(BoolLiteral literal, Logic2VampireLanguageMapperTrace trace, + Map variables) { + if (literal.value == true) { + createVLSTrue + } else { + createVLSFalse + } + } + + def dispatch protected VLSTerm transformTerm(IntLiteral literal, Logic2VampireLanguageMapperTrace trace, + Map variables) { + createVLSInt => [it.value = literal.value.toString()] + } + + def dispatch protected VLSTerm transformTerm(RealLiteral literal, Logic2VampireLanguageMapperTrace trace, + Map variables) { + createVLSReal => [it.value = literal.value.toString()] + } + + def dispatch protected VLSTerm transformTerm(Not not, Logic2VampireLanguageMapperTrace trace, + Map variables) { + createVLSUnaryNegation => [operand = not.operand.transformTerm(trace, variables)] + } + + def dispatch protected VLSTerm transformTerm(And and, Logic2VampireLanguageMapperTrace trace, + Map variables) { support.unfoldAnd(and.operands.map[transformTerm(trace, variables)]) } + + def dispatch protected VLSTerm transformTerm(Or or, Logic2VampireLanguageMapperTrace trace, + Map variables) { support.unfoldOr(or.operands.map[transformTerm(trace, variables)]) } + + def dispatch protected VLSTerm transformTerm(Impl impl, Logic2VampireLanguageMapperTrace trace, + Map variables) { + createVLSImplies => [ + left = impl.leftOperand.transformTerm(trace, variables) + right = impl.rightOperand.transformTerm(trace, variables) + ] + } + + def dispatch protected VLSTerm transformTerm(Iff iff, Logic2VampireLanguageMapperTrace trace, + Map variables) { + createVLSEquivalent => [ + left = iff.leftOperand.transformTerm(trace, variables) + right = iff.rightOperand.transformTerm(trace, variables) + ] + } + +// def dispatch protected VLSTerm transformTerm(MoreThan moreThan, Logic2VampireLanguageMapperTrace trace, Map variables) { +// createALSMore => [leftOperand = moreThan.leftOperand.transformTerm(trace,variables) rightOperand = moreThan.rightOperand.transformTerm(trace,variables)] } +// def dispatch protected VLSTerm transformTerm(LessThan lessThan, Logic2VampireLanguageMapperTrace trace, Map variables) { +// createALSLess => [leftOperand = lessThan.leftOperand.transformTerm(trace,variables) rightOperand = lessThan.rightOperand.transformTerm(trace,variables)] } +// def dispatch protected VLSTerm transformTerm(MoreOrEqualThan moreThan, Logic2VampireLanguageMapperTrace trace, Map variables) { +// createALSMeq => [leftOperand = moreThan.leftOperand.transformTerm(trace,variables) rightOperand = moreThan.rightOperand.transformTerm(trace,variables)] } +// def dispatch protected VLSTerm transformTerm(LessOrEqualThan lessThan, Logic2VampireLanguageMapperTrace trace, Map variables) { +// createALSLeq => [leftOperand = lessThan.leftOperand.transformTerm(trace,variables) rightOperand = lessThan.rightOperand.transformTerm(trace,variables)] } + def dispatch protected VLSTerm transformTerm(Equals equals, Logic2VampireLanguageMapperTrace trace, + Map variables) { + createVLSEquality => [ + left = equals.leftOperand.transformTerm(trace, variables) + right = equals.rightOperand.transformTerm(trace, variables) + ] + } + + def dispatch protected VLSTerm transformTerm(Distinct distinct, Logic2VampireLanguageMapperTrace trace, Map variables) { + support.unfoldDistinctTerms(this,distinct.operands,trace,variables) } +// +// def dispatch protected ALSTerm transformTerm(Plus plus, Logic2AlloyLanguageMapperTrace trace, Map variables) { +// createALSFunctionCall => [it.params += plus.leftOperand.transformTerm(trace,variables) it.params += plus.rightOperand.transformTerm(trace,variables) it.referredNumericOperator = ALSNumericOperator.PLUS] } +// def dispatch protected ALSTerm transformTerm(Minus minus, Logic2AlloyLanguageMapperTrace trace, Map variables) { +// createALSFunctionCall => [it.params += minus.leftOperand.transformTerm(trace,variables) it.params += minus.rightOperand.transformTerm(trace,variables) it.referredNumericOperator = ALSNumericOperator.SUB] } +// def dispatch protected ALSTerm transformTerm(Multiply multiply, Logic2AlloyLanguageMapperTrace trace, Map variables) { +// createALSFunctionCall => [it.params += multiply.leftOperand.transformTerm(trace,variables) it.params += multiply.rightOperand.transformTerm(trace,variables) it.referredNumericOperator = ALSNumericOperator.MUL] } +// def dispatch protected ALSTerm transformTerm(Divison div, Logic2AlloyLanguageMapperTrace trace, Map variables) { +// createALSFunctionCall => [it.params += div.leftOperand.transformTerm(trace,variables) it.params += div.rightOperand.transformTerm(trace,variables) it.referredNumericOperator = ALSNumericOperator.DIV] } +// def dispatch protected ALSTerm transformTerm(Mod mod, Logic2AlloyLanguageMapperTrace trace, Map variables) { +// createALSFunctionCall => [it.params += mod.leftOperand.transformTerm(trace,variables) it.params += mod.rightOperand.transformTerm(trace,variables) it.referredNumericOperator = ALSNumericOperator.REM] } +// + def dispatch protected VLSTerm transformTerm(Forall forall, Logic2VampireLanguageMapperTrace trace, + Map variables) { + support.createUniversallyQuantifiedExpression(this, forall, trace, variables) + } + + def dispatch protected VLSTerm transformTerm(Exists exists, Logic2VampireLanguageMapperTrace trace, + Map variables) { + support.createExistentiallyQuantifiedExpression(this, exists, trace, variables) + } + + def dispatch protected VLSTerm transformTerm(InstanceOf instanceOf, Logic2VampireLanguageMapperTrace trace, Map variables) { + return createVLSFunction => [ + it.constant = support.toIDMultiple("type", (instanceOf.range as ComplexTypeReference).referred.name ) + it.terms += instanceOf.value.transformTerm(trace, variables) + ] + } +// +// def dispatch protected ALSTerm transformTerm(TransitiveClosure tc, Logic2AlloyLanguageMapperTrace trace, Map variables) { +// return this.relationMapper.transformTransitiveRelationReference( +// tc.relation, +// tc.leftOperand.transformTerm(trace,variables), +// tc.rightOperand.transformTerm(trace,variables), +// trace +// ) +// } +// + def dispatch protected VLSTerm transformTerm(SymbolicValue symbolicValue, Logic2VampireLanguageMapperTrace trace, + Map variables) { + symbolicValue.symbolicReference.transformSymbolicReference(symbolicValue.parameterSubstitutions, trace, + variables) + } + + def dispatch protected VLSTerm transformSymbolicReference(DefinedElement referred, + List parameterSubstitutions, Logic2VampireLanguageMapperTrace trace, + Map variables) { + typeMapper.transformReference(referred, trace) + } + + def dispatch protected VLSTerm transformSymbolicReference(ConstantDeclaration constant, + List parameterSubstitutions, Logic2VampireLanguageMapperTrace trace, + Map variables) { + // might need to make sure that only declared csts get transformed. see for Alloy + val res = createVLSConstant => [ + // ask if necessary VLSConstantDeclaration and not just directly strng + it.name = support.toID(constant.name) + ] + // no postprocessing cuz booleans are accepted + return res + } + + // NOT NEEDED FOR NOW + // TODO + def dispatch protected VLSTerm transformSymbolicReference(ConstantDefinition constant, + List parameterSubstitutions, Logic2VampireLanguageMapperTrace trace, + Map variables) { +// val res = createVLSFunctionCall => [ +// it.referredDefinition = constant.lookup(trace.constantDefinition2Function) +// ] +// return support.postprocessResultOfSymbolicReference(constant.type,res,trace) + } + + def dispatch protected VLSTerm transformSymbolicReference(Variable variable, + List parameterSubstitutions, Logic2VampireLanguageMapperTrace trace, + Map variables) { + + // cannot treat variable as function (constant) because of name ID not being the same + // below does not work + val res = createVLSVariable => [ +// it.name = support.toIDMultiple("Var", variable.lookup(variables).name) + it.name = support.toID(variable.lookup(variables).name) + ] + // no need for potprocessing cuz booleans are supported + return res + } + + // TODO + def dispatch protected VLSTerm transformSymbolicReference(FunctionDeclaration function, + List parameterSubstitutions, Logic2VampireLanguageMapperTrace trace, + Map variables) { +// if(trace.functionDefinitions.containsKey(function)) { +// return this.transformSymbolicReference(function.lookup(trace.functionDefinitions),parameterSubstitutions,trace,variables) +// } else { +// if(functionMapper.transformedToHostedField(function,trace)) { +// val param = parameterSubstitutions.get(0).transformTerm(trace,variables) +// val res = createVLSJoin => [ +// leftOperand = support.prepareParameterOfSymbolicReference(function.parameters.get(0),param,trace) +// rightOperand = createVLSReference => [referred = function.lookup(trace.functionDeclaration2HostedField)] +// ] +// return support.postprocessResultOfSymbolicReference(function.range,res,trace) +// } else { +// val functionExpression = createVLSJoin=>[ +// leftOperand = createVLSReference => [referred = trace.logicLanguage] +// rightOperand = createVLSReference => [referred = function.lookup(trace.functionDeclaration2LanguageField)] +// ] +// val res = support.unfoldDotJoin(this,parameterSubstitutions,functionExpression,trace,variables) +// return support.postprocessResultOfSymbolicReference(function.range,res,trace) +// } +// } + } + + // TODO + def dispatch protected VLSTerm transformSymbolicReference(FunctionDefinition function, + List parameterSubstitutions, Logic2VampireLanguageMapperTrace trace, + Map variables) { +// val result = createVLSFunctionCall => [ +// it.referredDefinition = function.lookup(trace.functionDefinition2Function) +// it.params += parameterSubstitutions.map[it.transformTerm(trace,variables)] +// ] +// return support.postprocessResultOfSymbolicReference(function.range,result,trace) + } + + // TODO + /* + def dispatch protected VLSTerm transformSymbolicReference(Relation relation, + List parameterSubstitutions, Logic2VampireLanguageMapperTrace trace, + Map variables) { + if (trace.relationDefinitions.containsKey(relation)) { + this.transformSymbolicReference(relation.lookup(trace.relationDefinitions), + parameterSubstitutions, trace, variables) + } + else { +// if (relationMapper.transformToHostedField(relation, trace)) { +// val VLSRelation = relation.lookup(trace.relationDeclaration2Field) +// // R(a,b) => +// // b in a.R +// return createVLSSubset => [ +// it.leftOperand = parameterSubstitutions.get(1).transformTerm(trace, variables) +// it.rightOperand = createVLSJoin => [ +// it.leftOperand = parameterSubstitutions.get(0).transformTerm(trace, variables) +// it.rightOperand = createVLSReference => [it.referred = VLSRelation] +// ] +// ] +// } else { +// val target = createVLSJoin => [ +// leftOperand = createVLSReference => [referred = trace.logicLanguage] +// rightOperand = createVLSReference => [ +// referred = relation.lookup(trace.relationDeclaration2Global) +// ] +// ] +// val source = support.unfoldTermDirectProduct(this, parameterSubstitutions, trace, variables) +// +// return createVLSSubset => [ +// leftOperand = source +// rightOperand = target +// ] +// } + } + } + */ + + // TODO + def dispatch protected VLSTerm transformSymbolicReference(Relation relation, + List parameterSubstitutions, Logic2VampireLanguageMapperTrace trace, + Map variables) { +// createVLSFunction => [ +// it.referredDefinition = relation.lookup(trace.relationDefinition2Predicate) +// it.params += parameterSubstitutions.map[p|p.transformTerm(trace, variables)] +// ] + return createVLSFunction => [ + it.constant = support.toIDMultiple("rel", relation.name) + it.terms += parameterSubstitutions.map[p | p.transformTerm(trace,variables)] + ] + } + + } + \ No newline at end of file diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend new file mode 100644 index 00000000..135b3f07 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend @@ -0,0 +1,39 @@ +package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder + +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.RelationDeclaration +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel +import java.util.HashMap +import java.util.Map + +interface Logic2VampireLanguageMapper_TypeMapperTrace {} + +class Logic2VampireLanguageMapperTrace { +// public var ViatraQueryEngine incQueryEngine; + + //list of needed VLS components + public var VampireModel specification + public var VLSFofFormula logicLanguageBody + public var VLSTerm formula +//NOT NEEDED //public var VLSFunction constantDec + + public var Logic2VampireLanguageMapper_TypeMapperTrace typeMapperTrace + + +//NOT NEEDED //public val Map constantDeclaration2LanguageField = new HashMap + //public val Map constantDefinition2Function = new HashMap + + public var Map constantDefinitions + + public var Map relationDefinitions + public val Map relationVar2VLS = new HashMap + public val Map relationVar2TypeDec = new HashMap + +} \ No newline at end of file diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ConstantMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ConstantMapper.xtend new file mode 100644 index 00000000..2366ea15 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ConstantMapper.xtend @@ -0,0 +1,42 @@ +package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder + +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDefinition +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory + +class Logic2VampireLanguageMapper_ConstantMapper { + private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE + private val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support + val Logic2VampireLanguageMapper base + + public new(Logic2VampireLanguageMapper base) { + this.base = base + } + +//NOT NEEDED +// def protected dispatch transformConstant(ConstantDeclaration constant, Logic2VampireLanguageMapperTrace trace) { +// val c = createVLSFunctionDeclaration=> [ +// it.name = support.toID(constant.name) +// ] +// trace.constantDec.constant = c +// trace.constantDeclaration2LanguageField.put(constant, c); +// +// } + +//NOT Used In Sample + def protected dispatch transformConstant(ConstantDefinition constant, Logic2VampireLanguageMapperTrace trace) { + //error + //TODO +// val c = createVLSFofFormula=> [ +// name = support.toID(constant.name) +// fofRole = "axiom" +// fofFormula = base.transformTypeReference() +// ] + } + + def protected transformConstantDefinitionSpecification(ConstantDefinition constant, Logic2VampireLanguageMapperTrace trace) { + //TODO + } + + +} \ No newline at end of file diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend new file mode 100644 index 00000000..60653a42 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend @@ -0,0 +1,183 @@ +package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder + +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference +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.Variable +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory +import java.util.ArrayList +import java.util.HashMap +import java.util.List +import java.util.Map + +import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* + +class Logic2VampireLanguageMapper_RelationMapper { + private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE + private val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support + val Logic2VampireLanguageMapper base + + public new(Logic2VampireLanguageMapper base) { + this.base = base + } + + def dispatch public void transformRelation(RelationDefinition r, Logic2VampireLanguageMapperTrace trace) { + + // 1. store all variables in support wrt their name + // 1.1 if variable has type, creating list of type declarations + val Map relationVar2VLS = new HashMap + val Map relationVar2TypeDecComply = new HashMap + val Map relationVar2TypeDecRes = new HashMap + val typedefs = new ArrayList + for (variable : r.variables) { + val v = createVLSVariable => [ + it.name = support.toIDMultiple("Var", variable.name) + ] + relationVar2VLS.put(variable, v) + + val varTypeComply = createVLSFunction => [ + it.constant = support.toIDMultiple("type", (variable.range as ComplexTypeReference).referred.name) + it.terms += createVLSVariable => [ + it.name = support.toIDMultiple("Var", variable.name) + ] + ] + relationVar2TypeDecComply.put(variable, varTypeComply) + + val varTypeRes = createVLSFunction => [ + it.constant = support.toIDMultiple("type", (variable.range as ComplexTypeReference).referred.name) + it.terms += createVLSVariable => [ + it.name = support.toIDMultiple("Var", variable.name) + ] + ] + relationVar2TypeDecRes.put(variable, varTypeRes) + } + + val comply = createVLSFofFormula => [ + it.name = support.toIDMultiple("compliance", r.name) + it.fofRole = "axiom" + it.fofFormula = createVLSUniversalQuantifier => [ + for (variable : r.variables) { + val v = createVLSVariable => [ + it.name = variable.lookup(relationVar2VLS).name + ] + it.variables += v + + } + it.operand = createVLSImplies => [ + it.left = createVLSFunction => [ + it.constant = support.toIDMultiple("rel", r.name) + for (variable : r.variables) { + val v = createVLSVariable => [ + it.name = variable.lookup(relationVar2VLS).name + ] + it.terms += v + } + ] + it.right = support.unfoldAnd(new ArrayList(relationVar2TypeDecComply.values)) + ] + ] + ] + + val res = createVLSFofFormula => [ + it.name = support.toIDMultiple("relation", r.name) + it.fofRole = "axiom" + it.fofFormula = createVLSUniversalQuantifier => [ + for (variable : r.variables) { + val v = createVLSVariable => [ + it.name = variable.lookup(relationVar2VLS).name + ] + it.variables += v + + } + it.operand = createVLSImplies => [ + it.left = support.unfoldAnd(new ArrayList(relationVar2TypeDecRes.values)) + it.right = createVLSEquivalent => [ + it.left = createVLSFunction => [ + it.constant = support.toIDMultiple("rel", r.name) + for (variable : r.variables) { + val v = createVLSVariable => [ + it.name = variable.lookup(relationVar2VLS).name + ] + it.terms += v + + } + ] + it.right = base.transformTerm(r.value, trace, relationVar2VLS) + ] + + ] + + ] + + ] + + // trace.relationDefinition2Predicate.put(r,res) + trace.specification.formulas += comply; + trace.specification.formulas += res; + + } + + def dispatch public void transformRelation(RelationDeclaration r, Logic2VampireLanguageMapperTrace trace) { + + // 1. store all variables in support wrt their name + // 1.1 if variable has type, creating list of type declarations + val List relationVar2VLS = new ArrayList + val List relationVar2TypeDecComply = new ArrayList + val typedefs = new ArrayList + + for (i : 0.. [ + it.name = support.toIDMultiple("Var", i.toString) + ] + relationVar2VLS.add(v) + + val varTypeComply = createVLSFunction => [ + it.constant = support.toIDMultiple("type", (r.parameters.get(i) as ComplexTypeReference).referred.name) + it.terms += createVLSVariable => [ + it.name = support.toIDMultiple("Var", i.toString) + ] + ] + relationVar2TypeDecComply.add(varTypeComply) + + } + + + val comply = createVLSFofFormula => [ + it.name = support.toIDMultiple("compliance", r.name) + it.fofRole = "axiom" + it.fofFormula = createVLSUniversalQuantifier => [ + + for (i : 0.. [ + it.name = relationVar2VLS.get(i).name + ] + it.variables += v + + } + + it.operand = createVLSImplies => [ + it.left = createVLSFunction => [ + it.constant = support.toIDMultiple("rel", r.name) + + for (i : 0.. [ + it.name = relationVar2VLS.get(i).name + ] + it.terms += v + } + + ] + it.right = support.unfoldAnd(relationVar2TypeDecComply) + ] + ] + ] + + // trace.relationDefinition2Predicate.put(r,res) + trace.specification.formulas += comply + } + +} diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend new file mode 100644 index 00000000..ab92b42f --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend @@ -0,0 +1,148 @@ +package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder + +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.QuantifiedExpression +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory +import java.util.ArrayList +import java.util.HashMap +import java.util.List +import java.util.Map +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference +import org.eclipse.emf.common.util.EList +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term + +class Logic2VampireLanguageMapper_Support { + private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE + + // ID Handler + def protected String toIDMultiple(String... ids) { + ids.map[it.split("\\s+").join("_")].join("_") + } + + def protected String toID(String ids) { + ids.split("\\s+").join("_") + } + + // Support Functions + // booleans + // AND and OR + def protected VLSTerm unfoldAnd(List operands) { + if (operands.size == 1) { + return operands.head + } else if (operands.size > 1) { + return createVLSAnd => [ + left = operands.head + right = operands.subList(1, operands.size).unfoldAnd + ] + } else + throw new UnsupportedOperationException('''Logic operator with 0 operands!''') + } + + def protected VLSTerm unfoldOr(List operands) { + +// if(operands.size == 0) {basically return true} + /*else*/ if (operands.size == 1) { + return operands.head + } else if (operands.size > 1) { + return createVLSOr => [ + left = operands.head + right = operands.subList(1, operands.size).unfoldOr + ] + } else + throw new UnsupportedOperationException('''Logic operator with 0 operands!''') // TEMP + } + + def protected VLSTerm unfoldDistinctTerms(Logic2VampireLanguageMapper m, EList operands, + Logic2VampireLanguageMapperTrace trace, Map variables) { + if(operands.size == 1) { return m.transformTerm(operands.head,trace,variables) } + else if(operands.size > 1) { + val notEquals = new ArrayList(operands.size*operands.size/2) + for(i:0..[ + it.left= m.transformTerm(operands.get(i),trace,variables) + it.right = m.transformTerm(operands.get(j),trace,variables) + ] + } + } + return notEquals.unfoldAnd + } + else throw new UnsupportedOperationException('''Logic operator with 0 operands!''') + } + + // Symbolic + // def postprocessResultOfSymbolicReference(TypeReference type, VLSTerm term, Logic2VampireLanguageMapperTrace trace) { +// if(type instanceof BoolTypeReference) { +// return booleanToLogicValue(term ,trace) +// } +// else return term +// } +// def booleanToLogicValue(VLSTerm term, Logic2VampireLanguageMapperTrace trace) { +// throw new UnsupportedOperationException("TODO: auto-generated method stub") +// } + /* + * def protected String toID(List ids) { + * ids.map[it.split("\\s+").join("'")].join("'") + * } + */ + // QUANTIFIERS + VARIABLES + def protected VLSTerm createUniversallyQuantifiedExpression(Logic2VampireLanguageMapper mapper, + QuantifiedExpression expression, Logic2VampireLanguageMapperTrace trace, Map variables) { + val variableMap = expression.quantifiedVariables.toInvertedMap [ v | + createVLSVariable => [it.name = toIDMultiple("Var", v.name)] + ] + + val typedefs = new ArrayList + for (variable : expression.quantifiedVariables) { + val eq = createVLSFunction => [ + it.constant = toIDMultiple("type", (variable.range as ComplexTypeReference).referred.name) + it.terms += createVLSVariable => [ + it.name = toIDMultiple("Var", variable.name) + ] + + ] + typedefs.add(eq) + } + + + createVLSUniversalQuantifier => [ + it.variables += variableMap.values + it.operand = createVLSImplies => [ + it.left = unfoldAnd(typedefs) + it.right = mapper.transformTerm(expression.expression, trace, variables.withAddition(variableMap)) + ] + ] + } + + def protected VLSTerm createExistentiallyQuantifiedExpression(Logic2VampireLanguageMapper mapper, + QuantifiedExpression expression, Logic2VampireLanguageMapperTrace trace, Map variables) { + val variableMap = expression.quantifiedVariables.toInvertedMap [ v | + createVLSVariable => [it.name = toIDMultiple("Var", v.name)] + ] + + val typedefs = new ArrayList + for (variable : expression.quantifiedVariables) { + val eq = createVLSFunction => [ + it.constant = toIDMultiple("type", (variable.range as ComplexTypeReference).referred.name) + it.terms += createVLSVariable => [ + it.name = toIDMultiple("Var", variable.name) + ] + ] + typedefs.add(eq) + } + + typedefs.add(mapper.transformTerm(expression.expression, trace, variables.withAddition(variableMap))) + createVLSExistentialQuantifier => [ + it.variables += variableMap.values + it.operand = unfoldAnd(typedefs) + + ] + } + + def protected withAddition(Map map1, Map map2) { + new HashMap(map1) => [putAll(map2)] + } + +} diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend new file mode 100644 index 00000000..1f071635 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend @@ -0,0 +1,19 @@ +package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder + +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type +import java.util.Collection +import java.util.List +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm + +interface Logic2VampireLanguageMapper_TypeMapper { + def void transformTypes(Collection types, Collection elements, Logic2VampireLanguageMapper mapper, Logic2VampireLanguageMapperTrace trace); + //samples below 2 lines + def List transformTypeReference(Type referred, Logic2VampireLanguageMapper mapper, Logic2VampireLanguageMapperTrace trace) + def VLSTerm getUndefinedSupertype(Logic2VampireLanguageMapperTrace trace) + + def int getUndefinedSupertypeScope(int undefinedScope,Logic2VampireLanguageMapperTrace trace) + def VLSTerm transformReference(DefinedElement referred,Logic2VampireLanguageMapperTrace trace) + + def VampireModelInterpretation_TypeInterpretation getTypeInterpreter() +} \ No newline at end of file diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtend new file mode 100644 index 00000000..a0f0edda --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtend @@ -0,0 +1,21 @@ +package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder + +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm +import java.util.ArrayList +import java.util.HashMap +import java.util.List +import java.util.Map + +class Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes implements Logic2VampireLanguageMapper_TypeMapperTrace{ + +// public var VLSFofFormula objectSuperClass + public val Map type2Predicate = new HashMap; + public val Map definedElement2Declaration = new HashMap //Not Yet Used + public val Map type2PossibleNot = new HashMap + public val Map type2And = new HashMap + +} \ No newline at end of file diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend new file mode 100644 index 00000000..7221f3ff --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend @@ -0,0 +1,158 @@ +package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder + +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.logiclanguage.TypeDefinition +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory +import java.util.ArrayList +import java.util.Collection + +import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* + +class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2VampireLanguageMapper_TypeMapper { + private val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support + private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE + + new() { + LogicproblemPackage.eINSTANCE.class + } + + override transformTypes(Collection types, Collection elements, + Logic2VampireLanguageMapper mapper, Logic2VampireLanguageMapperTrace trace) { + val typeTrace = new Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes + trace.typeMapperTrace = typeTrace + + val VLSVariable variable = createVLSVariable => [it.name = "A"] // did not work + // 1. store predicates for declarations in trace + for (type : types) { + val typePred = createVLSFunction => [ + it.constant = support.toIDMultiple("type", type.name) + it.terms += createVLSVariable => [it.name = variable.name] + ] + typeTrace.type2Predicate.put(type, typePred) + } + + // 2. Map each type definition to fof formula + for (type : types.filter(TypeDefinition)) { + + val res = createVLSFofFormula => [ + it.name = support.toIDMultiple("typeDef", type.name) + // below is temporary solution + it.fofRole = "axiom" + it.fofFormula = createVLSUniversalQuantifier => [ + it.variables += createVLSVariable => [it.name = variable.name] + it.operand = createVLSEquivalent => [ + it.left = createVLSFunction => [ + it.constant = type.lookup(typeTrace.type2Predicate).constant + it.terms += createVLSVariable => [it.name = "A"] + ] + + type.lookup(typeTrace.type2Predicate) + it.right = support.unfoldOr(type.elements.map [ e | + createVLSEquality => [ + it.left = createVLSVariable => [it.name = variable.name] +// it.right = createVLSDoubleQuote => [ +// it.value = "\"" + e.name + "\"" +// ] + it.right = createVLSDoubleQuote => [ + it.value = "\"a" + e.name + "\"" + ] + ] + ]) + ] + ] + + ] + trace.specification.formulas += res + } + // 2.5. Currently allowing duplicate types. Not problematic cuz strings are by def unique + // 3. For each non-abstract type, create an and sequence containing all typedeclaration predicates + // and store in a map +// val List type2PossibleNot = new ArrayList +// val List type2And = new ArrayList + for (type : types.filter[!isIsAbstract]) { + for (type2 : types) { + // possible improvement: check all supertypes and decide if negated or not based on negations/not negations of supertypes + if (type == type2 || dfsSupertypeCheck(type, type2)) { + typeTrace.type2PossibleNot.put(type2, createVLSFunction => [ + it.constant = type2.lookup(typeTrace.type2Predicate).constant + it.terms += createVLSVariable => [it.name = "A"] + ]) + } else { + typeTrace.type2PossibleNot.put(type2, createVLSUnaryNegation => [ + it.operand = createVLSFunction => [ + it.constant = type2.lookup(typeTrace.type2Predicate).constant + it.terms += createVLSVariable => [it.name = "A"] + ] + ]) + } +// typeTrace.type2PossibleNot.put(type2, type2.lookup(typeTrace.type2Predicate)) + } + typeTrace.type2And.put(type, support.unfoldAnd(new ArrayList(typeTrace.type2PossibleNot.values))) +// typeTrace.type2And.put(type, type.lookup(typeTrace.type2Predicate) ) + typeTrace.type2PossibleNot.clear + } + + // 5. create fof function that is an or with all the elements in map + val hierarch = createVLSFofFormula => [ + it.name = "hierarchyHandler" + it.fofRole = "axiom" + it.fofFormula = createVLSUniversalQuantifier => [ + it.variables += createVLSVariable => [it.name = "A"] + it.operand = createVLSEquivalent => [ + it.left = createVLSFunction => [ + it.constant = "Object" + it.terms += createVLSVariable => [ + it.name = "A" + ] + ] + it.right = support.unfoldOr(new ArrayList(typeTrace.type2And.values)) + ] + ] + ] + + trace.specification.formulas += hierarch + } + + def boolean dfsSupertypeCheck(Type type, Type type2) { + // There is surely a better way to do this + if (type.supertypes.isEmpty) + return false + else { + if (type.supertypes.contains(type2)) + return true + else { + for (supertype : type.supertypes) { + if(dfsSupertypeCheck(supertype, type2)) return true + } + } + } + } + + override transformTypeReference(Type referred, Logic2VampireLanguageMapper mapper, + Logic2VampireLanguageMapperTrace trace) { + throw new UnsupportedOperationException("TODO: auto-generated method stub") + } + + override getUndefinedSupertype(Logic2VampireLanguageMapperTrace trace) { + throw new UnsupportedOperationException("TODO: auto-generated method stub") + } + + override getUndefinedSupertypeScope(int undefinedScope, Logic2VampireLanguageMapperTrace trace) { + throw new UnsupportedOperationException("TODO: auto-generated method stub") + } + + override transformReference(DefinedElement referred, Logic2VampireLanguageMapperTrace trace) { + createVLSDoubleQuote => [ + it.value = "\"a" + referred.name + "\"" + ] + } + + override getTypeInterpreter() { + throw new UnsupportedOperationException("TODO: auto-generated method stub") + } + +} diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation_TypeInterpretation.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation_TypeInterpretation.xtend new file mode 100644 index 00000000..66f4fb06 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation_TypeInterpretation.xtend @@ -0,0 +1,5 @@ +package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder + +interface VampireModelInterpretation_TypeInterpretation { + +} \ No newline at end of file diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtend new file mode 100644 index 00000000..863ec783 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtend @@ -0,0 +1,5 @@ +package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder + +class VampireModelInterpretation_TypeInterpretation_FilteredTypes implements VampireModelInterpretation_TypeInterpretation { + //TODO +} \ No newline at end of file diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin new file mode 100644 index 00000000..e8e82269 Binary files /dev/null and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin new file mode 100644 index 00000000..dee2a0a8 Binary files /dev/null and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.gitignore b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.gitignore new file mode 100644 index 00000000..9efd2ac5 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.gitignore @@ -0,0 +1,4 @@ +/.VampireSolver.java._trace +/.TypeMappingTechnique.java._trace +/.VampireBackendSolver.java._trace +/.VampireSolverConfiguration.java._trace diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/TypeMappingTechnique.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/TypeMappingTechnique.java new file mode 100644 index 00000000..8ffba2f1 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/TypeMappingTechnique.java @@ -0,0 +1,6 @@ +package ca.mcgill.ecse.dslreasoner.vampire.reasoner; + +@SuppressWarnings("all") +public enum TypeMappingTechnique { + FilteredTypes; +} diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireBackendSolver.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireBackendSolver.java new file mode 100644 index 00000000..91e9bed0 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireBackendSolver.java @@ -0,0 +1,5 @@ +package ca.mcgill.ecse.dslreasoner.vampire.reasoner; + +@SuppressWarnings("all") +public enum VampireBackendSolver { +} diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.java new file mode 100644 index 00000000..81cae109 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.java @@ -0,0 +1,80 @@ +package ca.mcgill.ecse.dslreasoner.vampire.reasoner; + +import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetup; +import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetupGenerated; +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration; +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel; +import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicModelInterpretation; +import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner; +import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException; +import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration; +import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput; +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem; +import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult; +import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult; +import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace; +import java.io.PrintWriter; +import java.util.List; +import org.eclipse.xtend2.lib.StringConcatenation; +import org.eclipse.xtext.xbase.lib.Exceptions; + +@SuppressWarnings("all") +public class VampireSolver extends LogicReasoner { + public VampireSolver() { + VampireLanguagePackage.eINSTANCE.eClass(); + final VampireLanguageStandaloneSetupGenerated x = new VampireLanguageStandaloneSetupGenerated(); + VampireLanguageStandaloneSetup.doSetup(); + } + + private final Logic2VampireLanguageMapper forwardMapper = new Logic2VampireLanguageMapper(new Logic2VampireLanguageMapper_TypeMapper_FilteredTypes()); + + private final String fileName = "problem.tptp"; + + @Override + public LogicResult solve(final LogicProblem problem, final LogicSolverConfiguration configuration, final ReasonerWorkspace workspace) throws LogicReasonerException { + try { + final VampireSolverConfiguration vampireConfig = this.asConfig(configuration); + final long transformationStart = System.currentTimeMillis(); + final TracedOutput result = this.forwardMapper.transformProblem(problem, vampireConfig); + final VampireModel vampireProblem = result.getOutput(); + final Logic2VampireLanguageMapperTrace forwardTrace = result.getTrace(); + String fileURI = null; + String vampireCode = null; + if (vampireConfig.writeToFile) { + fileURI = workspace.writeModel(vampireProblem, this.fileName).toFileString(); + } else { + vampireCode = workspace.writeModelToString(vampireProblem, this.fileName); + } + long _currentTimeMillis = System.currentTimeMillis(); + final long transformationTime = (_currentTimeMillis - transformationStart); + final PrintWriter out = new PrintWriter("output/files/vampireCode.tptp"); + out.println(vampireCode); + out.close(); + return null; + } catch (Throwable _e) { + throw Exceptions.sneakyThrow(_e); + } + } + + public VampireSolverConfiguration asConfig(final LogicSolverConfiguration configuration) { + if ((configuration instanceof VampireSolverConfiguration)) { + return ((VampireSolverConfiguration)configuration); + } else { + StringConcatenation _builder = new StringConcatenation(); + _builder.append("The configuration have to be an "); + String _simpleName = VampireSolverConfiguration.class.getSimpleName(); + _builder.append(_simpleName); + _builder.append("!"); + throw new IllegalArgumentException(_builder.toString()); + } + } + + @Override + public List getInterpretations(final ModelResult modelResult) { + return null; + } +} diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolverConfiguration.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolverConfiguration.java new file mode 100644 index 00000000..d392016e --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolverConfiguration.java @@ -0,0 +1,10 @@ +package ca.mcgill.ecse.dslreasoner.vampire.reasoner; + +import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration; + +@SuppressWarnings("all") +public class VampireSolverConfiguration extends LogicSolverConfiguration { + public int symmetry = 0; + + public boolean writeToFile = false; +} diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin new file mode 100644 index 00000000..10edee94 Binary files /dev/null and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin new file mode 100644 index 00000000..50c1d625 Binary files /dev/null and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin new file mode 100644 index 00000000..f331beac Binary files /dev/null and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin new file mode 100644 index 00000000..e929e637 Binary files /dev/null and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin new file mode 100644 index 00000000..cc7aea7c Binary files /dev/null and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin new file mode 100644 index 00000000..1b6cf5d1 Binary files /dev/null and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtendbin new file mode 100644 index 00000000..7a4d5bc7 Binary files /dev/null and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtendbin new file mode 100644 index 00000000..7b6b2f9a Binary files /dev/null and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin new file mode 100644 index 00000000..f8b3c54e Binary files /dev/null and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin new file mode 100644 index 00000000..52b870a3 Binary files /dev/null and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.gitignore b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.gitignore new file mode 100644 index 00000000..d27ff186 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.gitignore @@ -0,0 +1,11 @@ +/.Logic2VampireLanguageMapper_ConstantMapper.java._trace +/.Logic2VampireLanguageMapper.java._trace +/.Logic2VampireLanguageMapperTrace.java._trace +/.Logic2VampireLanguageMapper_TypeMapperTrace.java._trace +/.VampireModelInterpretation_TypeInterpretation.java._trace +/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.java._trace +/.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.java._trace +/.Logic2VampireLanguageMapper_TypeMapper.java._trace +/.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.java._trace +/.Logic2VampireLanguageMapper_Support.java._trace +/.Logic2VampireLanguageMapper_RelationMapper.java._trace diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java new file mode 100644 index 00000000..390a6b10 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java @@ -0,0 +1,442 @@ +package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; + +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration; +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_ConstantMapper; +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_RelationMapper; +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapper; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSComment; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSInt; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSReal; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUnaryNegation; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel; +import com.google.common.collect.Iterables; +import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput; +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.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.FunctionDeclaration; +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDefinition; +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.Not; +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Or; +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealLiteral; +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.SymbolicDeclaration; +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.TypeReference; +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.util.CollectionsUtil; +import java.util.Arrays; +import java.util.Collections; +import java.util.HashMap; +import java.util.List; +import java.util.Map; +import java.util.function.Consumer; +import org.eclipse.emf.common.util.EList; +import org.eclipse.xtend.lib.annotations.AccessorType; +import org.eclipse.xtend.lib.annotations.Accessors; +import org.eclipse.xtext.xbase.lib.Extension; +import org.eclipse.xtext.xbase.lib.Functions.Function1; +import org.eclipse.xtext.xbase.lib.IterableExtensions; +import org.eclipse.xtext.xbase.lib.ListExtensions; +import org.eclipse.xtext.xbase.lib.ObjectExtensions; +import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; +import org.eclipse.xtext.xbase.lib.Pure; + +@SuppressWarnings("all") +public class Logic2VampireLanguageMapper { + @Extension + private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE; + + private final Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support(); + + @Accessors(AccessorType.PUBLIC_GETTER) + private final Logic2VampireLanguageMapper_ConstantMapper constantMapper = new Logic2VampireLanguageMapper_ConstantMapper(this); + + @Accessors(AccessorType.PUBLIC_GETTER) + private final Logic2VampireLanguageMapper_RelationMapper relationMapper = new Logic2VampireLanguageMapper_RelationMapper(this); + + @Accessors(AccessorType.PUBLIC_GETTER) + private final Logic2VampireLanguageMapper_TypeMapper typeMapper; + + public Logic2VampireLanguageMapper(final Logic2VampireLanguageMapper_TypeMapper typeMapper) { + this.typeMapper = typeMapper; + } + + public TracedOutput transformProblem(final LogicProblem problem, final VampireSolverConfiguration configuration) { + VLSComment _createVLSComment = this.factory.createVLSComment(); + final Procedure1 _function = (VLSComment it) -> { + it.setComment("%This is an initial Test Comment \r"); + }; + final VLSComment initialComment = ObjectExtensions.operator_doubleArrow(_createVLSComment, _function); + VampireModel _createVampireModel = this.factory.createVampireModel(); + final Procedure1 _function_1 = (VampireModel it) -> { + EList _comments = it.getComments(); + _comments.add(initialComment); + }; + final VampireModel specification = ObjectExtensions.operator_doubleArrow(_createVampireModel, _function_1); + Logic2VampireLanguageMapperTrace _logic2VampireLanguageMapperTrace = new Logic2VampireLanguageMapperTrace(); + final Procedure1 _function_2 = (Logic2VampireLanguageMapperTrace it) -> { + it.specification = specification; + }; + final Logic2VampireLanguageMapperTrace trace = ObjectExtensions.operator_doubleArrow(_logic2VampireLanguageMapperTrace, _function_2); + boolean _isEmpty = problem.getTypes().isEmpty(); + boolean _not = (!_isEmpty); + if (_not) { + this.typeMapper.transformTypes(problem.getTypes(), problem.getElements(), this, trace); + } + trace.constantDefinitions = this.collectConstantDefinitions(problem); + trace.relationDefinitions = this.collectRelationDefinitions(problem); + final Consumer _function_3 = (Relation it) -> { + this.relationMapper.transformRelation(it, trace); + }; + problem.getRelations().forEach(_function_3); + final Consumer _function_4 = (ConstantDefinition it) -> { + this.constantMapper.transformConstantDefinitionSpecification(it, trace); + }; + Iterables.filter(problem.getConstants(), ConstantDefinition.class).forEach(_function_4); + EList _assertions = problem.getAssertions(); + for (final Assertion assertion : _assertions) { + this.transformAssertion(assertion, trace); + } + return new TracedOutput(specification, trace); + } + + protected VLSTerm _transformTypeReference(final BoolTypeReference boolTypeReference, final Logic2VampireLanguageMapperTrace trace) { + return null; + } + + private HashMap collectConstantDefinitions(final LogicProblem problem) { + final HashMap res = new HashMap(); + final Function1 _function = (ConstantDefinition it) -> { + ConstantDeclaration _defines = it.getDefines(); + return Boolean.valueOf((_defines != null)); + }; + final Consumer _function_1 = (ConstantDefinition it) -> { + res.put(it.getDefines(), it); + }; + IterableExtensions.filter(Iterables.filter(problem.getConstants(), ConstantDefinition.class), _function).forEach(_function_1); + return res; + } + + private HashMap collectRelationDefinitions(final LogicProblem problem) { + final HashMap res = new HashMap(); + final Function1 _function = (RelationDefinition it) -> { + RelationDeclaration _defines = it.getDefines(); + return Boolean.valueOf((_defines != null)); + }; + final Consumer _function_1 = (RelationDefinition it) -> { + res.put(it.getDefines(), it); + }; + IterableExtensions.filter(Iterables.filter(problem.getRelations(), RelationDefinition.class), _function).forEach(_function_1); + return res; + } + + protected boolean transformAssertion(final Assertion assertion, final Logic2VampireLanguageMapperTrace trace) { + boolean _xblockexpression = false; + { + VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); + final Procedure1 _function = (VLSFofFormula it) -> { + it.setName(this.support.toID(assertion.getName())); + it.setFofRole("axiom"); + it.setFofFormula(this.transformTerm(assertion.getValue(), trace, Collections.EMPTY_MAP)); + }; + final VLSFofFormula res = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula, _function); + EList _formulas = trace.specification.getFormulas(); + _xblockexpression = _formulas.add(res); + } + return _xblockexpression; + } + + protected VLSTerm _transformTerm(final BoolLiteral literal, final Logic2VampireLanguageMapperTrace trace, final Map variables) { + VLSTerm _xifexpression = null; + boolean _isValue = literal.isValue(); + boolean _equals = (_isValue == true); + if (_equals) { + _xifexpression = this.factory.createVLSTrue(); + } else { + _xifexpression = this.factory.createVLSFalse(); + } + return _xifexpression; + } + + protected VLSTerm _transformTerm(final IntLiteral literal, final Logic2VampireLanguageMapperTrace trace, final Map variables) { + VLSInt _createVLSInt = this.factory.createVLSInt(); + final Procedure1 _function = (VLSInt it) -> { + it.setValue(Integer.valueOf(literal.getValue()).toString()); + }; + return ObjectExtensions.operator_doubleArrow(_createVLSInt, _function); + } + + protected VLSTerm _transformTerm(final RealLiteral literal, final Logic2VampireLanguageMapperTrace trace, final Map variables) { + VLSReal _createVLSReal = this.factory.createVLSReal(); + final Procedure1 _function = (VLSReal it) -> { + it.setValue(literal.getValue().toString()); + }; + return ObjectExtensions.operator_doubleArrow(_createVLSReal, _function); + } + + protected VLSTerm _transformTerm(final Not not, final Logic2VampireLanguageMapperTrace trace, final Map variables) { + VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); + final Procedure1 _function = (VLSUnaryNegation it) -> { + it.setOperand(this.transformTerm(not.getOperand(), trace, variables)); + }; + return ObjectExtensions.operator_doubleArrow(_createVLSUnaryNegation, _function); + } + + protected VLSTerm _transformTerm(final And and, final Logic2VampireLanguageMapperTrace trace, final Map variables) { + final Function1 _function = (Term it) -> { + return this.transformTerm(it, trace, variables); + }; + return this.support.unfoldAnd(ListExtensions.map(and.getOperands(), _function)); + } + + protected VLSTerm _transformTerm(final Or or, final Logic2VampireLanguageMapperTrace trace, final Map variables) { + final Function1 _function = (Term it) -> { + return this.transformTerm(it, trace, variables); + }; + return this.support.unfoldOr(ListExtensions.map(or.getOperands(), _function)); + } + + protected VLSTerm _transformTerm(final Impl impl, final Logic2VampireLanguageMapperTrace trace, final Map variables) { + VLSImplies _createVLSImplies = this.factory.createVLSImplies(); + final Procedure1 _function = (VLSImplies it) -> { + it.setLeft(this.transformTerm(impl.getLeftOperand(), trace, variables)); + it.setRight(this.transformTerm(impl.getRightOperand(), trace, variables)); + }; + return ObjectExtensions.operator_doubleArrow(_createVLSImplies, _function); + } + + protected VLSTerm _transformTerm(final Iff iff, final Logic2VampireLanguageMapperTrace trace, final Map variables) { + VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); + final Procedure1 _function = (VLSEquivalent it) -> { + it.setLeft(this.transformTerm(iff.getLeftOperand(), trace, variables)); + it.setRight(this.transformTerm(iff.getRightOperand(), trace, variables)); + }; + return ObjectExtensions.operator_doubleArrow(_createVLSEquivalent, _function); + } + + protected VLSTerm _transformTerm(final Equals equals, final Logic2VampireLanguageMapperTrace trace, final Map variables) { + VLSEquality _createVLSEquality = this.factory.createVLSEquality(); + final Procedure1 _function = (VLSEquality it) -> { + it.setLeft(this.transformTerm(equals.getLeftOperand(), trace, variables)); + it.setRight(this.transformTerm(equals.getRightOperand(), trace, variables)); + }; + return ObjectExtensions.operator_doubleArrow(_createVLSEquality, _function); + } + + protected VLSTerm _transformTerm(final Distinct distinct, final Logic2VampireLanguageMapperTrace trace, final Map variables) { + return this.support.unfoldDistinctTerms(this, distinct.getOperands(), trace, variables); + } + + protected VLSTerm _transformTerm(final Forall forall, final Logic2VampireLanguageMapperTrace trace, final Map variables) { + return this.support.createUniversallyQuantifiedExpression(this, forall, trace, variables); + } + + protected VLSTerm _transformTerm(final Exists exists, final Logic2VampireLanguageMapperTrace trace, final Map variables) { + return this.support.createExistentiallyQuantifiedExpression(this, exists, trace, variables); + } + + protected VLSTerm _transformTerm(final InstanceOf instanceOf, final Logic2VampireLanguageMapperTrace trace, final Map variables) { + VLSFunction _createVLSFunction = this.factory.createVLSFunction(); + final Procedure1 _function = (VLSFunction it) -> { + TypeReference _range = instanceOf.getRange(); + it.setConstant(this.support.toIDMultiple("type", ((ComplexTypeReference) _range).getReferred().getName())); + EList _terms = it.getTerms(); + VLSTerm _transformTerm = this.transformTerm(instanceOf.getValue(), trace, variables); + _terms.add(_transformTerm); + }; + return ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function); + } + + protected VLSTerm _transformTerm(final SymbolicValue symbolicValue, final Logic2VampireLanguageMapperTrace trace, final Map variables) { + return this.transformSymbolicReference(symbolicValue.getSymbolicReference(), symbolicValue.getParameterSubstitutions(), trace, variables); + } + + protected VLSTerm _transformSymbolicReference(final DefinedElement referred, final List parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map variables) { + return this.typeMapper.transformReference(referred, trace); + } + + protected VLSTerm _transformSymbolicReference(final ConstantDeclaration constant, final List parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map variables) { + VLSConstant _createVLSConstant = this.factory.createVLSConstant(); + final Procedure1 _function = (VLSConstant it) -> { + it.setName(this.support.toID(constant.getName())); + }; + final VLSConstant res = ObjectExtensions.operator_doubleArrow(_createVLSConstant, _function); + return res; + } + + protected VLSTerm _transformSymbolicReference(final ConstantDefinition constant, final List parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map variables) { + return null; + } + + protected VLSTerm _transformSymbolicReference(final Variable variable, final List parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map variables) { + VLSVariable _createVLSVariable = this.factory.createVLSVariable(); + final Procedure1 _function = (VLSVariable it) -> { + it.setName(this.support.toID(CollectionsUtil.lookup(variable, variables).getName())); + }; + final VLSVariable res = ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function); + return res; + } + + protected VLSTerm _transformSymbolicReference(final FunctionDeclaration function, final List parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map variables) { + return null; + } + + protected VLSTerm _transformSymbolicReference(final FunctionDefinition function, final List parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map variables) { + return null; + } + + /** + * def dispatch protected VLSTerm transformSymbolicReference(Relation relation, + * List parameterSubstitutions, Logic2VampireLanguageMapperTrace trace, + * Map variables) { + * if (trace.relationDefinitions.containsKey(relation)) { + * this.transformSymbolicReference(relation.lookup(trace.relationDefinitions), + * parameterSubstitutions, trace, variables) + * } + * else { + * // if (relationMapper.transformToHostedField(relation, trace)) { + * // val VLSRelation = relation.lookup(trace.relationDeclaration2Field) + * // // R(a,b) => + * // // b in a.R + * // return createVLSSubset => [ + * // it.leftOperand = parameterSubstitutions.get(1).transformTerm(trace, variables) + * // it.rightOperand = createVLSJoin => [ + * // it.leftOperand = parameterSubstitutions.get(0).transformTerm(trace, variables) + * // it.rightOperand = createVLSReference => [it.referred = VLSRelation] + * // ] + * // ] + * // } else { + * // val target = createVLSJoin => [ + * // leftOperand = createVLSReference => [referred = trace.logicLanguage] + * // rightOperand = createVLSReference => [ + * // referred = relation.lookup(trace.relationDeclaration2Global) + * // ] + * // ] + * // val source = support.unfoldTermDirectProduct(this, parameterSubstitutions, trace, variables) + * // + * // return createVLSSubset => [ + * // leftOperand = source + * // rightOperand = target + * // ] + * // } + * } + * } + */ + protected VLSTerm _transformSymbolicReference(final Relation relation, final List parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map variables) { + VLSFunction _createVLSFunction = this.factory.createVLSFunction(); + final Procedure1 _function = (VLSFunction it) -> { + it.setConstant(this.support.toIDMultiple("rel", relation.getName())); + EList _terms = it.getTerms(); + final Function1 _function_1 = (Term p) -> { + return this.transformTerm(p, trace, variables); + }; + List _map = ListExtensions.map(parameterSubstitutions, _function_1); + Iterables.addAll(_terms, _map); + }; + return ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function); + } + + protected VLSTerm transformTypeReference(final BoolTypeReference boolTypeReference, final Logic2VampireLanguageMapperTrace trace) { + return _transformTypeReference(boolTypeReference, trace); + } + + protected VLSTerm transformTerm(final Term and, final Logic2VampireLanguageMapperTrace trace, final Map variables) { + if (and instanceof And) { + return _transformTerm((And)and, trace, variables); + } else if (and instanceof BoolLiteral) { + return _transformTerm((BoolLiteral)and, trace, variables); + } else if (and instanceof Distinct) { + return _transformTerm((Distinct)and, trace, variables); + } else if (and instanceof Equals) { + return _transformTerm((Equals)and, trace, variables); + } else if (and instanceof Exists) { + return _transformTerm((Exists)and, trace, variables); + } else if (and instanceof Forall) { + return _transformTerm((Forall)and, trace, variables); + } else if (and instanceof Iff) { + return _transformTerm((Iff)and, trace, variables); + } else if (and instanceof Impl) { + return _transformTerm((Impl)and, trace, variables); + } else if (and instanceof IntLiteral) { + return _transformTerm((IntLiteral)and, trace, variables); + } else if (and instanceof Not) { + return _transformTerm((Not)and, trace, variables); + } else if (and instanceof Or) { + return _transformTerm((Or)and, trace, variables); + } else if (and instanceof RealLiteral) { + return _transformTerm((RealLiteral)and, trace, variables); + } else if (and instanceof InstanceOf) { + return _transformTerm((InstanceOf)and, trace, variables); + } else if (and instanceof SymbolicValue) { + return _transformTerm((SymbolicValue)and, trace, variables); + } else { + throw new IllegalArgumentException("Unhandled parameter types: " + + Arrays.asList(and, trace, variables).toString()); + } + } + + protected VLSTerm transformSymbolicReference(final SymbolicDeclaration constant, final List parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map variables) { + if (constant instanceof ConstantDeclaration) { + return _transformSymbolicReference((ConstantDeclaration)constant, parameterSubstitutions, trace, variables); + } else if (constant instanceof ConstantDefinition) { + return _transformSymbolicReference((ConstantDefinition)constant, parameterSubstitutions, trace, variables); + } else if (constant instanceof FunctionDeclaration) { + return _transformSymbolicReference((FunctionDeclaration)constant, parameterSubstitutions, trace, variables); + } else if (constant instanceof FunctionDefinition) { + return _transformSymbolicReference((FunctionDefinition)constant, parameterSubstitutions, trace, variables); + } else if (constant instanceof DefinedElement) { + return _transformSymbolicReference((DefinedElement)constant, parameterSubstitutions, trace, variables); + } else if (constant instanceof Relation) { + return _transformSymbolicReference((Relation)constant, parameterSubstitutions, trace, variables); + } else if (constant instanceof Variable) { + return _transformSymbolicReference((Variable)constant, parameterSubstitutions, trace, variables); + } else { + throw new IllegalArgumentException("Unhandled parameter types: " + + Arrays.asList(constant, parameterSubstitutions, trace, variables).toString()); + } + } + + @Pure + public Logic2VampireLanguageMapper_ConstantMapper getConstantMapper() { + return this.constantMapper; + } + + @Pure + public Logic2VampireLanguageMapper_RelationMapper getRelationMapper() { + return this.relationMapper; + } + + @Pure + public Logic2VampireLanguageMapper_TypeMapper getTypeMapper() { + return this.typeMapper; + } +} diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java new file mode 100644 index 00000000..855815f8 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java @@ -0,0 +1,34 @@ +package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; + +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapperTrace; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel; +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.RelationDeclaration; +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition; +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable; +import java.util.HashMap; +import java.util.Map; + +@SuppressWarnings("all") +public class Logic2VampireLanguageMapperTrace { + public VampireModel specification; + + public VLSFofFormula logicLanguageBody; + + public VLSTerm formula; + + public Logic2VampireLanguageMapper_TypeMapperTrace typeMapperTrace; + + public Map constantDefinitions; + + public Map relationDefinitions; + + public final Map relationVar2VLS = new HashMap(); + + public final Map relationVar2TypeDec = new HashMap(); +} diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ConstantMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ConstantMapper.java new file mode 100644 index 00000000..e5f42e73 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ConstantMapper.java @@ -0,0 +1,34 @@ +package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; + +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDefinition; +import org.eclipse.xtext.xbase.lib.Extension; + +@SuppressWarnings("all") +public class Logic2VampireLanguageMapper_ConstantMapper { + @Extension + private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE; + + private final Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support(); + + private final Logic2VampireLanguageMapper base; + + public Logic2VampireLanguageMapper_ConstantMapper(final Logic2VampireLanguageMapper base) { + this.base = base; + } + + protected Object _transformConstant(final ConstantDefinition constant, final Logic2VampireLanguageMapperTrace trace) { + return null; + } + + protected Object transformConstantDefinitionSpecification(final ConstantDefinition constant, final Logic2VampireLanguageMapperTrace trace) { + return null; + } + + protected Object transformConstant(final ConstantDefinition constant, final Logic2VampireLanguageMapperTrace trace) { + return _transformConstant(constant, trace); + } +} diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java new file mode 100644 index 00000000..561402a7 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java @@ -0,0 +1,296 @@ +package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; + +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference; +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.TypeReference; +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable; +import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; +import java.util.ArrayList; +import java.util.Arrays; +import java.util.Collection; +import java.util.HashMap; +import java.util.List; +import java.util.Map; +import org.eclipse.emf.common.util.EList; +import org.eclipse.xtext.xbase.lib.Conversions; +import org.eclipse.xtext.xbase.lib.ExclusiveRange; +import org.eclipse.xtext.xbase.lib.Extension; +import org.eclipse.xtext.xbase.lib.ObjectExtensions; +import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; + +@SuppressWarnings("all") +public class Logic2VampireLanguageMapper_RelationMapper { + @Extension + private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE; + + private final Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support(); + + private final Logic2VampireLanguageMapper base; + + public Logic2VampireLanguageMapper_RelationMapper(final Logic2VampireLanguageMapper base) { + this.base = base; + } + + public void _transformRelation(final RelationDefinition r, final Logic2VampireLanguageMapperTrace trace) { + final Map relationVar2VLS = new HashMap(); + final Map relationVar2TypeDecComply = new HashMap(); + final Map relationVar2TypeDecRes = new HashMap(); + final ArrayList typedefs = new ArrayList(); + EList _variables = r.getVariables(); + for (final Variable variable : _variables) { + { + VLSVariable _createVLSVariable = this.factory.createVLSVariable(); + final Procedure1 _function = (VLSVariable it) -> { + it.setName(this.support.toIDMultiple("Var", variable.getName())); + }; + final VLSVariable v = ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function); + relationVar2VLS.put(variable, v); + VLSFunction _createVLSFunction = this.factory.createVLSFunction(); + final Procedure1 _function_1 = (VLSFunction it) -> { + TypeReference _range = variable.getRange(); + it.setConstant(this.support.toIDMultiple("type", ((ComplexTypeReference) _range).getReferred().getName())); + EList _terms = it.getTerms(); + VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable(); + final Procedure1 _function_2 = (VLSVariable it_1) -> { + it_1.setName(this.support.toIDMultiple("Var", variable.getName())); + }; + VLSVariable _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSVariable_1, _function_2); + _terms.add(_doubleArrow); + }; + final VLSFunction varTypeComply = ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function_1); + relationVar2TypeDecComply.put(variable, varTypeComply); + VLSFunction _createVLSFunction_1 = this.factory.createVLSFunction(); + final Procedure1 _function_2 = (VLSFunction it) -> { + TypeReference _range = variable.getRange(); + it.setConstant(this.support.toIDMultiple("type", ((ComplexTypeReference) _range).getReferred().getName())); + EList _terms = it.getTerms(); + VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable(); + final Procedure1 _function_3 = (VLSVariable it_1) -> { + it_1.setName(this.support.toIDMultiple("Var", variable.getName())); + }; + VLSVariable _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSVariable_1, _function_3); + _terms.add(_doubleArrow); + }; + final VLSFunction varTypeRes = ObjectExtensions.operator_doubleArrow(_createVLSFunction_1, _function_2); + relationVar2TypeDecRes.put(variable, varTypeRes); + } + } + VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); + final Procedure1 _function = (VLSFofFormula it) -> { + it.setName(this.support.toIDMultiple("compliance", r.getName())); + it.setFofRole("axiom"); + VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); + final Procedure1 _function_1 = (VLSUniversalQuantifier it_1) -> { + EList _variables_1 = r.getVariables(); + for (final Variable variable_1 : _variables_1) { + { + VLSVariable _createVLSVariable = this.factory.createVLSVariable(); + final Procedure1 _function_2 = (VLSVariable it_2) -> { + it_2.setName(CollectionsUtil.lookup(variable_1, relationVar2VLS).getName()); + }; + final VLSVariable v = ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function_2); + EList _variables_2 = it_1.getVariables(); + _variables_2.add(v); + } + } + VLSImplies _createVLSImplies = this.factory.createVLSImplies(); + final Procedure1 _function_2 = (VLSImplies it_2) -> { + VLSFunction _createVLSFunction = this.factory.createVLSFunction(); + final Procedure1 _function_3 = (VLSFunction it_3) -> { + it_3.setConstant(this.support.toIDMultiple("rel", r.getName())); + EList _variables_2 = r.getVariables(); + for (final Variable variable_2 : _variables_2) { + { + VLSVariable _createVLSVariable = this.factory.createVLSVariable(); + final Procedure1 _function_4 = (VLSVariable it_4) -> { + it_4.setName(CollectionsUtil.lookup(variable_2, relationVar2VLS).getName()); + }; + final VLSVariable v = ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function_4); + EList _terms = it_3.getTerms(); + _terms.add(v); + } + } + }; + VLSFunction _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function_3); + it_2.setLeft(_doubleArrow); + Collection _values = relationVar2TypeDecComply.values(); + ArrayList _arrayList = new ArrayList(_values); + it_2.setRight(this.support.unfoldAnd(_arrayList)); + }; + VLSImplies _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSImplies, _function_2); + it_1.setOperand(_doubleArrow); + }; + VLSUniversalQuantifier _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSUniversalQuantifier, _function_1); + it.setFofFormula(_doubleArrow); + }; + final VLSFofFormula comply = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula, _function); + VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); + final Procedure1 _function_1 = (VLSFofFormula it) -> { + it.setName(this.support.toIDMultiple("relation", r.getName())); + it.setFofRole("axiom"); + VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); + final Procedure1 _function_2 = (VLSUniversalQuantifier it_1) -> { + EList _variables_1 = r.getVariables(); + for (final Variable variable_1 : _variables_1) { + { + VLSVariable _createVLSVariable = this.factory.createVLSVariable(); + final Procedure1 _function_3 = (VLSVariable it_2) -> { + it_2.setName(CollectionsUtil.lookup(variable_1, relationVar2VLS).getName()); + }; + final VLSVariable v = ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function_3); + EList _variables_2 = it_1.getVariables(); + _variables_2.add(v); + } + } + VLSImplies _createVLSImplies = this.factory.createVLSImplies(); + final Procedure1 _function_3 = (VLSImplies it_2) -> { + Collection _values = relationVar2TypeDecRes.values(); + ArrayList _arrayList = new ArrayList(_values); + it_2.setLeft(this.support.unfoldAnd(_arrayList)); + VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); + final Procedure1 _function_4 = (VLSEquivalent it_3) -> { + VLSFunction _createVLSFunction = this.factory.createVLSFunction(); + final Procedure1 _function_5 = (VLSFunction it_4) -> { + it_4.setConstant(this.support.toIDMultiple("rel", r.getName())); + EList _variables_2 = r.getVariables(); + for (final Variable variable_2 : _variables_2) { + { + VLSVariable _createVLSVariable = this.factory.createVLSVariable(); + final Procedure1 _function_6 = (VLSVariable it_5) -> { + it_5.setName(CollectionsUtil.lookup(variable_2, relationVar2VLS).getName()); + }; + final VLSVariable v = ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function_6); + EList _terms = it_4.getTerms(); + _terms.add(v); + } + } + }; + VLSFunction _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function_5); + it_3.setLeft(_doubleArrow); + it_3.setRight(this.base.transformTerm(r.getValue(), trace, relationVar2VLS)); + }; + VLSEquivalent _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSEquivalent, _function_4); + it_2.setRight(_doubleArrow); + }; + VLSImplies _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSImplies, _function_3); + it_1.setOperand(_doubleArrow); + }; + VLSUniversalQuantifier _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSUniversalQuantifier, _function_2); + it.setFofFormula(_doubleArrow); + }; + final VLSFofFormula res = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula_1, _function_1); + EList _formulas = trace.specification.getFormulas(); + _formulas.add(comply); + EList _formulas_1 = trace.specification.getFormulas(); + _formulas_1.add(res); + } + + public void _transformRelation(final RelationDeclaration r, final Logic2VampireLanguageMapperTrace trace) { + final List relationVar2VLS = new ArrayList(); + final List relationVar2TypeDecComply = new ArrayList(); + final ArrayList typedefs = new ArrayList(); + int _length = ((Object[])Conversions.unwrapArray(r.getParameters(), Object.class)).length; + ExclusiveRange _doubleDotLessThan = new ExclusiveRange(0, _length, true); + for (final Integer i : _doubleDotLessThan) { + { + VLSVariable _createVLSVariable = this.factory.createVLSVariable(); + final Procedure1 _function = (VLSVariable it) -> { + it.setName(this.support.toIDMultiple("Var", i.toString())); + }; + final VLSVariable v = ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function); + relationVar2VLS.add(v); + VLSFunction _createVLSFunction = this.factory.createVLSFunction(); + final Procedure1 _function_1 = (VLSFunction it) -> { + TypeReference _get = r.getParameters().get((i).intValue()); + it.setConstant(this.support.toIDMultiple("type", ((ComplexTypeReference) _get).getReferred().getName())); + EList _terms = it.getTerms(); + VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable(); + final Procedure1 _function_2 = (VLSVariable it_1) -> { + it_1.setName(this.support.toIDMultiple("Var", i.toString())); + }; + VLSVariable _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSVariable_1, _function_2); + _terms.add(_doubleArrow); + }; + final VLSFunction varTypeComply = ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function_1); + relationVar2TypeDecComply.add(varTypeComply); + } + } + VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); + final Procedure1 _function = (VLSFofFormula it) -> { + it.setName(this.support.toIDMultiple("compliance", r.getName())); + it.setFofRole("axiom"); + VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); + final Procedure1 _function_1 = (VLSUniversalQuantifier it_1) -> { + int _length_1 = ((Object[])Conversions.unwrapArray(r.getParameters(), Object.class)).length; + ExclusiveRange _doubleDotLessThan_1 = new ExclusiveRange(0, _length_1, true); + for (final Integer i_1 : _doubleDotLessThan_1) { + { + VLSVariable _createVLSVariable = this.factory.createVLSVariable(); + final Procedure1 _function_2 = (VLSVariable it_2) -> { + it_2.setName(relationVar2VLS.get((i_1).intValue()).getName()); + }; + final VLSVariable v = ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function_2); + EList _variables = it_1.getVariables(); + _variables.add(v); + } + } + VLSImplies _createVLSImplies = this.factory.createVLSImplies(); + final Procedure1 _function_2 = (VLSImplies it_2) -> { + VLSFunction _createVLSFunction = this.factory.createVLSFunction(); + final Procedure1 _function_3 = (VLSFunction it_3) -> { + it_3.setConstant(this.support.toIDMultiple("rel", r.getName())); + int _length_2 = ((Object[])Conversions.unwrapArray(r.getParameters(), Object.class)).length; + ExclusiveRange _doubleDotLessThan_2 = new ExclusiveRange(0, _length_2, true); + for (final Integer i_2 : _doubleDotLessThan_2) { + { + VLSVariable _createVLSVariable = this.factory.createVLSVariable(); + final Procedure1 _function_4 = (VLSVariable it_4) -> { + it_4.setName(relationVar2VLS.get((i_2).intValue()).getName()); + }; + final VLSVariable v = ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function_4); + EList _terms = it_3.getTerms(); + _terms.add(v); + } + } + }; + VLSFunction _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function_3); + it_2.setLeft(_doubleArrow); + it_2.setRight(this.support.unfoldAnd(relationVar2TypeDecComply)); + }; + VLSImplies _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSImplies, _function_2); + it_1.setOperand(_doubleArrow); + }; + VLSUniversalQuantifier _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSUniversalQuantifier, _function_1); + it.setFofFormula(_doubleArrow); + }; + final VLSFofFormula comply = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula, _function); + EList _formulas = trace.specification.getFormulas(); + _formulas.add(comply); + } + + public void transformRelation(final Relation r, final Logic2VampireLanguageMapperTrace trace) { + if (r instanceof RelationDeclaration) { + _transformRelation((RelationDeclaration)r, trace); + return; + } else if (r instanceof RelationDefinition) { + _transformRelation((RelationDefinition)r, trace); + return; + } else { + throw new IllegalArgumentException("Unhandled parameter types: " + + Arrays.asList(r, trace).toString()); + } + } +} diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java new file mode 100644 index 00000000..e1be7df5 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java @@ -0,0 +1,242 @@ +package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; + +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSAnd; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSExistentialQuantifier; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSInequality; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSOr; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; +import com.google.common.collect.Iterables; +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference; +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.QuantifiedExpression; +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term; +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference; +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable; +import java.util.ArrayList; +import java.util.Collection; +import java.util.HashMap; +import java.util.List; +import java.util.Map; +import org.eclipse.emf.common.util.EList; +import org.eclipse.xtend2.lib.StringConcatenation; +import org.eclipse.xtext.xbase.lib.Conversions; +import org.eclipse.xtext.xbase.lib.ExclusiveRange; +import org.eclipse.xtext.xbase.lib.Extension; +import org.eclipse.xtext.xbase.lib.Functions.Function1; +import org.eclipse.xtext.xbase.lib.IterableExtensions; +import org.eclipse.xtext.xbase.lib.ListExtensions; +import org.eclipse.xtext.xbase.lib.ObjectExtensions; +import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; + +@SuppressWarnings("all") +public class Logic2VampireLanguageMapper_Support { + @Extension + private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE; + + protected String toIDMultiple(final String... ids) { + final Function1 _function = (String it) -> { + return IterableExtensions.join(((Iterable)Conversions.doWrapArray(it.split("\\s+"))), "_"); + }; + return IterableExtensions.join(ListExtensions.map(((List)Conversions.doWrapArray(ids)), _function), "_"); + } + + protected String toID(final String ids) { + return IterableExtensions.join(((Iterable)Conversions.doWrapArray(ids.split("\\s+"))), "_"); + } + + protected VLSTerm unfoldAnd(final List operands) { + int _size = operands.size(); + boolean _equals = (_size == 1); + if (_equals) { + return IterableExtensions.head(operands); + } else { + int _size_1 = operands.size(); + boolean _greaterThan = (_size_1 > 1); + if (_greaterThan) { + VLSAnd _createVLSAnd = this.factory.createVLSAnd(); + final Procedure1 _function = (VLSAnd it) -> { + it.setLeft(IterableExtensions.head(operands)); + it.setRight(this.unfoldAnd(operands.subList(1, operands.size()))); + }; + return ObjectExtensions.operator_doubleArrow(_createVLSAnd, _function); + } else { + StringConcatenation _builder = new StringConcatenation(); + _builder.append("Logic operator with 0 operands!"); + throw new UnsupportedOperationException(_builder.toString()); + } + } + } + + protected VLSTerm unfoldOr(final List operands) { + int _size = operands.size(); + boolean _equals = (_size == 1); + if (_equals) { + return IterableExtensions.head(operands); + } else { + int _size_1 = operands.size(); + boolean _greaterThan = (_size_1 > 1); + if (_greaterThan) { + VLSOr _createVLSOr = this.factory.createVLSOr(); + final Procedure1 _function = (VLSOr it) -> { + it.setLeft(IterableExtensions.head(operands)); + it.setRight(this.unfoldOr(operands.subList(1, operands.size()))); + }; + return ObjectExtensions.operator_doubleArrow(_createVLSOr, _function); + } else { + StringConcatenation _builder = new StringConcatenation(); + _builder.append("Logic operator with 0 operands!"); + throw new UnsupportedOperationException(_builder.toString()); + } + } + } + + protected VLSTerm unfoldDistinctTerms(final Logic2VampireLanguageMapper m, final EList operands, final Logic2VampireLanguageMapperTrace trace, final Map variables) { + int _size = operands.size(); + boolean _equals = (_size == 1); + if (_equals) { + return m.transformTerm(IterableExtensions.head(operands), trace, variables); + } else { + int _size_1 = operands.size(); + boolean _greaterThan = (_size_1 > 1); + if (_greaterThan) { + int _size_2 = operands.size(); + int _size_3 = operands.size(); + int _multiply = (_size_2 * _size_3); + int _divide = (_multiply / 2); + final ArrayList notEquals = new ArrayList(_divide); + int _size_4 = operands.size(); + ExclusiveRange _doubleDotLessThan = new ExclusiveRange(0, _size_4, true); + for (final Integer i : _doubleDotLessThan) { + int _size_5 = operands.size(); + ExclusiveRange _doubleDotLessThan_1 = new ExclusiveRange(((i).intValue() + 1), _size_5, true); + for (final Integer j : _doubleDotLessThan_1) { + VLSInequality _createVLSInequality = this.factory.createVLSInequality(); + final Procedure1 _function = (VLSInequality it) -> { + it.setLeft(m.transformTerm(operands.get((i).intValue()), trace, variables)); + it.setRight(m.transformTerm(operands.get((j).intValue()), trace, variables)); + }; + VLSInequality _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSInequality, _function); + notEquals.add(_doubleArrow); + } + } + return this.unfoldAnd(notEquals); + } else { + StringConcatenation _builder = new StringConcatenation(); + _builder.append("Logic operator with 0 operands!"); + throw new UnsupportedOperationException(_builder.toString()); + } + } + } + + /** + * def protected String toID(List ids) { + * ids.map[it.split("\\s+").join("'")].join("'") + * } + */ + protected VLSTerm createUniversallyQuantifiedExpression(final Logic2VampireLanguageMapper mapper, final QuantifiedExpression expression, final Logic2VampireLanguageMapperTrace trace, final Map variables) { + VLSUniversalQuantifier _xblockexpression = null; + { + final Function1 _function = (Variable v) -> { + VLSVariable _createVLSVariable = this.factory.createVLSVariable(); + final Procedure1 _function_1 = (VLSVariable it) -> { + it.setName(this.toIDMultiple("Var", v.getName())); + }; + return ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function_1); + }; + final Map variableMap = IterableExtensions.toInvertedMap(expression.getQuantifiedVariables(), _function); + final ArrayList typedefs = new ArrayList(); + EList _quantifiedVariables = expression.getQuantifiedVariables(); + for (final Variable variable : _quantifiedVariables) { + { + VLSFunction _createVLSFunction = this.factory.createVLSFunction(); + final Procedure1 _function_1 = (VLSFunction it) -> { + TypeReference _range = variable.getRange(); + it.setConstant(this.toIDMultiple("type", ((ComplexTypeReference) _range).getReferred().getName())); + EList _terms = it.getTerms(); + VLSVariable _createVLSVariable = this.factory.createVLSVariable(); + final Procedure1 _function_2 = (VLSVariable it_1) -> { + it_1.setName(this.toIDMultiple("Var", variable.getName())); + }; + VLSVariable _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function_2); + _terms.add(_doubleArrow); + }; + final VLSFunction eq = ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function_1); + typedefs.add(eq); + } + } + VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); + final Procedure1 _function_1 = (VLSUniversalQuantifier it) -> { + EList _variables = it.getVariables(); + Collection _values = variableMap.values(); + Iterables.addAll(_variables, _values); + VLSImplies _createVLSImplies = this.factory.createVLSImplies(); + final Procedure1 _function_2 = (VLSImplies it_1) -> { + it_1.setLeft(this.unfoldAnd(typedefs)); + it_1.setRight(mapper.transformTerm(expression.getExpression(), trace, this.withAddition(variables, variableMap))); + }; + VLSImplies _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSImplies, _function_2); + it.setOperand(_doubleArrow); + }; + _xblockexpression = ObjectExtensions.operator_doubleArrow(_createVLSUniversalQuantifier, _function_1); + } + return _xblockexpression; + } + + protected VLSTerm createExistentiallyQuantifiedExpression(final Logic2VampireLanguageMapper mapper, final QuantifiedExpression expression, final Logic2VampireLanguageMapperTrace trace, final Map variables) { + VLSExistentialQuantifier _xblockexpression = null; + { + final Function1 _function = (Variable v) -> { + VLSVariable _createVLSVariable = this.factory.createVLSVariable(); + final Procedure1 _function_1 = (VLSVariable it) -> { + it.setName(this.toIDMultiple("Var", v.getName())); + }; + return ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function_1); + }; + final Map variableMap = IterableExtensions.toInvertedMap(expression.getQuantifiedVariables(), _function); + final ArrayList typedefs = new ArrayList(); + EList _quantifiedVariables = expression.getQuantifiedVariables(); + for (final Variable variable : _quantifiedVariables) { + { + VLSFunction _createVLSFunction = this.factory.createVLSFunction(); + final Procedure1 _function_1 = (VLSFunction it) -> { + TypeReference _range = variable.getRange(); + it.setConstant(this.toIDMultiple("type", ((ComplexTypeReference) _range).getReferred().getName())); + EList _terms = it.getTerms(); + VLSVariable _createVLSVariable = this.factory.createVLSVariable(); + final Procedure1 _function_2 = (VLSVariable it_1) -> { + it_1.setName(this.toIDMultiple("Var", variable.getName())); + }; + VLSVariable _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function_2); + _terms.add(_doubleArrow); + }; + final VLSFunction eq = ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function_1); + typedefs.add(eq); + } + } + typedefs.add(mapper.transformTerm(expression.getExpression(), trace, this.withAddition(variables, variableMap))); + VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier(); + final Procedure1 _function_1 = (VLSExistentialQuantifier it) -> { + EList _variables = it.getVariables(); + Collection _values = variableMap.values(); + Iterables.addAll(_variables, _values); + it.setOperand(this.unfoldAnd(typedefs)); + }; + _xblockexpression = ObjectExtensions.operator_doubleArrow(_createVLSExistentialQuantifier, _function_1); + } + return _xblockexpression; + } + + protected HashMap withAddition(final Map map1, final Map map2) { + HashMap _hashMap = new HashMap(map1); + final Procedure1> _function = (HashMap it) -> { + it.putAll(map2); + }; + return ObjectExtensions.>operator_doubleArrow(_hashMap, _function); + } +} diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java new file mode 100644 index 00000000..c55e2421 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java @@ -0,0 +1,25 @@ +package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; + +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireModelInterpretation_TypeInterpretation; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement; +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; +import java.util.Collection; +import java.util.List; + +@SuppressWarnings("all") +public interface Logic2VampireLanguageMapper_TypeMapper { + public abstract void transformTypes(final Collection types, final Collection elements, final Logic2VampireLanguageMapper mapper, final Logic2VampireLanguageMapperTrace trace); + + public abstract List transformTypeReference(final Type referred, final Logic2VampireLanguageMapper mapper, final Logic2VampireLanguageMapperTrace trace); + + public abstract VLSTerm getUndefinedSupertype(final Logic2VampireLanguageMapperTrace trace); + + public abstract int getUndefinedSupertypeScope(final int undefinedScope, final Logic2VampireLanguageMapperTrace trace); + + public abstract VLSTerm transformReference(final DefinedElement referred, final Logic2VampireLanguageMapperTrace trace); + + public abstract VampireModelInterpretation_TypeInterpretation getTypeInterpreter(); +} diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapperTrace.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapperTrace.java new file mode 100644 index 00000000..1e08c8ad --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapperTrace.java @@ -0,0 +1,5 @@ +package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; + +@SuppressWarnings("all") +public interface Logic2VampireLanguageMapper_TypeMapperTrace { +} diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.java new file mode 100644 index 00000000..d674ac71 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.java @@ -0,0 +1,21 @@ +package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; + +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapperTrace; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement; +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; +import java.util.HashMap; +import java.util.Map; + +@SuppressWarnings("all") +public class Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes implements Logic2VampireLanguageMapper_TypeMapperTrace { + public final Map type2Predicate = new HashMap(); + + public final Map definedElement2Declaration = new HashMap(); + + public final Map type2PossibleNot = new HashMap(); + + public final Map type2And = new HashMap(); +} diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.java new file mode 100644 index 00000000..38ff37cd --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.java @@ -0,0 +1,287 @@ +package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; + +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapper; +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes; +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireModelInterpretation_TypeInterpretation; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSDoubleQuote; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUnaryNegation; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; +import com.google.common.base.Objects; +import com.google.common.collect.Iterables; +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.logiclanguage.TypeDefinition; +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage; +import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; +import java.util.ArrayList; +import java.util.Collection; +import java.util.List; +import org.eclipse.emf.common.util.EList; +import org.eclipse.xtext.xbase.lib.Extension; +import org.eclipse.xtext.xbase.lib.Functions.Function1; +import org.eclipse.xtext.xbase.lib.IterableExtensions; +import org.eclipse.xtext.xbase.lib.ListExtensions; +import org.eclipse.xtext.xbase.lib.ObjectExtensions; +import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; + +@SuppressWarnings("all") +public class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2VampireLanguageMapper_TypeMapper { + private final Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support(); + + @Extension + private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE; + + public Logic2VampireLanguageMapper_TypeMapper_FilteredTypes() { + LogicproblemPackage.eINSTANCE.getClass(); + } + + @Override + public void transformTypes(final Collection types, final Collection elements, final Logic2VampireLanguageMapper mapper, final Logic2VampireLanguageMapperTrace trace) { + final Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes typeTrace = new Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes(); + trace.typeMapperTrace = typeTrace; + VLSVariable _createVLSVariable = this.factory.createVLSVariable(); + final Procedure1 _function = (VLSVariable it) -> { + it.setName("A"); + }; + final VLSVariable variable = ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function); + for (final Type type : types) { + { + VLSFunction _createVLSFunction = this.factory.createVLSFunction(); + final Procedure1 _function_1 = (VLSFunction it) -> { + it.setConstant(this.support.toIDMultiple("type", type.getName())); + EList _terms = it.getTerms(); + VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable(); + final Procedure1 _function_2 = (VLSVariable it_1) -> { + it_1.setName(variable.getName()); + }; + VLSVariable _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSVariable_1, _function_2); + _terms.add(_doubleArrow); + }; + final VLSFunction typePred = ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function_1); + typeTrace.type2Predicate.put(type, typePred); + } + } + Iterable _filter = Iterables.filter(types, TypeDefinition.class); + for (final TypeDefinition type_1 : _filter) { + { + VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); + final Procedure1 _function_1 = (VLSFofFormula it) -> { + it.setName(this.support.toIDMultiple("typeDef", type_1.getName())); + it.setFofRole("axiom"); + VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); + final Procedure1 _function_2 = (VLSUniversalQuantifier it_1) -> { + EList _variables = it_1.getVariables(); + VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable(); + final Procedure1 _function_3 = (VLSVariable it_2) -> { + it_2.setName(variable.getName()); + }; + VLSVariable _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSVariable_1, _function_3); + _variables.add(_doubleArrow); + VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); + final Procedure1 _function_4 = (VLSEquivalent it_2) -> { + VLSFunction _createVLSFunction = this.factory.createVLSFunction(); + final Procedure1 _function_5 = (VLSFunction it_3) -> { + it_3.setConstant(CollectionsUtil.lookup(type_1, typeTrace.type2Predicate).getConstant()); + EList _terms = it_3.getTerms(); + VLSVariable _createVLSVariable_2 = this.factory.createVLSVariable(); + final Procedure1 _function_6 = (VLSVariable it_4) -> { + it_4.setName("A"); + }; + VLSVariable _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createVLSVariable_2, _function_6); + _terms.add(_doubleArrow_1); + }; + VLSFunction _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function_5); + it_2.setLeft(_doubleArrow_1); + CollectionsUtil.lookup(type_1, typeTrace.type2Predicate); + final Function1 _function_6 = (DefinedElement e) -> { + VLSEquality _createVLSEquality = this.factory.createVLSEquality(); + final Procedure1 _function_7 = (VLSEquality it_3) -> { + VLSVariable _createVLSVariable_2 = this.factory.createVLSVariable(); + final Procedure1 _function_8 = (VLSVariable it_4) -> { + it_4.setName(variable.getName()); + }; + VLSVariable _doubleArrow_2 = ObjectExtensions.operator_doubleArrow(_createVLSVariable_2, _function_8); + it_3.setLeft(_doubleArrow_2); + VLSDoubleQuote _createVLSDoubleQuote = this.factory.createVLSDoubleQuote(); + final Procedure1 _function_9 = (VLSDoubleQuote it_4) -> { + String _name = e.getName(); + String _plus = ("\"a" + _name); + String _plus_1 = (_plus + "\""); + it_4.setValue(_plus_1); + }; + VLSDoubleQuote _doubleArrow_3 = ObjectExtensions.operator_doubleArrow(_createVLSDoubleQuote, _function_9); + it_3.setRight(_doubleArrow_3); + }; + return ObjectExtensions.operator_doubleArrow(_createVLSEquality, _function_7); + }; + it_2.setRight(this.support.unfoldOr(ListExtensions.map(type_1.getElements(), _function_6))); + }; + VLSEquivalent _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createVLSEquivalent, _function_4); + it_1.setOperand(_doubleArrow_1); + }; + VLSUniversalQuantifier _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSUniversalQuantifier, _function_2); + it.setFofFormula(_doubleArrow); + }; + final VLSFofFormula res = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula, _function_1); + EList _formulas = trace.specification.getFormulas(); + _formulas.add(res); + } + } + final Function1 _function_1 = (Type it) -> { + boolean _isIsAbstract = it.isIsAbstract(); + return Boolean.valueOf((!_isIsAbstract)); + }; + Iterable _filter_1 = IterableExtensions.filter(types, _function_1); + for (final Type type_2 : _filter_1) { + { + for (final Type type2 : types) { + if ((Objects.equal(type_2, type2) || this.dfsSupertypeCheck(type_2, type2))) { + VLSFunction _createVLSFunction = this.factory.createVLSFunction(); + final Procedure1 _function_2 = (VLSFunction it) -> { + it.setConstant(CollectionsUtil.lookup(type2, typeTrace.type2Predicate).getConstant()); + EList _terms = it.getTerms(); + VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable(); + final Procedure1 _function_3 = (VLSVariable it_1) -> { + it_1.setName("A"); + }; + VLSVariable _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSVariable_1, _function_3); + _terms.add(_doubleArrow); + }; + VLSFunction _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function_2); + typeTrace.type2PossibleNot.put(type2, _doubleArrow); + } else { + VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); + final Procedure1 _function_3 = (VLSUnaryNegation it) -> { + VLSFunction _createVLSFunction_1 = this.factory.createVLSFunction(); + final Procedure1 _function_4 = (VLSFunction it_1) -> { + it_1.setConstant(CollectionsUtil.lookup(type2, typeTrace.type2Predicate).getConstant()); + EList _terms = it_1.getTerms(); + VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable(); + final Procedure1 _function_5 = (VLSVariable it_2) -> { + it_2.setName("A"); + }; + VLSVariable _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createVLSVariable_1, _function_5); + _terms.add(_doubleArrow_1); + }; + VLSFunction _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createVLSFunction_1, _function_4); + it.setOperand(_doubleArrow_1); + }; + VLSUnaryNegation _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createVLSUnaryNegation, _function_3); + typeTrace.type2PossibleNot.put(type2, _doubleArrow_1); + } + } + Collection _values = typeTrace.type2PossibleNot.values(); + ArrayList _arrayList = new ArrayList(_values); + typeTrace.type2And.put(type_2, this.support.unfoldAnd(_arrayList)); + typeTrace.type2PossibleNot.clear(); + } + } + VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); + final Procedure1 _function_2 = (VLSFofFormula it) -> { + it.setName("hierarchyHandler"); + it.setFofRole("axiom"); + VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); + final Procedure1 _function_3 = (VLSUniversalQuantifier it_1) -> { + EList _variables = it_1.getVariables(); + VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable(); + final Procedure1 _function_4 = (VLSVariable it_2) -> { + it_2.setName("A"); + }; + VLSVariable _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSVariable_1, _function_4); + _variables.add(_doubleArrow); + VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); + final Procedure1 _function_5 = (VLSEquivalent it_2) -> { + VLSFunction _createVLSFunction = this.factory.createVLSFunction(); + final Procedure1 _function_6 = (VLSFunction it_3) -> { + it_3.setConstant("Object"); + EList _terms = it_3.getTerms(); + VLSVariable _createVLSVariable_2 = this.factory.createVLSVariable(); + final Procedure1 _function_7 = (VLSVariable it_4) -> { + it_4.setName("A"); + }; + VLSVariable _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createVLSVariable_2, _function_7); + _terms.add(_doubleArrow_1); + }; + VLSFunction _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function_6); + it_2.setLeft(_doubleArrow_1); + Collection _values = typeTrace.type2And.values(); + ArrayList _arrayList = new ArrayList(_values); + it_2.setRight(this.support.unfoldOr(_arrayList)); + }; + VLSEquivalent _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createVLSEquivalent, _function_5); + it_1.setOperand(_doubleArrow_1); + }; + VLSUniversalQuantifier _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSUniversalQuantifier, _function_3); + it.setFofFormula(_doubleArrow); + }; + final VLSFofFormula hierarch = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula, _function_2); + EList _formulas = trace.specification.getFormulas(); + _formulas.add(hierarch); + } + + public boolean dfsSupertypeCheck(final Type type, final Type type2) { + boolean _xifexpression = false; + boolean _isEmpty = type.getSupertypes().isEmpty(); + if (_isEmpty) { + return false; + } else { + boolean _xifexpression_1 = false; + boolean _contains = type.getSupertypes().contains(type2); + if (_contains) { + return true; + } else { + EList _supertypes = type.getSupertypes(); + for (final Type supertype : _supertypes) { + boolean _dfsSupertypeCheck = this.dfsSupertypeCheck(supertype, type2); + if (_dfsSupertypeCheck) { + return true; + } + } + } + _xifexpression = _xifexpression_1; + } + return _xifexpression; + } + + @Override + public List transformTypeReference(final Type referred, final Logic2VampireLanguageMapper mapper, final Logic2VampireLanguageMapperTrace trace) { + throw new UnsupportedOperationException("TODO: auto-generated method stub"); + } + + @Override + public VLSTerm getUndefinedSupertype(final Logic2VampireLanguageMapperTrace trace) { + throw new UnsupportedOperationException("TODO: auto-generated method stub"); + } + + @Override + public int getUndefinedSupertypeScope(final int undefinedScope, final Logic2VampireLanguageMapperTrace trace) { + throw new UnsupportedOperationException("TODO: auto-generated method stub"); + } + + @Override + public VLSTerm transformReference(final DefinedElement referred, final Logic2VampireLanguageMapperTrace trace) { + VLSDoubleQuote _createVLSDoubleQuote = this.factory.createVLSDoubleQuote(); + final Procedure1 _function = (VLSDoubleQuote it) -> { + String _name = referred.getName(); + String _plus = ("\"a" + _name); + String _plus_1 = (_plus + "\""); + it.setValue(_plus_1); + }; + return ObjectExtensions.operator_doubleArrow(_createVLSDoubleQuote, _function); + } + + @Override + public VampireModelInterpretation_TypeInterpretation getTypeInterpreter() { + throw new UnsupportedOperationException("TODO: auto-generated method stub"); + } +} diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation_TypeInterpretation.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation_TypeInterpretation.java new file mode 100644 index 00000000..507831fa --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation_TypeInterpretation.java @@ -0,0 +1,5 @@ +package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; + +@SuppressWarnings("all") +public interface VampireModelInterpretation_TypeInterpretation { +} diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation_TypeInterpretation_FilteredTypes.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation_TypeInterpretation_FilteredTypes.java new file mode 100644 index 00000000..aff0dc9d --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation_TypeInterpretation_FilteredTypes.java @@ -0,0 +1,7 @@ +package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; + +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireModelInterpretation_TypeInterpretation; + +@SuppressWarnings("all") +public class VampireModelInterpretation_TypeInterpretation_FilteredTypes implements VampireModelInterpretation_TypeInterpretation { +} -- cgit v1.2.3-54-g00ecf