aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra
diff options
context:
space:
mode:
authorLibravatar Kristóf Marussy <marussy@mit.bme.hu>2020-05-10 22:13:21 +0200
committerLibravatar Kristóf Marussy <marussy@mit.bme.hu>2020-05-10 22:13:21 +0200
commit5a6eea9bd15597eab77bbcedb4b5116020f0a67d (patch)
tree6c86f7e5bd3d86fde29d3fee4fb4f912f35057bc /Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra
parentAdd satellite case study (diff)
parentMerge branch 'master' of https://github.com/viatra/VIATRA-Generator (diff)
downloadVIATRA-Generator-5a6eea9bd15597eab77bbcedb4b5116020f0a67d.tar.gz
VIATRA-Generator-5a6eea9bd15597eab77bbcedb4b5116020f0a67d.tar.zst
VIATRA-Generator-5a6eea9bd15597eab77bbcedb4b5116020f0a67d.zip
Merge branch 'master' of github.com:viatra/VIATRA-Generator
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra')
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend7
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend8
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend15
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnitPropagationPreconditionGenerator.xtend142
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend65
5 files changed, 147 insertions, 90 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 e7342ff7..975ace2f 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
@@ -17,6 +17,8 @@ import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher
17import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery 17import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery
18import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRule 18import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRule
19import org.eclipse.xtend.lib.annotations.Data 19import org.eclipse.xtend.lib.annotations.Data
20import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint
21import java.util.Map
20 22
21class ModelGenerationStatistics { 23class ModelGenerationStatistics {
22 public var long transformationExecutionTime = 0 24 public var long transformationExecutionTime = 0
@@ -36,6 +38,8 @@ class ModelGenerationStatistics {
36 38
37 Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidWF 39 Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidWF
38 40
41 Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unitPropagationPreconditions
42
39 Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allPatterns 43 Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allPatterns
40} 44}
41enum TypeInferenceMethod { 45enum TypeInferenceMethod {
@@ -77,6 +81,8 @@ class ModelGenerationMethodProvider {
77 81
78 val invalidWF = queries.getInvalidWFQueries.values 82 val invalidWF = queries.getInvalidWFQueries.values
79 83
84 val unitPropagationPreconditions = queries.getUnitPropagationPreconditionPatterns
85
80 return new ModelGenerationMethod( 86 return new ModelGenerationMethod(
81 statistics, 87 statistics,
82 objectRefinementRules.values, 88 objectRefinementRules.values,
@@ -84,6 +90,7 @@ class ModelGenerationMethodProvider {
84 unfinishedMultiplicities, 90 unfinishedMultiplicities,
85 unfinishedWF, 91 unfinishedWF,
86 invalidWF, 92 invalidWF,
93 unitPropagationPreconditions,
87 queries.allQueries 94 queries.allQueries
88 ) 95 )
89 } 96 }
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..18e3018a 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
21import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* 21import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
22import java.util.Collection 22import java.util.Collection
23import java.util.Set 23import java.util.Set
24import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint
25import 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,8 @@ 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)]
88 return new GeneratedPatterns( 96 return new GeneratedPatterns(
89 invalidWFQueries, 97 invalidWFQueries,
90 unfinishedWFQueries, 98 unfinishedWFQueries,
@@ -92,6 +100,7 @@ class PatternProvider {
92 refineObjectsQueries, 100 refineObjectsQueries,
93 refineTypeQueries, 101 refineTypeQueries,
94 refineRelationQueries, 102 refineRelationQueries,
103 unitPropagationPreconditionPatterns,
95 queries.values 104 queries.values
96 ) 105 )
97 } 106 }
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 f726a24f..d487db64 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
@@ -22,6 +22,7 @@ import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.NegativeP
22import java.util.Comparator 22import java.util.Comparator
23import java.util.ArrayList 23import java.util.ArrayList
24import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PDisjunction 24import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PDisjunction
25import java.util.LinkedHashSet
25 26
26@Data class UnitPropagation { 27@Data class UnitPropagation {
27 val PQuery q 28 val PQuery q
@@ -57,6 +58,11 @@ class UnitPropagationPreconditionGenerationResult {
57 return unitPropagation2PatternName.get(key) !== null 58 return unitPropagation2PatternName.get(key) !== null
58 } 59 }
59} 60}
61@Data
62class UnitPropagationPreconditionFinalResult {
63 CharSequence definitions
64 HashMap<PConstraint,String> constraint2PreconditionName
65}
60 66
61class UnitPropagationPreconditionGenerator { 67class UnitPropagationPreconditionGenerator {
62 val PatternGenerator base 68 val PatternGenerator base
@@ -75,30 +81,59 @@ class UnitPropagationPreconditionGenerator {
75 // Create an empty result 81 // Create an empty result
76 val res = new UnitPropagationPreconditionGenerationResult 82 val res = new UnitPropagationPreconditionGenerationResult
77 val wfs = base.wfQueries(problem)//.map[it.patternPQuery] 83 val wfs = base.wfQueries(problem)//.map[it.patternPQuery]
78 val mainPropagationNames = new LinkedList 84 val Map<PConstraint,List<Pair<String,Integer>>> mainPropagationNames = new HashMap
79 for(wf : wfs) { 85 for(wf : wfs) {
80 val query = wf.patternPQuery as PQuery 86 val query = wf.patternPQuery as PQuery
81 val relation = wf.target 87 val relation = wf.target
82 val allReferredChecks = query.allReferredConstraints.filter(ExpressionEvaluation) 88 val allReferredChecks = allReferredConstraints(relation,query).filter(ExpressionEvaluation)
83 89
84 for(referredCheck : allReferredChecks) { 90 for(referredCheck : allReferredChecks) {
85 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 mainPropagationNames.get(referredCheck).add(propagationPrecondition->query.parameterNames.size)
97 }
86 } 98 }
87 } 99 }
88 return ''' 100 val preconditions = new LinkedList
101 val constraint2Precondition = new HashMap
102 for(entry : mainPropagationNames.entrySet) {
103 val name = '''UPMUSTPropagate_«res.getOrGenerateConstraintName(entry.key)»''';
104 val def = '''
105 pattern «name»(«FOR index : 1..entry.key.arity SEPARATOR ", "»«canonizeName(index,PropagationModality::UP)»«ENDFOR»)
106 «FOR propagation : entry.value SEPARATOR " or "»
107 { find «propagation.key»(problem,interpretation,«FOR index : 0..<propagation.value SEPARATOR ','»_«ENDFOR»,«FOR index : 1..entry.key.arity SEPARATOR ", "»«canonizeName(index,PropagationModality::UP)»«ENDFOR»); }
108 «ENDFOR»'''
109 preconditions+=def
110 constraint2Precondition.put(entry.key,name)
111 }
112
113 val definitions = '''
89 «FOR def : res.definitions» 114 «FOR def : res.definitions»
90 «def» 115 «def»
91 «ENDFOR» 116 «ENDFOR»
92 117
93 // Main propagations: 118 // Collected propagation preconditions:
94 «FOR name : mainPropagationNames» 119
95 «name» 120 «FOR predondition : preconditions»
121 «predondition»
96 «ENDFOR» 122 «ENDFOR»
97 ''' 123 '''
124 return new UnitPropagationPreconditionFinalResult(definitions,constraint2Precondition)
98 } 125 }
99 def allReferredConstraints(PQuery query) { 126 def allReferredConstraints(Relation relation, PQuery query) {
100 val allReferredQueries = query.allReferredQueries 127 val allReferredQueries = query.allReferredQueries
101 return (#[query]+allReferredQueries).map[it.disjunctBodies.bodies].flatten.map[constraints].flatten 128 val problem = relation.eContainer as LogicProblem
129 val constraints = new LinkedHashSet
130 for(referredQuery: #[query]+allReferredQueries) {
131 val referredRelation = problem.annotations.filter(TransfomedViatraQuery).filter[it.patternPQuery === referredQuery].head.target
132 val bodies = (referredRelation.annotations.filter(TransfomedViatraQuery).head.optimizedDisjunction as PDisjunction).bodies
133 constraints.addAll(bodies.map[getConstraints].flatten)
134 }
135
136 return constraints
102 } 137 }
103 138
104 def getOrGeneratePropagationRule(UnitPropagationPreconditionGenerationResult res, Relation relation, PQuery q, PConstraint c, PropagationModality pm, Modality m3) { 139 def getOrGeneratePropagationRule(UnitPropagationPreconditionGenerationResult res, Relation relation, PQuery q, PConstraint c, PropagationModality pm, Modality m3) {
@@ -141,64 +176,67 @@ class UnitPropagationPreconditionGenerator {
141 // Otherwise, for PropagationModality::DOWN, the body cannot be satisfied 176 // Otherwise, for PropagationModality::DOWN, the body cannot be satisfied
142 } else { 177 } else {
143 val positives = body.constraints.filter(PositivePatternCall) 178 val positives = body.constraints.filter(PositivePatternCall)
144 val positiveRefers = positives.filter[it.referredQuery.allReferredConstraints.toSet.contains(c)] 179 for(positive: positives) {
145 for(positiveRefer: positiveRefers) { 180 val referredPQuery = positive.referredQuery
146 val referredPQuery = positiveRefer.referredQuery
147 val referredRelation = (relation.eContainer as LogicProblem) 181 val referredRelation = (relation.eContainer as LogicProblem)
148 .annotations.filter(TransfomedViatraQuery).filter[it.patternPQuery === referredPQuery].head.target 182 .annotations.filter(TransfomedViatraQuery).filter[it.patternPQuery === referredPQuery].head.target
149 val referredName = getOrGeneratePropagationRule(res,referredRelation,referredPQuery,c,pm,m3) 183 if(allReferredConstraints(referredRelation,referredPQuery).toSet.contains(c)) {
150 if(referredName !== null) { 184 val referredName = getOrGeneratePropagationRule(res,referredRelation,referredPQuery,c,pm,m3)
151 generatedBodies += ''' 185 if(referredName !== null) {
152 // Original Constraints 186 generatedBodies += '''
153 «FOR constraint : body.constraints.filter[it !== positiveRefer]» 187 // Original Constraints
154 «this.constraintTransformer.transformConstraint(constraint,m3,relation.annotations.filter(TransfomedViatraQuery).head.variableTrace)» 188 «FOR constraint : body.constraints.filter[it !== positive]»
155 «ENDFOR» 189 «this.constraintTransformer.transformConstraint(constraint,m3,relation.annotations.filter(TransfomedViatraQuery).head.variableTrace)»
156 // Propagation for constraint referred indirectly from this pattern through «referredName» 190 «ENDFOR»
157 find «referredName»(problem, interpretation, 191 // Propagation for constraint referred indirectly from this pattern through «referredName»
158 «FOR index : 0..<referredPQuery.parameters.size SEPARATOR ", "»«positiveRefer.getVariableInTuple(index).canonizeName»«ENDFOR», 192 find «referredName»(problem, interpretation,
159 «FOR index : 0..c.arity SEPARATOR ", "»«canonizeName(index,pm)»«ENDFOR»); 193 «FOR index : 0..<referredPQuery.parameters.size SEPARATOR ", "»«positive.getVariableInTuple(index).canonizeName»«ENDFOR»,
160 ''' 194 «FOR index : 0..c.arity SEPARATOR ", "»«canonizeName(index,pm)»«ENDFOR»);
195 '''
196 }
197 // Otherwise, if the referred pattern is not satisfiable, this pattern is not satisfiable either
161 } 198 }
162 // Otherwise, if the referred pattern is not satisfiable, this pattern is not satisfiable either
163 } 199 }
200
164 val negatives = body.constraints.filter(NegativePatternCall) 201 val negatives = body.constraints.filter(NegativePatternCall)
165 val negativeRefers = negatives.filter[it.referredQuery.allReferredConstraints.toSet.contains(c)] 202 for(negative : negatives) {
166 for(negativeRefer : negativeRefers) { 203 val referredPQuery = negative.referredQuery
167 val referredPQuery = negativeRefer.referredQuery
168 val referredRelation = (relation.eContainer as LogicProblem) 204 val referredRelation = (relation.eContainer as LogicProblem)
169 .annotations.filter(TransfomedViatraQuery).filter[it.patternPQuery === referredPQuery].head.target 205 .annotations.filter(TransfomedViatraQuery).filter[it.patternPQuery === referredPQuery].head.target
170 val referredName = getOrGeneratePropagationRule(res,referredRelation,referredPQuery,c,pm,m3.dual) 206 if(allReferredConstraints(referredRelation,referredPQuery).toSet.contains(c)) {
171 if(referredName !== null) { 207 val referredName = getOrGeneratePropagationRule(res,referredRelation,referredPQuery,c,pm,m3.dual)
172 generatedBodies += ''' 208 if(referredName !== null) {
173 // Original Constraints 209 generatedBodies += '''
174 «FOR constraint : body.constraints.filter[it !== negativeRefer]» 210 // Original Constraints
175 «this.constraintTransformer.transformConstraint(constraint,m3,relation.annotations.filter(TransfomedViatraQuery).head.variableTrace)» 211 «FOR constraint : body.constraints.filter[it !== negative]»
176 «ENDFOR» 212 «this.constraintTransformer.transformConstraint(constraint,m3,relation.annotations.filter(TransfomedViatraQuery).head.variableTrace)»
177 // Propagation for constraint referred indirectly from this pattern through «referredName» 213 «ENDFOR»
178 find «referredName»(problem, interpretation, 214 // Propagation for constraint referred indirectly from this pattern through «referredName»
179 «FOR index : 0..<referredPQuery.parameters.size SEPARATOR ", "»«(negativeRefer.actualParametersTuple.get(index) as PVariable).canonizeName»«ENDFOR», 215 find «referredName»(problem, interpretation,
180 «FOR index : 0..c.arity SEPARATOR ", "»«canonizeName(index,pm)»«ENDFOR»); 216 «FOR index : 0..<referredPQuery.parameters.size SEPARATOR ", "»«(negative.actualParametersTuple.get(index) as PVariable).canonizeName»«ENDFOR»,
181 ''' 217 «FOR index : 0..c.arity SEPARATOR ", "»«canonizeName(index,pm)»«ENDFOR»);
182 } else { 218 '''
183 generatedBodies += ''' 219 } else {
184 // Original Constraints 220 generatedBodies += '''
185 «FOR constraint : body.constraints.filter[it !== negativeRefer]» 221 // Original Constraints
186 «this.constraintTransformer.transformConstraint(constraint,m3,relation.annotations.filter(TransfomedViatraQuery).head.variableTrace)» 222 «FOR constraint : body.constraints.filter[it !== negative]»
187 «ENDFOR» 223 «this.constraintTransformer.transformConstraint(constraint,m3,relation.annotations.filter(TransfomedViatraQuery).head.variableTrace)»
188 // Propagation for constraint referred indirectly from this pattern through «referredName», 224 «ENDFOR»
189 // which was unsatisfiable 225 // Propagation for constraint referred indirectly from this pattern through «referredName»,
190 ''' 226 // which was unsatisfiable
227 '''
228 }
191 } 229 }
192 } 230 }
193 } 231 }
194 } 232 }
195 233
196 // Register the result 234 // Register the result
197 if(generatedBodies.size>=0) { 235 if(generatedBodies.empty) {
198 res.registerUnsatQuery(q,c,pm,m3) 236 res.registerUnsatQuery(q,c,pm,m3)
199 } else { 237 } else {
200 val definition = ''' 238 val definition = '''
201 pattern «name»( 239 private pattern «name»(
202 problem:LogicProblem, interpretation:PartialInterpretation, 240 problem:LogicProblem, interpretation:PartialInterpretation,
203 «FOR param : q.parameters SEPARATOR ', '»var_«param.name»«ENDFOR», 241 «FOR param : q.parameters SEPARATOR ', '»var_«param.name»«ENDFOR»,
204 «FOR arity : 1..constraintArity SEPARATOR ', '»«canonizeName(arity,pm)»«ENDFOR») 242 «FOR arity : 1..constraintArity SEPARATOR ', '»«canonizeName(arity,pm)»«ENDFOR»)
@@ -229,7 +267,7 @@ class UnitPropagationPreconditionGenerator {
229 } 267 }
230 val variablesInOrder = new ArrayList(c.affectedVariables) 268 val variablesInOrder = new ArrayList(c.affectedVariables)
231 variablesInOrder.toList.sort(comparator) 269 variablesInOrder.toList.sort(comparator)
232 return '''«FOR variableIndex : 1..variablesInOrder.size»«variablesInOrder.get(variableIndex-1).name»==«canonizeName(variableIndex,m)»;«ENDFOR»''' 270 return '''«FOR variableIndex : 1..variablesInOrder.size»«variablesInOrder.get(variableIndex-1).canonizeName»==«canonizeName(variableIndex,m)»;«ENDFOR»'''
233 } 271 }
234 def dispatch propagateVariables(PConstraint c, PropagationModality m) { 272 def dispatch propagateVariables(PConstraint c, PropagationModality m) {
235 throw new UnsupportedOperationException('''Constraint not supported: «c.class.simpleName»''') 273 throw new UnsupportedOperationException('''Constraint not supported: «c.class.simpleName»''')
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 b4cb9ec7..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
@@ -179,36 +179,37 @@ class RefinementRuleProvider {
179 179
180 if(containmentReferences.contains(relation)) { 180 if(containmentReferences.contains(relation)) {
181 val targetTypeInterpretation = getTypeInterpretation(i, relation, 1) 181 val targetTypeInterpretation = getTypeInterpretation(i, relation, 1)
182 182 if(!(targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.isIsAbstract) {
183 val inverseAnnotation = p.assertions.filter(InverseRelationAssertion).filter[it.inverseA === relation || it.inverseB === relation] 183 val inverseAnnotation = p.assertions.filter(InverseRelationAssertion).filter[it.inverseA === relation || it.inverseB === relation]
184 if(!inverseAnnotation.empty) { 184 if(!inverseAnnotation.empty) {
185 val onlyInverseAnnotation = if(inverseAnnotation.head.inverseA===relation) { 185 val onlyInverseAnnotation = if(inverseAnnotation.head.inverseA===relation) {
186 inverseAnnotation.head.inverseB 186 inverseAnnotation.head.inverseB
187 } else {
188 inverseAnnotation.head.inverseA
189 }
190 val inverseRelationInterpretation = i.partialrelationinterpretation.filter[it.interpretationOf === onlyInverseAnnotation].head
191 for(var times=0; times<number; times++) {
192 recursiveObjectCreation.get(sourceTypeInterpretation.interpretationOf) +=
193 new ObjectCreationInterpretationData(
194 i,
195 targetTypeInterpretation,
196 relationInterpretation,
197 inverseRelationInterpretation,
198 targetTypeInterpretation.getTypeConstructor
199 )
200 }
201
187 } else { 202 } else {
188 inverseAnnotation.head.inverseA 203 for(var times=0; times<number; times++) {
189 } 204 recursiveObjectCreation.get(sourceTypeInterpretation.interpretationOf) +=
190 val inverseRelationInterpretation = i.partialrelationinterpretation.filter[it.interpretationOf === onlyInverseAnnotation].head 205 new ObjectCreationInterpretationData(
191 for(var times=0; times<number; times++) { 206 i,
192 recursiveObjectCreation.get(sourceTypeInterpretation.interpretationOf) += 207 targetTypeInterpretation,
193 new ObjectCreationInterpretationData( 208 relationInterpretation,
194 i, 209 null,
195 targetTypeInterpretation, 210 targetTypeInterpretation.getTypeConstructor
196 relationInterpretation, 211 )
197 inverseRelationInterpretation, 212 }
198 targetTypeInterpretation.getTypeConstructor
199 )
200 }
201
202 } else {
203 for(var times=0; times<number; times++) {
204 recursiveObjectCreation.get(sourceTypeInterpretation.interpretationOf) +=
205 new ObjectCreationInterpretationData(
206 i,
207 targetTypeInterpretation,
208 relationInterpretation,
209 null,
210 targetTypeInterpretation.getTypeConstructor
211 )
212 } 213 }
213 } 214 }
214 } else if(relation.parameters.get(1) instanceof PrimitiveTypeReference) { 215 } else if(relation.parameters.get(1) instanceof PrimitiveTypeReference) {
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-07-16 20:04:01 +0000