aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.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.java')
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java510
1 files changed, 0 insertions, 510 deletions
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java
deleted file mode 100644
index dc5ec788..00000000
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java
+++ /dev/null
@@ -1,510 +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.Logic2VampireLanguageMapperTrace;
5import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_ConstantMapper;
6import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_ContainmentMapper;
7import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_RelationMapper;
8import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_ScopeMapper;
9import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support;
10import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapper;
11import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSComment;
12import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant;
13import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality;
14import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent;
15import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula;
16import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction;
17import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies;
18import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSInt;
19import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm;
20import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUnaryNegation;
21import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable;
22import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory;
23import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel;
24import com.google.common.base.Objects;
25import com.google.common.collect.Iterables;
26import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput;
27import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And;
28import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Assertion;
29import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolLiteral;
30import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference;
31import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference;
32import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration;
33import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDefinition;
34import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement;
35import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Distinct;
36import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Equals;
37import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Exists;
38import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Forall;
39import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration;
40import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDefinition;
41import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Iff;
42import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Impl;
43import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.InstanceOf;
44import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntLiteral;
45import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Not;
46import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Or;
47import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation;
48import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration;
49import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition;
50import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicDeclaration;
51import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue;
52import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term;
53import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type;
54import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference;
55import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable;
56import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.impl.RelationDeclarationImpl;
57import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.impl.RelationDefinitionImpl;
58import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem;
59import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil;
60import java.util.Arrays;
61import java.util.Collections;
62import java.util.HashMap;
63import java.util.List;
64import java.util.Map;
65import java.util.function.Consumer;
66import org.eclipse.emf.common.util.EList;
67import org.eclipse.xtend.lib.annotations.AccessorType;
68import org.eclipse.xtend.lib.annotations.Accessors;
69import org.eclipse.xtext.xbase.lib.CollectionLiterals;
70import org.eclipse.xtext.xbase.lib.Conversions;
71import org.eclipse.xtext.xbase.lib.ExclusiveRange;
72import org.eclipse.xtext.xbase.lib.Extension;
73import org.eclipse.xtext.xbase.lib.Functions.Function1;
74import org.eclipse.xtext.xbase.lib.IterableExtensions;
75import org.eclipse.xtext.xbase.lib.ListExtensions;
76import org.eclipse.xtext.xbase.lib.ObjectExtensions;
77import org.eclipse.xtext.xbase.lib.Procedures.Procedure1;
78import org.eclipse.xtext.xbase.lib.Pure;
79
80@SuppressWarnings("all")
81public class Logic2VampireLanguageMapper {
82 @Extension
83 private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE;
84
85 private final Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support();
86
87 @Accessors(AccessorType.PUBLIC_GETTER)
88 private final Logic2VampireLanguageMapper_ConstantMapper constantMapper = new Logic2VampireLanguageMapper_ConstantMapper(this);
89
90 @Accessors(AccessorType.PUBLIC_GETTER)
91 private final Logic2VampireLanguageMapper_ContainmentMapper containmentMapper = new Logic2VampireLanguageMapper_ContainmentMapper(this);
92
93 @Accessors(AccessorType.PUBLIC_GETTER)
94 private final Logic2VampireLanguageMapper_RelationMapper relationMapper = new Logic2VampireLanguageMapper_RelationMapper(this);
95
96 @Accessors(AccessorType.PUBLIC_GETTER)
97 private final Logic2VampireLanguageMapper_ScopeMapper scopeMapper = new Logic2VampireLanguageMapper_ScopeMapper(this);
98
99 @Accessors(AccessorType.PUBLIC_GETTER)
100 private final Logic2VampireLanguageMapper_TypeMapper typeMapper = new Logic2VampireLanguageMapper_TypeMapper(this);
101
102 public TracedOutput<VampireModel, Logic2VampireLanguageMapperTrace> transformProblem(final LogicProblem problem, final VampireSolverConfiguration config) {
103 VLSComment _createVLSComment = this.factory.createVLSComment();
104 final Procedure1<VLSComment> _function = (VLSComment it) -> {
105 it.setComment("%This is an initial Test Comment");
106 };
107 final VLSComment initialComment = ObjectExtensions.<VLSComment>operator_doubleArrow(_createVLSComment, _function);
108 VampireModel _createVampireModel = this.factory.createVampireModel();
109 final Procedure1<VampireModel> _function_1 = (VampireModel it) -> {
110 EList<VLSComment> _comments = it.getComments();
111 _comments.add(initialComment);
112 };
113 final VampireModel specification = ObjectExtensions.<VampireModel>operator_doubleArrow(_createVampireModel, _function_1);
114 Logic2VampireLanguageMapperTrace _logic2VampireLanguageMapperTrace = new Logic2VampireLanguageMapperTrace();
115 final Procedure1<Logic2VampireLanguageMapperTrace> _function_2 = (Logic2VampireLanguageMapperTrace it) -> {
116 it.specification = specification;
117 };
118 final Logic2VampireLanguageMapperTrace trace = ObjectExtensions.<Logic2VampireLanguageMapperTrace>operator_doubleArrow(_logic2VampireLanguageMapperTrace, _function_2);
119 boolean _isEmpty = problem.getTypes().isEmpty();
120 boolean _not = (!_isEmpty);
121 if (_not) {
122 this.typeMapper.transformTypes(problem.getTypes(), problem.getElements(), this, trace);
123 }
124 trace.relationDefinitions = this.collectRelationDefinitions(problem);
125 final Function1<Relation, Boolean> _function_3 = (Relation it) -> {
126 Class<? extends Relation> _class = it.getClass();
127 return Boolean.valueOf(Objects.equal(_class, RelationDefinitionImpl.class));
128 };
129 this.toTrace(IterableExtensions.<Relation>filter(problem.getRelations(), _function_3), trace);
130 final Consumer<Relation> _function_4 = (Relation it) -> {
131 Logic2VampireLanguageMapper _logic2VampireLanguageMapper = new Logic2VampireLanguageMapper();
132 this.relationMapper.transformRelation(it, trace, _logic2VampireLanguageMapper);
133 };
134 problem.getRelations().forEach(_function_4);
135 this.containmentMapper.transformContainment(config, problem.getContainmentHierarchies(), trace);
136 this.scopeMapper.transformScope(problem.getTypes(), config, trace);
137 trace.constantDefinitions = this.collectConstantDefinitions(problem);
138 final Consumer<ConstantDefinition> _function_5 = (ConstantDefinition it) -> {
139 this.constantMapper.transformConstantDefinitionSpecification(it, trace);
140 };
141 Iterables.<ConstantDefinition>filter(problem.getConstants(), ConstantDefinition.class).forEach(_function_5);
142 EList<Assertion> _assertions = problem.getAssertions();
143 for (final Assertion assertion : _assertions) {
144 this.transformAssertion(assertion, trace);
145 }
146 return new TracedOutput<VampireModel, Logic2VampireLanguageMapperTrace>(specification, trace);
147 }
148
149 public void toTrace(final Iterable<Relation> relations, final Logic2VampireLanguageMapperTrace trace) {
150 final List<VLSVariable> vars = CollectionLiterals.<VLSVariable>newArrayList();
151 for (final Relation rel : relations) {
152 {
153 final String[] nameArray = rel.getName().split(" ");
154 String relNameVar = "";
155 int _length = nameArray.length;
156 boolean _equals = (_length == 3);
157 if (_equals) {
158 relNameVar = this.support.toIDMultiple(nameArray[0], nameArray[2]);
159 } else {
160 relNameVar = rel.getName();
161 }
162 final String relName = relNameVar;
163 final RelationDefinition relDef = ((RelationDefinition) rel);
164 int _length_1 = ((Object[])Conversions.unwrapArray(rel.getParameters(), Object.class)).length;
165 ExclusiveRange _doubleDotLessThan = new ExclusiveRange(0, _length_1, true);
166 for (final Integer i : _doubleDotLessThan) {
167 {
168 VLSVariable _createVLSVariable = this.factory.createVLSVariable();
169 final Procedure1<VLSVariable> _function = (VLSVariable it) -> {
170 it.setName(this.support.toIDMultiple("V", i.toString()));
171 };
172 final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function);
173 vars.add(v);
174 }
175 }
176 VLSFunction _createVLSFunction = this.factory.createVLSFunction();
177 final Procedure1<VLSFunction> _function = (VLSFunction it) -> {
178 it.setConstant(this.support.toIDMultiple("r", relName));
179 for (final VLSVariable v : vars) {
180 EList<VLSTerm> _terms = it.getTerms();
181 VLSVariable _duplicate = this.support.duplicate(v);
182 _terms.add(_duplicate);
183 }
184 };
185 final VLSFunction relFunc = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function);
186 trace.relDef2Predicate.put(relDef, relFunc);
187 trace.predicate2RelDef.put(relFunc, relDef);
188 }
189 }
190 }
191
192 protected VLSTerm _transformTypeReference(final BoolTypeReference boolTypeReference, final Logic2VampireLanguageMapperTrace trace) {
193 return null;
194 }
195
196 private HashMap<ConstantDeclaration, ConstantDefinition> collectConstantDefinitions(final LogicProblem problem) {
197 final HashMap<ConstantDeclaration, ConstantDefinition> res = new HashMap<ConstantDeclaration, ConstantDefinition>();
198 final Function1<ConstantDefinition, Boolean> _function = (ConstantDefinition it) -> {
199 ConstantDeclaration _defines = it.getDefines();
200 return Boolean.valueOf((_defines != null));
201 };
202 final Consumer<ConstantDefinition> _function_1 = (ConstantDefinition it) -> {
203 res.put(it.getDefines(), it);
204 };
205 IterableExtensions.<ConstantDefinition>filter(Iterables.<ConstantDefinition>filter(problem.getConstants(), ConstantDefinition.class), _function).forEach(_function_1);
206 return res;
207 }
208
209 private HashMap<RelationDeclaration, RelationDefinition> collectRelationDefinitions(final LogicProblem problem) {
210 final HashMap<RelationDeclaration, RelationDefinition> res = new HashMap<RelationDeclaration, RelationDefinition>();
211 final Function1<RelationDefinition, Boolean> _function = (RelationDefinition it) -> {
212 RelationDeclaration _defines = it.getDefines();
213 return Boolean.valueOf((_defines != null));
214 };
215 final Consumer<RelationDefinition> _function_1 = (RelationDefinition it) -> {
216 res.put(it.getDefines(), it);
217 };
218 IterableExtensions.<RelationDefinition>filter(Iterables.<RelationDefinition>filter(problem.getRelations(), RelationDefinition.class), _function).forEach(_function_1);
219 return res;
220 }
221
222 protected boolean transformAssertion(final Assertion assertion, final Logic2VampireLanguageMapperTrace trace) {
223 boolean _xblockexpression = false;
224 {
225 VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();
226 final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> {
227 String _name = assertion.getName();
228 String _plus = ("assertion_" + _name);
229 it.setName(this.support.toID(_plus));
230 it.setFofRole("axiom");
231 it.setFofFormula(this.transformTerm(assertion.getValue(), trace, Collections.EMPTY_MAP));
232 };
233 final VLSFofFormula res = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function);
234 EList<VLSFofFormula> _formulas = trace.specification.getFormulas();
235 _xblockexpression = _formulas.add(res);
236 }
237 return _xblockexpression;
238 }
239
240 protected VLSTerm _transformTerm(final BoolLiteral literal, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {
241 VLSTerm _xifexpression = null;
242 boolean _isValue = literal.isValue();
243 boolean _equals = (_isValue == true);
244 if (_equals) {
245 _xifexpression = this.factory.createVLSTrue();
246 } else {
247 _xifexpression = this.factory.createVLSFalse();
248 }
249 return _xifexpression;
250 }
251
252 protected VLSTerm _transformTerm(final IntLiteral literal, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {
253 VLSInt _createVLSInt = this.factory.createVLSInt();
254 final Procedure1<VLSInt> _function = (VLSInt it) -> {
255 it.setValue(Integer.valueOf(literal.getValue()).toString());
256 };
257 return ObjectExtensions.<VLSInt>operator_doubleArrow(_createVLSInt, _function);
258 }
259
260 protected VLSTerm _transformTerm(final Not not, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {
261 VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation();
262 final Procedure1<VLSUnaryNegation> _function = (VLSUnaryNegation it) -> {
263 it.setOperand(this.transformTerm(not.getOperand(), trace, variables));
264 };
265 return ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function);
266 }
267
268 protected VLSTerm _transformTerm(final And and, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {
269 final Function1<Term, VLSTerm> _function = (Term it) -> {
270 return this.transformTerm(it, trace, variables);
271 };
272 return this.support.unfoldAnd(ListExtensions.<Term, VLSTerm>map(and.getOperands(), _function));
273 }
274
275 protected VLSTerm _transformTerm(final Or or, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {
276 final Function1<Term, VLSTerm> _function = (Term it) -> {
277 return this.transformTerm(it, trace, variables);
278 };
279 return this.support.unfoldOr(ListExtensions.<Term, VLSTerm>map(or.getOperands(), _function));
280 }
281
282 protected VLSTerm _transformTerm(final Impl impl, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {
283 VLSImplies _createVLSImplies = this.factory.createVLSImplies();
284 final Procedure1<VLSImplies> _function = (VLSImplies it) -> {
285 it.setLeft(this.transformTerm(impl.getLeftOperand(), trace, variables));
286 it.setRight(this.transformTerm(impl.getRightOperand(), trace, variables));
287 };
288 return ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function);
289 }
290
291 protected VLSTerm _transformTerm(final Iff iff, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {
292 VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent();
293 final Procedure1<VLSEquivalent> _function = (VLSEquivalent it) -> {
294 it.setLeft(this.transformTerm(iff.getLeftOperand(), trace, variables));
295 it.setRight(this.transformTerm(iff.getRightOperand(), trace, variables));
296 };
297 return ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function);
298 }
299
300 protected VLSTerm _transformTerm(final Equals equals, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {
301 VLSEquality _createVLSEquality = this.factory.createVLSEquality();
302 final Procedure1<VLSEquality> _function = (VLSEquality it) -> {
303 it.setLeft(this.transformTerm(equals.getLeftOperand(), trace, variables));
304 it.setRight(this.transformTerm(equals.getRightOperand(), trace, variables));
305 };
306 return ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function);
307 }
308
309 protected VLSTerm _transformTerm(final Distinct distinct, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {
310 return this.support.unfoldDistinctTerms(this, distinct.getOperands(), trace, variables);
311 }
312
313 protected VLSTerm _transformTerm(final Forall forall, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {
314 return this.support.createQuantifiedExpression(this, forall, trace, variables, true);
315 }
316
317 protected VLSTerm _transformTerm(final Exists exists, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {
318 return this.support.createQuantifiedExpression(this, exists, trace, variables, false);
319 }
320
321 protected VLSTerm _transformTerm(final InstanceOf instanceOf, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {
322 VLSFunction _createVLSFunction = this.factory.createVLSFunction();
323 final Procedure1<VLSFunction> _function = (VLSFunction it) -> {
324 TypeReference _range = instanceOf.getRange();
325 it.setConstant(CollectionsUtil.<Type, VLSFunction>lookup(((ComplexTypeReference) _range).getReferred(), trace.type2Predicate).getConstant());
326 EList<VLSTerm> _terms = it.getTerms();
327 VLSTerm _transformTerm = this.transformTerm(instanceOf.getValue(), trace, variables);
328 _terms.add(_transformTerm);
329 };
330 return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function);
331 }
332
333 protected VLSTerm _transformTerm(final SymbolicValue symbolicValue, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {
334 return this.transformSymbolicReference(symbolicValue.getSymbolicReference(), symbolicValue.getParameterSubstitutions(), trace, variables);
335 }
336
337 protected VLSTerm _transformSymbolicReference(final DefinedElement referred, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {
338 final String name = CollectionsUtil.<DefinedElement, String>lookup(referred, trace.definedElement2String);
339 VLSConstant _createVLSConstant = this.factory.createVLSConstant();
340 final Procedure1<VLSConstant> _function = (VLSConstant it) -> {
341 it.setName(name);
342 };
343 return ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _function);
344 }
345
346 protected VLSTerm _transformSymbolicReference(final ConstantDeclaration constant, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {
347 VLSConstant _createVLSConstant = this.factory.createVLSConstant();
348 final Procedure1<VLSConstant> _function = (VLSConstant it) -> {
349 it.setName(this.support.toID(constant.getName()));
350 };
351 final VLSConstant res = ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _function);
352 return res;
353 }
354
355 protected VLSTerm _transformSymbolicReference(final ConstantDefinition constant, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {
356 return null;
357 }
358
359 protected VLSTerm _transformSymbolicReference(final Variable variable, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {
360 return this.support.duplicate(CollectionsUtil.<Variable, VLSVariable>lookup(variable, variables));
361 }
362
363 protected VLSTerm _transformSymbolicReference(final FunctionDeclaration function, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {
364 return null;
365 }
366
367 protected VLSTerm _transformSymbolicReference(final FunctionDefinition function, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {
368 return null;
369 }
370
371 /**
372 * def dispatch protected VLSTerm transformSymbolicReference(Relation relation,
373 * List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace,
374 * Map<Variable, VLSVariable> variables) {
375 * if (trace.relationDefinitions.containsKey(relation)) {
376 * this.transformSymbolicReference(relation.lookup(trace.relationDefinitions),
377 * parameterSubstitutions, trace, variables)
378 * }
379 * else {
380 * // if (relationMapper.transformToHostedField(relation, trace)) {
381 * // val VLSRelation = relation.lookup(trace.relationDeclaration2Field)
382 * // // R(a,b) =>
383 * // // b in a.R
384 * // return createVLSSubset => [
385 * // it.leftOperand = parameterSubstitutions.get(1).transformTerm(trace, variables)
386 * // it.rightOperand = createVLSJoin => [
387 * // it.leftOperand = parameterSubstitutions.get(0).transformTerm(trace, variables)
388 * // it.rightOperand = createVLSReference => [it.referred = VLSRelation]
389 * // ]
390 * // ]
391 * // } else {
392 * // val target = createVLSJoin => [
393 * // leftOperand = createVLSReference => [referred = trace.logicLanguage]
394 * // rightOperand = createVLSReference => [
395 * // referred = relation.lookup(trace.relationDeclaration2Global)
396 * // ]
397 * // ]
398 * // val source = support.unfoldTermDirectProduct(this, parameterSubstitutions, trace, variables)
399 * //
400 * // return createVLSSubset => [
401 * // leftOperand = source
402 * // rightOperand = target
403 * // ]
404 * // }
405 * }
406 * }
407 */
408 protected VLSTerm _transformSymbolicReference(final Relation relation, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {
409 VLSFunction _createVLSFunction = this.factory.createVLSFunction();
410 final Procedure1<VLSFunction> _function = (VLSFunction it) -> {
411 Class<? extends Relation> _class = relation.getClass();
412 boolean _equals = Objects.equal(_class, RelationDeclarationImpl.class);
413 if (_equals) {
414 it.setConstant(CollectionsUtil.<RelationDeclaration, VLSFunction>lookup(((RelationDeclaration) relation), trace.rel2Predicate).getConstant());
415 } else {
416 it.setConstant(CollectionsUtil.<RelationDefinition, VLSFunction>lookup(((RelationDefinition) relation), trace.relDef2Predicate).getConstant());
417 }
418 EList<VLSTerm> _terms = it.getTerms();
419 final Function1<Term, VLSTerm> _function_1 = (Term p) -> {
420 return this.transformTerm(p, trace, variables);
421 };
422 List<VLSTerm> _map = ListExtensions.<Term, VLSTerm>map(parameterSubstitutions, _function_1);
423 Iterables.<VLSTerm>addAll(_terms, _map);
424 };
425 return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function);
426 }
427
428 protected VLSTerm transformTypeReference(final BoolTypeReference boolTypeReference, final Logic2VampireLanguageMapperTrace trace) {
429 return _transformTypeReference(boolTypeReference, trace);
430 }
431
432 protected VLSTerm transformTerm(final Term and, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {
433 if (and instanceof And) {
434 return _transformTerm((And)and, trace, variables);
435 } else if (and instanceof BoolLiteral) {
436 return _transformTerm((BoolLiteral)and, trace, variables);
437 } else if (and instanceof Distinct) {
438 return _transformTerm((Distinct)and, trace, variables);
439 } else if (and instanceof Equals) {
440 return _transformTerm((Equals)and, trace, variables);
441 } else if (and instanceof Exists) {
442 return _transformTerm((Exists)and, trace, variables);
443 } else if (and instanceof Forall) {
444 return _transformTerm((Forall)and, trace, variables);
445 } else if (and instanceof Iff) {
446 return _transformTerm((Iff)and, trace, variables);
447 } else if (and instanceof Impl) {
448 return _transformTerm((Impl)and, trace, variables);
449 } else if (and instanceof IntLiteral) {
450 return _transformTerm((IntLiteral)and, trace, variables);
451 } else if (and instanceof Not) {
452 return _transformTerm((Not)and, trace, variables);
453 } else if (and instanceof Or) {
454 return _transformTerm((Or)and, trace, variables);
455 } else if (and instanceof InstanceOf) {
456 return _transformTerm((InstanceOf)and, trace, variables);
457 } else if (and instanceof SymbolicValue) {
458 return _transformTerm((SymbolicValue)and, trace, variables);
459 } else {
460 throw new IllegalArgumentException("Unhandled parameter types: " +
461 Arrays.<Object>asList(and, trace, variables).toString());
462 }
463 }
464
465 protected VLSTerm transformSymbolicReference(final SymbolicDeclaration constant, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) {
466 if (constant instanceof ConstantDeclaration) {
467 return _transformSymbolicReference((ConstantDeclaration)constant, parameterSubstitutions, trace, variables);
468 } else if (constant instanceof ConstantDefinition) {
469 return _transformSymbolicReference((ConstantDefinition)constant, parameterSubstitutions, trace, variables);
470 } else if (constant instanceof FunctionDeclaration) {
471 return _transformSymbolicReference((FunctionDeclaration)constant, parameterSubstitutions, trace, variables);
472 } else if (constant instanceof FunctionDefinition) {
473 return _transformSymbolicReference((FunctionDefinition)constant, parameterSubstitutions, trace, variables);
474 } else if (constant instanceof DefinedElement) {
475 return _transformSymbolicReference((DefinedElement)constant, parameterSubstitutions, trace, variables);
476 } else if (constant instanceof Relation) {
477 return _transformSymbolicReference((Relation)constant, parameterSubstitutions, trace, variables);
478 } else if (constant instanceof Variable) {
479 return _transformSymbolicReference((Variable)constant, parameterSubstitutions, trace, variables);
480 } else {
481 throw new IllegalArgumentException("Unhandled parameter types: " +
482 Arrays.<Object>asList(constant, parameterSubstitutions, trace, variables).toString());
483 }
484 }
485
486 @Pure
487 public Logic2VampireLanguageMapper_ConstantMapper getConstantMapper() {
488 return this.constantMapper;
489 }
490
491 @Pure
492 public Logic2VampireLanguageMapper_ContainmentMapper getContainmentMapper() {
493 return this.containmentMapper;
494 }
495
496 @Pure
497 public Logic2VampireLanguageMapper_RelationMapper getRelationMapper() {
498 return this.relationMapper;
499 }
500
501 @Pure
502 public Logic2VampireLanguageMapper_ScopeMapper getScopeMapper() {
503 return this.scopeMapper;
504 }
505
506 @Pure
507 public Logic2VampireLanguageMapper_TypeMapper getTypeMapper() {
508 return this.typeMapper;
509 }
510}
generated by cgit v1.2.3-54-g00ecf (git 2.45.0) at 2024-05-05 18:50:35 +0000