UP patterns -> decision procedure trace finished

4 files changed, 59 insertions, 14 deletions

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 56138ee8..d5ebe318 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
@@ -155,8 +155,8 @@ class PatternGenerator {
                 Map<String,PQuery> fqn2PQuery,

                 TypeAnalysisResult typeAnalysisResult

         ) {

-                

-                return '''

+                val first = 

+                 '''

                         import epackage "http://www.bme.hu/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage"

                         import epackage "http://www.bme.hu/mit/inf/dslreasoner/logic/model/problem"

                         import epackage "http://www.bme.hu/mit/inf/dslreasoner/logic/model/language"

@@ -395,7 +395,9 @@ class PatternGenerator {
                         //////////

                         // 5 Unit Propagations

                         //////////

-                        «unitPropagationPreconditionGenerator.generateUnitPropagationRules(problem,problem.relations.filter(RelationDefinition),fqn2PQuery)»

                         '''

+                        val up = unitPropagationPreconditionGenerator.generateUnitPropagationRules(problem,problem.relations.filter(RelationDefinition),fqn2PQuery)

+                        val second = up.definitions

+                        return (first+second) -> up.constraint2PreconditionName

         }

 }

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 0e13a5e1..f576d1a1 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
@@ -21,6 +21,8 @@ import org.eclipse.xtend.lib.annotations.Data
 import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*

 import java.util.Collection

 import java.util.Set

+import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint

+import java.util.HashMap

 

 @Data class GeneratedPatterns {

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

@@ -29,6 +31,7 @@ import java.util.Set
         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<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>>  unitPropagationPreconditionPatterns

         public Collection<IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allQueries

 }

 

@@ -56,13 +59,15 @@ class PatternProvider {
                 } else {

                         null

                 }

-                val baseIndexerFile = patternGenerator.transformBaseProperties(problem,emptySolution,fqn2Query,typeAnalysisResult)

+                val patternGeneratorResult = patternGenerator.transformBaseProperties(problem,emptySolution,fqn2Query,typeAnalysisResult)

+                val baseIndexerFile = patternGeneratorResult.key

+                val unitPropagationTrace = patternGeneratorResult.value

                 if(writeToFile) {

                         workspace.writeText('''generated3valued.vql_deactivated''',baseIndexerFile)

                 }

                 val ParseUtil parseUtil = new ParseUtil

                 val generatedQueries = parseUtil.parse(baseIndexerFile)

-                val runtimeQueries = calclulateRuntimeQueries(patternGenerator,problem,emptySolution,typeAnalysisResult,generatedQueries);

+                val runtimeQueries = calclulateRuntimeQueries(patternGenerator,problem,emptySolution,typeAnalysisResult,unitPropagationTrace,generatedQueries);

                 return runtimeQueries

         }

         

@@ -71,7 +76,8 @@ class PatternProvider {
                 LogicProblem problem,

                 PartialInterpretation emptySolution,

                 TypeAnalysisResult typeAnalysisResult,

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

+                HashMap<PConstraint, String> unitPropagationTrace,

+                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)]

@@ -85,6 +91,9 @@ class PatternProvider {
                         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>>> 

+                        unitPropagationPreconditionPatterns = unitPropagationTrace.mapValues[it.lookup(queries)]

+                unitPropagationPreconditionPatterns.entrySet.forEach[println(it.key + "->" +it.value)]

                 return new GeneratedPatterns(

                         invalidWFQueries,

                         unfinishedWFQueries,

@@ -92,6 +101,7 @@ class PatternProvider {
                         refineObjectsQueries,

                         refineTypeQueries,

                         refineRelationQueries,

+                        unitPropagationPreconditionPatterns,

                         queries.values

                 )

         }

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnitPropagationPreconditionGenerator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnitPropagationPreconditionGenerator.xtend
index b5e344f7..7cf52b41 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnitPropagationPreconditionGenerator.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnitPropagationPreconditionGenerator.xtend
@@ -58,6 +58,11 @@ class UnitPropagationPreconditionGenerationResult {
                 return unitPropagation2PatternName.get(key) !== null

         }

 }

+@Data

+class UnitPropagationPreconditionFinalResult {

+        CharSequence definitions

+        HashMap<PConstraint,String> constraint2PreconditionName

+}

 

 class UnitPropagationPreconditionGenerator {

         val PatternGenerator base

@@ -76,23 +81,51 @@ class UnitPropagationPreconditionGenerator {
                 // Create an empty result

                 val res = new UnitPropagationPreconditionGenerationResult               

                 val wfs = base.wfQueries(problem)//.map[it.patternPQuery]

-                val mainPropagationNames = new LinkedHashSet

+                val Map<PConstraint,List<Pair<String,Integer>>> mainPropagationNames = new HashMap

                 for(wf : wfs) {

                         val query = wf.patternPQuery as PQuery

                         val relation = wf.target

                         val allReferredChecks = allReferredConstraints(relation,query).filter(ExpressionEvaluation)

                         

                         for(referredCheck : allReferredChecks) {

-                                mainPropagationNames+= getOrGeneratePropagationRule(res,relation,query,referredCheck,PropagationModality::UP, Modality::MUST)

+                                val propagationPrecondition = getOrGeneratePropagationRule(res,relation,query,referredCheck,PropagationModality::UP, Modality::MUST)

+                                if(!mainPropagationNames.containsKey(referredCheck)) {

+                                        mainPropagationNames.put(referredCheck,new LinkedList)

+                                }

+                                if(propagationPrecondition !== null) {

+                                        println(query.parameterNames)

+                                        println(query.parameterNames.size)

+                                        mainPropagationNames.get(referredCheck).add(propagationPrecondition->query.parameterNames.size)

+                                }

                         }

                 }

-                return '''

+                val preconditions = new LinkedList

+                val constraint2Precondition = new HashMap

+                for(entry : mainPropagationNames.entrySet) {

+                        val name = '''UPMUSTPropagate«res.getOrGenerateConstraintName(entry.key)»''';

+                        val def = '''

+                        pattern «name»(

+                                problem:LogicProblem, interpretation:PartialInterpretation,

+                                «FOR index : 1..entry.key.arity SEPARATOR ", "»«canonizeName(index,PropagationModality::UP)»«ENDFOR»)

+                                «FOR propagation : entry.value SEPARATOR " or "»

+                                        { find «propagation.key»(problem,interpretation,«FOR index : 0..<propagation.value SEPARATOR ','»_«ENDFOR»,«FOR index : 1..entry.key.arity SEPARATOR ", "»«canonizeName(index,PropagationModality::UP)»«ENDFOR»); }

+                                «ENDFOR»'''

+                        preconditions+=def

+                        constraint2Precondition.put(entry.key,name)

+                }

+                

+                val definitions = '''

                         «FOR def : res.definitions»

                                 «def»

                         «ENDFOR»

                         

-                        // Main propagations: «FOR name : mainPropagationNames SEPARATOR ", "»«name»«ENDFOR»

+                        // Collected propagation preconditions:

+                        

+                        «FOR predondition : preconditions»

+                                «predondition»

+                        «ENDFOR»

                 '''

+                return new UnitPropagationPreconditionFinalResult(definitions,constraint2Precondition)

         }

         def allReferredConstraints(Relation relation, PQuery query) {

                 val allReferredQueries = query.allReferredQueries

@@ -207,7 +240,7 @@ class UnitPropagationPreconditionGenerator {
                         res.registerUnsatQuery(q,c,pm,m3)

                 } else {

                         val definition = '''

-                                pattern «name»(

+                                private pattern «name»(

                                         problem:LogicProblem, interpretation:PartialInterpretation,

                                         «FOR param :  q.parameters SEPARATOR ', '»var_«param.name»«ENDFOR»,

                                         «FOR arity : 1..constraintArity SEPARATOR ', '»«canonizeName(arity,pm)»«ENDFOR»)

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend
index 7e53f944..db0e17b9 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend
@@ -90,7 +90,7 @@ class RefinementRuleProvider {
                 if(containmentRelation !== null) {

                         if(inverseRelation!== null) {

                                 ruleBuilder.action[match |

-                                        println(name)

+                                        //println(name)

                                         val startTime = System.nanoTime

                                         //val problem = match.get(0) as LogicProblem

                                         val interpretation = match.get(1) as PartialInterpretation

@@ -115,7 +115,7 @@ class RefinementRuleProvider {
                                 ]

                         } else {

                                 ruleBuilder.action[match |

-                                        println(name)

+                                        //println(name)

                                         val startTime = System.nanoTime

                                         //val problem = match.get(0) as LogicProblem

                                         val interpretation = match.get(1) as PartialInterpretation

@@ -139,7 +139,7 @@ class RefinementRuleProvider {
                         }

                 } else {

                         ruleBuilder.action[match |

-                                println(name)

+                                //println(name)

                                 val startTime = System.nanoTime

                                 //val problem = match.get(0) as LogicProblem

                                 val interpretation = match.get(1) as PartialInterpretation