From 598daf4605d97466d07c74b1bc76d165be145288 Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Thu, 25 Apr 2019 02:50:40 -0400 Subject: VAMPIRE: fixed MANY bugs in containment and scope. #40 is good for now --- .../vampire/reasoner/.VampireSolver.xtendbin | Bin 5892 -> 5892 bytes .../builder/.Logic2VampireLanguageMapper.xtendbin | Bin 18151 -> 18150 bytes .../.Logic2VampireLanguageMapperTrace.xtendbin | Bin 4581 -> 4656 bytes ...c2VampireLanguageMapper_ConstantMapper.xtendbin | Bin 3164 -> 3164 bytes ...ampireLanguageMapper_ContainmentMapper.xtendbin | Bin 11478 -> 11904 bytes ...c2VampireLanguageMapper_RelationMapper.xtendbin | Bin 6455 -> 6454 bytes ...ogic2VampireLanguageMapper_ScopeMapper.xtendbin | Bin 10180 -> 10667 bytes .../.Logic2VampireLanguageMapper_Support.xtendbin | Bin 13048 -> 13046 bytes ...Logic2VampireLanguageMapper_TypeMapper.xtendbin | Bin 11135 -> 11136 bytes .../builder/Logic2VampireLanguageMapperTrace.java | 2 + ...ic2VampireLanguageMapper_ContainmentMapper.java | 56 +++++++++----- .../Logic2VampireLanguageMapper_ScopeMapper.java | 82 ++++++++++++++++----- 12 files changed, 103 insertions(+), 37 deletions(-) (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire') 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 f312e3a8..677cb718 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 88960abc..d071aa8a 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 580eb165..48090814 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 adc1b1cf..154e42a2 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 57f21798..61774e26 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 355315f8..2798d324 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 77a5ce95..5f3f349b 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 5eef76af..787c44a2 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 b042022e..b6e94088 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/Logic2VampireLanguageMapperTrace.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java index f1600087..c2ae099e 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java @@ -33,6 +33,8 @@ public class Logic2VampireLanguageMapperTrace { public Object topLvlElementIsInInitialModel = null; + public Object topLevelType = null; + public final Map type2Predicate = new HashMap(); public final Map element2Predicate = new HashMap(); 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 07677b7a..dd549c29 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 @@ -37,6 +37,7 @@ 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; @@ -89,6 +90,7 @@ public class Logic2VampireLanguageMapper_ContainmentMapper { } final String topName = CollectionsUtil.lookup(topTermVar, trace.type2Predicate).getConstant().toString(); final VLSFunction topTerm = this.support.duplicate(CollectionsUtil.lookup(topTermVar, trace.type2Predicate)); + trace.topLevelType = topTermVar; boolean topLvlIsInInitModel = false; String topLvlString = ""; ArrayList listToCheck = CollectionLiterals.newArrayList(topTermVar); @@ -174,15 +176,16 @@ public class Logic2VampireLanguageMapper_ContainmentMapper { final Map> type2cont = new HashMap>(); for (final Relation l_2 : relationsList) { { - final VLSFunction rel = this.support.duplicate(CollectionsUtil.lookup(((RelationDeclaration) l_2), trace.rel2Predicate), varList); + final VLSFunction rel = CollectionsUtil.lookup(((RelationDeclaration) l_2), trace.rel2Predicate); TypeReference _get = l_2.getParameters().get(1); Type _referred = ((ComplexTypeReference) _get).getReferred(); final Type toType = ((Type) _referred); final VLSFunction toFunc = CollectionsUtil.lookup(toType, trace.type2Predicate); - this.addToMap(type2cont, toFunc, rel); - EList _subtypes = toType.getSubtypes(); - for (final Type c_1 : _subtypes) { - this.addToMap(type2cont, toFunc, rel); + this.addToMap(type2cont, this.support.duplicate(toFunc), this.support.duplicate(rel, varList)); + ArrayList subTypes = CollectionLiterals.newArrayList(); + this.support.listSubtypes(toType, subTypes); + for (final Type c_1 : subTypes) { + this.addToMap(type2cont, this.support.duplicate(CollectionsUtil.lookup(c_1, trace.type2Predicate)), this.support.duplicate(rel, varList)); } VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); final Procedure1 _function_4 = (VLSFofFormula it) -> { @@ -231,6 +234,11 @@ 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())); @@ -352,20 +360,32 @@ public class Logic2VampireLanguageMapper_ContainmentMapper { } protected Object addToMap(final Map> type2cont, final VLSFunction toFunc, final VLSFunction rel) { - Object _xifexpression = null; - boolean _containsKey = type2cont.containsKey(toFunc); - boolean _not = (!_containsKey); - if (_not) { - _xifexpression = type2cont.put(toFunc, CollectionLiterals.newArrayList(rel)); - } else { - boolean _xifexpression_1 = false; - boolean _contains = type2cont.get(toFunc).contains(rel); - boolean _not_1 = (!_contains); - if (_not_1) { - _xifexpression_1 = type2cont.get(toFunc).add(rel); + Object _xblockexpression = null; + { + boolean keyInMap = false; + VLSFunction existingKey = this.factory.createVLSFunction(); + Set _keySet = type2cont.keySet(); + for (final VLSFunction k : _keySet) { + boolean _equals = k.getConstant().equals(toFunc.getConstant()); + if (_equals) { + keyInMap = true; + existingKey = k; + } + } + Object _xifexpression = null; + if ((!keyInMap)) { + _xifexpression = type2cont.put(toFunc, CollectionLiterals.newArrayList(rel)); + } else { + boolean _xifexpression_1 = false; + boolean _contains = type2cont.get(existingKey).contains(rel); + boolean _not = (!_contains); + if (_not) { + _xifexpression_1 = type2cont.get(existingKey).add(rel); + } + _xifexpression = Boolean.valueOf(_xifexpression_1); } - _xifexpression = Boolean.valueOf(_xifexpression_1); + _xblockexpression = _xifexpression; } - return _xifexpression; + return _xblockexpression; } } 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 bf7b70d0..c2e4033b 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 @@ -14,7 +14,10 @@ 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.VampireLanguageFactory; +import com.google.common.base.Objects; +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.TypeDefinition; import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; import java.util.ArrayList; import java.util.HashMap; @@ -26,6 +29,7 @@ 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.Functions.Function1; +import org.eclipse.xtext.xbase.lib.IterableExtensions; import org.eclipse.xtext.xbase.lib.ListExtensions; import org.eclipse.xtext.xbase.lib.ObjectExtensions; import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; @@ -80,33 +84,73 @@ public class Logic2VampireLanguageMapper_ScopeMapper { } int minNum = (-1); Map startPoints = new HashMap(); - Set _keySet = config.typeScopes.minNewElementsByType.keySet(); - for (final Type tConfig : _keySet) { + final Function1 _function = (Type it) -> { + boolean _equals = it.equals(trace.topLevelType); + return Boolean.valueOf((!_equals)); + }; + Iterable _filter = IterableExtensions.filter(config.typeScopes.minNewElementsByType.keySet(), _function); + for (final Type t : _filter) { { - minNum = (CollectionsUtil.lookup(tConfig, config.typeScopes.minNewElementsByType)).intValue(); + int numIniIntModel = 0; + Set _keySet = trace.definedElement2String.keySet(); + for (final DefinedElement elem : _keySet) { + EList _definedInType = elem.getDefinedInType(); + for (final TypeDefinition tDefined : _definedInType) { + boolean _dfsSubtypeCheck = this.support.dfsSubtypeCheck(t, tDefined); + if (_dfsSubtypeCheck) { + int _numIniIntModel = numIniIntModel; + numIniIntModel = (_numIniIntModel + 1); + } + } + } + Integer _lookup = CollectionsUtil.lookup(t, config.typeScopes.minNewElementsByType); + int _minus = ((_lookup).intValue() - numIniIntModel); + minNum = _minus; if ((minNum != 0)) { this.getInstanceConstants((i_1 + minNum), i_1, localInstances, trace, true, false); - startPoints.put(tConfig, Integer.valueOf(i_1)); + startPoints.put(t, Integer.valueOf(i_1)); int _i = i_1; i_1 = (_i + minNum); - this.makeFofFormula(localInstances, trace, true, tConfig); + this.makeFofFormula(localInstances, trace, true, t); } } } - Set _keySet_1 = config.typeScopes.maxNewElementsByType.keySet(); - for (final Type tConfig_1 : _keySet_1) { + final Function1 _function_1 = (Type it) -> { + boolean _equals = it.equals(trace.topLevelType); + return Boolean.valueOf((!_equals)); + }; + Iterable _filter_1 = IterableExtensions.filter(config.typeScopes.maxNewElementsByType.keySet(), _function_1); + for (final Type t_1 : _filter_1) { { - Integer maxNum = CollectionsUtil.lookup(tConfig_1, config.typeScopes.maxNewElementsByType); - minNum = (CollectionsUtil.lookup(tConfig_1, config.typeScopes.minNewElementsByType)).intValue(); - Integer startpoint = CollectionsUtil.lookup(tConfig_1, startPoints); + int numIniIntModel = 0; + Set _keySet = trace.definedElement2String.keySet(); + for (final DefinedElement elem : _keySet) { + EList _definedInType = elem.getDefinedInType(); + boolean _equals = Objects.equal(_definedInType, t_1); + if (_equals) { + int _numIniIntModel = numIniIntModel; + numIniIntModel = (_numIniIntModel + 1); + } + } + Integer _lookup = CollectionsUtil.lookup(t_1, config.typeScopes.maxNewElementsByType); + int maxNum = ((_lookup).intValue() - numIniIntModel); + boolean _contains = config.typeScopes.minNewElementsByType.keySet().contains(t_1); + if (_contains) { + Integer _lookup_1 = CollectionsUtil.lookup(t_1, config.typeScopes.minNewElementsByType); + int _minus = ((_lookup_1).intValue() - numIniIntModel); + minNum = _minus; + } else { + minNum = 0; + } if ((minNum != 0)) { + Integer startpoint = CollectionsUtil.lookup(t_1, startPoints); this.getInstanceConstants(((startpoint).intValue() + minNum), (startpoint).intValue(), localInstances, trace, true, false); + } else { + localInstances.clear(); } - if (((maxNum).intValue() != minNum)) { - 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, tConfig_1); - } + int instEndInd = Math.min(GLOBAL_MAX, ((i_1 + maxNum) - minNum)); + this.getInstanceConstants(instEndInd, i_1, localInstances, trace, false, false); + this.makeFofFormula(localInstances, trace, false, t_1); } } final boolean DUPLICATES = config.uniquenessDuplicates; @@ -118,12 +162,12 @@ public class Logic2VampireLanguageMapper_ScopeMapper { { final int x = ind; VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); - final Procedure1 _function = (VLSFofFormula it) -> { + final Procedure1 _function_2 = (VLSFofFormula it) -> { it.setName(this.support.toIDMultiple("t_uniqueness", e.getName())); it.setFofRole("axiom"); it.setFofFormula(this.support.establishUniqueness(trace.uniqueInstances, e)); }; - final VLSFofFormula uniqueness = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula, _function); + final VLSFofFormula uniqueness = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula, _function_2); EList _formulas = trace.specification.getFormulas(); _formulas.add(uniqueness); ind++; @@ -135,12 +179,12 @@ public class Logic2VampireLanguageMapper_ScopeMapper { { final int x = ind; VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); - final Procedure1 _function = (VLSFofFormula it) -> { + final Procedure1 _function_2 = (VLSFofFormula it) -> { it.setName(this.support.toIDMultiple("t_uniqueness", e_1.getName())); it.setFofRole("axiom"); it.setFofFormula(this.support.establishUniqueness(trace.uniqueInstances.subList(x, numInst), e_1)); }; - final VLSFofFormula uniqueness = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula, _function); + final VLSFofFormula uniqueness = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula, _function_2); EList _formulas = trace.specification.getFormulas(); _formulas.add(uniqueness); ind++; -- cgit v1.2.3-54-g00ecf