diff options
author | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-08-29 06:26:02 -0400 |
---|---|---|
committer | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2020-06-07 19:41:39 -0400 |
commit | 15602c7cfbfc80b8c826855b94c9f9582650dd21 (patch) | |
tree | 3f90d5812e68215838efd52372bcc26df88b9033 /Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java | |
parent | VAMPIRE: integrate local Vampire executeable #32 (diff) | |
download | VIATRA-Generator-15602c7cfbfc80b8c826855b94c9f9582650dd21.tar.gz VIATRA-Generator-15602c7cfbfc80b8c826855b94c9f9582650dd21.tar.zst VIATRA-Generator-15602c7cfbfc80b8c826855b94c9f9582650dd21.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/builder/Logic2VampireLanguageMapper.java')
-rw-r--r-- | Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java | 14 |
1 files changed, 1 insertions, 13 deletions
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) { |