Fixed misformalization of (may/must)(X!=Y) for abstract objects

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»);'''

                 }

         }