diff options
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder')
10 files changed, 1006 insertions, 0 deletions
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend new file mode 100644 index 00000000..5ec15541 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend | |||
@@ -0,0 +1,386 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Assertion | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolLiteral | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference | ||
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference | ||
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration | ||
10 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDefinition | ||
11 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement | ||
12 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Distinct | ||
13 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Equals | ||
14 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Exists | ||
15 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Forall | ||
16 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration | ||
17 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDefinition | ||
18 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Iff | ||
19 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Impl | ||
20 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.InstanceOf | ||
21 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntLiteral | ||
22 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Not | ||
23 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Or | ||
24 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealLiteral | ||
25 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation | ||
26 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition | ||
27 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue | ||
28 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term | ||
29 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable | ||
30 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | ||
31 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration | ||
32 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm | ||
33 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable | ||
34 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory | ||
35 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel | ||
36 | import java.util.Collections | ||
37 | import java.util.HashMap | ||
38 | import java.util.List | ||
39 | import java.util.Map | ||
40 | import org.eclipse.xtend.lib.annotations.Accessors | ||
41 | |||
42 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | ||
43 | |||
44 | class Logic2VampireLanguageMapper { | ||
45 | private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE | ||
46 | private val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support; | ||
47 | @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_ConstantMapper constantMapper = new Logic2VampireLanguageMapper_ConstantMapper( | ||
48 | this) | ||
49 | @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_RelationMapper relationMapper = new Logic2VampireLanguageMapper_RelationMapper( | ||
50 | this) | ||
51 | @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_TypeMapper typeMapper | ||
52 | |||
53 | public new(Logic2VampireLanguageMapper_TypeMapper typeMapper) { | ||
54 | this.typeMapper = typeMapper | ||
55 | } | ||
56 | |||
57 | public def TracedOutput<VampireModel, Logic2VampireLanguageMapperTrace> transformProblem(LogicProblem problem, | ||
58 | VampireSolverConfiguration configuration) { | ||
59 | // create model bases | ||
60 | // TODO | ||
61 | val initialComment = createVLSComment => [ | ||
62 | it.comment = "%This is an initial Test Comment \r" | ||
63 | ] | ||
64 | |||
65 | val specification = createVampireModel => [ | ||
66 | it.comments += initialComment | ||
67 | ] | ||
68 | |||
69 | val trace = new Logic2VampireLanguageMapperTrace => [ | ||
70 | it.specification = specification | ||
71 | |||
72 | // it.incQueryEngine = viatraQueryEngine.on(new EMFScope(problem)) | ||
73 | ] | ||
74 | |||
75 | // call mappers | ||
76 | if (!problem.types.isEmpty) { | ||
77 | typeMapper.transformTypes(problem.types, problem.elements, this, trace) | ||
78 | } | ||
79 | |||
80 | trace.constantDefinitions = problem.collectConstantDefinitions | ||
81 | trace.relationDefinitions = problem.collectRelationDefinitions | ||
82 | |||
83 | problem.relations.forEach[this.relationMapper.transformRelation(it, trace)] | ||
84 | |||
85 | // only transforms definitions | ||
86 | // problem.constants.filter(ConstantDefinition).forEach[this.constantMapper.transformConstant(it, trace)] | ||
87 | problem.constants.filter(ConstantDefinition).forEach [ | ||
88 | this.constantMapper.transformConstantDefinitionSpecification(it, trace) | ||
89 | ] | ||
90 | |||
91 | // ////////////////// | ||
92 | // Transform Assertions | ||
93 | // ////////////////// | ||
94 | for (assertion : problem.assertions) { | ||
95 | transformAssertion(assertion, trace) | ||
96 | } | ||
97 | |||
98 | return new TracedOutput(specification, trace) | ||
99 | } | ||
100 | |||
101 | // End of transformProblem | ||
102 | // //////////// | ||
103 | // Type References | ||
104 | // //////////// | ||
105 | def dispatch protected VLSTerm transformTypeReference(BoolTypeReference boolTypeReference, | ||
106 | Logic2VampireLanguageMapperTrace trace) { | ||
107 | // TODO, Not Now | ||
108 | // return createALSReference => [ it.referred = support.getBooleanType(trace) ] | ||
109 | } | ||
110 | |||
111 | // //////////// | ||
112 | // Collectors | ||
113 | // //////////// | ||
114 | // exact Same as for Alloy | ||
115 | private def collectConstantDefinitions(LogicProblem problem) { | ||
116 | val res = new HashMap | ||
117 | problem.constants.filter(ConstantDefinition).filter[it.defines !== null].forEach [ | ||
118 | res.put(it.defines, it) | ||
119 | ] | ||
120 | return res | ||
121 | } | ||
122 | |||
123 | private def collectRelationDefinitions(LogicProblem problem) { | ||
124 | val res = new HashMap | ||
125 | problem.relations.filter(RelationDefinition).filter[it.defines !== null].forEach [ | ||
126 | res.put(it.defines, it) | ||
127 | ] | ||
128 | return res | ||
129 | } | ||
130 | |||
131 | // //////////// | ||
132 | // Assertions + Terms | ||
133 | // //////////// | ||
134 | def protected transformAssertion(Assertion assertion, Logic2VampireLanguageMapperTrace trace) { | ||
135 | val res = createVLSFofFormula => [ | ||
136 | it.name = support.toID(assertion.name) | ||
137 | // below is temporary solution | ||
138 | it.fofRole = "axiom" | ||
139 | it.fofFormula = assertion.value.transformTerm(trace, Collections.EMPTY_MAP) | ||
140 | // it.annotation = nothing | ||
141 | ] | ||
142 | trace.specification.formulas += res | ||
143 | } | ||
144 | |||
145 | def dispatch protected VLSTerm transformTerm(BoolLiteral literal, Logic2VampireLanguageMapperTrace trace, | ||
146 | Map<Variable, VLSVariable> variables) { | ||
147 | if (literal.value == true) { | ||
148 | createVLSTrue | ||
149 | } else { | ||
150 | createVLSFalse | ||
151 | } | ||
152 | } | ||
153 | |||
154 | def dispatch protected VLSTerm transformTerm(IntLiteral literal, Logic2VampireLanguageMapperTrace trace, | ||
155 | Map<Variable, VLSVariable> variables) { | ||
156 | createVLSInt => [it.value = literal.value.toString()] | ||
157 | } | ||
158 | |||
159 | def dispatch protected VLSTerm transformTerm(RealLiteral literal, Logic2VampireLanguageMapperTrace trace, | ||
160 | Map<Variable, VLSVariable> variables) { | ||
161 | createVLSReal => [it.value = literal.value.toString()] | ||
162 | } | ||
163 | |||
164 | def dispatch protected VLSTerm transformTerm(Not not, Logic2VampireLanguageMapperTrace trace, | ||
165 | Map<Variable, VLSVariable> variables) { | ||
166 | createVLSUnaryNegation => [operand = not.operand.transformTerm(trace, variables)] | ||
167 | } | ||
168 | |||
169 | def dispatch protected VLSTerm transformTerm(And and, Logic2VampireLanguageMapperTrace trace, | ||
170 | Map<Variable, VLSVariable> variables) { support.unfoldAnd(and.operands.map[transformTerm(trace, variables)]) } | ||
171 | |||
172 | def dispatch protected VLSTerm transformTerm(Or or, Logic2VampireLanguageMapperTrace trace, | ||
173 | Map<Variable, VLSVariable> variables) { support.unfoldOr(or.operands.map[transformTerm(trace, variables)]) } | ||
174 | |||
175 | def dispatch protected VLSTerm transformTerm(Impl impl, Logic2VampireLanguageMapperTrace trace, | ||
176 | Map<Variable, VLSVariable> variables) { | ||
177 | createVLSImplies => [ | ||
178 | left = impl.leftOperand.transformTerm(trace, variables) | ||
179 | right = impl.rightOperand.transformTerm(trace, variables) | ||
180 | ] | ||
181 | } | ||
182 | |||
183 | def dispatch protected VLSTerm transformTerm(Iff iff, Logic2VampireLanguageMapperTrace trace, | ||
184 | Map<Variable, VLSVariable> variables) { | ||
185 | createVLSEquivalent => [ | ||
186 | left = iff.leftOperand.transformTerm(trace, variables) | ||
187 | right = iff.rightOperand.transformTerm(trace, variables) | ||
188 | ] | ||
189 | } | ||
190 | |||
191 | // def dispatch protected VLSTerm transformTerm(MoreThan moreThan, Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables) { | ||
192 | // createALSMore => [leftOperand = moreThan.leftOperand.transformTerm(trace,variables) rightOperand = moreThan.rightOperand.transformTerm(trace,variables)] } | ||
193 | // def dispatch protected VLSTerm transformTerm(LessThan lessThan, Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables) { | ||
194 | // createALSLess => [leftOperand = lessThan.leftOperand.transformTerm(trace,variables) rightOperand = lessThan.rightOperand.transformTerm(trace,variables)] } | ||
195 | // def dispatch protected VLSTerm transformTerm(MoreOrEqualThan moreThan, Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables) { | ||
196 | // createALSMeq => [leftOperand = moreThan.leftOperand.transformTerm(trace,variables) rightOperand = moreThan.rightOperand.transformTerm(trace,variables)] } | ||
197 | // def dispatch protected VLSTerm transformTerm(LessOrEqualThan lessThan, Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables) { | ||
198 | // createALSLeq => [leftOperand = lessThan.leftOperand.transformTerm(trace,variables) rightOperand = lessThan.rightOperand.transformTerm(trace,variables)] } | ||
199 | def dispatch protected VLSTerm transformTerm(Equals equals, Logic2VampireLanguageMapperTrace trace, | ||
200 | Map<Variable, VLSVariable> variables) { | ||
201 | createVLSEquality => [ | ||
202 | left = equals.leftOperand.transformTerm(trace, variables) | ||
203 | right = equals.rightOperand.transformTerm(trace, variables) | ||
204 | ] | ||
205 | } | ||
206 | |||
207 | def dispatch protected VLSTerm transformTerm(Distinct distinct, Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables) { | ||
208 | support.unfoldDistinctTerms(this,distinct.operands,trace,variables) } | ||
209 | // | ||
210 | // def dispatch protected ALSTerm transformTerm(Plus plus, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
211 | // createALSFunctionCall => [it.params += plus.leftOperand.transformTerm(trace,variables) it.params += plus.rightOperand.transformTerm(trace,variables) it.referredNumericOperator = ALSNumericOperator.PLUS] } | ||
212 | // def dispatch protected ALSTerm transformTerm(Minus minus, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
213 | // createALSFunctionCall => [it.params += minus.leftOperand.transformTerm(trace,variables) it.params += minus.rightOperand.transformTerm(trace,variables) it.referredNumericOperator = ALSNumericOperator.SUB] } | ||
214 | // def dispatch protected ALSTerm transformTerm(Multiply multiply, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
215 | // createALSFunctionCall => [it.params += multiply.leftOperand.transformTerm(trace,variables) it.params += multiply.rightOperand.transformTerm(trace,variables) it.referredNumericOperator = ALSNumericOperator.MUL] } | ||
216 | // def dispatch protected ALSTerm transformTerm(Divison div, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
217 | // createALSFunctionCall => [it.params += div.leftOperand.transformTerm(trace,variables) it.params += div.rightOperand.transformTerm(trace,variables) it.referredNumericOperator = ALSNumericOperator.DIV] } | ||
218 | // def dispatch protected ALSTerm transformTerm(Mod mod, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
219 | // createALSFunctionCall => [it.params += mod.leftOperand.transformTerm(trace,variables) it.params += mod.rightOperand.transformTerm(trace,variables) it.referredNumericOperator = ALSNumericOperator.REM] } | ||
220 | // | ||
221 | def dispatch protected VLSTerm transformTerm(Forall forall, Logic2VampireLanguageMapperTrace trace, | ||
222 | Map<Variable, VLSVariable> variables) { | ||
223 | support.createUniversallyQuantifiedExpression(this, forall, trace, variables) | ||
224 | } | ||
225 | |||
226 | def dispatch protected VLSTerm transformTerm(Exists exists, Logic2VampireLanguageMapperTrace trace, | ||
227 | Map<Variable, VLSVariable> variables) { | ||
228 | support.createExistentiallyQuantifiedExpression(this, exists, trace, variables) | ||
229 | } | ||
230 | |||
231 | def dispatch protected VLSTerm transformTerm(InstanceOf instanceOf, Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables) { | ||
232 | return createVLSFunction => [ | ||
233 | it.constant = support.toIDMultiple("type", (instanceOf.range as ComplexTypeReference).referred.name ) | ||
234 | it.terms += instanceOf.value.transformTerm(trace, variables) | ||
235 | ] | ||
236 | } | ||
237 | // | ||
238 | // def dispatch protected ALSTerm transformTerm(TransitiveClosure tc, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | ||
239 | // return this.relationMapper.transformTransitiveRelationReference( | ||
240 | // tc.relation, | ||
241 | // tc.leftOperand.transformTerm(trace,variables), | ||
242 | // tc.rightOperand.transformTerm(trace,variables), | ||
243 | // trace | ||
244 | // ) | ||
245 | // } | ||
246 | // | ||
247 | def dispatch protected VLSTerm transformTerm(SymbolicValue symbolicValue, Logic2VampireLanguageMapperTrace trace, | ||
248 | Map<Variable, VLSVariable> variables) { | ||
249 | symbolicValue.symbolicReference.transformSymbolicReference(symbolicValue.parameterSubstitutions, trace, | ||
250 | variables) | ||
251 | } | ||
252 | |||
253 | def dispatch protected VLSTerm transformSymbolicReference(DefinedElement referred, | ||
254 | List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace, | ||
255 | Map<Variable, VLSVariable> variables) { | ||
256 | typeMapper.transformReference(referred, trace) | ||
257 | } | ||
258 | |||
259 | def dispatch protected VLSTerm transformSymbolicReference(ConstantDeclaration constant, | ||
260 | List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace, | ||
261 | Map<Variable, VLSVariable> variables) { | ||
262 | // might need to make sure that only declared csts get transformed. see for Alloy | ||
263 | val res = createVLSConstant => [ | ||
264 | // ask if necessary VLSConstantDeclaration and not just directly strng | ||
265 | it.name = support.toID(constant.name) | ||
266 | ] | ||
267 | // no postprocessing cuz booleans are accepted | ||
268 | return res | ||
269 | } | ||
270 | |||
271 | // NOT NEEDED FOR NOW | ||
272 | // TODO | ||
273 | def dispatch protected VLSTerm transformSymbolicReference(ConstantDefinition constant, | ||
274 | List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace, | ||
275 | Map<Variable, VLSVariable> variables) { | ||
276 | // val res = createVLSFunctionCall => [ | ||
277 | // it.referredDefinition = constant.lookup(trace.constantDefinition2Function) | ||
278 | // ] | ||
279 | // return support.postprocessResultOfSymbolicReference(constant.type,res,trace) | ||
280 | } | ||
281 | |||
282 | def dispatch protected VLSTerm transformSymbolicReference(Variable variable, | ||
283 | List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace, | ||
284 | Map<Variable, VLSVariable> variables) { | ||
285 | |||
286 | // cannot treat variable as function (constant) because of name ID not being the same | ||
287 | // below does not work | ||
288 | val res = createVLSVariable => [ | ||
289 | // it.name = support.toIDMultiple("Var", variable.lookup(variables).name) | ||
290 | it.name = support.toID(variable.lookup(variables).name) | ||
291 | ] | ||
292 | // no need for potprocessing cuz booleans are supported | ||
293 | return res | ||
294 | } | ||
295 | |||
296 | // TODO | ||
297 | def dispatch protected VLSTerm transformSymbolicReference(FunctionDeclaration function, | ||
298 | List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace, | ||
299 | Map<Variable, VLSVariable> variables) { | ||
300 | // if(trace.functionDefinitions.containsKey(function)) { | ||
301 | // return this.transformSymbolicReference(function.lookup(trace.functionDefinitions),parameterSubstitutions,trace,variables) | ||
302 | // } else { | ||
303 | // if(functionMapper.transformedToHostedField(function,trace)) { | ||
304 | // val param = parameterSubstitutions.get(0).transformTerm(trace,variables) | ||
305 | // val res = createVLSJoin => [ | ||
306 | // leftOperand = support.prepareParameterOfSymbolicReference(function.parameters.get(0),param,trace) | ||
307 | // rightOperand = createVLSReference => [referred = function.lookup(trace.functionDeclaration2HostedField)] | ||
308 | // ] | ||
309 | // return support.postprocessResultOfSymbolicReference(function.range,res,trace) | ||
310 | // } else { | ||
311 | // val functionExpression = createVLSJoin=>[ | ||
312 | // leftOperand = createVLSReference => [referred = trace.logicLanguage] | ||
313 | // rightOperand = createVLSReference => [referred = function.lookup(trace.functionDeclaration2LanguageField)] | ||
314 | // ] | ||
315 | // val res = support.unfoldDotJoin(this,parameterSubstitutions,functionExpression,trace,variables) | ||
316 | // return support.postprocessResultOfSymbolicReference(function.range,res,trace) | ||
317 | // } | ||
318 | // } | ||
319 | } | ||
320 | |||
321 | // TODO | ||
322 | def dispatch protected VLSTerm transformSymbolicReference(FunctionDefinition function, | ||
323 | List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace, | ||
324 | Map<Variable, VLSVariable> variables) { | ||
325 | // val result = createVLSFunctionCall => [ | ||
326 | // it.referredDefinition = function.lookup(trace.functionDefinition2Function) | ||
327 | // it.params += parameterSubstitutions.map[it.transformTerm(trace,variables)] | ||
328 | // ] | ||
329 | // return support.postprocessResultOfSymbolicReference(function.range,result,trace) | ||
330 | } | ||
331 | |||
332 | // TODO | ||
333 | /* | ||
334 | def dispatch protected VLSTerm transformSymbolicReference(Relation relation, | ||
335 | List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace, | ||
336 | Map<Variable, VLSVariable> variables) { | ||
337 | if (trace.relationDefinitions.containsKey(relation)) { | ||
338 | this.transformSymbolicReference(relation.lookup(trace.relationDefinitions), | ||
339 | parameterSubstitutions, trace, variables) | ||
340 | } | ||
341 | else { | ||
342 | // if (relationMapper.transformToHostedField(relation, trace)) { | ||
343 | // val VLSRelation = relation.lookup(trace.relationDeclaration2Field) | ||
344 | // // R(a,b) => | ||
345 | // // b in a.R | ||
346 | // return createVLSSubset => [ | ||
347 | // it.leftOperand = parameterSubstitutions.get(1).transformTerm(trace, variables) | ||
348 | // it.rightOperand = createVLSJoin => [ | ||
349 | // it.leftOperand = parameterSubstitutions.get(0).transformTerm(trace, variables) | ||
350 | // it.rightOperand = createVLSReference => [it.referred = VLSRelation] | ||
351 | // ] | ||
352 | // ] | ||
353 | // } else { | ||
354 | // val target = createVLSJoin => [ | ||
355 | // leftOperand = createVLSReference => [referred = trace.logicLanguage] | ||
356 | // rightOperand = createVLSReference => [ | ||
357 | // referred = relation.lookup(trace.relationDeclaration2Global) | ||
358 | // ] | ||
359 | // ] | ||
360 | // val source = support.unfoldTermDirectProduct(this, parameterSubstitutions, trace, variables) | ||
361 | // | ||
362 | // return createVLSSubset => [ | ||
363 | // leftOperand = source | ||
364 | // rightOperand = target | ||
365 | // ] | ||
366 | // } | ||
367 | } | ||
368 | } | ||
369 | */ | ||
370 | |||
371 | // TODO | ||
372 | def dispatch protected VLSTerm transformSymbolicReference(Relation relation, | ||
373 | List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace, | ||
374 | Map<Variable, VLSVariable> variables) { | ||
375 | // createVLSFunction => [ | ||
376 | // it.referredDefinition = relation.lookup(trace.relationDefinition2Predicate) | ||
377 | // it.params += parameterSubstitutions.map[p|p.transformTerm(trace, variables)] | ||
378 | // ] | ||
379 | return createVLSFunction => [ | ||
380 | it.constant = support.toIDMultiple("rel", relation.name) | ||
381 | it.terms += parameterSubstitutions.map[p | p.transformTerm(trace,variables)] | ||
382 | ] | ||
383 | } | ||
384 | |||
385 | } | ||
386 | \ No newline at end of file | ||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend new file mode 100644 index 00000000..135b3f07 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend | |||
@@ -0,0 +1,39 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDefinition | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable | ||
8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula | ||
9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction | ||
10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm | ||
11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable | ||
12 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel | ||
13 | import java.util.HashMap | ||
14 | import java.util.Map | ||
15 | |||
16 | interface Logic2VampireLanguageMapper_TypeMapperTrace {} | ||
17 | |||
18 | class Logic2VampireLanguageMapperTrace { | ||
19 | // public var ViatraQueryEngine incQueryEngine; | ||
20 | |||
21 | //list of needed VLS components | ||
22 | public var VampireModel specification | ||
23 | public var VLSFofFormula logicLanguageBody | ||
24 | public var VLSTerm formula | ||
25 | //NOT NEEDED //public var VLSFunction constantDec | ||
26 | |||
27 | public var Logic2VampireLanguageMapper_TypeMapperTrace typeMapperTrace | ||
28 | |||
29 | |||
30 | //NOT NEEDED //public val Map<ConstantDeclaration, VLSFunctionDeclaration> constantDeclaration2LanguageField = new HashMap | ||
31 | //public val Map<ConstantDefinition, ALSFunctionDefinition> constantDefinition2Function = new HashMap | ||
32 | |||
33 | public var Map<ConstantDeclaration, ConstantDefinition> constantDefinitions | ||
34 | |||
35 | public var Map<RelationDeclaration, RelationDefinition> relationDefinitions | ||
36 | public val Map<Variable, VLSVariable> relationVar2VLS = new HashMap | ||
37 | public val Map<Variable, VLSFunction> relationVar2TypeDec = new HashMap | ||
38 | |||
39 | } \ No newline at end of file | ||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ConstantMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ConstantMapper.xtend new file mode 100644 index 00000000..2366ea15 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ConstantMapper.xtend | |||
@@ -0,0 +1,42 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDefinition | ||
5 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory | ||
6 | |||
7 | class Logic2VampireLanguageMapper_ConstantMapper { | ||
8 | private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE | ||
9 | private val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support | ||
10 | val Logic2VampireLanguageMapper base | ||
11 | |||
12 | public new(Logic2VampireLanguageMapper base) { | ||
13 | this.base = base | ||
14 | } | ||
15 | |||
16 | //NOT NEEDED | ||
17 | // def protected dispatch transformConstant(ConstantDeclaration constant, Logic2VampireLanguageMapperTrace trace) { | ||
18 | // val c = createVLSFunctionDeclaration=> [ | ||
19 | // it.name = support.toID(constant.name) | ||
20 | // ] | ||
21 | // trace.constantDec.constant = c | ||
22 | // trace.constantDeclaration2LanguageField.put(constant, c); | ||
23 | // | ||
24 | // } | ||
25 | |||
26 | //NOT Used In Sample | ||
27 | def protected dispatch transformConstant(ConstantDefinition constant, Logic2VampireLanguageMapperTrace trace) { | ||
28 | //error | ||
29 | //TODO | ||
30 | // val c = createVLSFofFormula=> [ | ||
31 | // name = support.toID(constant.name) | ||
32 | // fofRole = "axiom" | ||
33 | // fofFormula = base.transformTypeReference() | ||
34 | // ] | ||
35 | } | ||
36 | |||
37 | def protected transformConstantDefinitionSpecification(ConstantDefinition constant, Logic2VampireLanguageMapperTrace trace) { | ||
38 | //TODO | ||
39 | } | ||
40 | |||
41 | |||
42 | } \ No newline at end of file | ||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend new file mode 100644 index 00000000..60653a42 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend | |||
@@ -0,0 +1,183 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable | ||
7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction | ||
8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm | ||
9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable | ||
10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory | ||
11 | import java.util.ArrayList | ||
12 | import java.util.HashMap | ||
13 | import java.util.List | ||
14 | import java.util.Map | ||
15 | |||
16 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | ||
17 | |||
18 | class Logic2VampireLanguageMapper_RelationMapper { | ||
19 | private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE | ||
20 | private val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support | ||
21 | val Logic2VampireLanguageMapper base | ||
22 | |||
23 | public new(Logic2VampireLanguageMapper base) { | ||
24 | this.base = base | ||
25 | } | ||
26 | |||
27 | def dispatch public void transformRelation(RelationDefinition r, Logic2VampireLanguageMapperTrace trace) { | ||
28 | |||
29 | // 1. store all variables in support wrt their name | ||
30 | // 1.1 if variable has type, creating list of type declarations | ||
31 | val Map<Variable, VLSVariable> relationVar2VLS = new HashMap | ||
32 | val Map<Variable, VLSFunction> relationVar2TypeDecComply = new HashMap | ||
33 | val Map<Variable, VLSFunction> relationVar2TypeDecRes = new HashMap | ||
34 | val typedefs = new ArrayList<VLSTerm> | ||
35 | for (variable : r.variables) { | ||
36 | val v = createVLSVariable => [ | ||
37 | it.name = support.toIDMultiple("Var", variable.name) | ||
38 | ] | ||
39 | relationVar2VLS.put(variable, v) | ||
40 | |||
41 | val varTypeComply = createVLSFunction => [ | ||
42 | it.constant = support.toIDMultiple("type", (variable.range as ComplexTypeReference).referred.name) | ||
43 | it.terms += createVLSVariable => [ | ||
44 | it.name = support.toIDMultiple("Var", variable.name) | ||
45 | ] | ||
46 | ] | ||
47 | relationVar2TypeDecComply.put(variable, varTypeComply) | ||
48 | |||
49 | val varTypeRes = createVLSFunction => [ | ||
50 | it.constant = support.toIDMultiple("type", (variable.range as ComplexTypeReference).referred.name) | ||
51 | it.terms += createVLSVariable => [ | ||
52 | it.name = support.toIDMultiple("Var", variable.name) | ||
53 | ] | ||
54 | ] | ||
55 | relationVar2TypeDecRes.put(variable, varTypeRes) | ||
56 | } | ||
57 | |||
58 | val comply = createVLSFofFormula => [ | ||
59 | it.name = support.toIDMultiple("compliance", r.name) | ||
60 | it.fofRole = "axiom" | ||
61 | it.fofFormula = createVLSUniversalQuantifier => [ | ||
62 | for (variable : r.variables) { | ||
63 | val v = createVLSVariable => [ | ||
64 | it.name = variable.lookup(relationVar2VLS).name | ||
65 | ] | ||
66 | it.variables += v | ||
67 | |||
68 | } | ||
69 | it.operand = createVLSImplies => [ | ||
70 | it.left = createVLSFunction => [ | ||
71 | it.constant = support.toIDMultiple("rel", r.name) | ||
72 | for (variable : r.variables) { | ||
73 | val v = createVLSVariable => [ | ||
74 | it.name = variable.lookup(relationVar2VLS).name | ||
75 | ] | ||
76 | it.terms += v | ||
77 | } | ||
78 | ] | ||
79 | it.right = support.unfoldAnd(new ArrayList<VLSTerm>(relationVar2TypeDecComply.values)) | ||
80 | ] | ||
81 | ] | ||
82 | ] | ||
83 | |||
84 | val res = createVLSFofFormula => [ | ||
85 | it.name = support.toIDMultiple("relation", r.name) | ||
86 | it.fofRole = "axiom" | ||
87 | it.fofFormula = createVLSUniversalQuantifier => [ | ||
88 | for (variable : r.variables) { | ||
89 | val v = createVLSVariable => [ | ||
90 | it.name = variable.lookup(relationVar2VLS).name | ||
91 | ] | ||
92 | it.variables += v | ||
93 | |||
94 | } | ||
95 | it.operand = createVLSImplies => [ | ||
96 | it.left = support.unfoldAnd(new ArrayList<VLSTerm>(relationVar2TypeDecRes.values)) | ||
97 | it.right = createVLSEquivalent => [ | ||
98 | it.left = createVLSFunction => [ | ||
99 | it.constant = support.toIDMultiple("rel", r.name) | ||
100 | for (variable : r.variables) { | ||
101 | val v = createVLSVariable => [ | ||
102 | it.name = variable.lookup(relationVar2VLS).name | ||
103 | ] | ||
104 | it.terms += v | ||
105 | |||
106 | } | ||
107 | ] | ||
108 | it.right = base.transformTerm(r.value, trace, relationVar2VLS) | ||
109 | ] | ||
110 | |||
111 | ] | ||
112 | |||
113 | ] | ||
114 | |||
115 | ] | ||
116 | |||
117 | // trace.relationDefinition2Predicate.put(r,res) | ||
118 | trace.specification.formulas += comply; | ||
119 | trace.specification.formulas += res; | ||
120 | |||
121 | } | ||
122 | |||
123 | def dispatch public void transformRelation(RelationDeclaration r, Logic2VampireLanguageMapperTrace trace) { | ||
124 | |||
125 | // 1. store all variables in support wrt their name | ||
126 | // 1.1 if variable has type, creating list of type declarations | ||
127 | val List<VLSVariable> relationVar2VLS = new ArrayList | ||
128 | val List<VLSFunction> relationVar2TypeDecComply = new ArrayList | ||
129 | val typedefs = new ArrayList<VLSTerm> | ||
130 | |||
131 | for (i : 0..<r.parameters.length) { | ||
132 | |||
133 | val v = createVLSVariable => [ | ||
134 | it.name = support.toIDMultiple("Var", i.toString) | ||
135 | ] | ||
136 | relationVar2VLS.add(v) | ||
137 | |||
138 | val varTypeComply = createVLSFunction => [ | ||
139 | it.constant = support.toIDMultiple("type", (r.parameters.get(i) as ComplexTypeReference).referred.name) | ||
140 | it.terms += createVLSVariable => [ | ||
141 | it.name = support.toIDMultiple("Var", i.toString) | ||
142 | ] | ||
143 | ] | ||
144 | relationVar2TypeDecComply.add(varTypeComply) | ||
145 | |||
146 | } | ||
147 | |||
148 | |||
149 | val comply = createVLSFofFormula => [ | ||
150 | it.name = support.toIDMultiple("compliance", r.name) | ||
151 | it.fofRole = "axiom" | ||
152 | it.fofFormula = createVLSUniversalQuantifier => [ | ||
153 | |||
154 | for (i : 0..<r.parameters.length) { | ||
155 | val v = createVLSVariable => [ | ||
156 | it.name = relationVar2VLS.get(i).name | ||
157 | ] | ||
158 | it.variables += v | ||
159 | |||
160 | } | ||
161 | |||
162 | it.operand = createVLSImplies => [ | ||
163 | it.left = createVLSFunction => [ | ||
164 | it.constant = support.toIDMultiple("rel", r.name) | ||
165 | |||
166 | for (i : 0..<r.parameters.length) { | ||
167 | val v = createVLSVariable => [ | ||
168 | it.name = relationVar2VLS.get(i).name | ||
169 | ] | ||
170 | it.terms += v | ||
171 | } | ||
172 | |||
173 | ] | ||
174 | it.right = support.unfoldAnd(relationVar2TypeDecComply) | ||
175 | ] | ||
176 | ] | ||
177 | ] | ||
178 | |||
179 | // trace.relationDefinition2Predicate.put(r,res) | ||
180 | trace.specification.formulas += comply | ||
181 | } | ||
182 | |||
183 | } | ||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend new file mode 100644 index 00000000..ab92b42f --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend | |||
@@ -0,0 +1,148 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.QuantifiedExpression | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable | ||
5 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm | ||
6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable | ||
7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory | ||
8 | import java.util.ArrayList | ||
9 | import java.util.HashMap | ||
10 | import java.util.List | ||
11 | import java.util.Map | ||
12 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference | ||
13 | import org.eclipse.emf.common.util.EList | ||
14 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term | ||
15 | |||
16 | class Logic2VampireLanguageMapper_Support { | ||
17 | private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE | ||
18 | |||
19 | // ID Handler | ||
20 | def protected String toIDMultiple(String... ids) { | ||
21 | ids.map[it.split("\\s+").join("_")].join("_") | ||
22 | } | ||
23 | |||
24 | def protected String toID(String ids) { | ||
25 | ids.split("\\s+").join("_") | ||
26 | } | ||
27 | |||
28 | // Support Functions | ||
29 | // booleans | ||
30 | // AND and OR | ||
31 | def protected VLSTerm unfoldAnd(List<? extends VLSTerm> operands) { | ||
32 | if (operands.size == 1) { | ||
33 | return operands.head | ||
34 | } else if (operands.size > 1) { | ||
35 | return createVLSAnd => [ | ||
36 | left = operands.head | ||
37 | right = operands.subList(1, operands.size).unfoldAnd | ||
38 | ] | ||
39 | } else | ||
40 | throw new UnsupportedOperationException('''Logic operator with 0 operands!''') | ||
41 | } | ||
42 | |||
43 | def protected VLSTerm unfoldOr(List<? extends VLSTerm> operands) { | ||
44 | |||
45 | // if(operands.size == 0) {basically return true} | ||
46 | /*else*/ if (operands.size == 1) { | ||
47 | return operands.head | ||
48 | } else if (operands.size > 1) { | ||
49 | return createVLSOr => [ | ||
50 | left = operands.head | ||
51 | right = operands.subList(1, operands.size).unfoldOr | ||
52 | ] | ||
53 | } else | ||
54 | throw new UnsupportedOperationException('''Logic operator with 0 operands!''') // TEMP | ||
55 | } | ||
56 | |||
57 | def protected VLSTerm unfoldDistinctTerms(Logic2VampireLanguageMapper m, EList<Term> operands, | ||
58 | Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables) { | ||
59 | if(operands.size == 1) { return m.transformTerm(operands.head,trace,variables) } | ||
60 | else if(operands.size > 1) { | ||
61 | val notEquals = new ArrayList<VLSTerm>(operands.size*operands.size/2) | ||
62 | for(i:0..<operands.size) { | ||
63 | for(j: i+1..<operands.size) { | ||
64 | notEquals+=createVLSInequality=>[ | ||
65 | it.left= m.transformTerm(operands.get(i),trace,variables) | ||
66 | it.right = m.transformTerm(operands.get(j),trace,variables) | ||
67 | ] | ||
68 | } | ||
69 | } | ||
70 | return notEquals.unfoldAnd | ||
71 | } | ||
72 | else throw new UnsupportedOperationException('''Logic operator with 0 operands!''') | ||
73 | } | ||
74 | |||
75 | // Symbolic | ||
76 | // def postprocessResultOfSymbolicReference(TypeReference type, VLSTerm term, Logic2VampireLanguageMapperTrace trace) { | ||
77 | // if(type instanceof BoolTypeReference) { | ||
78 | // return booleanToLogicValue(term ,trace) | ||
79 | // } | ||
80 | // else return term | ||
81 | // } | ||
82 | // def booleanToLogicValue(VLSTerm term, Logic2VampireLanguageMapperTrace trace) { | ||
83 | // throw new UnsupportedOperationException("TODO: auto-generated method stub") | ||
84 | // } | ||
85 | /* | ||
86 | * def protected String toID(List<String> ids) { | ||
87 | * ids.map[it.split("\\s+").join("'")].join("'") | ||
88 | * } | ||
89 | */ | ||
90 | // QUANTIFIERS + VARIABLES | ||
91 | def protected VLSTerm createUniversallyQuantifiedExpression(Logic2VampireLanguageMapper mapper, | ||
92 | QuantifiedExpression expression, Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables) { | ||
93 | val variableMap = expression.quantifiedVariables.toInvertedMap [ v | | ||
94 | createVLSVariable => [it.name = toIDMultiple("Var", v.name)] | ||
95 | ] | ||
96 | |||
97 | val typedefs = new ArrayList<VLSTerm> | ||
98 | for (variable : expression.quantifiedVariables) { | ||
99 | val eq = createVLSFunction => [ | ||
100 | it.constant = toIDMultiple("type", (variable.range as ComplexTypeReference).referred.name) | ||
101 | it.terms += createVLSVariable => [ | ||
102 | it.name = toIDMultiple("Var", variable.name) | ||
103 | ] | ||
104 | |||
105 | ] | ||
106 | typedefs.add(eq) | ||
107 | } | ||
108 | |||
109 | |||
110 | createVLSUniversalQuantifier => [ | ||
111 | it.variables += variableMap.values | ||
112 | it.operand = createVLSImplies => [ | ||
113 | it.left = unfoldAnd(typedefs) | ||
114 | it.right = mapper.transformTerm(expression.expression, trace, variables.withAddition(variableMap)) | ||
115 | ] | ||
116 | ] | ||
117 | } | ||
118 | |||
119 | def protected VLSTerm createExistentiallyQuantifiedExpression(Logic2VampireLanguageMapper mapper, | ||
120 | QuantifiedExpression expression, Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables) { | ||
121 | val variableMap = expression.quantifiedVariables.toInvertedMap [ v | | ||
122 | createVLSVariable => [it.name = toIDMultiple("Var", v.name)] | ||
123 | ] | ||
124 | |||
125 | val typedefs = new ArrayList<VLSTerm> | ||
126 | for (variable : expression.quantifiedVariables) { | ||
127 | val eq = createVLSFunction => [ | ||
128 | it.constant = toIDMultiple("type", (variable.range as ComplexTypeReference).referred.name) | ||
129 | it.terms += createVLSVariable => [ | ||
130 | it.name = toIDMultiple("Var", variable.name) | ||
131 | ] | ||
132 | ] | ||
133 | typedefs.add(eq) | ||
134 | } | ||
135 | |||
136 | typedefs.add(mapper.transformTerm(expression.expression, trace, variables.withAddition(variableMap))) | ||
137 | createVLSExistentialQuantifier => [ | ||
138 | it.variables += variableMap.values | ||
139 | it.operand = unfoldAnd(typedefs) | ||
140 | |||
141 | ] | ||
142 | } | ||
143 | |||
144 | def protected withAddition(Map<Variable, VLSVariable> map1, Map<Variable, VLSVariable> map2) { | ||
145 | new HashMap(map1) => [putAll(map2)] | ||
146 | } | ||
147 | |||
148 | } | ||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend new file mode 100644 index 00000000..1f071635 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend | |||
@@ -0,0 +1,19 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
5 | import java.util.Collection | ||
6 | import java.util.List | ||
7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm | ||
8 | |||
9 | interface Logic2VampireLanguageMapper_TypeMapper { | ||
10 | def void transformTypes(Collection<Type> types, Collection<DefinedElement> elements, Logic2VampireLanguageMapper mapper, Logic2VampireLanguageMapperTrace trace); | ||
11 | //samples below 2 lines | ||
12 | def List<VLSTerm> transformTypeReference(Type referred, Logic2VampireLanguageMapper mapper, Logic2VampireLanguageMapperTrace trace) | ||
13 | def VLSTerm getUndefinedSupertype(Logic2VampireLanguageMapperTrace trace) | ||
14 | |||
15 | def int getUndefinedSupertypeScope(int undefinedScope,Logic2VampireLanguageMapperTrace trace) | ||
16 | def VLSTerm transformReference(DefinedElement referred,Logic2VampireLanguageMapperTrace trace) | ||
17 | |||
18 | def VampireModelInterpretation_TypeInterpretation getTypeInterpreter() | ||
19 | } \ No newline at end of file | ||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtend new file mode 100644 index 00000000..a0f0edda --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes.xtend | |||
@@ -0,0 +1,21 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
5 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality | ||
6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction | ||
7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm | ||
8 | import java.util.ArrayList | ||
9 | import java.util.HashMap | ||
10 | import java.util.List | ||
11 | import java.util.Map | ||
12 | |||
13 | class Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes implements Logic2VampireLanguageMapper_TypeMapperTrace{ | ||
14 | |||
15 | // public var VLSFofFormula objectSuperClass | ||
16 | public val Map<Type, VLSFunction> type2Predicate = new HashMap; | ||
17 | public val Map<DefinedElement, VLSEquality> definedElement2Declaration = new HashMap //Not Yet Used | ||
18 | public val Map<Type, VLSTerm> type2PossibleNot = new HashMap | ||
19 | public val Map<Type, VLSTerm> type2And = new HashMap | ||
20 | |||
21 | } \ No newline at end of file | ||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend new file mode 100644 index 00000000..7221f3ff --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend | |||
@@ -0,0 +1,158 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage | ||
7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm | ||
8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable | ||
9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory | ||
10 | import java.util.ArrayList | ||
11 | import java.util.Collection | ||
12 | |||
13 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | ||
14 | |||
15 | class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2VampireLanguageMapper_TypeMapper { | ||
16 | private val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support | ||
17 | private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE | ||
18 | |||
19 | new() { | ||
20 | LogicproblemPackage.eINSTANCE.class | ||
21 | } | ||
22 | |||
23 | override transformTypes(Collection<Type> types, Collection<DefinedElement> elements, | ||
24 | Logic2VampireLanguageMapper mapper, Logic2VampireLanguageMapperTrace trace) { | ||
25 | val typeTrace = new Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes | ||
26 | trace.typeMapperTrace = typeTrace | ||
27 | |||
28 | val VLSVariable variable = createVLSVariable => [it.name = "A"] // did not work | ||
29 | // 1. store predicates for declarations in trace | ||
30 | for (type : types) { | ||
31 | val typePred = createVLSFunction => [ | ||
32 | it.constant = support.toIDMultiple("type", type.name) | ||
33 | it.terms += createVLSVariable => [it.name = variable.name] | ||
34 | ] | ||
35 | typeTrace.type2Predicate.put(type, typePred) | ||
36 | } | ||
37 | |||
38 | // 2. Map each type definition to fof formula | ||
39 | for (type : types.filter(TypeDefinition)) { | ||
40 | |||
41 | val res = createVLSFofFormula => [ | ||
42 | it.name = support.toIDMultiple("typeDef", type.name) | ||
43 | // below is temporary solution | ||
44 | it.fofRole = "axiom" | ||
45 | it.fofFormula = createVLSUniversalQuantifier => [ | ||
46 | it.variables += createVLSVariable => [it.name = variable.name] | ||
47 | it.operand = createVLSEquivalent => [ | ||
48 | it.left = createVLSFunction => [ | ||
49 | it.constant = type.lookup(typeTrace.type2Predicate).constant | ||
50 | it.terms += createVLSVariable => [it.name = "A"] | ||
51 | ] | ||
52 | |||
53 | type.lookup(typeTrace.type2Predicate) | ||
54 | it.right = support.unfoldOr(type.elements.map [ e | | ||
55 | createVLSEquality => [ | ||
56 | it.left = createVLSVariable => [it.name = variable.name] | ||
57 | // it.right = createVLSDoubleQuote => [ | ||
58 | // it.value = "\"" + e.name + "\"" | ||
59 | // ] | ||
60 | it.right = createVLSDoubleQuote => [ | ||
61 | it.value = "\"a" + e.name + "\"" | ||
62 | ] | ||
63 | ] | ||
64 | ]) | ||
65 | ] | ||
66 | ] | ||
67 | |||
68 | ] | ||
69 | trace.specification.formulas += res | ||
70 | } | ||
71 | // 2.5. Currently allowing duplicate types. Not problematic cuz strings are by def unique | ||
72 | // 3. For each non-abstract type, create an and sequence containing all typedeclaration predicates | ||
73 | // and store in a map | ||
74 | // val List<VLSTerm> type2PossibleNot = new ArrayList | ||
75 | // val List<VLSTerm> type2And = new ArrayList | ||
76 | for (type : types.filter[!isIsAbstract]) { | ||
77 | for (type2 : types) { | ||
78 | // possible improvement: check all supertypes and decide if negated or not based on negations/not negations of supertypes | ||
79 | if (type == type2 || dfsSupertypeCheck(type, type2)) { | ||
80 | typeTrace.type2PossibleNot.put(type2, createVLSFunction => [ | ||
81 | it.constant = type2.lookup(typeTrace.type2Predicate).constant | ||
82 | it.terms += createVLSVariable => [it.name = "A"] | ||
83 | ]) | ||
84 | } else { | ||
85 | typeTrace.type2PossibleNot.put(type2, createVLSUnaryNegation => [ | ||
86 | it.operand = createVLSFunction => [ | ||
87 | it.constant = type2.lookup(typeTrace.type2Predicate).constant | ||
88 | it.terms += createVLSVariable => [it.name = "A"] | ||
89 | ] | ||
90 | ]) | ||
91 | } | ||
92 | // typeTrace.type2PossibleNot.put(type2, type2.lookup(typeTrace.type2Predicate)) | ||
93 | } | ||
94 | typeTrace.type2And.put(type, support.unfoldAnd(new ArrayList<VLSTerm>(typeTrace.type2PossibleNot.values))) | ||
95 | // typeTrace.type2And.put(type, type.lookup(typeTrace.type2Predicate) ) | ||
96 | typeTrace.type2PossibleNot.clear | ||
97 | } | ||
98 | |||
99 | // 5. create fof function that is an or with all the elements in map | ||
100 | val hierarch = createVLSFofFormula => [ | ||
101 | it.name = "hierarchyHandler" | ||
102 | it.fofRole = "axiom" | ||
103 | it.fofFormula = createVLSUniversalQuantifier => [ | ||
104 | it.variables += createVLSVariable => [it.name = "A"] | ||
105 | it.operand = createVLSEquivalent => [ | ||
106 | it.left = createVLSFunction => [ | ||
107 | it.constant = "Object" | ||
108 | it.terms += createVLSVariable => [ | ||
109 | it.name = "A" | ||
110 | ] | ||
111 | ] | ||
112 | it.right = support.unfoldOr(new ArrayList<VLSTerm>(typeTrace.type2And.values)) | ||
113 | ] | ||
114 | ] | ||
115 | ] | ||
116 | |||
117 | trace.specification.formulas += hierarch | ||
118 | } | ||
119 | |||
120 | def boolean dfsSupertypeCheck(Type type, Type type2) { | ||
121 | // There is surely a better way to do this | ||
122 | if (type.supertypes.isEmpty) | ||
123 | return false | ||
124 | else { | ||
125 | if (type.supertypes.contains(type2)) | ||
126 | return true | ||
127 | else { | ||
128 | for (supertype : type.supertypes) { | ||
129 | if(dfsSupertypeCheck(supertype, type2)) return true | ||
130 | } | ||
131 | } | ||
132 | } | ||
133 | } | ||
134 | |||
135 | override transformTypeReference(Type referred, Logic2VampireLanguageMapper mapper, | ||
136 | Logic2VampireLanguageMapperTrace trace) { | ||
137 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | ||
138 | } | ||
139 | |||
140 | override getUndefinedSupertype(Logic2VampireLanguageMapperTrace trace) { | ||
141 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | ||
142 | } | ||
143 | |||
144 | override getUndefinedSupertypeScope(int undefinedScope, Logic2VampireLanguageMapperTrace trace) { | ||
145 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | ||
146 | } | ||
147 | |||
148 | override transformReference(DefinedElement referred, Logic2VampireLanguageMapperTrace trace) { | ||
149 | createVLSDoubleQuote => [ | ||
150 | it.value = "\"a" + referred.name + "\"" | ||
151 | ] | ||
152 | } | ||
153 | |||
154 | override getTypeInterpreter() { | ||
155 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | ||
156 | } | ||
157 | |||
158 | } | ||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation_TypeInterpretation.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation_TypeInterpretation.xtend new file mode 100644 index 00000000..66f4fb06 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation_TypeInterpretation.xtend | |||
@@ -0,0 +1,5 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder | ||
2 | |||
3 | interface VampireModelInterpretation_TypeInterpretation { | ||
4 | |||
5 | } \ No newline at end of file | ||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtend new file mode 100644 index 00000000..863ec783 --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtend | |||
@@ -0,0 +1,5 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder | ||
2 | |||
3 | class VampireModelInterpretation_TypeInterpretation_FilteredTypes implements VampireModelInterpretation_TypeInterpretation { | ||
4 | //TODO | ||
5 | } \ No newline at end of file | ||