From 56df1f808fa2289c3e97d45d84bce8acc8937280 Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Thu, 14 Mar 2019 03:45:46 -0400 Subject: Implement Containment mapping (partially) and revisit enum mapping --- .../Logic2VampireLanguageMapper_TypeMapper.java | 99 ++++++++++++++++------ 1 file changed, 71 insertions(+), 28 deletions(-) (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java') 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 b8d74f36..ec759ebf 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 @@ -3,8 +3,10 @@ package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSAnd; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSDoubleQuote; +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; @@ -18,7 +20,6 @@ import com.google.common.base.Objects; import com.google.common.collect.Iterables; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition; import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage; import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; @@ -56,6 +57,7 @@ public class Logic2VampireLanguageMapper_TypeMapper { it.setName("A"); }; final VLSVariable variable = ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function); + int globalCounter = 0; for (final Type type : types) { { VLSFunction _createVLSFunction = this.factory.createVLSFunction(); @@ -92,7 +94,31 @@ public class Logic2VampireLanguageMapper_TypeMapper { }; final VLSFunction enumElemPred = ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function_1); trace.element2Predicate.put(e, enumElemPred); - orElems.add(enumElemPred); + } + } + final List possibleNots = CollectionLiterals.newArrayList(); + final List typeDefs = CollectionLiterals.newArrayList(); + EList _elements_1 = type_1.getElements(); + for (final DefinedElement t1 : _elements_1) { + { + EList _elements_2 = type_1.getElements(); + for (final DefinedElement t2 : _elements_2) { + boolean _equals = Objects.equal(t1, t2); + if (_equals) { + final VLSFunction fct = this.support.duplicate(CollectionsUtil.lookup(t2, trace.element2Predicate), variable); + possibleNots.add(fct); + } else { + final VLSFunction op = this.support.duplicate(CollectionsUtil.lookup(t2, trace.element2Predicate), variable); + VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); + final Procedure1 _function_1 = (VLSUnaryNegation it) -> { + it.setOperand(op); + }; + final VLSUnaryNegation negFct = ObjectExtensions.operator_doubleArrow(_createVLSUnaryNegation, _function_1); + possibleNots.add(negFct); + } + } + typeDefs.add(this.support.unfoldAnd(possibleNots)); + possibleNots.clear(); } } VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); @@ -107,7 +133,13 @@ public class Logic2VampireLanguageMapper_TypeMapper { VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); final Procedure1 _function_3 = (VLSEquivalent it_2) -> { it_2.setLeft(CollectionsUtil.lookup(type_1, trace.type2Predicate)); - it_2.setRight(this.support.unfoldOr(orElems)); + VLSAnd _createVLSAnd = this.factory.createVLSAnd(); + final Procedure1 _function_4 = (VLSAnd it_3) -> { + it_3.setLeft(this.support.topLevelTypeFunc(variable)); + it_3.setRight(this.support.unfoldOr(typeDefs)); + }; + VLSAnd _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSAnd, _function_4); + it_2.setRight(_doubleArrow); }; VLSEquivalent _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSEquivalent, _function_3); it_1.setOperand(_doubleArrow); @@ -118,8 +150,7 @@ public class Logic2VampireLanguageMapper_TypeMapper { final VLSFofFormula res = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula, _function_1); EList _formulas = trace.specification.getFormulas(); _formulas.add(res); - final List enumScopeElems = CollectionLiterals.newArrayList(); - for (int i = 0; (i < ((Object[])Conversions.unwrapArray(type_1.getElements(), Object.class)).length); i++) { + for (int i = globalCounter; (i < (globalCounter + ((Object[])Conversions.unwrapArray(type_1.getElements(), Object.class)).length)); i++) { { final int num = (i + 1); VLSFunctionAsTerm _createVLSFunctionAsTerm = this.factory.createVLSFunctionAsTerm(); @@ -129,38 +160,50 @@ public class Logic2VampireLanguageMapper_TypeMapper { final VLSFunctionAsTerm cstTerm = ObjectExtensions.operator_doubleArrow(_createVLSFunctionAsTerm, _function_2); final VLSConstant cst = this.support.toConstant(cstTerm); trace.uniqueInstances.add(cst); - final VLSFunction fct = this.support.duplicate(CollectionsUtil.lookup(type_1.getElements().get(i), trace.element2Predicate), cstTerm); - enumScopeElems.add(fct); - for (int j = 0; (j < ((Object[])Conversions.unwrapArray(type_1.getElements(), Object.class)).length); j++) { - if ((j != i)) { - final VLSFunction op = this.support.duplicate(CollectionsUtil.lookup(type_1.getElements().get(j), trace.element2Predicate), cstTerm); - VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); - final Procedure1 _function_3 = (VLSUnaryNegation it) -> { - it.setOperand(op); + final int index = i; + VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); + final Procedure1 _function_3 = (VLSFofFormula it) -> { + it.setName(this.support.toIDMultiple("enumScope", type_1.getName().split(" ")[0], + type_1.getElements().get(index).getName().split(" ")[0])); + it.setFofRole("axiom"); + VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); + final Procedure1 _function_4 = (VLSUniversalQuantifier it_1) -> { + EList _variables = it_1.getVariables(); + VLSVariable _duplicate = this.support.duplicate(variable); + _variables.add(_duplicate); + VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); + final Procedure1 _function_5 = (VLSEquivalent it_2) -> { + VLSEquality _createVLSEquality = this.factory.createVLSEquality(); + final Procedure1 _function_6 = (VLSEquality it_3) -> { + it_3.setLeft(this.support.duplicate(variable)); + it_3.setRight(this.support.duplicate(this.support.toConstant(cstTerm))); + }; + VLSEquality _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSEquality, _function_6); + it_2.setLeft(_doubleArrow); + it_2.setRight(this.support.duplicate(CollectionsUtil.lookup(type_1.getElements().get(index), trace.element2Predicate), variable)); }; - final VLSUnaryNegation negFct = ObjectExtensions.operator_doubleArrow(_createVLSUnaryNegation, _function_3); - enumScopeElems.add(negFct); - } - } + VLSEquivalent _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSEquivalent, _function_5); + it_1.setOperand(_doubleArrow); + }; + VLSUniversalQuantifier _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSUniversalQuantifier, _function_4); + it.setFofFormula(_doubleArrow); + }; + final VLSFofFormula enumScope = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula_1, _function_3); + EList _formulas_1 = trace.specification.getFormulas(); + _formulas_1.add(enumScope); } } - VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); - final Procedure1 _function_2 = (VLSFofFormula it) -> { - it.setName(this.support.toIDMultiple("enumScope", type_1.getName().split(" ")[0])); - it.setFofRole("axiom"); - it.setFofFormula(this.support.unfoldAnd(enumScopeElems)); - }; - final VLSFofFormula enumScope = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula_1, _function_2); - EList _formulas_1 = trace.specification.getFormulas(); - _formulas_1.add(enumScope); + int _globalCounter = globalCounter; + int _size = type_1.getElements().size(); + globalCounter = (_globalCounter + _size); } } final Function1 _function_1 = (Type it) -> { boolean _isIsAbstract = it.isIsAbstract(); return Boolean.valueOf((!_isIsAbstract)); }; - Iterable _filter_1 = Iterables.filter(IterableExtensions.filter(types, _function_1), TypeDeclaration.class); - for (final TypeDeclaration t1 : _filter_1) { + Iterable _filter_1 = IterableExtensions.filter(types, _function_1); + for (final Type t1 : _filter_1) { { for (final Type t2 : types) { if ((Objects.equal(t1, t2) || this.support.dfsSupertypeCheck(t1, t2))) { -- cgit v1.2.3-70-g09d2