Merge remote-tracking branch 'origin/master' into kris

3 files changed, 11 insertions, 5 deletions

diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/META-INF/MANIFEST.MF b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/META-INF/MANIFEST.MF
index 1fda4212..8fa4517d 100644
--- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/META-INF/MANIFEST.MF
+++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/META-INF/MANIFEST.MF
@@ -17,7 +17,8 @@ Require-Bundle: com.google.guava,
  org.eclipse.emf.ecore;visibility:=reexport,

  hu.bme.mit.inf.dslreasoner.logic.model;bundle-version="1.0.0";visibility:=reexport,

  org.eclipse.viatra.query.runtime.base.itc;bundle-version="1.5.0",

- org.eclipse.viatra.query.patternlanguage.emf;bundle-version="2.0.0"

+ org.eclipse.viatra.query.patternlanguage.emf;bundle-version="2.0.0",

+ org.eclipse.xtext

 Bundle-ActivationPolicy: lazy

 Export-Package: hu.bme.mit.inf.dslreasoner.viatra2logic,

  hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations,

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 c9e64a9d..24b3e870 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 a67a24c4..cedcec5a 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»);'''

                 }

         }