From edfd98b8fca74489ae338077f43521b6c5e6606f Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Wed, 6 Mar 2019 02:59:19 -0500 Subject: Continue improving code style (need sleep) --- .../builder/.Logic2VampireLanguageMapper.xtendbin | Bin 18008 -> 17847 bytes .../.Logic2VampireLanguageMapperTrace.xtendbin | Bin 3708 -> 3708 bytes ...c2VampireLanguageMapper_ConstantMapper.xtendbin | Bin 3164 -> 3164 bytes ...c2VampireLanguageMapper_RelationMapper.xtendbin | Bin 8177 -> 8207 bytes ...ogic2VampireLanguageMapper_ScopeMapper.xtendbin | Bin 6096 -> 6096 bytes .../.Logic2VampireLanguageMapper_Support.xtendbin | Bin 11367 -> 10926 bytes ...Logic2VampireLanguageMapper_TypeMapper.xtendbin | Bin 3223 -> 3223 bytes ...geMapper_TypeMapperTrace_FilteredTypes.xtendbin | Bin 2643 -> 2643 bytes ...anguageMapper_TypeMapper_FilteredTypes.xtendbin | Bin 8565 -> 8564 bytes .../reasoner/builder/.Vampire2LogicMapper.xtendbin | Bin 1720 -> 1720 bytes .../reasoner/builder/.VampireHandler.xtendbin | Bin 4908 -> 4908 bytes ...ModelInterpretation_TypeInterpretation.xtendbin | Bin 1491 -> 1491 bytes ...ation_TypeInterpretation_FilteredTypes.xtendbin | Bin 1688 -> 1688 bytes .../builder/Logic2VampireLanguageMapper.java | 16 ++-- ...Logic2VampireLanguageMapper_RelationMapper.java | 36 ++++---- .../Logic2VampireLanguageMapper_Support.java | 102 +++++++-------------- 16 files changed, 55 insertions(+), 99 deletions(-) (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder') 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 5fc0da27..f0cd1c7c 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 562b9bbf..7d15db96 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 dd7bdf86..8fed8f56 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_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 496d27b3..a40e27e4 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 4a03f2ce..4b6b4a1e 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 511f4a1f..c3035658 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 37e9480c..2e21736e 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/.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtendbin index f473c4bc..e870dabc 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.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_FilteredTypes.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtendbin index e53791d6..ed198ef6 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtendbin 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 1b112c56..83697125 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.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 c8284658..063650c5 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/.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 89d4c657..e36d2270 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin 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 3c98bd64..5e5be153 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.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 6643576f..dc2cd5ec 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 @@ -50,6 +50,7 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicDeclaration; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term; +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable; import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem; @@ -262,18 +263,18 @@ public class Logic2VampireLanguageMapper { } protected VLSTerm _transformTerm(final Forall forall, final Logic2VampireLanguageMapperTrace trace, final Map variables) { - return this.support.createUniversallyQuantifiedExpression(this, forall, trace, variables); + return this.support.createQuantifiedExpression(this, forall, trace, variables, true); } protected VLSTerm _transformTerm(final Exists exists, final Logic2VampireLanguageMapperTrace trace, final Map variables) { - return this.support.createExistentiallyQuantifiedExpression(this, exists, trace, variables); + return this.support.createQuantifiedExpression(this, exists, trace, variables, false); } protected VLSTerm _transformTerm(final InstanceOf instanceOf, final Logic2VampireLanguageMapperTrace trace, final Map variables) { VLSFunction _createVLSFunction = this.factory.createVLSFunction(); final Procedure1 _function = (VLSFunction it) -> { TypeReference _range = instanceOf.getRange(); - it.setConstant(this.support.toIDMultiple("t", ((ComplexTypeReference) _range).getReferred().getName())); + it.setConstant(CollectionsUtil.lookup(((ComplexTypeReference) _range).getReferred(), trace.type2Predicate).getConstant()); EList _terms = it.getTerms(); VLSTerm _transformTerm = this.transformTerm(instanceOf.getValue(), trace, variables); _terms.add(_transformTerm); @@ -303,12 +304,7 @@ public class Logic2VampireLanguageMapper { } protected VLSTerm _transformSymbolicReference(final Variable variable, final List parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map variables) { - VLSVariable _createVLSVariable = this.factory.createVLSVariable(); - final Procedure1 _function = (VLSVariable it) -> { - it.setName(this.support.toID(CollectionsUtil.lookup(variable, variables).getName())); - }; - final VLSVariable res = ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function); - return res; + return this.support.duplicate(CollectionsUtil.lookup(variable, variables)); } protected VLSTerm _transformSymbolicReference(final FunctionDeclaration function, final List parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map variables) { @@ -359,7 +355,7 @@ public class Logic2VampireLanguageMapper { protected VLSTerm _transformSymbolicReference(final Relation relation, final List parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map variables) { VLSFunction _createVLSFunction = this.factory.createVLSFunction(); final Procedure1 _function = (VLSFunction it) -> { - it.setConstant(this.support.toIDMultiple("rel", relation.getName())); + it.setConstant(CollectionsUtil.lookup(((RelationDeclaration) relation), trace.rel2Predicate).getConstant()); EList _terms = it.getTerms(); final Function1 _function_1 = (Term p) -> { return this.transformTerm(p, trace, variables); 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 4f5c6acc..d5745333 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 @@ -48,7 +48,6 @@ public class Logic2VampireLanguageMapper_RelationMapper { public void _transformRelation(final RelationDeclaration r, final Logic2VampireLanguageMapperTrace trace) { final List relVar2VLS = new ArrayList(); final List relVar2TypeDecComply = new ArrayList(); - final ArrayList typedefs = new ArrayList(); int _length = ((Object[])Conversions.unwrapArray(r.getParameters(), Object.class)).length; ExclusiveRange _doubleDotLessThan = new ExclusiveRange(0, _length, true); for (final Integer i : _doubleDotLessThan) { @@ -68,8 +67,7 @@ public class Logic2VampireLanguageMapper_RelationMapper { VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); final Procedure1 _function = (VLSFofFormula it) -> { final String[] nameArray = r.getName().split(" "); - it.setName(this.support.toIDMultiple("compliance", nameArray[0], - nameArray[2])); + it.setName(this.support.toIDMultiple("compliance", nameArray[0], nameArray[2])); it.setFofRole("axiom"); VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); final Procedure1 _function_1 = (VLSUniversalQuantifier it_1) -> { @@ -82,23 +80,16 @@ public class Logic2VampireLanguageMapper_RelationMapper { final Procedure1 _function_2 = (VLSImplies it_2) -> { VLSFunction _createVLSFunction = this.factory.createVLSFunction(); final Procedure1 _function_3 = (VLSFunction it_3) -> { - it_3.setConstant(this.support.toIDMultiple("rel", r.getName())); - int _length_1 = ((Object[])Conversions.unwrapArray(r.getParameters(), Object.class)).length; - ExclusiveRange _doubleDotLessThan_1 = new ExclusiveRange(0, _length_1, true); - for (final Integer i_1 : _doubleDotLessThan_1) { - { - VLSVariable _createVLSVariable = this.factory.createVLSVariable(); - final Procedure1 _function_4 = (VLSVariable it_4) -> { - it_4.setName(relVar2VLS.get((i_1).intValue()).getName()); - }; - final VLSVariable v_1 = ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function_4); - EList _terms = it_3.getTerms(); - _terms.add(v_1); - } + it_3.setConstant(this.support.toIDMultiple("r", nameArray[0], nameArray[2])); + for (final VLSVariable v_1 : relVar2VLS) { + EList _terms = it_3.getTerms(); + VLSVariable _duplicate_1 = this.support.duplicate(v_1); + _terms.add(_duplicate_1); } }; - VLSFunction _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function_3); - it_2.setLeft(_doubleArrow); + final VLSFunction rel = ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function_3); + trace.rel2Predicate.put(r, rel); + it_2.setLeft(this.support.duplicate(rel)); it_2.setRight(this.support.unfoldAnd(relVar2TypeDecComply)); }; VLSImplies _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSImplies, _function_2); @@ -139,9 +130,9 @@ public class Logic2VampireLanguageMapper_RelationMapper { relationVar2TypeDecRes.put(variable, this.support.duplicate(varTypeComply)); } } + final String[] nameArray = reldef.getName().split(" "); VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); final Procedure1 _function = (VLSFofFormula it) -> { - final String[] nameArray = reldef.getName().split(" "); int _length = nameArray.length; int _minus = (_length - 2); int _length_1 = nameArray.length; @@ -190,7 +181,12 @@ public class Logic2VampireLanguageMapper_RelationMapper { final VLSFofFormula comply = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula, _function); VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); final Procedure1 _function_1 = (VLSFofFormula it) -> { - it.setName(this.support.toIDMultiple("relation", reldef.getName())); + int _length = nameArray.length; + int _minus = (_length - 2); + int _length_1 = nameArray.length; + int _minus_1 = (_length_1 - 1); + it.setName(this.support.toIDMultiple("relation", nameArray[_minus], + nameArray[_minus_1])); it.setFofRole("axiom"); VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); final Procedure1 _function_2 = (VLSUniversalQuantifier it_1) -> { 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 35497eab..72ca44e9 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 @@ -20,6 +20,7 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable; +import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; import java.util.ArrayList; import java.util.Collection; import java.util.HashMap; @@ -220,13 +221,13 @@ public class Logic2VampireLanguageMapper_Support { * ids.map[it.split("\\s+").join("'")].join("'") * } */ - protected VLSTerm createUniversallyQuantifiedExpression(final Logic2VampireLanguageMapper mapper, final QuantifiedExpression expression, final Logic2VampireLanguageMapperTrace trace, final Map variables) { - VLSUniversalQuantifier _xblockexpression = null; + protected VLSTerm createQuantifiedExpression(final Logic2VampireLanguageMapper mapper, final QuantifiedExpression expression, final Logic2VampireLanguageMapperTrace trace, final Map variables, final boolean isUniversal) { + VLSTerm _xblockexpression = null; { final Function1 _function = (Variable v) -> { VLSVariable _createVLSVariable = this.factory.createVLSVariable(); final Procedure1 _function_1 = (VLSVariable it) -> { - it.setName(this.toIDMultiple("Var", v.getName())); + it.setName(this.toIDMultiple("V", v.getName())); }; return ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function_1); }; @@ -235,80 +236,43 @@ public class Logic2VampireLanguageMapper_Support { EList _quantifiedVariables = expression.getQuantifiedVariables(); for (final Variable variable : _quantifiedVariables) { { - VLSFunction _createVLSFunction = this.factory.createVLSFunction(); - final Procedure1 _function_1 = (VLSFunction it) -> { - TypeReference _range = variable.getRange(); - it.setConstant(this.toIDMultiple("t", ((ComplexTypeReference) _range).getReferred().getName())); - EList _terms = it.getTerms(); - VLSVariable _createVLSVariable = this.factory.createVLSVariable(); - final Procedure1 _function_2 = (VLSVariable it_1) -> { - it_1.setName(this.toIDMultiple("Var", variable.getName())); - }; - VLSVariable _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function_2); - _terms.add(_doubleArrow); - }; - final VLSFunction eq = ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function_1); + TypeReference _range = variable.getRange(); + final VLSFunction eq = this.duplicate(CollectionsUtil.lookup(((ComplexTypeReference) _range).getReferred(), trace.type2Predicate), CollectionsUtil.lookup(variable, variableMap)); typedefs.add(eq); } } - VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); - final Procedure1 _function_1 = (VLSUniversalQuantifier it) -> { - EList _variables = it.getVariables(); - Collection _values = variableMap.values(); - Iterables.addAll(_variables, _values); - VLSImplies _createVLSImplies = this.factory.createVLSImplies(); - final Procedure1 _function_2 = (VLSImplies it_1) -> { - it_1.setLeft(this.unfoldAnd(typedefs)); - it_1.setRight(mapper.transformTerm(expression.getExpression(), trace, this.withAddition(variables, variableMap))); - }; - VLSImplies _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSImplies, _function_2); - it.setOperand(_doubleArrow); - }; - _xblockexpression = ObjectExtensions.operator_doubleArrow(_createVLSUniversalQuantifier, _function_1); - } - return _xblockexpression; - } - - protected VLSTerm createExistentiallyQuantifiedExpression(final Logic2VampireLanguageMapper mapper, final QuantifiedExpression expression, final Logic2VampireLanguageMapperTrace trace, final Map variables) { - VLSExistentialQuantifier _xblockexpression = null; - { - final Function1 _function = (Variable v) -> { - VLSVariable _createVLSVariable = this.factory.createVLSVariable(); - final Procedure1 _function_1 = (VLSVariable it) -> { - it.setName(this.toIDMultiple("Var", v.getName())); + VLSTerm _xifexpression = null; + if (isUniversal) { + VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); + final Procedure1 _function_1 = (VLSUniversalQuantifier it) -> { + EList _variables = it.getVariables(); + Collection _values = variableMap.values(); + Iterables.addAll(_variables, _values); + VLSImplies _createVLSImplies = this.factory.createVLSImplies(); + final Procedure1 _function_2 = (VLSImplies it_1) -> { + it_1.setLeft(this.unfoldAnd(typedefs)); + it_1.setRight(mapper.transformTerm(expression.getExpression(), trace, this.withAddition(variables, variableMap))); + }; + VLSImplies _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSImplies, _function_2); + it.setOperand(_doubleArrow); }; - return ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function_1); - }; - final Map variableMap = IterableExtensions.toInvertedMap(expression.getQuantifiedVariables(), _function); - final ArrayList typedefs = new ArrayList(); - EList _quantifiedVariables = expression.getQuantifiedVariables(); - for (final Variable variable : _quantifiedVariables) { + _xifexpression = ObjectExtensions.operator_doubleArrow(_createVLSUniversalQuantifier, _function_1); + } else { + VLSExistentialQuantifier _xblockexpression_1 = null; { - VLSFunction _createVLSFunction = this.factory.createVLSFunction(); - final Procedure1 _function_1 = (VLSFunction it) -> { - TypeReference _range = variable.getRange(); - it.setConstant(this.toIDMultiple("t", ((ComplexTypeReference) _range).getReferred().getName())); - EList _terms = it.getTerms(); - VLSVariable _createVLSVariable = this.factory.createVLSVariable(); - final Procedure1 _function_2 = (VLSVariable it_1) -> { - it_1.setName(this.toIDMultiple("Var", variable.getName())); - }; - VLSVariable _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function_2); - _terms.add(_doubleArrow); + 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(); + Collection _values = variableMap.values(); + Iterables.addAll(_variables, _values); + it.setOperand(this.unfoldAnd(typedefs)); }; - final VLSFunction eq = ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function_1); - typedefs.add(eq); + _xblockexpression_1 = ObjectExtensions.operator_doubleArrow(_createVLSExistentialQuantifier, _function_2); } + _xifexpression = _xblockexpression_1; } - typedefs.add(mapper.transformTerm(expression.getExpression(), trace, this.withAddition(variables, variableMap))); - VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier(); - final Procedure1 _function_1 = (VLSExistentialQuantifier it) -> { - EList _variables = it.getVariables(); - Collection _values = variableMap.values(); - Iterables.addAll(_variables, _values); - it.setOperand(this.unfoldAnd(typedefs)); - }; - _xblockexpression = ObjectExtensions.operator_doubleArrow(_createVLSExistentialQuantifier, _function_1); + _xblockexpression = _xifexpression; } return _xblockexpression; } -- cgit v1.2.3-54-g00ecf