From a143c9f7a5b9da04dc0617705119841c24e3fc41 Mon Sep 17 00:00:00 2001 From: oszka Date: Tue, 16 Apr 2019 10:28:25 +0200 Subject: Fixed misformalization of (may/must)(X!=Y) for abstract objects --- .../viatrasolver/logic2viatra/patterns/PatternGenerator.xtend | 5 +++++ .../logic2viatra/patterns/RelationDefinitionIndexer.xtend | 8 ++++---- 2 files changed, 9 insertions(+), 4 deletions(-) diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend index a2b11632..d4c76bb4 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend @@ -203,6 +203,11 @@ class PatternGenerator { find mayExist(problem,interpretation,b); a == b; } + pattern mustEquivalent(problem:LogicProblem, interpretation:PartialInterpretation, a: DefinedElement, b: DefinedElement) { + find mustExist(problem,interpretation,a); + find mustExist(problem,interpretation,b); + a == b; + } //////////////////////// // 0.3 Required Patterns by TypeIndexer diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDefinitionIndexer.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDefinitionIndexer.xtend index 329d3658..9723373f 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDefinitionIndexer.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDefinitionIndexer.xtend @@ -179,7 +179,7 @@ class RelationDefinitionIndexer { } private def CharSequence transformEquality(Modality modality, PVariable a, PVariable b) { - if(modality.isMustOrCurrent) '''«a.canonizeName» == «b.canonizeName»;''' + if(modality.isMustOrCurrent) '''find mustEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);''' else '''find mayEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);''' } @@ -187,11 +187,11 @@ class RelationDefinitionIndexer { val a = inequality.who val b = inequality.withWhom if(modality.isCurrent) { - return '''«a.canonizeName» != «b.canonizeName»;''' + return '''neg find mustEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);''' } else if(modality.isMust) { return '''neg find mayEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);''' - } else { - return '''«a.canonizeName» != «b.canonizeName»;''' + } else { // modality.isMay + return '''neg find mustEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);''' } } -- cgit v1.2.3-54-g00ecf