aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend
diff options
context:
space:
mode:
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend')
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend386
1 files changed, 386 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 @@
1package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder
2
3import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput
4import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And
5import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Assertion
6import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolLiteral
7import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference
8import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference
9import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration
10import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDefinition
11import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
12import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Distinct
13import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Equals
14import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Exists
15import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Forall
16import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration
17import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDefinition
18import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Iff
19import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Impl
20import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.InstanceOf
21import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntLiteral
22import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Not
23import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Or
24import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealLiteral
25import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation
26import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition
27import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue
28import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term
29import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable
30import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
31import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration
32import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm
33import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable
34import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory
35import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel
36import java.util.Collections
37import java.util.HashMap
38import java.util.List
39import java.util.Map
40import org.eclipse.xtend.lib.annotations.Accessors
41
42import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
43
44class 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
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-06-17 16:47:17 +0000