separated must and current UP rules to support non-prop neg finds

4 files changed, 60 insertions, 23 deletions

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend
index 975ace2f..be11ed78 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend
@@ -38,7 +38,8 @@ class ModelGenerationStatistics {
          

          Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidWF

          

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

+         Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> mustUnitPropagationPreconditions

+         Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> currentUnitPropagationPreconditions

          

          Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allPatterns

 }

@@ -81,7 +82,8 @@ class ModelGenerationMethodProvider {
                 

                 val invalidWF = queries.getInvalidWFQueries.values

                 

-                val unitPropagationPreconditions = queries.getUnitPropagationPreconditionPatterns

+                val mustUnitPropagationPreconditions = queries.getMustUnitPropagationPreconditionPatterns

+                val currentUnitPropagationPreconditions = queries.getCurrentUnitPropagationPreconditionPatterns

                 

                 return new ModelGenerationMethod(

                         statistics,

@@ -90,7 +92,8 @@ class ModelGenerationMethodProvider {
                         unfinishedMultiplicities,

                         unfinishedWF,

                         invalidWF,

-                        unitPropagationPreconditions,

+                        mustUnitPropagationPreconditions,

+                        currentUnitPropagationPreconditions,

                         queries.allQueries

                 )

         }

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 d5ebe318..219f99e9 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
@@ -26,6 +26,14 @@ import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery
 import org.eclipse.xtend.lib.annotations.Accessors

 

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

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

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

+

+@Data class PatternGeneratorResult {

+        CharSequence patternText

+        HashMap<PConstraint,String> constraint2MustPreconditionName

+        HashMap<PConstraint,String> constraint2CurrentPreconditionName

+}

 

 class PatternGenerator {

         @Accessors(PUBLIC_GETTER) val TypeIndexer typeIndexer //= new TypeIndexer(this)

@@ -149,7 +157,7 @@ class PatternGenerator {
                 problem.allTypeReferences.exists[it instanceof StringTypeReference]

         }

         

-        public def transformBaseProperties(

+        public def PatternGeneratorResult transformBaseProperties(

                 LogicProblem problem,

                 PartialInterpretation emptySolution,

                 Map<String,PQuery> fqn2PQuery,

@@ -398,6 +406,6 @@ class PatternGenerator {
                         '''

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

                         val second = up.definitions

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

+                        return new PatternGeneratorResult(first+second,up.constraint2MustPreconditionName,up.constraint2CurrentPreconditionName)

         }

 }

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 18e3018a..750107f6 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
@@ -31,7 +31,8 @@ import java.util.HashMap
         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 Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>>  mustUnitPropagationPreconditionPatterns

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

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

 }

 

@@ -60,14 +61,15 @@ class PatternProvider {
                         null

                 }

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

-                val baseIndexerFile = patternGeneratorResult.key

-                val unitPropagationTrace = patternGeneratorResult.value

+                val baseIndexerFile = patternGeneratorResult.patternText

+                val mustUnitPropagationTrace = patternGeneratorResult.constraint2MustPreconditionName

+                val currentUnitPropagationTrace = patternGeneratorResult.constraint2CurrentPreconditionName

                 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,unitPropagationTrace,generatedQueries);

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

                 return runtimeQueries

         }

         

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

                 PartialInterpretation emptySolution,

                 TypeAnalysisResult typeAnalysisResult,

-                HashMap<PConstraint, String> unitPropagationTrace,

+                HashMap<PConstraint, String> mustUnitPropagationTrace,

+                HashMap<PConstraint, String> currentUnitPropagationTrace,

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

         ) {

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

@@ -92,7 +95,9 @@ class PatternProvider {
                 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)]

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

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

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

                 return new GeneratedPatterns(

                         invalidWFQueries,

                         unfinishedWFQueries,

@@ -100,7 +105,8 @@ class PatternProvider {
                         refineObjectsQueries,

                         refineTypeQueries,

                         refineRelationQueries,

-                        unitPropagationPreconditionPatterns,

+                        mustUnitPropagationPreconditionPatterns,

+                        currentUnitPropagationPreconditionPatterns,

                         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 d487db64..91a7a2c2 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
@@ -61,7 +61,8 @@ class UnitPropagationPreconditionGenerationResult {
 @Data

 class UnitPropagationPreconditionFinalResult {

         CharSequence definitions

-        HashMap<PConstraint,String> constraint2PreconditionName

+        HashMap<PConstraint,String> constraint2MustPreconditionName

+        HashMap<PConstraint,String> constraint2CurrentPreconditionName

 }

 

 class UnitPropagationPreconditionGenerator {

@@ -81,25 +82,34 @@ class UnitPropagationPreconditionGenerator {
                 // Create an empty result

                 val res = new UnitPropagationPreconditionGenerationResult               

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

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

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

+                val Map<PConstraint,List<Pair<String,Integer>>> mainCurrentPropagationNames = 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) {

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

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

-                                        mainPropagationNames.put(referredCheck,new LinkedList)

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

+                                val currentPropagationPrecondition = getOrGeneratePropagationRule(res,relation,query,referredCheck,PropagationModality::UP, Modality::CURRENT)

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

+                                        mainMustPropagationNames.put(referredCheck,new LinkedList)

                                 }

-                                if(propagationPrecondition !== null) {

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

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

+                                        mainCurrentPropagationNames.put(referredCheck,new LinkedList)

+                                }

+                                if(mustPropagationPrecondition !== null) {

+                                        mainMustPropagationNames.get(referredCheck).add(mustPropagationPrecondition->query.parameterNames.size)

+                                }

+                                if(currentPropagationPrecondition !== null) {

+                                        mainCurrentPropagationNames.get(referredCheck).add(currentPropagationPrecondition->query.parameterNames.size)

                                 }

                         }

                 }

                 val preconditions = new LinkedList

-                val constraint2Precondition = new HashMap

-                for(entry : mainPropagationNames.entrySet) {

+                val constraint2MustPrecondition = new HashMap

+                val constraint2CurrentPrecondition = new HashMap

+                for(entry : mainMustPropagationNames.entrySet) {

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

                         val def = '''

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

@@ -107,7 +117,17 @@ class UnitPropagationPreconditionGenerator {
                                         { 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)

+                        constraint2MustPrecondition.put(entry.key,name)

+                }

+                for(entry : mainCurrentPropagationNames.entrySet) {

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

+                        val def = '''

+                        pattern «name»(«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

+                        constraint2CurrentPrecondition.put(entry.key,name)

                 }

                 

                 val definitions = '''

@@ -121,7 +141,7 @@ class UnitPropagationPreconditionGenerator {
                                 «predondition»

                         «ENDFOR»

                 '''

-                return new UnitPropagationPreconditionFinalResult(definitions,constraint2Precondition)

+                return new UnitPropagationPreconditionFinalResult(definitions,constraint2MustPrecondition,constraint2CurrentPrecondition)

         }

         def allReferredConstraints(Relation relation, PQuery query) {

                 val allReferredQueries = query.allReferredQueries