aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java
diff options
context:
space:
mode:
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java')
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java302
1 files changed, 0 insertions, 302 deletions
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
deleted file mode 100644
index d6c90484..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java
+++ /dev/null
@@ -1,302 +0,0 @@
1package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder;
2
3import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration;
4import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper;
5import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace;
6import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support;
7import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSAnd;
8import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant;
9import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality;
10import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula;
11import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction;
12import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies;
13import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm;
14import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTffTerm;
15import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier;
16import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable;
17import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory;
18import com.google.common.base.Objects;
19import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement;
20import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type;
21import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition;
22import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil;
23import java.util.ArrayList;
24import java.util.HashMap;
25import java.util.List;
26import java.util.Map;
27import java.util.Set;
28import org.eclipse.emf.common.util.EList;
29import org.eclipse.xtext.xbase.lib.CollectionLiterals;
30import org.eclipse.xtext.xbase.lib.Conversions;
31import org.eclipse.xtext.xbase.lib.Extension;
32import org.eclipse.xtext.xbase.lib.Functions.Function1;
33import org.eclipse.xtext.xbase.lib.IterableExtensions;
34import org.eclipse.xtext.xbase.lib.ListExtensions;
35import org.eclipse.xtext.xbase.lib.ObjectExtensions;
36import org.eclipse.xtext.xbase.lib.Procedures.Procedure1;
37
38@SuppressWarnings("all")
39public class Logic2VampireLanguageMapper_ScopeMapper {
40 @Extension
41 private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE;
42
43 private final Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support();
44
45 private final Logic2VampireLanguageMapper base;
46
47 private final VLSVariable variable = ObjectExtensions.<VLSVariable>operator_doubleArrow(this.factory.createVLSVariable(), ((Procedure1<VLSVariable>) (VLSVariable it) -> {
48 it.setName("A");
49 }));
50
51 public Logic2VampireLanguageMapper_ScopeMapper(final Logic2VampireLanguageMapper base) {
52 this.base = base;
53 }
54
55 public void _transformScope(final List<Type> types, final VampireSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) {
56 int elemsInIM = trace.definedElement2String.size();
57 final int ABSOLUTE_MIN = 0;
58 final int ABSOLUTE_MAX = (Integer.MAX_VALUE - elemsInIM);
59 final int GLOBAL_MIN = (config.typeScopes.minNewElements - elemsInIM);
60 final int GLOBAL_MAX = (config.typeScopes.maxNewElements - elemsInIM);
61 final ArrayList<VLSConstant> localInstances = CollectionLiterals.<VLSConstant>newArrayList();
62 final boolean consistant = (GLOBAL_MAX >= GLOBAL_MIN);
63 if ((GLOBAL_MIN != ABSOLUTE_MIN)) {
64 this.getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, (!consistant));
65 if (consistant) {
66 for (final VLSConstant i : trace.uniqueInstances) {
67 localInstances.add(this.support.duplicate(i));
68 }
69 this.makeFofFormula(localInstances, trace, true, null);
70 } else {
71 this.makeFofFormula(((ArrayList) trace.uniqueInstances), trace, true, null);
72 }
73 }
74 if ((GLOBAL_MAX != ABSOLUTE_MAX)) {
75 this.getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, consistant);
76 if (consistant) {
77 this.makeFofFormula(((ArrayList) trace.uniqueInstances), trace, false, null);
78 } else {
79 this.makeFofFormula(localInstances, trace, false, null);
80 }
81 }
82 int i_1 = 1;
83 if ((((Boolean) trace.topLvlElementIsInInitialModel)).booleanValue()) {
84 i_1 = 0;
85 }
86 int minNum = (-1);
87 Map<Type, Integer> startPoints = new HashMap<Type, Integer>();
88 final Function1<Type, Boolean> _function = (Type it) -> {
89 boolean _equals = it.equals(trace.topLevelType);
90 return Boolean.valueOf((!_equals));
91 };
92 Iterable<Type> _filter = IterableExtensions.<Type>filter(config.typeScopes.minNewElementsByType.keySet(), _function);
93 for (final Type t : _filter) {
94 {
95 int numIniIntModel = 0;
96 Set<DefinedElement> _keySet = trace.definedElement2String.keySet();
97 for (final DefinedElement elem : _keySet) {
98 EList<TypeDefinition> _definedInType = elem.getDefinedInType();
99 for (final TypeDefinition tDefined : _definedInType) {
100 boolean _dfsSubtypeCheck = this.support.dfsSubtypeCheck(t, tDefined);
101 if (_dfsSubtypeCheck) {
102 int _numIniIntModel = numIniIntModel;
103 numIniIntModel = (_numIniIntModel + 1);
104 }
105 }
106 }
107 Integer _lookup = CollectionsUtil.<Type, Integer>lookup(t, config.typeScopes.minNewElementsByType);
108 int _minus = ((_lookup).intValue() - numIniIntModel);
109 minNum = _minus;
110 if ((minNum != 0)) {
111 this.getInstanceConstants((i_1 + minNum), i_1, localInstances, trace, true, false);
112 startPoints.put(t, Integer.valueOf(i_1));
113 int _i = i_1;
114 i_1 = (_i + minNum);
115 this.makeFofFormula(localInstances, trace, true, t);
116 }
117 }
118 }
119 final Function1<Type, Boolean> _function_1 = (Type it) -> {
120 boolean _equals = it.equals(trace.topLevelType);
121 return Boolean.valueOf((!_equals));
122 };
123 Iterable<Type> _filter_1 = IterableExtensions.<Type>filter(config.typeScopes.maxNewElementsByType.keySet(), _function_1);
124 for (final Type t_1 : _filter_1) {
125 {
126 int numIniIntModel = 0;
127 Set<DefinedElement> _keySet = trace.definedElement2String.keySet();
128 for (final DefinedElement elem : _keySet) {
129 EList<TypeDefinition> _definedInType = elem.getDefinedInType();
130 boolean _equals = Objects.equal(_definedInType, t_1);
131 if (_equals) {
132 int _numIniIntModel = numIniIntModel;
133 numIniIntModel = (_numIniIntModel + 1);
134 }
135 }
136 Integer _lookup = CollectionsUtil.<Type, Integer>lookup(t_1, config.typeScopes.maxNewElementsByType);
137 int maxNum = ((_lookup).intValue() - numIniIntModel);
138 boolean _contains = config.typeScopes.minNewElementsByType.keySet().contains(t_1);
139 if (_contains) {
140 Integer _lookup_1 = CollectionsUtil.<Type, Integer>lookup(t_1, config.typeScopes.minNewElementsByType);
141 int _minus = ((_lookup_1).intValue() - numIniIntModel);
142 minNum = _minus;
143 } else {
144 minNum = 0;
145 }
146 if ((minNum != 0)) {
147 Integer startpoint = CollectionsUtil.<Type, Integer>lookup(t_1, startPoints);
148 this.getInstanceConstants(((startpoint).intValue() + minNum), (startpoint).intValue(), localInstances, trace, true, false);
149 } else {
150 localInstances.clear();
151 }
152 int instEndInd = Math.min(GLOBAL_MAX, ((i_1 + maxNum) - minNum));
153 this.getInstanceConstants(instEndInd, i_1, localInstances, trace, false, false);
154 this.makeFofFormula(localInstances, trace, false, t_1);
155 }
156 }
157 final boolean DUPLICATES = config.uniquenessDuplicates;
158 final int numInst = ((Object[])Conversions.unwrapArray(trace.uniqueInstances, Object.class)).length;
159 int ind = 1;
160 if ((numInst != 0)) {
161 if (DUPLICATES) {
162 for (final VLSConstant e : trace.uniqueInstances) {
163 {
164 final int x = ind;
165 VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();
166 final Procedure1<VLSFofFormula> _function_2 = (VLSFofFormula it) -> {
167 it.setName(this.support.toIDMultiple("t_uniqueness", e.getName()));
168 it.setFofRole("axiom");
169 it.setFofFormula(this.support.establishUniqueness(trace.uniqueInstances, e));
170 };
171 final VLSFofFormula uniqueness = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_2);
172 EList<VLSFofFormula> _formulas = trace.specification.getFormulas();
173 _formulas.add(uniqueness);
174 ind++;
175 }
176 }
177 } else {
178 List<VLSConstant> _subList = trace.uniqueInstances.subList(0, (numInst - 1));
179 for (final VLSConstant e_1 : _subList) {
180 {
181 final int x = ind;
182 VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();
183 final Procedure1<VLSFofFormula> _function_2 = (VLSFofFormula it) -> {
184 it.setName(this.support.toIDMultiple("t_uniqueness", e_1.getName()));
185 it.setFofRole("axiom");
186 it.setFofFormula(this.support.establishUniqueness(trace.uniqueInstances.subList(x, numInst), e_1));
187 };
188 final VLSFofFormula uniqueness = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_2);
189 EList<VLSFofFormula> _formulas = trace.specification.getFormulas();
190 _formulas.add(uniqueness);
191 ind++;
192 }
193 }
194 }
195 }
196 }
197
198 protected void getInstanceConstants(final int endInd, final int startInd, final ArrayList list, final Logic2VampireLanguageMapperTrace trace, final boolean clear, final boolean addToTrace) {
199 if (clear) {
200 list.clear();
201 }
202 for (int i = startInd; (i < endInd); i++) {
203 {
204 final int num = (i + 1);
205 VLSConstant _createVLSConstant = this.factory.createVLSConstant();
206 final Procedure1<VLSConstant> _function = (VLSConstant it) -> {
207 it.setName(("o" + Integer.valueOf(num)));
208 };
209 final VLSConstant cst = ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _function);
210 if (addToTrace) {
211 trace.uniqueInstances.add(cst);
212 }
213 list.add(cst);
214 }
215 }
216 }
217
218 protected void makeFofFormula(final ArrayList list, final Logic2VampireLanguageMapperTrace trace, final boolean minimum, final Type type) {
219 String nm = "";
220 VLSTerm tm = null;
221 if ((type == null)) {
222 nm = "object";
223 tm = this.support.topLevelTypeFunc();
224 } else {
225 nm = CollectionsUtil.<Type, VLSFunction>lookup(type, trace.type2Predicate).getConstant().toString();
226 VLSAnd _createVLSAnd = this.factory.createVLSAnd();
227 final Procedure1<VLSAnd> _function = (VLSAnd it) -> {
228 it.setLeft(this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(type, trace.type2Predicate)));
229 it.setRight(this.support.topLevelTypeFunc());
230 };
231 VLSAnd _doubleArrow = ObjectExtensions.<VLSAnd>operator_doubleArrow(_createVLSAnd, _function);
232 tm = _doubleArrow;
233 }
234 final String name = nm;
235 final VLSTerm term = tm;
236 VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();
237 final Procedure1<VLSFofFormula> _function_1 = (VLSFofFormula it) -> {
238 String _xifexpression = null;
239 if (minimum) {
240 _xifexpression = "min";
241 } else {
242 _xifexpression = "max";
243 }
244 it.setName(this.support.toIDMultiple("typeScope", _xifexpression, name));
245 it.setFofRole("axiom");
246 VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();
247 final Procedure1<VLSUniversalQuantifier> _function_2 = (VLSUniversalQuantifier it_1) -> {
248 EList<VLSTffTerm> _variables = it_1.getVariables();
249 VLSVariable _duplicate = this.support.duplicate(this.variable);
250 _variables.add(_duplicate);
251 VLSImplies _createVLSImplies = this.factory.createVLSImplies();
252 final Procedure1<VLSImplies> _function_3 = (VLSImplies it_2) -> {
253 if (minimum) {
254 final Function1<VLSTerm, VLSEquality> _function_4 = (VLSTerm i) -> {
255 VLSEquality _createVLSEquality = this.factory.createVLSEquality();
256 final Procedure1<VLSEquality> _function_5 = (VLSEquality it_3) -> {
257 VLSVariable _createVLSVariable = this.factory.createVLSVariable();
258 final Procedure1<VLSVariable> _function_6 = (VLSVariable it_4) -> {
259 it_4.setName(this.variable.getName());
260 };
261 VLSVariable _doubleArrow_1 = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_6);
262 it_3.setLeft(_doubleArrow_1);
263 it_3.setRight(i);
264 };
265 return ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_5);
266 };
267 it_2.setLeft(this.support.unfoldOr(ListExtensions.<VLSTerm, VLSEquality>map(list, _function_4)));
268 it_2.setRight(term);
269 } else {
270 it_2.setLeft(term);
271 final Function1<VLSTerm, VLSEquality> _function_5 = (VLSTerm i) -> {
272 VLSEquality _createVLSEquality = this.factory.createVLSEquality();
273 final Procedure1<VLSEquality> _function_6 = (VLSEquality it_3) -> {
274 VLSVariable _createVLSVariable = this.factory.createVLSVariable();
275 final Procedure1<VLSVariable> _function_7 = (VLSVariable it_4) -> {
276 it_4.setName(this.variable.getName());
277 };
278 VLSVariable _doubleArrow_1 = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_7);
279 it_3.setLeft(_doubleArrow_1);
280 it_3.setRight(i);
281 };
282 return ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_6);
283 };
284 it_2.setRight(this.support.unfoldOr(ListExtensions.<VLSTerm, VLSEquality>map(list, _function_5)));
285 }
286 };
287 VLSImplies _doubleArrow_1 = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_3);
288 it_1.setOperand(_doubleArrow_1);
289 };
290 VLSUniversalQuantifier _doubleArrow_1 = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_2);
291 it.setFofFormula(_doubleArrow_1);
292 };
293 final VLSFofFormula cstDec = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_1);
294 EList<VLSFofFormula> _formulas = trace.specification.getFormulas();
295 _formulas.add(cstDec);
296 }
297
298 public void transformScope(final List<Type> types, final VampireSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) {
299 _transformScope(types, config, trace);
300 return;
301 }
302}
generated by cgit v1.2.3-54-g00ecf (git 2.45.0) at 2024-05-05 11:40:18 +0000