diff options
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill')
29 files changed, 1514 insertions, 0 deletions
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 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin | |||
Binary files 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 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin | |||
Binary files 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 @@ | |||
1 | /.VampireSolver.java._trace | ||
2 | /.TypeMappingTechnique.java._trace | ||
3 | /.VampireBackendSolver.java._trace | ||
4 | /.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 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner; | ||
2 | |||
3 | @SuppressWarnings("all") | ||
4 | public enum TypeMappingTechnique { | ||
5 | FilteredTypes; | ||
6 | } | ||
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 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner; | ||
2 | |||
3 | @SuppressWarnings("all") | ||
4 | public enum VampireBackendSolver { | ||
5 | } | ||
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 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner; | ||
2 | |||
3 | import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetup; | ||
4 | import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetupGenerated; | ||
5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration; | ||
6 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; | ||
7 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; | ||
8 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes; | ||
9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage; | ||
10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel; | ||
11 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicModelInterpretation; | ||
12 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner; | ||
13 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException; | ||
14 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration; | ||
15 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput; | ||
16 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem; | ||
17 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult; | ||
18 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult; | ||
19 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace; | ||
20 | import java.io.PrintWriter; | ||
21 | import java.util.List; | ||
22 | import org.eclipse.xtend2.lib.StringConcatenation; | ||
23 | import org.eclipse.xtext.xbase.lib.Exceptions; | ||
24 | |||
25 | @SuppressWarnings("all") | ||
26 | public class VampireSolver extends LogicReasoner { | ||
27 | public VampireSolver() { | ||
28 | VampireLanguagePackage.eINSTANCE.eClass(); | ||
29 | final VampireLanguageStandaloneSetupGenerated x = new VampireLanguageStandaloneSetupGenerated(); | ||
30 | VampireLanguageStandaloneSetup.doSetup(); | ||
31 | } | ||
32 | |||
33 | private final Logic2VampireLanguageMapper forwardMapper = new Logic2VampireLanguageMapper(new Logic2VampireLanguageMapper_TypeMapper_FilteredTypes()); | ||
34 | |||
35 | private final String fileName = "problem.tptp"; | ||
36 | |||
37 | @Override | ||
38 | public LogicResult solve(final LogicProblem problem, final LogicSolverConfiguration configuration, final ReasonerWorkspace workspace) throws LogicReasonerException { | ||
39 | try { | ||
40 | final VampireSolverConfiguration vampireConfig = this.asConfig(configuration); | ||
41 | final long transformationStart = System.currentTimeMillis(); | ||
42 | final TracedOutput<VampireModel, Logic2VampireLanguageMapperTrace> result = this.forwardMapper.transformProblem(problem, vampireConfig); | ||
43 | final VampireModel vampireProblem = result.getOutput(); | ||
44 | final Logic2VampireLanguageMapperTrace forwardTrace = result.getTrace(); | ||
45 | String fileURI = null; | ||
46 | String vampireCode = null; | ||
47 | if (vampireConfig.writeToFile) { | ||
48 | fileURI = workspace.writeModel(vampireProblem, this.fileName).toFileString(); | ||
49 | } else { | ||
50 | vampireCode = workspace.writeModelToString(vampireProblem, this.fileName); | ||
51 | } | ||
52 | long _currentTimeMillis = System.currentTimeMillis(); | ||
53 | final long transformationTime = (_currentTimeMillis - transformationStart); | ||
54 | final PrintWriter out = new PrintWriter("output/files/vampireCode.tptp"); | ||
55 | out.println(vampireCode); | ||
56 | out.close(); | ||
57 | return null; | ||
58 | } catch (Throwable _e) { | ||
59 | throw Exceptions.sneakyThrow(_e); | ||
60 | } | ||
61 | } | ||
62 | |||
63 | public VampireSolverConfiguration asConfig(final LogicSolverConfiguration configuration) { | ||
64 | if ((configuration instanceof VampireSolverConfiguration)) { | ||
65 | return ((VampireSolverConfiguration)configuration); | ||
66 | } else { | ||
67 | StringConcatenation _builder = new StringConcatenation(); | ||
68 | _builder.append("The configuration have to be an "); | ||
69 | String _simpleName = VampireSolverConfiguration.class.getSimpleName(); | ||
70 | _builder.append(_simpleName); | ||
71 | _builder.append("!"); | ||
72 | throw new IllegalArgumentException(_builder.toString()); | ||
73 | } | ||
74 | } | ||
75 | |||
76 | @Override | ||
77 | public List<? extends LogicModelInterpretation> getInterpretations(final ModelResult modelResult) { | ||
78 | return null; | ||
79 | } | ||
80 | } | ||
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 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner; | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration; | ||
4 | |||
5 | @SuppressWarnings("all") | ||
6 | public class VampireSolverConfiguration extends LogicSolverConfiguration { | ||
7 | public int symmetry = 0; | ||
8 | |||
9 | public boolean writeToFile = false; | ||
10 | } | ||
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 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin | |||
Binary files 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 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin | |||
Binary files 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 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin | |||
Binary files 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 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin | |||
Binary files 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 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin | |||
Binary files 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 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin | |||
Binary files 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 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtendbin | |||
Binary files 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 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtendbin | |||
Binary files 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 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin | |||
Binary files 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 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin | |||
Binary files 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 @@ | |||
1 | /.Logic2VampireLanguageMapper_ConstantMapper.java._trace | ||
2 | /.Logic2VampireLanguageMapper.java._trace | ||
3 | /.Logic2VampireLanguageMapperTrace.java._trace | ||
4 | /.Logic2VampireLanguageMapper_TypeMapperTrace.java._trace | ||
5 | /.VampireModelInterpretation_TypeInterpretation.java._trace | ||
6 | /.VampireModelInterpretation_TypeInterpretation_FilteredTypes.java._trace | ||
7 | /.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.java._trace | ||
8 | /.Logic2VampireLanguageMapper_TypeMapper.java._trace | ||
9 | /.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.java._trace | ||
10 | /.Logic2VampireLanguageMapper_Support.java._trace | ||
11 | /.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 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; | ||
2 | |||
3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration; | ||
4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; | ||
5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_ConstantMapper; | ||
6 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_RelationMapper; | ||
7 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; | ||
8 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapper; | ||
9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSComment; | ||
10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant; | ||
11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality; | ||
12 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent; | ||
13 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; | ||
14 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; | ||
15 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies; | ||
16 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSInt; | ||
17 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSReal; | ||
18 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; | ||
19 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUnaryNegation; | ||
20 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; | ||
21 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; | ||
22 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel; | ||
23 | import com.google.common.collect.Iterables; | ||
24 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput; | ||
25 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And; | ||
26 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Assertion; | ||
27 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolLiteral; | ||
28 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference; | ||
29 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference; | ||
30 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration; | ||
31 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDefinition; | ||
32 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement; | ||
33 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Distinct; | ||
34 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Equals; | ||
35 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Exists; | ||
36 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Forall; | ||
37 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration; | ||
38 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDefinition; | ||
39 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Iff; | ||
40 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Impl; | ||
41 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.InstanceOf; | ||
42 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntLiteral; | ||
43 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Not; | ||
44 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Or; | ||
45 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealLiteral; | ||
46 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation; | ||
47 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration; | ||
48 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition; | ||
49 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicDeclaration; | ||
50 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue; | ||
51 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term; | ||
52 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference; | ||
53 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable; | ||
54 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem; | ||
55 | import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; | ||
56 | import java.util.Arrays; | ||
57 | import java.util.Collections; | ||
58 | import java.util.HashMap; | ||
59 | import java.util.List; | ||
60 | import java.util.Map; | ||
61 | import java.util.function.Consumer; | ||
62 | import org.eclipse.emf.common.util.EList; | ||
63 | import org.eclipse.xtend.lib.annotations.AccessorType; | ||
64 | import org.eclipse.xtend.lib.annotations.Accessors; | ||
65 | import org.eclipse.xtext.xbase.lib.Extension; | ||
66 | import org.eclipse.xtext.xbase.lib.Functions.Function1; | ||
67 | import org.eclipse.xtext.xbase.lib.IterableExtensions; | ||
68 | import org.eclipse.xtext.xbase.lib.ListExtensions; | ||
69 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; | ||
70 | import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; | ||
71 | import org.eclipse.xtext.xbase.lib.Pure; | ||
72 | |||
73 | @SuppressWarnings("all") | ||
74 | public class Logic2VampireLanguageMapper { | ||
75 | @Extension | ||
76 | private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE; | ||
77 | |||
78 | private final Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support(); | ||
79 | |||
80 | @Accessors(AccessorType.PUBLIC_GETTER) | ||
81 | private final Logic2VampireLanguageMapper_ConstantMapper constantMapper = new Logic2VampireLanguageMapper_ConstantMapper(this); | ||
82 | |||
83 | @Accessors(AccessorType.PUBLIC_GETTER) | ||
84 | private final Logic2VampireLanguageMapper_RelationMapper relationMapper = new Logic2VampireLanguageMapper_RelationMapper(this); | ||
85 | |||
86 | @Accessors(AccessorType.PUBLIC_GETTER) | ||
87 | private final Logic2VampireLanguageMapper_TypeMapper typeMapper; | ||
88 | |||
89 | public Logic2VampireLanguageMapper(final Logic2VampireLanguageMapper_TypeMapper typeMapper) { | ||
90 | this.typeMapper = typeMapper; | ||
91 | } | ||
92 | |||
93 | public TracedOutput<VampireModel, Logic2VampireLanguageMapperTrace> transformProblem(final LogicProblem problem, final VampireSolverConfiguration configuration) { | ||
94 | VLSComment _createVLSComment = this.factory.createVLSComment(); | ||
95 | final Procedure1<VLSComment> _function = (VLSComment it) -> { | ||
96 | it.setComment("%This is an initial Test Comment \r"); | ||
97 | }; | ||
98 | final VLSComment initialComment = ObjectExtensions.<VLSComment>operator_doubleArrow(_createVLSComment, _function); | ||
99 | VampireModel _createVampireModel = this.factory.createVampireModel(); | ||
100 | final Procedure1<VampireModel> _function_1 = (VampireModel it) -> { | ||
101 | EList<VLSComment> _comments = it.getComments(); | ||
102 | _comments.add(initialComment); | ||
103 | }; | ||
104 | final VampireModel specification = ObjectExtensions.<VampireModel>operator_doubleArrow(_createVampireModel, _function_1); | ||
105 | Logic2VampireLanguageMapperTrace _logic2VampireLanguageMapperTrace = new Logic2VampireLanguageMapperTrace(); | ||
106 | final Procedure1<Logic2VampireLanguageMapperTrace> _function_2 = (Logic2VampireLanguageMapperTrace it) -> { | ||
107 | it.specification = specification; | ||
108 | }; | ||
109 | final Logic2VampireLanguageMapperTrace trace = ObjectExtensions.<Logic2VampireLanguageMapperTrace>operator_doubleArrow(_logic2VampireLanguageMapperTrace, _function_2); | ||
110 | boolean _isEmpty = problem.getTypes().isEmpty(); | ||
111 | boolean _not = (!_isEmpty); | ||
112 | if (_not) { | ||
113 | this.typeMapper.transformTypes(problem.getTypes(), problem.getElements(), this, trace); | ||
114 | } | ||
115 | trace.constantDefinitions = this.collectConstantDefinitions(problem); | ||
116 | trace.relationDefinitions = this.collectRelationDefinitions(problem); | ||
117 | final Consumer<Relation> _function_3 = (Relation it) -> { | ||
118 | this.relationMapper.transformRelation(it, trace); | ||
119 | }; | ||
120 | problem.getRelations().forEach(_function_3); | ||
121 | final Consumer<ConstantDefinition> _function_4 = (ConstantDefinition it) -> { | ||
122 | this.constantMapper.transformConstantDefinitionSpecification(it, trace); | ||
123 | }; | ||
124 | Iterables.<ConstantDefinition>filter(problem.getConstants(), ConstantDefinition.class).forEach(_function_4); | ||
125 | EList<Assertion> _assertions = problem.getAssertions(); | ||
126 | for (final Assertion assertion : _assertions) { | ||
127 | this.transformAssertion(assertion, trace); | ||
128 | } | ||
129 | return new TracedOutput<VampireModel, Logic2VampireLanguageMapperTrace>(specification, trace); | ||
130 | } | ||
131 | |||
132 | protected VLSTerm _transformTypeReference(final BoolTypeReference boolTypeReference, final Logic2VampireLanguageMapperTrace trace) { | ||
133 | return null; | ||
134 | } | ||
135 | |||
136 | private HashMap<ConstantDeclaration, ConstantDefinition> collectConstantDefinitions(final LogicProblem problem) { | ||
137 | final HashMap<ConstantDeclaration, ConstantDefinition> res = new HashMap<ConstantDeclaration, ConstantDefinition>(); | ||
138 | final Function1<ConstantDefinition, Boolean> _function = (ConstantDefinition it) -> { | ||
139 | ConstantDeclaration _defines = it.getDefines(); | ||
140 | return Boolean.valueOf((_defines != null)); | ||
141 | }; | ||
142 | final Consumer<ConstantDefinition> _function_1 = (ConstantDefinition it) -> { | ||
143 | res.put(it.getDefines(), it); | ||
144 | }; | ||
145 | IterableExtensions.<ConstantDefinition>filter(Iterables.<ConstantDefinition>filter(problem.getConstants(), ConstantDefinition.class), _function).forEach(_function_1); | ||
146 | return res; | ||
147 | } | ||
148 | |||
149 | private HashMap<RelationDeclaration, RelationDefinition> collectRelationDefinitions(final LogicProblem problem) { | ||
150 | final HashMap<RelationDeclaration, RelationDefinition> res = new HashMap<RelationDeclaration, RelationDefinition>(); | ||
151 | final Function1<RelationDefinition, Boolean> _function = (RelationDefinition it) -> { | ||
152 | RelationDeclaration _defines = it.getDefines(); | ||
153 | return Boolean.valueOf((_defines != null)); | ||
154 | }; | ||
155 | final Consumer<RelationDefinition> _function_1 = (RelationDefinition it) -> { | ||
156 | res.put(it.getDefines(), it); | ||
157 | }; | ||
158 | IterableExtensions.<RelationDefinition>filter(Iterables.<RelationDefinition>filter(problem.getRelations(), RelationDefinition.class), _function).forEach(_function_1); | ||
159 | return res; | ||
160 | } | ||
161 | |||
162 | protected boolean transformAssertion(final Assertion assertion, final Logic2VampireLanguageMapperTrace trace) { | ||
163 | boolean _xblockexpression = false; | ||
164 | { | ||
165 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | ||
166 | final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> { | ||
167 | it.setName(this.support.toID(assertion.getName())); | ||
168 | it.setFofRole("axiom"); | ||
169 | it.setFofFormula(this.transformTerm(assertion.getValue(), trace, Collections.EMPTY_MAP)); | ||
170 | }; | ||
171 | final VLSFofFormula res = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function); | ||
172 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); | ||
173 | _xblockexpression = _formulas.add(res); | ||
174 | } | ||
175 | return _xblockexpression; | ||
176 | } | ||
177 | |||
178 | protected VLSTerm _transformTerm(final BoolLiteral literal, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
179 | VLSTerm _xifexpression = null; | ||
180 | boolean _isValue = literal.isValue(); | ||
181 | boolean _equals = (_isValue == true); | ||
182 | if (_equals) { | ||
183 | _xifexpression = this.factory.createVLSTrue(); | ||
184 | } else { | ||
185 | _xifexpression = this.factory.createVLSFalse(); | ||
186 | } | ||
187 | return _xifexpression; | ||
188 | } | ||
189 | |||
190 | protected VLSTerm _transformTerm(final IntLiteral literal, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
191 | VLSInt _createVLSInt = this.factory.createVLSInt(); | ||
192 | final Procedure1<VLSInt> _function = (VLSInt it) -> { | ||
193 | it.setValue(Integer.valueOf(literal.getValue()).toString()); | ||
194 | }; | ||
195 | return ObjectExtensions.<VLSInt>operator_doubleArrow(_createVLSInt, _function); | ||
196 | } | ||
197 | |||
198 | protected VLSTerm _transformTerm(final RealLiteral literal, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
199 | VLSReal _createVLSReal = this.factory.createVLSReal(); | ||
200 | final Procedure1<VLSReal> _function = (VLSReal it) -> { | ||
201 | it.setValue(literal.getValue().toString()); | ||
202 | }; | ||
203 | return ObjectExtensions.<VLSReal>operator_doubleArrow(_createVLSReal, _function); | ||
204 | } | ||
205 | |||
206 | protected VLSTerm _transformTerm(final Not not, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
207 | VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); | ||
208 | final Procedure1<VLSUnaryNegation> _function = (VLSUnaryNegation it) -> { | ||
209 | it.setOperand(this.transformTerm(not.getOperand(), trace, variables)); | ||
210 | }; | ||
211 | return ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function); | ||
212 | } | ||
213 | |||
214 | protected VLSTerm _transformTerm(final And and, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
215 | final Function1<Term, VLSTerm> _function = (Term it) -> { | ||
216 | return this.transformTerm(it, trace, variables); | ||
217 | }; | ||
218 | return this.support.unfoldAnd(ListExtensions.<Term, VLSTerm>map(and.getOperands(), _function)); | ||
219 | } | ||
220 | |||
221 | protected VLSTerm _transformTerm(final Or or, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
222 | final Function1<Term, VLSTerm> _function = (Term it) -> { | ||
223 | return this.transformTerm(it, trace, variables); | ||
224 | }; | ||
225 | return this.support.unfoldOr(ListExtensions.<Term, VLSTerm>map(or.getOperands(), _function)); | ||
226 | } | ||
227 | |||
228 | protected VLSTerm _transformTerm(final Impl impl, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
229 | VLSImplies _createVLSImplies = this.factory.createVLSImplies(); | ||
230 | final Procedure1<VLSImplies> _function = (VLSImplies it) -> { | ||
231 | it.setLeft(this.transformTerm(impl.getLeftOperand(), trace, variables)); | ||
232 | it.setRight(this.transformTerm(impl.getRightOperand(), trace, variables)); | ||
233 | }; | ||
234 | return ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function); | ||
235 | } | ||
236 | |||
237 | protected VLSTerm _transformTerm(final Iff iff, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
238 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); | ||
239 | final Procedure1<VLSEquivalent> _function = (VLSEquivalent it) -> { | ||
240 | it.setLeft(this.transformTerm(iff.getLeftOperand(), trace, variables)); | ||
241 | it.setRight(this.transformTerm(iff.getRightOperand(), trace, variables)); | ||
242 | }; | ||
243 | return ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function); | ||
244 | } | ||
245 | |||
246 | protected VLSTerm _transformTerm(final Equals equals, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
247 | VLSEquality _createVLSEquality = this.factory.createVLSEquality(); | ||
248 | final Procedure1<VLSEquality> _function = (VLSEquality it) -> { | ||
249 | it.setLeft(this.transformTerm(equals.getLeftOperand(), trace, variables)); | ||
250 | it.setRight(this.transformTerm(equals.getRightOperand(), trace, variables)); | ||
251 | }; | ||
252 | return ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function); | ||
253 | } | ||
254 | |||
255 | protected VLSTerm _transformTerm(final Distinct distinct, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
256 | return this.support.unfoldDistinctTerms(this, distinct.getOperands(), trace, variables); | ||
257 | } | ||
258 | |||
259 | protected VLSTerm _transformTerm(final Forall forall, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
260 | return this.support.createUniversallyQuantifiedExpression(this, forall, trace, variables); | ||
261 | } | ||
262 | |||
263 | protected VLSTerm _transformTerm(final Exists exists, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
264 | return this.support.createExistentiallyQuantifiedExpression(this, exists, trace, variables); | ||
265 | } | ||
266 | |||
267 | protected VLSTerm _transformTerm(final InstanceOf instanceOf, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
268 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
269 | final Procedure1<VLSFunction> _function = (VLSFunction it) -> { | ||
270 | TypeReference _range = instanceOf.getRange(); | ||
271 | it.setConstant(this.support.toIDMultiple("type", ((ComplexTypeReference) _range).getReferred().getName())); | ||
272 | EList<VLSTerm> _terms = it.getTerms(); | ||
273 | VLSTerm _transformTerm = this.transformTerm(instanceOf.getValue(), trace, variables); | ||
274 | _terms.add(_transformTerm); | ||
275 | }; | ||
276 | return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function); | ||
277 | } | ||
278 | |||
279 | protected VLSTerm _transformTerm(final SymbolicValue symbolicValue, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
280 | return this.transformSymbolicReference(symbolicValue.getSymbolicReference(), symbolicValue.getParameterSubstitutions(), trace, variables); | ||
281 | } | ||
282 | |||
283 | protected VLSTerm _transformSymbolicReference(final DefinedElement referred, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
284 | return this.typeMapper.transformReference(referred, trace); | ||
285 | } | ||
286 | |||
287 | protected VLSTerm _transformSymbolicReference(final ConstantDeclaration constant, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
288 | VLSConstant _createVLSConstant = this.factory.createVLSConstant(); | ||
289 | final Procedure1<VLSConstant> _function = (VLSConstant it) -> { | ||
290 | it.setName(this.support.toID(constant.getName())); | ||
291 | }; | ||
292 | final VLSConstant res = ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _function); | ||
293 | return res; | ||
294 | } | ||
295 | |||
296 | protected VLSTerm _transformSymbolicReference(final ConstantDefinition constant, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
297 | return null; | ||
298 | } | ||
299 | |||
300 | protected VLSTerm _transformSymbolicReference(final Variable variable, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
301 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
302 | final Procedure1<VLSVariable> _function = (VLSVariable it) -> { | ||
303 | it.setName(this.support.toID(CollectionsUtil.<Variable, VLSVariable>lookup(variable, variables).getName())); | ||
304 | }; | ||
305 | final VLSVariable res = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function); | ||
306 | return res; | ||
307 | } | ||
308 | |||
309 | protected VLSTerm _transformSymbolicReference(final FunctionDeclaration function, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
310 | return null; | ||
311 | } | ||
312 | |||
313 | protected VLSTerm _transformSymbolicReference(final FunctionDefinition function, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
314 | return null; | ||
315 | } | ||
316 | |||
317 | /** | ||
318 | * def dispatch protected VLSTerm transformSymbolicReference(Relation relation, | ||
319 | * List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace, | ||
320 | * Map<Variable, VLSVariable> variables) { | ||
321 | * if (trace.relationDefinitions.containsKey(relation)) { | ||
322 | * this.transformSymbolicReference(relation.lookup(trace.relationDefinitions), | ||
323 | * parameterSubstitutions, trace, variables) | ||
324 | * } | ||
325 | * else { | ||
326 | * // if (relationMapper.transformToHostedField(relation, trace)) { | ||
327 | * // val VLSRelation = relation.lookup(trace.relationDeclaration2Field) | ||
328 | * // // R(a,b) => | ||
329 | * // // b in a.R | ||
330 | * // return createVLSSubset => [ | ||
331 | * // it.leftOperand = parameterSubstitutions.get(1).transformTerm(trace, variables) | ||
332 | * // it.rightOperand = createVLSJoin => [ | ||
333 | * // it.leftOperand = parameterSubstitutions.get(0).transformTerm(trace, variables) | ||
334 | * // it.rightOperand = createVLSReference => [it.referred = VLSRelation] | ||
335 | * // ] | ||
336 | * // ] | ||
337 | * // } else { | ||
338 | * // val target = createVLSJoin => [ | ||
339 | * // leftOperand = createVLSReference => [referred = trace.logicLanguage] | ||
340 | * // rightOperand = createVLSReference => [ | ||
341 | * // referred = relation.lookup(trace.relationDeclaration2Global) | ||
342 | * // ] | ||
343 | * // ] | ||
344 | * // val source = support.unfoldTermDirectProduct(this, parameterSubstitutions, trace, variables) | ||
345 | * // | ||
346 | * // return createVLSSubset => [ | ||
347 | * // leftOperand = source | ||
348 | * // rightOperand = target | ||
349 | * // ] | ||
350 | * // } | ||
351 | * } | ||
352 | * } | ||
353 | */ | ||
354 | protected VLSTerm _transformSymbolicReference(final Relation relation, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
355 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
356 | final Procedure1<VLSFunction> _function = (VLSFunction it) -> { | ||
357 | it.setConstant(this.support.toIDMultiple("rel", relation.getName())); | ||
358 | EList<VLSTerm> _terms = it.getTerms(); | ||
359 | final Function1<Term, VLSTerm> _function_1 = (Term p) -> { | ||
360 | return this.transformTerm(p, trace, variables); | ||
361 | }; | ||
362 | List<VLSTerm> _map = ListExtensions.<Term, VLSTerm>map(parameterSubstitutions, _function_1); | ||
363 | Iterables.<VLSTerm>addAll(_terms, _map); | ||
364 | }; | ||
365 | return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function); | ||
366 | } | ||
367 | |||
368 | protected VLSTerm transformTypeReference(final BoolTypeReference boolTypeReference, final Logic2VampireLanguageMapperTrace trace) { | ||
369 | return _transformTypeReference(boolTypeReference, trace); | ||
370 | } | ||
371 | |||
372 | protected VLSTerm transformTerm(final Term and, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
373 | if (and instanceof And) { | ||
374 | return _transformTerm((And)and, trace, variables); | ||
375 | } else if (and instanceof BoolLiteral) { | ||
376 | return _transformTerm((BoolLiteral)and, trace, variables); | ||
377 | } else if (and instanceof Distinct) { | ||
378 | return _transformTerm((Distinct)and, trace, variables); | ||
379 | } else if (and instanceof Equals) { | ||
380 | return _transformTerm((Equals)and, trace, variables); | ||
381 | } else if (and instanceof Exists) { | ||
382 | return _transformTerm((Exists)and, trace, variables); | ||
383 | } else if (and instanceof Forall) { | ||
384 | return _transformTerm((Forall)and, trace, variables); | ||
385 | } else if (and instanceof Iff) { | ||
386 | return _transformTerm((Iff)and, trace, variables); | ||
387 | } else if (and instanceof Impl) { | ||
388 | return _transformTerm((Impl)and, trace, variables); | ||
389 | } else if (and instanceof IntLiteral) { | ||
390 | return _transformTerm((IntLiteral)and, trace, variables); | ||
391 | } else if (and instanceof Not) { | ||
392 | return _transformTerm((Not)and, trace, variables); | ||
393 | } else if (and instanceof Or) { | ||
394 | return _transformTerm((Or)and, trace, variables); | ||
395 | } else if (and instanceof RealLiteral) { | ||
396 | return _transformTerm((RealLiteral)and, trace, variables); | ||
397 | } else if (and instanceof InstanceOf) { | ||
398 | return _transformTerm((InstanceOf)and, trace, variables); | ||
399 | } else if (and instanceof SymbolicValue) { | ||
400 | return _transformTerm((SymbolicValue)and, trace, variables); | ||
401 | } else { | ||
402 | throw new IllegalArgumentException("Unhandled parameter types: " + | ||
403 | Arrays.<Object>asList(and, trace, variables).toString()); | ||
404 | } | ||
405 | } | ||
406 | |||
407 | protected VLSTerm transformSymbolicReference(final SymbolicDeclaration constant, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
408 | if (constant instanceof ConstantDeclaration) { | ||
409 | return _transformSymbolicReference((ConstantDeclaration)constant, parameterSubstitutions, trace, variables); | ||
410 | } else if (constant instanceof ConstantDefinition) { | ||
411 | return _transformSymbolicReference((ConstantDefinition)constant, parameterSubstitutions, trace, variables); | ||
412 | } else if (constant instanceof FunctionDeclaration) { | ||
413 | return _transformSymbolicReference((FunctionDeclaration)constant, parameterSubstitutions, trace, variables); | ||
414 | } else if (constant instanceof FunctionDefinition) { | ||
415 | return _transformSymbolicReference((FunctionDefinition)constant, parameterSubstitutions, trace, variables); | ||
416 | } else if (constant instanceof DefinedElement) { | ||
417 | return _transformSymbolicReference((DefinedElement)constant, parameterSubstitutions, trace, variables); | ||
418 | } else if (constant instanceof Relation) { | ||
419 | return _transformSymbolicReference((Relation)constant, parameterSubstitutions, trace, variables); | ||
420 | } else if (constant instanceof Variable) { | ||
421 | return _transformSymbolicReference((Variable)constant, parameterSubstitutions, trace, variables); | ||
422 | } else { | ||
423 | throw new IllegalArgumentException("Unhandled parameter types: " + | ||
424 | Arrays.<Object>asList(constant, parameterSubstitutions, trace, variables).toString()); | ||
425 | } | ||
426 | } | ||
427 | |||
428 | @Pure | ||
429 | public Logic2VampireLanguageMapper_ConstantMapper getConstantMapper() { | ||
430 | return this.constantMapper; | ||
431 | } | ||
432 | |||
433 | @Pure | ||
434 | public Logic2VampireLanguageMapper_RelationMapper getRelationMapper() { | ||
435 | return this.relationMapper; | ||
436 | } | ||
437 | |||
438 | @Pure | ||
439 | public Logic2VampireLanguageMapper_TypeMapper getTypeMapper() { | ||
440 | return this.typeMapper; | ||
441 | } | ||
442 | } | ||
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 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; | ||
2 | |||
3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapperTrace; | ||
4 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; | ||
5 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; | ||
6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; | ||
7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; | ||
8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel; | ||
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration; | ||
10 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDefinition; | ||
11 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration; | ||
12 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition; | ||
13 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable; | ||
14 | import java.util.HashMap; | ||
15 | import java.util.Map; | ||
16 | |||
17 | @SuppressWarnings("all") | ||
18 | public class Logic2VampireLanguageMapperTrace { | ||
19 | public VampireModel specification; | ||
20 | |||
21 | public VLSFofFormula logicLanguageBody; | ||
22 | |||
23 | public VLSTerm formula; | ||
24 | |||
25 | public Logic2VampireLanguageMapper_TypeMapperTrace typeMapperTrace; | ||
26 | |||
27 | public Map<ConstantDeclaration, ConstantDefinition> constantDefinitions; | ||
28 | |||
29 | public Map<RelationDeclaration, RelationDefinition> relationDefinitions; | ||
30 | |||
31 | public final Map<Variable, VLSVariable> relationVar2VLS = new HashMap<Variable, VLSVariable>(); | ||
32 | |||
33 | public final Map<Variable, VLSFunction> relationVar2TypeDec = new HashMap<Variable, VLSFunction>(); | ||
34 | } | ||
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 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; | ||
2 | |||
3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; | ||
4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; | ||
5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; | ||
6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDefinition; | ||
8 | import org.eclipse.xtext.xbase.lib.Extension; | ||
9 | |||
10 | @SuppressWarnings("all") | ||
11 | public class Logic2VampireLanguageMapper_ConstantMapper { | ||
12 | @Extension | ||
13 | private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE; | ||
14 | |||
15 | private final Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support(); | ||
16 | |||
17 | private final Logic2VampireLanguageMapper base; | ||
18 | |||
19 | public Logic2VampireLanguageMapper_ConstantMapper(final Logic2VampireLanguageMapper base) { | ||
20 | this.base = base; | ||
21 | } | ||
22 | |||
23 | protected Object _transformConstant(final ConstantDefinition constant, final Logic2VampireLanguageMapperTrace trace) { | ||
24 | return null; | ||
25 | } | ||
26 | |||
27 | protected Object transformConstantDefinitionSpecification(final ConstantDefinition constant, final Logic2VampireLanguageMapperTrace trace) { | ||
28 | return null; | ||
29 | } | ||
30 | |||
31 | protected Object transformConstant(final ConstantDefinition constant, final Logic2VampireLanguageMapperTrace trace) { | ||
32 | return _transformConstant(constant, trace); | ||
33 | } | ||
34 | } | ||
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 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; | ||
2 | |||
3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; | ||
4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; | ||
5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; | ||
6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent; | ||
7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; | ||
8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; | ||
9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies; | ||
10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; | ||
11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; | ||
12 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; | ||
13 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; | ||
14 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference; | ||
15 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation; | ||
16 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration; | ||
17 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition; | ||
18 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference; | ||
19 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable; | ||
20 | import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; | ||
21 | import java.util.ArrayList; | ||
22 | import java.util.Arrays; | ||
23 | import java.util.Collection; | ||
24 | import java.util.HashMap; | ||
25 | import java.util.List; | ||
26 | import java.util.Map; | ||
27 | import org.eclipse.emf.common.util.EList; | ||
28 | import org.eclipse.xtext.xbase.lib.Conversions; | ||
29 | import org.eclipse.xtext.xbase.lib.ExclusiveRange; | ||
30 | import org.eclipse.xtext.xbase.lib.Extension; | ||
31 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; | ||
32 | import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; | ||
33 | |||
34 | @SuppressWarnings("all") | ||
35 | public class Logic2VampireLanguageMapper_RelationMapper { | ||
36 | @Extension | ||
37 | private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE; | ||
38 | |||
39 | private final Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support(); | ||
40 | |||
41 | private final Logic2VampireLanguageMapper base; | ||
42 | |||
43 | public Logic2VampireLanguageMapper_RelationMapper(final Logic2VampireLanguageMapper base) { | ||
44 | this.base = base; | ||
45 | } | ||
46 | |||
47 | public void _transformRelation(final RelationDefinition r, final Logic2VampireLanguageMapperTrace trace) { | ||
48 | final Map<Variable, VLSVariable> relationVar2VLS = new HashMap<Variable, VLSVariable>(); | ||
49 | final Map<Variable, VLSFunction> relationVar2TypeDecComply = new HashMap<Variable, VLSFunction>(); | ||
50 | final Map<Variable, VLSFunction> relationVar2TypeDecRes = new HashMap<Variable, VLSFunction>(); | ||
51 | final ArrayList<VLSTerm> typedefs = new ArrayList<VLSTerm>(); | ||
52 | EList<Variable> _variables = r.getVariables(); | ||
53 | for (final Variable variable : _variables) { | ||
54 | { | ||
55 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
56 | final Procedure1<VLSVariable> _function = (VLSVariable it) -> { | ||
57 | it.setName(this.support.toIDMultiple("Var", variable.getName())); | ||
58 | }; | ||
59 | final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function); | ||
60 | relationVar2VLS.put(variable, v); | ||
61 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
62 | final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> { | ||
63 | TypeReference _range = variable.getRange(); | ||
64 | it.setConstant(this.support.toIDMultiple("type", ((ComplexTypeReference) _range).getReferred().getName())); | ||
65 | EList<VLSTerm> _terms = it.getTerms(); | ||
66 | VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable(); | ||
67 | final Procedure1<VLSVariable> _function_2 = (VLSVariable it_1) -> { | ||
68 | it_1.setName(this.support.toIDMultiple("Var", variable.getName())); | ||
69 | }; | ||
70 | VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_2); | ||
71 | _terms.add(_doubleArrow); | ||
72 | }; | ||
73 | final VLSFunction varTypeComply = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_1); | ||
74 | relationVar2TypeDecComply.put(variable, varTypeComply); | ||
75 | VLSFunction _createVLSFunction_1 = this.factory.createVLSFunction(); | ||
76 | final Procedure1<VLSFunction> _function_2 = (VLSFunction it) -> { | ||
77 | TypeReference _range = variable.getRange(); | ||
78 | it.setConstant(this.support.toIDMultiple("type", ((ComplexTypeReference) _range).getReferred().getName())); | ||
79 | EList<VLSTerm> _terms = it.getTerms(); | ||
80 | VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable(); | ||
81 | final Procedure1<VLSVariable> _function_3 = (VLSVariable it_1) -> { | ||
82 | it_1.setName(this.support.toIDMultiple("Var", variable.getName())); | ||
83 | }; | ||
84 | VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_3); | ||
85 | _terms.add(_doubleArrow); | ||
86 | }; | ||
87 | final VLSFunction varTypeRes = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction_1, _function_2); | ||
88 | relationVar2TypeDecRes.put(variable, varTypeRes); | ||
89 | } | ||
90 | } | ||
91 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | ||
92 | final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> { | ||
93 | it.setName(this.support.toIDMultiple("compliance", r.getName())); | ||
94 | it.setFofRole("axiom"); | ||
95 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | ||
96 | final Procedure1<VLSUniversalQuantifier> _function_1 = (VLSUniversalQuantifier it_1) -> { | ||
97 | EList<Variable> _variables_1 = r.getVariables(); | ||
98 | for (final Variable variable_1 : _variables_1) { | ||
99 | { | ||
100 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
101 | final Procedure1<VLSVariable> _function_2 = (VLSVariable it_2) -> { | ||
102 | it_2.setName(CollectionsUtil.<Variable, VLSVariable>lookup(variable_1, relationVar2VLS).getName()); | ||
103 | }; | ||
104 | final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_2); | ||
105 | EList<VLSVariable> _variables_2 = it_1.getVariables(); | ||
106 | _variables_2.add(v); | ||
107 | } | ||
108 | } | ||
109 | VLSImplies _createVLSImplies = this.factory.createVLSImplies(); | ||
110 | final Procedure1<VLSImplies> _function_2 = (VLSImplies it_2) -> { | ||
111 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
112 | final Procedure1<VLSFunction> _function_3 = (VLSFunction it_3) -> { | ||
113 | it_3.setConstant(this.support.toIDMultiple("rel", r.getName())); | ||
114 | EList<Variable> _variables_2 = r.getVariables(); | ||
115 | for (final Variable variable_2 : _variables_2) { | ||
116 | { | ||
117 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
118 | final Procedure1<VLSVariable> _function_4 = (VLSVariable it_4) -> { | ||
119 | it_4.setName(CollectionsUtil.<Variable, VLSVariable>lookup(variable_2, relationVar2VLS).getName()); | ||
120 | }; | ||
121 | final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_4); | ||
122 | EList<VLSTerm> _terms = it_3.getTerms(); | ||
123 | _terms.add(v); | ||
124 | } | ||
125 | } | ||
126 | }; | ||
127 | VLSFunction _doubleArrow = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_3); | ||
128 | it_2.setLeft(_doubleArrow); | ||
129 | Collection<VLSFunction> _values = relationVar2TypeDecComply.values(); | ||
130 | ArrayList<VLSTerm> _arrayList = new ArrayList<VLSTerm>(_values); | ||
131 | it_2.setRight(this.support.unfoldAnd(_arrayList)); | ||
132 | }; | ||
133 | VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_2); | ||
134 | it_1.setOperand(_doubleArrow); | ||
135 | }; | ||
136 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_1); | ||
137 | it.setFofFormula(_doubleArrow); | ||
138 | }; | ||
139 | final VLSFofFormula comply = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function); | ||
140 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); | ||
141 | final Procedure1<VLSFofFormula> _function_1 = (VLSFofFormula it) -> { | ||
142 | it.setName(this.support.toIDMultiple("relation", r.getName())); | ||
143 | it.setFofRole("axiom"); | ||
144 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | ||
145 | final Procedure1<VLSUniversalQuantifier> _function_2 = (VLSUniversalQuantifier it_1) -> { | ||
146 | EList<Variable> _variables_1 = r.getVariables(); | ||
147 | for (final Variable variable_1 : _variables_1) { | ||
148 | { | ||
149 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
150 | final Procedure1<VLSVariable> _function_3 = (VLSVariable it_2) -> { | ||
151 | it_2.setName(CollectionsUtil.<Variable, VLSVariable>lookup(variable_1, relationVar2VLS).getName()); | ||
152 | }; | ||
153 | final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_3); | ||
154 | EList<VLSVariable> _variables_2 = it_1.getVariables(); | ||
155 | _variables_2.add(v); | ||
156 | } | ||
157 | } | ||
158 | VLSImplies _createVLSImplies = this.factory.createVLSImplies(); | ||
159 | final Procedure1<VLSImplies> _function_3 = (VLSImplies it_2) -> { | ||
160 | Collection<VLSFunction> _values = relationVar2TypeDecRes.values(); | ||
161 | ArrayList<VLSTerm> _arrayList = new ArrayList<VLSTerm>(_values); | ||
162 | it_2.setLeft(this.support.unfoldAnd(_arrayList)); | ||
163 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); | ||
164 | final Procedure1<VLSEquivalent> _function_4 = (VLSEquivalent it_3) -> { | ||
165 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
166 | final Procedure1<VLSFunction> _function_5 = (VLSFunction it_4) -> { | ||
167 | it_4.setConstant(this.support.toIDMultiple("rel", r.getName())); | ||
168 | EList<Variable> _variables_2 = r.getVariables(); | ||
169 | for (final Variable variable_2 : _variables_2) { | ||
170 | { | ||
171 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
172 | final Procedure1<VLSVariable> _function_6 = (VLSVariable it_5) -> { | ||
173 | it_5.setName(CollectionsUtil.<Variable, VLSVariable>lookup(variable_2, relationVar2VLS).getName()); | ||
174 | }; | ||
175 | final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_6); | ||
176 | EList<VLSTerm> _terms = it_4.getTerms(); | ||
177 | _terms.add(v); | ||
178 | } | ||
179 | } | ||
180 | }; | ||
181 | VLSFunction _doubleArrow = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_5); | ||
182 | it_3.setLeft(_doubleArrow); | ||
183 | it_3.setRight(this.base.transformTerm(r.getValue(), trace, relationVar2VLS)); | ||
184 | }; | ||
185 | VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_4); | ||
186 | it_2.setRight(_doubleArrow); | ||
187 | }; | ||
188 | VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_3); | ||
189 | it_1.setOperand(_doubleArrow); | ||
190 | }; | ||
191 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_2); | ||
192 | it.setFofFormula(_doubleArrow); | ||
193 | }; | ||
194 | final VLSFofFormula res = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_1); | ||
195 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); | ||
196 | _formulas.add(comply); | ||
197 | EList<VLSFofFormula> _formulas_1 = trace.specification.getFormulas(); | ||
198 | _formulas_1.add(res); | ||
199 | } | ||
200 | |||
201 | public void _transformRelation(final RelationDeclaration r, final Logic2VampireLanguageMapperTrace trace) { | ||
202 | final List<VLSVariable> relationVar2VLS = new ArrayList<VLSVariable>(); | ||
203 | final List<VLSFunction> relationVar2TypeDecComply = new ArrayList<VLSFunction>(); | ||
204 | final ArrayList<VLSTerm> typedefs = new ArrayList<VLSTerm>(); | ||
205 | int _length = ((Object[])Conversions.unwrapArray(r.getParameters(), Object.class)).length; | ||
206 | ExclusiveRange _doubleDotLessThan = new ExclusiveRange(0, _length, true); | ||
207 | for (final Integer i : _doubleDotLessThan) { | ||
208 | { | ||
209 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
210 | final Procedure1<VLSVariable> _function = (VLSVariable it) -> { | ||
211 | it.setName(this.support.toIDMultiple("Var", i.toString())); | ||
212 | }; | ||
213 | final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function); | ||
214 | relationVar2VLS.add(v); | ||
215 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
216 | final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> { | ||
217 | TypeReference _get = r.getParameters().get((i).intValue()); | ||
218 | it.setConstant(this.support.toIDMultiple("type", ((ComplexTypeReference) _get).getReferred().getName())); | ||
219 | EList<VLSTerm> _terms = it.getTerms(); | ||
220 | VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable(); | ||
221 | final Procedure1<VLSVariable> _function_2 = (VLSVariable it_1) -> { | ||
222 | it_1.setName(this.support.toIDMultiple("Var", i.toString())); | ||
223 | }; | ||
224 | VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_2); | ||
225 | _terms.add(_doubleArrow); | ||
226 | }; | ||
227 | final VLSFunction varTypeComply = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_1); | ||
228 | relationVar2TypeDecComply.add(varTypeComply); | ||
229 | } | ||
230 | } | ||
231 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | ||
232 | final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> { | ||
233 | it.setName(this.support.toIDMultiple("compliance", r.getName())); | ||
234 | it.setFofRole("axiom"); | ||
235 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | ||
236 | final Procedure1<VLSUniversalQuantifier> _function_1 = (VLSUniversalQuantifier it_1) -> { | ||
237 | int _length_1 = ((Object[])Conversions.unwrapArray(r.getParameters(), Object.class)).length; | ||
238 | ExclusiveRange _doubleDotLessThan_1 = new ExclusiveRange(0, _length_1, true); | ||
239 | for (final Integer i_1 : _doubleDotLessThan_1) { | ||
240 | { | ||
241 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
242 | final Procedure1<VLSVariable> _function_2 = (VLSVariable it_2) -> { | ||
243 | it_2.setName(relationVar2VLS.get((i_1).intValue()).getName()); | ||
244 | }; | ||
245 | final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_2); | ||
246 | EList<VLSVariable> _variables = it_1.getVariables(); | ||
247 | _variables.add(v); | ||
248 | } | ||
249 | } | ||
250 | VLSImplies _createVLSImplies = this.factory.createVLSImplies(); | ||
251 | final Procedure1<VLSImplies> _function_2 = (VLSImplies it_2) -> { | ||
252 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
253 | final Procedure1<VLSFunction> _function_3 = (VLSFunction it_3) -> { | ||
254 | it_3.setConstant(this.support.toIDMultiple("rel", r.getName())); | ||
255 | int _length_2 = ((Object[])Conversions.unwrapArray(r.getParameters(), Object.class)).length; | ||
256 | ExclusiveRange _doubleDotLessThan_2 = new ExclusiveRange(0, _length_2, true); | ||
257 | for (final Integer i_2 : _doubleDotLessThan_2) { | ||
258 | { | ||
259 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
260 | final Procedure1<VLSVariable> _function_4 = (VLSVariable it_4) -> { | ||
261 | it_4.setName(relationVar2VLS.get((i_2).intValue()).getName()); | ||
262 | }; | ||
263 | final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_4); | ||
264 | EList<VLSTerm> _terms = it_3.getTerms(); | ||
265 | _terms.add(v); | ||
266 | } | ||
267 | } | ||
268 | }; | ||
269 | VLSFunction _doubleArrow = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_3); | ||
270 | it_2.setLeft(_doubleArrow); | ||
271 | it_2.setRight(this.support.unfoldAnd(relationVar2TypeDecComply)); | ||
272 | }; | ||
273 | VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_2); | ||
274 | it_1.setOperand(_doubleArrow); | ||
275 | }; | ||
276 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_1); | ||
277 | it.setFofFormula(_doubleArrow); | ||
278 | }; | ||
279 | final VLSFofFormula comply = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function); | ||
280 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); | ||
281 | _formulas.add(comply); | ||
282 | } | ||
283 | |||
284 | public void transformRelation(final Relation r, final Logic2VampireLanguageMapperTrace trace) { | ||
285 | if (r instanceof RelationDeclaration) { | ||
286 | _transformRelation((RelationDeclaration)r, trace); | ||
287 | return; | ||
288 | } else if (r instanceof RelationDefinition) { | ||
289 | _transformRelation((RelationDefinition)r, trace); | ||
290 | return; | ||
291 | } else { | ||
292 | throw new IllegalArgumentException("Unhandled parameter types: " + | ||
293 | Arrays.<Object>asList(r, trace).toString()); | ||
294 | } | ||
295 | } | ||
296 | } | ||
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 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; | ||
2 | |||
3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; | ||
4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; | ||
5 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSAnd; | ||
6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSExistentialQuantifier; | ||
7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; | ||
8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies; | ||
9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSInequality; | ||
10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSOr; | ||
11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; | ||
12 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; | ||
13 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; | ||
14 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; | ||
15 | import com.google.common.collect.Iterables; | ||
16 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference; | ||
17 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.QuantifiedExpression; | ||
18 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term; | ||
19 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference; | ||
20 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable; | ||
21 | import java.util.ArrayList; | ||
22 | import java.util.Collection; | ||
23 | import java.util.HashMap; | ||
24 | import java.util.List; | ||
25 | import java.util.Map; | ||
26 | import org.eclipse.emf.common.util.EList; | ||
27 | import org.eclipse.xtend2.lib.StringConcatenation; | ||
28 | import org.eclipse.xtext.xbase.lib.Conversions; | ||
29 | import org.eclipse.xtext.xbase.lib.ExclusiveRange; | ||
30 | import org.eclipse.xtext.xbase.lib.Extension; | ||
31 | import org.eclipse.xtext.xbase.lib.Functions.Function1; | ||
32 | import org.eclipse.xtext.xbase.lib.IterableExtensions; | ||
33 | import org.eclipse.xtext.xbase.lib.ListExtensions; | ||
34 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; | ||
35 | import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; | ||
36 | |||
37 | @SuppressWarnings("all") | ||
38 | public class Logic2VampireLanguageMapper_Support { | ||
39 | @Extension | ||
40 | private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE; | ||
41 | |||
42 | protected String toIDMultiple(final String... ids) { | ||
43 | final Function1<String, String> _function = (String it) -> { | ||
44 | return IterableExtensions.join(((Iterable<?>)Conversions.doWrapArray(it.split("\\s+"))), "_"); | ||
45 | }; | ||
46 | return IterableExtensions.join(ListExtensions.<String, String>map(((List<String>)Conversions.doWrapArray(ids)), _function), "_"); | ||
47 | } | ||
48 | |||
49 | protected String toID(final String ids) { | ||
50 | return IterableExtensions.join(((Iterable<?>)Conversions.doWrapArray(ids.split("\\s+"))), "_"); | ||
51 | } | ||
52 | |||
53 | protected VLSTerm unfoldAnd(final List<? extends VLSTerm> operands) { | ||
54 | int _size = operands.size(); | ||
55 | boolean _equals = (_size == 1); | ||
56 | if (_equals) { | ||
57 | return IterableExtensions.head(operands); | ||
58 | } else { | ||
59 | int _size_1 = operands.size(); | ||
60 | boolean _greaterThan = (_size_1 > 1); | ||
61 | if (_greaterThan) { | ||
62 | VLSAnd _createVLSAnd = this.factory.createVLSAnd(); | ||
63 | final Procedure1<VLSAnd> _function = (VLSAnd it) -> { | ||
64 | it.setLeft(IterableExtensions.head(operands)); | ||
65 | it.setRight(this.unfoldAnd(operands.subList(1, operands.size()))); | ||
66 | }; | ||
67 | return ObjectExtensions.<VLSAnd>operator_doubleArrow(_createVLSAnd, _function); | ||
68 | } else { | ||
69 | StringConcatenation _builder = new StringConcatenation(); | ||
70 | _builder.append("Logic operator with 0 operands!"); | ||
71 | throw new UnsupportedOperationException(_builder.toString()); | ||
72 | } | ||
73 | } | ||
74 | } | ||
75 | |||
76 | protected VLSTerm unfoldOr(final List<? extends VLSTerm> operands) { | ||
77 | int _size = operands.size(); | ||
78 | boolean _equals = (_size == 1); | ||
79 | if (_equals) { | ||
80 | return IterableExtensions.head(operands); | ||
81 | } else { | ||
82 | int _size_1 = operands.size(); | ||
83 | boolean _greaterThan = (_size_1 > 1); | ||
84 | if (_greaterThan) { | ||
85 | VLSOr _createVLSOr = this.factory.createVLSOr(); | ||
86 | final Procedure1<VLSOr> _function = (VLSOr it) -> { | ||
87 | it.setLeft(IterableExtensions.head(operands)); | ||
88 | it.setRight(this.unfoldOr(operands.subList(1, operands.size()))); | ||
89 | }; | ||
90 | return ObjectExtensions.<VLSOr>operator_doubleArrow(_createVLSOr, _function); | ||
91 | } else { | ||
92 | StringConcatenation _builder = new StringConcatenation(); | ||
93 | _builder.append("Logic operator with 0 operands!"); | ||
94 | throw new UnsupportedOperationException(_builder.toString()); | ||
95 | } | ||
96 | } | ||
97 | } | ||
98 | |||
99 | protected VLSTerm unfoldDistinctTerms(final Logic2VampireLanguageMapper m, final EList<Term> operands, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
100 | int _size = operands.size(); | ||
101 | boolean _equals = (_size == 1); | ||
102 | if (_equals) { | ||
103 | return m.transformTerm(IterableExtensions.<Term>head(operands), trace, variables); | ||
104 | } else { | ||
105 | int _size_1 = operands.size(); | ||
106 | boolean _greaterThan = (_size_1 > 1); | ||
107 | if (_greaterThan) { | ||
108 | int _size_2 = operands.size(); | ||
109 | int _size_3 = operands.size(); | ||
110 | int _multiply = (_size_2 * _size_3); | ||
111 | int _divide = (_multiply / 2); | ||
112 | final ArrayList<VLSTerm> notEquals = new ArrayList<VLSTerm>(_divide); | ||
113 | int _size_4 = operands.size(); | ||
114 | ExclusiveRange _doubleDotLessThan = new ExclusiveRange(0, _size_4, true); | ||
115 | for (final Integer i : _doubleDotLessThan) { | ||
116 | int _size_5 = operands.size(); | ||
117 | ExclusiveRange _doubleDotLessThan_1 = new ExclusiveRange(((i).intValue() + 1), _size_5, true); | ||
118 | for (final Integer j : _doubleDotLessThan_1) { | ||
119 | VLSInequality _createVLSInequality = this.factory.createVLSInequality(); | ||
120 | final Procedure1<VLSInequality> _function = (VLSInequality it) -> { | ||
121 | it.setLeft(m.transformTerm(operands.get((i).intValue()), trace, variables)); | ||
122 | it.setRight(m.transformTerm(operands.get((j).intValue()), trace, variables)); | ||
123 | }; | ||
124 | VLSInequality _doubleArrow = ObjectExtensions.<VLSInequality>operator_doubleArrow(_createVLSInequality, _function); | ||
125 | notEquals.add(_doubleArrow); | ||
126 | } | ||
127 | } | ||
128 | return this.unfoldAnd(notEquals); | ||
129 | } else { | ||
130 | StringConcatenation _builder = new StringConcatenation(); | ||
131 | _builder.append("Logic operator with 0 operands!"); | ||
132 | throw new UnsupportedOperationException(_builder.toString()); | ||
133 | } | ||
134 | } | ||
135 | } | ||
136 | |||
137 | /** | ||
138 | * def protected String toID(List<String> ids) { | ||
139 | * ids.map[it.split("\\s+").join("'")].join("'") | ||
140 | * } | ||
141 | */ | ||
142 | protected VLSTerm createUniversallyQuantifiedExpression(final Logic2VampireLanguageMapper mapper, final QuantifiedExpression expression, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
143 | VLSUniversalQuantifier _xblockexpression = null; | ||
144 | { | ||
145 | final Function1<Variable, VLSVariable> _function = (Variable v) -> { | ||
146 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
147 | final Procedure1<VLSVariable> _function_1 = (VLSVariable it) -> { | ||
148 | it.setName(this.toIDMultiple("Var", v.getName())); | ||
149 | }; | ||
150 | return ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_1); | ||
151 | }; | ||
152 | final Map<Variable, VLSVariable> variableMap = IterableExtensions.<Variable, VLSVariable>toInvertedMap(expression.getQuantifiedVariables(), _function); | ||
153 | final ArrayList<VLSTerm> typedefs = new ArrayList<VLSTerm>(); | ||
154 | EList<Variable> _quantifiedVariables = expression.getQuantifiedVariables(); | ||
155 | for (final Variable variable : _quantifiedVariables) { | ||
156 | { | ||
157 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
158 | final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> { | ||
159 | TypeReference _range = variable.getRange(); | ||
160 | it.setConstant(this.toIDMultiple("type", ((ComplexTypeReference) _range).getReferred().getName())); | ||
161 | EList<VLSTerm> _terms = it.getTerms(); | ||
162 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
163 | final Procedure1<VLSVariable> _function_2 = (VLSVariable it_1) -> { | ||
164 | it_1.setName(this.toIDMultiple("Var", variable.getName())); | ||
165 | }; | ||
166 | VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_2); | ||
167 | _terms.add(_doubleArrow); | ||
168 | }; | ||
169 | final VLSFunction eq = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_1); | ||
170 | typedefs.add(eq); | ||
171 | } | ||
172 | } | ||
173 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | ||
174 | final Procedure1<VLSUniversalQuantifier> _function_1 = (VLSUniversalQuantifier it) -> { | ||
175 | EList<VLSVariable> _variables = it.getVariables(); | ||
176 | Collection<VLSVariable> _values = variableMap.values(); | ||
177 | Iterables.<VLSVariable>addAll(_variables, _values); | ||
178 | VLSImplies _createVLSImplies = this.factory.createVLSImplies(); | ||
179 | final Procedure1<VLSImplies> _function_2 = (VLSImplies it_1) -> { | ||
180 | it_1.setLeft(this.unfoldAnd(typedefs)); | ||
181 | it_1.setRight(mapper.transformTerm(expression.getExpression(), trace, this.withAddition(variables, variableMap))); | ||
182 | }; | ||
183 | VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_2); | ||
184 | it.setOperand(_doubleArrow); | ||
185 | }; | ||
186 | _xblockexpression = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_1); | ||
187 | } | ||
188 | return _xblockexpression; | ||
189 | } | ||
190 | |||
191 | protected VLSTerm createExistentiallyQuantifiedExpression(final Logic2VampireLanguageMapper mapper, final QuantifiedExpression expression, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
192 | VLSExistentialQuantifier _xblockexpression = null; | ||
193 | { | ||
194 | final Function1<Variable, VLSVariable> _function = (Variable v) -> { | ||
195 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
196 | final Procedure1<VLSVariable> _function_1 = (VLSVariable it) -> { | ||
197 | it.setName(this.toIDMultiple("Var", v.getName())); | ||
198 | }; | ||
199 | return ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_1); | ||
200 | }; | ||
201 | final Map<Variable, VLSVariable> variableMap = IterableExtensions.<Variable, VLSVariable>toInvertedMap(expression.getQuantifiedVariables(), _function); | ||
202 | final ArrayList<VLSTerm> typedefs = new ArrayList<VLSTerm>(); | ||
203 | EList<Variable> _quantifiedVariables = expression.getQuantifiedVariables(); | ||
204 | for (final Variable variable : _quantifiedVariables) { | ||
205 | { | ||
206 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
207 | final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> { | ||
208 | TypeReference _range = variable.getRange(); | ||
209 | it.setConstant(this.toIDMultiple("type", ((ComplexTypeReference) _range).getReferred().getName())); | ||
210 | EList<VLSTerm> _terms = it.getTerms(); | ||
211 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
212 | final Procedure1<VLSVariable> _function_2 = (VLSVariable it_1) -> { | ||
213 | it_1.setName(this.toIDMultiple("Var", variable.getName())); | ||
214 | }; | ||
215 | VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_2); | ||
216 | _terms.add(_doubleArrow); | ||
217 | }; | ||
218 | final VLSFunction eq = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_1); | ||
219 | typedefs.add(eq); | ||
220 | } | ||
221 | } | ||
222 | typedefs.add(mapper.transformTerm(expression.getExpression(), trace, this.withAddition(variables, variableMap))); | ||
223 | VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier(); | ||
224 | final Procedure1<VLSExistentialQuantifier> _function_1 = (VLSExistentialQuantifier it) -> { | ||
225 | EList<VLSVariable> _variables = it.getVariables(); | ||
226 | Collection<VLSVariable> _values = variableMap.values(); | ||
227 | Iterables.<VLSVariable>addAll(_variables, _values); | ||
228 | it.setOperand(this.unfoldAnd(typedefs)); | ||
229 | }; | ||
230 | _xblockexpression = ObjectExtensions.<VLSExistentialQuantifier>operator_doubleArrow(_createVLSExistentialQuantifier, _function_1); | ||
231 | } | ||
232 | return _xblockexpression; | ||
233 | } | ||
234 | |||
235 | protected HashMap<Variable, VLSVariable> withAddition(final Map<Variable, VLSVariable> map1, final Map<Variable, VLSVariable> map2) { | ||
236 | HashMap<Variable, VLSVariable> _hashMap = new HashMap<Variable, VLSVariable>(map1); | ||
237 | final Procedure1<HashMap<Variable, VLSVariable>> _function = (HashMap<Variable, VLSVariable> it) -> { | ||
238 | it.putAll(map2); | ||
239 | }; | ||
240 | return ObjectExtensions.<HashMap<Variable, VLSVariable>>operator_doubleArrow(_hashMap, _function); | ||
241 | } | ||
242 | } | ||
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 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; | ||
2 | |||
3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; | ||
4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; | ||
5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireModelInterpretation_TypeInterpretation; | ||
6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement; | ||
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; | ||
9 | import java.util.Collection; | ||
10 | import java.util.List; | ||
11 | |||
12 | @SuppressWarnings("all") | ||
13 | public interface Logic2VampireLanguageMapper_TypeMapper { | ||
14 | public abstract void transformTypes(final Collection<Type> types, final Collection<DefinedElement> elements, final Logic2VampireLanguageMapper mapper, final Logic2VampireLanguageMapperTrace trace); | ||
15 | |||
16 | public abstract List<VLSTerm> transformTypeReference(final Type referred, final Logic2VampireLanguageMapper mapper, final Logic2VampireLanguageMapperTrace trace); | ||
17 | |||
18 | public abstract VLSTerm getUndefinedSupertype(final Logic2VampireLanguageMapperTrace trace); | ||
19 | |||
20 | public abstract int getUndefinedSupertypeScope(final int undefinedScope, final Logic2VampireLanguageMapperTrace trace); | ||
21 | |||
22 | public abstract VLSTerm transformReference(final DefinedElement referred, final Logic2VampireLanguageMapperTrace trace); | ||
23 | |||
24 | public abstract VampireModelInterpretation_TypeInterpretation getTypeInterpreter(); | ||
25 | } | ||
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 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; | ||
2 | |||
3 | @SuppressWarnings("all") | ||
4 | public interface Logic2VampireLanguageMapper_TypeMapperTrace { | ||
5 | } | ||
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 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; | ||
2 | |||
3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapperTrace; | ||
4 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality; | ||
5 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; | ||
6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement; | ||
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; | ||
9 | import java.util.HashMap; | ||
10 | import java.util.Map; | ||
11 | |||
12 | @SuppressWarnings("all") | ||
13 | public class Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes implements Logic2VampireLanguageMapper_TypeMapperTrace { | ||
14 | public final Map<Type, VLSFunction> type2Predicate = new HashMap<Type, VLSFunction>(); | ||
15 | |||
16 | public final Map<DefinedElement, VLSEquality> definedElement2Declaration = new HashMap<DefinedElement, VLSEquality>(); | ||
17 | |||
18 | public final Map<Type, VLSTerm> type2PossibleNot = new HashMap<Type, VLSTerm>(); | ||
19 | |||
20 | public final Map<Type, VLSTerm> type2And = new HashMap<Type, VLSTerm>(); | ||
21 | } | ||
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 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; | ||
2 | |||
3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; | ||
4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; | ||
5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; | ||
6 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapper; | ||
7 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes; | ||
8 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireModelInterpretation_TypeInterpretation; | ||
9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSDoubleQuote; | ||
10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality; | ||
11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent; | ||
12 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; | ||
13 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; | ||
14 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; | ||
15 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUnaryNegation; | ||
16 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; | ||
17 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; | ||
18 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; | ||
19 | import com.google.common.base.Objects; | ||
20 | import com.google.common.collect.Iterables; | ||
21 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement; | ||
22 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; | ||
23 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition; | ||
24 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage; | ||
25 | import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; | ||
26 | import java.util.ArrayList; | ||
27 | import java.util.Collection; | ||
28 | import java.util.List; | ||
29 | import org.eclipse.emf.common.util.EList; | ||
30 | import org.eclipse.xtext.xbase.lib.Extension; | ||
31 | import org.eclipse.xtext.xbase.lib.Functions.Function1; | ||
32 | import org.eclipse.xtext.xbase.lib.IterableExtensions; | ||
33 | import org.eclipse.xtext.xbase.lib.ListExtensions; | ||
34 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; | ||
35 | import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; | ||
36 | |||
37 | @SuppressWarnings("all") | ||
38 | public class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2VampireLanguageMapper_TypeMapper { | ||
39 | private final Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support(); | ||
40 | |||
41 | @Extension | ||
42 | private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE; | ||
43 | |||
44 | public Logic2VampireLanguageMapper_TypeMapper_FilteredTypes() { | ||
45 | LogicproblemPackage.eINSTANCE.getClass(); | ||
46 | } | ||
47 | |||
48 | @Override | ||
49 | public void transformTypes(final Collection<Type> types, final Collection<DefinedElement> elements, final Logic2VampireLanguageMapper mapper, final Logic2VampireLanguageMapperTrace trace) { | ||
50 | final Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes typeTrace = new Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes(); | ||
51 | trace.typeMapperTrace = typeTrace; | ||
52 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
53 | final Procedure1<VLSVariable> _function = (VLSVariable it) -> { | ||
54 | it.setName("A"); | ||
55 | }; | ||
56 | final VLSVariable variable = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function); | ||
57 | for (final Type type : types) { | ||
58 | { | ||
59 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
60 | final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> { | ||
61 | it.setConstant(this.support.toIDMultiple("type", type.getName())); | ||
62 | EList<VLSTerm> _terms = it.getTerms(); | ||
63 | VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable(); | ||
64 | final Procedure1<VLSVariable> _function_2 = (VLSVariable it_1) -> { | ||
65 | it_1.setName(variable.getName()); | ||
66 | }; | ||
67 | VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_2); | ||
68 | _terms.add(_doubleArrow); | ||
69 | }; | ||
70 | final VLSFunction typePred = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_1); | ||
71 | typeTrace.type2Predicate.put(type, typePred); | ||
72 | } | ||
73 | } | ||
74 | Iterable<TypeDefinition> _filter = Iterables.<TypeDefinition>filter(types, TypeDefinition.class); | ||
75 | for (final TypeDefinition type_1 : _filter) { | ||
76 | { | ||
77 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | ||
78 | final Procedure1<VLSFofFormula> _function_1 = (VLSFofFormula it) -> { | ||
79 | it.setName(this.support.toIDMultiple("typeDef", type_1.getName())); | ||
80 | it.setFofRole("axiom"); | ||
81 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | ||
82 | final Procedure1<VLSUniversalQuantifier> _function_2 = (VLSUniversalQuantifier it_1) -> { | ||
83 | EList<VLSVariable> _variables = it_1.getVariables(); | ||
84 | VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable(); | ||
85 | final Procedure1<VLSVariable> _function_3 = (VLSVariable it_2) -> { | ||
86 | it_2.setName(variable.getName()); | ||
87 | }; | ||
88 | VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_3); | ||
89 | _variables.add(_doubleArrow); | ||
90 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); | ||
91 | final Procedure1<VLSEquivalent> _function_4 = (VLSEquivalent it_2) -> { | ||
92 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
93 | final Procedure1<VLSFunction> _function_5 = (VLSFunction it_3) -> { | ||
94 | it_3.setConstant(CollectionsUtil.<TypeDefinition, VLSFunction>lookup(type_1, typeTrace.type2Predicate).getConstant()); | ||
95 | EList<VLSTerm> _terms = it_3.getTerms(); | ||
96 | VLSVariable _createVLSVariable_2 = this.factory.createVLSVariable(); | ||
97 | final Procedure1<VLSVariable> _function_6 = (VLSVariable it_4) -> { | ||
98 | it_4.setName("A"); | ||
99 | }; | ||
100 | VLSVariable _doubleArrow_1 = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_2, _function_6); | ||
101 | _terms.add(_doubleArrow_1); | ||
102 | }; | ||
103 | VLSFunction _doubleArrow_1 = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_5); | ||
104 | it_2.setLeft(_doubleArrow_1); | ||
105 | CollectionsUtil.<TypeDefinition, VLSFunction>lookup(type_1, typeTrace.type2Predicate); | ||
106 | final Function1<DefinedElement, VLSEquality> _function_6 = (DefinedElement e) -> { | ||
107 | VLSEquality _createVLSEquality = this.factory.createVLSEquality(); | ||
108 | final Procedure1<VLSEquality> _function_7 = (VLSEquality it_3) -> { | ||
109 | VLSVariable _createVLSVariable_2 = this.factory.createVLSVariable(); | ||
110 | final Procedure1<VLSVariable> _function_8 = (VLSVariable it_4) -> { | ||
111 | it_4.setName(variable.getName()); | ||
112 | }; | ||
113 | VLSVariable _doubleArrow_2 = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_2, _function_8); | ||
114 | it_3.setLeft(_doubleArrow_2); | ||
115 | VLSDoubleQuote _createVLSDoubleQuote = this.factory.createVLSDoubleQuote(); | ||
116 | final Procedure1<VLSDoubleQuote> _function_9 = (VLSDoubleQuote it_4) -> { | ||
117 | String _name = e.getName(); | ||
118 | String _plus = ("\"a" + _name); | ||
119 | String _plus_1 = (_plus + "\""); | ||
120 | it_4.setValue(_plus_1); | ||
121 | }; | ||
122 | VLSDoubleQuote _doubleArrow_3 = ObjectExtensions.<VLSDoubleQuote>operator_doubleArrow(_createVLSDoubleQuote, _function_9); | ||
123 | it_3.setRight(_doubleArrow_3); | ||
124 | }; | ||
125 | return ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_7); | ||
126 | }; | ||
127 | it_2.setRight(this.support.unfoldOr(ListExtensions.<DefinedElement, VLSEquality>map(type_1.getElements(), _function_6))); | ||
128 | }; | ||
129 | VLSEquivalent _doubleArrow_1 = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_4); | ||
130 | it_1.setOperand(_doubleArrow_1); | ||
131 | }; | ||
132 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_2); | ||
133 | it.setFofFormula(_doubleArrow); | ||
134 | }; | ||
135 | final VLSFofFormula res = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_1); | ||
136 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); | ||
137 | _formulas.add(res); | ||
138 | } | ||
139 | } | ||
140 | final Function1<Type, Boolean> _function_1 = (Type it) -> { | ||
141 | boolean _isIsAbstract = it.isIsAbstract(); | ||
142 | return Boolean.valueOf((!_isIsAbstract)); | ||
143 | }; | ||
144 | Iterable<Type> _filter_1 = IterableExtensions.<Type>filter(types, _function_1); | ||
145 | for (final Type type_2 : _filter_1) { | ||
146 | { | ||
147 | for (final Type type2 : types) { | ||
148 | if ((Objects.equal(type_2, type2) || this.dfsSupertypeCheck(type_2, type2))) { | ||
149 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
150 | final Procedure1<VLSFunction> _function_2 = (VLSFunction it) -> { | ||
151 | it.setConstant(CollectionsUtil.<Type, VLSFunction>lookup(type2, typeTrace.type2Predicate).getConstant()); | ||
152 | EList<VLSTerm> _terms = it.getTerms(); | ||
153 | VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable(); | ||
154 | final Procedure1<VLSVariable> _function_3 = (VLSVariable it_1) -> { | ||
155 | it_1.setName("A"); | ||
156 | }; | ||
157 | VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_3); | ||
158 | _terms.add(_doubleArrow); | ||
159 | }; | ||
160 | VLSFunction _doubleArrow = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_2); | ||
161 | typeTrace.type2PossibleNot.put(type2, _doubleArrow); | ||
162 | } else { | ||
163 | VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); | ||
164 | final Procedure1<VLSUnaryNegation> _function_3 = (VLSUnaryNegation it) -> { | ||
165 | VLSFunction _createVLSFunction_1 = this.factory.createVLSFunction(); | ||
166 | final Procedure1<VLSFunction> _function_4 = (VLSFunction it_1) -> { | ||
167 | it_1.setConstant(CollectionsUtil.<Type, VLSFunction>lookup(type2, typeTrace.type2Predicate).getConstant()); | ||
168 | EList<VLSTerm> _terms = it_1.getTerms(); | ||
169 | VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable(); | ||
170 | final Procedure1<VLSVariable> _function_5 = (VLSVariable it_2) -> { | ||
171 | it_2.setName("A"); | ||
172 | }; | ||
173 | VLSVariable _doubleArrow_1 = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_5); | ||
174 | _terms.add(_doubleArrow_1); | ||
175 | }; | ||
176 | VLSFunction _doubleArrow_1 = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction_1, _function_4); | ||
177 | it.setOperand(_doubleArrow_1); | ||
178 | }; | ||
179 | VLSUnaryNegation _doubleArrow_1 = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_3); | ||
180 | typeTrace.type2PossibleNot.put(type2, _doubleArrow_1); | ||
181 | } | ||
182 | } | ||
183 | Collection<VLSTerm> _values = typeTrace.type2PossibleNot.values(); | ||
184 | ArrayList<VLSTerm> _arrayList = new ArrayList<VLSTerm>(_values); | ||
185 | typeTrace.type2And.put(type_2, this.support.unfoldAnd(_arrayList)); | ||
186 | typeTrace.type2PossibleNot.clear(); | ||
187 | } | ||
188 | } | ||
189 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | ||
190 | final Procedure1<VLSFofFormula> _function_2 = (VLSFofFormula it) -> { | ||
191 | it.setName("hierarchyHandler"); | ||
192 | it.setFofRole("axiom"); | ||
193 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | ||
194 | final Procedure1<VLSUniversalQuantifier> _function_3 = (VLSUniversalQuantifier it_1) -> { | ||
195 | EList<VLSVariable> _variables = it_1.getVariables(); | ||
196 | VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable(); | ||
197 | final Procedure1<VLSVariable> _function_4 = (VLSVariable it_2) -> { | ||
198 | it_2.setName("A"); | ||
199 | }; | ||
200 | VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_4); | ||
201 | _variables.add(_doubleArrow); | ||
202 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); | ||
203 | final Procedure1<VLSEquivalent> _function_5 = (VLSEquivalent it_2) -> { | ||
204 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
205 | final Procedure1<VLSFunction> _function_6 = (VLSFunction it_3) -> { | ||
206 | it_3.setConstant("Object"); | ||
207 | EList<VLSTerm> _terms = it_3.getTerms(); | ||
208 | VLSVariable _createVLSVariable_2 = this.factory.createVLSVariable(); | ||
209 | final Procedure1<VLSVariable> _function_7 = (VLSVariable it_4) -> { | ||
210 | it_4.setName("A"); | ||
211 | }; | ||
212 | VLSVariable _doubleArrow_1 = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_2, _function_7); | ||
213 | _terms.add(_doubleArrow_1); | ||
214 | }; | ||
215 | VLSFunction _doubleArrow_1 = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_6); | ||
216 | it_2.setLeft(_doubleArrow_1); | ||
217 | Collection<VLSTerm> _values = typeTrace.type2And.values(); | ||
218 | ArrayList<VLSTerm> _arrayList = new ArrayList<VLSTerm>(_values); | ||
219 | it_2.setRight(this.support.unfoldOr(_arrayList)); | ||
220 | }; | ||
221 | VLSEquivalent _doubleArrow_1 = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_5); | ||
222 | it_1.setOperand(_doubleArrow_1); | ||
223 | }; | ||
224 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_3); | ||
225 | it.setFofFormula(_doubleArrow); | ||
226 | }; | ||
227 | final VLSFofFormula hierarch = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_2); | ||
228 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); | ||
229 | _formulas.add(hierarch); | ||
230 | } | ||
231 | |||
232 | public boolean dfsSupertypeCheck(final Type type, final Type type2) { | ||
233 | boolean _xifexpression = false; | ||
234 | boolean _isEmpty = type.getSupertypes().isEmpty(); | ||
235 | if (_isEmpty) { | ||
236 | return false; | ||
237 | } else { | ||
238 | boolean _xifexpression_1 = false; | ||
239 | boolean _contains = type.getSupertypes().contains(type2); | ||
240 | if (_contains) { | ||
241 | return true; | ||
242 | } else { | ||
243 | EList<Type> _supertypes = type.getSupertypes(); | ||
244 | for (final Type supertype : _supertypes) { | ||
245 | boolean _dfsSupertypeCheck = this.dfsSupertypeCheck(supertype, type2); | ||
246 | if (_dfsSupertypeCheck) { | ||
247 | return true; | ||
248 | } | ||
249 | } | ||
250 | } | ||
251 | _xifexpression = _xifexpression_1; | ||
252 | } | ||
253 | return _xifexpression; | ||
254 | } | ||
255 | |||
256 | @Override | ||
257 | public List<VLSTerm> transformTypeReference(final Type referred, final Logic2VampireLanguageMapper mapper, final Logic2VampireLanguageMapperTrace trace) { | ||
258 | throw new UnsupportedOperationException("TODO: auto-generated method stub"); | ||
259 | } | ||
260 | |||
261 | @Override | ||
262 | public VLSTerm getUndefinedSupertype(final Logic2VampireLanguageMapperTrace trace) { | ||
263 | throw new UnsupportedOperationException("TODO: auto-generated method stub"); | ||
264 | } | ||
265 | |||
266 | @Override | ||
267 | public int getUndefinedSupertypeScope(final int undefinedScope, final Logic2VampireLanguageMapperTrace trace) { | ||
268 | throw new UnsupportedOperationException("TODO: auto-generated method stub"); | ||
269 | } | ||
270 | |||
271 | @Override | ||
272 | public VLSTerm transformReference(final DefinedElement referred, final Logic2VampireLanguageMapperTrace trace) { | ||
273 | VLSDoubleQuote _createVLSDoubleQuote = this.factory.createVLSDoubleQuote(); | ||
274 | final Procedure1<VLSDoubleQuote> _function = (VLSDoubleQuote it) -> { | ||
275 | String _name = referred.getName(); | ||
276 | String _plus = ("\"a" + _name); | ||
277 | String _plus_1 = (_plus + "\""); | ||
278 | it.setValue(_plus_1); | ||
279 | }; | ||
280 | return ObjectExtensions.<VLSDoubleQuote>operator_doubleArrow(_createVLSDoubleQuote, _function); | ||
281 | } | ||
282 | |||
283 | @Override | ||
284 | public VampireModelInterpretation_TypeInterpretation getTypeInterpreter() { | ||
285 | throw new UnsupportedOperationException("TODO: auto-generated method stub"); | ||
286 | } | ||
287 | } | ||
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 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; | ||
2 | |||
3 | @SuppressWarnings("all") | ||
4 | public interface VampireModelInterpretation_TypeInterpretation { | ||
5 | } | ||
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 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; | ||
2 | |||
3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireModelInterpretation_TypeInterpretation; | ||
4 | |||
5 | @SuppressWarnings("all") | ||
6 | public class VampireModelInterpretation_TypeInterpretation_FilteredTypes implements VampireModelInterpretation_TypeInterpretation { | ||
7 | } | ||