diff options
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire')
38 files changed, 2113 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..b86e8068 --- /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..8e50f399 --- /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..70f60102 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.gitignore | |||
@@ -0,0 +1,10 @@ | |||
1 | /.VampireSolver.java._trace | ||
2 | /.TypeMappingTechnique.java._trace | ||
3 | /.VampireBackendSolver.java._trace | ||
4 | /.VampireSolverConfiguration.java._trace | ||
5 | /.VampireAnalyzerConfiguration.xtendbin | ||
6 | /.VampireSolver.xtendbin | ||
7 | /TypeMappingTechnique.java | ||
8 | /VampireBackendSolver.java | ||
9 | /VampireSolver.java | ||
10 | /VampireSolverConfiguration.java | ||
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..d9d75887 --- /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,78 @@ | |||
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.Vampire2LogicMapper; | ||
9 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireHandler; | ||
10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage; | ||
11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel; | ||
12 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel; | ||
13 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicModelInterpretation; | ||
14 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner; | ||
15 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException; | ||
16 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration; | ||
17 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput; | ||
18 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem; | ||
19 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult; | ||
20 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult; | ||
21 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace; | ||
22 | import java.util.List; | ||
23 | import org.eclipse.xtend2.lib.StringConcatenation; | ||
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(); | ||
34 | |||
35 | private final Vampire2LogicMapper backwardMapper = new Vampire2LogicMapper(); | ||
36 | |||
37 | private final VampireHandler handler = new VampireHandler(); | ||
38 | |||
39 | private final String fileName = "vampireProblem.tptp"; | ||
40 | |||
41 | @Override | ||
42 | public LogicResult solve(final LogicProblem problem, final LogicSolverConfiguration config, final ReasonerWorkspace workspace) throws LogicReasonerException { | ||
43 | final VampireSolverConfiguration vampireConfig = this.asConfig(config); | ||
44 | final long transformationStart = System.currentTimeMillis(); | ||
45 | final TracedOutput<VampireModel, Logic2VampireLanguageMapperTrace> result = this.forwardMapper.transformProblem(problem, vampireConfig); | ||
46 | final VampireModel vampireProblem = result.getOutput(); | ||
47 | final Logic2VampireLanguageMapperTrace forwardTrace = result.getTrace(); | ||
48 | String fileURI = null; | ||
49 | String vampireCode = null; | ||
50 | vampireCode = workspace.writeModelToString(vampireProblem, this.fileName); | ||
51 | final boolean writeFile = ((vampireConfig.documentationLevel == DocumentationLevel.NORMAL) || | ||
52 | (vampireConfig.documentationLevel == DocumentationLevel.FULL)); | ||
53 | if (writeFile) { | ||
54 | fileURI = workspace.writeModel(vampireProblem, this.fileName).toFileString(); | ||
55 | } | ||
56 | long _currentTimeMillis = System.currentTimeMillis(); | ||
57 | final long transformationTime = (_currentTimeMillis - transformationStart); | ||
58 | return null; | ||
59 | } | ||
60 | |||
61 | public VampireSolverConfiguration asConfig(final LogicSolverConfiguration configuration) { | ||
62 | if ((configuration instanceof VampireSolverConfiguration)) { | ||
63 | return ((VampireSolverConfiguration)configuration); | ||
64 | } else { | ||
65 | StringConcatenation _builder = new StringConcatenation(); | ||
66 | _builder.append("The configuration have to be an "); | ||
67 | String _simpleName = VampireSolverConfiguration.class.getSimpleName(); | ||
68 | _builder.append(_simpleName); | ||
69 | _builder.append("!"); | ||
70 | throw new IllegalArgumentException(_builder.toString()); | ||
71 | } | ||
72 | } | ||
73 | |||
74 | @Override | ||
75 | public List<? extends LogicModelInterpretation> getInterpretations(final ModelResult modelResult) { | ||
76 | return null; | ||
77 | } | ||
78 | } | ||
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..1f6b3d42 --- /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,7 @@ | |||
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 | } | ||
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..99ba52b8 --- /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..0210a300 --- /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..7b01a284 --- /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_ContainmentMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin new file mode 100644 index 00000000..9f455fdd --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.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..0b91349d --- /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_ScopeMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin new file mode 100644 index 00000000..07e249ce --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.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..115249ba --- /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..2e86d0c7 --- /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..e870dabc --- /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..ed198ef6 --- /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/.Vampire2LogicMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin new file mode 100644 index 00000000..cf8e4acd --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.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/.VampireHandler.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin new file mode 100644 index 00000000..07d5b7b4 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.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..983108a2 --- /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..4442cdea --- /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..8a9aa4bb --- /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,42 @@ | |||
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 | ||
12 | /.Logic2VampireLanguageMapper.xtendbin | ||
13 | /.Logic2VampireLanguageMapperTrace.xtendbin | ||
14 | /.Logic2VampireLanguageMapper_ConstantMapper.xtendbin | ||
15 | /.Logic2VampireLanguageMapper_RelationMapper.xtendbin | ||
16 | /.Logic2VampireLanguageMapper_Support.xtendbin | ||
17 | /.Logic2VampireLanguageMapper_TypeMapper.xtendbin | ||
18 | /.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtendbin | ||
19 | /.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtendbin | ||
20 | /.VampireModelInterpretation_TypeInterpretation.xtendbin | ||
21 | /.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin | ||
22 | /Logic2VampireLanguageMapper.java | ||
23 | /Logic2VampireLanguageMapperTrace.java | ||
24 | /Logic2VampireLanguageMapper_ConstantMapper.java | ||
25 | /Logic2VampireLanguageMapper_RelationMapper.java | ||
26 | /Logic2VampireLanguageMapper_Support.java | ||
27 | /Logic2VampireLanguageMapper_TypeMapper.java | ||
28 | /Logic2VampireLanguageMapper_TypeMapperTrace.java | ||
29 | /Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.java | ||
30 | /Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.java | ||
31 | /VampireModelInterpretation_TypeInterpretation.java | ||
32 | /VampireModelInterpretation_TypeInterpretation_FilteredTypes.java | ||
33 | /.Vampire2LogicMapper.java._trace | ||
34 | /.VampireHandler.java._trace | ||
35 | /.MonitoredVampireSolution.java._trace | ||
36 | /.SolverConfiguration.java._trace | ||
37 | /.VampireSolverException.java._trace | ||
38 | /.VampireSolutionModel.java._trace | ||
39 | /.VampireCallerWithTimeout.java._trace | ||
40 | /.Logic2VampireLanguageMapper_ScopeMapper.java._trace | ||
41 | /.Logic2VampireLanguageMapper_Containment.java._trace | ||
42 | /.Logic2VampireLanguageMapper_ContainmentMapper.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..36a727b2 --- /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,454 @@ | |||
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_ContainmentMapper; | ||
7 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_RelationMapper; | ||
8 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_ScopeMapper; | ||
9 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; | ||
10 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapper; | ||
11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSComment; | ||
12 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant; | ||
13 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality; | ||
14 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent; | ||
15 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; | ||
16 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; | ||
17 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies; | ||
18 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSInt; | ||
19 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSReal; | ||
20 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; | ||
21 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUnaryNegation; | ||
22 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; | ||
23 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; | ||
24 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel; | ||
25 | import com.google.common.collect.Iterables; | ||
26 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput; | ||
27 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And; | ||
28 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Assertion; | ||
29 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolLiteral; | ||
30 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference; | ||
31 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference; | ||
32 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration; | ||
33 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDefinition; | ||
34 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement; | ||
35 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Distinct; | ||
36 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Equals; | ||
37 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Exists; | ||
38 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Forall; | ||
39 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration; | ||
40 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDefinition; | ||
41 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Iff; | ||
42 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Impl; | ||
43 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.InstanceOf; | ||
44 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntLiteral; | ||
45 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Not; | ||
46 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Or; | ||
47 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealLiteral; | ||
48 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation; | ||
49 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration; | ||
50 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition; | ||
51 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicDeclaration; | ||
52 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue; | ||
53 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term; | ||
54 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; | ||
55 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference; | ||
56 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable; | ||
57 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem; | ||
58 | import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; | ||
59 | import java.util.Arrays; | ||
60 | import java.util.Collections; | ||
61 | import java.util.HashMap; | ||
62 | import java.util.List; | ||
63 | import java.util.Map; | ||
64 | import java.util.function.Consumer; | ||
65 | import org.eclipse.emf.common.util.EList; | ||
66 | import org.eclipse.xtend.lib.annotations.AccessorType; | ||
67 | import org.eclipse.xtend.lib.annotations.Accessors; | ||
68 | import org.eclipse.xtext.xbase.lib.Extension; | ||
69 | import org.eclipse.xtext.xbase.lib.Functions.Function1; | ||
70 | import org.eclipse.xtext.xbase.lib.IterableExtensions; | ||
71 | import org.eclipse.xtext.xbase.lib.ListExtensions; | ||
72 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; | ||
73 | import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; | ||
74 | import org.eclipse.xtext.xbase.lib.Pure; | ||
75 | |||
76 | @SuppressWarnings("all") | ||
77 | public class Logic2VampireLanguageMapper { | ||
78 | @Extension | ||
79 | private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE; | ||
80 | |||
81 | private final Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support(); | ||
82 | |||
83 | @Accessors(AccessorType.PUBLIC_GETTER) | ||
84 | private final Logic2VampireLanguageMapper_ConstantMapper constantMapper = new Logic2VampireLanguageMapper_ConstantMapper(this); | ||
85 | |||
86 | @Accessors(AccessorType.PUBLIC_GETTER) | ||
87 | private final Logic2VampireLanguageMapper_ContainmentMapper containmentMapper = new Logic2VampireLanguageMapper_ContainmentMapper(this); | ||
88 | |||
89 | @Accessors(AccessorType.PUBLIC_GETTER) | ||
90 | private final Logic2VampireLanguageMapper_RelationMapper relationMapper = new Logic2VampireLanguageMapper_RelationMapper(this); | ||
91 | |||
92 | @Accessors(AccessorType.PUBLIC_GETTER) | ||
93 | private final Logic2VampireLanguageMapper_ScopeMapper scopeMapper = new Logic2VampireLanguageMapper_ScopeMapper(this); | ||
94 | |||
95 | @Accessors(AccessorType.PUBLIC_GETTER) | ||
96 | private final Logic2VampireLanguageMapper_TypeMapper typeMapper = new Logic2VampireLanguageMapper_TypeMapper(this); | ||
97 | |||
98 | public TracedOutput<VampireModel, Logic2VampireLanguageMapperTrace> transformProblem(final LogicProblem problem, final VampireSolverConfiguration config) { | ||
99 | VLSComment _createVLSComment = this.factory.createVLSComment(); | ||
100 | final Procedure1<VLSComment> _function = (VLSComment it) -> { | ||
101 | it.setComment("This is an initial Test Comment"); | ||
102 | }; | ||
103 | final VLSComment initialComment = ObjectExtensions.<VLSComment>operator_doubleArrow(_createVLSComment, _function); | ||
104 | VampireModel _createVampireModel = this.factory.createVampireModel(); | ||
105 | final Procedure1<VampireModel> _function_1 = (VampireModel it) -> { | ||
106 | EList<VLSComment> _comments = it.getComments(); | ||
107 | _comments.add(initialComment); | ||
108 | }; | ||
109 | final VampireModel specification = ObjectExtensions.<VampireModel>operator_doubleArrow(_createVampireModel, _function_1); | ||
110 | Logic2VampireLanguageMapperTrace _logic2VampireLanguageMapperTrace = new Logic2VampireLanguageMapperTrace(); | ||
111 | final Procedure1<Logic2VampireLanguageMapperTrace> _function_2 = (Logic2VampireLanguageMapperTrace it) -> { | ||
112 | it.specification = specification; | ||
113 | }; | ||
114 | final Logic2VampireLanguageMapperTrace trace = ObjectExtensions.<Logic2VampireLanguageMapperTrace>operator_doubleArrow(_logic2VampireLanguageMapperTrace, _function_2); | ||
115 | boolean _isEmpty = problem.getTypes().isEmpty(); | ||
116 | boolean _not = (!_isEmpty); | ||
117 | if (_not) { | ||
118 | this.typeMapper.transformTypes(problem.getTypes(), problem.getElements(), this, trace); | ||
119 | } | ||
120 | this.scopeMapper.transformScope(config, trace); | ||
121 | trace.relationDefinitions = this.collectRelationDefinitions(problem); | ||
122 | final Consumer<Relation> _function_3 = (Relation it) -> { | ||
123 | this.relationMapper.transformRelation(it, trace); | ||
124 | }; | ||
125 | problem.getRelations().forEach(_function_3); | ||
126 | this.containmentMapper.transformContainment(problem.getContainmentHierarchies(), trace); | ||
127 | trace.constantDefinitions = this.collectConstantDefinitions(problem); | ||
128 | final Consumer<ConstantDefinition> _function_4 = (ConstantDefinition it) -> { | ||
129 | this.constantMapper.transformConstantDefinitionSpecification(it, trace); | ||
130 | }; | ||
131 | Iterables.<ConstantDefinition>filter(problem.getConstants(), ConstantDefinition.class).forEach(_function_4); | ||
132 | EList<Assertion> _assertions = problem.getAssertions(); | ||
133 | for (final Assertion assertion : _assertions) { | ||
134 | this.transformAssertion(assertion, trace); | ||
135 | } | ||
136 | return new TracedOutput<VampireModel, Logic2VampireLanguageMapperTrace>(specification, trace); | ||
137 | } | ||
138 | |||
139 | protected VLSTerm _transformTypeReference(final BoolTypeReference boolTypeReference, final Logic2VampireLanguageMapperTrace trace) { | ||
140 | return null; | ||
141 | } | ||
142 | |||
143 | private HashMap<ConstantDeclaration, ConstantDefinition> collectConstantDefinitions(final LogicProblem problem) { | ||
144 | final HashMap<ConstantDeclaration, ConstantDefinition> res = new HashMap<ConstantDeclaration, ConstantDefinition>(); | ||
145 | final Function1<ConstantDefinition, Boolean> _function = (ConstantDefinition it) -> { | ||
146 | ConstantDeclaration _defines = it.getDefines(); | ||
147 | return Boolean.valueOf((_defines != null)); | ||
148 | }; | ||
149 | final Consumer<ConstantDefinition> _function_1 = (ConstantDefinition it) -> { | ||
150 | res.put(it.getDefines(), it); | ||
151 | }; | ||
152 | IterableExtensions.<ConstantDefinition>filter(Iterables.<ConstantDefinition>filter(problem.getConstants(), ConstantDefinition.class), _function).forEach(_function_1); | ||
153 | return res; | ||
154 | } | ||
155 | |||
156 | private HashMap<RelationDeclaration, RelationDefinition> collectRelationDefinitions(final LogicProblem problem) { | ||
157 | final HashMap<RelationDeclaration, RelationDefinition> res = new HashMap<RelationDeclaration, RelationDefinition>(); | ||
158 | final Function1<RelationDefinition, Boolean> _function = (RelationDefinition it) -> { | ||
159 | RelationDeclaration _defines = it.getDefines(); | ||
160 | return Boolean.valueOf((_defines != null)); | ||
161 | }; | ||
162 | final Consumer<RelationDefinition> _function_1 = (RelationDefinition it) -> { | ||
163 | res.put(it.getDefines(), it); | ||
164 | }; | ||
165 | IterableExtensions.<RelationDefinition>filter(Iterables.<RelationDefinition>filter(problem.getRelations(), RelationDefinition.class), _function).forEach(_function_1); | ||
166 | return res; | ||
167 | } | ||
168 | |||
169 | protected boolean transformAssertion(final Assertion assertion, final Logic2VampireLanguageMapperTrace trace) { | ||
170 | boolean _xblockexpression = false; | ||
171 | { | ||
172 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | ||
173 | final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> { | ||
174 | it.setName(this.support.toID(assertion.getName())); | ||
175 | it.setFofRole("axiom"); | ||
176 | it.setFofFormula(this.transformTerm(assertion.getValue(), trace, Collections.EMPTY_MAP)); | ||
177 | }; | ||
178 | final VLSFofFormula res = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function); | ||
179 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); | ||
180 | _xblockexpression = _formulas.add(res); | ||
181 | } | ||
182 | return _xblockexpression; | ||
183 | } | ||
184 | |||
185 | protected VLSTerm _transformTerm(final BoolLiteral literal, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
186 | VLSTerm _xifexpression = null; | ||
187 | boolean _isValue = literal.isValue(); | ||
188 | boolean _equals = (_isValue == true); | ||
189 | if (_equals) { | ||
190 | _xifexpression = this.factory.createVLSTrue(); | ||
191 | } else { | ||
192 | _xifexpression = this.factory.createVLSFalse(); | ||
193 | } | ||
194 | return _xifexpression; | ||
195 | } | ||
196 | |||
197 | protected VLSTerm _transformTerm(final IntLiteral literal, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
198 | VLSInt _createVLSInt = this.factory.createVLSInt(); | ||
199 | final Procedure1<VLSInt> _function = (VLSInt it) -> { | ||
200 | it.setValue(Integer.valueOf(literal.getValue()).toString()); | ||
201 | }; | ||
202 | return ObjectExtensions.<VLSInt>operator_doubleArrow(_createVLSInt, _function); | ||
203 | } | ||
204 | |||
205 | protected VLSTerm _transformTerm(final RealLiteral literal, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
206 | VLSReal _createVLSReal = this.factory.createVLSReal(); | ||
207 | final Procedure1<VLSReal> _function = (VLSReal it) -> { | ||
208 | it.setValue(literal.getValue().toString()); | ||
209 | }; | ||
210 | return ObjectExtensions.<VLSReal>operator_doubleArrow(_createVLSReal, _function); | ||
211 | } | ||
212 | |||
213 | protected VLSTerm _transformTerm(final Not not, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
214 | VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); | ||
215 | final Procedure1<VLSUnaryNegation> _function = (VLSUnaryNegation it) -> { | ||
216 | it.setOperand(this.transformTerm(not.getOperand(), trace, variables)); | ||
217 | }; | ||
218 | return ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function); | ||
219 | } | ||
220 | |||
221 | protected VLSTerm _transformTerm(final And and, 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.unfoldAnd(ListExtensions.<Term, VLSTerm>map(and.getOperands(), _function)); | ||
226 | } | ||
227 | |||
228 | protected VLSTerm _transformTerm(final Or or, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
229 | final Function1<Term, VLSTerm> _function = (Term it) -> { | ||
230 | return this.transformTerm(it, trace, variables); | ||
231 | }; | ||
232 | return this.support.unfoldOr(ListExtensions.<Term, VLSTerm>map(or.getOperands(), _function)); | ||
233 | } | ||
234 | |||
235 | protected VLSTerm _transformTerm(final Impl impl, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
236 | VLSImplies _createVLSImplies = this.factory.createVLSImplies(); | ||
237 | final Procedure1<VLSImplies> _function = (VLSImplies it) -> { | ||
238 | it.setLeft(this.transformTerm(impl.getLeftOperand(), trace, variables)); | ||
239 | it.setRight(this.transformTerm(impl.getRightOperand(), trace, variables)); | ||
240 | }; | ||
241 | return ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function); | ||
242 | } | ||
243 | |||
244 | protected VLSTerm _transformTerm(final Iff iff, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
245 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); | ||
246 | final Procedure1<VLSEquivalent> _function = (VLSEquivalent it) -> { | ||
247 | it.setLeft(this.transformTerm(iff.getLeftOperand(), trace, variables)); | ||
248 | it.setRight(this.transformTerm(iff.getRightOperand(), trace, variables)); | ||
249 | }; | ||
250 | return ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function); | ||
251 | } | ||
252 | |||
253 | protected VLSTerm _transformTerm(final Equals equals, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
254 | VLSEquality _createVLSEquality = this.factory.createVLSEquality(); | ||
255 | final Procedure1<VLSEquality> _function = (VLSEquality it) -> { | ||
256 | it.setLeft(this.transformTerm(equals.getLeftOperand(), trace, variables)); | ||
257 | it.setRight(this.transformTerm(equals.getRightOperand(), trace, variables)); | ||
258 | }; | ||
259 | return ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function); | ||
260 | } | ||
261 | |||
262 | protected VLSTerm _transformTerm(final Distinct distinct, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
263 | return this.support.unfoldDistinctTerms(this, distinct.getOperands(), trace, variables); | ||
264 | } | ||
265 | |||
266 | protected VLSTerm _transformTerm(final Forall forall, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
267 | return this.support.createQuantifiedExpression(this, forall, trace, variables, true); | ||
268 | } | ||
269 | |||
270 | protected VLSTerm _transformTerm(final Exists exists, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
271 | return this.support.createQuantifiedExpression(this, exists, trace, variables, false); | ||
272 | } | ||
273 | |||
274 | protected VLSTerm _transformTerm(final InstanceOf instanceOf, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
275 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
276 | final Procedure1<VLSFunction> _function = (VLSFunction it) -> { | ||
277 | TypeReference _range = instanceOf.getRange(); | ||
278 | it.setConstant(CollectionsUtil.<Type, VLSFunction>lookup(((ComplexTypeReference) _range).getReferred(), trace.type2Predicate).getConstant()); | ||
279 | EList<VLSTerm> _terms = it.getTerms(); | ||
280 | VLSTerm _transformTerm = this.transformTerm(instanceOf.getValue(), trace, variables); | ||
281 | _terms.add(_transformTerm); | ||
282 | }; | ||
283 | return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function); | ||
284 | } | ||
285 | |||
286 | protected VLSTerm _transformTerm(final SymbolicValue symbolicValue, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
287 | return this.transformSymbolicReference(symbolicValue.getSymbolicReference(), symbolicValue.getParameterSubstitutions(), trace, variables); | ||
288 | } | ||
289 | |||
290 | protected VLSTerm _transformSymbolicReference(final DefinedElement referred, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
291 | return this.typeMapper.transformReference(referred, trace); | ||
292 | } | ||
293 | |||
294 | protected VLSTerm _transformSymbolicReference(final ConstantDeclaration constant, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
295 | VLSConstant _createVLSConstant = this.factory.createVLSConstant(); | ||
296 | final Procedure1<VLSConstant> _function = (VLSConstant it) -> { | ||
297 | it.setName(this.support.toID(constant.getName())); | ||
298 | }; | ||
299 | final VLSConstant res = ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _function); | ||
300 | return res; | ||
301 | } | ||
302 | |||
303 | protected VLSTerm _transformSymbolicReference(final ConstantDefinition constant, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
304 | return null; | ||
305 | } | ||
306 | |||
307 | protected VLSTerm _transformSymbolicReference(final Variable variable, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
308 | return this.support.duplicate(CollectionsUtil.<Variable, VLSVariable>lookup(variable, variables)); | ||
309 | } | ||
310 | |||
311 | protected VLSTerm _transformSymbolicReference(final FunctionDeclaration function, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
312 | return null; | ||
313 | } | ||
314 | |||
315 | protected VLSTerm _transformSymbolicReference(final FunctionDefinition function, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
316 | return null; | ||
317 | } | ||
318 | |||
319 | /** | ||
320 | * def dispatch protected VLSTerm transformSymbolicReference(Relation relation, | ||
321 | * List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace, | ||
322 | * Map<Variable, VLSVariable> variables) { | ||
323 | * if (trace.relationDefinitions.containsKey(relation)) { | ||
324 | * this.transformSymbolicReference(relation.lookup(trace.relationDefinitions), | ||
325 | * parameterSubstitutions, trace, variables) | ||
326 | * } | ||
327 | * else { | ||
328 | * // if (relationMapper.transformToHostedField(relation, trace)) { | ||
329 | * // val VLSRelation = relation.lookup(trace.relationDeclaration2Field) | ||
330 | * // // R(a,b) => | ||
331 | * // // b in a.R | ||
332 | * // return createVLSSubset => [ | ||
333 | * // it.leftOperand = parameterSubstitutions.get(1).transformTerm(trace, variables) | ||
334 | * // it.rightOperand = createVLSJoin => [ | ||
335 | * // it.leftOperand = parameterSubstitutions.get(0).transformTerm(trace, variables) | ||
336 | * // it.rightOperand = createVLSReference => [it.referred = VLSRelation] | ||
337 | * // ] | ||
338 | * // ] | ||
339 | * // } else { | ||
340 | * // val target = createVLSJoin => [ | ||
341 | * // leftOperand = createVLSReference => [referred = trace.logicLanguage] | ||
342 | * // rightOperand = createVLSReference => [ | ||
343 | * // referred = relation.lookup(trace.relationDeclaration2Global) | ||
344 | * // ] | ||
345 | * // ] | ||
346 | * // val source = support.unfoldTermDirectProduct(this, parameterSubstitutions, trace, variables) | ||
347 | * // | ||
348 | * // return createVLSSubset => [ | ||
349 | * // leftOperand = source | ||
350 | * // rightOperand = target | ||
351 | * // ] | ||
352 | * // } | ||
353 | * } | ||
354 | * } | ||
355 | */ | ||
356 | protected VLSTerm _transformSymbolicReference(final Relation relation, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
357 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
358 | final Procedure1<VLSFunction> _function = (VLSFunction it) -> { | ||
359 | it.setConstant(CollectionsUtil.<RelationDeclaration, VLSFunction>lookup(((RelationDeclaration) relation), trace.rel2Predicate).getConstant()); | ||
360 | EList<VLSTerm> _terms = it.getTerms(); | ||
361 | final Function1<Term, VLSTerm> _function_1 = (Term p) -> { | ||
362 | return this.transformTerm(p, trace, variables); | ||
363 | }; | ||
364 | List<VLSTerm> _map = ListExtensions.<Term, VLSTerm>map(parameterSubstitutions, _function_1); | ||
365 | Iterables.<VLSTerm>addAll(_terms, _map); | ||
366 | }; | ||
367 | return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function); | ||
368 | } | ||
369 | |||
370 | protected VLSTerm transformTypeReference(final BoolTypeReference boolTypeReference, final Logic2VampireLanguageMapperTrace trace) { | ||
371 | return _transformTypeReference(boolTypeReference, trace); | ||
372 | } | ||
373 | |||
374 | protected VLSTerm transformTerm(final Term and, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
375 | if (and instanceof And) { | ||
376 | return _transformTerm((And)and, trace, variables); | ||
377 | } else if (and instanceof BoolLiteral) { | ||
378 | return _transformTerm((BoolLiteral)and, trace, variables); | ||
379 | } else if (and instanceof Distinct) { | ||
380 | return _transformTerm((Distinct)and, trace, variables); | ||
381 | } else if (and instanceof Equals) { | ||
382 | return _transformTerm((Equals)and, trace, variables); | ||
383 | } else if (and instanceof Exists) { | ||
384 | return _transformTerm((Exists)and, trace, variables); | ||
385 | } else if (and instanceof Forall) { | ||
386 | return _transformTerm((Forall)and, trace, variables); | ||
387 | } else if (and instanceof Iff) { | ||
388 | return _transformTerm((Iff)and, trace, variables); | ||
389 | } else if (and instanceof Impl) { | ||
390 | return _transformTerm((Impl)and, trace, variables); | ||
391 | } else if (and instanceof IntLiteral) { | ||
392 | return _transformTerm((IntLiteral)and, trace, variables); | ||
393 | } else if (and instanceof Not) { | ||
394 | return _transformTerm((Not)and, trace, variables); | ||
395 | } else if (and instanceof Or) { | ||
396 | return _transformTerm((Or)and, trace, variables); | ||
397 | } else if (and instanceof RealLiteral) { | ||
398 | return _transformTerm((RealLiteral)and, trace, variables); | ||
399 | } else if (and instanceof InstanceOf) { | ||
400 | return _transformTerm((InstanceOf)and, trace, variables); | ||
401 | } else if (and instanceof SymbolicValue) { | ||
402 | return _transformTerm((SymbolicValue)and, trace, variables); | ||
403 | } else { | ||
404 | throw new IllegalArgumentException("Unhandled parameter types: " + | ||
405 | Arrays.<Object>asList(and, trace, variables).toString()); | ||
406 | } | ||
407 | } | ||
408 | |||
409 | protected VLSTerm transformSymbolicReference(final SymbolicDeclaration constant, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
410 | if (constant instanceof ConstantDeclaration) { | ||
411 | return _transformSymbolicReference((ConstantDeclaration)constant, parameterSubstitutions, trace, variables); | ||
412 | } else if (constant instanceof ConstantDefinition) { | ||
413 | return _transformSymbolicReference((ConstantDefinition)constant, parameterSubstitutions, trace, variables); | ||
414 | } else if (constant instanceof FunctionDeclaration) { | ||
415 | return _transformSymbolicReference((FunctionDeclaration)constant, parameterSubstitutions, trace, variables); | ||
416 | } else if (constant instanceof FunctionDefinition) { | ||
417 | return _transformSymbolicReference((FunctionDefinition)constant, parameterSubstitutions, trace, variables); | ||
418 | } else if (constant instanceof DefinedElement) { | ||
419 | return _transformSymbolicReference((DefinedElement)constant, parameterSubstitutions, trace, variables); | ||
420 | } else if (constant instanceof Relation) { | ||
421 | return _transformSymbolicReference((Relation)constant, parameterSubstitutions, trace, variables); | ||
422 | } else if (constant instanceof Variable) { | ||
423 | return _transformSymbolicReference((Variable)constant, parameterSubstitutions, trace, variables); | ||
424 | } else { | ||
425 | throw new IllegalArgumentException("Unhandled parameter types: " + | ||
426 | Arrays.<Object>asList(constant, parameterSubstitutions, trace, variables).toString()); | ||
427 | } | ||
428 | } | ||
429 | |||
430 | @Pure | ||
431 | public Logic2VampireLanguageMapper_ConstantMapper getConstantMapper() { | ||
432 | return this.constantMapper; | ||
433 | } | ||
434 | |||
435 | @Pure | ||
436 | public Logic2VampireLanguageMapper_ContainmentMapper getContainmentMapper() { | ||
437 | return this.containmentMapper; | ||
438 | } | ||
439 | |||
440 | @Pure | ||
441 | public Logic2VampireLanguageMapper_RelationMapper getRelationMapper() { | ||
442 | return this.relationMapper; | ||
443 | } | ||
444 | |||
445 | @Pure | ||
446 | public Logic2VampireLanguageMapper_ScopeMapper getScopeMapper() { | ||
447 | return this.scopeMapper; | ||
448 | } | ||
449 | |||
450 | @Pure | ||
451 | public Logic2VampireLanguageMapper_TypeMapper getTypeMapper() { | ||
452 | return this.typeMapper; | ||
453 | } | ||
454 | } | ||
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..24df5fcd --- /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,51 @@ | |||
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.VLSConstant; | ||
5 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; | ||
6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; | ||
7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; | ||
8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; | ||
9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel; | ||
10 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration; | ||
11 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDefinition; | ||
12 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement; | ||
13 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration; | ||
14 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition; | ||
15 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; | ||
16 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable; | ||
17 | import java.util.HashMap; | ||
18 | import java.util.List; | ||
19 | import java.util.Map; | ||
20 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; | ||
21 | |||
22 | @SuppressWarnings("all") | ||
23 | public class Logic2VampireLanguageMapperTrace { | ||
24 | public VampireModel specification; | ||
25 | |||
26 | public VLSFofFormula logicLanguageBody; | ||
27 | |||
28 | public VLSTerm formula; | ||
29 | |||
30 | public Logic2VampireLanguageMapper_TypeMapperTrace typeMapperTrace; | ||
31 | |||
32 | public final Map<Type, VLSFunction> type2Predicate = new HashMap<Type, VLSFunction>(); | ||
33 | |||
34 | public final Map<DefinedElement, VLSFunction> element2Predicate = new HashMap<DefinedElement, VLSFunction>(); | ||
35 | |||
36 | public final Map<Type, VLSTerm> type2PossibleNot = new HashMap<Type, VLSTerm>(); | ||
37 | |||
38 | public final Map<Type, VLSTerm> type2And = new HashMap<Type, VLSTerm>(); | ||
39 | |||
40 | public final List<VLSConstant> uniqueInstances = CollectionLiterals.<VLSConstant>newArrayList(); | ||
41 | |||
42 | public Map<ConstantDeclaration, ConstantDefinition> constantDefinitions; | ||
43 | |||
44 | public Map<RelationDeclaration, RelationDefinition> relationDefinitions; | ||
45 | |||
46 | public Map<RelationDeclaration, VLSFunction> rel2Predicate = new HashMap<RelationDeclaration, VLSFunction>(); | ||
47 | |||
48 | public final Map<Variable, VLSVariable> relationVar2VLS = new HashMap<Variable, VLSVariable>(); | ||
49 | |||
50 | public final Map<Variable, VLSFunction> relationVar2TypeDec = new HashMap<Variable, VLSFunction>(); | ||
51 | } | ||
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_ContainmentMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java new file mode 100644 index 00000000..da0e5615 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java | |||
@@ -0,0 +1,180 @@ | |||
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.VLSAnd; | ||
7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant; | ||
8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality; | ||
9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent; | ||
10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSExistentialQuantifier; | ||
11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; | ||
12 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; | ||
13 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies; | ||
14 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; | ||
15 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; | ||
16 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; | ||
17 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference; | ||
18 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation; | ||
19 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration; | ||
20 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; | ||
21 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference; | ||
22 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy; | ||
23 | import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; | ||
24 | import java.util.ArrayList; | ||
25 | import java.util.List; | ||
26 | import org.eclipse.emf.common.util.EList; | ||
27 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; | ||
28 | import org.eclipse.xtext.xbase.lib.Extension; | ||
29 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; | ||
30 | import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; | ||
31 | |||
32 | @SuppressWarnings("all") | ||
33 | public class Logic2VampireLanguageMapper_ContainmentMapper { | ||
34 | @Extension | ||
35 | private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE; | ||
36 | |||
37 | private final Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support(); | ||
38 | |||
39 | private final Logic2VampireLanguageMapper base; | ||
40 | |||
41 | private final VLSVariable variable = ObjectExtensions.<VLSVariable>operator_doubleArrow(this.factory.createVLSVariable(), ((Procedure1<VLSVariable>) (VLSVariable it) -> { | ||
42 | it.setName("A"); | ||
43 | })); | ||
44 | |||
45 | public Logic2VampireLanguageMapper_ContainmentMapper(final Logic2VampireLanguageMapper base) { | ||
46 | this.base = base; | ||
47 | } | ||
48 | |||
49 | public void transformContainment(final List<ContainmentHierarchy> hierarchies, final Logic2VampireLanguageMapperTrace trace) { | ||
50 | final ContainmentHierarchy hierarchy = hierarchies.get(0); | ||
51 | final EList<Type> containmentListCopy = hierarchy.getTypesOrderedInHierarchy(); | ||
52 | final EList<Relation> relationsList = hierarchy.getContainmentRelations(); | ||
53 | for (final Relation l : relationsList) { | ||
54 | { | ||
55 | TypeReference _get = l.getParameters().get(1); | ||
56 | Type _referred = ((ComplexTypeReference) _get).getReferred(); | ||
57 | Type pointingTo = ((Type) _referred); | ||
58 | containmentListCopy.remove(pointingTo); | ||
59 | EList<Type> _subtypes = pointingTo.getSubtypes(); | ||
60 | for (final Type c : _subtypes) { | ||
61 | containmentListCopy.remove(c); | ||
62 | } | ||
63 | } | ||
64 | } | ||
65 | final String topName = CollectionsUtil.<Type, VLSFunction>lookup(containmentListCopy.get(0), trace.type2Predicate).getConstant().toString(); | ||
66 | final VLSFunction topTerm = this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(containmentListCopy.get(0), trace.type2Predicate)); | ||
67 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | ||
68 | final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> { | ||
69 | it.setName(this.support.toIDMultiple("containment_topLevel", topName)); | ||
70 | it.setFofRole("axiom"); | ||
71 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | ||
72 | final Procedure1<VLSUniversalQuantifier> _function_1 = (VLSUniversalQuantifier it_1) -> { | ||
73 | EList<VLSVariable> _variables = it_1.getVariables(); | ||
74 | VLSVariable _duplicate = this.support.duplicate(this.variable); | ||
75 | _variables.add(_duplicate); | ||
76 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); | ||
77 | final Procedure1<VLSEquivalent> _function_2 = (VLSEquivalent it_2) -> { | ||
78 | it_2.setLeft(topTerm); | ||
79 | VLSEquality _createVLSEquality = this.factory.createVLSEquality(); | ||
80 | final Procedure1<VLSEquality> _function_3 = (VLSEquality it_3) -> { | ||
81 | it_3.setLeft(this.support.duplicate(this.variable)); | ||
82 | VLSConstant _createVLSConstant = this.factory.createVLSConstant(); | ||
83 | final Procedure1<VLSConstant> _function_4 = (VLSConstant it_4) -> { | ||
84 | it_4.setName("o1"); | ||
85 | }; | ||
86 | VLSConstant _doubleArrow = ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _function_4); | ||
87 | it_3.setRight(_doubleArrow); | ||
88 | }; | ||
89 | VLSEquality _doubleArrow = ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_3); | ||
90 | it_2.setRight(_doubleArrow); | ||
91 | }; | ||
92 | VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_2); | ||
93 | it_1.setOperand(_doubleArrow); | ||
94 | }; | ||
95 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_1); | ||
96 | it.setFofFormula(_doubleArrow); | ||
97 | }; | ||
98 | final VLSFofFormula contTop = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function); | ||
99 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); | ||
100 | _formulas.add(contTop); | ||
101 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
102 | final Procedure1<VLSVariable> _function_1 = (VLSVariable it) -> { | ||
103 | it.setName("A"); | ||
104 | }; | ||
105 | final VLSVariable varA = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_1); | ||
106 | VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable(); | ||
107 | final Procedure1<VLSVariable> _function_2 = (VLSVariable it) -> { | ||
108 | it.setName("B"); | ||
109 | }; | ||
110 | final VLSVariable varB = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_2); | ||
111 | final ArrayList<VLSVariable> varList = CollectionLiterals.<VLSVariable>newArrayList(varB, varA); | ||
112 | for (final Relation l_1 : relationsList) { | ||
113 | { | ||
114 | final String relName = CollectionsUtil.<RelationDeclaration, VLSFunction>lookup(((RelationDeclaration) l_1), trace.rel2Predicate).getConstant().toString(); | ||
115 | TypeReference _get = l_1.getParameters().get(0); | ||
116 | Type _referred = ((ComplexTypeReference) _get).getReferred(); | ||
117 | final Type fromType = ((Type) _referred); | ||
118 | TypeReference _get_1 = l_1.getParameters().get(1); | ||
119 | Type _referred_1 = ((ComplexTypeReference) _get_1).getReferred(); | ||
120 | final Type toType = ((Type) _referred_1); | ||
121 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); | ||
122 | final Procedure1<VLSFofFormula> _function_3 = (VLSFofFormula it) -> { | ||
123 | it.setName(this.support.toIDMultiple("containment", relName)); | ||
124 | it.setFofRole("axiom"); | ||
125 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | ||
126 | final Procedure1<VLSUniversalQuantifier> _function_4 = (VLSUniversalQuantifier it_1) -> { | ||
127 | EList<VLSVariable> _variables = it_1.getVariables(); | ||
128 | VLSVariable _duplicate = this.support.duplicate(varA); | ||
129 | _variables.add(_duplicate); | ||
130 | VLSImplies _createVLSImplies = this.factory.createVLSImplies(); | ||
131 | final Procedure1<VLSImplies> _function_5 = (VLSImplies it_2) -> { | ||
132 | it_2.setLeft(this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(toType, trace.type2Predicate), varA)); | ||
133 | VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier(); | ||
134 | final Procedure1<VLSExistentialQuantifier> _function_6 = (VLSExistentialQuantifier it_3) -> { | ||
135 | EList<VLSVariable> _variables_1 = it_3.getVariables(); | ||
136 | VLSVariable _duplicate_1 = this.support.duplicate(varB); | ||
137 | _variables_1.add(_duplicate_1); | ||
138 | VLSAnd _createVLSAnd = this.factory.createVLSAnd(); | ||
139 | final Procedure1<VLSAnd> _function_7 = (VLSAnd it_4) -> { | ||
140 | it_4.setLeft(this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(fromType, trace.type2Predicate), varB)); | ||
141 | it_4.setRight(this.support.duplicate(CollectionsUtil.<RelationDeclaration, VLSFunction>lookup(((RelationDeclaration) l_1), trace.rel2Predicate), varList)); | ||
142 | }; | ||
143 | VLSAnd _doubleArrow = ObjectExtensions.<VLSAnd>operator_doubleArrow(_createVLSAnd, _function_7); | ||
144 | it_3.setOperand(_doubleArrow); | ||
145 | }; | ||
146 | VLSExistentialQuantifier _doubleArrow = ObjectExtensions.<VLSExistentialQuantifier>operator_doubleArrow(_createVLSExistentialQuantifier, _function_6); | ||
147 | it_2.setRight(_doubleArrow); | ||
148 | VLSEquality _createVLSEquality = this.factory.createVLSEquality(); | ||
149 | final Procedure1<VLSEquality> _function_7 = (VLSEquality it_3) -> { | ||
150 | it_3.setLeft(this.support.duplicate(this.variable)); | ||
151 | VLSConstant _createVLSConstant = this.factory.createVLSConstant(); | ||
152 | final Procedure1<VLSConstant> _function_8 = (VLSConstant it_4) -> { | ||
153 | it_4.setName("o1"); | ||
154 | }; | ||
155 | VLSConstant _doubleArrow_1 = ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _function_8); | ||
156 | it_3.setRight(_doubleArrow_1); | ||
157 | }; | ||
158 | ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_7); | ||
159 | }; | ||
160 | VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_5); | ||
161 | it_1.setOperand(_doubleArrow); | ||
162 | }; | ||
163 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_4); | ||
164 | it.setFofFormula(_doubleArrow); | ||
165 | }; | ||
166 | final VLSFofFormula relFormula = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_3); | ||
167 | EList<VLSFofFormula> _formulas_1 = trace.specification.getFormulas(); | ||
168 | _formulas_1.add(relFormula); | ||
169 | TypeReference _get_2 = l_1.getParameters().get(1); | ||
170 | Type _referred_2 = ((ComplexTypeReference) _get_2).getReferred(); | ||
171 | Type pointingTo = ((Type) _referred_2); | ||
172 | containmentListCopy.remove(pointingTo); | ||
173 | EList<Type> _subtypes = pointingTo.getSubtypes(); | ||
174 | for (final Type c : _subtypes) { | ||
175 | containmentListCopy.remove(c); | ||
176 | } | ||
177 | } | ||
178 | } | ||
179 | } | ||
180 | } | ||
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..d5745333 --- /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,260 @@ | |||
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.Type; | ||
19 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference; | ||
20 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable; | ||
21 | import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; | ||
22 | import java.util.ArrayList; | ||
23 | import java.util.Arrays; | ||
24 | import java.util.Collection; | ||
25 | import java.util.HashMap; | ||
26 | import java.util.List; | ||
27 | import java.util.Map; | ||
28 | import org.eclipse.emf.common.util.EList; | ||
29 | import org.eclipse.xtext.xbase.lib.Conversions; | ||
30 | import org.eclipse.xtext.xbase.lib.ExclusiveRange; | ||
31 | import org.eclipse.xtext.xbase.lib.Extension; | ||
32 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; | ||
33 | import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; | ||
34 | |||
35 | @SuppressWarnings("all") | ||
36 | public class Logic2VampireLanguageMapper_RelationMapper { | ||
37 | @Extension | ||
38 | private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE; | ||
39 | |||
40 | private final Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support(); | ||
41 | |||
42 | private final Logic2VampireLanguageMapper base; | ||
43 | |||
44 | public Logic2VampireLanguageMapper_RelationMapper(final Logic2VampireLanguageMapper base) { | ||
45 | this.base = base; | ||
46 | } | ||
47 | |||
48 | public void _transformRelation(final RelationDeclaration r, final Logic2VampireLanguageMapperTrace trace) { | ||
49 | final List<VLSVariable> relVar2VLS = new ArrayList<VLSVariable>(); | ||
50 | final List<VLSFunction> relVar2TypeDecComply = new ArrayList<VLSFunction>(); | ||
51 | int _length = ((Object[])Conversions.unwrapArray(r.getParameters(), Object.class)).length; | ||
52 | ExclusiveRange _doubleDotLessThan = new ExclusiveRange(0, _length, true); | ||
53 | for (final Integer i : _doubleDotLessThan) { | ||
54 | { | ||
55 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
56 | final Procedure1<VLSVariable> _function = (VLSVariable it) -> { | ||
57 | it.setName(this.support.toIDMultiple("V", i.toString())); | ||
58 | }; | ||
59 | final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function); | ||
60 | relVar2VLS.add(v); | ||
61 | TypeReference _get = r.getParameters().get((i).intValue()); | ||
62 | final Type relType = ((ComplexTypeReference) _get).getReferred(); | ||
63 | final VLSFunction varTypeComply = this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(relType, trace.type2Predicate), v); | ||
64 | relVar2TypeDecComply.add(varTypeComply); | ||
65 | } | ||
66 | } | ||
67 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | ||
68 | final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> { | ||
69 | final String[] nameArray = r.getName().split(" "); | ||
70 | it.setName(this.support.toIDMultiple("compliance", nameArray[0], nameArray[2])); | ||
71 | it.setFofRole("axiom"); | ||
72 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | ||
73 | final Procedure1<VLSUniversalQuantifier> _function_1 = (VLSUniversalQuantifier it_1) -> { | ||
74 | for (final VLSVariable v : relVar2VLS) { | ||
75 | EList<VLSVariable> _variables = it_1.getVariables(); | ||
76 | VLSVariable _duplicate = this.support.duplicate(v); | ||
77 | _variables.add(_duplicate); | ||
78 | } | ||
79 | VLSImplies _createVLSImplies = this.factory.createVLSImplies(); | ||
80 | final Procedure1<VLSImplies> _function_2 = (VLSImplies it_2) -> { | ||
81 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
82 | final Procedure1<VLSFunction> _function_3 = (VLSFunction it_3) -> { | ||
83 | it_3.setConstant(this.support.toIDMultiple("r", nameArray[0], nameArray[2])); | ||
84 | for (final VLSVariable v_1 : relVar2VLS) { | ||
85 | EList<VLSTerm> _terms = it_3.getTerms(); | ||
86 | VLSVariable _duplicate_1 = this.support.duplicate(v_1); | ||
87 | _terms.add(_duplicate_1); | ||
88 | } | ||
89 | }; | ||
90 | final VLSFunction rel = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_3); | ||
91 | trace.rel2Predicate.put(r, rel); | ||
92 | it_2.setLeft(this.support.duplicate(rel)); | ||
93 | it_2.setRight(this.support.unfoldAnd(relVar2TypeDecComply)); | ||
94 | }; | ||
95 | VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_2); | ||
96 | it_1.setOperand(_doubleArrow); | ||
97 | }; | ||
98 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_1); | ||
99 | it.setFofFormula(_doubleArrow); | ||
100 | }; | ||
101 | final VLSFofFormula comply = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function); | ||
102 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); | ||
103 | _formulas.add(comply); | ||
104 | } | ||
105 | |||
106 | public void _transformRelation(final RelationDefinition reldef, final Logic2VampireLanguageMapperTrace trace) { | ||
107 | final Map<Variable, VLSVariable> relationVar2VLS = new HashMap<Variable, VLSVariable>(); | ||
108 | final Map<Variable, VLSFunction> relationVar2TypeDecComply = new HashMap<Variable, VLSFunction>(); | ||
109 | final Map<Variable, VLSFunction> relationVar2TypeDecRes = new HashMap<Variable, VLSFunction>(); | ||
110 | final ArrayList<VLSTerm> typedefs = new ArrayList<VLSTerm>(); | ||
111 | EList<Variable> _variables = reldef.getVariables(); | ||
112 | for (final Variable variable : _variables) { | ||
113 | { | ||
114 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
115 | final Procedure1<VLSVariable> _function = (VLSVariable it) -> { | ||
116 | it.setName(this.support.toIDMultiple("V", variable.getName())); | ||
117 | }; | ||
118 | final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function); | ||
119 | relationVar2VLS.put(variable, v); | ||
120 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
121 | final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> { | ||
122 | TypeReference _range = variable.getRange(); | ||
123 | it.setConstant(this.support.toIDMultiple("t", ((ComplexTypeReference) _range).getReferred().getName())); | ||
124 | EList<VLSTerm> _terms = it.getTerms(); | ||
125 | VLSVariable _duplicate = this.support.duplicate(v); | ||
126 | _terms.add(_duplicate); | ||
127 | }; | ||
128 | final VLSFunction varTypeComply = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_1); | ||
129 | relationVar2TypeDecComply.put(variable, varTypeComply); | ||
130 | relationVar2TypeDecRes.put(variable, this.support.duplicate(varTypeComply)); | ||
131 | } | ||
132 | } | ||
133 | final String[] nameArray = reldef.getName().split(" "); | ||
134 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | ||
135 | final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> { | ||
136 | int _length = nameArray.length; | ||
137 | int _minus = (_length - 2); | ||
138 | int _length_1 = nameArray.length; | ||
139 | int _minus_1 = (_length_1 - 1); | ||
140 | it.setName(this.support.toIDMultiple("compliance", nameArray[_minus], | ||
141 | nameArray[_minus_1])); | ||
142 | it.setFofRole("axiom"); | ||
143 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | ||
144 | final Procedure1<VLSUniversalQuantifier> _function_1 = (VLSUniversalQuantifier it_1) -> { | ||
145 | EList<Variable> _variables_1 = reldef.getVariables(); | ||
146 | for (final Variable variable_1 : _variables_1) { | ||
147 | EList<VLSVariable> _variables_2 = it_1.getVariables(); | ||
148 | VLSVariable _duplicate = this.support.duplicate(CollectionsUtil.<Variable, VLSVariable>lookup(variable_1, relationVar2VLS)); | ||
149 | _variables_2.add(_duplicate); | ||
150 | } | ||
151 | VLSImplies _createVLSImplies = this.factory.createVLSImplies(); | ||
152 | final Procedure1<VLSImplies> _function_2 = (VLSImplies it_2) -> { | ||
153 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
154 | final Procedure1<VLSFunction> _function_3 = (VLSFunction it_3) -> { | ||
155 | it_3.setConstant(this.support.toIDMultiple("rel", reldef.getName())); | ||
156 | EList<Variable> _variables_3 = reldef.getVariables(); | ||
157 | for (final Variable variable_2 : _variables_3) { | ||
158 | { | ||
159 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
160 | final Procedure1<VLSVariable> _function_4 = (VLSVariable it_4) -> { | ||
161 | it_4.setName(CollectionsUtil.<Variable, VLSVariable>lookup(variable_2, relationVar2VLS).getName()); | ||
162 | }; | ||
163 | final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_4); | ||
164 | EList<VLSTerm> _terms = it_3.getTerms(); | ||
165 | _terms.add(v); | ||
166 | } | ||
167 | } | ||
168 | }; | ||
169 | VLSFunction _doubleArrow = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_3); | ||
170 | it_2.setLeft(_doubleArrow); | ||
171 | Collection<VLSFunction> _values = relationVar2TypeDecComply.values(); | ||
172 | ArrayList<VLSTerm> _arrayList = new ArrayList<VLSTerm>(_values); | ||
173 | it_2.setRight(this.support.unfoldAnd(_arrayList)); | ||
174 | }; | ||
175 | VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_2); | ||
176 | it_1.setOperand(_doubleArrow); | ||
177 | }; | ||
178 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_1); | ||
179 | it.setFofFormula(_doubleArrow); | ||
180 | }; | ||
181 | final VLSFofFormula comply = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function); | ||
182 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); | ||
183 | final Procedure1<VLSFofFormula> _function_1 = (VLSFofFormula it) -> { | ||
184 | int _length = nameArray.length; | ||
185 | int _minus = (_length - 2); | ||
186 | int _length_1 = nameArray.length; | ||
187 | int _minus_1 = (_length_1 - 1); | ||
188 | it.setName(this.support.toIDMultiple("relation", nameArray[_minus], | ||
189 | nameArray[_minus_1])); | ||
190 | it.setFofRole("axiom"); | ||
191 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | ||
192 | final Procedure1<VLSUniversalQuantifier> _function_2 = (VLSUniversalQuantifier it_1) -> { | ||
193 | EList<Variable> _variables_1 = reldef.getVariables(); | ||
194 | for (final Variable variable_1 : _variables_1) { | ||
195 | { | ||
196 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
197 | final Procedure1<VLSVariable> _function_3 = (VLSVariable it_2) -> { | ||
198 | it_2.setName(CollectionsUtil.<Variable, VLSVariable>lookup(variable_1, relationVar2VLS).getName()); | ||
199 | }; | ||
200 | final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_3); | ||
201 | EList<VLSVariable> _variables_2 = it_1.getVariables(); | ||
202 | _variables_2.add(v); | ||
203 | } | ||
204 | } | ||
205 | VLSImplies _createVLSImplies = this.factory.createVLSImplies(); | ||
206 | final Procedure1<VLSImplies> _function_3 = (VLSImplies it_2) -> { | ||
207 | Collection<VLSFunction> _values = relationVar2TypeDecRes.values(); | ||
208 | ArrayList<VLSTerm> _arrayList = new ArrayList<VLSTerm>(_values); | ||
209 | it_2.setLeft(this.support.unfoldAnd(_arrayList)); | ||
210 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); | ||
211 | final Procedure1<VLSEquivalent> _function_4 = (VLSEquivalent it_3) -> { | ||
212 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
213 | final Procedure1<VLSFunction> _function_5 = (VLSFunction it_4) -> { | ||
214 | it_4.setConstant(this.support.toIDMultiple("rel", reldef.getName())); | ||
215 | EList<Variable> _variables_2 = reldef.getVariables(); | ||
216 | for (final Variable variable_2 : _variables_2) { | ||
217 | { | ||
218 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
219 | final Procedure1<VLSVariable> _function_6 = (VLSVariable it_5) -> { | ||
220 | it_5.setName(CollectionsUtil.<Variable, VLSVariable>lookup(variable_2, relationVar2VLS).getName()); | ||
221 | }; | ||
222 | final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_6); | ||
223 | EList<VLSTerm> _terms = it_4.getTerms(); | ||
224 | _terms.add(v); | ||
225 | } | ||
226 | } | ||
227 | }; | ||
228 | VLSFunction _doubleArrow = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_5); | ||
229 | it_3.setLeft(_doubleArrow); | ||
230 | it_3.setRight(this.base.transformTerm(reldef.getValue(), trace, relationVar2VLS)); | ||
231 | }; | ||
232 | VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_4); | ||
233 | it_2.setRight(_doubleArrow); | ||
234 | }; | ||
235 | VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_3); | ||
236 | it_1.setOperand(_doubleArrow); | ||
237 | }; | ||
238 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_2); | ||
239 | it.setFofFormula(_doubleArrow); | ||
240 | }; | ||
241 | final VLSFofFormula res = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_1); | ||
242 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); | ||
243 | _formulas.add(comply); | ||
244 | EList<VLSFofFormula> _formulas_1 = trace.specification.getFormulas(); | ||
245 | _formulas_1.add(res); | ||
246 | } | ||
247 | |||
248 | public void transformRelation(final Relation r, final Logic2VampireLanguageMapperTrace trace) { | ||
249 | if (r instanceof RelationDeclaration) { | ||
250 | _transformRelation((RelationDeclaration)r, trace); | ||
251 | return; | ||
252 | } else if (r instanceof RelationDefinition) { | ||
253 | _transformRelation((RelationDefinition)r, trace); | ||
254 | return; | ||
255 | } else { | ||
256 | throw new IllegalArgumentException("Unhandled parameter types: " + | ||
257 | Arrays.<Object>asList(r, trace).toString()); | ||
258 | } | ||
259 | } | ||
260 | } | ||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java new file mode 100644 index 00000000..d2a6bff2 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java | |||
@@ -0,0 +1,215 @@ | |||
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.VLSAnd; | ||
7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant; | ||
8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality; | ||
9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; | ||
10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; | ||
11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies; | ||
12 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; | ||
13 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; | ||
14 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; | ||
15 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; | ||
16 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration; | ||
17 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; | ||
18 | import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; | ||
19 | import java.util.ArrayList; | ||
20 | import java.util.HashMap; | ||
21 | import java.util.Map; | ||
22 | import java.util.Set; | ||
23 | import org.eclipse.emf.common.util.EList; | ||
24 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; | ||
25 | import org.eclipse.xtext.xbase.lib.Conversions; | ||
26 | import org.eclipse.xtext.xbase.lib.Extension; | ||
27 | import org.eclipse.xtext.xbase.lib.Functions.Function1; | ||
28 | import org.eclipse.xtext.xbase.lib.ListExtensions; | ||
29 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; | ||
30 | import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; | ||
31 | |||
32 | @SuppressWarnings("all") | ||
33 | public class Logic2VampireLanguageMapper_ScopeMapper { | ||
34 | @Extension | ||
35 | private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE; | ||
36 | |||
37 | private final Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support(); | ||
38 | |||
39 | private final Logic2VampireLanguageMapper base; | ||
40 | |||
41 | private final VLSVariable variable = ObjectExtensions.<VLSVariable>operator_doubleArrow(this.factory.createVLSVariable(), ((Procedure1<VLSVariable>) (VLSVariable it) -> { | ||
42 | it.setName("A"); | ||
43 | })); | ||
44 | |||
45 | public Logic2VampireLanguageMapper_ScopeMapper(final Logic2VampireLanguageMapper base) { | ||
46 | this.base = base; | ||
47 | } | ||
48 | |||
49 | public void _transformScope(final LogicSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) { | ||
50 | final int GLOBAL_MIN = config.typeScopes.minNewElements; | ||
51 | final int GLOBAL_MAX = config.typeScopes.maxNewElements; | ||
52 | final ArrayList<VLSConstant> localInstances = CollectionLiterals.<VLSConstant>newArrayList(); | ||
53 | if ((GLOBAL_MIN != 0)) { | ||
54 | this.getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, false); | ||
55 | for (final VLSConstant i : trace.uniqueInstances) { | ||
56 | localInstances.add(this.support.duplicate(i)); | ||
57 | } | ||
58 | this.makeFofFormula(localInstances, trace, true, null); | ||
59 | } | ||
60 | if ((GLOBAL_MAX != 0)) { | ||
61 | this.getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, true); | ||
62 | this.makeFofFormula(((ArrayList) trace.uniqueInstances), trace, false, null); | ||
63 | } | ||
64 | int i_1 = 1; | ||
65 | int minNum = (-1); | ||
66 | Map<Type, Integer> startPoints = new HashMap<Type, Integer>(); | ||
67 | Set<Type> _keySet = config.typeScopes.minNewElementsByType.keySet(); | ||
68 | for (final Type t : _keySet) { | ||
69 | { | ||
70 | minNum = (CollectionsUtil.<Type, Integer>lookup(t, config.typeScopes.minNewElementsByType)).intValue(); | ||
71 | if ((minNum != 0)) { | ||
72 | this.getInstanceConstants((i_1 + minNum), i_1, localInstances, trace, true, false); | ||
73 | startPoints.put(t, Integer.valueOf(i_1)); | ||
74 | int _i = i_1; | ||
75 | i_1 = (_i + minNum); | ||
76 | this.makeFofFormula(localInstances, trace, true, t); | ||
77 | } | ||
78 | } | ||
79 | } | ||
80 | Set<Type> _keySet_1 = config.typeScopes.maxNewElementsByType.keySet(); | ||
81 | for (final Type t_1 : _keySet_1) { | ||
82 | { | ||
83 | Integer maxNum = CollectionsUtil.<Type, Integer>lookup(t_1, config.typeScopes.maxNewElementsByType); | ||
84 | minNum = (CollectionsUtil.<Type, Integer>lookup(t_1, config.typeScopes.minNewElementsByType)).intValue(); | ||
85 | Integer startpoint = CollectionsUtil.<Type, Integer>lookup(t_1, startPoints); | ||
86 | if ((minNum != 0)) { | ||
87 | this.getInstanceConstants(((startpoint).intValue() + minNum), (startpoint).intValue(), localInstances, trace, true, false); | ||
88 | } | ||
89 | if (((maxNum).intValue() != minNum)) { | ||
90 | int instEndInd = Math.min(GLOBAL_MAX, ((i_1 + (maxNum).intValue()) - minNum)); | ||
91 | this.getInstanceConstants(instEndInd, i_1, localInstances, trace, false, false); | ||
92 | this.makeFofFormula(localInstances, trace, false, t_1); | ||
93 | } | ||
94 | } | ||
95 | } | ||
96 | int _length = ((Object[])Conversions.unwrapArray(trace.uniqueInstances, Object.class)).length; | ||
97 | boolean _notEquals = (_length != 0); | ||
98 | if (_notEquals) { | ||
99 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | ||
100 | final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> { | ||
101 | it.setName("typeUniqueness"); | ||
102 | it.setFofRole("axiom"); | ||
103 | it.setFofFormula(this.support.establishUniqueness(trace.uniqueInstances)); | ||
104 | }; | ||
105 | final VLSFofFormula uniqueness = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function); | ||
106 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); | ||
107 | _formulas.add(uniqueness); | ||
108 | } | ||
109 | } | ||
110 | |||
111 | protected void getInstanceConstants(final int endInd, final int startInd, final ArrayList list, final Logic2VampireLanguageMapperTrace trace, final boolean clear, final boolean addToTrace) { | ||
112 | if (clear) { | ||
113 | list.clear(); | ||
114 | } | ||
115 | for (int i = startInd; (i < endInd); i++) { | ||
116 | { | ||
117 | final int num = (i + 1); | ||
118 | VLSConstant _createVLSConstant = this.factory.createVLSConstant(); | ||
119 | final Procedure1<VLSConstant> _function = (VLSConstant it) -> { | ||
120 | it.setName(("o" + Integer.valueOf(num))); | ||
121 | }; | ||
122 | final VLSConstant cst = ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _function); | ||
123 | if (addToTrace) { | ||
124 | trace.uniqueInstances.add(cst); | ||
125 | } | ||
126 | list.add(cst); | ||
127 | } | ||
128 | } | ||
129 | } | ||
130 | |||
131 | protected void makeFofFormula(final ArrayList list, final Logic2VampireLanguageMapperTrace trace, final boolean minimum, final Type type) { | ||
132 | String nm = ""; | ||
133 | VLSTerm tm = null; | ||
134 | if ((type == null)) { | ||
135 | nm = "object"; | ||
136 | tm = this.support.topLevelTypeFunc(); | ||
137 | } else { | ||
138 | nm = CollectionsUtil.<Type, VLSFunction>lookup(type, trace.type2Predicate).getConstant().toString(); | ||
139 | VLSAnd _createVLSAnd = this.factory.createVLSAnd(); | ||
140 | final Procedure1<VLSAnd> _function = (VLSAnd it) -> { | ||
141 | it.setLeft(this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(type, trace.type2Predicate))); | ||
142 | it.setRight(this.support.topLevelTypeFunc()); | ||
143 | }; | ||
144 | VLSAnd _doubleArrow = ObjectExtensions.<VLSAnd>operator_doubleArrow(_createVLSAnd, _function); | ||
145 | tm = _doubleArrow; | ||
146 | } | ||
147 | final String name = nm; | ||
148 | final VLSTerm term = tm; | ||
149 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | ||
150 | final Procedure1<VLSFofFormula> _function_1 = (VLSFofFormula it) -> { | ||
151 | String _xifexpression = null; | ||
152 | if (minimum) { | ||
153 | _xifexpression = "min"; | ||
154 | } else { | ||
155 | _xifexpression = "max"; | ||
156 | } | ||
157 | it.setName(this.support.toIDMultiple("typeScope", _xifexpression, name)); | ||
158 | it.setFofRole("axiom"); | ||
159 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | ||
160 | final Procedure1<VLSUniversalQuantifier> _function_2 = (VLSUniversalQuantifier it_1) -> { | ||
161 | EList<VLSVariable> _variables = it_1.getVariables(); | ||
162 | VLSVariable _duplicate = this.support.duplicate(this.variable); | ||
163 | _variables.add(_duplicate); | ||
164 | VLSImplies _createVLSImplies = this.factory.createVLSImplies(); | ||
165 | final Procedure1<VLSImplies> _function_3 = (VLSImplies it_2) -> { | ||
166 | if (minimum) { | ||
167 | final Function1<VLSTerm, VLSEquality> _function_4 = (VLSTerm i) -> { | ||
168 | VLSEquality _createVLSEquality = this.factory.createVLSEquality(); | ||
169 | final Procedure1<VLSEquality> _function_5 = (VLSEquality it_3) -> { | ||
170 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
171 | final Procedure1<VLSVariable> _function_6 = (VLSVariable it_4) -> { | ||
172 | it_4.setName(this.variable.getName()); | ||
173 | }; | ||
174 | VLSVariable _doubleArrow_1 = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_6); | ||
175 | it_3.setLeft(_doubleArrow_1); | ||
176 | it_3.setRight(i); | ||
177 | }; | ||
178 | return ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_5); | ||
179 | }; | ||
180 | it_2.setLeft(this.support.unfoldOr(ListExtensions.<VLSTerm, VLSEquality>map(list, _function_4))); | ||
181 | it_2.setRight(term); | ||
182 | } else { | ||
183 | it_2.setLeft(term); | ||
184 | final Function1<VLSTerm, VLSEquality> _function_5 = (VLSTerm i) -> { | ||
185 | VLSEquality _createVLSEquality = this.factory.createVLSEquality(); | ||
186 | final Procedure1<VLSEquality> _function_6 = (VLSEquality it_3) -> { | ||
187 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
188 | final Procedure1<VLSVariable> _function_7 = (VLSVariable it_4) -> { | ||
189 | it_4.setName(this.variable.getName()); | ||
190 | }; | ||
191 | VLSVariable _doubleArrow_1 = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_7); | ||
192 | it_3.setLeft(_doubleArrow_1); | ||
193 | it_3.setRight(i); | ||
194 | }; | ||
195 | return ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_6); | ||
196 | }; | ||
197 | it_2.setRight(this.support.unfoldOr(ListExtensions.<VLSTerm, VLSEquality>map(list, _function_5))); | ||
198 | } | ||
199 | }; | ||
200 | VLSImplies _doubleArrow_1 = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_3); | ||
201 | it_1.setOperand(_doubleArrow_1); | ||
202 | }; | ||
203 | VLSUniversalQuantifier _doubleArrow_1 = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_2); | ||
204 | it.setFofFormula(_doubleArrow_1); | ||
205 | }; | ||
206 | final VLSFofFormula cstDec = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_1); | ||
207 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); | ||
208 | _formulas.add(cstDec); | ||
209 | } | ||
210 | |||
211 | public void transformScope(final LogicSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) { | ||
212 | _transformScope(config, trace); | ||
213 | return; | ||
214 | } | ||
215 | } | ||
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..119d01f1 --- /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,383 @@ | |||
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.VLSConstant; | ||
7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSExistentialQuantifier; | ||
8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; | ||
9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunctionAsTerm; | ||
10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies; | ||
11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSInequality; | ||
12 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSOr; | ||
13 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; | ||
14 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; | ||
15 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; | ||
16 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; | ||
17 | import com.google.common.collect.Iterables; | ||
18 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference; | ||
19 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.QuantifiedExpression; | ||
20 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term; | ||
21 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; | ||
22 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference; | ||
23 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable; | ||
24 | import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; | ||
25 | import java.util.ArrayList; | ||
26 | import java.util.Collection; | ||
27 | import java.util.HashMap; | ||
28 | import java.util.List; | ||
29 | import java.util.Map; | ||
30 | import org.eclipse.emf.common.util.EList; | ||
31 | import org.eclipse.xtend2.lib.StringConcatenation; | ||
32 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; | ||
33 | import org.eclipse.xtext.xbase.lib.Conversions; | ||
34 | import org.eclipse.xtext.xbase.lib.ExclusiveRange; | ||
35 | import org.eclipse.xtext.xbase.lib.Extension; | ||
36 | import org.eclipse.xtext.xbase.lib.Functions.Function1; | ||
37 | import org.eclipse.xtext.xbase.lib.IterableExtensions; | ||
38 | import org.eclipse.xtext.xbase.lib.ListExtensions; | ||
39 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; | ||
40 | import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; | ||
41 | |||
42 | @SuppressWarnings("all") | ||
43 | public class Logic2VampireLanguageMapper_Support { | ||
44 | @Extension | ||
45 | private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE; | ||
46 | |||
47 | protected String toIDMultiple(final String... ids) { | ||
48 | final Function1<String, String> _function = (String it) -> { | ||
49 | return IterableExtensions.join(((Iterable<?>)Conversions.doWrapArray(it.split("\\s+"))), "_"); | ||
50 | }; | ||
51 | return IterableExtensions.join(ListExtensions.<String, String>map(((List<String>)Conversions.doWrapArray(ids)), _function), "_"); | ||
52 | } | ||
53 | |||
54 | protected String toID(final String ids) { | ||
55 | return IterableExtensions.join(((Iterable<?>)Conversions.doWrapArray(ids.split("\\s+"))), "_"); | ||
56 | } | ||
57 | |||
58 | protected VLSVariable duplicate(final VLSVariable term) { | ||
59 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
60 | final Procedure1<VLSVariable> _function = (VLSVariable it) -> { | ||
61 | it.setName(term.getName()); | ||
62 | }; | ||
63 | return ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function); | ||
64 | } | ||
65 | |||
66 | protected VLSFunctionAsTerm duplicate(final VLSFunctionAsTerm term) { | ||
67 | VLSFunctionAsTerm _createVLSFunctionAsTerm = this.factory.createVLSFunctionAsTerm(); | ||
68 | final Procedure1<VLSFunctionAsTerm> _function = (VLSFunctionAsTerm it) -> { | ||
69 | it.setFunctor(term.getFunctor()); | ||
70 | }; | ||
71 | return ObjectExtensions.<VLSFunctionAsTerm>operator_doubleArrow(_createVLSFunctionAsTerm, _function); | ||
72 | } | ||
73 | |||
74 | protected VLSConstant duplicate(final VLSConstant term) { | ||
75 | VLSConstant _createVLSConstant = this.factory.createVLSConstant(); | ||
76 | final Procedure1<VLSConstant> _function = (VLSConstant it) -> { | ||
77 | it.setName(term.getName()); | ||
78 | }; | ||
79 | return ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _function); | ||
80 | } | ||
81 | |||
82 | protected VLSFunction duplicate(final VLSFunction term) { | ||
83 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
84 | final Procedure1<VLSFunction> _function = (VLSFunction it) -> { | ||
85 | it.setConstant(term.getConstant()); | ||
86 | EList<VLSTerm> _terms = term.getTerms(); | ||
87 | for (final VLSTerm v : _terms) { | ||
88 | EList<VLSTerm> _terms_1 = it.getTerms(); | ||
89 | VLSVariable _duplicate = this.duplicate(((VLSVariable) v)); | ||
90 | _terms_1.add(_duplicate); | ||
91 | } | ||
92 | }; | ||
93 | return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function); | ||
94 | } | ||
95 | |||
96 | protected VLSFunction duplicate(final VLSFunction term, final VLSVariable v) { | ||
97 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
98 | final Procedure1<VLSFunction> _function = (VLSFunction it) -> { | ||
99 | it.setConstant(term.getConstant()); | ||
100 | EList<VLSTerm> _terms = it.getTerms(); | ||
101 | VLSVariable _duplicate = this.duplicate(v); | ||
102 | _terms.add(_duplicate); | ||
103 | }; | ||
104 | return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function); | ||
105 | } | ||
106 | |||
107 | protected VLSFunction duplicate(final VLSFunction term, final List<VLSVariable> vars) { | ||
108 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
109 | final Procedure1<VLSFunction> _function = (VLSFunction it) -> { | ||
110 | it.setConstant(term.getConstant()); | ||
111 | for (final VLSVariable v : vars) { | ||
112 | EList<VLSTerm> _terms = it.getTerms(); | ||
113 | VLSVariable _duplicate = this.duplicate(v); | ||
114 | _terms.add(_duplicate); | ||
115 | } | ||
116 | }; | ||
117 | return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function); | ||
118 | } | ||
119 | |||
120 | protected VLSFunction duplicate(final VLSFunction term, final VLSFunctionAsTerm v) { | ||
121 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
122 | final Procedure1<VLSFunction> _function = (VLSFunction it) -> { | ||
123 | it.setConstant(term.getConstant()); | ||
124 | EList<VLSTerm> _terms = it.getTerms(); | ||
125 | VLSFunctionAsTerm _duplicate = this.duplicate(v); | ||
126 | _terms.add(_duplicate); | ||
127 | }; | ||
128 | return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function); | ||
129 | } | ||
130 | |||
131 | protected VLSConstant toConstant(final VLSFunctionAsTerm term) { | ||
132 | VLSConstant _createVLSConstant = this.factory.createVLSConstant(); | ||
133 | final Procedure1<VLSConstant> _function = (VLSConstant it) -> { | ||
134 | it.setName(term.getFunctor()); | ||
135 | }; | ||
136 | return ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _function); | ||
137 | } | ||
138 | |||
139 | protected VLSFunction topLevelTypeFunc() { | ||
140 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
141 | final Procedure1<VLSFunction> _function = (VLSFunction it) -> { | ||
142 | it.setConstant("object"); | ||
143 | EList<VLSTerm> _terms = it.getTerms(); | ||
144 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
145 | final Procedure1<VLSVariable> _function_1 = (VLSVariable it_1) -> { | ||
146 | it_1.setName("A"); | ||
147 | }; | ||
148 | VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_1); | ||
149 | _terms.add(_doubleArrow); | ||
150 | }; | ||
151 | return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function); | ||
152 | } | ||
153 | |||
154 | protected VLSFunction topLevelTypeFunc(final VLSVariable v) { | ||
155 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
156 | final Procedure1<VLSFunction> _function = (VLSFunction it) -> { | ||
157 | it.setConstant("object"); | ||
158 | EList<VLSTerm> _terms = it.getTerms(); | ||
159 | VLSVariable _duplicate = this.duplicate(v); | ||
160 | _terms.add(_duplicate); | ||
161 | }; | ||
162 | return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function); | ||
163 | } | ||
164 | |||
165 | protected VLSFunction topLevelTypeFunc(final VLSFunctionAsTerm v) { | ||
166 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
167 | final Procedure1<VLSFunction> _function = (VLSFunction it) -> { | ||
168 | it.setConstant("object"); | ||
169 | EList<VLSTerm> _terms = it.getTerms(); | ||
170 | VLSFunctionAsTerm _duplicate = this.duplicate(v); | ||
171 | _terms.add(_duplicate); | ||
172 | }; | ||
173 | return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function); | ||
174 | } | ||
175 | |||
176 | public VLSTerm establishUniqueness(final List<VLSConstant> terms) { | ||
177 | final List<VLSInequality> eqs = CollectionLiterals.<VLSInequality>newArrayList(); | ||
178 | List<VLSConstant> _subList = terms.subList(1, ((Object[])Conversions.unwrapArray(terms, Object.class)).length); | ||
179 | for (final VLSConstant t1 : _subList) { | ||
180 | List<VLSConstant> _subList_1 = terms.subList(0, terms.indexOf(t1)); | ||
181 | for (final VLSConstant t2 : _subList_1) { | ||
182 | { | ||
183 | VLSInequality _createVLSInequality = this.factory.createVLSInequality(); | ||
184 | final Procedure1<VLSInequality> _function = (VLSInequality it) -> { | ||
185 | VLSConstant _createVLSConstant = this.factory.createVLSConstant(); | ||
186 | final Procedure1<VLSConstant> _function_1 = (VLSConstant it_1) -> { | ||
187 | it_1.setName(t2.getName()); | ||
188 | }; | ||
189 | VLSConstant _doubleArrow = ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _function_1); | ||
190 | it.setLeft(_doubleArrow); | ||
191 | VLSConstant _createVLSConstant_1 = this.factory.createVLSConstant(); | ||
192 | final Procedure1<VLSConstant> _function_2 = (VLSConstant it_1) -> { | ||
193 | it_1.setName(t1.getName()); | ||
194 | }; | ||
195 | VLSConstant _doubleArrow_1 = ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant_1, _function_2); | ||
196 | it.setRight(_doubleArrow_1); | ||
197 | }; | ||
198 | final VLSInequality eq = ObjectExtensions.<VLSInequality>operator_doubleArrow(_createVLSInequality, _function); | ||
199 | eqs.add(eq); | ||
200 | } | ||
201 | } | ||
202 | } | ||
203 | return this.unfoldAnd(eqs); | ||
204 | } | ||
205 | |||
206 | protected VLSTerm unfoldAnd(final List<? extends VLSTerm> operands) { | ||
207 | int _size = operands.size(); | ||
208 | boolean _equals = (_size == 1); | ||
209 | if (_equals) { | ||
210 | return IterableExtensions.head(operands); | ||
211 | } else { | ||
212 | int _size_1 = operands.size(); | ||
213 | boolean _greaterThan = (_size_1 > 1); | ||
214 | if (_greaterThan) { | ||
215 | VLSAnd _createVLSAnd = this.factory.createVLSAnd(); | ||
216 | final Procedure1<VLSAnd> _function = (VLSAnd it) -> { | ||
217 | it.setLeft(IterableExtensions.head(operands)); | ||
218 | it.setRight(this.unfoldAnd(operands.subList(1, operands.size()))); | ||
219 | }; | ||
220 | return ObjectExtensions.<VLSAnd>operator_doubleArrow(_createVLSAnd, _function); | ||
221 | } else { | ||
222 | StringConcatenation _builder = new StringConcatenation(); | ||
223 | _builder.append("Logic operator with 0 operands!"); | ||
224 | throw new UnsupportedOperationException(_builder.toString()); | ||
225 | } | ||
226 | } | ||
227 | } | ||
228 | |||
229 | protected VLSTerm unfoldOr(final List<? extends VLSTerm> operands) { | ||
230 | int _size = operands.size(); | ||
231 | boolean _equals = (_size == 1); | ||
232 | if (_equals) { | ||
233 | return IterableExtensions.head(operands); | ||
234 | } else { | ||
235 | int _size_1 = operands.size(); | ||
236 | boolean _greaterThan = (_size_1 > 1); | ||
237 | if (_greaterThan) { | ||
238 | VLSOr _createVLSOr = this.factory.createVLSOr(); | ||
239 | final Procedure1<VLSOr> _function = (VLSOr it) -> { | ||
240 | it.setLeft(IterableExtensions.head(operands)); | ||
241 | it.setRight(this.unfoldOr(operands.subList(1, operands.size()))); | ||
242 | }; | ||
243 | return ObjectExtensions.<VLSOr>operator_doubleArrow(_createVLSOr, _function); | ||
244 | } else { | ||
245 | StringConcatenation _builder = new StringConcatenation(); | ||
246 | _builder.append("Logic operator with 0 operands!"); | ||
247 | throw new UnsupportedOperationException(_builder.toString()); | ||
248 | } | ||
249 | } | ||
250 | } | ||
251 | |||
252 | protected VLSTerm unfoldDistinctTerms(final Logic2VampireLanguageMapper m, final EList<Term> operands, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
253 | int _size = operands.size(); | ||
254 | boolean _equals = (_size == 1); | ||
255 | if (_equals) { | ||
256 | return m.transformTerm(IterableExtensions.<Term>head(operands), trace, variables); | ||
257 | } else { | ||
258 | int _size_1 = operands.size(); | ||
259 | boolean _greaterThan = (_size_1 > 1); | ||
260 | if (_greaterThan) { | ||
261 | int _size_2 = operands.size(); | ||
262 | int _size_3 = operands.size(); | ||
263 | int _multiply = (_size_2 * _size_3); | ||
264 | int _divide = (_multiply / 2); | ||
265 | final ArrayList<VLSTerm> notEquals = new ArrayList<VLSTerm>(_divide); | ||
266 | int _size_4 = operands.size(); | ||
267 | ExclusiveRange _doubleDotLessThan = new ExclusiveRange(0, _size_4, true); | ||
268 | for (final Integer i : _doubleDotLessThan) { | ||
269 | int _size_5 = operands.size(); | ||
270 | ExclusiveRange _doubleDotLessThan_1 = new ExclusiveRange(((i).intValue() + 1), _size_5, true); | ||
271 | for (final Integer j : _doubleDotLessThan_1) { | ||
272 | VLSInequality _createVLSInequality = this.factory.createVLSInequality(); | ||
273 | final Procedure1<VLSInequality> _function = (VLSInequality it) -> { | ||
274 | it.setLeft(m.transformTerm(operands.get((i).intValue()), trace, variables)); | ||
275 | it.setRight(m.transformTerm(operands.get((j).intValue()), trace, variables)); | ||
276 | }; | ||
277 | VLSInequality _doubleArrow = ObjectExtensions.<VLSInequality>operator_doubleArrow(_createVLSInequality, _function); | ||
278 | notEquals.add(_doubleArrow); | ||
279 | } | ||
280 | } | ||
281 | return this.unfoldAnd(notEquals); | ||
282 | } else { | ||
283 | StringConcatenation _builder = new StringConcatenation(); | ||
284 | _builder.append("Logic operator with 0 operands!"); | ||
285 | throw new UnsupportedOperationException(_builder.toString()); | ||
286 | } | ||
287 | } | ||
288 | } | ||
289 | |||
290 | /** | ||
291 | * def protected String toID(List<String> ids) { | ||
292 | * ids.map[it.split("\\s+").join("'")].join("'") | ||
293 | * } | ||
294 | */ | ||
295 | protected VLSTerm createQuantifiedExpression(final Logic2VampireLanguageMapper mapper, final QuantifiedExpression expression, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables, final boolean isUniversal) { | ||
296 | VLSTerm _xblockexpression = null; | ||
297 | { | ||
298 | final Function1<Variable, VLSVariable> _function = (Variable v) -> { | ||
299 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
300 | final Procedure1<VLSVariable> _function_1 = (VLSVariable it) -> { | ||
301 | it.setName(this.toIDMultiple("V", v.getName())); | ||
302 | }; | ||
303 | return ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_1); | ||
304 | }; | ||
305 | final Map<Variable, VLSVariable> variableMap = IterableExtensions.<Variable, VLSVariable>toInvertedMap(expression.getQuantifiedVariables(), _function); | ||
306 | final ArrayList<VLSTerm> typedefs = new ArrayList<VLSTerm>(); | ||
307 | EList<Variable> _quantifiedVariables = expression.getQuantifiedVariables(); | ||
308 | for (final Variable variable : _quantifiedVariables) { | ||
309 | { | ||
310 | TypeReference _range = variable.getRange(); | ||
311 | final VLSFunction eq = this.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(((ComplexTypeReference) _range).getReferred(), trace.type2Predicate), | ||
312 | CollectionsUtil.<Variable, VLSVariable>lookup(variable, variableMap)); | ||
313 | typedefs.add(eq); | ||
314 | } | ||
315 | } | ||
316 | VLSTerm _xifexpression = null; | ||
317 | if (isUniversal) { | ||
318 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | ||
319 | final Procedure1<VLSUniversalQuantifier> _function_1 = (VLSUniversalQuantifier it) -> { | ||
320 | EList<VLSVariable> _variables = it.getVariables(); | ||
321 | Collection<VLSVariable> _values = variableMap.values(); | ||
322 | Iterables.<VLSVariable>addAll(_variables, _values); | ||
323 | VLSImplies _createVLSImplies = this.factory.createVLSImplies(); | ||
324 | final Procedure1<VLSImplies> _function_2 = (VLSImplies it_1) -> { | ||
325 | it_1.setLeft(this.unfoldAnd(typedefs)); | ||
326 | it_1.setRight(mapper.transformTerm(expression.getExpression(), trace, this.withAddition(variables, variableMap))); | ||
327 | }; | ||
328 | VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_2); | ||
329 | it.setOperand(_doubleArrow); | ||
330 | }; | ||
331 | _xifexpression = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_1); | ||
332 | } else { | ||
333 | VLSExistentialQuantifier _xblockexpression_1 = null; | ||
334 | { | ||
335 | typedefs.add(mapper.transformTerm(expression.getExpression(), trace, this.withAddition(variables, variableMap))); | ||
336 | VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier(); | ||
337 | final Procedure1<VLSExistentialQuantifier> _function_2 = (VLSExistentialQuantifier it) -> { | ||
338 | EList<VLSVariable> _variables = it.getVariables(); | ||
339 | Collection<VLSVariable> _values = variableMap.values(); | ||
340 | Iterables.<VLSVariable>addAll(_variables, _values); | ||
341 | it.setOperand(this.unfoldAnd(typedefs)); | ||
342 | }; | ||
343 | _xblockexpression_1 = ObjectExtensions.<VLSExistentialQuantifier>operator_doubleArrow(_createVLSExistentialQuantifier, _function_2); | ||
344 | } | ||
345 | _xifexpression = _xblockexpression_1; | ||
346 | } | ||
347 | _xblockexpression = _xifexpression; | ||
348 | } | ||
349 | return _xblockexpression; | ||
350 | } | ||
351 | |||
352 | protected boolean dfsSupertypeCheck(final Type type, final Type type2) { | ||
353 | boolean _xifexpression = false; | ||
354 | boolean _isEmpty = type.getSupertypes().isEmpty(); | ||
355 | if (_isEmpty) { | ||
356 | return false; | ||
357 | } else { | ||
358 | boolean _xifexpression_1 = false; | ||
359 | boolean _contains = type.getSupertypes().contains(type2); | ||
360 | if (_contains) { | ||
361 | return true; | ||
362 | } else { | ||
363 | EList<Type> _supertypes = type.getSupertypes(); | ||
364 | for (final Type supertype : _supertypes) { | ||
365 | boolean _dfsSupertypeCheck = this.dfsSupertypeCheck(supertype, type2); | ||
366 | if (_dfsSupertypeCheck) { | ||
367 | return true; | ||
368 | } | ||
369 | } | ||
370 | } | ||
371 | _xifexpression = _xifexpression_1; | ||
372 | } | ||
373 | return _xifexpression; | ||
374 | } | ||
375 | |||
376 | protected HashMap<Variable, VLSVariable> withAddition(final Map<Variable, VLSVariable> map1, final Map<Variable, VLSVariable> map2) { | ||
377 | HashMap<Variable, VLSVariable> _hashMap = new HashMap<Variable, VLSVariable>(map1); | ||
378 | final Procedure1<HashMap<Variable, VLSVariable>> _function = (HashMap<Variable, VLSVariable> it) -> { | ||
379 | it.putAll(map2); | ||
380 | }; | ||
381 | return ObjectExtensions.<HashMap<Variable, VLSVariable>>operator_doubleArrow(_hashMap, _function); | ||
382 | } | ||
383 | } | ||
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..ec759ebf --- /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,281 @@ | |||
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.VLSAnd; | ||
7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant; | ||
8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSDoubleQuote; | ||
9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality; | ||
10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent; | ||
11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; | ||
12 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; | ||
13 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunctionAsTerm; | ||
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.CollectionLiterals; | ||
31 | import org.eclipse.xtext.xbase.lib.Conversions; | ||
32 | import org.eclipse.xtext.xbase.lib.Extension; | ||
33 | import org.eclipse.xtext.xbase.lib.Functions.Function1; | ||
34 | import org.eclipse.xtext.xbase.lib.IterableExtensions; | ||
35 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; | ||
36 | import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; | ||
37 | |||
38 | @SuppressWarnings("all") | ||
39 | public class Logic2VampireLanguageMapper_TypeMapper { | ||
40 | @Extension | ||
41 | private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE; | ||
42 | |||
43 | private final Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support(); | ||
44 | |||
45 | private final Logic2VampireLanguageMapper base; | ||
46 | |||
47 | public Logic2VampireLanguageMapper_TypeMapper(final Logic2VampireLanguageMapper base) { | ||
48 | LogicproblemPackage.eINSTANCE.getClass(); | ||
49 | this.base = base; | ||
50 | } | ||
51 | |||
52 | protected boolean transformTypes(final Collection<Type> types, final Collection<DefinedElement> elements, final Logic2VampireLanguageMapper mapper, final Logic2VampireLanguageMapperTrace trace) { | ||
53 | boolean _xblockexpression = false; | ||
54 | { | ||
55 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
56 | final Procedure1<VLSVariable> _function = (VLSVariable it) -> { | ||
57 | it.setName("A"); | ||
58 | }; | ||
59 | final VLSVariable variable = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function); | ||
60 | int globalCounter = 0; | ||
61 | for (final Type type : types) { | ||
62 | { | ||
63 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
64 | final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> { | ||
65 | it.setConstant(this.support.toIDMultiple("t", type.getName().split(" ")[0])); | ||
66 | EList<VLSTerm> _terms = it.getTerms(); | ||
67 | VLSVariable _duplicate = this.support.duplicate(variable); | ||
68 | _terms.add(_duplicate); | ||
69 | }; | ||
70 | final VLSFunction typePred = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_1); | ||
71 | trace.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 | final List<VLSFunction> orElems = CollectionLiterals.<VLSFunction>newArrayList(); | ||
78 | EList<DefinedElement> _elements = type_1.getElements(); | ||
79 | for (final DefinedElement e : _elements) { | ||
80 | { | ||
81 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
82 | final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> { | ||
83 | final String[] splitName = e.getName().split(" "); | ||
84 | int _length = splitName.length; | ||
85 | boolean _greaterThan = (_length > 2); | ||
86 | if (_greaterThan) { | ||
87 | it.setConstant(this.support.toIDMultiple("e", splitName[0], splitName[2])); | ||
88 | } else { | ||
89 | it.setConstant(this.support.toIDMultiple("e", splitName[0])); | ||
90 | } | ||
91 | EList<VLSTerm> _terms = it.getTerms(); | ||
92 | VLSVariable _duplicate = this.support.duplicate(variable); | ||
93 | _terms.add(_duplicate); | ||
94 | }; | ||
95 | final VLSFunction enumElemPred = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_1); | ||
96 | trace.element2Predicate.put(e, enumElemPred); | ||
97 | } | ||
98 | } | ||
99 | final List<VLSTerm> possibleNots = CollectionLiterals.<VLSTerm>newArrayList(); | ||
100 | final List<VLSTerm> typeDefs = CollectionLiterals.<VLSTerm>newArrayList(); | ||
101 | EList<DefinedElement> _elements_1 = type_1.getElements(); | ||
102 | for (final DefinedElement t1 : _elements_1) { | ||
103 | { | ||
104 | EList<DefinedElement> _elements_2 = type_1.getElements(); | ||
105 | for (final DefinedElement t2 : _elements_2) { | ||
106 | boolean _equals = Objects.equal(t1, t2); | ||
107 | if (_equals) { | ||
108 | final VLSFunction fct = this.support.duplicate(CollectionsUtil.<DefinedElement, VLSFunction>lookup(t2, trace.element2Predicate), variable); | ||
109 | possibleNots.add(fct); | ||
110 | } else { | ||
111 | final VLSFunction op = this.support.duplicate(CollectionsUtil.<DefinedElement, VLSFunction>lookup(t2, trace.element2Predicate), variable); | ||
112 | VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); | ||
113 | final Procedure1<VLSUnaryNegation> _function_1 = (VLSUnaryNegation it) -> { | ||
114 | it.setOperand(op); | ||
115 | }; | ||
116 | final VLSUnaryNegation negFct = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_1); | ||
117 | possibleNots.add(negFct); | ||
118 | } | ||
119 | } | ||
120 | typeDefs.add(this.support.unfoldAnd(possibleNots)); | ||
121 | possibleNots.clear(); | ||
122 | } | ||
123 | } | ||
124 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | ||
125 | final Procedure1<VLSFofFormula> _function_1 = (VLSFofFormula it) -> { | ||
126 | it.setName(this.support.toIDMultiple("typeDef", type_1.getName().split(" ")[0])); | ||
127 | it.setFofRole("axiom"); | ||
128 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | ||
129 | final Procedure1<VLSUniversalQuantifier> _function_2 = (VLSUniversalQuantifier it_1) -> { | ||
130 | EList<VLSVariable> _variables = it_1.getVariables(); | ||
131 | VLSVariable _duplicate = this.support.duplicate(variable); | ||
132 | _variables.add(_duplicate); | ||
133 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); | ||
134 | final Procedure1<VLSEquivalent> _function_3 = (VLSEquivalent it_2) -> { | ||
135 | it_2.setLeft(CollectionsUtil.<TypeDefinition, VLSFunction>lookup(type_1, trace.type2Predicate)); | ||
136 | VLSAnd _createVLSAnd = this.factory.createVLSAnd(); | ||
137 | final Procedure1<VLSAnd> _function_4 = (VLSAnd it_3) -> { | ||
138 | it_3.setLeft(this.support.topLevelTypeFunc(variable)); | ||
139 | it_3.setRight(this.support.unfoldOr(typeDefs)); | ||
140 | }; | ||
141 | VLSAnd _doubleArrow = ObjectExtensions.<VLSAnd>operator_doubleArrow(_createVLSAnd, _function_4); | ||
142 | it_2.setRight(_doubleArrow); | ||
143 | }; | ||
144 | VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_3); | ||
145 | it_1.setOperand(_doubleArrow); | ||
146 | }; | ||
147 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_2); | ||
148 | it.setFofFormula(_doubleArrow); | ||
149 | }; | ||
150 | final VLSFofFormula res = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_1); | ||
151 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); | ||
152 | _formulas.add(res); | ||
153 | for (int i = globalCounter; (i < (globalCounter + ((Object[])Conversions.unwrapArray(type_1.getElements(), Object.class)).length)); i++) { | ||
154 | { | ||
155 | final int num = (i + 1); | ||
156 | VLSFunctionAsTerm _createVLSFunctionAsTerm = this.factory.createVLSFunctionAsTerm(); | ||
157 | final Procedure1<VLSFunctionAsTerm> _function_2 = (VLSFunctionAsTerm it) -> { | ||
158 | it.setFunctor(("eo" + Integer.valueOf(num))); | ||
159 | }; | ||
160 | final VLSFunctionAsTerm cstTerm = ObjectExtensions.<VLSFunctionAsTerm>operator_doubleArrow(_createVLSFunctionAsTerm, _function_2); | ||
161 | final VLSConstant cst = this.support.toConstant(cstTerm); | ||
162 | trace.uniqueInstances.add(cst); | ||
163 | final int index = i; | ||
164 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); | ||
165 | final Procedure1<VLSFofFormula> _function_3 = (VLSFofFormula it) -> { | ||
166 | it.setName(this.support.toIDMultiple("enumScope", type_1.getName().split(" ")[0], | ||
167 | type_1.getElements().get(index).getName().split(" ")[0])); | ||
168 | it.setFofRole("axiom"); | ||
169 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | ||
170 | final Procedure1<VLSUniversalQuantifier> _function_4 = (VLSUniversalQuantifier it_1) -> { | ||
171 | EList<VLSVariable> _variables = it_1.getVariables(); | ||
172 | VLSVariable _duplicate = this.support.duplicate(variable); | ||
173 | _variables.add(_duplicate); | ||
174 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); | ||
175 | final Procedure1<VLSEquivalent> _function_5 = (VLSEquivalent it_2) -> { | ||
176 | VLSEquality _createVLSEquality = this.factory.createVLSEquality(); | ||
177 | final Procedure1<VLSEquality> _function_6 = (VLSEquality it_3) -> { | ||
178 | it_3.setLeft(this.support.duplicate(variable)); | ||
179 | it_3.setRight(this.support.duplicate(this.support.toConstant(cstTerm))); | ||
180 | }; | ||
181 | VLSEquality _doubleArrow = ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_6); | ||
182 | it_2.setLeft(_doubleArrow); | ||
183 | it_2.setRight(this.support.duplicate(CollectionsUtil.<DefinedElement, VLSFunction>lookup(type_1.getElements().get(index), trace.element2Predicate), variable)); | ||
184 | }; | ||
185 | VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_5); | ||
186 | it_1.setOperand(_doubleArrow); | ||
187 | }; | ||
188 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_4); | ||
189 | it.setFofFormula(_doubleArrow); | ||
190 | }; | ||
191 | final VLSFofFormula enumScope = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_3); | ||
192 | EList<VLSFofFormula> _formulas_1 = trace.specification.getFormulas(); | ||
193 | _formulas_1.add(enumScope); | ||
194 | } | ||
195 | } | ||
196 | int _globalCounter = globalCounter; | ||
197 | int _size = type_1.getElements().size(); | ||
198 | globalCounter = (_globalCounter + _size); | ||
199 | } | ||
200 | } | ||
201 | final Function1<Type, Boolean> _function_1 = (Type it) -> { | ||
202 | boolean _isIsAbstract = it.isIsAbstract(); | ||
203 | return Boolean.valueOf((!_isIsAbstract)); | ||
204 | }; | ||
205 | Iterable<Type> _filter_1 = IterableExtensions.<Type>filter(types, _function_1); | ||
206 | for (final Type t1 : _filter_1) { | ||
207 | { | ||
208 | for (final Type t2 : types) { | ||
209 | if ((Objects.equal(t1, t2) || this.support.dfsSupertypeCheck(t1, t2))) { | ||
210 | trace.type2PossibleNot.put(t2, this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(t2, trace.type2Predicate))); | ||
211 | } else { | ||
212 | VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); | ||
213 | final Procedure1<VLSUnaryNegation> _function_2 = (VLSUnaryNegation it) -> { | ||
214 | it.setOperand(this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(t2, trace.type2Predicate))); | ||
215 | }; | ||
216 | VLSUnaryNegation _doubleArrow = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_2); | ||
217 | trace.type2PossibleNot.put(t2, _doubleArrow); | ||
218 | } | ||
219 | } | ||
220 | Collection<VLSTerm> _values = trace.type2PossibleNot.values(); | ||
221 | ArrayList<VLSTerm> _arrayList = new ArrayList<VLSTerm>(_values); | ||
222 | trace.type2And.put(t1, this.support.unfoldAnd(_arrayList)); | ||
223 | trace.type2PossibleNot.clear(); | ||
224 | } | ||
225 | } | ||
226 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | ||
227 | final Procedure1<VLSFofFormula> _function_2 = (VLSFofFormula it) -> { | ||
228 | it.setName("inheritanceHierarchyHandler"); | ||
229 | it.setFofRole("axiom"); | ||
230 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | ||
231 | final Procedure1<VLSUniversalQuantifier> _function_3 = (VLSUniversalQuantifier it_1) -> { | ||
232 | EList<VLSVariable> _variables = it_1.getVariables(); | ||
233 | VLSVariable _duplicate = this.support.duplicate(variable); | ||
234 | _variables.add(_duplicate); | ||
235 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); | ||
236 | final Procedure1<VLSEquivalent> _function_4 = (VLSEquivalent it_2) -> { | ||
237 | it_2.setLeft(this.support.topLevelTypeFunc()); | ||
238 | Collection<VLSTerm> _values = trace.type2And.values(); | ||
239 | final ArrayList<VLSTerm> reversedList = new ArrayList<VLSTerm>(_values); | ||
240 | it_2.setRight(this.support.unfoldOr(reversedList)); | ||
241 | }; | ||
242 | VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_4); | ||
243 | it_1.setOperand(_doubleArrow); | ||
244 | }; | ||
245 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_3); | ||
246 | it.setFofFormula(_doubleArrow); | ||
247 | }; | ||
248 | final VLSFofFormula hierarch = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_2); | ||
249 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); | ||
250 | _xblockexpression = _formulas.add(hierarch); | ||
251 | } | ||
252 | return _xblockexpression; | ||
253 | } | ||
254 | |||
255 | protected void transformTypeReference(final Type referred, final Logic2VampireLanguageMapper mapper, final Logic2VampireLanguageMapperTrace trace) { | ||
256 | throw new UnsupportedOperationException("TODO: auto-generated method stub"); | ||
257 | } | ||
258 | |||
259 | protected void getUndefinedSupertype(final Logic2VampireLanguageMapperTrace trace) { | ||
260 | throw new UnsupportedOperationException("TODO: auto-generated method stub"); | ||
261 | } | ||
262 | |||
263 | protected void getUndefinedSupertypeScope(final int undefinedScope, final Logic2VampireLanguageMapperTrace trace) { | ||
264 | throw new UnsupportedOperationException("TODO: auto-generated method stub"); | ||
265 | } | ||
266 | |||
267 | protected VLSDoubleQuote transformReference(final DefinedElement referred, final Logic2VampireLanguageMapperTrace trace) { | ||
268 | VLSDoubleQuote _createVLSDoubleQuote = this.factory.createVLSDoubleQuote(); | ||
269 | final Procedure1<VLSDoubleQuote> _function = (VLSDoubleQuote it) -> { | ||
270 | String _name = referred.getName(); | ||
271 | String _plus = ("\"a" + _name); | ||
272 | String _plus_1 = (_plus + "\""); | ||
273 | it.setValue(_plus_1); | ||
274 | }; | ||
275 | return ObjectExtensions.<VLSDoubleQuote>operator_doubleArrow(_createVLSDoubleQuote, _function); | ||
276 | } | ||
277 | |||
278 | protected void getTypeInterpreter() { | ||
279 | throw new UnsupportedOperationException("TODO: auto-generated method stub"); | ||
280 | } | ||
281 | } | ||
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..f7c6cb70 --- /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,20 @@ | |||
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.VLSFunction; | ||
5 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement; | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; | ||
8 | import java.util.HashMap; | ||
9 | import java.util.Map; | ||
10 | |||
11 | @SuppressWarnings("all") | ||
12 | public class Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes implements Logic2VampireLanguageMapper_TypeMapperTrace { | ||
13 | public final Map<Type, VLSFunction> type2Predicate = new HashMap<Type, VLSFunction>(); | ||
14 | |||
15 | public final Map<DefinedElement, VLSFunction> element2Predicate = new HashMap<DefinedElement, VLSFunction>(); | ||
16 | |||
17 | public final Map<Type, VLSTerm> type2PossibleNot = new HashMap<Type, VLSTerm>(); | ||
18 | |||
19 | public final Map<Type, VLSTerm> type2And = new HashMap<Type, VLSTerm>(); | ||
20 | } | ||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.java new file mode 100644 index 00000000..f4b5a1d2 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.java | |||
@@ -0,0 +1,5 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; | ||
2 | |||
3 | @SuppressWarnings("all") | ||
4 | public class Vampire2LogicMapper { | ||
5 | } | ||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.java new file mode 100644 index 00000000..1cac2633 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.java | |||
@@ -0,0 +1,12 @@ | |||
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.vampireLanguage.VampireModel; | ||
5 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace; | ||
6 | |||
7 | @SuppressWarnings("all") | ||
8 | public class VampireHandler { | ||
9 | public Object callSolver(final VampireModel problem, final ReasonerWorkspace workspace, final VampireSolverConfiguration configuration, final String vampireCode) { | ||
10 | return null; | ||
11 | } | ||
12 | } | ||
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 | } | ||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireSolutionModel.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireSolutionModel.java new file mode 100644 index 00000000..3c43c4ea --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireSolutionModel.java | |||
@@ -0,0 +1,34 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; | ||
2 | |||
3 | import org.eclipse.xtend.lib.annotations.Data; | ||
4 | import org.eclipse.xtext.xbase.lib.Pure; | ||
5 | import org.eclipse.xtext.xbase.lib.util.ToStringBuilder; | ||
6 | |||
7 | @Data | ||
8 | @SuppressWarnings("all") | ||
9 | public class VampireSolutionModel { | ||
10 | @Override | ||
11 | @Pure | ||
12 | public int hashCode() { | ||
13 | return 1; | ||
14 | } | ||
15 | |||
16 | @Override | ||
17 | @Pure | ||
18 | public boolean equals(final Object obj) { | ||
19 | if (this == obj) | ||
20 | return true; | ||
21 | if (obj == null) | ||
22 | return false; | ||
23 | if (getClass() != obj.getClass()) | ||
24 | return false; | ||
25 | return true; | ||
26 | } | ||
27 | |||
28 | @Override | ||
29 | @Pure | ||
30 | public String toString() { | ||
31 | ToStringBuilder b = new ToStringBuilder(this); | ||
32 | return b.toString(); | ||
33 | } | ||
34 | } | ||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireSolverException.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireSolverException.java new file mode 100644 index 00000000..b96df82a --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireSolverException.java | |||
@@ -0,0 +1,19 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; | ||
2 | |||
3 | import java.util.List; | ||
4 | import org.eclipse.xtext.xbase.lib.IterableExtensions; | ||
5 | |||
6 | @SuppressWarnings("all") | ||
7 | public class VampireSolverException extends Exception { | ||
8 | public VampireSolverException(final String s) { | ||
9 | super(s); | ||
10 | } | ||
11 | |||
12 | public VampireSolverException(final String s, final Exception e) { | ||
13 | super(s, e); | ||
14 | } | ||
15 | |||
16 | public VampireSolverException(final String s, final List<String> errors, final Exception e) { | ||
17 | super(((s + "\n") + IterableExtensions.join(errors, "\n")), e); | ||
18 | } | ||
19 | } | ||