aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill
diff options
context:
space:
mode:
authorLibravatar ArenBabikian <aren.babikian@mail.mcgill.ca>2019-08-29 16:54:53 -0400
committerLibravatar ArenBabikian <aren.babikian@mail.mcgill.ca>2020-06-07 19:41:41 -0400
commit5cfe202ab86f117e35b286cfadf7f8301bce3a43 (patch)
treed3d6bc6b07a841dac02af22523c37327c309a119 /Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill
parentVAMPIRE: adapt grammar to Vampire solution + get model from text (diff)
downloadVIATRA-Generator-5cfe202ab86f117e35b286cfadf7f8301bce3a43.tar.gz
VIATRA-Generator-5cfe202ab86f117e35b286cfadf7f8301bce3a43.tar.zst
VIATRA-Generator-5cfe202ab86f117e35b286cfadf7f8301bce3a43.zip
VAMPIRE: setup structure of model interpretation
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill')
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbinbin2691 -> 2691 bytes
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbinbin6465 -> 6957 bytes
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.java26
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbinbin17754 -> 17754 bytes
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbinbin4692 -> 4692 bytes
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbinbin3164 -> 3164 bytes
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbinbin11835 -> 11835 bytes
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbinbin6497 -> 6497 bytes
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbinbin10701 -> 10701 bytes
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbinbin13083 -> 13083 bytes
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbinbin11170 -> 11170 bytes
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbinbin1720 -> 3858 bytes
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbinbin6445 -> 6386 bytes
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbinbin1491 -> 1491 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.xtendbinbin1688 -> 1688 bytes
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.java31
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.java9
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireSolutionModel.java34
18 files changed, 56 insertions, 44 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
index b9600616..499504af 100644
--- 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
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
index 43992ea0..298a6c08 100644
--- 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
Binary files differ
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
index 410b47ed..a7780e97 100644
--- 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
@@ -5,8 +5,10 @@ import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetupGenerated;
5import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration; 5import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration;
6import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; 6import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper;
7import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; 7import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace;
8import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.MonitoredVampireSolution;
8import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Vampire2LogicMapper; 9import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Vampire2LogicMapper;
9import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireHandler; 10import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireHandler;
11import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireModelInterpretation;
10import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage; 12import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage;
11import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel; 13import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel;
12import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel; 14import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel;
@@ -21,9 +23,10 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult;
21import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace; 23import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace;
22import java.util.List; 24import java.util.List;
23import org.eclipse.emf.common.util.EList; 25import org.eclipse.emf.common.util.EList;
24import org.eclipse.emf.ecore.EObject;
25import org.eclipse.xtend2.lib.StringConcatenation; 26import org.eclipse.xtend2.lib.StringConcatenation;
26import org.eclipse.xtext.xbase.lib.Exceptions; 27import org.eclipse.xtext.xbase.lib.Exceptions;
28import org.eclipse.xtext.xbase.lib.Functions.Function1;
29import org.eclipse.xtext.xbase.lib.ListExtensions;
27 30
28@SuppressWarnings("all") 31@SuppressWarnings("all")
29public class VampireSolver extends LogicReasoner { 32public class VampireSolver extends LogicReasoner {
@@ -72,10 +75,14 @@ public class VampireSolver extends LogicReasoner {
72 long _currentTimeMillis = System.currentTimeMillis(); 75 long _currentTimeMillis = System.currentTimeMillis();
73 final long transformationTime = (_currentTimeMillis - transformationStart); 76 final long transformationTime = (_currentTimeMillis - transformationStart);
74 final long solverStart = System.currentTimeMillis(); 77 final long solverStart = System.currentTimeMillis();
75 final EList<EObject> result2 = this.handler.callSolver(vampireProblem, workspace, vampireConfig); 78 final MonitoredVampireSolution vampSol = this.handler.callSolver(vampireProblem, workspace, vampireConfig);
76 long _currentTimeMillis_1 = System.currentTimeMillis(); 79 long _currentTimeMillis_1 = System.currentTimeMillis();
77 final long solvingTime = (_currentTimeMillis_1 - solverStart); 80 final long solvingTime = (_currentTimeMillis_1 - solverStart);
78 return null; 81 final long backTransformationStart = System.currentTimeMillis();
82 final ModelResult logicResult = this.backwardMapper.transformOutput(problem, vampireConfig.solutionScope.numberOfRequiredSolution, vampSol, forwardTrace, transformationTime);
83 long _currentTimeMillis_2 = System.currentTimeMillis();
84 final long backTransformationTime = (_currentTimeMillis_2 - backTransformationStart);
85 return logicResult;
79 } 86 }
80 87
81 public VampireSolverConfiguration asConfig(final LogicSolverConfiguration configuration) { 88 public VampireSolverConfiguration asConfig(final LogicSolverConfiguration configuration) {
@@ -93,6 +100,17 @@ public class VampireSolver extends LogicReasoner {
93 100
94 @Override 101 @Override
95 public List<? extends LogicModelInterpretation> getInterpretations(final ModelResult modelResult) { 102 public List<? extends LogicModelInterpretation> getInterpretations(final ModelResult modelResult) {
96 return null; 103 List<VampireModelInterpretation> _xblockexpression = null;
104 {
105 final EList<Object> sols = modelResult.getRepresentation();
106 final Function1<Object, VampireModelInterpretation> _function = (Object it) -> {
107 Object _trace = modelResult.getTrace();
108 return new VampireModelInterpretation(
109 ((VampireModel) it),
110 ((Logic2VampireLanguageMapperTrace) _trace));
111 };
112 _xblockexpression = ListExtensions.<Object, VampireModelInterpretation>map(sols, _function);
113 }
114 return _xblockexpression;
97 } 115 }
98} 116}
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
index 19608361..863b572e 100644
--- 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
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
index 791a9524..410f2550 100644
--- 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
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
index 89003c27..b1b39a4f 100644
--- 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
Binary files differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin
index b37d993a..3710e753 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin
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
index 45afcecc..9dc7abaf 100644
--- 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
Binary files differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin
index 0f4dc63a..7029d196 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin
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
index ab58fcab..03aead59 100644
--- 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
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
index cf19663e..62960704 100644
--- 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
Binary files differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin
index f8b35528..56a10b3c 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin
Binary files differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin
index 0b2cb192..319f863c 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin
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
index ffd37ea3..3b6009bb 100644
--- 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
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
index 9ddc7bd0..d8329084 100644
--- 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
Binary files differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.java
index f4b5a1d2..29a2ecea 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.java
@@ -1,5 +1,36 @@
1package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; 1package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder;
2 2
3import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace;
4import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.MonitoredVampireSolution;
5import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel;
6import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem;
7import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory;
8import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult;
9import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.Statistics;
10import org.eclipse.emf.common.util.EList;
11import org.eclipse.xtext.xbase.lib.Extension;
12import org.eclipse.xtext.xbase.lib.ObjectExtensions;
13import org.eclipse.xtext.xbase.lib.Procedures.Procedure1;
14
3@SuppressWarnings("all") 15@SuppressWarnings("all")
4public class Vampire2LogicMapper { 16public class Vampire2LogicMapper {
17 @Extension
18 private final LogicresultFactory resultFactory = LogicresultFactory.eINSTANCE;
19
20 public ModelResult transformOutput(final LogicProblem problem, final int requiredNumberOfSolution, final MonitoredVampireSolution monitoredVampireSolution, final Logic2VampireLanguageMapperTrace trace, final long transformationTime) {
21 ModelResult _createModelResult = this.resultFactory.createModelResult();
22 final Procedure1<ModelResult> _function = (ModelResult it) -> {
23 it.setProblem(problem);
24 EList<Object> _representation = it.getRepresentation();
25 VampireModel _generatedModel = monitoredVampireSolution.getGeneratedModel();
26 _representation.add(_generatedModel);
27 it.setTrace(trace);
28 it.setStatistics(this.transformStatistics(monitoredVampireSolution, transformationTime));
29 };
30 return ObjectExtensions.<ModelResult>operator_doubleArrow(_createModelResult, _function);
31 }
32
33 public Statistics transformStatistics(final MonitoredVampireSolution solution, final long transformationTime) {
34 return this.resultFactory.createStatistics();
35 }
5} 36}
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.java
index 7f6ce1c6..4764ae28 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.java
@@ -1,9 +1,8 @@
1package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; 1package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder;
2 2
3import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration; 3import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration;
4import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSComment; 4import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.MonitoredVampireSolution;
5import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel; 5import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel;
6import ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireModelImpl;
7import com.google.common.base.Objects; 6import com.google.common.base.Objects;
8import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace; 7import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace;
9import java.io.BufferedReader; 8import java.io.BufferedReader;
@@ -16,11 +15,10 @@ import org.eclipse.emf.ecore.EObject;
16import org.eclipse.xtext.xbase.lib.CollectionLiterals; 15import org.eclipse.xtext.xbase.lib.CollectionLiterals;
17import org.eclipse.xtext.xbase.lib.Conversions; 16import org.eclipse.xtext.xbase.lib.Conversions;
18import org.eclipse.xtext.xbase.lib.Exceptions; 17import org.eclipse.xtext.xbase.lib.Exceptions;
19import org.eclipse.xtext.xbase.lib.InputOutput;
20 18
21@SuppressWarnings("all") 19@SuppressWarnings("all")
22public class VampireHandler { 20public class VampireHandler {
23 public EList<EObject> callSolver(final VampireModel problem, final ReasonerWorkspace workspace, final VampireSolverConfiguration configuration) { 21 public MonitoredVampireSolution callSolver(final VampireModel problem, final ReasonerWorkspace workspace, final VampireSolverConfiguration configuration) {
24 try { 22 try {
25 final String CMD = "cmd /c "; 23 final String CMD = "cmd /c ";
26 final String VAMPDIR = "..\\..\\Solvers\\Vampire-Solver\\ca.mcgill.ecse.dslreasoner.vampire.reasoner\\lib\\"; 24 final String VAMPDIR = "..\\..\\Solvers\\Vampire-Solver\\ca.mcgill.ecse.dslreasoner.vampire.reasoner\\lib\\";
@@ -48,8 +46,7 @@ public class VampireHandler {
48 workspace.getFile(TEMPNAME).delete(); 46 workspace.getFile(TEMPNAME).delete();
49 final EList<EObject> root = workspace.<VampireModel>readModel(VampireModel.class, SOLNNAME).eResource().getContents(); 47 final EList<EObject> root = workspace.<VampireModel>readModel(VampireModel.class, SOLNNAME).eResource().getContents();
50 EObject _get = root.get(0); 48 EObject _get = root.get(0);
51 InputOutput.<EList<VLSComment>>println(((VampireModelImpl) _get).getComments()); 49 return new MonitoredVampireSolution(((VampireModel) _get));
52 return root;
53 } catch (Throwable _e) { 50 } catch (Throwable _e) {
54 throw Exceptions.sneakyThrow(_e); 51 throw Exceptions.sneakyThrow(_e);
55 } 52 }
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireSolutionModel.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireSolutionModel.java
deleted file mode 100644
index 3c43c4ea..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireSolutionModel.java
+++ /dev/null
@@ -1,34 +0,0 @@
1package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder;
2
3import org.eclipse.xtend.lib.annotations.Data;
4import org.eclipse.xtext.xbase.lib.Pure;
5import org.eclipse.xtext.xbase.lib.util.ToStringBuilder;
6
7@Data
8@SuppressWarnings("all")
9public class VampireSolutionModel {
10 @Override
11 @Pure
12 public int hashCode() {
13 return 1;
14 }
15
16 @Override
17 @Pure
18 public boolean equals(final Object obj) {
19 if (this == obj)
20 return true;
21 if (obj == null)
22 return false;
23 if (getClass() != obj.getClass())
24 return false;
25 return true;
26 }
27
28 @Override
29 @Pure
30 public String toString() {
31 ToStringBuilder b = new ToStringBuilder(this);
32 return b.toString();
33 }
34}