From 06b2801cd5893ced25745d79959592f99b4ef83b Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Wed, 24 Apr 2019 19:54:57 -0400 Subject: VAMPIRE : initial model handling almost done. only typeScope remains #40 --- .../vampire/reasoner/.VampireSolver.xtendbin | Bin 5892 -> 5892 bytes .../builder/.Logic2VampireLanguageMapper.xtendbin | Bin 18159 -> 18151 bytes .../.Logic2VampireLanguageMapperTrace.xtendbin | Bin 4481 -> 4581 bytes ...c2VampireLanguageMapper_ConstantMapper.xtendbin | Bin 3164 -> 3164 bytes ...ampireLanguageMapper_ContainmentMapper.xtendbin | Bin 11150 -> 11478 bytes ...c2VampireLanguageMapper_RelationMapper.xtendbin | Bin 6457 -> 6455 bytes ...ogic2VampireLanguageMapper_ScopeMapper.xtendbin | Bin 9839 -> 10180 bytes .../.Logic2VampireLanguageMapper_Support.xtendbin | Bin 13048 -> 13048 bytes ...Logic2VampireLanguageMapper_TypeMapper.xtendbin | Bin 11070 -> 11135 bytes .../builder/Logic2VampireLanguageMapper.java | 2 +- .../builder/Logic2VampireLanguageMapperTrace.java | 2 + ...ic2VampireLanguageMapper_ContainmentMapper.java | 31 ++++--- .../Logic2VampireLanguageMapper_ScopeMapper.java | 32 ++++--- .../Logic2VampireLanguageMapper_TypeMapper.java | 102 +++++++++++---------- 14 files changed, 94 insertions(+), 75 deletions(-) (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca') 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 80a74b4c..f312e3a8 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 2dc1ce19..88960abc 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 3c14aa6c..580eb165 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 b51b8ceb..adc1b1cf 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 02b4f393..57f21798 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 1feb9930..355315f8 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 fbc106a5..77a5ce95 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 77ffdd4b..5eef76af 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 070afd3c..b042022e 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.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java index f04bd7dc..65f58281 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 @@ -117,13 +117,13 @@ public class Logic2VampireLanguageMapper { if (_not) { this.typeMapper.transformTypes(problem.getTypes(), problem.getElements(), this, trace); } - this.scopeMapper.transformScope(config, trace); trace.relationDefinitions = this.collectRelationDefinitions(problem); final Consumer _function_3 = (Relation it) -> { this.relationMapper.transformRelation(it, trace); }; problem.getRelations().forEach(_function_3); this.containmentMapper.transformContainment(config, problem.getContainmentHierarchies(), trace); + this.scopeMapper.transformScope(problem.getTypes(), config, trace); trace.constantDefinitions = this.collectConstantDefinitions(problem); final Consumer _function_4 = (ConstantDefinition it) -> { this.constantMapper.transformConstantDefinitionSpecification(it, trace); 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 621a6e58..f1600087 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 @@ -31,6 +31,8 @@ public class Logic2VampireLanguageMapperTrace { public Map definedElement2String = new HashMap(); + public Object topLvlElementIsInInitialModel = 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 855d7637..07677b7a 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 @@ -25,6 +25,7 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration; 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.logic.model.logiclanguage.TypeReference; +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.impl.TypeDefinitionImpl; import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy; import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; import java.util.ArrayList; @@ -36,7 +37,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; @@ -91,10 +91,17 @@ public class Logic2VampireLanguageMapper_ContainmentMapper { final VLSFunction topTerm = this.support.duplicate(CollectionsUtil.lookup(topTermVar, trace.type2Predicate)); boolean topLvlIsInInitModel = false; String topLvlString = ""; - EList _subtypes = topTermVar.getSubtypes(); - for (final Type c : _subtypes) { - boolean _equals = c.getClass().getSimpleName().equals("TypeDefinitionImpl"); + ArrayList listToCheck = CollectionLiterals.newArrayList(topTermVar); + listToCheck.addAll(topTermVar.getSubtypes()); + for (final Type c : listToCheck) { + Class _class = c.getClass(); + boolean _equals = Objects.equal(_class, TypeDefinitionImpl.class); if (_equals) { + int _length = ((Object[])Conversions.unwrapArray(((TypeDefinition) c).getElements(), Object.class)).length; + boolean _greaterThan = (_length > 1); + if (_greaterThan) { + throw new IllegalArgumentException("You cannot have multiple top-level elements in your initial model"); + } EList _elements = ((TypeDefinition) c).getElements(); for (final DefinedElement d : _elements) { boolean _containsKey = trace.definedElement2String.containsKey(d); @@ -105,10 +112,9 @@ public class Logic2VampireLanguageMapper_ContainmentMapper { } } } + trace.topLvlElementIsInInitialModel = Boolean.valueOf(topLvlIsInInitModel); final boolean topInIM = topLvlIsInInitModel; final String topStr = topLvlString; - InputOutput.print(Boolean.valueOf(topInIM)); - InputOutput.print(topStr); VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); final Procedure1 _function = (VLSFofFormula it) -> { it.setName(this.support.toIDMultiple("containment_topLevel", topName)); @@ -174,8 +180,8 @@ public class Logic2VampireLanguageMapper_ContainmentMapper { final Type toType = ((Type) _referred); final VLSFunction toFunc = CollectionsUtil.lookup(toType, trace.type2Predicate); this.addToMap(type2cont, toFunc, rel); - EList _subtypes_1 = toType.getSubtypes(); - for (final Type c_1 : _subtypes_1) { + EList _subtypes = toType.getSubtypes(); + for (final Type c_1 : _subtypes) { this.addToMap(type2cont, toFunc, rel); } VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); @@ -242,9 +248,9 @@ public class Logic2VampireLanguageMapper_ContainmentMapper { EList _variables_1 = it_3.getVariables(); VLSVariable _duplicate_1 = this.support.duplicate(varB); _variables_1.add(_duplicate_1); - int _length = ((Object[])Conversions.unwrapArray(e.getValue(), Object.class)).length; - boolean _greaterThan = (_length > 1); - if (_greaterThan) { + int _length_1 = ((Object[])Conversions.unwrapArray(e.getValue(), Object.class)).length; + boolean _greaterThan_1 = (_length_1 > 1); + if (_greaterThan_1) { it_3.setOperand(this.makeUnique(e.getValue())); } else { it_3.setOperand(e.getValue().get(0)); @@ -282,7 +288,8 @@ public class Logic2VampireLanguageMapper_ContainmentMapper { { for (final Relation l_3 : relationsList) { { - final VLSFunction rel = this.support.duplicate(CollectionsUtil.lookup(((RelationDeclaration) l_3), trace.rel2Predicate), CollectionLiterals.newArrayList(variables.get(j), variables.get(((j + 1) % i)))); + final VLSFunction rel = this.support.duplicate(CollectionsUtil.lookup(((RelationDeclaration) l_3), trace.rel2Predicate), + CollectionLiterals.newArrayList(variables.get(j), variables.get(((j + 1) % i)))); disjunctionList.add(rel); } } 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 f5d35b28..bf7b70d0 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 @@ -47,11 +47,12 @@ public class Logic2VampireLanguageMapper_ScopeMapper { this.base = base; } - public void _transformScope(final VampireSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) { + public void _transformScope(final List types, final VampireSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) { final int ABSOLUTE_MIN = 0; final int ABSOLUTE_MAX = Integer.MAX_VALUE; - final int GLOBAL_MIN = config.typeScopes.minNewElements; - final int GLOBAL_MAX = config.typeScopes.maxNewElements; + int elemsInIM = trace.definedElement2String.size(); + final int GLOBAL_MIN = (config.typeScopes.minNewElements - elemsInIM); + final int GLOBAL_MAX = (config.typeScopes.maxNewElements - elemsInIM); final ArrayList localInstances = CollectionLiterals.newArrayList(); final boolean consistant = (GLOBAL_MAX > GLOBAL_MIN); if ((GLOBAL_MIN != ABSOLUTE_MIN)) { @@ -74,34 +75,37 @@ public class Logic2VampireLanguageMapper_ScopeMapper { } } int i_1 = 1; + if ((((Boolean) trace.topLvlElementIsInInitialModel)).booleanValue()) { + i_1 = 0; + } int minNum = (-1); Map startPoints = new HashMap(); Set _keySet = config.typeScopes.minNewElementsByType.keySet(); - for (final Type t : _keySet) { + for (final Type tConfig : _keySet) { { - minNum = (CollectionsUtil.lookup(t, config.typeScopes.minNewElementsByType)).intValue(); + minNum = (CollectionsUtil.lookup(tConfig, config.typeScopes.minNewElementsByType)).intValue(); if ((minNum != 0)) { this.getInstanceConstants((i_1 + minNum), i_1, localInstances, trace, true, false); - startPoints.put(t, Integer.valueOf(i_1)); + startPoints.put(tConfig, Integer.valueOf(i_1)); int _i = i_1; i_1 = (_i + minNum); - this.makeFofFormula(localInstances, trace, true, t); + this.makeFofFormula(localInstances, trace, true, tConfig); } } } Set _keySet_1 = config.typeScopes.maxNewElementsByType.keySet(); - for (final Type t_1 : _keySet_1) { + for (final Type tConfig_1 : _keySet_1) { { - Integer maxNum = CollectionsUtil.lookup(t_1, config.typeScopes.maxNewElementsByType); - minNum = (CollectionsUtil.lookup(t_1, config.typeScopes.minNewElementsByType)).intValue(); - Integer startpoint = CollectionsUtil.lookup(t_1, startPoints); + 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); if ((minNum != 0)) { this.getInstanceConstants(((startpoint).intValue() + minNum), (startpoint).intValue(), localInstances, trace, true, false); } 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, t_1); + this.makeFofFormula(localInstances, trace, false, tConfig_1); } } } @@ -246,8 +250,8 @@ public class Logic2VampireLanguageMapper_ScopeMapper { _formulas.add(cstDec); } - public void transformScope(final VampireSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) { - _transformScope(config, trace); + public void transformScope(final List types, final VampireSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) { + _transformScope(types, config, trace); return; } } 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 2d9d566d..73e59774 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 @@ -77,10 +77,16 @@ public class Logic2VampireLanguageMapper_TypeMapper { trace.type2Predicate.put(type, typePred); } } - Iterable _filter = Iterables.filter(types, TypeDefinition.class); + final Function1 _function_1 = (TypeDefinition it) -> { + boolean _isIsAbstract = it.isIsAbstract(); + return Boolean.valueOf((!_isIsAbstract)); + }; + Iterable _filter = IterableExtensions.filter(Iterables.filter(types, TypeDefinition.class), _function_1); for (final TypeDefinition type_1 : _filter) { { - final boolean isNotEnum = ((((Object[])Conversions.unwrapArray(type_1.getSupertypes(), Object.class)).length == 1) && type_1.getSupertypes().get(0).isIsAbstract()); + final int len = type_1.getName().length(); + boolean _equals = type_1.getName().substring((len - 4), len).equals("enum"); + final boolean isNotEnum = (!_equals); final List orElems = CollectionLiterals.newArrayList(); EList _elements = type_1.getElements(); for (final DefinedElement e : _elements) { @@ -88,21 +94,21 @@ public class Logic2VampireLanguageMapper_TypeMapper { final String[] nameArray = e.getName().split(" "); String relNameVar = ""; int _length = nameArray.length; - boolean _equals = (_length == 3); - if (_equals) { + boolean _equals_1 = (_length == 3); + if (_equals_1) { relNameVar = this.support.toIDMultiple(nameArray[0], nameArray[2]); } else { relNameVar = e.getName(); } final String relName = relNameVar; VLSFunction _createVLSFunction = this.factory.createVLSFunction(); - final Procedure1 _function_1 = (VLSFunction it) -> { + final Procedure1 _function_2 = (VLSFunction it) -> { it.setConstant(this.support.toIDMultiple("e", relName)); EList _terms = it.getTerms(); VLSVariable _duplicate = this.support.duplicate(variable); _terms.add(_duplicate); }; - final VLSFunction enumElemPred = ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function_1); + final VLSFunction enumElemPred = ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function_2); trace.element2Predicate.put(e, enumElemPred); } } @@ -113,17 +119,17 @@ public class Logic2VampireLanguageMapper_TypeMapper { { EList _elements_2 = type_1.getElements(); for (final DefinedElement t2 : _elements_2) { - boolean _equals = Objects.equal(t1, t2); - if (_equals) { + boolean _equals_1 = Objects.equal(t1, t2); + if (_equals_1) { 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) -> { + final Procedure1 _function_2 = (VLSUnaryNegation it) -> { it.setOperand(op); }; - final VLSUnaryNegation negFct = ObjectExtensions.operator_doubleArrow(_createVLSUnaryNegation, _function_1); + final VLSUnaryNegation negFct = ObjectExtensions.operator_doubleArrow(_createVLSUnaryNegation, _function_2); possibleNots.add(negFct); } } @@ -132,32 +138,32 @@ public class Logic2VampireLanguageMapper_TypeMapper { } } VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); - final Procedure1 _function_1 = (VLSFofFormula it) -> { + final Procedure1 _function_2 = (VLSFofFormula it) -> { it.setName(this.support.toIDMultiple("typeDef", CollectionsUtil.lookup(type_1, trace.type2Predicate).getConstant().toString())); it.setFofRole("axiom"); VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); - final Procedure1 _function_2 = (VLSUniversalQuantifier it_1) -> { + final Procedure1 _function_3 = (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_3 = (VLSEquivalent it_2) -> { + final Procedure1 _function_4 = (VLSEquivalent it_2) -> { it_2.setLeft(CollectionsUtil.lookup(type_1, trace.type2Predicate)); VLSAnd _createVLSAnd = this.factory.createVLSAnd(); - final Procedure1 _function_4 = (VLSAnd it_3) -> { + final Procedure1 _function_5 = (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); + VLSAnd _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSAnd, _function_5); it_2.setRight(_doubleArrow); }; - VLSEquivalent _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSEquivalent, _function_3); + VLSEquivalent _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSEquivalent, _function_4); it_1.setOperand(_doubleArrow); }; - VLSUniversalQuantifier _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSUniversalQuantifier, _function_2); + VLSUniversalQuantifier _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSUniversalQuantifier, _function_3); it.setFofFormula(_doubleArrow); }; - final VLSFofFormula res = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula, _function_1); + final VLSFofFormula res = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula, _function_2); EList _formulas = trace.specification.getFormulas(); _formulas.add(res); for (int i = globalCounter; (i < (globalCounter + ((Object[])Conversions.unwrapArray(type_1.getElements(), Object.class)).length)); i++) { @@ -165,17 +171,17 @@ public class Logic2VampireLanguageMapper_TypeMapper { final int num = (i + 1); final int index = (i - globalCounter); VLSFunctionAsTerm _createVLSFunctionAsTerm = this.factory.createVLSFunctionAsTerm(); - final Procedure1 _function_2 = (VLSFunctionAsTerm it) -> { + final Procedure1 _function_3 = (VLSFunctionAsTerm it) -> { it.setFunctor(("eo" + Integer.valueOf(num))); }; - final VLSFunctionAsTerm cstTerm = ObjectExtensions.operator_doubleArrow(_createVLSFunctionAsTerm, _function_2); + final VLSFunctionAsTerm cstTerm = ObjectExtensions.operator_doubleArrow(_createVLSFunctionAsTerm, _function_3); if (isNotEnum) { trace.definedElement2String.put(type_1.getElements().get(index), cstTerm.getFunctor()); } final VLSConstant cst = this.support.toConstant(cstTerm); trace.uniqueInstances.add(cst); VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); - final Procedure1 _function_3 = (VLSFofFormula it) -> { + final Procedure1 _function_4 = (VLSFofFormula it) -> { String _xifexpression = null; if (isNotEnum) { _xifexpression = "definedType"; @@ -186,28 +192,28 @@ public class Logic2VampireLanguageMapper_TypeMapper { type_1.getElements().get(index).getName().split(" ")[0])); it.setFofRole("axiom"); VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); - final Procedure1 _function_4 = (VLSUniversalQuantifier it_1) -> { + final Procedure1 _function_5 = (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) -> { + final Procedure1 _function_6 = (VLSEquivalent it_2) -> { VLSEquality _createVLSEquality = this.factory.createVLSEquality(); - final Procedure1 _function_6 = (VLSEquality it_3) -> { + final Procedure1 _function_7 = (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); + VLSEquality _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSEquality, _function_7); it_2.setLeft(_doubleArrow); it_2.setRight(this.support.duplicate(CollectionsUtil.lookup(type_1.getElements().get(index), trace.element2Predicate), variable)); }; - VLSEquivalent _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSEquivalent, _function_5); + VLSEquivalent _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSEquivalent, _function_6); it_1.setOperand(_doubleArrow); }; - VLSUniversalQuantifier _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSUniversalQuantifier, _function_4); + VLSUniversalQuantifier _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSUniversalQuantifier, _function_5); it.setFofFormula(_doubleArrow); }; - final VLSFofFormula enumScope = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula_1, _function_3); + final VLSFofFormula enumScope = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula_1, _function_4); EList _formulas_1 = trace.specification.getFormulas(); _formulas_1.add(enumScope); } @@ -217,11 +223,11 @@ public class Logic2VampireLanguageMapper_TypeMapper { globalCounter = (_globalCounter + _size); } } - final Function1 _function_1 = (Type it) -> { + final Function1 _function_2 = (Type it) -> { boolean _isIsAbstract = it.isIsAbstract(); return Boolean.valueOf((!_isIsAbstract)); }; - Iterable _filter_1 = IterableExtensions.filter(types, _function_1); + Iterable _filter_1 = IterableExtensions.filter(types, _function_2); for (final Type t1 : _filter_1) { { for (final Type t2 : types) { @@ -229,10 +235,10 @@ public class Logic2VampireLanguageMapper_TypeMapper { trace.type2PossibleNot.put(t2, this.support.duplicate(CollectionsUtil.lookup(t2, trace.type2Predicate))); } else { VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); - final Procedure1 _function_2 = (VLSUnaryNegation it) -> { + final Procedure1 _function_3 = (VLSUnaryNegation it) -> { it.setOperand(this.support.duplicate(CollectionsUtil.lookup(t2, trace.type2Predicate))); }; - VLSUnaryNegation _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSUnaryNegation, _function_2); + VLSUnaryNegation _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSUnaryNegation, _function_3); trace.type2PossibleNot.put(t2, _doubleArrow); } } @@ -245,63 +251,63 @@ public class Logic2VampireLanguageMapper_TypeMapper { final List type2Not = CollectionLiterals.newArrayList(); for (final Type t : types) { VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); - final Procedure1 _function_2 = (VLSUnaryNegation it) -> { + final Procedure1 _function_3 = (VLSUnaryNegation it) -> { it.setOperand(this.support.duplicate(CollectionsUtil.lookup(t, trace.type2Predicate))); }; - VLSUnaryNegation _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSUnaryNegation, _function_2); + VLSUnaryNegation _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSUnaryNegation, _function_3); type2Not.add(_doubleArrow); } VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); - final Procedure1 _function_3 = (VLSFofFormula it) -> { + final Procedure1 _function_4 = (VLSFofFormula it) -> { it.setName("notObjectHandler"); it.setFofRole("axiom"); VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); - final Procedure1 _function_4 = (VLSUniversalQuantifier it_1) -> { + final Procedure1 _function_5 = (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) -> { + final Procedure1 _function_6 = (VLSEquivalent it_2) -> { VLSUnaryNegation _createVLSUnaryNegation_1 = this.factory.createVLSUnaryNegation(); - final Procedure1 _function_6 = (VLSUnaryNegation it_3) -> { + final Procedure1 _function_7 = (VLSUnaryNegation it_3) -> { it_3.setOperand(this.support.topLevelTypeFunc()); }; - VLSUnaryNegation _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createVLSUnaryNegation_1, _function_6); + VLSUnaryNegation _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createVLSUnaryNegation_1, _function_7); it_2.setLeft(_doubleArrow_1); it_2.setRight(this.support.unfoldAnd(type2Not)); }; - VLSEquivalent _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createVLSEquivalent, _function_5); + VLSEquivalent _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createVLSEquivalent, _function_6); it_1.setOperand(_doubleArrow_1); }; - VLSUniversalQuantifier _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createVLSUniversalQuantifier, _function_4); + VLSUniversalQuantifier _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createVLSUniversalQuantifier, _function_5); it.setFofFormula(_doubleArrow_1); }; - final VLSFofFormula notObj = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula, _function_3); + final VLSFofFormula notObj = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula, _function_4); EList _formulas = trace.specification.getFormulas(); _formulas.add(notObj); VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); - final Procedure1 _function_4 = (VLSFofFormula it) -> { + final Procedure1 _function_5 = (VLSFofFormula it) -> { it.setName("inheritanceHierarchyHandler"); it.setFofRole("axiom"); VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); - final Procedure1 _function_5 = (VLSUniversalQuantifier it_1) -> { + final Procedure1 _function_6 = (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_6 = (VLSEquivalent it_2) -> { + final Procedure1 _function_7 = (VLSEquivalent it_2) -> { it_2.setLeft(this.support.topLevelTypeFunc()); Collection _values = trace.type2And.values(); final ArrayList reversedList = new ArrayList(_values); it_2.setRight(this.support.unfoldOr(reversedList)); }; - VLSEquivalent _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createVLSEquivalent, _function_6); + VLSEquivalent _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createVLSEquivalent, _function_7); it_1.setOperand(_doubleArrow_1); }; - VLSUniversalQuantifier _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createVLSUniversalQuantifier, _function_5); + VLSUniversalQuantifier _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createVLSUniversalQuantifier, _function_6); it.setFofFormula(_doubleArrow_1); }; - final VLSFofFormula hierarch = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula_1, _function_4); + final VLSFofFormula hierarch = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula_1, _function_5); EList _formulas_1 = trace.specification.getFormulas(); _xblockexpression = _formulas_1.add(hierarch); } -- cgit v1.2.3-54-g00ecf