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.java260
1 files changed, 260 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..d5745333
--- /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,260 @@
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.Type;
19import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference;
20import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable;
21import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil;
22import java.util.ArrayList;
23import java.util.Arrays;
24import java.util.Collection;
25import java.util.HashMap;
26import java.util.List;
27import java.util.Map;
28import org.eclipse.emf.common.util.EList;
29import org.eclipse.xtext.xbase.lib.Conversions;
30import org.eclipse.xtext.xbase.lib.ExclusiveRange;
31import org.eclipse.xtext.xbase.lib.Extension;
32import org.eclipse.xtext.xbase.lib.ObjectExtensions;
33import org.eclipse.xtext.xbase.lib.Procedures.Procedure1;
34
35@SuppressWarnings("all")
36public class Logic2VampireLanguageMapper_RelationMapper {
37 @Extension
38 private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE;
39
40 private final Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support();
41
42 private final Logic2VampireLanguageMapper base;
43
44 public Logic2VampireLanguageMapper_RelationMapper(final Logic2VampireLanguageMapper base) {
45 this.base = base;
46 }
47
48 public void _transformRelation(final RelationDeclaration r, final Logic2VampireLanguageMapperTrace trace) {
49 final List<VLSVariable> relVar2VLS = new ArrayList<VLSVariable>();
50 final List<VLSFunction> relVar2TypeDecComply = new ArrayList<VLSFunction>();
51 int _length = ((Object[])Conversions.unwrapArray(r.getParameters(), Object.class)).length;
52 ExclusiveRange _doubleDotLessThan = new ExclusiveRange(0, _length, true);
53 for (final Integer i : _doubleDotLessThan) {
54 {
55 VLSVariable _createVLSVariable = this.factory.createVLSVariable();
56 final Procedure1<VLSVariable> _function = (VLSVariable it) -> {
57 it.setName(this.support.toIDMultiple("V", i.toString()));
58 };
59 final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function);
60 relVar2VLS.add(v);
61 TypeReference _get = r.getParameters().get((i).intValue());
62 final Type relType = ((ComplexTypeReference) _get).getReferred();
63 final VLSFunction varTypeComply = this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(relType, trace.type2Predicate), v);
64 relVar2TypeDecComply.add(varTypeComply);
65 }
66 }
67 VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();
68 final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> {
69 final String[] nameArray = r.getName().split(" ");
70 it.setName(this.support.toIDMultiple("compliance", nameArray[0], nameArray[2]));
71 it.setFofRole("axiom");
72 VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();
73 final Procedure1<VLSUniversalQuantifier> _function_1 = (VLSUniversalQuantifier it_1) -> {
74 for (final VLSVariable v : relVar2VLS) {
75 EList<VLSVariable> _variables = it_1.getVariables();
76 VLSVariable _duplicate = this.support.duplicate(v);
77 _variables.add(_duplicate);
78 }
79 VLSImplies _createVLSImplies = this.factory.createVLSImplies();
80 final Procedure1<VLSImplies> _function_2 = (VLSImplies it_2) -> {
81 VLSFunction _createVLSFunction = this.factory.createVLSFunction();
82 final Procedure1<VLSFunction> _function_3 = (VLSFunction it_3) -> {
83 it_3.setConstant(this.support.toIDMultiple("r", nameArray[0], nameArray[2]));
84 for (final VLSVariable v_1 : relVar2VLS) {
85 EList<VLSTerm> _terms = it_3.getTerms();
86 VLSVariable _duplicate_1 = this.support.duplicate(v_1);
87 _terms.add(_duplicate_1);
88 }
89 };
90 final VLSFunction rel = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_3);
91 trace.rel2Predicate.put(r, rel);
92 it_2.setLeft(this.support.duplicate(rel));
93 it_2.setRight(this.support.unfoldAnd(relVar2TypeDecComply));
94 };
95 VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_2);
96 it_1.setOperand(_doubleArrow);
97 };
98 VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_1);
99 it.setFofFormula(_doubleArrow);
100 };
101 final VLSFofFormula comply = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function);
102 EList<VLSFofFormula> _formulas = trace.specification.getFormulas();
103 _formulas.add(comply);
104 }
105
106 public void _transformRelation(final RelationDefinition reldef, final Logic2VampireLanguageMapperTrace trace) {
107 final Map<Variable, VLSVariable> relationVar2VLS = new HashMap<Variable, VLSVariable>();
108 final Map<Variable, VLSFunction> relationVar2TypeDecComply = new HashMap<Variable, VLSFunction>();
109 final Map<Variable, VLSFunction> relationVar2TypeDecRes = new HashMap<Variable, VLSFunction>();
110 final ArrayList<VLSTerm> typedefs = new ArrayList<VLSTerm>();
111 EList<Variable> _variables = reldef.getVariables();
112 for (final Variable variable : _variables) {
113 {
114 VLSVariable _createVLSVariable = this.factory.createVLSVariable();
115 final Procedure1<VLSVariable> _function = (VLSVariable it) -> {
116 it.setName(this.support.toIDMultiple("V", variable.getName()));
117 };
118 final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function);
119 relationVar2VLS.put(variable, v);
120 VLSFunction _createVLSFunction = this.factory.createVLSFunction();
121 final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> {
122 TypeReference _range = variable.getRange();
123 it.setConstant(this.support.toIDMultiple("t", ((ComplexTypeReference) _range).getReferred().getName()));
124 EList<VLSTerm> _terms = it.getTerms();
125 VLSVariable _duplicate = this.support.duplicate(v);
126 _terms.add(_duplicate);
127 };
128 final VLSFunction varTypeComply = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_1);
129 relationVar2TypeDecComply.put(variable, varTypeComply);
130 relationVar2TypeDecRes.put(variable, this.support.duplicate(varTypeComply));
131 }
132 }
133 final String[] nameArray = reldef.getName().split(" ");
134 VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();
135 final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> {
136 int _length = nameArray.length;
137 int _minus = (_length - 2);
138 int _length_1 = nameArray.length;
139 int _minus_1 = (_length_1 - 1);
140 it.setName(this.support.toIDMultiple("compliance", nameArray[_minus],
141 nameArray[_minus_1]));
142 it.setFofRole("axiom");
143 VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();
144 final Procedure1<VLSUniversalQuantifier> _function_1 = (VLSUniversalQuantifier it_1) -> {
145 EList<Variable> _variables_1 = reldef.getVariables();
146 for (final Variable variable_1 : _variables_1) {
147 EList<VLSVariable> _variables_2 = it_1.getVariables();
148 VLSVariable _duplicate = this.support.duplicate(CollectionsUtil.<Variable, VLSVariable>lookup(variable_1, relationVar2VLS));
149 _variables_2.add(_duplicate);
150 }
151 VLSImplies _createVLSImplies = this.factory.createVLSImplies();
152 final Procedure1<VLSImplies> _function_2 = (VLSImplies it_2) -> {
153 VLSFunction _createVLSFunction = this.factory.createVLSFunction();
154 final Procedure1<VLSFunction> _function_3 = (VLSFunction it_3) -> {
155 it_3.setConstant(this.support.toIDMultiple("rel", reldef.getName()));
156 EList<Variable> _variables_3 = reldef.getVariables();
157 for (final Variable variable_2 : _variables_3) {
158 {
159 VLSVariable _createVLSVariable = this.factory.createVLSVariable();
160 final Procedure1<VLSVariable> _function_4 = (VLSVariable it_4) -> {
161 it_4.setName(CollectionsUtil.<Variable, VLSVariable>lookup(variable_2, relationVar2VLS).getName());
162 };
163 final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_4);
164 EList<VLSTerm> _terms = it_3.getTerms();
165 _terms.add(v);
166 }
167 }
168 };
169 VLSFunction _doubleArrow = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_3);
170 it_2.setLeft(_doubleArrow);
171 Collection<VLSFunction> _values = relationVar2TypeDecComply.values();
172 ArrayList<VLSTerm> _arrayList = new ArrayList<VLSTerm>(_values);
173 it_2.setRight(this.support.unfoldAnd(_arrayList));
174 };
175 VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_2);
176 it_1.setOperand(_doubleArrow);
177 };
178 VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_1);
179 it.setFofFormula(_doubleArrow);
180 };
181 final VLSFofFormula comply = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function);
182 VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula();
183 final Procedure1<VLSFofFormula> _function_1 = (VLSFofFormula it) -> {
184 int _length = nameArray.length;
185 int _minus = (_length - 2);
186 int _length_1 = nameArray.length;
187 int _minus_1 = (_length_1 - 1);
188 it.setName(this.support.toIDMultiple("relation", nameArray[_minus],
189 nameArray[_minus_1]));
190 it.setFofRole("axiom");
191 VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();
192 final Procedure1<VLSUniversalQuantifier> _function_2 = (VLSUniversalQuantifier it_1) -> {
193 EList<Variable> _variables_1 = reldef.getVariables();
194 for (final Variable variable_1 : _variables_1) {
195 {
196 VLSVariable _createVLSVariable = this.factory.createVLSVariable();
197 final Procedure1<VLSVariable> _function_3 = (VLSVariable it_2) -> {
198 it_2.setName(CollectionsUtil.<Variable, VLSVariable>lookup(variable_1, relationVar2VLS).getName());
199 };
200 final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_3);
201 EList<VLSVariable> _variables_2 = it_1.getVariables();
202 _variables_2.add(v);
203 }
204 }
205 VLSImplies _createVLSImplies = this.factory.createVLSImplies();
206 final Procedure1<VLSImplies> _function_3 = (VLSImplies it_2) -> {
207 Collection<VLSFunction> _values = relationVar2TypeDecRes.values();
208 ArrayList<VLSTerm> _arrayList = new ArrayList<VLSTerm>(_values);
209 it_2.setLeft(this.support.unfoldAnd(_arrayList));
210 VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent();
211 final Procedure1<VLSEquivalent> _function_4 = (VLSEquivalent it_3) -> {
212 VLSFunction _createVLSFunction = this.factory.createVLSFunction();
213 final Procedure1<VLSFunction> _function_5 = (VLSFunction it_4) -> {
214 it_4.setConstant(this.support.toIDMultiple("rel", reldef.getName()));
215 EList<Variable> _variables_2 = reldef.getVariables();
216 for (final Variable variable_2 : _variables_2) {
217 {
218 VLSVariable _createVLSVariable = this.factory.createVLSVariable();
219 final Procedure1<VLSVariable> _function_6 = (VLSVariable it_5) -> {
220 it_5.setName(CollectionsUtil.<Variable, VLSVariable>lookup(variable_2, relationVar2VLS).getName());
221 };
222 final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function_6);
223 EList<VLSTerm> _terms = it_4.getTerms();
224 _terms.add(v);
225 }
226 }
227 };
228 VLSFunction _doubleArrow = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_5);
229 it_3.setLeft(_doubleArrow);
230 it_3.setRight(this.base.transformTerm(reldef.getValue(), trace, relationVar2VLS));
231 };
232 VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_4);
233 it_2.setRight(_doubleArrow);
234 };
235 VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_3);
236 it_1.setOperand(_doubleArrow);
237 };
238 VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_2);
239 it.setFofFormula(_doubleArrow);
240 };
241 final VLSFofFormula res = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_1);
242 EList<VLSFofFormula> _formulas = trace.specification.getFormulas();
243 _formulas.add(comply);
244 EList<VLSFofFormula> _formulas_1 = trace.specification.getFormulas();
245 _formulas_1.add(res);
246 }
247
248 public void transformRelation(final Relation r, final Logic2VampireLanguageMapperTrace trace) {
249 if (r instanceof RelationDeclaration) {
250 _transformRelation((RelationDeclaration)r, trace);
251 return;
252 } else if (r instanceof RelationDefinition) {
253 _transformRelation((RelationDefinition)r, trace);
254 return;
255 } else {
256 throw new IllegalArgumentException("Unhandled parameter types: " +
257 Arrays.<Object>asList(r, trace).toString());
258 }
259 }
260}
generated by cgit v1.2.3-70-g09d2 (git 2.46.0) at 2024-09-12 09:47:12 +0000