diff options
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.xtend | 203 |
1 files changed, 104 insertions, 99 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 index cd48a032..e2c15b75 100644 --- 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 | |||
@@ -48,6 +48,8 @@ class Logic2VampireLanguageMapper { | |||
48 | this) | 48 | this) |
49 | @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_RelationMapper relationMapper = new Logic2VampireLanguageMapper_RelationMapper( | 49 | @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_RelationMapper relationMapper = new Logic2VampireLanguageMapper_RelationMapper( |
50 | this) | 50 | this) |
51 | @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_ScopeMapper scopeMapper = new Logic2VampireLanguageMapper_ScopeMapper( | ||
52 | this) | ||
51 | @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_TypeMapper typeMapper | 53 | @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_TypeMapper typeMapper |
52 | 54 | ||
53 | public new(Logic2VampireLanguageMapper_TypeMapper typeMapper) { | 55 | public new(Logic2VampireLanguageMapper_TypeMapper typeMapper) { |
@@ -72,11 +74,15 @@ class Logic2VampireLanguageMapper { | |||
72 | // it.incQueryEngine = viatraQueryEngine.on(new EMFScope(problem)) | 74 | // it.incQueryEngine = viatraQueryEngine.on(new EMFScope(problem)) |
73 | ] | 75 | ] |
74 | 76 | ||
75 | // call mappers | 77 | // TYPE MAPPER |
76 | if (!problem.types.isEmpty) { | 78 | if (!problem.types.isEmpty) { |
77 | typeMapper.transformTypes(problem.types, problem.elements, this, trace) | 79 | typeMapper.transformTypes(problem.types, problem.elements, this, trace) |
78 | } | 80 | } |
79 | 81 | ||
82 | // SCOPE MAPPER | ||
83 | scopeMapper.transformScope(config, trace) | ||
84 | |||
85 | |||
80 | trace.constantDefinitions = problem.collectConstantDefinitions | 86 | trace.constantDefinitions = problem.collectConstantDefinitions |
81 | trace.relationDefinitions = problem.collectRelationDefinitions | 87 | trace.relationDefinitions = problem.collectRelationDefinitions |
82 | 88 | ||
@@ -204,8 +210,9 @@ class Logic2VampireLanguageMapper { | |||
204 | ] | 210 | ] |
205 | } | 211 | } |
206 | 212 | ||
207 | def dispatch protected VLSTerm transformTerm(Distinct distinct, Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables) { | 213 | def dispatch protected VLSTerm transformTerm(Distinct distinct, Logic2VampireLanguageMapperTrace trace, |
208 | support.unfoldDistinctTerms(this,distinct.operands,trace,variables) } | 214 | Map<Variable, VLSVariable> variables) { support.unfoldDistinctTerms(this, distinct.operands, trace, variables) } |
215 | |||
209 | // | 216 | // |
210 | // def dispatch protected ALSTerm transformTerm(Plus plus, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | 217 | // 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] } | 218 | // createALSFunctionCall => [it.params += plus.leftOperand.transformTerm(trace,variables) it.params += plus.rightOperand.transformTerm(trace,variables) it.referredNumericOperator = ALSNumericOperator.PLUS] } |
@@ -228,12 +235,14 @@ class Logic2VampireLanguageMapper { | |||
228 | support.createExistentiallyQuantifiedExpression(this, exists, trace, variables) | 235 | support.createExistentiallyQuantifiedExpression(this, exists, trace, variables) |
229 | } | 236 | } |
230 | 237 | ||
231 | def dispatch protected VLSTerm transformTerm(InstanceOf instanceOf, Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables) { | 238 | def dispatch protected VLSTerm transformTerm(InstanceOf instanceOf, Logic2VampireLanguageMapperTrace trace, |
239 | Map<Variable, VLSVariable> variables) { | ||
232 | return createVLSFunction => [ | 240 | return createVLSFunction => [ |
233 | it.constant = support.toIDMultiple("type", (instanceOf.range as ComplexTypeReference).referred.name ) | 241 | it.constant = support.toIDMultiple("type", (instanceOf.range as ComplexTypeReference).referred.name) |
234 | it.terms += instanceOf.value.transformTerm(trace, variables) | 242 | it.terms += instanceOf.value.transformTerm(trace, variables) |
235 | ] | 243 | ] |
236 | } | 244 | } |
245 | |||
237 | // | 246 | // |
238 | // def dispatch protected ALSTerm transformTerm(TransitiveClosure tc, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { | 247 | // def dispatch protected ALSTerm transformTerm(TransitiveClosure tc, Logic2AlloyLanguageMapperTrace trace, Map<Variable, ALSVariableDeclaration> variables) { |
239 | // return this.relationMapper.transformTransitiveRelationReference( | 248 | // return this.relationMapper.transformTransitiveRelationReference( |
@@ -253,50 +262,49 @@ class Logic2VampireLanguageMapper { | |||
253 | def dispatch protected VLSTerm transformSymbolicReference(DefinedElement referred, | 262 | def dispatch protected VLSTerm transformSymbolicReference(DefinedElement referred, |
254 | List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace, | 263 | List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace, |
255 | Map<Variable, VLSVariable> variables) { | 264 | Map<Variable, VLSVariable> variables) { |
256 | typeMapper.transformReference(referred, trace) | 265 | typeMapper.transformReference(referred, trace) |
257 | } | 266 | } |
258 | 267 | ||
259 | def dispatch protected VLSTerm transformSymbolicReference(ConstantDeclaration constant, | 268 | def dispatch protected VLSTerm transformSymbolicReference(ConstantDeclaration constant, |
260 | List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace, | 269 | List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace, |
261 | Map<Variable, VLSVariable> variables) { | 270 | Map<Variable, VLSVariable> variables) { |
262 | // might need to make sure that only declared csts get transformed. see for Alloy | 271 | // might need to make sure that only declared csts get transformed. see for Alloy |
263 | val res = createVLSConstant => [ | 272 | val res = createVLSConstant => [ |
264 | // ask if necessary VLSConstantDeclaration and not just directly strng | 273 | // ask if necessary VLSConstantDeclaration and not just directly strng |
265 | it.name = support.toID(constant.name) | 274 | it.name = support.toID(constant.name) |
266 | ] | 275 | ] |
267 | // no postprocessing cuz booleans are accepted | 276 | // no postprocessing cuz booleans are accepted |
268 | return res | 277 | return res |
269 | } | 278 | } |
270 | 279 | ||
271 | // NOT NEEDED FOR NOW | 280 | // NOT NEEDED FOR NOW |
272 | // TODO | 281 | // TODO |
273 | def dispatch protected VLSTerm transformSymbolicReference(ConstantDefinition constant, | 282 | def dispatch protected VLSTerm transformSymbolicReference(ConstantDefinition constant, |
274 | List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace, | 283 | List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace, |
275 | Map<Variable, VLSVariable> variables) { | 284 | Map<Variable, VLSVariable> variables) { |
276 | // val res = createVLSFunctionCall => [ | 285 | // val res = createVLSFunctionCall => [ |
277 | // it.referredDefinition = constant.lookup(trace.constantDefinition2Function) | 286 | // it.referredDefinition = constant.lookup(trace.constantDefinition2Function) |
278 | // ] | 287 | // ] |
279 | // return support.postprocessResultOfSymbolicReference(constant.type,res,trace) | 288 | // return support.postprocessResultOfSymbolicReference(constant.type,res,trace) |
280 | } | 289 | } |
281 | 290 | ||
282 | def dispatch protected VLSTerm transformSymbolicReference(Variable variable, | 291 | def dispatch protected VLSTerm transformSymbolicReference(Variable variable, List<Term> parameterSubstitutions, |
283 | List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace, | 292 | Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables) { |
284 | Map<Variable, VLSVariable> variables) { | ||
285 | 293 | ||
286 | // cannot treat variable as function (constant) because of name ID not being the same | 294 | // cannot treat variable as function (constant) because of name ID not being the same |
287 | // below does not work | 295 | // below does not work |
288 | val res = createVLSVariable => [ | 296 | val res = createVLSVariable => [ |
289 | // it.name = support.toIDMultiple("Var", variable.lookup(variables).name) | 297 | // it.name = support.toIDMultiple("Var", variable.lookup(variables).name) |
290 | it.name = support.toID(variable.lookup(variables).name) | 298 | it.name = support.toID(variable.lookup(variables).name) |
291 | ] | 299 | ] |
292 | // no need for potprocessing cuz booleans are supported | 300 | // no need for potprocessing cuz booleans are supported |
293 | return res | 301 | return res |
294 | } | 302 | } |
295 | 303 | ||
296 | // TODO | 304 | // TODO |
297 | def dispatch protected VLSTerm transformSymbolicReference(FunctionDeclaration function, | 305 | def dispatch protected VLSTerm transformSymbolicReference(FunctionDeclaration function, |
298 | List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace, | 306 | List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace, |
299 | Map<Variable, VLSVariable> variables) { | 307 | Map<Variable, VLSVariable> variables) { |
300 | // if(trace.functionDefinitions.containsKey(function)) { | 308 | // if(trace.functionDefinitions.containsKey(function)) { |
301 | // return this.transformSymbolicReference(function.lookup(trace.functionDefinitions),parameterSubstitutions,trace,variables) | 309 | // return this.transformSymbolicReference(function.lookup(trace.functionDefinitions),parameterSubstitutions,trace,variables) |
302 | // } else { | 310 | // } else { |
@@ -316,71 +324,68 @@ class Logic2VampireLanguageMapper { | |||
316 | // return support.postprocessResultOfSymbolicReference(function.range,res,trace) | 324 | // return support.postprocessResultOfSymbolicReference(function.range,res,trace) |
317 | // } | 325 | // } |
318 | // } | 326 | // } |
319 | } | 327 | } |
320 | 328 | ||
321 | // TODO | 329 | // TODO |
322 | def dispatch protected VLSTerm transformSymbolicReference(FunctionDefinition function, | 330 | def dispatch protected VLSTerm transformSymbolicReference(FunctionDefinition function, |
323 | List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace, | 331 | List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace, |
324 | Map<Variable, VLSVariable> variables) { | 332 | Map<Variable, VLSVariable> variables) { |
325 | // val result = createVLSFunctionCall => [ | 333 | // val result = createVLSFunctionCall => [ |
326 | // it.referredDefinition = function.lookup(trace.functionDefinition2Function) | 334 | // it.referredDefinition = function.lookup(trace.functionDefinition2Function) |
327 | // it.params += parameterSubstitutions.map[it.transformTerm(trace,variables)] | 335 | // it.params += parameterSubstitutions.map[it.transformTerm(trace,variables)] |
328 | // ] | 336 | // ] |
329 | // return support.postprocessResultOfSymbolicReference(function.range,result,trace) | 337 | // return support.postprocessResultOfSymbolicReference(function.range,result,trace) |
330 | } | 338 | } |
331 | 339 | ||
332 | // TODO | 340 | // TODO |
333 | /* | 341 | /* |
334 | def dispatch protected VLSTerm transformSymbolicReference(Relation relation, | 342 | * def dispatch protected VLSTerm transformSymbolicReference(Relation relation, |
335 | List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace, | 343 | * List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace, |
336 | Map<Variable, VLSVariable> variables) { | 344 | * Map<Variable, VLSVariable> variables) { |
337 | if (trace.relationDefinitions.containsKey(relation)) { | 345 | * if (trace.relationDefinitions.containsKey(relation)) { |
338 | this.transformSymbolicReference(relation.lookup(trace.relationDefinitions), | 346 | * this.transformSymbolicReference(relation.lookup(trace.relationDefinitions), |
339 | parameterSubstitutions, trace, variables) | 347 | * parameterSubstitutions, trace, variables) |
340 | } | 348 | * } |
341 | else { | 349 | * else { |
342 | // if (relationMapper.transformToHostedField(relation, trace)) { | 350 | * // if (relationMapper.transformToHostedField(relation, trace)) { |
343 | // val VLSRelation = relation.lookup(trace.relationDeclaration2Field) | 351 | * // val VLSRelation = relation.lookup(trace.relationDeclaration2Field) |
344 | // // R(a,b) => | 352 | * // // R(a,b) => |
345 | // // b in a.R | 353 | * // // b in a.R |
346 | // return createVLSSubset => [ | 354 | * // return createVLSSubset => [ |
347 | // it.leftOperand = parameterSubstitutions.get(1).transformTerm(trace, variables) | 355 | * // it.leftOperand = parameterSubstitutions.get(1).transformTerm(trace, variables) |
348 | // it.rightOperand = createVLSJoin => [ | 356 | * // it.rightOperand = createVLSJoin => [ |
349 | // it.leftOperand = parameterSubstitutions.get(0).transformTerm(trace, variables) | 357 | * // it.leftOperand = parameterSubstitutions.get(0).transformTerm(trace, variables) |
350 | // it.rightOperand = createVLSReference => [it.referred = VLSRelation] | 358 | * // it.rightOperand = createVLSReference => [it.referred = VLSRelation] |
351 | // ] | 359 | * // ] |
352 | // ] | 360 | * // ] |
353 | // } else { | 361 | * // } else { |
354 | // val target = createVLSJoin => [ | 362 | * // val target = createVLSJoin => [ |
355 | // leftOperand = createVLSReference => [referred = trace.logicLanguage] | 363 | * // leftOperand = createVLSReference => [referred = trace.logicLanguage] |
356 | // rightOperand = createVLSReference => [ | 364 | * // rightOperand = createVLSReference => [ |
357 | // referred = relation.lookup(trace.relationDeclaration2Global) | 365 | * // referred = relation.lookup(trace.relationDeclaration2Global) |
358 | // ] | 366 | * // ] |
359 | // ] | 367 | * // ] |
360 | // val source = support.unfoldTermDirectProduct(this, parameterSubstitutions, trace, variables) | 368 | * // val source = support.unfoldTermDirectProduct(this, parameterSubstitutions, trace, variables) |
361 | // | 369 | * // |
362 | // return createVLSSubset => [ | 370 | * // return createVLSSubset => [ |
363 | // leftOperand = source | 371 | * // leftOperand = source |
364 | // rightOperand = target | 372 | * // rightOperand = target |
365 | // ] | 373 | * // ] |
366 | // } | 374 | * // } |
367 | } | 375 | * } |
368 | } | 376 | * } |
369 | */ | 377 | */ |
370 | 378 | // TODO | |
371 | // TODO | 379 | def dispatch protected VLSTerm transformSymbolicReference(Relation relation, List<Term> parameterSubstitutions, |
372 | def dispatch protected VLSTerm transformSymbolicReference(Relation relation, | 380 | Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables) { |
373 | List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace, | ||
374 | Map<Variable, VLSVariable> variables) { | ||
375 | // createVLSFunction => [ | 381 | // createVLSFunction => [ |
376 | // it.referredDefinition = relation.lookup(trace.relationDefinition2Predicate) | 382 | // it.referredDefinition = relation.lookup(trace.relationDefinition2Predicate) |
377 | // it.params += parameterSubstitutions.map[p|p.transformTerm(trace, variables)] | 383 | // it.params += parameterSubstitutions.map[p|p.transformTerm(trace, variables)] |
378 | // ] | 384 | // ] |
379 | return createVLSFunction => [ | 385 | return createVLSFunction => [ |
380 | it.constant = support.toIDMultiple("rel", relation.name) | 386 | it.constant = support.toIDMultiple("rel", relation.name) |
381 | it.terms += parameterSubstitutions.map[p | p.transformTerm(trace,variables)] | 387 | it.terms += parameterSubstitutions.map[p|p.transformTerm(trace, variables)] |
382 | ] | 388 | ] |
383 | } | 389 | } |
384 | 390 | ||
385 | } | 391 | } |
386 | \ No newline at end of file | ||