diff options
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca')
14 files changed, 38 insertions, 16 deletions
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin index 5c634ba0..b86e8068 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin | |||
Binary files differ | |||
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 19d48790..052e0175 100644 --- 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 | |||
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.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin index 2db39cf0..1296bf9e 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 1fba7ac4..0210a300 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 9ef3a39c..fd625384 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_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 687f4889..978571d2 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 d59b2e98..b98f0332 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 eb12e24a..8238a89e 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 70eb3434..f64a218b 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/.Vampire2LogicMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin index 0077e151..cf8e4acd 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.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/.VampireHandler.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin index 62de24fc..07d5b7b4 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.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/.VampireModelInterpretation_TypeInterpretation.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin index d00ac8ca..983108a2 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.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/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin index b86330dc..4442cdea 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.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.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java index a412241a..1950cad0 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 | |||
@@ -6,6 +6,7 @@ import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguage | |||
6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant; | 6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant; |
7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality; | 7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality; |
8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; | 8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; |
9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; | ||
9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies; | 10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies; |
10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; | 11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; |
11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; | 12 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; |
@@ -15,6 +16,8 @@ import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration; | |||
15 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; | 16 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; |
16 | import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; | 17 | import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; |
17 | import java.util.ArrayList; | 18 | import java.util.ArrayList; |
19 | import java.util.HashMap; | ||
20 | import java.util.Map; | ||
18 | import java.util.Set; | 21 | import java.util.Set; |
19 | import org.eclipse.emf.common.util.EList; | 22 | import org.eclipse.emf.common.util.EList; |
20 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; | 23 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; |
@@ -47,24 +50,26 @@ public class Logic2VampireLanguageMapper_ScopeMapper { | |||
47 | final int GLOBAL_MAX = config.typeScopes.maxNewElements; | 50 | final int GLOBAL_MAX = config.typeScopes.maxNewElements; |
48 | final ArrayList<Object> localInstances = CollectionLiterals.<Object>newArrayList(); | 51 | final ArrayList<Object> localInstances = CollectionLiterals.<Object>newArrayList(); |
49 | if ((GLOBAL_MIN != 0)) { | 52 | if ((GLOBAL_MIN != 0)) { |
50 | this.getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, false); | 53 | this.getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, false); |
51 | this.makeFofFormula(localInstances, trace, true, "object"); | 54 | this.makeFofFormula(localInstances, trace, true, null); |
52 | } | 55 | } |
53 | if ((GLOBAL_MAX != 0)) { | 56 | if ((GLOBAL_MAX != 0)) { |
54 | this.getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true); | 57 | this.getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, true); |
55 | this.makeFofFormula(localInstances, trace, false, "object"); | 58 | this.makeFofFormula(localInstances, trace, false, null); |
56 | } | 59 | } |
57 | int i = 0; | 60 | int i = 0; |
58 | int minNum = (-1); | 61 | int minNum = (-1); |
62 | Map<Type, Integer> startPoints = new HashMap<Type, Integer>(); | ||
59 | Set<Type> _keySet = config.typeScopes.minNewElementsByType.keySet(); | 63 | Set<Type> _keySet = config.typeScopes.minNewElementsByType.keySet(); |
60 | for (final Type t : _keySet) { | 64 | for (final Type t : _keySet) { |
61 | { | 65 | { |
62 | minNum = (CollectionsUtil.<Type, Integer>lookup(t, config.typeScopes.minNewElementsByType)).intValue(); | 66 | minNum = (CollectionsUtil.<Type, Integer>lookup(t, config.typeScopes.minNewElementsByType)).intValue(); |
63 | if ((minNum != 0)) { | 67 | if ((minNum != 0)) { |
64 | this.getInstanceConstants((i + minNum), i, localInstances, trace, false); | 68 | this.getInstanceConstants((i + minNum), i, localInstances, trace, true, false); |
69 | startPoints.put(t, Integer.valueOf(i)); | ||
65 | int _i = i; | 70 | int _i = i; |
66 | i = (_i + minNum); | 71 | i = (_i + minNum); |
67 | this.makeFofFormula(localInstances, trace, true, t.toString()); | 72 | this.makeFofFormula(localInstances, trace, true, t); |
68 | } | 73 | } |
69 | } | 74 | } |
70 | } | 75 | } |
@@ -73,10 +78,14 @@ public class Logic2VampireLanguageMapper_ScopeMapper { | |||
73 | { | 78 | { |
74 | Integer maxNum = CollectionsUtil.<Type, Integer>lookup(t_1, config.typeScopes.maxNewElementsByType); | 79 | Integer maxNum = CollectionsUtil.<Type, Integer>lookup(t_1, config.typeScopes.maxNewElementsByType); |
75 | minNum = (CollectionsUtil.<Type, Integer>lookup(t_1, config.typeScopes.minNewElementsByType)).intValue(); | 80 | minNum = (CollectionsUtil.<Type, Integer>lookup(t_1, config.typeScopes.minNewElementsByType)).intValue(); |
76 | if (((maxNum).intValue() != 0)) { | 81 | Integer startpoint = CollectionsUtil.<Type, Integer>lookup(t_1, startPoints); |
77 | int forLimit = Math.min(GLOBAL_MAX, ((i + (maxNum).intValue()) - minNum)); | 82 | if ((minNum != 0)) { |
78 | this.getInstanceConstants(GLOBAL_MAX, i, localInstances, trace, false); | 83 | this.getInstanceConstants(((startpoint).intValue() + minNum), (startpoint).intValue(), localInstances, trace, true, false); |
79 | this.makeFofFormula(localInstances, trace, false, t_1.toString()); | 84 | } |
85 | if (((maxNum).intValue() != minNum)) { | ||
86 | int instEndInd = Math.min(GLOBAL_MAX, ((i + (maxNum).intValue()) - minNum)); | ||
87 | this.getInstanceConstants(instEndInd, i, localInstances, trace, false, false); | ||
88 | this.makeFofFormula(localInstances, trace, false, t_1); | ||
80 | } | 89 | } |
81 | } | 90 | } |
82 | } | 91 | } |
@@ -95,9 +104,11 @@ public class Logic2VampireLanguageMapper_ScopeMapper { | |||
95 | } | 104 | } |
96 | } | 105 | } |
97 | 106 | ||
98 | protected void getInstanceConstants(final int numElems, final int init, final ArrayList list, final Logic2VampireLanguageMapperTrace trace, final boolean addToTrace) { | 107 | protected void getInstanceConstants(final int endInd, final int startInd, final ArrayList list, final Logic2VampireLanguageMapperTrace trace, final boolean clear, final boolean addToTrace) { |
99 | list.clear(); | 108 | if (clear) { |
100 | for (int i = init; (i < numElems); i++) { | 109 | list.clear(); |
110 | } | ||
111 | for (int i = startInd; (i < endInd); i++) { | ||
101 | { | 112 | { |
102 | final int num = (i + 1); | 113 | final int num = (i + 1); |
103 | VLSConstant _createVLSConstant = this.factory.createVLSConstant(); | 114 | VLSConstant _createVLSConstant = this.factory.createVLSConstant(); |
@@ -113,7 +124,18 @@ public class Logic2VampireLanguageMapper_ScopeMapper { | |||
113 | } | 124 | } |
114 | } | 125 | } |
115 | 126 | ||
116 | protected void makeFofFormula(final ArrayList list, final Logic2VampireLanguageMapperTrace trace, final boolean minimum, final String name) { | 127 | protected void makeFofFormula(final ArrayList list, final Logic2VampireLanguageMapperTrace trace, final boolean minimum, final Type type) { |
128 | String nm = ""; | ||
129 | VLSFunction tm = null; | ||
130 | if ((type == null)) { | ||
131 | nm = "object"; | ||
132 | tm = this.support.topLevelTypeFunc(); | ||
133 | } else { | ||
134 | nm = CollectionsUtil.<Type, VLSFunction>lookup(type, trace.type2Predicate).getConstant().toString(); | ||
135 | tm = this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(type, trace.type2Predicate)); | ||
136 | } | ||
137 | final String name = nm; | ||
138 | final VLSFunction term = tm; | ||
117 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | 139 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); |
118 | final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> { | 140 | final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> { |
119 | String _xifexpression = null; | 141 | String _xifexpression = null; |
@@ -146,8 +168,9 @@ public class Logic2VampireLanguageMapper_ScopeMapper { | |||
146 | return ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_4); | 168 | return ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_4); |
147 | }; | 169 | }; |
148 | it_2.setLeft(this.support.unfoldOr(ListExtensions.<VLSTerm, VLSEquality>map(list, _function_3))); | 170 | it_2.setLeft(this.support.unfoldOr(ListExtensions.<VLSTerm, VLSEquality>map(list, _function_3))); |
149 | it_2.setRight(this.support.topLevelTypeFunc()); | 171 | it_2.setRight(term); |
150 | } else { | 172 | } else { |
173 | it_2.setLeft(term); | ||
151 | final Function1<VLSTerm, VLSEquality> _function_4 = (VLSTerm i) -> { | 174 | final Function1<VLSTerm, VLSEquality> _function_4 = (VLSTerm i) -> { |
152 | VLSEquality _createVLSEquality = this.factory.createVLSEquality(); | 175 | VLSEquality _createVLSEquality = this.factory.createVLSEquality(); |
153 | final Procedure1<VLSEquality> _function_5 = (VLSEquality it_3) -> { | 176 | final Procedure1<VLSEquality> _function_5 = (VLSEquality it_3) -> { |
@@ -162,7 +185,6 @@ public class Logic2VampireLanguageMapper_ScopeMapper { | |||
162 | return ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_5); | 185 | return ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_5); |
163 | }; | 186 | }; |
164 | it_2.setRight(this.support.unfoldOr(ListExtensions.<VLSTerm, VLSEquality>map(list, _function_4))); | 187 | it_2.setRight(this.support.unfoldOr(ListExtensions.<VLSTerm, VLSEquality>map(list, _function_4))); |
165 | it_2.setLeft(this.support.topLevelTypeFunc()); | ||
166 | } | 188 | } |
167 | }; | 189 | }; |
168 | VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_2); | 190 | VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_2); |