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