From 20f131a3f09edf8e1455f20b4f486629147e7eff Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Tue, 15 Jan 2019 12:44:33 -0500 Subject: Initial workspace setup --- .../.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 + 29 files changed, 1514 insertions(+) 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/xtend-gen/ca/mcgill/ecse/dslreasoner') 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