From d7730cb0d684d6324622021a310d9b4a53e7531c 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_ScopeMapper.java | 78 ++++++++++++---------- 1 file changed, 44 insertions(+), 34 deletions(-) (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java') 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 1950cad0..d2a6bff2 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 @@ -3,6 +3,7 @@ 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.VLSEquality; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; @@ -48,16 +49,19 @@ public class Logic2VampireLanguageMapper_ScopeMapper { public void _transformScope(final LogicSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) { final int GLOBAL_MIN = config.typeScopes.minNewElements; final int GLOBAL_MAX = config.typeScopes.maxNewElements; - final ArrayList localInstances = CollectionLiterals.newArrayList(); + final ArrayList localInstances = CollectionLiterals.newArrayList(); if ((GLOBAL_MIN != 0)) { this.getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, false); + for (final VLSConstant i : trace.uniqueInstances) { + localInstances.add(this.support.duplicate(i)); + } this.makeFofFormula(localInstances, trace, true, null); } if ((GLOBAL_MAX != 0)) { this.getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, true); - this.makeFofFormula(localInstances, trace, false, null); + this.makeFofFormula(((ArrayList) trace.uniqueInstances), trace, false, null); } - int i = 0; + int i_1 = 1; int minNum = (-1); Map startPoints = new HashMap(); Set _keySet = config.typeScopes.minNewElementsByType.keySet(); @@ -65,10 +69,10 @@ public class Logic2VampireLanguageMapper_ScopeMapper { { minNum = (CollectionsUtil.lookup(t, config.typeScopes.minNewElementsByType)).intValue(); if ((minNum != 0)) { - this.getInstanceConstants((i + minNum), i, localInstances, trace, true, false); - startPoints.put(t, Integer.valueOf(i)); - int _i = i; - i = (_i + minNum); + this.getInstanceConstants((i_1 + minNum), i_1, localInstances, trace, true, false); + startPoints.put(t, Integer.valueOf(i_1)); + int _i = i_1; + i_1 = (_i + minNum); this.makeFofFormula(localInstances, trace, true, t); } } @@ -83,8 +87,8 @@ public class Logic2VampireLanguageMapper_ScopeMapper { this.getInstanceConstants(((startpoint).intValue() + minNum), (startpoint).intValue(), localInstances, trace, true, false); } if (((maxNum).intValue() != minNum)) { - int instEndInd = Math.min(GLOBAL_MAX, ((i + (maxNum).intValue()) - minNum)); - this.getInstanceConstants(instEndInd, i, localInstances, trace, false, false); + int instEndInd = Math.min(GLOBAL_MAX, ((i_1 + (maxNum).intValue()) - minNum)); + this.getInstanceConstants(instEndInd, i_1, localInstances, trace, false, false); this.makeFofFormula(localInstances, trace, false, t_1); } } @@ -126,18 +130,24 @@ public class Logic2VampireLanguageMapper_ScopeMapper { protected void makeFofFormula(final ArrayList list, final Logic2VampireLanguageMapperTrace trace, final boolean minimum, final Type type) { String nm = ""; - VLSFunction tm = null; + VLSTerm tm = null; if ((type == null)) { nm = "object"; tm = this.support.topLevelTypeFunc(); } else { nm = CollectionsUtil.lookup(type, trace.type2Predicate).getConstant().toString(); - tm = this.support.duplicate(CollectionsUtil.lookup(type, trace.type2Predicate)); + VLSAnd _createVLSAnd = this.factory.createVLSAnd(); + final Procedure1 _function = (VLSAnd it) -> { + it.setLeft(this.support.duplicate(CollectionsUtil.lookup(type, trace.type2Predicate))); + it.setRight(this.support.topLevelTypeFunc()); + }; + VLSAnd _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSAnd, _function); + tm = _doubleArrow; } final String name = nm; - final VLSFunction term = tm; + final VLSTerm term = tm; VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); - final Procedure1 _function = (VLSFofFormula it) -> { + final Procedure1 _function_1 = (VLSFofFormula it) -> { String _xifexpression = null; if (minimum) { _xifexpression = "min"; @@ -147,53 +157,53 @@ public class Logic2VampireLanguageMapper_ScopeMapper { it.setName(this.support.toIDMultiple("typeScope", _xifexpression, name)); it.setFofRole("axiom"); VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); - final Procedure1 _function_1 = (VLSUniversalQuantifier it_1) -> { + final Procedure1 _function_2 = (VLSUniversalQuantifier it_1) -> { EList _variables = it_1.getVariables(); VLSVariable _duplicate = this.support.duplicate(this.variable); _variables.add(_duplicate); VLSImplies _createVLSImplies = this.factory.createVLSImplies(); - final Procedure1 _function_2 = (VLSImplies it_2) -> { + final Procedure1 _function_3 = (VLSImplies it_2) -> { if (minimum) { - final Function1 _function_3 = (VLSTerm i) -> { + final Function1 _function_4 = (VLSTerm i) -> { VLSEquality _createVLSEquality = this.factory.createVLSEquality(); - final Procedure1 _function_4 = (VLSEquality it_3) -> { + final Procedure1 _function_5 = (VLSEquality it_3) -> { VLSVariable _createVLSVariable = this.factory.createVLSVariable(); - final Procedure1 _function_5 = (VLSVariable it_4) -> { + final Procedure1 _function_6 = (VLSVariable it_4) -> { it_4.setName(this.variable.getName()); }; - VLSVariable _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function_5); - it_3.setLeft(_doubleArrow); + VLSVariable _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function_6); + it_3.setLeft(_doubleArrow_1); it_3.setRight(i); }; - return ObjectExtensions.operator_doubleArrow(_createVLSEquality, _function_4); + return ObjectExtensions.operator_doubleArrow(_createVLSEquality, _function_5); }; - it_2.setLeft(this.support.unfoldOr(ListExtensions.map(list, _function_3))); + it_2.setLeft(this.support.unfoldOr(ListExtensions.map(list, _function_4))); it_2.setRight(term); } else { it_2.setLeft(term); - final Function1 _function_4 = (VLSTerm i) -> { + final Function1 _function_5 = (VLSTerm i) -> { VLSEquality _createVLSEquality = this.factory.createVLSEquality(); - final Procedure1 _function_5 = (VLSEquality it_3) -> { + final Procedure1 _function_6 = (VLSEquality it_3) -> { VLSVariable _createVLSVariable = this.factory.createVLSVariable(); - final Procedure1 _function_6 = (VLSVariable it_4) -> { + final Procedure1 _function_7 = (VLSVariable it_4) -> { it_4.setName(this.variable.getName()); }; - VLSVariable _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function_6); - it_3.setLeft(_doubleArrow); + VLSVariable _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function_7); + it_3.setLeft(_doubleArrow_1); it_3.setRight(i); }; - return ObjectExtensions.operator_doubleArrow(_createVLSEquality, _function_5); + return ObjectExtensions.operator_doubleArrow(_createVLSEquality, _function_6); }; - it_2.setRight(this.support.unfoldOr(ListExtensions.map(list, _function_4))); + it_2.setRight(this.support.unfoldOr(ListExtensions.map(list, _function_5))); } }; - VLSImplies _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSImplies, _function_2); - it_1.setOperand(_doubleArrow); + VLSImplies _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createVLSImplies, _function_3); + it_1.setOperand(_doubleArrow_1); }; - VLSUniversalQuantifier _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSUniversalQuantifier, _function_1); - it.setFofFormula(_doubleArrow); + VLSUniversalQuantifier _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createVLSUniversalQuantifier, _function_2); + it.setFofFormula(_doubleArrow_1); }; - final VLSFofFormula cstDec = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula, _function); + final VLSFofFormula cstDec = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula, _function_1); EList _formulas = trace.specification.getFormulas(); _formulas.add(cstDec); } -- cgit v1.2.3-54-g00ecf