aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.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_TypeMapper_FilteredTypes.java')
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.java287
1 files changed, 287 insertions, 0 deletions
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.java
new file mode 100644
index 00000000..38ff37cd
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.java
@@ -0,0 +1,287 @@
1package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder;
2
3import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper;
4import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace;
5import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support;
6import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapper;
7import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes;
8import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireModelInterpretation_TypeInterpretation;
9import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSDoubleQuote;
10import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality;
11import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent;
12import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula;
13import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction;
14import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm;
15import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUnaryNegation;
16import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier;
17import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable;
18import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory;
19import com.google.common.base.Objects;
20import com.google.common.collect.Iterables;
21import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement;
22import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type;
23import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition;
24import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage;
25import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil;
26import java.util.ArrayList;
27import java.util.Collection;
28import java.util.List;
29import org.eclipse.emf.common.util.EList;
30import org.eclipse.xtext.xbase.lib.Extension;
31import org.eclipse.xtext.xbase.lib.Functions.Function1;
32import org.eclipse.xtext.xbase.lib.IterableExtensions;
33import org.eclipse.xtext.xbase.lib.ListExtensions;
34import org.eclipse.xtext.xbase.lib.ObjectExtensions;
35import org.eclipse.xtext.xbase.lib.Procedures.Procedure1;
36
37@SuppressWarnings("all")
38public class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2VampireLanguageMapper_TypeMapper {
39 private final Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support();
40
41 @Extension
42 private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE;
43
44 public Logic2VampireLanguageMapper_TypeMapper_FilteredTypes() {
45 LogicproblemPackage.eINSTANCE.getClass();
46 }
47
48 @Override
49 public void transformTypes(final Collection<Type> types, final Collection<DefinedElement> elements, final Logic2VampireLanguageMapper mapper, final Logic2VampireLanguageMapperTrace trace) {
50 final Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes typeTrace = new Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes();
51 trace.typeMapperTrace = typeTrace;
52 VLSVariable _createVLSVariable = this.factory.createVLSVariable();
53 final Procedure1<VLSVariable> _function = (VLSVariable it) -> {
54 it.setName("A");
55 };
56 final VLSVariable variable = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function);
57 for (final Type type : types) {
58 {
59 VLSFunction _createVLSFunction = this.factory.createVLSFunction();
60 final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> {
61 it.setConstant(this.support.toIDMultiple("type", type.getName()));
62 EList<VLSTerm> _terms = it.getTerms();
63 VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable();
64 final Procedure1<VLSVariable> _function_2 = (VLSVariable it_1) -> {
65 it_1.setName(variable.getName());
66 };
67 VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_2);
68 _terms.add(_doubleArrow);
69 };
70 final VLSFunction typePred = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_1);
71 typeTrace.type2Predicate.put(type, typePred);
72 }
73 }
74 Iterable<TypeDefinition> _filter = Iterables.<TypeDefinition>filter(types, TypeDefinition.class);
75 for (final TypeDefinition type_1 : _filter) {
76 {
77 VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();
78 final Procedure1<VLSFofFormula> _function_1 = (VLSFofFormula it) -> {
79 it.setName(this.support.toIDMultiple("typeDef", type_1.getName()));
80 it.setFofRole("axiom");
81 VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();
82 final Procedure1<VLSUniversalQuantifier> _function_2 = (VLSUniversalQuantifier it_1) -> {
83 EList<VLSVariable> _variables = it_1.getVariables();
84 VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable();
85 final Procedure1<VLSVariable> _function_3 = (VLSVariable it_2) -> {
86 it_2.setName(variable.getName());
87 };
88 VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_3);
89 _variables.add(_doubleArrow);
90 VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent();
91 final Procedure1<VLSEquivalent> _function_4 = (VLSEquivalent it_2) -> {
92 VLSFunction _createVLSFunction = this.factory.createVLSFunction();
93 final Procedure1<VLSFunction> _function_5 = (VLSFunction it_3) -> {
94 it_3.setConstant(CollectionsUtil.<TypeDefinition, VLSFunction>lookup(type_1, typeTrace.type2Predicate).getConstant());
95 EList<VLSTerm> _terms = it_3.getTerms();
96 VLSVariable _createVLSVariable_2 = this.factory.createVLSVariable();
97 final Procedure1<VLSVariable> _function_6 = (VLSVariable it_4) -> {
98 it_4.setName("A");
99 };
100 VLSVariable _doubleArrow_1 = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_2, _function_6);
101 _terms.add(_doubleArrow_1);
102 };
103 VLSFunction _doubleArrow_1 = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_5);
104 it_2.setLeft(_doubleArrow_1);
105 CollectionsUtil.<TypeDefinition, VLSFunction>lookup(type_1, typeTrace.type2Predicate);
106 final Function1<DefinedElement, VLSEquality> _function_6 = (DefinedElement e) -> {
107 VLSEquality _createVLSEquality = this.factory.createVLSEquality();
108 final Procedure1<VLSEquality> _function_7 = (VLSEquality it_3) -> {
109 VLSVariable _createVLSVariable_2 = this.factory.createVLSVariable();
110 final Procedure1<VLSVariable> _function_8 = (VLSVariable it_4) -> {
111 it_4.setName(variable.getName());
112 };
113 VLSVariable _doubleArrow_2 = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_2, _function_8);
114 it_3.setLeft(_doubleArrow_2);
115 VLSDoubleQuote _createVLSDoubleQuote = this.factory.createVLSDoubleQuote();
116 final Procedure1<VLSDoubleQuote> _function_9 = (VLSDoubleQuote it_4) -> {
117 String _name = e.getName();
118 String _plus = ("\"a" + _name);
119 String _plus_1 = (_plus + "\"");
120 it_4.setValue(_plus_1);
121 };
122 VLSDoubleQuote _doubleArrow_3 = ObjectExtensions.<VLSDoubleQuote>operator_doubleArrow(_createVLSDoubleQuote, _function_9);
123 it_3.setRight(_doubleArrow_3);
124 };
125 return ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_7);
126 };
127 it_2.setRight(this.support.unfoldOr(ListExtensions.<DefinedElement, VLSEquality>map(type_1.getElements(), _function_6)));
128 };
129 VLSEquivalent _doubleArrow_1 = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_4);
130 it_1.setOperand(_doubleArrow_1);
131 };
132 VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_2);
133 it.setFofFormula(_doubleArrow);
134 };
135 final VLSFofFormula res = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_1);
136 EList<VLSFofFormula> _formulas = trace.specification.getFormulas();
137 _formulas.add(res);
138 }
139 }
140 final Function1<Type, Boolean> _function_1 = (Type it) -> {
141 boolean _isIsAbstract = it.isIsAbstract();
142 return Boolean.valueOf((!_isIsAbstract));
143 };
144 Iterable<Type> _filter_1 = IterableExtensions.<Type>filter(types, _function_1);
145 for (final Type type_2 : _filter_1) {
146 {
147 for (final Type type2 : types) {
148 if ((Objects.equal(type_2, type2) || this.dfsSupertypeCheck(type_2, type2))) {
149 VLSFunction _createVLSFunction = this.factory.createVLSFunction();
150 final Procedure1<VLSFunction> _function_2 = (VLSFunction it) -> {
151 it.setConstant(CollectionsUtil.<Type, VLSFunction>lookup(type2, typeTrace.type2Predicate).getConstant());
152 EList<VLSTerm> _terms = it.getTerms();
153 VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable();
154 final Procedure1<VLSVariable> _function_3 = (VLSVariable it_1) -> {
155 it_1.setName("A");
156 };
157 VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_3);
158 _terms.add(_doubleArrow);
159 };
160 VLSFunction _doubleArrow = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_2);
161 typeTrace.type2PossibleNot.put(type2, _doubleArrow);
162 } else {
163 VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation();
164 final Procedure1<VLSUnaryNegation> _function_3 = (VLSUnaryNegation it) -> {
165 VLSFunction _createVLSFunction_1 = this.factory.createVLSFunction();
166 final Procedure1<VLSFunction> _function_4 = (VLSFunction it_1) -> {
167 it_1.setConstant(CollectionsUtil.<Type, VLSFunction>lookup(type2, typeTrace.type2Predicate).getConstant());
168 EList<VLSTerm> _terms = it_1.getTerms();
169 VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable();
170 final Procedure1<VLSVariable> _function_5 = (VLSVariable it_2) -> {
171 it_2.setName("A");
172 };
173 VLSVariable _doubleArrow_1 = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_5);
174 _terms.add(_doubleArrow_1);
175 };
176 VLSFunction _doubleArrow_1 = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction_1, _function_4);
177 it.setOperand(_doubleArrow_1);
178 };
179 VLSUnaryNegation _doubleArrow_1 = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_3);
180 typeTrace.type2PossibleNot.put(type2, _doubleArrow_1);
181 }
182 }
183 Collection<VLSTerm> _values = typeTrace.type2PossibleNot.values();
184 ArrayList<VLSTerm> _arrayList = new ArrayList<VLSTerm>(_values);
185 typeTrace.type2And.put(type_2, this.support.unfoldAnd(_arrayList));
186 typeTrace.type2PossibleNot.clear();
187 }
188 }
189 VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();
190 final Procedure1<VLSFofFormula> _function_2 = (VLSFofFormula it) -> {
191 it.setName("hierarchyHandler");
192 it.setFofRole("axiom");
193 VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();
194 final Procedure1<VLSUniversalQuantifier> _function_3 = (VLSUniversalQuantifier it_1) -> {
195 EList<VLSVariable> _variables = it_1.getVariables();
196 VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable();
197 final Procedure1<VLSVariable> _function_4 = (VLSVariable it_2) -> {
198 it_2.setName("A");
199 };
200 VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_4);
201 _variables.add(_doubleArrow);
202 VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent();
203 final Procedure1<VLSEquivalent> _function_5 = (VLSEquivalent it_2) -> {
204 VLSFunction _createVLSFunction = this.factory.createVLSFunction();
205 final Procedure1<VLSFunction> _function_6 = (VLSFunction it_3) -> {
206 it_3.setConstant("Object");
207 EList<VLSTerm> _terms = it_3.getTerms();
208 VLSVariable _createVLSVariable_2 = this.factory.createVLSVariable();
209 final Procedure1<VLSVariable> _function_7 = (VLSVariable it_4) -> {
210 it_4.setName("A");
211 };
212 VLSVariable _doubleArrow_1 = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_2, _function_7);
213 _terms.add(_doubleArrow_1);
214 };
215 VLSFunction _doubleArrow_1 = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_6);
216 it_2.setLeft(_doubleArrow_1);
217 Collection<VLSTerm> _values = typeTrace.type2And.values();
218 ArrayList<VLSTerm> _arrayList = new ArrayList<VLSTerm>(_values);
219 it_2.setRight(this.support.unfoldOr(_arrayList));
220 };
221 VLSEquivalent _doubleArrow_1 = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_5);
222 it_1.setOperand(_doubleArrow_1);
223 };
224 VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_3);
225 it.setFofFormula(_doubleArrow);
226 };
227 final VLSFofFormula hierarch = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_2);
228 EList<VLSFofFormula> _formulas = trace.specification.getFormulas();
229 _formulas.add(hierarch);
230 }
231
232 public boolean dfsSupertypeCheck(final Type type, final Type type2) {
233 boolean _xifexpression = false;
234 boolean _isEmpty = type.getSupertypes().isEmpty();
235 if (_isEmpty) {
236 return false;
237 } else {
238 boolean _xifexpression_1 = false;
239 boolean _contains = type.getSupertypes().contains(type2);
240 if (_contains) {
241 return true;
242 } else {
243 EList<Type> _supertypes = type.getSupertypes();
244 for (final Type supertype : _supertypes) {
245 boolean _dfsSupertypeCheck = this.dfsSupertypeCheck(supertype, type2);
246 if (_dfsSupertypeCheck) {
247 return true;
248 }
249 }
250 }
251 _xifexpression = _xifexpression_1;
252 }
253 return _xifexpression;
254 }
255
256 @Override
257 public List<VLSTerm> transformTypeReference(final Type referred, final Logic2VampireLanguageMapper mapper, final Logic2VampireLanguageMapperTrace trace) {
258 throw new UnsupportedOperationException("TODO: auto-generated method stub");
259 }
260
261 @Override
262 public VLSTerm getUndefinedSupertype(final Logic2VampireLanguageMapperTrace trace) {
263 throw new UnsupportedOperationException("TODO: auto-generated method stub");
264 }
265
266 @Override
267 public int getUndefinedSupertypeScope(final int undefinedScope, final Logic2VampireLanguageMapperTrace trace) {
268 throw new UnsupportedOperationException("TODO: auto-generated method stub");
269 }
270
271 @Override
272 public VLSTerm transformReference(final DefinedElement referred, final Logic2VampireLanguageMapperTrace trace) {
273 VLSDoubleQuote _createVLSDoubleQuote = this.factory.createVLSDoubleQuote();
274 final Procedure1<VLSDoubleQuote> _function = (VLSDoubleQuote it) -> {
275 String _name = referred.getName();
276 String _plus = ("\"a" + _name);
277 String _plus_1 = (_plus + "\"");
278 it.setValue(_plus_1);
279 };
280 return ObjectExtensions.<VLSDoubleQuote>operator_doubleArrow(_createVLSDoubleQuote, _function);
281 }
282
283 @Override
284 public VampireModelInterpretation_TypeInterpretation getTypeInterpreter() {
285 throw new UnsupportedOperationException("TODO: auto-generated method stub");
286 }
287}
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-06-17 18:58:41 +0000