From 7aa34753b7bddeba0e0ba2ecbea9b5bec88b10a8 Mon Sep 17 00:00:00 2001
From: Oszkar Semerath <semerath@mit.bme.hu>
Date: Fri, 8 May 2020 23:32:07 +0200
Subject: UP patterns -> decision procedure trace finished

---
 .../logic2viatra/patterns/PatternGenerator.xtend   |  8 ++--
 .../logic2viatra/patterns/PatternProvider.xtend    | 16 ++++++--
 .../UnitPropagationPreconditionGenerator.xtend     | 43 +++++++++++++++++++---
 .../rules/RefinementRuleProvider.xtend             |  6 +--
 4 files changed, 59 insertions(+), 14 deletions(-)

(limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src')

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
-- 
cgit v1.2.3-54-g00ecf