From 15602c7cfbfc80b8c826855b94c9f9582650dd21 Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Thu, 29 Aug 2019 06:26:02 -0400 Subject: VAMPIRE: adapt grammar to Vampire solution + get model from text --- .../vampire/reasoner/.VampireSolver.xtendbin | Bin 6386 -> 6465 bytes .../builder/.Logic2VampireLanguageMapper.xtendbin | Bin 18150 -> 17754 bytes .../.Logic2VampireLanguageMapperTrace.xtendbin | Bin 4656 -> 4692 bytes ...c2VampireLanguageMapper_ConstantMapper.xtendbin | Bin 3164 -> 3164 bytes ...ampireLanguageMapper_ContainmentMapper.xtendbin | Bin 11904 -> 11835 bytes ...c2VampireLanguageMapper_RelationMapper.xtendbin | Bin 6454 -> 6497 bytes ...ogic2VampireLanguageMapper_ScopeMapper.xtendbin | Bin 10667 -> 10701 bytes .../.Logic2VampireLanguageMapper_Support.xtendbin | Bin 13048 -> 13083 bytes ...Logic2VampireLanguageMapper_TypeMapper.xtendbin | Bin 11136 -> 11170 bytes .../reasoner/builder/.VampireHandler.xtendbin | Bin 6553 -> 6445 bytes .../builder/Logic2VampireLanguageMapper.java | 14 +---- ...ic2VampireLanguageMapper_ContainmentMapper.java | 25 ++++---- ...Logic2VampireLanguageMapper_RelationMapper.java | 3 +- .../Logic2VampireLanguageMapper_ScopeMapper.java | 3 +- .../Logic2VampireLanguageMapper_Support.java | 9 +-- .../Logic2VampireLanguageMapper_TypeMapper.java | 9 +-- .../vampire/reasoner/builder/VampireHandler.java | 64 ++++++++++----------- 17 files changed, 55 insertions(+), 72 deletions(-) (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner') 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 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin 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 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin 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 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin 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 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin 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 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin 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 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin 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 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin 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 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin 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 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin 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 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin 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; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSInt; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSReal; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUnaryNegation; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; @@ -44,7 +43,6 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.InstanceOf; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntLiteral; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Not; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Or; -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealLiteral; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition; @@ -98,7 +96,7 @@ public class Logic2VampireLanguageMapper { public TracedOutput transformProblem(final LogicProblem problem, final VampireSolverConfiguration config) { VLSComment _createVLSComment = this.factory.createVLSComment(); final Procedure1 _function = (VLSComment it) -> { - it.setComment("This is an initial Test Comment"); + it.setComment("%This is an initial Test Comment"); }; final VLSComment initialComment = ObjectExtensions.operator_doubleArrow(_createVLSComment, _function); VampireModel _createVampireModel = this.factory.createVampireModel(); @@ -202,14 +200,6 @@ public class Logic2VampireLanguageMapper { return ObjectExtensions.operator_doubleArrow(_createVLSInt, _function); } - protected VLSTerm _transformTerm(final RealLiteral literal, final Logic2VampireLanguageMapperTrace trace, final Map variables) { - VLSReal _createVLSReal = this.factory.createVLSReal(); - final Procedure1 _function = (VLSReal it) -> { - it.setValue(literal.getValue().toString()); - }; - return ObjectExtensions.operator_doubleArrow(_createVLSReal, _function); - } - protected VLSTerm _transformTerm(final Not not, final Logic2VampireLanguageMapperTrace trace, final Map variables) { VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); final Procedure1 _function = (VLSUnaryNegation it) -> { @@ -394,8 +384,6 @@ public class Logic2VampireLanguageMapper { return _transformTerm((Not)and, trace, variables); } else if (and instanceof Or) { return _transformTerm((Or)and, trace, variables); - } else if (and instanceof RealLiteral) { - return _transformTerm((RealLiteral)and, trace, variables); } else if (and instanceof InstanceOf) { return _transformTerm((InstanceOf)and, trace, variables); } 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; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUnaryNegation; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariableDeclaration; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; import com.google.common.base.Objects; import com.google.common.collect.Iterables; @@ -37,7 +38,6 @@ import org.eclipse.emf.common.util.EList; import org.eclipse.xtext.xbase.lib.CollectionLiterals; import org.eclipse.xtext.xbase.lib.Conversions; import org.eclipse.xtext.xbase.lib.Extension; -import org.eclipse.xtext.xbase.lib.InputOutput; import org.eclipse.xtext.xbase.lib.ObjectExtensions; import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; @@ -123,7 +123,7 @@ public class Logic2VampireLanguageMapper_ContainmentMapper { it.setFofRole("axiom"); VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); final Procedure1 _function_1 = (VLSUniversalQuantifier it_1) -> { - EList _variables = it_1.getVariables(); + EList _variables = it_1.getVariables(); VLSVariable _duplicate = this.support.duplicate(this.variable); _variables.add(_duplicate); VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); @@ -193,10 +193,10 @@ public class Logic2VampireLanguageMapper_ContainmentMapper { it.setFofRole("axiom"); VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier(); final Procedure1 _function_5 = (VLSExistentialQuantifier it_1) -> { - EList _variables = it_1.getVariables(); + EList _variables = it_1.getVariables(); VLSVariable _duplicate = this.support.duplicate(varA); _variables.add(_duplicate); - EList _variables_1 = it_1.getVariables(); + EList _variables_1 = it_1.getVariables(); VLSVariable _duplicate_1 = this.support.duplicate(varB); _variables_1.add(_duplicate_1); VLSImplies _createVLSImplies = this.factory.createVLSImplies(); @@ -206,10 +206,10 @@ public class Logic2VampireLanguageMapper_ContainmentMapper { final Procedure1 _function_7 = (VLSUnaryNegation it_3) -> { VLSExistentialQuantifier _createVLSExistentialQuantifier_1 = this.factory.createVLSExistentialQuantifier(); final Procedure1 _function_8 = (VLSExistentialQuantifier it_4) -> { - EList _variables_2 = it_4.getVariables(); + EList _variables_2 = it_4.getVariables(); VLSVariable _duplicate_2 = this.support.duplicate(varC); _variables_2.add(_duplicate_2); - EList _variables_3 = it_4.getVariables(); + EList _variables_3 = it_4.getVariables(); VLSVariable _duplicate_3 = this.support.duplicate(varB); _variables_3.add(_duplicate_3); it_4.setOperand(this.support.duplicate(rel, CollectionLiterals.newArrayList(varC, varB))); @@ -234,18 +234,13 @@ public class Logic2VampireLanguageMapper_ContainmentMapper { Set>> _entrySet = type2cont.entrySet(); for (final Map.Entry> e : _entrySet) { { - VLSFunction _key = e.getKey(); - String _plus = (_key + " "); - List _value = e.getValue(); - String _plus_1 = (_plus + _value); - InputOutput.println(_plus_1); VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); final Procedure1 _function_4 = (VLSFofFormula it) -> { it.setName(this.support.toIDMultiple("containment_contained", e.getKey().getConstant().toString())); it.setFofRole("axiom"); VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); final Procedure1 _function_5 = (VLSUniversalQuantifier it_1) -> { - EList _variables = it_1.getVariables(); + EList _variables = it_1.getVariables(); VLSVariable _duplicate = this.support.duplicate(varA); _variables.add(_duplicate); VLSImplies _createVLSImplies = this.factory.createVLSImplies(); @@ -253,7 +248,7 @@ public class Logic2VampireLanguageMapper_ContainmentMapper { it_2.setLeft(this.support.duplicate(e.getKey(), varA)); VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier(); final Procedure1 _function_7 = (VLSExistentialQuantifier it_3) -> { - EList _variables_1 = it_3.getVariables(); + EList _variables_1 = it_3.getVariables(); VLSVariable _duplicate_1 = this.support.duplicate(varB); _variables_1.add(_duplicate_1); int _length_1 = ((Object[])Conversions.unwrapArray(e.getValue(), Object.class)).length; @@ -313,9 +308,9 @@ public class Logic2VampireLanguageMapper_ContainmentMapper { final Procedure1 _function_6 = (VLSUnaryNegation it_1) -> { VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier(); final Procedure1 _function_7 = (VLSExistentialQuantifier it_2) -> { - EList _variables = it_2.getVariables(); + EList _variables = it_2.getVariables(); List _duplicate = this.support.duplicate(variables); - Iterables.addAll(_variables, _duplicate); + Iterables.addAll(_variables, _duplicate); it_2.setOperand(this.support.unfoldAnd(conjunctionList)); }; VLSExistentialQuantifier _doubleArrow_1 = ObjectExtensions.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; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariableDeclaration; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation; @@ -76,7 +77,7 @@ public class Logic2VampireLanguageMapper_RelationMapper { VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); final Procedure1 _function_1 = (VLSUniversalQuantifier it_1) -> { for (final VLSVariable v : relVar2VLS) { - EList _variables = it_1.getVariables(); + EList _variables = it_1.getVariables(); VLSVariable _duplicate = this.support.duplicate(v); _variables.add(_duplicate); } 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; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariableDeclaration; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; import com.google.common.base.Objects; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement; @@ -244,7 +245,7 @@ public class Logic2VampireLanguageMapper_ScopeMapper { it.setFofRole("axiom"); VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); final Procedure1 _function_2 = (VLSUniversalQuantifier it_1) -> { - EList _variables = it_1.getVariables(); + EList _variables = it_1.getVariables(); VLSVariable _duplicate = this.support.duplicate(this.variable); _variables.add(_duplicate); 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; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariableDeclaration; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; import com.google.common.base.Objects; import com.google.common.collect.Iterables; @@ -323,9 +324,9 @@ public class Logic2VampireLanguageMapper_Support { if (isUniversal) { VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); final Procedure1 _function_1 = (VLSUniversalQuantifier it) -> { - EList _variables = it.getVariables(); + EList _variables = it.getVariables(); Collection _values = variableMap.values(); - Iterables.addAll(_variables, _values); + Iterables.addAll(_variables, _values); VLSImplies _createVLSImplies = this.factory.createVLSImplies(); final Procedure1 _function_2 = (VLSImplies it_1) -> { it_1.setLeft(this.unfoldAnd(typedefs)); @@ -341,9 +342,9 @@ public class Logic2VampireLanguageMapper_Support { typedefs.add(mapper.transformTerm(expression.getExpression(), trace, this.withAddition(variables, variableMap))); VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier(); final Procedure1 _function_2 = (VLSExistentialQuantifier it) -> { - EList _variables = it.getVariables(); + EList _variables = it.getVariables(); Collection _values = variableMap.values(); - Iterables.addAll(_variables, _values); + Iterables.addAll(_variables, _values); it.setOperand(this.unfoldAnd(typedefs)); }; _xblockexpression_1 = ObjectExtensions.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; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUnaryNegation; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariableDeclaration; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; import com.google.common.base.Objects; import com.google.common.collect.Iterables; @@ -143,7 +144,7 @@ public class Logic2VampireLanguageMapper_TypeMapper { it.setFofRole("axiom"); VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); final Procedure1 _function_3 = (VLSUniversalQuantifier it_1) -> { - EList _variables = it_1.getVariables(); + EList _variables = it_1.getVariables(); VLSVariable _duplicate = this.support.duplicate(variable); _variables.add(_duplicate); VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); @@ -193,7 +194,7 @@ public class Logic2VampireLanguageMapper_TypeMapper { it.setFofRole("axiom"); VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); final Procedure1 _function_5 = (VLSUniversalQuantifier it_1) -> { - EList _variables = it_1.getVariables(); + EList _variables = it_1.getVariables(); VLSVariable _duplicate = this.support.duplicate(variable); _variables.add(_duplicate); VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); @@ -263,7 +264,7 @@ public class Logic2VampireLanguageMapper_TypeMapper { it.setFofRole("axiom"); VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); final Procedure1 _function_5 = (VLSUniversalQuantifier it_1) -> { - EList _variables = it_1.getVariables(); + EList _variables = it_1.getVariables(); VLSVariable _duplicate = this.support.duplicate(variable); _variables.add(_duplicate); VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); @@ -291,7 +292,7 @@ public class Logic2VampireLanguageMapper_TypeMapper { it.setFofRole("axiom"); VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); final Procedure1 _function_6 = (VLSUniversalQuantifier it_1) -> { - EList _variables = it_1.getVariables(); + EList _variables = it_1.getVariables(); VLSVariable _duplicate = this.support.duplicate(variable); _variables.add(_duplicate); 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 @@ package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSComment; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireLanguageFactoryImpl; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.impl.VampireModelImpl; import com.google.common.base.Objects; import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace; import java.io.BufferedReader; import java.io.InputStream; import java.io.InputStreamReader; import java.util.List; -import java.util.Map; import org.eclipse.emf.common.util.EList; import org.eclipse.emf.common.util.URI; import org.eclipse.emf.ecore.EObject; -import org.eclipse.emf.ecore.resource.Resource; import org.eclipse.xtext.xbase.lib.CollectionLiterals; import org.eclipse.xtext.xbase.lib.Conversions; import org.eclipse.xtext.xbase.lib.Exceptions; +import org.eclipse.xtext.xbase.lib.InputOutput; @SuppressWarnings("all") public class VampireHandler { public EList callSolver(final VampireModel problem, final ReasonerWorkspace workspace, final VampireSolverConfiguration configuration) { try { - EList _xblockexpression = null; - { - final String CMD = "cmd /c "; - final String VAMPDIR = "..\\..\\Solvers\\Vampire-Solver\\ca.mcgill.ecse.dslreasoner.vampire.reasoner\\lib\\"; - final String VAMPNAME = "vampire.exe"; - final String TEMPNAME = "TEMP.tptp"; - final String OPTION = " --mode casc_sat "; - final String SOLNNAME = "solution.tptp"; - final String PATH = "C:/cygwin64/bin"; - final URI wsURI = workspace.getWorkspaceURI(); - final String tempLoc = (wsURI + TEMPNAME); - String _plus = (wsURI + SOLNNAME); - final String solnLoc = (_plus + " "); - final String vampLoc = (VAMPDIR + VAMPNAME); - String tempURI = workspace.writeModel(problem, TEMPNAME).toFileString(); - final Process p = Runtime.getRuntime().exec((((((CMD + vampLoc) + OPTION) + tempLoc) + " > ") + solnLoc), ((String[])Conversions.unwrapArray(CollectionLiterals.newArrayList(("Path=" + PATH)), String.class))); - p.waitFor(); - InputStream _inputStream = p.getInputStream(); - InputStreamReader _inputStreamReader = new InputStreamReader(_inputStream); - final BufferedReader reader = new BufferedReader(_inputStreamReader); - final List output = CollectionLiterals.newArrayList(); - String line = ""; - while ((!Objects.equal((line = reader.readLine()), null))) { - output.add((line + "\n")); - } - workspace.getFile(TEMPNAME).delete(); - Map _extensionToFactoryMap = Resource.Factory.Registry.INSTANCE.getExtensionToFactoryMap(); - VampireLanguageFactoryImpl _vampireLanguageFactoryImpl = new VampireLanguageFactoryImpl(); - _extensionToFactoryMap.put("*", _vampireLanguageFactoryImpl); - _xblockexpression = workspace.readModel(VampireModel.class, SOLNNAME).eResource().getContents(); + final String CMD = "cmd /c "; + final String VAMPDIR = "..\\..\\Solvers\\Vampire-Solver\\ca.mcgill.ecse.dslreasoner.vampire.reasoner\\lib\\"; + final String VAMPNAME = "vampire.exe"; + final String TEMPNAME = "TEMP.tptp"; + final String OPTION = " --mode casc_sat "; + final String SOLNNAME = "solution.tptp"; + final String PATH = "C:/cygwin64/bin"; + final URI wsURI = workspace.getWorkspaceURI(); + final String tempLoc = (wsURI + TEMPNAME); + String _plus = (wsURI + SOLNNAME); + final String solnLoc = (_plus + " "); + final String vampLoc = (VAMPDIR + VAMPNAME); + String tempURI = workspace.writeModel(problem, TEMPNAME).toFileString(); + final Process p = Runtime.getRuntime().exec((((((CMD + vampLoc) + OPTION) + tempLoc) + " > ") + solnLoc), ((String[])Conversions.unwrapArray(CollectionLiterals.newArrayList(("Path=" + PATH)), String.class))); + p.waitFor(); + InputStream _inputStream = p.getInputStream(); + InputStreamReader _inputStreamReader = new InputStreamReader(_inputStream); + final BufferedReader reader = new BufferedReader(_inputStreamReader); + final List output = CollectionLiterals.newArrayList(); + String line = ""; + while ((!Objects.equal((line = reader.readLine()), null))) { + output.add((line + "\n")); } - return _xblockexpression; + workspace.getFile(TEMPNAME).delete(); + final EList root = workspace.readModel(VampireModel.class, SOLNNAME).eResource().getContents(); + EObject _get = root.get(0); + InputOutput.>println(((VampireModelImpl) _get).getComments()); + return root; } catch (Throwable _e) { throw Exceptions.sneakyThrow(_e); } -- cgit v1.2.3-54-g00ecf