Viatra Solver support for tasks with no partial model

3 files changed, 47 insertions, 8 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 4b7af959..1081fafc 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
@@ -25,6 +25,12 @@ class GenericTypeRefinementGenerator extends TypeRefinementGenerator {
                         inverseRelations.put(it.inverseB,it.inverseA)

                 ]

                 return '''

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

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

+                        find interpretation(problem,interpretation);

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

+                        find mustExist(problem, interpretation, root);

+                }«ENDFOR»

                 «FOR type:newObjectTypes»

                         «IF(containment.typesOrderedInHierarchy.contains(type))»

                                 «FOR containmentRelation : containment.containmentRelations.filter[canBeContainedByRelation(it,type)]»

@@ -66,6 +72,18 @@ class GenericTypeRefinementGenerator extends TypeRefinementGenerator {
                                                 }

                                         «ENDIF»

                                 «ENDFOR»

+                                pattern «patternName(null,null,type)»(

+                                        problem:LogicProblem, interpretation:PartialInterpretation,

+                                        typeInterpretation:PartialTypeInterpratation)

+                                {

+                                        find interpretation(problem,interpretation);

+                                        neg find hasElementInContainment(problem,interpretation);

+                                        PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation);

+                                        PartialTypeInterpratation.interpretationOf.name(type,"«type.name»");

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

+                                        find mayExist(problem, interpretation, newObject);

+                                        neg find mustExist(problem, interpretation, newObject);

+                                }

                         «ELSE»

                                 pattern createObject_«this.patternName(null,null,type)»(

                                         problem:LogicProblem, interpretation:PartialInterpretation,

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 a9ce9d73..7e3fad91 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
@@ -1,19 +1,20 @@
 package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns

 

+import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.InverseRelationAssertion

+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference

 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation

 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type

+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration

+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy

 import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem

 import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysisResult

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

-import java.util.Map

-import org.eclipse.xtend.lib.annotations.Data

 import java.util.HashMap

-import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.InverseRelationAssertion

-import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration

-import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference

 import java.util.LinkedHashMap

+import java.util.Map

+import org.eclipse.xtend.lib.annotations.Data

+

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

-import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy

 

 @Data

 class ObjectCreationPrecondition {

@@ -54,6 +55,9 @@ abstract class TypeRefinementGenerator {
                                                         patternName(containmentRelation,null,type))

                                         }

                                 }

+                                objectCreationQueries.put(

+                                        new ObjectCreationPrecondition(null,null,type),

+                                        patternName(null,null,type))

                         } else {

                                 objectCreationQueries.put(

                                         new ObjectCreationPrecondition(null,null,type),

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 be54d63c..81f2f7db 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
@@ -15,7 +15,6 @@ class TypeRefinementWithPreliminaryTypeAnalysis extends TypeRefinementGenerator{
         }

         override requiresTypeAnalysis() { true }

 

-        

         override generateRefineObjectQueries(LogicProblem p, PartialInterpretation emptySolution, TypeAnalysisResult typeAnalysisResult) {

                 val possibleNewDynamicType = typeAnalysisResult.possibleNewDynamicTypes

                 val containment = p.containmentHierarchies.head

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

                 ]

                 return '''

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

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

+                        find interpretation(problem,interpretation);

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

+                        find mustExist(problem, interpretation, root);

+                }«ENDFOR»

                 «FOR type:possibleNewDynamicType»

                         «IF(containment.typesOrderedInHierarchy.contains(type))»

                                 «FOR containmentRelation : containment.containmentRelations.filter[canBeContainedByRelation(it,type)]»

@@ -66,8 +71,20 @@ class TypeRefinementWithPreliminaryTypeAnalysis extends TypeRefinementGenerator{
                                                 }

                                         «ENDIF»

                                 «ENDFOR»

+                                pattern «patternName(null,null,type)»(

+                                        problem:LogicProblem, interpretation:PartialInterpretation,

+                                        typeInterpretation:PartialTypeInterpratation)

+                                {

+                                        find interpretation(problem,interpretation);

+                                        neg find hasElementInContainment(problem,interpretation);

+                                        PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation);

+                                        PartialTypeInterpratation.interpretationOf.name(type,"«type.name»");

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

+                                        find mayExist(problem, interpretation, newObject);

+                                        neg find mustExist(problem, interpretation, newObject);

+                                }

                         «ELSE»

-                                pattern createObject_«base.canonizeName(type.name)»(

+                                pattern «this.patternName(null,null,type)»(

                                         problem:LogicProblem, interpretation:PartialInterpretation,

                                         typeInterpretation:PartialTypeInterpratation)

                                 {