Containment root constraint propagator

4 files changed, 58 insertions, 43 deletions

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/GenericTypeRefinementGenerator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/GenericTypeRefinementGenerator.xtend
index 2e03d6ed..c9f6abce 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/GenericTypeRefinementGenerator.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/GenericTypeRefinementGenerator.xtend
@@ -11,7 +11,7 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.par
 import java.util.HashMap

 

 class GenericTypeRefinementGenerator extends TypeRefinementGenerator {

-        public new(PatternGenerator base) {

+        new(PatternGenerator base) {

                 super(base)

         }

         override requiresTypeAnalysis() { false }

@@ -25,7 +25,7 @@ class GenericTypeRefinementGenerator extends TypeRefinementGenerator {
                         inverseRelations.put(it.inverseB,it.inverseA)

                 ]

                 return '''

-                private pattern hasElementInContainment(problem:LogicProblem, interpretation:PartialInterpretation)

+                pattern «hasElementInContainmentName»(problem:LogicProblem, interpretation:PartialInterpretation)

                 «FOR type :containment.typesOrderedInHierarchy SEPARATOR "or"»{

                         find interpretation(problem,interpretation);

                         «base.typeIndexer.referInstanceOf(type,Modality.MUST,"root")»

@@ -77,7 +77,7 @@ class GenericTypeRefinementGenerator extends TypeRefinementGenerator {
                                         typeInterpretation:PartialComplexTypeInterpretation)

                                 {

                                         find interpretation(problem,interpretation);

-                                        neg find hasElementInContainment(problem,interpretation);

+                                        neg find  «hasElementInContainmentName»(problem,interpretation);

                                         PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation);

                                         PartialComplexTypeInterpretation.interpretationOf.name(type,"«type.name»");

                                         «base.typeIndexer.referInstanceOf(type,Modality.MAY,"newObject")»

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend
index 90f79810..b10c8e88 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend
@@ -12,6 +12,7 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysisResult
 import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeInferenceMethod

 import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.RelationConstraints

 import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.RelationMultiplicityConstraint

+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy

 import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.util.ParseUtil

 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation

 import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace

@@ -25,13 +26,13 @@ import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery
 import org.eclipse.xtend.lib.annotations.Data

 

 import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*

-import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy

 

 @Data

 class GeneratedPatterns {

         public Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidWFQueries

         public Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWFQueries

         public Map<RelationMultiplicityConstraint, UnifinishedMultiplicityQueries> multiplicityConstraintQueries

+        public IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> hasElementInContainmentQuery

         public Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedMulticiplicityQueries

         public Map<ObjectCreationPrecondition, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineObjectQueries

         public Map<? extends Type, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineTypeQueries

@@ -105,6 +106,8 @@ class PatternProvider {
                                 unrepairableMultiplicityQueryName?.lookup(queries),

                                 remainingInverseMultiplicityQueryName?.lookup(queries), remainingContentsQueryName?.lookup(queries))

                 ]

+                val hasElementInContainmentQuery = patternGenerator.typeRefinementGenerator.hasElementInContainmentName.lookup(

+                        queries)

                 val unfinishedMultiplicityQueries = multiplicityConstraintQueries.entrySet.filter [

                         value.unfinishedMultiplicityQuery !== null

                 ].toMap([key.relation], [value.unfinishedMultiplicityQuery])

@@ -126,6 +129,7 @@ class PatternProvider {
                         invalidWFQueries,

                         unfinishedWFQueries,

                         multiplicityConstraintQueries,

+                        hasElementInContainmentQuery,

                         unfinishedMultiplicityQueries,

                         refineObjectsQueries,

                         refineTypeQueries,

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeRefinementGenerator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeRefinementGenerator.xtend
index ee7299cd..4ef336ae 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeRefinementGenerator.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeRefinementGenerator.xtend
@@ -25,69 +25,76 @@ class ObjectCreationPrecondition {
 

 abstract class TypeRefinementGenerator {

         val protected PatternGenerator base;

-        public new(PatternGenerator base) {

+

+        new(PatternGenerator base) {

                 this.base = base

         }

-        

-        public def boolean requiresTypeAnalysis()

-        public def CharSequence generateRefineObjectQueries(LogicProblem p, PartialInterpretation emptySolution, TypeAnalysisResult typeAnalysisResult)

-        public def CharSequence generateRefineTypeQueries(LogicProblem p, PartialInterpretation emptySolution, TypeAnalysisResult typeAnalysisResult)

-        public def Map<? extends Type, String> getRefineTypeQueryNames(LogicProblem p, PartialInterpretation emptySolution, TypeAnalysisResult typeAnalysisResult)

-        

-        public def getRefineObjectQueryNames(LogicProblem p, PartialInterpretation emptySolution, TypeAnalysisResult typeAnalysisResult) {

-                val Map<ObjectCreationPrecondition,String> objectCreationQueries = new LinkedHashMap

+

+        def boolean requiresTypeAnalysis()

+

+        def CharSequence generateRefineObjectQueries(LogicProblem p, PartialInterpretation emptySolution,

+                TypeAnalysisResult typeAnalysisResult)

+

+        def CharSequence generateRefineTypeQueries(LogicProblem p, PartialInterpretation emptySolution,

+                TypeAnalysisResult typeAnalysisResult)

+

+        def Map<? extends Type, String> getRefineTypeQueryNames(LogicProblem p, PartialInterpretation emptySolution,

+                TypeAnalysisResult typeAnalysisResult)

+

+        def getRefineObjectQueryNames(LogicProblem p, PartialInterpretation emptySolution,

+                TypeAnalysisResult typeAnalysisResult) {

+                val Map<ObjectCreationPrecondition, String> objectCreationQueries = new LinkedHashMap

                 val containment = p.containmentHierarchies.head

                 val inverseRelations = new HashMap

-                p.annotations.filter(InverseRelationAssertion).forEach[

-                        inverseRelations.put(it.inverseA,it.inverseB)

-                        inverseRelations.put(it.inverseB,it.inverseA)

+                p.annotations.filter(InverseRelationAssertion).forEach [

+                        inverseRelations.put(it.inverseA, it.inverseB)

+                        inverseRelations.put(it.inverseB, it.inverseA)

                 ]

-                for(type: p.types.filter(TypeDeclaration).filter[!it.isAbstract]) {

-                        if(containment.typeInContainment(type)) {

-                                for(containmentRelation : containment.containmentRelations.filter[canBeContainedByRelation(it,type)]) {

-                                        if(inverseRelations.containsKey(containmentRelation)) {

+                for (type : p.types.filter(TypeDeclaration).filter[!it.isAbstract]) {

+                        if (containment.typeInContainment(type)) {

+                                for (containmentRelation : containment.containmentRelations.

+                                        filter[canBeContainedByRelation(it, type)]) {

+                                        if (inverseRelations.containsKey(containmentRelation)) {

                                                 objectCreationQueries.put(

-                                                        new ObjectCreationPrecondition(containmentRelation,inverseRelations.get(containmentRelation),type),

-                                                        this.patternName(containmentRelation,inverseRelations.get(containmentRelation),type))

+                                                        new ObjectCreationPrecondition(containmentRelation,

+                                                                inverseRelations.get(containmentRelation), type),

+                                                        this.patternName(containmentRelation, inverseRelations.get(containmentRelation), type))

                                         } else {

-                                                objectCreationQueries.put(

-                                                        new ObjectCreationPrecondition(containmentRelation,null,type),

-                                                        patternName(containmentRelation,null,type))

+                                                objectCreationQueries.put(new ObjectCreationPrecondition(containmentRelation, null, type),

+                                                        patternName(containmentRelation, null, type))

                                         }

                                 }

-                                objectCreationQueries.put(

-                                        new ObjectCreationPrecondition(null,null,type),

-                                        patternName(null,null,type))

+                                objectCreationQueries.put(new ObjectCreationPrecondition(null, null, type),

+                                        patternName(null, null, type))

                         } else {

-                                objectCreationQueries.put(

-                                        new ObjectCreationPrecondition(null,null,type),

-                                        this.patternName(null,null,type))

+                                objectCreationQueries.put(new ObjectCreationPrecondition(null, null, type),

+                                        this.patternName(null, null, type))

                         }

                 }

                 return objectCreationQueries

         }

-        

+

         protected def canBeContainedByRelation(Relation r, Type t) {

-                if(r.parameters.size==2) {

+                if (r.parameters.size == 2) {

                         val param = r.parameters.get(1)

-                        if(param instanceof ComplexTypeReference) {

+                        if (param instanceof ComplexTypeReference) {

                                 val allSuperTypes = t.transitiveClosureStar[it.supertypes]

-                                for(superType : allSuperTypes) {

+                                for (superType : allSuperTypes) {

                                         if(param.referred == superType) return true

                                 }

                         }

                 }

                 return false

         }

-        

+

         private def typeInContainment(ContainmentHierarchy hierarchy, Type type) {

                 val allSuperTypes = type.transitiveClosureStar[it.supertypes]

                 return allSuperTypes.exists[hierarchy.typesOrderedInHierarchy.contains(it)]

         }

-        

+

         protected def String patternName(Relation containmentRelation, Relation inverseContainment, Type newType) {

-                if(containmentRelation !== null) {

-                        if(inverseContainment !== null) {

+                if (containmentRelation !== null) {

+                        if (inverseContainment !== null) {

                                 '''createObject_«base.canonizeName(newType.name)»_by_«base.canonizeName(containmentRelation.name)»_with_«base.canonizeName(inverseContainment.name)»'''

                         } else {

                                 '''createObject_«base.canonizeName(newType.name)»_by_«base.canonizeName(containmentRelation.name)»'''

@@ -96,4 +103,8 @@ abstract class TypeRefinementGenerator {
                         '''createObject_«base.canonizeName(newType.name)»'''

                 }

         }

-}
\ No newline at end of file
+

+        def hasElementInContainmentName() {

+                "hasElementInContainment"

+        }

+}

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeRefinementWithPreliminaryTypeAnalysis.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeRefinementWithPreliminaryTypeAnalysis.xtend
index cbbbcb08..1a81695e 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeRefinementWithPreliminaryTypeAnalysis.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeRefinementWithPreliminaryTypeAnalysis.xtend
@@ -10,7 +10,7 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.par
 import java.util.HashMap

 

 class TypeRefinementWithPreliminaryTypeAnalysis extends TypeRefinementGenerator{

-        public new(PatternGenerator base) {

+        new(PatternGenerator base) {

                 super(base)

         }

         override requiresTypeAnalysis() { true }

@@ -24,7 +24,7 @@ class TypeRefinementWithPreliminaryTypeAnalysis extends TypeRefinementGenerator{
                         inverseRelations.put(it.inverseB,it.inverseA)

                 ]

                 return '''

-                private pattern hasElementInContainment(problem:LogicProblem, interpretation:PartialInterpretation)

+                pattern «hasElementInContainmentName»(problem:LogicProblem, interpretation:PartialInterpretation)

                 «FOR type :containment.typesOrderedInHierarchy SEPARATOR "or"»{

                         find interpretation(problem,interpretation);

                         «base.typeIndexer.referInstanceOf(type,Modality.MUST,"root")»

@@ -76,7 +76,7 @@ class TypeRefinementWithPreliminaryTypeAnalysis extends TypeRefinementGenerator{
                                         typeInterpretation:PartialComplexTypeInterpretation)

                                 {

                                         find interpretation(problem,interpretation);

-                                        neg find hasElementInContainment(problem,interpretation);

+                                        neg find «hasElementInContainmentName»(problem,interpretation);

                                         PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation);

                                         PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"«type.name»");

                                         «base.typeIndexer.referInstanceOf(type,Modality.MAY,"newObject")»