diff options
author | 2020-05-08 23:32:07 +0200 | |
---|---|---|
committer | 2020-05-08 23:32:07 +0200 | |
commit | 7aa34753b7bddeba0e0ba2ecbea9b5bec88b10a8 (patch) | |
tree | cb065859b4d41a2bc4e467015a62d040eb03d15d /Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra | |
parent | contained objects instantiated immediately if target class non-abstract (diff) | |
download | VIATRA-Generator-7aa34753b7bddeba0e0ba2ecbea9b5bec88b10a8.tar.gz VIATRA-Generator-7aa34753b7bddeba0e0ba2ecbea9b5bec88b10a8.tar.zst VIATRA-Generator-7aa34753b7bddeba0e0ba2ecbea9b5bec88b10a8.zip |
UP patterns -> decision procedure trace finished
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra')
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 { | |||
155 | Map<String,PQuery> fqn2PQuery, | 155 | Map<String,PQuery> fqn2PQuery, |
156 | TypeAnalysisResult typeAnalysisResult | 156 | TypeAnalysisResult typeAnalysisResult |
157 | ) { | 157 | ) { |
158 | 158 | val first = | |
159 | return ''' | 159 | ''' |
160 | import epackage "http://www.bme.hu/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage" | 160 | import epackage "http://www.bme.hu/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage" |
161 | import epackage "http://www.bme.hu/mit/inf/dslreasoner/logic/model/problem" | 161 | import epackage "http://www.bme.hu/mit/inf/dslreasoner/logic/model/problem" |
162 | import epackage "http://www.bme.hu/mit/inf/dslreasoner/logic/model/language" | 162 | import epackage "http://www.bme.hu/mit/inf/dslreasoner/logic/model/language" |
@@ -395,7 +395,9 @@ class PatternGenerator { | |||
395 | ////////// | 395 | ////////// |
396 | // 5 Unit Propagations | 396 | // 5 Unit Propagations |
397 | ////////// | 397 | ////////// |
398 | «unitPropagationPreconditionGenerator.generateUnitPropagationRules(problem,problem.relations.filter(RelationDefinition),fqn2PQuery)» | ||
399 | ''' | 398 | ''' |
399 | val up = unitPropagationPreconditionGenerator.generateUnitPropagationRules(problem,problem.relations.filter(RelationDefinition),fqn2PQuery) | ||
400 | val second = up.definitions | ||
401 | return (first+second) -> up.constraint2PreconditionName | ||
400 | } | 402 | } |
401 | } | 403 | } |
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 | |||
21 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | 21 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* |
22 | import java.util.Collection | 22 | import java.util.Collection |
23 | import java.util.Set | 23 | import java.util.Set |
24 | import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint | ||
25 | import java.util.HashMap | ||
24 | 26 | ||
25 | @Data class GeneratedPatterns { | 27 | @Data class GeneratedPatterns { |
26 | public Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidWFQueries | 28 | public Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidWFQueries |
@@ -29,6 +31,7 @@ import java.util.Set | |||
29 | public Map<ObjectCreationPrecondition, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineObjectQueries | 31 | public Map<ObjectCreationPrecondition, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineObjectQueries |
30 | public Map<? extends Type, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineTypeQueries | 32 | public Map<? extends Type, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineTypeQueries |
31 | public Map<Pair<RelationDeclaration, Relation>, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refinerelationQueries | 33 | public Map<Pair<RelationDeclaration, Relation>, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refinerelationQueries |
34 | public Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unitPropagationPreconditionPatterns | ||
32 | public Collection<IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allQueries | 35 | public Collection<IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allQueries |
33 | } | 36 | } |
34 | 37 | ||
@@ -56,13 +59,15 @@ class PatternProvider { | |||
56 | } else { | 59 | } else { |
57 | null | 60 | null |
58 | } | 61 | } |
59 | val baseIndexerFile = patternGenerator.transformBaseProperties(problem,emptySolution,fqn2Query,typeAnalysisResult) | 62 | val patternGeneratorResult = patternGenerator.transformBaseProperties(problem,emptySolution,fqn2Query,typeAnalysisResult) |
63 | val baseIndexerFile = patternGeneratorResult.key | ||
64 | val unitPropagationTrace = patternGeneratorResult.value | ||
60 | if(writeToFile) { | 65 | if(writeToFile) { |
61 | workspace.writeText('''generated3valued.vql_deactivated''',baseIndexerFile) | 66 | workspace.writeText('''generated3valued.vql_deactivated''',baseIndexerFile) |
62 | } | 67 | } |
63 | val ParseUtil parseUtil = new ParseUtil | 68 | val ParseUtil parseUtil = new ParseUtil |
64 | val generatedQueries = parseUtil.parse(baseIndexerFile) | 69 | val generatedQueries = parseUtil.parse(baseIndexerFile) |
65 | val runtimeQueries = calclulateRuntimeQueries(patternGenerator,problem,emptySolution,typeAnalysisResult,generatedQueries); | 70 | val runtimeQueries = calclulateRuntimeQueries(patternGenerator,problem,emptySolution,typeAnalysisResult,unitPropagationTrace,generatedQueries); |
66 | return runtimeQueries | 71 | return runtimeQueries |
67 | } | 72 | } |
68 | 73 | ||
@@ -71,7 +76,8 @@ class PatternProvider { | |||
71 | LogicProblem problem, | 76 | LogicProblem problem, |
72 | PartialInterpretation emptySolution, | 77 | PartialInterpretation emptySolution, |
73 | TypeAnalysisResult typeAnalysisResult, | 78 | TypeAnalysisResult typeAnalysisResult, |
74 | Map<String, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> queries | 79 | HashMap<PConstraint, String> unitPropagationTrace, |
80 | Map<String, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> queries | ||
75 | ) { | 81 | ) { |
76 | val Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> | 82 | val Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> |
77 | invalidWFQueries = patternGenerator.invalidIndexer.getInvalidateByWfQueryNames(problem).mapValues[it.lookup(queries)] | 83 | invalidWFQueries = patternGenerator.invalidIndexer.getInvalidateByWfQueryNames(problem).mapValues[it.lookup(queries)] |
@@ -85,6 +91,9 @@ class PatternProvider { | |||
85 | refineTypeQueries = patternGenerator.typeRefinementGenerator.getRefineTypeQueryNames(problem,emptySolution,typeAnalysisResult).mapValues[it.lookup(queries)] | 91 | refineTypeQueries = patternGenerator.typeRefinementGenerator.getRefineTypeQueryNames(problem,emptySolution,typeAnalysisResult).mapValues[it.lookup(queries)] |
86 | val Map<Pair<RelationDeclaration, Relation>, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> | 92 | val Map<Pair<RelationDeclaration, Relation>, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> |
87 | refineRelationQueries = patternGenerator.relationRefinementGenerator.getRefineRelationQueries(problem).mapValues[it.lookup(queries)] | 93 | refineRelationQueries = patternGenerator.relationRefinementGenerator.getRefineRelationQueries(problem).mapValues[it.lookup(queries)] |
94 | val Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> | ||
95 | unitPropagationPreconditionPatterns = unitPropagationTrace.mapValues[it.lookup(queries)] | ||
96 | unitPropagationPreconditionPatterns.entrySet.forEach[println(it.key + "->" +it.value)] | ||
88 | return new GeneratedPatterns( | 97 | return new GeneratedPatterns( |
89 | invalidWFQueries, | 98 | invalidWFQueries, |
90 | unfinishedWFQueries, | 99 | unfinishedWFQueries, |
@@ -92,6 +101,7 @@ class PatternProvider { | |||
92 | refineObjectsQueries, | 101 | refineObjectsQueries, |
93 | refineTypeQueries, | 102 | refineTypeQueries, |
94 | refineRelationQueries, | 103 | refineRelationQueries, |
104 | unitPropagationPreconditionPatterns, | ||
95 | queries.values | 105 | queries.values |
96 | ) | 106 | ) |
97 | } | 107 | } |
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 { | |||
58 | return unitPropagation2PatternName.get(key) !== null | 58 | return unitPropagation2PatternName.get(key) !== null |
59 | } | 59 | } |
60 | } | 60 | } |
61 | @Data | ||
62 | class UnitPropagationPreconditionFinalResult { | ||
63 | CharSequence definitions | ||
64 | HashMap<PConstraint,String> constraint2PreconditionName | ||
65 | } | ||
61 | 66 | ||
62 | class UnitPropagationPreconditionGenerator { | 67 | class UnitPropagationPreconditionGenerator { |
63 | val PatternGenerator base | 68 | val PatternGenerator base |
@@ -76,23 +81,51 @@ class UnitPropagationPreconditionGenerator { | |||
76 | // Create an empty result | 81 | // Create an empty result |
77 | val res = new UnitPropagationPreconditionGenerationResult | 82 | val res = new UnitPropagationPreconditionGenerationResult |
78 | val wfs = base.wfQueries(problem)//.map[it.patternPQuery] | 83 | val wfs = base.wfQueries(problem)//.map[it.patternPQuery] |
79 | val mainPropagationNames = new LinkedHashSet | 84 | val Map<PConstraint,List<Pair<String,Integer>>> mainPropagationNames = new HashMap |
80 | for(wf : wfs) { | 85 | for(wf : wfs) { |
81 | val query = wf.patternPQuery as PQuery | 86 | val query = wf.patternPQuery as PQuery |
82 | val relation = wf.target | 87 | val relation = wf.target |
83 | val allReferredChecks = allReferredConstraints(relation,query).filter(ExpressionEvaluation) | 88 | val allReferredChecks = allReferredConstraints(relation,query).filter(ExpressionEvaluation) |
84 | 89 | ||
85 | for(referredCheck : allReferredChecks) { | 90 | for(referredCheck : allReferredChecks) { |
86 | mainPropagationNames+= getOrGeneratePropagationRule(res,relation,query,referredCheck,PropagationModality::UP, Modality::MUST) | 91 | val propagationPrecondition = getOrGeneratePropagationRule(res,relation,query,referredCheck,PropagationModality::UP, Modality::MUST) |
92 | if(!mainPropagationNames.containsKey(referredCheck)) { | ||
93 | mainPropagationNames.put(referredCheck,new LinkedList) | ||
94 | } | ||
95 | if(propagationPrecondition !== null) { | ||
96 | println(query.parameterNames) | ||
97 | println(query.parameterNames.size) | ||
98 | mainPropagationNames.get(referredCheck).add(propagationPrecondition->query.parameterNames.size) | ||
99 | } | ||
87 | } | 100 | } |
88 | } | 101 | } |
89 | return ''' | 102 | val preconditions = new LinkedList |
103 | val constraint2Precondition = new HashMap | ||
104 | for(entry : mainPropagationNames.entrySet) { | ||
105 | val name = '''UPMUSTPropagate«res.getOrGenerateConstraintName(entry.key)»'''; | ||
106 | val def = ''' | ||
107 | pattern «name»( | ||
108 | problem:LogicProblem, interpretation:PartialInterpretation, | ||
109 | «FOR index : 1..entry.key.arity SEPARATOR ", "»«canonizeName(index,PropagationModality::UP)»«ENDFOR») | ||
110 | «FOR propagation : entry.value SEPARATOR " or "» | ||
111 | { find «propagation.key»(problem,interpretation,«FOR index : 0..<propagation.value SEPARATOR ','»_«ENDFOR»,«FOR index : 1..entry.key.arity SEPARATOR ", "»«canonizeName(index,PropagationModality::UP)»«ENDFOR»); } | ||
112 | «ENDFOR»''' | ||
113 | preconditions+=def | ||
114 | constraint2Precondition.put(entry.key,name) | ||
115 | } | ||
116 | |||
117 | val definitions = ''' | ||
90 | «FOR def : res.definitions» | 118 | «FOR def : res.definitions» |
91 | «def» | 119 | «def» |
92 | «ENDFOR» | 120 | «ENDFOR» |
93 | 121 | ||
94 | // Main propagations: «FOR name : mainPropagationNames SEPARATOR ", "»«name»«ENDFOR» | 122 | // Collected propagation preconditions: |
123 | |||
124 | «FOR predondition : preconditions» | ||
125 | «predondition» | ||
126 | «ENDFOR» | ||
95 | ''' | 127 | ''' |
128 | return new UnitPropagationPreconditionFinalResult(definitions,constraint2Precondition) | ||
96 | } | 129 | } |
97 | def allReferredConstraints(Relation relation, PQuery query) { | 130 | def allReferredConstraints(Relation relation, PQuery query) { |
98 | val allReferredQueries = query.allReferredQueries | 131 | val allReferredQueries = query.allReferredQueries |
@@ -207,7 +240,7 @@ class UnitPropagationPreconditionGenerator { | |||
207 | res.registerUnsatQuery(q,c,pm,m3) | 240 | res.registerUnsatQuery(q,c,pm,m3) |
208 | } else { | 241 | } else { |
209 | val definition = ''' | 242 | val definition = ''' |
210 | pattern «name»( | 243 | private pattern «name»( |
211 | problem:LogicProblem, interpretation:PartialInterpretation, | 244 | problem:LogicProblem, interpretation:PartialInterpretation, |
212 | «FOR param : q.parameters SEPARATOR ', '»var_«param.name»«ENDFOR», | 245 | «FOR param : q.parameters SEPARATOR ', '»var_«param.name»«ENDFOR», |
213 | «FOR arity : 1..constraintArity SEPARATOR ', '»«canonizeName(arity,pm)»«ENDFOR») | 246 | «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 { | |||
90 | if(containmentRelation !== null) { | 90 | if(containmentRelation !== null) { |
91 | if(inverseRelation!== null) { | 91 | if(inverseRelation!== null) { |
92 | ruleBuilder.action[match | | 92 | ruleBuilder.action[match | |
93 | println(name) | 93 | //println(name) |
94 | val startTime = System.nanoTime | 94 | val startTime = System.nanoTime |
95 | //val problem = match.get(0) as LogicProblem | 95 | //val problem = match.get(0) as LogicProblem |
96 | val interpretation = match.get(1) as PartialInterpretation | 96 | val interpretation = match.get(1) as PartialInterpretation |
@@ -115,7 +115,7 @@ class RefinementRuleProvider { | |||
115 | ] | 115 | ] |
116 | } else { | 116 | } else { |
117 | ruleBuilder.action[match | | 117 | ruleBuilder.action[match | |
118 | println(name) | 118 | //println(name) |
119 | val startTime = System.nanoTime | 119 | val startTime = System.nanoTime |
120 | //val problem = match.get(0) as LogicProblem | 120 | //val problem = match.get(0) as LogicProblem |
121 | val interpretation = match.get(1) as PartialInterpretation | 121 | val interpretation = match.get(1) as PartialInterpretation |
@@ -139,7 +139,7 @@ class RefinementRuleProvider { | |||
139 | } | 139 | } |
140 | } else { | 140 | } else { |
141 | ruleBuilder.action[match | | 141 | ruleBuilder.action[match | |
142 | println(name) | 142 | //println(name) |
143 | val startTime = System.nanoTime | 143 | val startTime = System.nanoTime |
144 | //val problem = match.get(0) as LogicProblem | 144 | //val problem = match.get(0) as LogicProblem |
145 | val interpretation = match.get(1) as PartialInterpretation | 145 | val interpretation = match.get(1) as PartialInterpretation |