diff options
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder')
13 files changed, 94 insertions, 75 deletions
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 --- 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 | |||
Binary files 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 --- 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 | |||
Binary files 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 --- 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 | |||
Binary files 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 --- 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 | |||
Binary files 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 --- 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 | |||
Binary files 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 --- 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 | |||
Binary files 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 --- 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 | |||
Binary files 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 --- 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 | |||
Binary files 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 { | |||
117 | if (_not) { | 117 | if (_not) { |
118 | this.typeMapper.transformTypes(problem.getTypes(), problem.getElements(), this, trace); | 118 | this.typeMapper.transformTypes(problem.getTypes(), problem.getElements(), this, trace); |
119 | } | 119 | } |
120 | this.scopeMapper.transformScope(config, trace); | ||
121 | trace.relationDefinitions = this.collectRelationDefinitions(problem); | 120 | trace.relationDefinitions = this.collectRelationDefinitions(problem); |
122 | final Consumer<Relation> _function_3 = (Relation it) -> { | 121 | final Consumer<Relation> _function_3 = (Relation it) -> { |
123 | this.relationMapper.transformRelation(it, trace); | 122 | this.relationMapper.transformRelation(it, trace); |
124 | }; | 123 | }; |
125 | problem.getRelations().forEach(_function_3); | 124 | problem.getRelations().forEach(_function_3); |
126 | this.containmentMapper.transformContainment(config, problem.getContainmentHierarchies(), trace); | 125 | this.containmentMapper.transformContainment(config, problem.getContainmentHierarchies(), trace); |
126 | this.scopeMapper.transformScope(problem.getTypes(), config, trace); | ||
127 | trace.constantDefinitions = this.collectConstantDefinitions(problem); | 127 | trace.constantDefinitions = this.collectConstantDefinitions(problem); |
128 | final Consumer<ConstantDefinition> _function_4 = (ConstantDefinition it) -> { | 128 | final Consumer<ConstantDefinition> _function_4 = (ConstantDefinition it) -> { |
129 | this.constantMapper.transformConstantDefinitionSpecification(it, trace); | 129 | 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 { | |||
31 | 31 | ||
32 | public Map<DefinedElement, String> definedElement2String = new HashMap<DefinedElement, String>(); | 32 | public Map<DefinedElement, String> definedElement2String = new HashMap<DefinedElement, String>(); |
33 | 33 | ||
34 | public Object topLvlElementIsInInitialModel = null; | ||
35 | |||
34 | public final Map<Type, VLSFunction> type2Predicate = new HashMap<Type, VLSFunction>(); | 36 | public final Map<Type, VLSFunction> type2Predicate = new HashMap<Type, VLSFunction>(); |
35 | 37 | ||
36 | public final Map<DefinedElement, VLSFunction> element2Predicate = new HashMap<DefinedElement, VLSFunction>(); | 38 | public final Map<DefinedElement, VLSFunction> element2Predicate = new HashMap<DefinedElement, VLSFunction>(); |
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; | |||
25 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; | 25 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; |
26 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition; | 26 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition; |
27 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference; | 27 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference; |
28 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.impl.TypeDefinitionImpl; | ||
28 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy; | 29 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy; |
29 | import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; | 30 | import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; |
30 | import java.util.ArrayList; | 31 | import java.util.ArrayList; |
@@ -36,7 +37,6 @@ import org.eclipse.emf.common.util.EList; | |||
36 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; | 37 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; |
37 | import org.eclipse.xtext.xbase.lib.Conversions; | 38 | import org.eclipse.xtext.xbase.lib.Conversions; |
38 | import org.eclipse.xtext.xbase.lib.Extension; | 39 | import org.eclipse.xtext.xbase.lib.Extension; |
39 | import org.eclipse.xtext.xbase.lib.InputOutput; | ||
40 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; | 40 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; |
41 | import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; | 41 | import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; |
42 | 42 | ||
@@ -91,10 +91,17 @@ public class Logic2VampireLanguageMapper_ContainmentMapper { | |||
91 | final VLSFunction topTerm = this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(topTermVar, trace.type2Predicate)); | 91 | final VLSFunction topTerm = this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(topTermVar, trace.type2Predicate)); |
92 | boolean topLvlIsInInitModel = false; | 92 | boolean topLvlIsInInitModel = false; |
93 | String topLvlString = ""; | 93 | String topLvlString = ""; |
94 | EList<Type> _subtypes = topTermVar.getSubtypes(); | 94 | ArrayList<Type> listToCheck = CollectionLiterals.<Type>newArrayList(topTermVar); |
95 | for (final Type c : _subtypes) { | 95 | listToCheck.addAll(topTermVar.getSubtypes()); |
96 | boolean _equals = c.getClass().getSimpleName().equals("TypeDefinitionImpl"); | 96 | for (final Type c : listToCheck) { |
97 | Class<? extends Type> _class = c.getClass(); | ||
98 | boolean _equals = Objects.equal(_class, TypeDefinitionImpl.class); | ||
97 | if (_equals) { | 99 | if (_equals) { |
100 | int _length = ((Object[])Conversions.unwrapArray(((TypeDefinition) c).getElements(), Object.class)).length; | ||
101 | boolean _greaterThan = (_length > 1); | ||
102 | if (_greaterThan) { | ||
103 | throw new IllegalArgumentException("You cannot have multiple top-level elements in your initial model"); | ||
104 | } | ||
98 | EList<DefinedElement> _elements = ((TypeDefinition) c).getElements(); | 105 | EList<DefinedElement> _elements = ((TypeDefinition) c).getElements(); |
99 | for (final DefinedElement d : _elements) { | 106 | for (final DefinedElement d : _elements) { |
100 | boolean _containsKey = trace.definedElement2String.containsKey(d); | 107 | boolean _containsKey = trace.definedElement2String.containsKey(d); |
@@ -105,10 +112,9 @@ public class Logic2VampireLanguageMapper_ContainmentMapper { | |||
105 | } | 112 | } |
106 | } | 113 | } |
107 | } | 114 | } |
115 | trace.topLvlElementIsInInitialModel = Boolean.valueOf(topLvlIsInInitModel); | ||
108 | final boolean topInIM = topLvlIsInInitModel; | 116 | final boolean topInIM = topLvlIsInInitModel; |
109 | final String topStr = topLvlString; | 117 | final String topStr = topLvlString; |
110 | InputOutput.<Boolean>print(Boolean.valueOf(topInIM)); | ||
111 | InputOutput.<String>print(topStr); | ||
112 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | 118 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); |
113 | final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> { | 119 | final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> { |
114 | it.setName(this.support.toIDMultiple("containment_topLevel", topName)); | 120 | it.setName(this.support.toIDMultiple("containment_topLevel", topName)); |
@@ -174,8 +180,8 @@ public class Logic2VampireLanguageMapper_ContainmentMapper { | |||
174 | final Type toType = ((Type) _referred); | 180 | final Type toType = ((Type) _referred); |
175 | final VLSFunction toFunc = CollectionsUtil.<Type, VLSFunction>lookup(toType, trace.type2Predicate); | 181 | final VLSFunction toFunc = CollectionsUtil.<Type, VLSFunction>lookup(toType, trace.type2Predicate); |
176 | this.addToMap(type2cont, toFunc, rel); | 182 | this.addToMap(type2cont, toFunc, rel); |
177 | EList<Type> _subtypes_1 = toType.getSubtypes(); | 183 | EList<Type> _subtypes = toType.getSubtypes(); |
178 | for (final Type c_1 : _subtypes_1) { | 184 | for (final Type c_1 : _subtypes) { |
179 | this.addToMap(type2cont, toFunc, rel); | 185 | this.addToMap(type2cont, toFunc, rel); |
180 | } | 186 | } |
181 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); | 187 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); |
@@ -242,9 +248,9 @@ public class Logic2VampireLanguageMapper_ContainmentMapper { | |||
242 | EList<VLSVariable> _variables_1 = it_3.getVariables(); | 248 | EList<VLSVariable> _variables_1 = it_3.getVariables(); |
243 | VLSVariable _duplicate_1 = this.support.duplicate(varB); | 249 | VLSVariable _duplicate_1 = this.support.duplicate(varB); |
244 | _variables_1.add(_duplicate_1); | 250 | _variables_1.add(_duplicate_1); |
245 | int _length = ((Object[])Conversions.unwrapArray(e.getValue(), Object.class)).length; | 251 | int _length_1 = ((Object[])Conversions.unwrapArray(e.getValue(), Object.class)).length; |
246 | boolean _greaterThan = (_length > 1); | 252 | boolean _greaterThan_1 = (_length_1 > 1); |
247 | if (_greaterThan) { | 253 | if (_greaterThan_1) { |
248 | it_3.setOperand(this.makeUnique(e.getValue())); | 254 | it_3.setOperand(this.makeUnique(e.getValue())); |
249 | } else { | 255 | } else { |
250 | it_3.setOperand(e.getValue().get(0)); | 256 | it_3.setOperand(e.getValue().get(0)); |
@@ -282,7 +288,8 @@ public class Logic2VampireLanguageMapper_ContainmentMapper { | |||
282 | { | 288 | { |
283 | for (final Relation l_3 : relationsList) { | 289 | for (final Relation l_3 : relationsList) { |
284 | { | 290 | { |
285 | final VLSFunction rel = this.support.duplicate(CollectionsUtil.<RelationDeclaration, VLSFunction>lookup(((RelationDeclaration) l_3), trace.rel2Predicate), CollectionLiterals.<VLSVariable>newArrayList(variables.get(j), variables.get(((j + 1) % i)))); | 291 | final VLSFunction rel = this.support.duplicate(CollectionsUtil.<RelationDeclaration, VLSFunction>lookup(((RelationDeclaration) l_3), trace.rel2Predicate), |
292 | CollectionLiterals.<VLSVariable>newArrayList(variables.get(j), variables.get(((j + 1) % i)))); | ||
286 | disjunctionList.add(rel); | 293 | disjunctionList.add(rel); |
287 | } | 294 | } |
288 | } | 295 | } |
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 { | |||
47 | this.base = base; | 47 | this.base = base; |
48 | } | 48 | } |
49 | 49 | ||
50 | public void _transformScope(final VampireSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) { | 50 | public void _transformScope(final List<Type> types, final VampireSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) { |
51 | final int ABSOLUTE_MIN = 0; | 51 | final int ABSOLUTE_MIN = 0; |
52 | final int ABSOLUTE_MAX = Integer.MAX_VALUE; | 52 | final int ABSOLUTE_MAX = Integer.MAX_VALUE; |
53 | final int GLOBAL_MIN = config.typeScopes.minNewElements; | 53 | int elemsInIM = trace.definedElement2String.size(); |
54 | final int GLOBAL_MAX = config.typeScopes.maxNewElements; | 54 | final int GLOBAL_MIN = (config.typeScopes.minNewElements - elemsInIM); |
55 | final int GLOBAL_MAX = (config.typeScopes.maxNewElements - elemsInIM); | ||
55 | final ArrayList<VLSConstant> localInstances = CollectionLiterals.<VLSConstant>newArrayList(); | 56 | final ArrayList<VLSConstant> localInstances = CollectionLiterals.<VLSConstant>newArrayList(); |
56 | final boolean consistant = (GLOBAL_MAX > GLOBAL_MIN); | 57 | final boolean consistant = (GLOBAL_MAX > GLOBAL_MIN); |
57 | if ((GLOBAL_MIN != ABSOLUTE_MIN)) { | 58 | if ((GLOBAL_MIN != ABSOLUTE_MIN)) { |
@@ -74,34 +75,37 @@ public class Logic2VampireLanguageMapper_ScopeMapper { | |||
74 | } | 75 | } |
75 | } | 76 | } |
76 | int i_1 = 1; | 77 | int i_1 = 1; |
78 | if ((((Boolean) trace.topLvlElementIsInInitialModel)).booleanValue()) { | ||
79 | i_1 = 0; | ||
80 | } | ||
77 | int minNum = (-1); | 81 | int minNum = (-1); |
78 | Map<Type, Integer> startPoints = new HashMap<Type, Integer>(); | 82 | Map<Type, Integer> startPoints = new HashMap<Type, Integer>(); |
79 | Set<Type> _keySet = config.typeScopes.minNewElementsByType.keySet(); | 83 | Set<Type> _keySet = config.typeScopes.minNewElementsByType.keySet(); |
80 | for (final Type t : _keySet) { | 84 | for (final Type tConfig : _keySet) { |
81 | { | 85 | { |
82 | minNum = (CollectionsUtil.<Type, Integer>lookup(t, config.typeScopes.minNewElementsByType)).intValue(); | 86 | minNum = (CollectionsUtil.<Type, Integer>lookup(tConfig, config.typeScopes.minNewElementsByType)).intValue(); |
83 | if ((minNum != 0)) { | 87 | if ((minNum != 0)) { |
84 | this.getInstanceConstants((i_1 + minNum), i_1, localInstances, trace, true, false); | 88 | this.getInstanceConstants((i_1 + minNum), i_1, localInstances, trace, true, false); |
85 | startPoints.put(t, Integer.valueOf(i_1)); | 89 | startPoints.put(tConfig, Integer.valueOf(i_1)); |
86 | int _i = i_1; | 90 | int _i = i_1; |
87 | i_1 = (_i + minNum); | 91 | i_1 = (_i + minNum); |
88 | this.makeFofFormula(localInstances, trace, true, t); | 92 | this.makeFofFormula(localInstances, trace, true, tConfig); |
89 | } | 93 | } |
90 | } | 94 | } |
91 | } | 95 | } |
92 | Set<Type> _keySet_1 = config.typeScopes.maxNewElementsByType.keySet(); | 96 | Set<Type> _keySet_1 = config.typeScopes.maxNewElementsByType.keySet(); |
93 | for (final Type t_1 : _keySet_1) { | 97 | for (final Type tConfig_1 : _keySet_1) { |
94 | { | 98 | { |
95 | Integer maxNum = CollectionsUtil.<Type, Integer>lookup(t_1, config.typeScopes.maxNewElementsByType); | 99 | Integer maxNum = CollectionsUtil.<Type, Integer>lookup(tConfig_1, config.typeScopes.maxNewElementsByType); |
96 | minNum = (CollectionsUtil.<Type, Integer>lookup(t_1, config.typeScopes.minNewElementsByType)).intValue(); | 100 | minNum = (CollectionsUtil.<Type, Integer>lookup(tConfig_1, config.typeScopes.minNewElementsByType)).intValue(); |
97 | Integer startpoint = CollectionsUtil.<Type, Integer>lookup(t_1, startPoints); | 101 | Integer startpoint = CollectionsUtil.<Type, Integer>lookup(tConfig_1, startPoints); |
98 | if ((minNum != 0)) { | 102 | if ((minNum != 0)) { |
99 | this.getInstanceConstants(((startpoint).intValue() + minNum), (startpoint).intValue(), localInstances, trace, true, false); | 103 | this.getInstanceConstants(((startpoint).intValue() + minNum), (startpoint).intValue(), localInstances, trace, true, false); |
100 | } | 104 | } |
101 | if (((maxNum).intValue() != minNum)) { | 105 | if (((maxNum).intValue() != minNum)) { |
102 | int instEndInd = Math.min(GLOBAL_MAX, ((i_1 + (maxNum).intValue()) - minNum)); | 106 | int instEndInd = Math.min(GLOBAL_MAX, ((i_1 + (maxNum).intValue()) - minNum)); |
103 | this.getInstanceConstants(instEndInd, i_1, localInstances, trace, false, false); | 107 | this.getInstanceConstants(instEndInd, i_1, localInstances, trace, false, false); |
104 | this.makeFofFormula(localInstances, trace, false, t_1); | 108 | this.makeFofFormula(localInstances, trace, false, tConfig_1); |
105 | } | 109 | } |
106 | } | 110 | } |
107 | } | 111 | } |
@@ -246,8 +250,8 @@ public class Logic2VampireLanguageMapper_ScopeMapper { | |||
246 | _formulas.add(cstDec); | 250 | _formulas.add(cstDec); |
247 | } | 251 | } |
248 | 252 | ||
249 | public void transformScope(final VampireSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) { | 253 | public void transformScope(final List<Type> types, final VampireSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) { |
250 | _transformScope(config, trace); | 254 | _transformScope(types, config, trace); |
251 | return; | 255 | return; |
252 | } | 256 | } |
253 | } | 257 | } |
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 { | |||
77 | trace.type2Predicate.put(type, typePred); | 77 | trace.type2Predicate.put(type, typePred); |
78 | } | 78 | } |
79 | } | 79 | } |
80 | Iterable<TypeDefinition> _filter = Iterables.<TypeDefinition>filter(types, TypeDefinition.class); | 80 | final Function1<TypeDefinition, Boolean> _function_1 = (TypeDefinition it) -> { |
81 | boolean _isIsAbstract = it.isIsAbstract(); | ||
82 | return Boolean.valueOf((!_isIsAbstract)); | ||
83 | }; | ||
84 | Iterable<TypeDefinition> _filter = IterableExtensions.<TypeDefinition>filter(Iterables.<TypeDefinition>filter(types, TypeDefinition.class), _function_1); | ||
81 | for (final TypeDefinition type_1 : _filter) { | 85 | for (final TypeDefinition type_1 : _filter) { |
82 | { | 86 | { |
83 | final boolean isNotEnum = ((((Object[])Conversions.unwrapArray(type_1.getSupertypes(), Object.class)).length == 1) && type_1.getSupertypes().get(0).isIsAbstract()); | 87 | final int len = type_1.getName().length(); |
88 | boolean _equals = type_1.getName().substring((len - 4), len).equals("enum"); | ||
89 | final boolean isNotEnum = (!_equals); | ||
84 | final List<VLSFunction> orElems = CollectionLiterals.<VLSFunction>newArrayList(); | 90 | final List<VLSFunction> orElems = CollectionLiterals.<VLSFunction>newArrayList(); |
85 | EList<DefinedElement> _elements = type_1.getElements(); | 91 | EList<DefinedElement> _elements = type_1.getElements(); |
86 | for (final DefinedElement e : _elements) { | 92 | for (final DefinedElement e : _elements) { |
@@ -88,21 +94,21 @@ public class Logic2VampireLanguageMapper_TypeMapper { | |||
88 | final String[] nameArray = e.getName().split(" "); | 94 | final String[] nameArray = e.getName().split(" "); |
89 | String relNameVar = ""; | 95 | String relNameVar = ""; |
90 | int _length = nameArray.length; | 96 | int _length = nameArray.length; |
91 | boolean _equals = (_length == 3); | 97 | boolean _equals_1 = (_length == 3); |
92 | if (_equals) { | 98 | if (_equals_1) { |
93 | relNameVar = this.support.toIDMultiple(nameArray[0], nameArray[2]); | 99 | relNameVar = this.support.toIDMultiple(nameArray[0], nameArray[2]); |
94 | } else { | 100 | } else { |
95 | relNameVar = e.getName(); | 101 | relNameVar = e.getName(); |
96 | } | 102 | } |
97 | final String relName = relNameVar; | 103 | final String relName = relNameVar; |
98 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | 104 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); |
99 | final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> { | 105 | final Procedure1<VLSFunction> _function_2 = (VLSFunction it) -> { |
100 | it.setConstant(this.support.toIDMultiple("e", relName)); | 106 | it.setConstant(this.support.toIDMultiple("e", relName)); |
101 | EList<VLSTerm> _terms = it.getTerms(); | 107 | EList<VLSTerm> _terms = it.getTerms(); |
102 | VLSVariable _duplicate = this.support.duplicate(variable); | 108 | VLSVariable _duplicate = this.support.duplicate(variable); |
103 | _terms.add(_duplicate); | 109 | _terms.add(_duplicate); |
104 | }; | 110 | }; |
105 | final VLSFunction enumElemPred = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_1); | 111 | final VLSFunction enumElemPred = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_2); |
106 | trace.element2Predicate.put(e, enumElemPred); | 112 | trace.element2Predicate.put(e, enumElemPred); |
107 | } | 113 | } |
108 | } | 114 | } |
@@ -113,17 +119,17 @@ public class Logic2VampireLanguageMapper_TypeMapper { | |||
113 | { | 119 | { |
114 | EList<DefinedElement> _elements_2 = type_1.getElements(); | 120 | EList<DefinedElement> _elements_2 = type_1.getElements(); |
115 | for (final DefinedElement t2 : _elements_2) { | 121 | for (final DefinedElement t2 : _elements_2) { |
116 | boolean _equals = Objects.equal(t1, t2); | 122 | boolean _equals_1 = Objects.equal(t1, t2); |
117 | if (_equals) { | 123 | if (_equals_1) { |
118 | final VLSFunction fct = this.support.duplicate(CollectionsUtil.<DefinedElement, VLSFunction>lookup(t2, trace.element2Predicate), variable); | 124 | final VLSFunction fct = this.support.duplicate(CollectionsUtil.<DefinedElement, VLSFunction>lookup(t2, trace.element2Predicate), variable); |
119 | possibleNots.add(fct); | 125 | possibleNots.add(fct); |
120 | } else { | 126 | } else { |
121 | final VLSFunction op = this.support.duplicate(CollectionsUtil.<DefinedElement, VLSFunction>lookup(t2, trace.element2Predicate), variable); | 127 | final VLSFunction op = this.support.duplicate(CollectionsUtil.<DefinedElement, VLSFunction>lookup(t2, trace.element2Predicate), variable); |
122 | VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); | 128 | VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); |
123 | final Procedure1<VLSUnaryNegation> _function_1 = (VLSUnaryNegation it) -> { | 129 | final Procedure1<VLSUnaryNegation> _function_2 = (VLSUnaryNegation it) -> { |
124 | it.setOperand(op); | 130 | it.setOperand(op); |
125 | }; | 131 | }; |
126 | final VLSUnaryNegation negFct = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_1); | 132 | final VLSUnaryNegation negFct = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_2); |
127 | possibleNots.add(negFct); | 133 | possibleNots.add(negFct); |
128 | } | 134 | } |
129 | } | 135 | } |
@@ -132,32 +138,32 @@ public class Logic2VampireLanguageMapper_TypeMapper { | |||
132 | } | 138 | } |
133 | } | 139 | } |
134 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | 140 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); |
135 | final Procedure1<VLSFofFormula> _function_1 = (VLSFofFormula it) -> { | 141 | final Procedure1<VLSFofFormula> _function_2 = (VLSFofFormula it) -> { |
136 | it.setName(this.support.toIDMultiple("typeDef", CollectionsUtil.<TypeDefinition, VLSFunction>lookup(type_1, trace.type2Predicate).getConstant().toString())); | 142 | it.setName(this.support.toIDMultiple("typeDef", CollectionsUtil.<TypeDefinition, VLSFunction>lookup(type_1, trace.type2Predicate).getConstant().toString())); |
137 | it.setFofRole("axiom"); | 143 | it.setFofRole("axiom"); |
138 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | 144 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); |
139 | final Procedure1<VLSUniversalQuantifier> _function_2 = (VLSUniversalQuantifier it_1) -> { | 145 | final Procedure1<VLSUniversalQuantifier> _function_3 = (VLSUniversalQuantifier it_1) -> { |
140 | EList<VLSVariable> _variables = it_1.getVariables(); | 146 | EList<VLSVariable> _variables = it_1.getVariables(); |
141 | VLSVariable _duplicate = this.support.duplicate(variable); | 147 | VLSVariable _duplicate = this.support.duplicate(variable); |
142 | _variables.add(_duplicate); | 148 | _variables.add(_duplicate); |
143 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); | 149 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); |
144 | final Procedure1<VLSEquivalent> _function_3 = (VLSEquivalent it_2) -> { | 150 | final Procedure1<VLSEquivalent> _function_4 = (VLSEquivalent it_2) -> { |
145 | it_2.setLeft(CollectionsUtil.<TypeDefinition, VLSFunction>lookup(type_1, trace.type2Predicate)); | 151 | it_2.setLeft(CollectionsUtil.<TypeDefinition, VLSFunction>lookup(type_1, trace.type2Predicate)); |
146 | VLSAnd _createVLSAnd = this.factory.createVLSAnd(); | 152 | VLSAnd _createVLSAnd = this.factory.createVLSAnd(); |
147 | final Procedure1<VLSAnd> _function_4 = (VLSAnd it_3) -> { | 153 | final Procedure1<VLSAnd> _function_5 = (VLSAnd it_3) -> { |
148 | it_3.setLeft(this.support.topLevelTypeFunc(variable)); | 154 | it_3.setLeft(this.support.topLevelTypeFunc(variable)); |
149 | it_3.setRight(this.support.unfoldOr(typeDefs)); | 155 | it_3.setRight(this.support.unfoldOr(typeDefs)); |
150 | }; | 156 | }; |
151 | VLSAnd _doubleArrow = ObjectExtensions.<VLSAnd>operator_doubleArrow(_createVLSAnd, _function_4); | 157 | VLSAnd _doubleArrow = ObjectExtensions.<VLSAnd>operator_doubleArrow(_createVLSAnd, _function_5); |
152 | it_2.setRight(_doubleArrow); | 158 | it_2.setRight(_doubleArrow); |
153 | }; | 159 | }; |
154 | VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_3); | 160 | VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_4); |
155 | it_1.setOperand(_doubleArrow); | 161 | it_1.setOperand(_doubleArrow); |
156 | }; | 162 | }; |
157 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_2); | 163 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_3); |
158 | it.setFofFormula(_doubleArrow); | 164 | it.setFofFormula(_doubleArrow); |
159 | }; | 165 | }; |
160 | final VLSFofFormula res = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_1); | 166 | final VLSFofFormula res = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_2); |
161 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); | 167 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); |
162 | _formulas.add(res); | 168 | _formulas.add(res); |
163 | for (int i = globalCounter; (i < (globalCounter + ((Object[])Conversions.unwrapArray(type_1.getElements(), Object.class)).length)); i++) { | 169 | for (int i = globalCounter; (i < (globalCounter + ((Object[])Conversions.unwrapArray(type_1.getElements(), Object.class)).length)); i++) { |
@@ -165,17 +171,17 @@ public class Logic2VampireLanguageMapper_TypeMapper { | |||
165 | final int num = (i + 1); | 171 | final int num = (i + 1); |
166 | final int index = (i - globalCounter); | 172 | final int index = (i - globalCounter); |
167 | VLSFunctionAsTerm _createVLSFunctionAsTerm = this.factory.createVLSFunctionAsTerm(); | 173 | VLSFunctionAsTerm _createVLSFunctionAsTerm = this.factory.createVLSFunctionAsTerm(); |
168 | final Procedure1<VLSFunctionAsTerm> _function_2 = (VLSFunctionAsTerm it) -> { | 174 | final Procedure1<VLSFunctionAsTerm> _function_3 = (VLSFunctionAsTerm it) -> { |
169 | it.setFunctor(("eo" + Integer.valueOf(num))); | 175 | it.setFunctor(("eo" + Integer.valueOf(num))); |
170 | }; | 176 | }; |
171 | final VLSFunctionAsTerm cstTerm = ObjectExtensions.<VLSFunctionAsTerm>operator_doubleArrow(_createVLSFunctionAsTerm, _function_2); | 177 | final VLSFunctionAsTerm cstTerm = ObjectExtensions.<VLSFunctionAsTerm>operator_doubleArrow(_createVLSFunctionAsTerm, _function_3); |
172 | if (isNotEnum) { | 178 | if (isNotEnum) { |
173 | trace.definedElement2String.put(type_1.getElements().get(index), cstTerm.getFunctor()); | 179 | trace.definedElement2String.put(type_1.getElements().get(index), cstTerm.getFunctor()); |
174 | } | 180 | } |
175 | final VLSConstant cst = this.support.toConstant(cstTerm); | 181 | final VLSConstant cst = this.support.toConstant(cstTerm); |
176 | trace.uniqueInstances.add(cst); | 182 | trace.uniqueInstances.add(cst); |
177 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); | 183 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); |
178 | final Procedure1<VLSFofFormula> _function_3 = (VLSFofFormula it) -> { | 184 | final Procedure1<VLSFofFormula> _function_4 = (VLSFofFormula it) -> { |
179 | String _xifexpression = null; | 185 | String _xifexpression = null; |
180 | if (isNotEnum) { | 186 | if (isNotEnum) { |
181 | _xifexpression = "definedType"; | 187 | _xifexpression = "definedType"; |
@@ -186,28 +192,28 @@ public class Logic2VampireLanguageMapper_TypeMapper { | |||
186 | type_1.getElements().get(index).getName().split(" ")[0])); | 192 | type_1.getElements().get(index).getName().split(" ")[0])); |
187 | it.setFofRole("axiom"); | 193 | it.setFofRole("axiom"); |
188 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | 194 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); |
189 | final Procedure1<VLSUniversalQuantifier> _function_4 = (VLSUniversalQuantifier it_1) -> { | 195 | final Procedure1<VLSUniversalQuantifier> _function_5 = (VLSUniversalQuantifier it_1) -> { |
190 | EList<VLSVariable> _variables = it_1.getVariables(); | 196 | EList<VLSVariable> _variables = it_1.getVariables(); |
191 | VLSVariable _duplicate = this.support.duplicate(variable); | 197 | VLSVariable _duplicate = this.support.duplicate(variable); |
192 | _variables.add(_duplicate); | 198 | _variables.add(_duplicate); |
193 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); | 199 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); |
194 | final Procedure1<VLSEquivalent> _function_5 = (VLSEquivalent it_2) -> { | 200 | final Procedure1<VLSEquivalent> _function_6 = (VLSEquivalent it_2) -> { |
195 | VLSEquality _createVLSEquality = this.factory.createVLSEquality(); | 201 | VLSEquality _createVLSEquality = this.factory.createVLSEquality(); |
196 | final Procedure1<VLSEquality> _function_6 = (VLSEquality it_3) -> { | 202 | final Procedure1<VLSEquality> _function_7 = (VLSEquality it_3) -> { |
197 | it_3.setLeft(this.support.duplicate(variable)); | 203 | it_3.setLeft(this.support.duplicate(variable)); |
198 | it_3.setRight(this.support.duplicate(this.support.toConstant(cstTerm))); | 204 | it_3.setRight(this.support.duplicate(this.support.toConstant(cstTerm))); |
199 | }; | 205 | }; |
200 | VLSEquality _doubleArrow = ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_6); | 206 | VLSEquality _doubleArrow = ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_7); |
201 | it_2.setLeft(_doubleArrow); | 207 | it_2.setLeft(_doubleArrow); |
202 | it_2.setRight(this.support.duplicate(CollectionsUtil.<DefinedElement, VLSFunction>lookup(type_1.getElements().get(index), trace.element2Predicate), variable)); | 208 | it_2.setRight(this.support.duplicate(CollectionsUtil.<DefinedElement, VLSFunction>lookup(type_1.getElements().get(index), trace.element2Predicate), variable)); |
203 | }; | 209 | }; |
204 | VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_5); | 210 | VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_6); |
205 | it_1.setOperand(_doubleArrow); | 211 | it_1.setOperand(_doubleArrow); |
206 | }; | 212 | }; |
207 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_4); | 213 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_5); |
208 | it.setFofFormula(_doubleArrow); | 214 | it.setFofFormula(_doubleArrow); |
209 | }; | 215 | }; |
210 | final VLSFofFormula enumScope = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_3); | 216 | final VLSFofFormula enumScope = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_4); |
211 | EList<VLSFofFormula> _formulas_1 = trace.specification.getFormulas(); | 217 | EList<VLSFofFormula> _formulas_1 = trace.specification.getFormulas(); |
212 | _formulas_1.add(enumScope); | 218 | _formulas_1.add(enumScope); |
213 | } | 219 | } |
@@ -217,11 +223,11 @@ public class Logic2VampireLanguageMapper_TypeMapper { | |||
217 | globalCounter = (_globalCounter + _size); | 223 | globalCounter = (_globalCounter + _size); |
218 | } | 224 | } |
219 | } | 225 | } |
220 | final Function1<Type, Boolean> _function_1 = (Type it) -> { | 226 | final Function1<Type, Boolean> _function_2 = (Type it) -> { |
221 | boolean _isIsAbstract = it.isIsAbstract(); | 227 | boolean _isIsAbstract = it.isIsAbstract(); |
222 | return Boolean.valueOf((!_isIsAbstract)); | 228 | return Boolean.valueOf((!_isIsAbstract)); |
223 | }; | 229 | }; |
224 | Iterable<Type> _filter_1 = IterableExtensions.<Type>filter(types, _function_1); | 230 | Iterable<Type> _filter_1 = IterableExtensions.<Type>filter(types, _function_2); |
225 | for (final Type t1 : _filter_1) { | 231 | for (final Type t1 : _filter_1) { |
226 | { | 232 | { |
227 | for (final Type t2 : types) { | 233 | for (final Type t2 : types) { |
@@ -229,10 +235,10 @@ public class Logic2VampireLanguageMapper_TypeMapper { | |||
229 | trace.type2PossibleNot.put(t2, this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(t2, trace.type2Predicate))); | 235 | trace.type2PossibleNot.put(t2, this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(t2, trace.type2Predicate))); |
230 | } else { | 236 | } else { |
231 | VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); | 237 | VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); |
232 | final Procedure1<VLSUnaryNegation> _function_2 = (VLSUnaryNegation it) -> { | 238 | final Procedure1<VLSUnaryNegation> _function_3 = (VLSUnaryNegation it) -> { |
233 | it.setOperand(this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(t2, trace.type2Predicate))); | 239 | it.setOperand(this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(t2, trace.type2Predicate))); |
234 | }; | 240 | }; |
235 | VLSUnaryNegation _doubleArrow = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_2); | 241 | VLSUnaryNegation _doubleArrow = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_3); |
236 | trace.type2PossibleNot.put(t2, _doubleArrow); | 242 | trace.type2PossibleNot.put(t2, _doubleArrow); |
237 | } | 243 | } |
238 | } | 244 | } |
@@ -245,63 +251,63 @@ public class Logic2VampireLanguageMapper_TypeMapper { | |||
245 | final List<VLSTerm> type2Not = CollectionLiterals.<VLSTerm>newArrayList(); | 251 | final List<VLSTerm> type2Not = CollectionLiterals.<VLSTerm>newArrayList(); |
246 | for (final Type t : types) { | 252 | for (final Type t : types) { |
247 | VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); | 253 | VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); |
248 | final Procedure1<VLSUnaryNegation> _function_2 = (VLSUnaryNegation it) -> { | 254 | final Procedure1<VLSUnaryNegation> _function_3 = (VLSUnaryNegation it) -> { |
249 | it.setOperand(this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(t, trace.type2Predicate))); | 255 | it.setOperand(this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(t, trace.type2Predicate))); |
250 | }; | 256 | }; |
251 | VLSUnaryNegation _doubleArrow = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_2); | 257 | VLSUnaryNegation _doubleArrow = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_3); |
252 | type2Not.add(_doubleArrow); | 258 | type2Not.add(_doubleArrow); |
253 | } | 259 | } |
254 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | 260 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); |
255 | final Procedure1<VLSFofFormula> _function_3 = (VLSFofFormula it) -> { | 261 | final Procedure1<VLSFofFormula> _function_4 = (VLSFofFormula it) -> { |
256 | it.setName("notObjectHandler"); | 262 | it.setName("notObjectHandler"); |
257 | it.setFofRole("axiom"); | 263 | it.setFofRole("axiom"); |
258 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | 264 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); |
259 | final Procedure1<VLSUniversalQuantifier> _function_4 = (VLSUniversalQuantifier it_1) -> { | 265 | final Procedure1<VLSUniversalQuantifier> _function_5 = (VLSUniversalQuantifier it_1) -> { |
260 | EList<VLSVariable> _variables = it_1.getVariables(); | 266 | EList<VLSVariable> _variables = it_1.getVariables(); |
261 | VLSVariable _duplicate = this.support.duplicate(variable); | 267 | VLSVariable _duplicate = this.support.duplicate(variable); |
262 | _variables.add(_duplicate); | 268 | _variables.add(_duplicate); |
263 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); | 269 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); |
264 | final Procedure1<VLSEquivalent> _function_5 = (VLSEquivalent it_2) -> { | 270 | final Procedure1<VLSEquivalent> _function_6 = (VLSEquivalent it_2) -> { |
265 | VLSUnaryNegation _createVLSUnaryNegation_1 = this.factory.createVLSUnaryNegation(); | 271 | VLSUnaryNegation _createVLSUnaryNegation_1 = this.factory.createVLSUnaryNegation(); |
266 | final Procedure1<VLSUnaryNegation> _function_6 = (VLSUnaryNegation it_3) -> { | 272 | final Procedure1<VLSUnaryNegation> _function_7 = (VLSUnaryNegation it_3) -> { |
267 | it_3.setOperand(this.support.topLevelTypeFunc()); | 273 | it_3.setOperand(this.support.topLevelTypeFunc()); |
268 | }; | 274 | }; |
269 | VLSUnaryNegation _doubleArrow_1 = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation_1, _function_6); | 275 | VLSUnaryNegation _doubleArrow_1 = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation_1, _function_7); |
270 | it_2.setLeft(_doubleArrow_1); | 276 | it_2.setLeft(_doubleArrow_1); |
271 | it_2.setRight(this.support.unfoldAnd(type2Not)); | 277 | it_2.setRight(this.support.unfoldAnd(type2Not)); |
272 | }; | 278 | }; |
273 | VLSEquivalent _doubleArrow_1 = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_5); | 279 | VLSEquivalent _doubleArrow_1 = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_6); |
274 | it_1.setOperand(_doubleArrow_1); | 280 | it_1.setOperand(_doubleArrow_1); |
275 | }; | 281 | }; |
276 | VLSUniversalQuantifier _doubleArrow_1 = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_4); | 282 | VLSUniversalQuantifier _doubleArrow_1 = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_5); |
277 | it.setFofFormula(_doubleArrow_1); | 283 | it.setFofFormula(_doubleArrow_1); |
278 | }; | 284 | }; |
279 | final VLSFofFormula notObj = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_3); | 285 | final VLSFofFormula notObj = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_4); |
280 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); | 286 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); |
281 | _formulas.add(notObj); | 287 | _formulas.add(notObj); |
282 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); | 288 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); |
283 | final Procedure1<VLSFofFormula> _function_4 = (VLSFofFormula it) -> { | 289 | final Procedure1<VLSFofFormula> _function_5 = (VLSFofFormula it) -> { |
284 | it.setName("inheritanceHierarchyHandler"); | 290 | it.setName("inheritanceHierarchyHandler"); |
285 | it.setFofRole("axiom"); | 291 | it.setFofRole("axiom"); |
286 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | 292 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); |
287 | final Procedure1<VLSUniversalQuantifier> _function_5 = (VLSUniversalQuantifier it_1) -> { | 293 | final Procedure1<VLSUniversalQuantifier> _function_6 = (VLSUniversalQuantifier it_1) -> { |
288 | EList<VLSVariable> _variables = it_1.getVariables(); | 294 | EList<VLSVariable> _variables = it_1.getVariables(); |
289 | VLSVariable _duplicate = this.support.duplicate(variable); | 295 | VLSVariable _duplicate = this.support.duplicate(variable); |
290 | _variables.add(_duplicate); | 296 | _variables.add(_duplicate); |
291 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); | 297 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); |
292 | final Procedure1<VLSEquivalent> _function_6 = (VLSEquivalent it_2) -> { | 298 | final Procedure1<VLSEquivalent> _function_7 = (VLSEquivalent it_2) -> { |
293 | it_2.setLeft(this.support.topLevelTypeFunc()); | 299 | it_2.setLeft(this.support.topLevelTypeFunc()); |
294 | Collection<VLSTerm> _values = trace.type2And.values(); | 300 | Collection<VLSTerm> _values = trace.type2And.values(); |
295 | final ArrayList<VLSTerm> reversedList = new ArrayList<VLSTerm>(_values); | 301 | final ArrayList<VLSTerm> reversedList = new ArrayList<VLSTerm>(_values); |
296 | it_2.setRight(this.support.unfoldOr(reversedList)); | 302 | it_2.setRight(this.support.unfoldOr(reversedList)); |
297 | }; | 303 | }; |
298 | VLSEquivalent _doubleArrow_1 = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_6); | 304 | VLSEquivalent _doubleArrow_1 = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_7); |
299 | it_1.setOperand(_doubleArrow_1); | 305 | it_1.setOperand(_doubleArrow_1); |
300 | }; | 306 | }; |
301 | VLSUniversalQuantifier _doubleArrow_1 = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_5); | 307 | VLSUniversalQuantifier _doubleArrow_1 = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_6); |
302 | it.setFofFormula(_doubleArrow_1); | 308 | it.setFofFormula(_doubleArrow_1); |
303 | }; | 309 | }; |
304 | final VLSFofFormula hierarch = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_4); | 310 | final VLSFofFormula hierarch = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_5); |
305 | EList<VLSFofFormula> _formulas_1 = trace.specification.getFormulas(); | 311 | EList<VLSFofFormula> _formulas_1 = trace.specification.getFormulas(); |
306 | _xblockexpression = _formulas_1.add(hierarch); | 312 | _xblockexpression = _formulas_1.add(hierarch); |
307 | } | 313 | } |