aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.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_RelationMapper.java')
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java296
1 files changed, 296 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_RelationMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java
new file mode 100644
index 00000000..561402a7
--- /dev/null
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java
@@ -0,0 +1,296 @@
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.vampireLanguage.VLSEquivalent;
7import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula;
8import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction;
9import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies;
10import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm;
11import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier;
12import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable;
13import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory;
14import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference;
15import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation;
16import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration;
17import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition;
18import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference;
19import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable;
20import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil;
21import java.util.ArrayList;
22import java.util.Arrays;
23import java.util.Collection;
24import java.util.HashMap;
25import java.util.List;
26import java.util.Map;
27import org.eclipse.emf.common.util.EList;
28import org.eclipse.xtext.xbase.lib.Conversions;
29import org.eclipse.xtext.xbase.lib.ExclusiveRange;
30import org.eclipse.xtext.xbase.lib.Extension;
31import org.eclipse.xtext.xbase.lib.ObjectExtensions;
32import org.eclipse.xtext.xbase.lib.Procedures.Procedure1;
33
34@SuppressWarnings("all")
35public class Logic2VampireLanguageMapper_RelationMapper {
36 @Extension
37 private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE;
38
39 private final Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support();
40
41 private final Logic2VampireLanguageMapper base;
42
43 public Logic2VampireLanguageMapper_RelationMapper(final Logic2VampireLanguageMapper base) {
44 this.base = base;
45 }
46
47 public void _transformRelation(final RelationDefinition r, final Logic2VampireLanguageMapperTrace trace) {
48 final Map<Variable, VLSVariable> relationVar2VLS = new HashMap<Variable, VLSVariable>();
49 final Map<Variable, VLSFunction> relationVar2TypeDecComply = new HashMap<Variable, VLSFunction>();
50 final Map<Variable, VLSFunction> relationVar2TypeDecRes = new HashMap<Variable, VLSFunction>();
51 final ArrayList<VLSTerm> typedefs = new ArrayList<VLSTerm>();
52 EList<Variable> _variables = r.getVariables();
53 for (final Variable variable : _variables) {
54 {
55 VLSVariable _createVLSVariable = this.factory.createVLSVariable();
56 final Procedure1<VLSVariable> _function = (VLSVariable it) -> {
57 it.setName(this.support.toIDMultiple("Var", variable.getName()));
58 };
59 final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function);
60 relationVar2VLS.put(variable, v);
61 VLSFunction _createVLSFunction = this.factory.createVLSFunction();
62 final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> {
63 TypeReference _range = variable.getRange();
64 it.setConstant(this.support.toIDMultiple("type", ((ComplexTypeReference) _range).getReferred().getName()));
65 EList<VLSTerm> _terms = it.getTerms();
66 VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable();
67 final Procedure1<VLSVariable> _function_2 = (VLSVariable it_1) -> {
68 it_1.setName(this.support.toIDMultiple("Var", variable.getName()));
69 };
70 VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_2);
71 _terms.add(_doubleArrow);
72 };
73 final VLSFunction varTypeComply = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_1);
74 relationVar2TypeDecComply.put(variable, varTypeComply);
75 VLSFunction _createVLSFunction_1 = this.factory.createVLSFunction();
76 final Procedure1<VLSFunction> _function_2 = (VLSFunction it) -> {
77 TypeReference _range = variable.getRange();
78 it.setConstant(this.support.toIDMultiple("type", ((ComplexTypeReference) _range).getReferred().getName()));
79 EList<VLSTerm> _terms = it.getTerms();
80 VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable();
81 final Procedure1<VLSVariable> _function_3 = (VLSVariable it_1) -> {
82 it_1.setName(this.support.toIDMultiple("Var", variable.getName()));
83 };
84 VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_3);
85 _terms.add(_doubleArrow);
86 };
87 final VLSFunction varTypeRes = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction_1, _function_2);
88 relationVar2TypeDecRes.put(variable, varTypeRes);
89 }
90 }
91 VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();
92 final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> {
93 it.setName(this.support.toIDMultiple("compliance", r.getName()));
94 it.setFofRole("axiom");
95 VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();
96 final Procedure1<VLSUniversalQuantifier> _function_1 = (VLSUniversalQuantifier it_1) -> {
97 EList<Variable> _variables_1 = r.getVariables();
98 for (final Variable variable_1 : _variables_1) {
99 {
100 VLSVariable _createVLSVariable = this.factory.createVLSVariable();
101 final Procedure1<VLSVariable> _function_2 = (VLSVariable it_2) -> {
102 it_2.setName(CollectionsUtil.<Variable, VLSVariable>lookup(variable_1, relationVar2VLS).getName());
103 };
104 final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_2);
105 EList<VLSVariable> _variables_2 = it_1.getVariables();
106 _variables_2.add(v);
107 }
108 }
109 VLSImplies _createVLSImplies = this.factory.createVLSImplies();
110 final Procedure1<VLSImplies> _function_2 = (VLSImplies it_2) -> {
111 VLSFunction _createVLSFunction = this.factory.createVLSFunction();
112 final Procedure1<VLSFunction> _function_3 = (VLSFunction it_3) -> {
113 it_3.setConstant(this.support.toIDMultiple("rel", r.getName()));
114 EList<Variable> _variables_2 = r.getVariables();
115 for (final Variable variable_2 : _variables_2) {
116 {
117 VLSVariable _createVLSVariable = this.factory.createVLSVariable();
118 final Procedure1<VLSVariable> _function_4 = (VLSVariable it_4) -> {
119 it_4.setName(CollectionsUtil.<Variable, VLSVariable>lookup(variable_2, relationVar2VLS).getName());
120 };
121 final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_4);
122 EList<VLSTerm> _terms = it_3.getTerms();
123 _terms.add(v);
124 }
125 }
126 };
127 VLSFunction _doubleArrow = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_3);
128 it_2.setLeft(_doubleArrow);
129 Collection<VLSFunction> _values = relationVar2TypeDecComply.values();
130 ArrayList<VLSTerm> _arrayList = new ArrayList<VLSTerm>(_values);
131 it_2.setRight(this.support.unfoldAnd(_arrayList));
132 };
133 VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_2);
134 it_1.setOperand(_doubleArrow);
135 };
136 VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_1);
137 it.setFofFormula(_doubleArrow);
138 };
139 final VLSFofFormula comply = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function);
140 VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula();
141 final Procedure1<VLSFofFormula> _function_1 = (VLSFofFormula it) -> {
142 it.setName(this.support.toIDMultiple("relation", r.getName()));
143 it.setFofRole("axiom");
144 VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();
145 final Procedure1<VLSUniversalQuantifier> _function_2 = (VLSUniversalQuantifier it_1) -> {
146 EList<Variable> _variables_1 = r.getVariables();
147 for (final Variable variable_1 : _variables_1) {
148 {
149 VLSVariable _createVLSVariable = this.factory.createVLSVariable();
150 final Procedure1<VLSVariable> _function_3 = (VLSVariable it_2) -> {
151 it_2.setName(CollectionsUtil.<Variable, VLSVariable>lookup(variable_1, relationVar2VLS).getName());
152 };
153 final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_3);
154 EList<VLSVariable> _variables_2 = it_1.getVariables();
155 _variables_2.add(v);
156 }
157 }
158 VLSImplies _createVLSImplies = this.factory.createVLSImplies();
159 final Procedure1<VLSImplies> _function_3 = (VLSImplies it_2) -> {
160 Collection<VLSFunction> _values = relationVar2TypeDecRes.values();
161 ArrayList<VLSTerm> _arrayList = new ArrayList<VLSTerm>(_values);
162 it_2.setLeft(this.support.unfoldAnd(_arrayList));
163 VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent();
164 final Procedure1<VLSEquivalent> _function_4 = (VLSEquivalent it_3) -> {
165 VLSFunction _createVLSFunction = this.factory.createVLSFunction();
166 final Procedure1<VLSFunction> _function_5 = (VLSFunction it_4) -> {
167 it_4.setConstant(this.support.toIDMultiple("rel", r.getName()));
168 EList<Variable> _variables_2 = r.getVariables();
169 for (final Variable variable_2 : _variables_2) {
170 {
171 VLSVariable _createVLSVariable = this.factory.createVLSVariable();
172 final Procedure1<VLSVariable> _function_6 = (VLSVariable it_5) -> {
173 it_5.setName(CollectionsUtil.<Variable, VLSVariable>lookup(variable_2, relationVar2VLS).getName());
174 };
175 final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_6);
176 EList<VLSTerm> _terms = it_4.getTerms();
177 _terms.add(v);
178 }
179 }
180 };
181 VLSFunction _doubleArrow = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_5);
182 it_3.setLeft(_doubleArrow);
183 it_3.setRight(this.base.transformTerm(r.getValue(), trace, relationVar2VLS));
184 };
185 VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_4);
186 it_2.setRight(_doubleArrow);
187 };
188 VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_3);
189 it_1.setOperand(_doubleArrow);
190 };
191 VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_2);
192 it.setFofFormula(_doubleArrow);
193 };
194 final VLSFofFormula res = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_1);
195 EList<VLSFofFormula> _formulas = trace.specification.getFormulas();
196 _formulas.add(comply);
197 EList<VLSFofFormula> _formulas_1 = trace.specification.getFormulas();
198 _formulas_1.add(res);
199 }
200
201 public void _transformRelation(final RelationDeclaration r, final Logic2VampireLanguageMapperTrace trace) {
202 final List<VLSVariable> relationVar2VLS = new ArrayList<VLSVariable>();
203 final List<VLSFunction> relationVar2TypeDecComply = new ArrayList<VLSFunction>();
204 final ArrayList<VLSTerm> typedefs = new ArrayList<VLSTerm>();
205 int _length = ((Object[])Conversions.unwrapArray(r.getParameters(), Object.class)).length;
206 ExclusiveRange _doubleDotLessThan = new ExclusiveRange(0, _length, true);
207 for (final Integer i : _doubleDotLessThan) {
208 {
209 VLSVariable _createVLSVariable = this.factory.createVLSVariable();
210 final Procedure1<VLSVariable> _function = (VLSVariable it) -> {
211 it.setName(this.support.toIDMultiple("Var", i.toString()));
212 };
213 final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function);
214 relationVar2VLS.add(v);
215 VLSFunction _createVLSFunction = this.factory.createVLSFunction();
216 final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> {
217 TypeReference _get = r.getParameters().get((i).intValue());
218 it.setConstant(this.support.toIDMultiple("type", ((ComplexTypeReference) _get).getReferred().getName()));
219 EList<VLSTerm> _terms = it.getTerms();
220 VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable();
221 final Procedure1<VLSVariable> _function_2 = (VLSVariable it_1) -> {
222 it_1.setName(this.support.toIDMultiple("Var", i.toString()));
223 };
224 VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_2);
225 _terms.add(_doubleArrow);
226 };
227 final VLSFunction varTypeComply = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_1);
228 relationVar2TypeDecComply.add(varTypeComply);
229 }
230 }
231 VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();
232 final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> {
233 it.setName(this.support.toIDMultiple("compliance", r.getName()));
234 it.setFofRole("axiom");
235 VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();
236 final Procedure1<VLSUniversalQuantifier> _function_1 = (VLSUniversalQuantifier it_1) -> {
237 int _length_1 = ((Object[])Conversions.unwrapArray(r.getParameters(), Object.class)).length;
238 ExclusiveRange _doubleDotLessThan_1 = new ExclusiveRange(0, _length_1, true);
239 for (final Integer i_1 : _doubleDotLessThan_1) {
240 {
241 VLSVariable _createVLSVariable = this.factory.createVLSVariable();
242 final Procedure1<VLSVariable> _function_2 = (VLSVariable it_2) -> {
243 it_2.setName(relationVar2VLS.get((i_1).intValue()).getName());
244 };
245 final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_2);
246 EList<VLSVariable> _variables = it_1.getVariables();
247 _variables.add(v);
248 }
249 }
250 VLSImplies _createVLSImplies = this.factory.createVLSImplies();
251 final Procedure1<VLSImplies> _function_2 = (VLSImplies it_2) -> {
252 VLSFunction _createVLSFunction = this.factory.createVLSFunction();
253 final Procedure1<VLSFunction> _function_3 = (VLSFunction it_3) -> {
254 it_3.setConstant(this.support.toIDMultiple("rel", r.getName()));
255 int _length_2 = ((Object[])Conversions.unwrapArray(r.getParameters(), Object.class)).length;
256 ExclusiveRange _doubleDotLessThan_2 = new ExclusiveRange(0, _length_2, true);
257 for (final Integer i_2 : _doubleDotLessThan_2) {
258 {
259 VLSVariable _createVLSVariable = this.factory.createVLSVariable();
260 final Procedure1<VLSVariable> _function_4 = (VLSVariable it_4) -> {
261 it_4.setName(relationVar2VLS.get((i_2).intValue()).getName());
262 };
263 final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_4);
264 EList<VLSTerm> _terms = it_3.getTerms();
265 _terms.add(v);
266 }
267 }
268 };
269 VLSFunction _doubleArrow = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_3);
270 it_2.setLeft(_doubleArrow);
271 it_2.setRight(this.support.unfoldAnd(relationVar2TypeDecComply));
272 };
273 VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_2);
274 it_1.setOperand(_doubleArrow);
275 };
276 VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_1);
277 it.setFofFormula(_doubleArrow);
278 };
279 final VLSFofFormula comply = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function);
280 EList<VLSFofFormula> _formulas = trace.specification.getFormulas();
281 _formulas.add(comply);
282 }
283
284 public void transformRelation(final Relation r, final Logic2VampireLanguageMapperTrace trace) {
285 if (r instanceof RelationDeclaration) {
286 _transformRelation((RelationDeclaration)r, trace);
287 return;
288 } else if (r instanceof RelationDefinition) {
289 _transformRelation((RelationDefinition)r, trace);
290 return;
291 } else {
292 throw new IllegalArgumentException("Unhandled parameter types: " +
293 Arrays.<Object>asList(r, trace).toString());
294 }
295 }
296}
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-07-01 10:49:10 +0000