3 files changed, 47 insertions, 0 deletions

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/GenericTypeIndexer.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/GenericTypeIndexer.xtend
index d11b5960..d6a15c1a 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/GenericTypeIndexer.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/GenericTypeIndexer.xtend
@@ -155,6 +155,11 @@ class GenericTypeIndexer extends TypeIndexer {
                 find supertypeStar(type,definedSupertype);

                 TypeDefinition(definedSupertype);

         }

+        

+        private pattern scopeDisallowsNewElementsFromType(typeInterpretation:PartialComplexTypeInterpretation) {

+                Scope.targetTypeInterpretation(scope,typeInterpretation);

+                Scope.maxNewElements(scope,0);

+        }

         '''

         

         public override generateInstanceOfQueries(LogicProblem problem, PartialInterpretation emptySolution,TypeAnalysisResult typeAnalysisResult) {

@@ -190,6 +195,7 @@ class GenericTypeIndexer extends TypeIndexer {
                         Type.name(type,"«type.name»");

                         find possibleDynamicType(problem,interpretation,dynamic,element);

                         find supertypeStar(dynamic,type);

+                        neg find scopeDisallowsNewElementsFromType(dynamic);

                 }

                 '''

         }

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 39b6fbc0..329d3658 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
@@ -24,6 +24,7 @@ import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.TypeCo
 import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery

 

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

+import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.TypeFilterConstraint

 

 class RelationDefinitionIndexer {

         val PatternGenerator base;

@@ -141,6 +142,35 @@ class RelationDefinitionIndexer {
                         throw new UnsupportedOperationException('''Unsupported touple size: «touple.size»''')

                 }

         }

+        private dispatch def transformConstraint(TypeFilterConstraint constraint, Modality modality) {

+                val touple = constraint.variablesTuple

+                if(touple.size == 1) {

+                        val inputKey = constraint.equivalentJudgement.inputKey

+                        if(inputKey instanceof EClassTransitiveInstancesKey) {

+                                return base.typeIndexer.referInstanceOf(inputKey.emfKey,modality.toMustMay,

+                                        (constraint.getVariablesTuple.get(0) as PVariable).canonizeName)

+                        } else if(inputKey instanceof EDataTypeInSlotsKey){

+                                return '''// type constraint is enforced by construction'''

+                        }

+                        

+                } else if(touple.size == 2){

+                        val key = (constraint.equivalentJudgement.inputKey as EStructuralFeatureInstancesKey).emfKey

+                        if(key instanceof EReference) {

+                                return base.referRelationByName(

+                                        key,

+                                        (constraint.getVariablesTuple.get(0) as PVariable).canonizeName,

+                                        (constraint.getVariablesTuple.get(1) as PVariable).canonizeName,

+                                        modality.toMustMay)

+                        } else if (key instanceof EAttribute) {

+                                return base.referAttributeByName(key,

+                                        (constraint.getVariablesTuple.get(0) as PVariable).canonizeName,

+                                        (constraint.getVariablesTuple.get(1) as PVariable).canonizeName,

+                                        modality.toMustMay)

+                        } else throw new UnsupportedOperationException('''unknown key: «key.class»''')

+                } else {

+                        throw new UnsupportedOperationException('''Unsupported touple size: «touple.size»''')

+                }

+        }

         

         private dispatch def transformConstraint(Equality equality, Modality modality) {

                 val a = equality.who

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeIndexerWithPreliminaryTypeAnalysis.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeIndexerWithPreliminaryTypeAnalysis.xtend
index 67a886d1..d3af0426 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeIndexerWithPreliminaryTypeAnalysis.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeIndexerWithPreliminaryTypeAnalysis.xtend
@@ -72,6 +72,15 @@ class TypeIndexerWithPreliminaryTypeAnalysis extends TypeIndexer{
                         null

                 }

                 '''

+                private pattern scopeDisallowsNew«base.canonizeName(type.name)»(problem:LogicProblem, interpretation:PartialInterpretation) {

+                        find interpretation(problem,interpretation);

+                        PartialInterpretation.scopes(interpretation,scope);

+                        Scope.targetTypeInterpretation(scope,typeInterpretation);

+                        Scope.maxNewElements(scope,0);

+                        PartialComplexTypeInterpretation.interpretationOf(typeInterpretation,type);

+                        Type.name(type,"«type.name»");

+                }

+                

                 /**

                  * An element may be an instance of type "«type.name»".

                  */

@@ -82,6 +91,7 @@ class TypeIndexerWithPreliminaryTypeAnalysis extends TypeIndexer{
                         «FOR inhibitorType : inhibitorTypes»

                                 neg «referInstanceOf(inhibitorType,Modality.MUST,"element")»

                         «ENDFOR»

+                        neg find scopeDisallowsNew«base.canonizeName(type.name)»(problem, interpretation);

                         neg find isPrimitive(element);

                 } or {

                         find interpretation(problem,interpretation);

@@ -89,6 +99,7 @@ class TypeIndexerWithPreliminaryTypeAnalysis extends TypeIndexer{
                         «FOR inhibitorType : inhibitorTypes»

                                 neg «referInstanceOf(inhibitorType,Modality.MUST,"element")»

                         «ENDFOR»

+                        neg find scopeDisallowsNew«base.canonizeName(type.name)»(problem, interpretation);

                         neg find isPrimitive(element);

                 } or

                 «ENDIF»