diff options
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.java | 510 |
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 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; | ||
2 | |||
3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration; | ||
4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; | ||
5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_ConstantMapper; | ||
6 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_ContainmentMapper; | ||
7 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_RelationMapper; | ||
8 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_ScopeMapper; | ||
9 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; | ||
10 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapper; | ||
11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSComment; | ||
12 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant; | ||
13 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality; | ||
14 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent; | ||
15 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; | ||
16 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; | ||
17 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies; | ||
18 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSInt; | ||
19 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; | ||
20 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUnaryNegation; | ||
21 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; | ||
22 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; | ||
23 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel; | ||
24 | import com.google.common.base.Objects; | ||
25 | import com.google.common.collect.Iterables; | ||
26 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput; | ||
27 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And; | ||
28 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Assertion; | ||
29 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolLiteral; | ||
30 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference; | ||
31 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference; | ||
32 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration; | ||
33 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDefinition; | ||
34 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement; | ||
35 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Distinct; | ||
36 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Equals; | ||
37 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Exists; | ||
38 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Forall; | ||
39 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration; | ||
40 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDefinition; | ||
41 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Iff; | ||
42 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Impl; | ||
43 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.InstanceOf; | ||
44 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntLiteral; | ||
45 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Not; | ||
46 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Or; | ||
47 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation; | ||
48 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration; | ||
49 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition; | ||
50 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicDeclaration; | ||
51 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue; | ||
52 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term; | ||
53 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; | ||
54 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference; | ||
55 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable; | ||
56 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.impl.RelationDeclarationImpl; | ||
57 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.impl.RelationDefinitionImpl; | ||
58 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem; | ||
59 | import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; | ||
60 | import java.util.Arrays; | ||
61 | import java.util.Collections; | ||
62 | import java.util.HashMap; | ||
63 | import java.util.List; | ||
64 | import java.util.Map; | ||
65 | import java.util.function.Consumer; | ||
66 | import org.eclipse.emf.common.util.EList; | ||
67 | import org.eclipse.xtend.lib.annotations.AccessorType; | ||
68 | import org.eclipse.xtend.lib.annotations.Accessors; | ||
69 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; | ||
70 | import org.eclipse.xtext.xbase.lib.Conversions; | ||
71 | import org.eclipse.xtext.xbase.lib.ExclusiveRange; | ||
72 | import org.eclipse.xtext.xbase.lib.Extension; | ||
73 | import org.eclipse.xtext.xbase.lib.Functions.Function1; | ||
74 | import org.eclipse.xtext.xbase.lib.IterableExtensions; | ||
75 | import org.eclipse.xtext.xbase.lib.ListExtensions; | ||
76 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; | ||
77 | import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; | ||
78 | import org.eclipse.xtext.xbase.lib.Pure; | ||
79 | |||
80 | @SuppressWarnings("all") | ||
81 | public 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 | } | ||