diff options
author | 2019-08-29 06:26:02 -0400 | |
---|---|---|
committer | 2019-08-29 06:26:02 -0400 | |
commit | 9ef9aef5ef8baa7e579d4eb4a5d27a7983f32c8b (patch) | |
tree | 0dd50253bffe482ae15f5b8c5fc46bbbad45f0e4 /Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner | |
parent | VAMPIRE: integrate local Vampire executeable #32 (diff) | |
download | VIATRA-Generator-9ef9aef5ef8baa7e579d4eb4a5d27a7983f32c8b.tar.gz VIATRA-Generator-9ef9aef5ef8baa7e579d4eb4a5d27a7983f32c8b.tar.zst VIATRA-Generator-9ef9aef5ef8baa7e579d4eb4a5d27a7983f32c8b.zip |
VAMPIRE: adapt grammar to Vampire solution + get model from text
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner')
17 files changed, 55 insertions, 72 deletions
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 a7942958..43992ea0 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/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 487f9569..19608361 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 bd61b874..791a9524 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 2e58cecd..89003c27 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 1b894303..b37d993a 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 4b7fd4bf..45afcecc 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 6626adf4..0f4dc63a 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 339baea9..ab58fcab 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 868f30e7..cf19663e 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/.VampireHandler.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin index 08ffcb3b..0b2cb192 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/Logic2VampireLanguageMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java index 65f58281..58da7ccd 100644 --- 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 | |||
@@ -16,7 +16,6 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; | |||
16 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; | 16 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; |
17 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies; | 17 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies; |
18 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSInt; | 18 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSInt; |
19 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSReal; | ||
20 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; | 19 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; |
21 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUnaryNegation; | 20 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUnaryNegation; |
22 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; | 21 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; |
@@ -44,7 +43,6 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.InstanceOf; | |||
44 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntLiteral; | 43 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntLiteral; |
45 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Not; | 44 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Not; |
46 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Or; | 45 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Or; |
47 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealLiteral; | ||
48 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation; | 46 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation; |
49 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration; | 47 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration; |
50 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition; | 48 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition; |
@@ -98,7 +96,7 @@ public class Logic2VampireLanguageMapper { | |||
98 | public TracedOutput<VampireModel, Logic2VampireLanguageMapperTrace> transformProblem(final LogicProblem problem, final VampireSolverConfiguration config) { | 96 | public TracedOutput<VampireModel, Logic2VampireLanguageMapperTrace> transformProblem(final LogicProblem problem, final VampireSolverConfiguration config) { |
99 | VLSComment _createVLSComment = this.factory.createVLSComment(); | 97 | VLSComment _createVLSComment = this.factory.createVLSComment(); |
100 | final Procedure1<VLSComment> _function = (VLSComment it) -> { | 98 | final Procedure1<VLSComment> _function = (VLSComment it) -> { |
101 | it.setComment("This is an initial Test Comment"); | 99 | it.setComment("%This is an initial Test Comment"); |
102 | }; | 100 | }; |
103 | final VLSComment initialComment = ObjectExtensions.<VLSComment>operator_doubleArrow(_createVLSComment, _function); | 101 | final VLSComment initialComment = ObjectExtensions.<VLSComment>operator_doubleArrow(_createVLSComment, _function); |
104 | VampireModel _createVampireModel = this.factory.createVampireModel(); | 102 | VampireModel _createVampireModel = this.factory.createVampireModel(); |
@@ -202,14 +200,6 @@ public class Logic2VampireLanguageMapper { | |||
202 | return ObjectExtensions.<VLSInt>operator_doubleArrow(_createVLSInt, _function); | 200 | return ObjectExtensions.<VLSInt>operator_doubleArrow(_createVLSInt, _function); |
203 | } | 201 | } |
204 | 202 | ||
205 | protected VLSTerm _transformTerm(final RealLiteral literal, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | ||
206 | VLSReal _createVLSReal = this.factory.createVLSReal(); | ||
207 | final Procedure1<VLSReal> _function = (VLSReal it) -> { | ||
208 | it.setValue(literal.getValue().toString()); | ||
209 | }; | ||
210 | return ObjectExtensions.<VLSReal>operator_doubleArrow(_createVLSReal, _function); | ||
211 | } | ||
212 | |||
213 | protected VLSTerm _transformTerm(final Not not, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | 203 | protected VLSTerm _transformTerm(final Not not, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { |
214 | VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); | 204 | VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); |
215 | final Procedure1<VLSUnaryNegation> _function = (VLSUnaryNegation it) -> { | 205 | final Procedure1<VLSUnaryNegation> _function = (VLSUnaryNegation it) -> { |
@@ -394,8 +384,6 @@ public class Logic2VampireLanguageMapper { | |||
394 | return _transformTerm((Not)and, trace, variables); | 384 | return _transformTerm((Not)and, trace, variables); |
395 | } else if (and instanceof Or) { | 385 | } else if (and instanceof Or) { |
396 | return _transformTerm((Or)and, trace, variables); | 386 | return _transformTerm((Or)and, trace, variables); |
397 | } else if (and instanceof RealLiteral) { | ||
398 | return _transformTerm((RealLiteral)and, trace, variables); | ||
399 | } else if (and instanceof InstanceOf) { | 387 | } else if (and instanceof InstanceOf) { |
400 | return _transformTerm((InstanceOf)and, trace, variables); | 388 | return _transformTerm((InstanceOf)and, trace, variables); |
401 | } else if (and instanceof SymbolicValue) { | 389 | } else if (and instanceof SymbolicValue) { |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java index dd549c29..7daf1b2f 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java | |||
@@ -15,6 +15,7 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; | |||
15 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUnaryNegation; | 15 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUnaryNegation; |
16 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; | 16 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; |
17 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; | 17 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; |
18 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariableDeclaration; | ||
18 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; | 19 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; |
19 | import com.google.common.base.Objects; | 20 | import com.google.common.base.Objects; |
20 | import com.google.common.collect.Iterables; | 21 | import com.google.common.collect.Iterables; |
@@ -37,7 +38,6 @@ import org.eclipse.emf.common.util.EList; | |||
37 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; | 38 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; |
38 | import org.eclipse.xtext.xbase.lib.Conversions; | 39 | import org.eclipse.xtext.xbase.lib.Conversions; |
39 | import org.eclipse.xtext.xbase.lib.Extension; | 40 | import org.eclipse.xtext.xbase.lib.Extension; |
40 | import org.eclipse.xtext.xbase.lib.InputOutput; | ||
41 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; | 41 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; |
42 | import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; | 42 | import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; |
43 | 43 | ||
@@ -123,7 +123,7 @@ public class Logic2VampireLanguageMapper_ContainmentMapper { | |||
123 | it.setFofRole("axiom"); | 123 | it.setFofRole("axiom"); |
124 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | 124 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); |
125 | final Procedure1<VLSUniversalQuantifier> _function_1 = (VLSUniversalQuantifier it_1) -> { | 125 | final Procedure1<VLSUniversalQuantifier> _function_1 = (VLSUniversalQuantifier it_1) -> { |
126 | EList<VLSVariable> _variables = it_1.getVariables(); | 126 | EList<VLSVariableDeclaration> _variables = it_1.getVariables(); |
127 | VLSVariable _duplicate = this.support.duplicate(this.variable); | 127 | VLSVariable _duplicate = this.support.duplicate(this.variable); |
128 | _variables.add(_duplicate); | 128 | _variables.add(_duplicate); |
129 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); | 129 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); |
@@ -193,10 +193,10 @@ public class Logic2VampireLanguageMapper_ContainmentMapper { | |||
193 | it.setFofRole("axiom"); | 193 | it.setFofRole("axiom"); |
194 | VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier(); | 194 | VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier(); |
195 | final Procedure1<VLSExistentialQuantifier> _function_5 = (VLSExistentialQuantifier it_1) -> { | 195 | final Procedure1<VLSExistentialQuantifier> _function_5 = (VLSExistentialQuantifier it_1) -> { |
196 | EList<VLSVariable> _variables = it_1.getVariables(); | 196 | EList<VLSVariableDeclaration> _variables = it_1.getVariables(); |
197 | VLSVariable _duplicate = this.support.duplicate(varA); | 197 | VLSVariable _duplicate = this.support.duplicate(varA); |
198 | _variables.add(_duplicate); | 198 | _variables.add(_duplicate); |
199 | EList<VLSVariable> _variables_1 = it_1.getVariables(); | 199 | EList<VLSVariableDeclaration> _variables_1 = it_1.getVariables(); |
200 | VLSVariable _duplicate_1 = this.support.duplicate(varB); | 200 | VLSVariable _duplicate_1 = this.support.duplicate(varB); |
201 | _variables_1.add(_duplicate_1); | 201 | _variables_1.add(_duplicate_1); |
202 | VLSImplies _createVLSImplies = this.factory.createVLSImplies(); | 202 | VLSImplies _createVLSImplies = this.factory.createVLSImplies(); |
@@ -206,10 +206,10 @@ public class Logic2VampireLanguageMapper_ContainmentMapper { | |||
206 | final Procedure1<VLSUnaryNegation> _function_7 = (VLSUnaryNegation it_3) -> { | 206 | final Procedure1<VLSUnaryNegation> _function_7 = (VLSUnaryNegation it_3) -> { |
207 | VLSExistentialQuantifier _createVLSExistentialQuantifier_1 = this.factory.createVLSExistentialQuantifier(); | 207 | VLSExistentialQuantifier _createVLSExistentialQuantifier_1 = this.factory.createVLSExistentialQuantifier(); |
208 | final Procedure1<VLSExistentialQuantifier> _function_8 = (VLSExistentialQuantifier it_4) -> { | 208 | final Procedure1<VLSExistentialQuantifier> _function_8 = (VLSExistentialQuantifier it_4) -> { |
209 | EList<VLSVariable> _variables_2 = it_4.getVariables(); | 209 | EList<VLSVariableDeclaration> _variables_2 = it_4.getVariables(); |
210 | VLSVariable _duplicate_2 = this.support.duplicate(varC); | 210 | VLSVariable _duplicate_2 = this.support.duplicate(varC); |
211 | _variables_2.add(_duplicate_2); | 211 | _variables_2.add(_duplicate_2); |
212 | EList<VLSVariable> _variables_3 = it_4.getVariables(); | 212 | EList<VLSVariableDeclaration> _variables_3 = it_4.getVariables(); |
213 | VLSVariable _duplicate_3 = this.support.duplicate(varB); | 213 | VLSVariable _duplicate_3 = this.support.duplicate(varB); |
214 | _variables_3.add(_duplicate_3); | 214 | _variables_3.add(_duplicate_3); |
215 | it_4.setOperand(this.support.duplicate(rel, CollectionLiterals.<VLSVariable>newArrayList(varC, varB))); | 215 | it_4.setOperand(this.support.duplicate(rel, CollectionLiterals.<VLSVariable>newArrayList(varC, varB))); |
@@ -234,18 +234,13 @@ public class Logic2VampireLanguageMapper_ContainmentMapper { | |||
234 | Set<Map.Entry<VLSFunction, List<VLSFunction>>> _entrySet = type2cont.entrySet(); | 234 | Set<Map.Entry<VLSFunction, List<VLSFunction>>> _entrySet = type2cont.entrySet(); |
235 | for (final Map.Entry<VLSFunction, List<VLSFunction>> e : _entrySet) { | 235 | for (final Map.Entry<VLSFunction, List<VLSFunction>> e : _entrySet) { |
236 | { | 236 | { |
237 | VLSFunction _key = e.getKey(); | ||
238 | String _plus = (_key + " "); | ||
239 | List<VLSFunction> _value = e.getValue(); | ||
240 | String _plus_1 = (_plus + _value); | ||
241 | InputOutput.<String>println(_plus_1); | ||
242 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); | 237 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); |
243 | final Procedure1<VLSFofFormula> _function_4 = (VLSFofFormula it) -> { | 238 | final Procedure1<VLSFofFormula> _function_4 = (VLSFofFormula it) -> { |
244 | it.setName(this.support.toIDMultiple("containment_contained", e.getKey().getConstant().toString())); | 239 | it.setName(this.support.toIDMultiple("containment_contained", e.getKey().getConstant().toString())); |
245 | it.setFofRole("axiom"); | 240 | it.setFofRole("axiom"); |
246 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | 241 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); |
247 | final Procedure1<VLSUniversalQuantifier> _function_5 = (VLSUniversalQuantifier it_1) -> { | 242 | final Procedure1<VLSUniversalQuantifier> _function_5 = (VLSUniversalQuantifier it_1) -> { |
248 | EList<VLSVariable> _variables = it_1.getVariables(); | 243 | EList<VLSVariableDeclaration> _variables = it_1.getVariables(); |
249 | VLSVariable _duplicate = this.support.duplicate(varA); | 244 | VLSVariable _duplicate = this.support.duplicate(varA); |
250 | _variables.add(_duplicate); | 245 | _variables.add(_duplicate); |
251 | VLSImplies _createVLSImplies = this.factory.createVLSImplies(); | 246 | VLSImplies _createVLSImplies = this.factory.createVLSImplies(); |
@@ -253,7 +248,7 @@ public class Logic2VampireLanguageMapper_ContainmentMapper { | |||
253 | it_2.setLeft(this.support.duplicate(e.getKey(), varA)); | 248 | it_2.setLeft(this.support.duplicate(e.getKey(), varA)); |
254 | VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier(); | 249 | VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier(); |
255 | final Procedure1<VLSExistentialQuantifier> _function_7 = (VLSExistentialQuantifier it_3) -> { | 250 | final Procedure1<VLSExistentialQuantifier> _function_7 = (VLSExistentialQuantifier it_3) -> { |
256 | EList<VLSVariable> _variables_1 = it_3.getVariables(); | 251 | EList<VLSVariableDeclaration> _variables_1 = it_3.getVariables(); |
257 | VLSVariable _duplicate_1 = this.support.duplicate(varB); | 252 | VLSVariable _duplicate_1 = this.support.duplicate(varB); |
258 | _variables_1.add(_duplicate_1); | 253 | _variables_1.add(_duplicate_1); |
259 | int _length_1 = ((Object[])Conversions.unwrapArray(e.getValue(), Object.class)).length; | 254 | int _length_1 = ((Object[])Conversions.unwrapArray(e.getValue(), Object.class)).length; |
@@ -313,9 +308,9 @@ public class Logic2VampireLanguageMapper_ContainmentMapper { | |||
313 | final Procedure1<VLSUnaryNegation> _function_6 = (VLSUnaryNegation it_1) -> { | 308 | final Procedure1<VLSUnaryNegation> _function_6 = (VLSUnaryNegation it_1) -> { |
314 | VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier(); | 309 | VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier(); |
315 | final Procedure1<VLSExistentialQuantifier> _function_7 = (VLSExistentialQuantifier it_2) -> { | 310 | final Procedure1<VLSExistentialQuantifier> _function_7 = (VLSExistentialQuantifier it_2) -> { |
316 | EList<VLSVariable> _variables = it_2.getVariables(); | 311 | EList<VLSVariableDeclaration> _variables = it_2.getVariables(); |
317 | List<VLSVariable> _duplicate = this.support.duplicate(variables); | 312 | List<VLSVariable> _duplicate = this.support.duplicate(variables); |
318 | Iterables.<VLSVariable>addAll(_variables, _duplicate); | 313 | Iterables.<VLSVariableDeclaration>addAll(_variables, _duplicate); |
319 | it_2.setOperand(this.support.unfoldAnd(conjunctionList)); | 314 | it_2.setOperand(this.support.unfoldAnd(conjunctionList)); |
320 | }; | 315 | }; |
321 | VLSExistentialQuantifier _doubleArrow_1 = ObjectExtensions.<VLSExistentialQuantifier>operator_doubleArrow(_createVLSExistentialQuantifier, _function_7); | 316 | VLSExistentialQuantifier _doubleArrow_1 = ObjectExtensions.<VLSExistentialQuantifier>operator_doubleArrow(_createVLSExistentialQuantifier, _function_7); |
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 index c6565f6a..657c3292 100644 --- 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 | |||
@@ -9,6 +9,7 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies; | |||
9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; | 9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; |
10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; | 10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; |
11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; | 11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; |
12 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariableDeclaration; | ||
12 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; | 13 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; |
13 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference; | 14 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference; |
14 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation; | 15 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation; |
@@ -76,7 +77,7 @@ public class Logic2VampireLanguageMapper_RelationMapper { | |||
76 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | 77 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); |
77 | final Procedure1<VLSUniversalQuantifier> _function_1 = (VLSUniversalQuantifier it_1) -> { | 78 | final Procedure1<VLSUniversalQuantifier> _function_1 = (VLSUniversalQuantifier it_1) -> { |
78 | for (final VLSVariable v : relVar2VLS) { | 79 | for (final VLSVariable v : relVar2VLS) { |
79 | EList<VLSVariable> _variables = it_1.getVariables(); | 80 | EList<VLSVariableDeclaration> _variables = it_1.getVariables(); |
80 | VLSVariable _duplicate = this.support.duplicate(v); | 81 | VLSVariable _duplicate = this.support.duplicate(v); |
81 | _variables.add(_duplicate); | 82 | _variables.add(_duplicate); |
82 | } | 83 | } |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java index c2e4033b..6d4767a7 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java | |||
@@ -13,6 +13,7 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies; | |||
13 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; | 13 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; |
14 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; | 14 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; |
15 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; | 15 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; |
16 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariableDeclaration; | ||
16 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; | 17 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; |
17 | import com.google.common.base.Objects; | 18 | import com.google.common.base.Objects; |
18 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement; | 19 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement; |
@@ -244,7 +245,7 @@ public class Logic2VampireLanguageMapper_ScopeMapper { | |||
244 | it.setFofRole("axiom"); | 245 | it.setFofRole("axiom"); |
245 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | 246 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); |
246 | final Procedure1<VLSUniversalQuantifier> _function_2 = (VLSUniversalQuantifier it_1) -> { | 247 | final Procedure1<VLSUniversalQuantifier> _function_2 = (VLSUniversalQuantifier it_1) -> { |
247 | EList<VLSVariable> _variables = it_1.getVariables(); | 248 | EList<VLSVariableDeclaration> _variables = it_1.getVariables(); |
248 | VLSVariable _duplicate = this.support.duplicate(this.variable); | 249 | VLSVariable _duplicate = this.support.duplicate(this.variable); |
249 | _variables.add(_duplicate); | 250 | _variables.add(_duplicate); |
250 | VLSImplies _createVLSImplies = this.factory.createVLSImplies(); | 251 | VLSImplies _createVLSImplies = this.factory.createVLSImplies(); |
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 index f1d73bec..6cd53fae 100644 --- 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 | |||
@@ -13,6 +13,7 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSOr; | |||
13 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; | 13 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; |
14 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; | 14 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; |
15 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; | 15 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; |
16 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariableDeclaration; | ||
16 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; | 17 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; |
17 | import com.google.common.base.Objects; | 18 | import com.google.common.base.Objects; |
18 | import com.google.common.collect.Iterables; | 19 | import com.google.common.collect.Iterables; |
@@ -323,9 +324,9 @@ public class Logic2VampireLanguageMapper_Support { | |||
323 | if (isUniversal) { | 324 | if (isUniversal) { |
324 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | 325 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); |
325 | final Procedure1<VLSUniversalQuantifier> _function_1 = (VLSUniversalQuantifier it) -> { | 326 | final Procedure1<VLSUniversalQuantifier> _function_1 = (VLSUniversalQuantifier it) -> { |
326 | EList<VLSVariable> _variables = it.getVariables(); | 327 | EList<VLSVariableDeclaration> _variables = it.getVariables(); |
327 | Collection<VLSVariable> _values = variableMap.values(); | 328 | Collection<VLSVariable> _values = variableMap.values(); |
328 | Iterables.<VLSVariable>addAll(_variables, _values); | 329 | Iterables.<VLSVariableDeclaration>addAll(_variables, _values); |
329 | VLSImplies _createVLSImplies = this.factory.createVLSImplies(); | 330 | VLSImplies _createVLSImplies = this.factory.createVLSImplies(); |
330 | final Procedure1<VLSImplies> _function_2 = (VLSImplies it_1) -> { | 331 | final Procedure1<VLSImplies> _function_2 = (VLSImplies it_1) -> { |
331 | it_1.setLeft(this.unfoldAnd(typedefs)); | 332 | it_1.setLeft(this.unfoldAnd(typedefs)); |
@@ -341,9 +342,9 @@ public class Logic2VampireLanguageMapper_Support { | |||
341 | typedefs.add(mapper.transformTerm(expression.getExpression(), trace, this.withAddition(variables, variableMap))); | 342 | typedefs.add(mapper.transformTerm(expression.getExpression(), trace, this.withAddition(variables, variableMap))); |
342 | VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier(); | 343 | VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier(); |
343 | final Procedure1<VLSExistentialQuantifier> _function_2 = (VLSExistentialQuantifier it) -> { | 344 | final Procedure1<VLSExistentialQuantifier> _function_2 = (VLSExistentialQuantifier it) -> { |
344 | EList<VLSVariable> _variables = it.getVariables(); | 345 | EList<VLSVariableDeclaration> _variables = it.getVariables(); |
345 | Collection<VLSVariable> _values = variableMap.values(); | 346 | Collection<VLSVariable> _values = variableMap.values(); |
346 | Iterables.<VLSVariable>addAll(_variables, _values); | 347 | Iterables.<VLSVariableDeclaration>addAll(_variables, _values); |
347 | it.setOperand(this.unfoldAnd(typedefs)); | 348 | it.setOperand(this.unfoldAnd(typedefs)); |
348 | }; | 349 | }; |
349 | _xblockexpression_1 = ObjectExtensions.<VLSExistentialQuantifier>operator_doubleArrow(_createVLSExistentialQuantifier, _function_2); | 350 | _xblockexpression_1 = ObjectExtensions.<VLSExistentialQuantifier>operator_doubleArrow(_createVLSExistentialQuantifier, _function_2); |
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 index 73e59774..7921f204 100644 --- 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 | |||
@@ -15,6 +15,7 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; | |||
15 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUnaryNegation; | 15 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUnaryNegation; |
16 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; | 16 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; |
17 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; | 17 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; |
18 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariableDeclaration; | ||
18 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; | 19 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; |
19 | import com.google.common.base.Objects; | 20 | import com.google.common.base.Objects; |
20 | import com.google.common.collect.Iterables; | 21 | import com.google.common.collect.Iterables; |
@@ -143,7 +144,7 @@ public class Logic2VampireLanguageMapper_TypeMapper { | |||
143 | it.setFofRole("axiom"); | 144 | it.setFofRole("axiom"); |
144 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | 145 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); |
145 | final Procedure1<VLSUniversalQuantifier> _function_3 = (VLSUniversalQuantifier it_1) -> { | 146 | final Procedure1<VLSUniversalQuantifier> _function_3 = (VLSUniversalQuantifier it_1) -> { |
146 | EList<VLSVariable> _variables = it_1.getVariables(); | 147 | EList<VLSVariableDeclaration> _variables = it_1.getVariables(); |
147 | VLSVariable _duplicate = this.support.duplicate(variable); | 148 | VLSVariable _duplicate = this.support.duplicate(variable); |
148 | _variables.add(_duplicate); | 149 | _variables.add(_duplicate); |
149 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); | 150 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); |
@@ -193,7 +194,7 @@ public class Logic2VampireLanguageMapper_TypeMapper { | |||
193 | it.setFofRole("axiom"); | 194 | it.setFofRole("axiom"); |
194 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | 195 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); |
195 | final Procedure1<VLSUniversalQuantifier> _function_5 = (VLSUniversalQuantifier it_1) -> { | 196 | final Procedure1<VLSUniversalQuantifier> _function_5 = (VLSUniversalQuantifier it_1) -> { |
196 | EList<VLSVariable> _variables = it_1.getVariables(); | 197 | EList<VLSVariableDeclaration> _variables = it_1.getVariables(); |
197 | VLSVariable _duplicate = this.support.duplicate(variable); | 198 | VLSVariable _duplicate = this.support.duplicate(variable); |
198 | _variables.add(_duplicate); | 199 | _variables.add(_duplicate); |
199 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); | 200 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); |
@@ -263,7 +264,7 @@ public class Logic2VampireLanguageMapper_TypeMapper { | |||
263 | it.setFofRole("axiom"); | 264 | it.setFofRole("axiom"); |
264 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | 265 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); |
265 | final Procedure1<VLSUniversalQuantifier> _function_5 = (VLSUniversalQuantifier it_1) -> { | 266 | final Procedure1<VLSUniversalQuantifier> _function_5 = (VLSUniversalQuantifier it_1) -> { |
266 | EList<VLSVariable> _variables = it_1.getVariables(); | 267 | EList<VLSVariableDeclaration> _variables = it_1.getVariables(); |
267 | VLSVariable _duplicate = this.support.duplicate(variable); | 268 | VLSVariable _duplicate = this.support.duplicate(variable); |
268 | _variables.add(_duplicate); | 269 | _variables.add(_duplicate); |
269 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); | 270 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); |
@@ -291,7 +292,7 @@ public class Logic2VampireLanguageMapper_TypeMapper { | |||
291 | it.setFofRole("axiom"); | 292 | it.setFofRole("axiom"); |
292 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | 293 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); |
293 | final Procedure1<VLSUniversalQuantifier> _function_6 = (VLSUniversalQuantifier it_1) -> { | 294 | final Procedure1<VLSUniversalQuantifier> _function_6 = (VLSUniversalQuantifier it_1) -> { |
294 | EList<VLSVariable> _variables = it_1.getVariables(); | 295 | EList<VLSVariableDeclaration> _variables = it_1.getVariables(); |
295 | VLSVariable _duplicate = this.support.duplicate(variable); | 296 | VLSVariable _duplicate = this.support.duplicate(variable); |
296 | _variables.add(_duplicate); | 297 | _variables.add(_duplicate); |
297 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); | 298 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); |
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 1479e6b7..7f6ce1c6 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,59 +1,55 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; | 1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; |
2 | 2 | ||
3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration; | 3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration; |
4 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSComment; | ||
4 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel; | 5 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel; |
5 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguageFactoryImpl; | 6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireModelImpl; |
6 | import com.google.common.base.Objects; | 7 | import com.google.common.base.Objects; |
7 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace; | 8 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace; |
8 | import java.io.BufferedReader; | 9 | import java.io.BufferedReader; |
9 | import java.io.InputStream; | 10 | import java.io.InputStream; |
10 | import java.io.InputStreamReader; | 11 | import java.io.InputStreamReader; |
11 | import java.util.List; | 12 | import java.util.List; |
12 | import java.util.Map; | ||
13 | import org.eclipse.emf.common.util.EList; | 13 | import org.eclipse.emf.common.util.EList; |
14 | import org.eclipse.emf.common.util.URI; | 14 | import org.eclipse.emf.common.util.URI; |
15 | import org.eclipse.emf.ecore.EObject; | 15 | import org.eclipse.emf.ecore.EObject; |
16 | import org.eclipse.emf.ecore.resource.Resource; | ||
17 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; | 16 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; |
18 | import org.eclipse.xtext.xbase.lib.Conversions; | 17 | import org.eclipse.xtext.xbase.lib.Conversions; |
19 | import org.eclipse.xtext.xbase.lib.Exceptions; | 18 | import org.eclipse.xtext.xbase.lib.Exceptions; |
19 | import org.eclipse.xtext.xbase.lib.InputOutput; | ||
20 | 20 | ||
21 | @SuppressWarnings("all") | 21 | @SuppressWarnings("all") |
22 | public class VampireHandler { | 22 | public class VampireHandler { |
23 | public EList<EObject> callSolver(final VampireModel problem, final ReasonerWorkspace workspace, final VampireSolverConfiguration configuration) { | 23 | public EList<EObject> callSolver(final VampireModel problem, final ReasonerWorkspace workspace, final VampireSolverConfiguration configuration) { |
24 | try { | 24 | try { |
25 | EList<EObject> _xblockexpression = null; | 25 | final String CMD = "cmd /c "; |
26 | { | 26 | final String VAMPDIR = "..\\..\\Solvers\\Vampire-Solver\\ca.mcgill.ecse.dslreasoner.vampire.reasoner\\lib\\"; |
27 | final String CMD = "cmd /c "; | 27 | final String VAMPNAME = "vampire.exe"; |
28 | final String VAMPDIR = "..\\..\\Solvers\\Vampire-Solver\\ca.mcgill.ecse.dslreasoner.vampire.reasoner\\lib\\"; | 28 | final String TEMPNAME = "TEMP.tptp"; |
29 | final String VAMPNAME = "vampire.exe"; | 29 | final String OPTION = " --mode casc_sat "; |
30 | final String TEMPNAME = "TEMP.tptp"; | 30 | final String SOLNNAME = "solution.tptp"; |
31 | final String OPTION = " --mode casc_sat "; | 31 | final String PATH = "C:/cygwin64/bin"; |
32 | final String SOLNNAME = "solution.tptp"; | 32 | final URI wsURI = workspace.getWorkspaceURI(); |
33 | final String PATH = "C:/cygwin64/bin"; | 33 | final String tempLoc = (wsURI + TEMPNAME); |
34 | final URI wsURI = workspace.getWorkspaceURI(); | 34 | String _plus = (wsURI + SOLNNAME); |
35 | final String tempLoc = (wsURI + TEMPNAME); | 35 | final String solnLoc = (_plus + " "); |
36 | String _plus = (wsURI + SOLNNAME); | 36 | final String vampLoc = (VAMPDIR + VAMPNAME); |
37 | final String solnLoc = (_plus + " "); | 37 | String tempURI = workspace.writeModel(problem, TEMPNAME).toFileString(); |
38 | final String vampLoc = (VAMPDIR + VAMPNAME); | 38 | final Process p = Runtime.getRuntime().exec((((((CMD + vampLoc) + OPTION) + tempLoc) + " > ") + solnLoc), ((String[])Conversions.unwrapArray(CollectionLiterals.<String>newArrayList(("Path=" + PATH)), String.class))); |
39 | String tempURI = workspace.writeModel(problem, TEMPNAME).toFileString(); | 39 | p.waitFor(); |
40 | final Process p = Runtime.getRuntime().exec((((((CMD + vampLoc) + OPTION) + tempLoc) + " > ") + solnLoc), ((String[])Conversions.unwrapArray(CollectionLiterals.<String>newArrayList(("Path=" + PATH)), String.class))); | 40 | InputStream _inputStream = p.getInputStream(); |
41 | p.waitFor(); | 41 | InputStreamReader _inputStreamReader = new InputStreamReader(_inputStream); |
42 | InputStream _inputStream = p.getInputStream(); | 42 | final BufferedReader reader = new BufferedReader(_inputStreamReader); |
43 | InputStreamReader _inputStreamReader = new InputStreamReader(_inputStream); | 43 | final List<String> output = CollectionLiterals.<String>newArrayList(); |
44 | final BufferedReader reader = new BufferedReader(_inputStreamReader); | 44 | String line = ""; |
45 | final List<String> output = CollectionLiterals.<String>newArrayList(); | 45 | while ((!Objects.equal((line = reader.readLine()), null))) { |
46 | String line = ""; | 46 | output.add((line + "\n")); |
47 | while ((!Objects.equal((line = reader.readLine()), null))) { | ||
48 | output.add((line + "\n")); | ||
49 | } | ||
50 | workspace.getFile(TEMPNAME).delete(); | ||
51 | Map<String, Object> _extensionToFactoryMap = Resource.Factory.Registry.INSTANCE.getExtensionToFactoryMap(); | ||
52 | VampireLanguageFactoryImpl _vampireLanguageFactoryImpl = new VampireLanguageFactoryImpl(); | ||
53 | _extensionToFactoryMap.put("*", _vampireLanguageFactoryImpl); | ||
54 | _xblockexpression = workspace.<VampireModel>readModel(VampireModel.class, SOLNNAME).eResource().getContents(); | ||
55 | } | 47 | } |
56 | return _xblockexpression; | 48 | workspace.getFile(TEMPNAME).delete(); |
49 | final EList<EObject> root = workspace.<VampireModel>readModel(VampireModel.class, SOLNNAME).eResource().getContents(); | ||
50 | EObject _get = root.get(0); | ||
51 | InputOutput.<EList<VLSComment>>println(((VampireModelImpl) _get).getComments()); | ||
52 | return root; | ||
57 | } catch (Throwable _e) { | 53 | } catch (Throwable _e) { |
58 | throw Exceptions.sneakyThrow(_e); | 54 | throw Exceptions.sneakyThrow(_e); |
59 | } | 55 | } |