MoDeS3 unit propagation WIP

1 files changed, 31 insertions, 25 deletions

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 d57705ce..21fd1989 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
@@ -36,9 +36,9 @@ import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
         public Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWFQueries

         public Map<RelationMultiplicityConstraint, UnifinishedMultiplicityQueries> multiplicityConstraintQueries

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

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

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

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

-        public Map<Pair<RelationDeclaration, Relation>,  IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refinerelationQueries

+        public Map<Pair<RelationDeclaration, Relation>, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refinerelationQueries

         public Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> mustUnitPropagationPreconditionPatterns

         public Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> currentUnitPropagationPreconditionPatterns

         public Map<RelationDefinition, ModalPatternQueries> modalRelationQueries

@@ -56,7 +56,7 @@ class ModalPatternQueries {
 class UnifinishedMultiplicityQueries {

         val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> existingMultiplicityQuery

         val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> existingInverseMultiplicityQuery

-        

+

         def Set<IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> getAllQueries() {

                 val builder = ImmutableSet.builder

                 if (existingMultiplicityQuery !== null) {

@@ -75,8 +75,9 @@ class PatternProvider {
 

         def generateQueries(LogicProblem problem, PartialInterpretation emptySolution, ModelGenerationStatistics statistics,

                 Set<PQuery> existingQueries, ReasonerWorkspace workspace, TypeInferenceMethod typeInferenceMethod,

-                ScopePropagatorStrategy scopePropagatorStrategy, RelationConstraints relationConstraints, 

-                Collection<LinearTypeConstraintHint> hints, boolean writeToFile) {

+                ScopePropagatorStrategy scopePropagatorStrategy, RelationConstraints relationConstraints,

+                Collection<LinearTypeConstraintHint> hints,

+                Collection<UnitPropagationPatternGenerator> unitPropagationPatternGenerators, boolean writeToFile) {

                 val fqn2Query = existingQueries.toMap[it.fullyQualifiedName]

                 val PatternGenerator patternGenerator = new PatternGenerator(typeInferenceMethod, scopePropagatorStrategy)

                 val typeAnalysisResult = if (patternGenerator.requiresTypeAnalysis) {

@@ -89,15 +90,15 @@ class PatternProvider {
                                 null

                         }

                 val patternGeneratorResult = patternGenerator.transformBaseProperties(problem, emptySolution, fqn2Query,

-                        typeAnalysisResult, relationConstraints, hints)

+                        typeAnalysisResult, relationConstraints, hints, unitPropagationPatternGenerators)

                 if (writeToFile) {

                         workspace.writeText('''generated3valued.vql_deactivated''', patternGeneratorResult.patternText)

                 }

                 val ParseUtil parseUtil = new ParseUtil

                 val generatedQueries = parseUtil.parse(patternGeneratorResult.patternText)

                 val runtimeQueries = calclulateRuntimeQueries(patternGenerator, problem, emptySolution, typeAnalysisResult,

-                        patternGeneratorResult.constraint2MustPreconditionName, patternGeneratorResult.constraint2CurrentPreconditionName,

-                        relationConstraints, generatedQueries)

+                        patternGeneratorResult.constraint2MustPreconditionName,

+                        patternGeneratorResult.constraint2CurrentPreconditionName, relationConstraints, generatedQueries)

                 return runtimeQueries

         }

 

@@ -111,12 +112,13 @@ class PatternProvider {
                 RelationConstraints relationConstraints,

                 Map<String, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> queries

         ) {

-                val Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>>

-                        invalidWFQueries = patternGenerator.invalidIndexer.getInvalidateByWfQueryNames(problem).mapValues[it.lookup(queries)]

-                val Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>>

-                        unfinishedWFQueries = patternGenerator.unfinishedIndexer.getUnfinishedWFQueryNames(problem).mapValues[it.lookup(queries)]

-                        

-                val unfinishedMultiplicities = patternGenerator.unfinishedIndexer.getUnfinishedMultiplicityQueries(relationConstraints.multiplicityConstraints)

+                val Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidWFQueries = patternGenerator.

+                        invalidIndexer.getInvalidateByWfQueryNames(problem).mapValues[it.lookup(queries)]

+                val Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWFQueries = patternGenerator.

+                        unfinishedIndexer.getUnfinishedWFQueryNames(problem).mapValues[it.lookup(queries)]

+

+                val unfinishedMultiplicities = patternGenerator.unfinishedIndexer.getUnfinishedMultiplicityQueries(

+                        relationConstraints.multiplicityConstraints)

                 val multiplicityConstraintQueries = unfinishedMultiplicities.mapValues [

                         new UnifinishedMultiplicityQueries(existingMultiplicityQueryName?.lookup(queries),

                                 existingInverseMultiplicityQueryName?.lookup(queries))

@@ -124,16 +126,20 @@ class PatternProvider {
                 val hasElementInContainmentQuery = patternGenerator.typeRefinementGenerator.hasElementInContainmentName.lookup(

                         queries)

 

-                val Map<ObjectCreationPrecondition,  IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>>

-                        refineObjectsQueries = patternGenerator.typeRefinementGenerator.getRefineObjectQueryNames(problem,emptySolution,typeAnalysisResult).mapValues[it.lookup(queries)]

-                val Map<? extends Type,  IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>>

-                        refineTypeQueries = patternGenerator.typeRefinementGenerator.getRefineTypeQueryNames(problem,emptySolution,typeAnalysisResult).mapValues[it.lookup(queries)]

-                val Map<Pair<RelationDeclaration, Relation>,  IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>>

-                        refineRelationQueries = patternGenerator.relationRefinementGenerator.getRefineRelationQueries(problem).mapValues[it.lookup(queries)]

-                val Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> 

-                        mustUnitPropagationPreconditionPatterns = mustUnitPropagationTrace.mapValues[it.lookup(queries)]

-                val Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> 

-                        currentUnitPropagationPreconditionPatterns = currentUnitPropagationTrace.mapValues[it.lookup(queries)]

+                val Map<ObjectCreationPrecondition, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineObjectsQueries = patternGenerator.

+                        typeRefinementGenerator.getRefineObjectQueryNames(problem, emptySolution, typeAnalysisResult).mapValues [

+                                it.lookup(queries)

+                        ]

+                val Map<? extends Type, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineTypeQueries = patternGenerator.

+                        typeRefinementGenerator.getRefineTypeQueryNames(problem, emptySolution, typeAnalysisResult).mapValues [

+                                it.lookup(queries)

+                        ]

+                val Map<Pair<RelationDeclaration, Relation>, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineRelationQueries = patternGenerator.

+                        relationRefinementGenerator.getRefineRelationQueries(problem).mapValues[it.lookup(queries)]

+                val Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> mustUnitPropagationPreconditionPatterns = mustUnitPropagationTrace.

+                        mapValues[it.lookup(queries)]

+                val Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> currentUnitPropagationPreconditionPatterns = currentUnitPropagationTrace.

+                        mapValues[it.lookup(queries)]

 

                 val modalRelationQueries = problem.relations.filter(RelationDefinition).toMap([it], [ relationDefinition |

                         val indexer = patternGenerator.relationDefinitionIndexer

@@ -143,7 +149,7 @@ class PatternProvider {
                                 indexer.relationDefinitionName(relationDefinition, Modality.CURRENT).lookup(queries)

                         )

                 ])

-                

+

                 return new GeneratedPatterns(

                         invalidWFQueries,

                         unfinishedWFQueries,