diff options
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java')
-rw-r--r-- | Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java | 386 |
1 files changed, 0 insertions, 386 deletions
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 deleted file mode 100644 index 2100b92f..00000000 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java +++ /dev/null | |||
@@ -1,386 +0,0 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; | ||
2 | |||
3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration; | ||
4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; | ||
5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; | ||
6 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; | ||
7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant; | ||
8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality; | ||
9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent; | ||
10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSExistentialQuantifier; | ||
11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; | ||
12 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; | ||
13 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies; | ||
14 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; | ||
15 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTffTerm; | ||
16 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUnaryNegation; | ||
17 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; | ||
18 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; | ||
19 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; | ||
20 | import com.google.common.base.Objects; | ||
21 | import com.google.common.collect.Iterables; | ||
22 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference; | ||
23 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement; | ||
24 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation; | ||
25 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration; | ||
26 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; | ||
27 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition; | ||
28 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference; | ||
29 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.impl.TypeDefinitionImpl; | ||
30 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy; | ||
31 | import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; | ||
32 | import java.util.ArrayList; | ||
33 | import java.util.HashMap; | ||
34 | import java.util.List; | ||
35 | import java.util.Map; | ||
36 | import java.util.Set; | ||
37 | import org.eclipse.emf.common.util.EList; | ||
38 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; | ||
39 | import org.eclipse.xtext.xbase.lib.Conversions; | ||
40 | import org.eclipse.xtext.xbase.lib.Extension; | ||
41 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; | ||
42 | import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; | ||
43 | |||
44 | @SuppressWarnings("all") | ||
45 | public class Logic2VampireLanguageMapper_ContainmentMapper { | ||
46 | @Extension | ||
47 | private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE; | ||
48 | |||
49 | private final Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support(); | ||
50 | |||
51 | private final Logic2VampireLanguageMapper base; | ||
52 | |||
53 | private final VLSVariable variable = ObjectExtensions.<VLSVariable>operator_doubleArrow(this.factory.createVLSVariable(), ((Procedure1<VLSVariable>) (VLSVariable it) -> { | ||
54 | it.setName("A"); | ||
55 | })); | ||
56 | |||
57 | public Logic2VampireLanguageMapper_ContainmentMapper(final Logic2VampireLanguageMapper base) { | ||
58 | this.base = base; | ||
59 | } | ||
60 | |||
61 | public void transformContainment(final VampireSolverConfiguration config, final List<ContainmentHierarchy> hierarchies, final Logic2VampireLanguageMapperTrace trace) { | ||
62 | final ContainmentHierarchy hierarchy = hierarchies.get(0); | ||
63 | final EList<Type> containmentListCopy = hierarchy.getTypesOrderedInHierarchy(); | ||
64 | final EList<Relation> relationsList = hierarchy.getContainmentRelations(); | ||
65 | final ArrayList<Object> toRemove = CollectionLiterals.<Object>newArrayList(); | ||
66 | for (final Relation l : relationsList) { | ||
67 | { | ||
68 | TypeReference _get = l.getParameters().get(1); | ||
69 | Type _referred = ((ComplexTypeReference) _get).getReferred(); | ||
70 | Type pointingTo = ((Type) _referred); | ||
71 | containmentListCopy.remove(pointingTo); | ||
72 | List<Type> allSubtypes = CollectionLiterals.<Type>newArrayList(); | ||
73 | this.support.listSubtypes(pointingTo, allSubtypes); | ||
74 | for (final Type c : allSubtypes) { | ||
75 | containmentListCopy.remove(c); | ||
76 | } | ||
77 | } | ||
78 | } | ||
79 | Type topTermVar = containmentListCopy.get(0); | ||
80 | for (final Relation l_1 : relationsList) { | ||
81 | { | ||
82 | TypeReference _get = l_1.getParameters().get(0); | ||
83 | Type _referred = ((ComplexTypeReference) _get).getReferred(); | ||
84 | Type pointingFrom = ((Type) _referred); | ||
85 | boolean _contains = containmentListCopy.contains(pointingFrom); | ||
86 | if (_contains) { | ||
87 | topTermVar = pointingFrom; | ||
88 | } | ||
89 | } | ||
90 | } | ||
91 | final String topName = CollectionsUtil.<Type, VLSFunction>lookup(topTermVar, trace.type2Predicate).getConstant().toString(); | ||
92 | final VLSFunction topTerm = this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(topTermVar, trace.type2Predicate)); | ||
93 | trace.topLevelType = topTermVar; | ||
94 | boolean topLvlIsInInitModel = false; | ||
95 | String topLvlString = ""; | ||
96 | ArrayList<Type> listToCheck = CollectionLiterals.<Type>newArrayList(topTermVar); | ||
97 | listToCheck.addAll(topTermVar.getSubtypes()); | ||
98 | for (final Type c : listToCheck) { | ||
99 | Class<? extends Type> _class = c.getClass(); | ||
100 | boolean _equals = Objects.equal(_class, TypeDefinitionImpl.class); | ||
101 | if (_equals) { | ||
102 | int _length = ((Object[])Conversions.unwrapArray(((TypeDefinition) c).getElements(), Object.class)).length; | ||
103 | boolean _greaterThan = (_length > 1); | ||
104 | if (_greaterThan) { | ||
105 | throw new IllegalArgumentException("You cannot have multiple top-level elements in your initial model"); | ||
106 | } | ||
107 | EList<DefinedElement> _elements = ((TypeDefinition) c).getElements(); | ||
108 | for (final DefinedElement d : _elements) { | ||
109 | boolean _containsKey = trace.definedElement2String.containsKey(d); | ||
110 | if (_containsKey) { | ||
111 | topLvlIsInInitModel = true; | ||
112 | topLvlString = CollectionsUtil.<DefinedElement, String>lookup(d, trace.definedElement2String); | ||
113 | } | ||
114 | } | ||
115 | } | ||
116 | } | ||
117 | trace.topLvlElementIsInInitialModel = Boolean.valueOf(topLvlIsInInitModel); | ||
118 | final boolean topInIM = topLvlIsInInitModel; | ||
119 | final String topStr = topLvlString; | ||
120 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | ||
121 | final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> { | ||
122 | it.setName(this.support.toIDMultiple("containment_topLevel", topName)); | ||
123 | it.setFofRole("axiom"); | ||
124 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | ||
125 | final Procedure1<VLSUniversalQuantifier> _function_1 = (VLSUniversalQuantifier it_1) -> { | ||
126 | EList<VLSTffTerm> _variables = it_1.getVariables(); | ||
127 | VLSVariable _duplicate = this.support.duplicate(this.variable); | ||
128 | _variables.add(_duplicate); | ||
129 | VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); | ||
130 | final Procedure1<VLSEquivalent> _function_2 = (VLSEquivalent it_2) -> { | ||
131 | it_2.setLeft(topTerm); | ||
132 | VLSEquality _createVLSEquality = this.factory.createVLSEquality(); | ||
133 | final Procedure1<VLSEquality> _function_3 = (VLSEquality it_3) -> { | ||
134 | it_3.setLeft(this.support.duplicate(this.variable)); | ||
135 | VLSConstant _createVLSConstant = this.factory.createVLSConstant(); | ||
136 | final Procedure1<VLSConstant> _function_4 = (VLSConstant it_4) -> { | ||
137 | String _xifexpression = null; | ||
138 | if (topInIM) { | ||
139 | _xifexpression = topStr; | ||
140 | } else { | ||
141 | _xifexpression = "o1"; | ||
142 | } | ||
143 | it_4.setName(_xifexpression); | ||
144 | }; | ||
145 | VLSConstant _doubleArrow = ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _function_4); | ||
146 | it_3.setRight(_doubleArrow); | ||
147 | }; | ||
148 | VLSEquality _doubleArrow = ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_3); | ||
149 | it_2.setRight(_doubleArrow); | ||
150 | }; | ||
151 | VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_2); | ||
152 | it_1.setOperand(_doubleArrow); | ||
153 | }; | ||
154 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_1); | ||
155 | it.setFofFormula(_doubleArrow); | ||
156 | }; | ||
157 | final VLSFofFormula contTop = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function); | ||
158 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); | ||
159 | _formulas.add(contTop); | ||
160 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | ||
161 | final Procedure1<VLSVariable> _function_1 = (VLSVariable it) -> { | ||
162 | it.setName("A"); | ||
163 | }; | ||
164 | final VLSVariable varA = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_1); | ||
165 | VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable(); | ||
166 | final Procedure1<VLSVariable> _function_2 = (VLSVariable it) -> { | ||
167 | it.setName("B"); | ||
168 | }; | ||
169 | final VLSVariable varB = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_2); | ||
170 | VLSVariable _createVLSVariable_2 = this.factory.createVLSVariable(); | ||
171 | final Procedure1<VLSVariable> _function_3 = (VLSVariable it) -> { | ||
172 | it.setName("C"); | ||
173 | }; | ||
174 | final VLSVariable varC = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_2, _function_3); | ||
175 | final ArrayList<VLSVariable> varList = CollectionLiterals.<VLSVariable>newArrayList(varB, varA); | ||
176 | final Map<VLSFunction, List<VLSFunction>> type2cont = new HashMap<VLSFunction, List<VLSFunction>>(); | ||
177 | for (final Relation l_2 : relationsList) { | ||
178 | { | ||
179 | final VLSFunction rel = CollectionsUtil.<RelationDeclaration, VLSFunction>lookup(((RelationDeclaration) l_2), trace.rel2Predicate); | ||
180 | TypeReference _get = l_2.getParameters().get(1); | ||
181 | Type _referred = ((ComplexTypeReference) _get).getReferred(); | ||
182 | final Type toType = ((Type) _referred); | ||
183 | final VLSFunction toFunc = CollectionsUtil.<Type, VLSFunction>lookup(toType, trace.type2Predicate); | ||
184 | this.addToMap(type2cont, this.support.duplicate(toFunc), this.support.duplicate(rel, varList)); | ||
185 | ArrayList<Type> subTypes = CollectionLiterals.<Type>newArrayList(); | ||
186 | this.support.listSubtypes(toType, subTypes); | ||
187 | for (final Type c_1 : subTypes) { | ||
188 | this.addToMap(type2cont, this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(c_1, trace.type2Predicate)), this.support.duplicate(rel, varList)); | ||
189 | } | ||
190 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); | ||
191 | final Procedure1<VLSFofFormula> _function_4 = (VLSFofFormula it) -> { | ||
192 | it.setName(this.support.toIDMultiple("containment_noDup", rel.getConstant().toString())); | ||
193 | it.setFofRole("axiom"); | ||
194 | VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier(); | ||
195 | final Procedure1<VLSExistentialQuantifier> _function_5 = (VLSExistentialQuantifier it_1) -> { | ||
196 | EList<VLSTffTerm> _variables = it_1.getVariables(); | ||
197 | VLSVariable _duplicate = this.support.duplicate(varA); | ||
198 | _variables.add(_duplicate); | ||
199 | EList<VLSTffTerm> _variables_1 = it_1.getVariables(); | ||
200 | VLSVariable _duplicate_1 = this.support.duplicate(varB); | ||
201 | _variables_1.add(_duplicate_1); | ||
202 | VLSImplies _createVLSImplies = this.factory.createVLSImplies(); | ||
203 | final Procedure1<VLSImplies> _function_6 = (VLSImplies it_2) -> { | ||
204 | it_2.setLeft(this.support.duplicate(rel, CollectionLiterals.<VLSVariable>newArrayList(varA, varB))); | ||
205 | VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); | ||
206 | final Procedure1<VLSUnaryNegation> _function_7 = (VLSUnaryNegation it_3) -> { | ||
207 | VLSExistentialQuantifier _createVLSExistentialQuantifier_1 = this.factory.createVLSExistentialQuantifier(); | ||
208 | final Procedure1<VLSExistentialQuantifier> _function_8 = (VLSExistentialQuantifier it_4) -> { | ||
209 | EList<VLSTffTerm> _variables_2 = it_4.getVariables(); | ||
210 | VLSVariable _duplicate_2 = this.support.duplicate(varC); | ||
211 | _variables_2.add(_duplicate_2); | ||
212 | EList<VLSTffTerm> _variables_3 = it_4.getVariables(); | ||
213 | VLSVariable _duplicate_3 = this.support.duplicate(varB); | ||
214 | _variables_3.add(_duplicate_3); | ||
215 | it_4.setOperand(this.support.duplicate(rel, CollectionLiterals.<VLSVariable>newArrayList(varC, varB))); | ||
216 | }; | ||
217 | VLSExistentialQuantifier _doubleArrow = ObjectExtensions.<VLSExistentialQuantifier>operator_doubleArrow(_createVLSExistentialQuantifier_1, _function_8); | ||
218 | it_3.setOperand(_doubleArrow); | ||
219 | }; | ||
220 | VLSUnaryNegation _doubleArrow = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_7); | ||
221 | it_2.setRight(_doubleArrow); | ||
222 | }; | ||
223 | VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_6); | ||
224 | it_1.setOperand(_doubleArrow); | ||
225 | }; | ||
226 | VLSExistentialQuantifier _doubleArrow = ObjectExtensions.<VLSExistentialQuantifier>operator_doubleArrow(_createVLSExistentialQuantifier, _function_5); | ||
227 | it.setFofFormula(_doubleArrow); | ||
228 | }; | ||
229 | final VLSFofFormula relFormula = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_4); | ||
230 | EList<VLSFofFormula> _formulas_1 = trace.specification.getFormulas(); | ||
231 | _formulas_1.add(relFormula); | ||
232 | } | ||
233 | } | ||
234 | Set<Map.Entry<VLSFunction, List<VLSFunction>>> _entrySet = type2cont.entrySet(); | ||
235 | for (final Map.Entry<VLSFunction, List<VLSFunction>> e : _entrySet) { | ||
236 | { | ||
237 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); | ||
238 | final Procedure1<VLSFofFormula> _function_4 = (VLSFofFormula it) -> { | ||
239 | it.setName(this.support.toIDMultiple("containment_contained", e.getKey().getConstant().toString())); | ||
240 | it.setFofRole("axiom"); | ||
241 | VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); | ||
242 | final Procedure1<VLSUniversalQuantifier> _function_5 = (VLSUniversalQuantifier it_1) -> { | ||
243 | EList<VLSTffTerm> _variables = it_1.getVariables(); | ||
244 | VLSVariable _duplicate = this.support.duplicate(varA); | ||
245 | _variables.add(_duplicate); | ||
246 | VLSImplies _createVLSImplies = this.factory.createVLSImplies(); | ||
247 | final Procedure1<VLSImplies> _function_6 = (VLSImplies it_2) -> { | ||
248 | it_2.setLeft(this.support.duplicate(e.getKey(), varA)); | ||
249 | VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier(); | ||
250 | final Procedure1<VLSExistentialQuantifier> _function_7 = (VLSExistentialQuantifier it_3) -> { | ||
251 | EList<VLSTffTerm> _variables_1 = it_3.getVariables(); | ||
252 | VLSVariable _duplicate_1 = this.support.duplicate(varB); | ||
253 | _variables_1.add(_duplicate_1); | ||
254 | int _length_1 = ((Object[])Conversions.unwrapArray(e.getValue(), Object.class)).length; | ||
255 | boolean _greaterThan_1 = (_length_1 > 1); | ||
256 | if (_greaterThan_1) { | ||
257 | it_3.setOperand(this.makeUnique(e.getValue())); | ||
258 | } else { | ||
259 | it_3.setOperand(e.getValue().get(0)); | ||
260 | } | ||
261 | }; | ||
262 | VLSExistentialQuantifier _doubleArrow = ObjectExtensions.<VLSExistentialQuantifier>operator_doubleArrow(_createVLSExistentialQuantifier, _function_7); | ||
263 | it_2.setRight(_doubleArrow); | ||
264 | }; | ||
265 | VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_6); | ||
266 | it_1.setOperand(_doubleArrow); | ||
267 | }; | ||
268 | VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_5); | ||
269 | it.setFofFormula(_doubleArrow); | ||
270 | }; | ||
271 | final VLSFofFormula relFormula = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_4); | ||
272 | EList<VLSFofFormula> _formulas_1 = trace.specification.getFormulas(); | ||
273 | _formulas_1.add(relFormula); | ||
274 | } | ||
275 | } | ||
276 | final ArrayList<VLSVariable> variables = CollectionLiterals.<VLSVariable>newArrayList(); | ||
277 | final ArrayList<VLSFunction> disjunctionList = CollectionLiterals.<VLSFunction>newArrayList(); | ||
278 | final ArrayList<VLSTerm> conjunctionList = CollectionLiterals.<VLSTerm>newArrayList(); | ||
279 | for (int i = 1; (i <= config.contCycleLevel); i++) { | ||
280 | { | ||
281 | final int ind = i; | ||
282 | VLSVariable _createVLSVariable_3 = this.factory.createVLSVariable(); | ||
283 | final Procedure1<VLSVariable> _function_4 = (VLSVariable it) -> { | ||
284 | String _string = Integer.toString(ind); | ||
285 | String _plus = ("V" + _string); | ||
286 | it.setName(_plus); | ||
287 | }; | ||
288 | VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_3, _function_4); | ||
289 | variables.add(_doubleArrow); | ||
290 | for (int j = 0; (j < i); j++) { | ||
291 | { | ||
292 | for (final Relation l_3 : relationsList) { | ||
293 | { | ||
294 | final VLSFunction rel = this.support.duplicate(CollectionsUtil.<RelationDeclaration, VLSFunction>lookup(((RelationDeclaration) l_3), trace.rel2Predicate), | ||
295 | CollectionLiterals.<VLSVariable>newArrayList(variables.get(j), variables.get(((j + 1) % i)))); | ||
296 | disjunctionList.add(rel); | ||
297 | } | ||
298 | } | ||
299 | conjunctionList.add(this.support.unfoldOr(disjunctionList)); | ||
300 | disjunctionList.clear(); | ||
301 | } | ||
302 | } | ||
303 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); | ||
304 | final Procedure1<VLSFofFormula> _function_5 = (VLSFofFormula it) -> { | ||
305 | it.setName(this.support.toIDMultiple("containment_noCycle", Integer.toString(ind))); | ||
306 | it.setFofRole("axiom"); | ||
307 | VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); | ||
308 | final Procedure1<VLSUnaryNegation> _function_6 = (VLSUnaryNegation it_1) -> { | ||
309 | VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier(); | ||
310 | final Procedure1<VLSExistentialQuantifier> _function_7 = (VLSExistentialQuantifier it_2) -> { | ||
311 | EList<VLSTffTerm> _variables = it_2.getVariables(); | ||
312 | List<VLSVariable> _duplicate = this.support.duplicate(variables); | ||
313 | Iterables.<VLSTffTerm>addAll(_variables, _duplicate); | ||
314 | it_2.setOperand(this.support.unfoldAnd(conjunctionList)); | ||
315 | }; | ||
316 | VLSExistentialQuantifier _doubleArrow_1 = ObjectExtensions.<VLSExistentialQuantifier>operator_doubleArrow(_createVLSExistentialQuantifier, _function_7); | ||
317 | it_1.setOperand(_doubleArrow_1); | ||
318 | }; | ||
319 | VLSUnaryNegation _doubleArrow_1 = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_6); | ||
320 | it.setFofFormula(_doubleArrow_1); | ||
321 | }; | ||
322 | final VLSFofFormula contCycleForm = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_5); | ||
323 | EList<VLSFofFormula> _formulas_1 = trace.specification.getFormulas(); | ||
324 | _formulas_1.add(contCycleForm); | ||
325 | conjunctionList.clear(); | ||
326 | } | ||
327 | } | ||
328 | } | ||
329 | |||
330 | protected VLSTerm makeUnique(final List<VLSFunction> list) { | ||
331 | final List<VLSTerm> possibleNots = CollectionLiterals.<VLSTerm>newArrayList(); | ||
332 | final List<VLSTerm> uniqueRels = CollectionLiterals.<VLSTerm>newArrayList(); | ||
333 | for (final VLSFunction t1 : list) { | ||
334 | { | ||
335 | for (final VLSFunction t2 : list) { | ||
336 | boolean _equals = Objects.equal(t1, t2); | ||
337 | if (_equals) { | ||
338 | final VLSFunction fct = this.support.duplicate(t2); | ||
339 | possibleNots.add(fct); | ||
340 | } else { | ||
341 | final VLSFunction op = this.support.duplicate(t2); | ||
342 | VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); | ||
343 | final Procedure1<VLSUnaryNegation> _function = (VLSUnaryNegation it) -> { | ||
344 | it.setOperand(op); | ||
345 | }; | ||
346 | final VLSUnaryNegation negFct = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function); | ||
347 | possibleNots.add(negFct); | ||
348 | } | ||
349 | } | ||
350 | uniqueRels.add(this.support.unfoldAnd(possibleNots)); | ||
351 | possibleNots.clear(); | ||
352 | } | ||
353 | } | ||
354 | return this.support.unfoldOr(uniqueRels); | ||
355 | } | ||
356 | |||
357 | protected Object addToMap(final Map<VLSFunction, List<VLSFunction>> type2cont, final VLSFunction toFunc, final VLSFunction rel) { | ||
358 | Object _xblockexpression = null; | ||
359 | { | ||
360 | boolean keyInMap = false; | ||
361 | VLSFunction existingKey = this.factory.createVLSFunction(); | ||
362 | Set<VLSFunction> _keySet = type2cont.keySet(); | ||
363 | for (final VLSFunction k : _keySet) { | ||
364 | boolean _equals = k.getConstant().equals(toFunc.getConstant()); | ||
365 | if (_equals) { | ||
366 | keyInMap = true; | ||
367 | existingKey = k; | ||
368 | } | ||
369 | } | ||
370 | Object _xifexpression = null; | ||
371 | if ((!keyInMap)) { | ||
372 | _xifexpression = type2cont.put(toFunc, CollectionLiterals.<VLSFunction>newArrayList(rel)); | ||
373 | } else { | ||
374 | boolean _xifexpression_1 = false; | ||
375 | boolean _contains = type2cont.get(existingKey).contains(rel); | ||
376 | boolean _not = (!_contains); | ||
377 | if (_not) { | ||
378 | _xifexpression_1 = type2cont.get(existingKey).add(rel); | ||
379 | } | ||
380 | _xifexpression = Boolean.valueOf(_xifexpression_1); | ||
381 | } | ||
382 | _xblockexpression = _xifexpression; | ||
383 | } | ||
384 | return _xblockexpression; | ||
385 | } | ||
386 | } | ||