aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme
diff options
context:
space:
mode:
authorLibravatar Kristóf Marussy <marussy@mit.bme.hu>2020-05-19 21:22:01 +0200
committerLibravatar Kristóf Marussy <marussy@mit.bme.hu>2020-05-19 22:11:37 +0200
commit167e0470bc4562f77d46d8af8c0ef6794dfee693 (patch)
tree8f647b4a6d6b412b9e912a4e0841a2898e830b13 /Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme
parentConfig language WIP (diff)
parentMerge branch 'master' of https://github.com/viatra/VIATRA-Generator (diff)
downloadVIATRA-Generator-167e0470bc4562f77d46d8af8c0ef6794dfee693.tar.gz
VIATRA-Generator-167e0470bc4562f77d46d8af8c0ef6794dfee693.tar.zst
VIATRA-Generator-167e0470bc4562f77d46d8af8c0ef6794dfee693.zip
Merge remote-tracking branch 'upstream/master'
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme')
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend11
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/MultiplicityGoalConstraintCalculator.xtend32
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ScopePropagator.xtend69
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PConstraintTransformer.xtend24
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PExpressionGenerator.xtend29
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend164
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend47
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDeclarationIndexer.xtend4
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnfinishedIndexer.xtend12
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnitPropagationPreconditionGenerator.xtend46
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend93
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend88
12 files changed, 385 insertions, 234 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..ca09ae00 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 {
38 38
39 Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidWF 39 Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidWF
40 40
41 Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unitPropagationPreconditions 41 Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> mustUnitPropagationPreconditions
42 Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> currentUnitPropagationPreconditions
42 43
43 Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allPatterns 44 Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allPatterns
44} 45}
@@ -76,12 +77,13 @@ class ModelGenerationMethodProvider {
76 objectRefinementRules = refinementRuleProvider.createObjectRefinementRules(logicProblem, emptySolution, queries,scopePropagator,nameNewElements,statistics) 77 objectRefinementRules = refinementRuleProvider.createObjectRefinementRules(logicProblem, emptySolution, queries,scopePropagator,nameNewElements,statistics)
77 val relationRefinementRules = refinementRuleProvider.createRelationRefinementRules(queries,statistics) 78 val relationRefinementRules = refinementRuleProvider.createRelationRefinementRules(queries,statistics)
78 79
79 val unfinishedMultiplicities = goalConstraintProvider.getUnfinishedMultiplicityQueries(queries) 80 val unfinishedMultiplicities = goalConstraintProvider.getUnfinishedMultiplicityQueries(logicProblem,queries)
80 val unfinishedWF = queries.getUnfinishedWFQueries.values 81 val unfinishedWF = queries.getUnfinishedWFQueries.values
81 82
82 val invalidWF = queries.getInvalidWFQueries.values 83 val invalidWF = queries.getInvalidWFQueries.values
83 84
84 val unitPropagationPreconditions = queries.getUnitPropagationPreconditionPatterns 85 val mustUnitPropagationPreconditions = queries.getMustUnitPropagationPreconditionPatterns
86 val currentUnitPropagationPreconditions = queries.getCurrentUnitPropagationPreconditionPatterns
85 87
86 return new ModelGenerationMethod( 88 return new ModelGenerationMethod(
87 statistics, 89 statistics,
@@ -90,7 +92,8 @@ class ModelGenerationMethodProvider {
90 unfinishedMultiplicities, 92 unfinishedMultiplicities,
91 unfinishedWF, 93 unfinishedWF,
92 invalidWF, 94 invalidWF,
93 unitPropagationPreconditions, 95 mustUnitPropagationPreconditions,
96 currentUnitPropagationPreconditions,
94 queries.allQueries 97 queries.allQueries
95 ) 98 )
96 } 99 }
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/MultiplicityGoalConstraintCalculator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/MultiplicityGoalConstraintCalculator.xtend
index e05160d0..05ce4f6e 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/MultiplicityGoalConstraintCalculator.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/MultiplicityGoalConstraintCalculator.xtend
@@ -10,23 +10,36 @@ class MultiplicityGoalConstraintCalculator {
10 val String targetRelationName; 10 val String targetRelationName;
11 val IQuerySpecification<?> querySpecification; 11 val IQuerySpecification<?> querySpecification;
12 var ViatraQueryMatcher<?> matcher; 12 var ViatraQueryMatcher<?> matcher;
13 val int minValue
14 val boolean containment
15 val int cost
13 16
14 public new(String targetRelationName, IQuerySpecification<?> querySpecification) { 17 public new(String targetRelationName, IQuerySpecification<?> querySpecification, int minValue, boolean containment, int cost) {
15 this.targetRelationName = targetRelationName 18 this.targetRelationName = targetRelationName
16 this.querySpecification = querySpecification 19 this.querySpecification = querySpecification
17 this.matcher = null 20 this.matcher = null
21 this.minValue = minValue
22 this.containment = containment
23 this.cost = cost
18 } 24 }
19 25
20 public new(MultiplicityGoalConstraintCalculator other) { 26 public new(MultiplicityGoalConstraintCalculator other) {
21 this.targetRelationName = other.targetRelationName 27 this.targetRelationName = other.targetRelationName
22 this.querySpecification = other.querySpecification 28 this.querySpecification = other.querySpecification
23 this.matcher = null 29 this.matcher = null
30 this.minValue = other.minValue
31 this.containment = other.containment
32 this.cost = other.cost
24 } 33 }
25 34
26 def public getName() { 35 def public getName() {
27 targetRelationName 36 targetRelationName
28 } 37 }
29 38
39 def isContainment() {
40 return containment
41 }
42
30 def public init(Notifier notifier) { 43 def public init(Notifier notifier) {
31 val engine = ViatraQueryEngine.on(new EMFScope(notifier)) 44 val engine = ViatraQueryEngine.on(new EMFScope(notifier))
32 matcher = querySpecification.getMatcher(engine) 45 matcher = querySpecification.getMatcher(engine)
@@ -36,11 +49,18 @@ class MultiplicityGoalConstraintCalculator {
36 var res = 0 49 var res = 0
37 val allMatches = this.matcher.allMatches 50 val allMatches = this.matcher.allMatches
38 for(match : allMatches) { 51 for(match : allMatches) {
39 //println(targetRelationName+ " missing multiplicity: "+match.get(3)) 52
40 val missingMultiplicity = match.get(4) as Integer 53 val existingMultiplicity = match.get(4) as Integer
41 res += missingMultiplicity 54 if(existingMultiplicity < this.minValue) {
55 val missingMultiplicity = this.minValue-existingMultiplicity
56 res += missingMultiplicity
57 }
58// if(missingMultiplicity!=0) {
59// println(targetRelationName+ " missing multiplicity: "+missingMultiplicity)
60// }
42 } 61 }
43 //println(targetRelationName+ " all missing multiplicities: "+res) 62// if(res>0)
44 return res 63// println(targetRelationName+ " all missing multiplicities: "+res + "*"+cost+"="+res*cost)
64 return res*cost
45 } 65 }
46} \ No newline at end of file 66} \ No newline at end of file
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ScopePropagator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ScopePropagator.xtend
index df38337e..8012776f 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ScopePropagator.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ScopePropagator.xtend
@@ -8,6 +8,7 @@ import java.util.Map
8import java.util.Set 8import java.util.Set
9import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialComplexTypeInterpretation 9import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialComplexTypeInterpretation
10import java.util.HashSet 10import java.util.HashSet
11import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialPrimitiveInterpretation
11 12
12class ScopePropagator { 13class ScopePropagator {
13 PartialInterpretation partialInterpretation 14 PartialInterpretation partialInterpretation
@@ -61,37 +62,42 @@ class ScopePropagator {
61 } 62 }
62 63
63 def public propagateAdditionToType(PartialTypeInterpratation t) { 64 def public propagateAdditionToType(PartialTypeInterpratation t) {
64// println('''Adding to «(t as PartialComplexTypeInterpretation).interpretationOf.name»''') 65 val isPrimitive = t instanceof PartialPrimitiveInterpretation || t === null
65 val targetScope = type2Scope.get(t) 66 if(!isPrimitive) {
66 if(targetScope!==null) { 67 // println('''Adding to «(t as PartialComplexTypeInterpretation).interpretationOf.name»''')
67 targetScope.removeOne 68 val targetScope = type2Scope.get(t)
68 val sups = superScopes.get(targetScope) 69 if(targetScope!==null) {
69 sups.forEach[removeOne] 70 targetScope.removeOne
70 } 71 val sups = superScopes.get(targetScope)
71 72 sups.forEach[removeOne]
72 if(this.partialInterpretation.minNewElements > 0) { 73 }
73 this.partialInterpretation.minNewElements = this.partialInterpretation.minNewElements-1 74
74 } 75
75 if(this.partialInterpretation.maxNewElements > 0) { 76 if(this.partialInterpretation.minNewElements > 0 ) {
76 this.partialInterpretation.maxNewElements = this.partialInterpretation.maxNewElements-1 77 this.partialInterpretation.minNewElements = this.partialInterpretation.minNewElements-1
77 } else if(this.partialInterpretation.maxNewElements === 0) { 78 }
78 throw new IllegalArgumentException('''Inconsistent object creation: lower node limit is 0!''') 79 if(this.partialInterpretation.maxNewElements > 0) {
80 this.partialInterpretation.maxNewElements = this.partialInterpretation.maxNewElements-1
81 } else if(this.partialInterpretation.maxNewElements === 0) {
82 this.partialInterpretation.maxNewElements = 0
83 //throw new IllegalArgumentException('''Inconsistent object creation: lower node limit is 0!''')
84 }
85
86 // subScopes.get(targetScope).forEach[propagateUpperLimitDown(it,targetScope)]
87 // for(sup: sups) {
88 // subScopes.get(sup).forEach[propagateUpperLimitDown(it,sup)]
89 // }
90 // for(scope : type2Scope.values) {
91 // propagateUpperLimitDown(scope,partialInterpretation)
92 // }
93
94 propagateAllScopeConstraints
95
96 // println('''Target Scope: «targetScope.minNewElements» - «targetScope.maxNewElements»''')
97 // println(''' «this.partialInterpretation.minNewElements» - «this.partialInterpretation.maxNewElements»''')
98 // this.partialInterpretation.scopes.forEach[println(''' «(it.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name»: «it.minNewElements»-«it.maxNewElements»''')]
99 // println('''All constraints are propagated upon increasing «(t as PartialComplexTypeInterpretation).interpretationOf.name»''')
79 } 100 }
80
81// subScopes.get(targetScope).forEach[propagateUpperLimitDown(it,targetScope)]
82// for(sup: sups) {
83// subScopes.get(sup).forEach[propagateUpperLimitDown(it,sup)]
84// }
85// for(scope : type2Scope.values) {
86// propagateUpperLimitDown(scope,partialInterpretation)
87// }
88
89 propagateAllScopeConstraints
90
91// println('''Target Scope: «targetScope.minNewElements» - «targetScope.maxNewElements»''')
92// println(''' «this.partialInterpretation.minNewElements» - «this.partialInterpretation.maxNewElements»''')
93// this.partialInterpretation.scopes.forEach[println(''' «(it.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name»: «it.minNewElements»-«it.maxNewElements»''')]
94// println('''All constraints are propagated upon increasing «(t as PartialComplexTypeInterpretation).interpretationOf.name»''')
95 } 101 }
96 102
97 private def propagateLowerLimitUp(Scope subScope, Scope superScope) { 103 private def propagateLowerLimitUp(Scope subScope, Scope superScope) {
@@ -147,7 +153,8 @@ class ScopePropagator {
147 } 153 }
148 private def removeOne(Scope scope) { 154 private def removeOne(Scope scope) {
149 if(scope.maxNewElements===0) { 155 if(scope.maxNewElements===0) {
150 throw new IllegalArgumentException('''Inconsistent object creation: «scope.targetTypeInterpretation»''') 156 scope.maxNewElements=0
157 //throw new IllegalArgumentException('''Inconsistent object creation: «scope.targetTypeInterpretation»''')
151 } else if(scope.maxNewElements>0) { 158 } else if(scope.maxNewElements>0) {
152 scope.maxNewElements= scope.maxNewElements-1 159 scope.maxNewElements= scope.maxNewElements-1
153 } 160 }
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PConstraintTransformer.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PConstraintTransformer.xtend
index 5ca78e97..dd5cade1 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PConstraintTransformer.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PConstraintTransformer.xtend
@@ -28,6 +28,7 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.StringTypeReference
28import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference 28import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference
29import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntTypeReference 29import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntTypeReference
30import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference 30import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference
31import java.util.Map
31 32
32class PConstraintTransformer { 33class PConstraintTransformer {
33 val extension RelationDefinitionIndexer relationDefinitionIndexer; 34 val extension RelationDefinitionIndexer relationDefinitionIndexer;
@@ -195,7 +196,9 @@ class PConstraintTransformer {
195 def hasValue(PVariable v, String target, Modality m, List<VariableMapping> variableMapping) { 196 def hasValue(PVariable v, String target, Modality m, List<VariableMapping> variableMapping) {
196 val typeReference = variableMapping.filter[it.sourcePVariable === v].head.targetLogicVariable.range as PrimitiveTypeReference 197 val typeReference = variableMapping.filter[it.sourcePVariable === v].head.targetLogicVariable.range as PrimitiveTypeReference
197 if(m.isMay) { 198 if(m.isMay) {
198 '''PrimitiveElement.valueSet(«v.canonizeName»,«v.valueSetted»); «hasValueExpressionByRef(typeReference,v,v.valueVariable)» check(!«v.valueSetted»||«v.valueVariable»==«target»));''' 199 '''PrimitiveElement.valueSet(«v.canonizeName»,«v.valueSetted»); «hasValueExpressionByRef(typeReference,v,v.valueVariable)»
200««« check(!«v.valueSetted»||«v.valueVariable»==«target»));
201'''
199 } else { // Must or current 202 } else { // Must or current
200 '''PrimitiveElement.valueSet(«v.canonizeName»,true);«hasValueExpressionByRef(typeReference,v,target)»''' 203 '''PrimitiveElement.valueSet(«v.canonizeName»,true);«hasValueExpressionByRef(typeReference,v,target)»'''
201 } 204 }
@@ -226,23 +229,28 @@ class PConstraintTransformer {
226 throw new UnsupportedOperationException('''Only check expressions are supported "«e.class.name»"!''') 229 throw new UnsupportedOperationException('''Only check expressions are supported "«e.class.name»"!''')
227 } else { 230 } else {
228 val expression = expressionExtractor.extractExpression(e.evaluator) 231 val expression = expressionExtractor.extractExpression(e.evaluator)
232 val Map<PVariable, PrimitiveTypeReference> variable2Type = e.affectedVariables.toInvertedMap[v|variableMapping.filter[it.sourcePVariable === v].head.targetLogicVariable.range as PrimitiveTypeReference]
229 if(modality.isMay) { 233 if(modality.isMay) {
230 return ''' 234 return '''
231 «FOR variable: e.affectedVariables» 235 «FOR variable: e.affectedVariables»
232 PrimitiveElement.valueSet(«variable.canonizeName»,«variable.valueSetted»); «hasValueExpression(variableMapping,variable,variable.valueVariable)» 236 PrimitiveElement.valueSet(«variable.canonizeName»,«variable.valueSetted»); «hasValueExpression(variableMapping,variable,variable.valueVariable)»
233 «ENDFOR» 237 «ENDFOR»
234 check( 238««« check(
235 «FOR variable: e.affectedVariables SEPARATOR " || "»!«variable.valueSetted»«ENDFOR» 239««« «FOR variable: e.affectedVariables SEPARATOR " || "»!«variable.valueSetted»«ENDFOR»
236 || 240««« «IF variable2Type.values.filter(RealTypeReference).empty»
237 («expressionGenerator.translateExpression(expression,e.affectedVariables.toInvertedMap[valueVariable])») 241««« ||
238 ); 242««« («expressionGenerator.translateExpression(expression,e.affectedVariables.toInvertedMap[valueVariable],variable2Type)»)
243««« «ENDIF»
244««« );
239 ''' 245 '''
240 } else { // Must or Current 246 } else { // Must or Current
241 return ''' 247 return '''
242 «FOR variable: e.affectedVariables» 248 «FOR variable: e.affectedVariables»
243 PrimitiveElement.valueSet(«variable.canonizeName»,true); «hasValueExpression(variableMapping,variable,variable.valueVariable)» 249 PrimitiveElement.valueSet(«variable.canonizeName»,true); «hasValueExpression(variableMapping,variable,variable.valueVariable)»
244 «ENDFOR» 250 «ENDFOR»
245 check(«expressionGenerator.translateExpression(expression,e.affectedVariables.toInvertedMap[valueVariable])»); 251««« «IF variable2Type.values.filter(RealTypeReference).empty»
252««« check(«expressionGenerator.translateExpression(expression,e.affectedVariables.toInvertedMap[valueVariable],variable2Type)»);
253««« «ENDIF»
246 ''' 254 '''
247 } 255 }
248 } 256 }
@@ -257,7 +265,7 @@ class PConstraintTransformer {
257 «FOR variable: e.affectedVariables» 265 «FOR variable: e.affectedVariables»
258 PrimitiveElement.valueSet(«variable.canonizeName»,«variable.valueSetted»); «hasValueExpression(variableMapping,variable,variable.valueVariable)» 266 PrimitiveElement.valueSet(«variable.canonizeName»,«variable.valueSetted»); «hasValueExpression(variableMapping,variable,variable.valueVariable)»
259 «ENDFOR» 267 «ENDFOR»
260 check(«FOR variable: e.affectedVariables SEPARATOR " || "»!«variable.valueSetted»«ENDFOR»); 268««« check(«FOR variable: e.affectedVariables SEPARATOR " || "»!«variable.valueSetted»«ENDFOR»);
261 ''' 269 '''
262 } 270 }
263 271
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PExpressionGenerator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PExpressionGenerator.xtend
index 303c87b9..62ff92b2 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PExpressionGenerator.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PExpressionGenerator.xtend
@@ -8,6 +8,8 @@ import org.eclipse.xtext.xbase.XFeatureCall
8import org.eclipse.xtext.xbase.XMemberFeatureCall 8import org.eclipse.xtext.xbase.XMemberFeatureCall
9import org.eclipse.xtext.xbase.XNumberLiteral 9import org.eclipse.xtext.xbase.XNumberLiteral
10import org.eclipse.xtext.xbase.XUnaryOperation 10import org.eclipse.xtext.xbase.XUnaryOperation
11import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.PrimitiveTypeReference
12import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference
11 13
12class PExpressionGenerator { 14class PExpressionGenerator {
13 static val N_Base = "org.eclipse.xtext.xbase.lib." 15 static val N_Base = "org.eclipse.xtext.xbase.lib."
@@ -38,9 +40,9 @@ class PExpressionGenerator {
38 40
39 static val N_POWER2 = "java.lang.Math.pow" 41 static val N_POWER2 = "java.lang.Math.pow"
40 42
41 def dispatch CharSequence translateExpression(XBinaryOperation e, Map<PVariable,String> valueName) { 43 def dispatch CharSequence translateExpression(XBinaryOperation e, Map<PVariable,String> valueName, Map<PVariable, PrimitiveTypeReference> variable2Type) {
42 val left = e.leftOperand.translateExpression(valueName) 44 val left = e.leftOperand.translateExpression(valueName,variable2Type)
43 val right = e.rightOperand.translateExpression(valueName) 45 val right = e.rightOperand.translateExpression(valueName,variable2Type)
44 val feature = e.feature.qualifiedName 46 val feature = e.feature.qualifiedName
45 if(feature.isN(N_MINUS2)) { return '''(«left»-«right»)'''} 47 if(feature.isN(N_MINUS2)) { return '''(«left»-«right»)'''}
46 else if(feature.isN(N_PLUS2)) { return '''(«left»+«right»)''' } 48 else if(feature.isN(N_PLUS2)) { return '''(«left»+«right»)''' }
@@ -65,8 +67,8 @@ class PExpressionGenerator {
65 } 67 }
66 } 68 }
67 69
68 def dispatch CharSequence translateExpression(XUnaryOperation e, Map<PVariable,String> valueName) { 70 def dispatch CharSequence translateExpression(XUnaryOperation e, Map<PVariable,String> valueName, Map<PVariable, PrimitiveTypeReference> variable2Type) {
69 val operand = e.operand.translateExpression(valueName) 71 val operand = e.operand.translateExpression(valueName,variable2Type)
70 val feature = e.feature.qualifiedName 72 val feature = e.feature.qualifiedName
71 if(feature.isN(N_MINUS1)) { return '''(-«operand»)'''} 73 if(feature.isN(N_MINUS1)) { return '''(-«operand»)'''}
72 else if(feature.isN(N_PLUS1)) { return '''(+«operand»)'''} 74 else if(feature.isN(N_PLUS1)) { return '''(+«operand»)'''}
@@ -78,8 +80,8 @@ class PExpressionGenerator {
78 } 80 }
79 } 81 }
80 82
81 def dispatch CharSequence translateExpression(XMemberFeatureCall e, Map<PVariable,String> valueName) { 83 def dispatch CharSequence translateExpression(XMemberFeatureCall e, Map<PVariable,String> valueName, Map<PVariable, PrimitiveTypeReference> variable2Type) {
82 val transformedArguments = e.actualArguments.map[translateExpression(valueName)] 84 val transformedArguments = e.actualArguments.map[translateExpression(valueName,variable2Type)]
83 val feature = e.feature.qualifiedName 85 val feature = e.feature.qualifiedName
84 if(feature == N_POWER2) { 86 if(feature == N_POWER2) {
85 return '''Math.pow(«transformedArguments.get(0)»,«transformedArguments.get(1)»)''' 87 return '''Math.pow(«transformedArguments.get(0)»,«transformedArguments.get(1)»)'''
@@ -91,19 +93,24 @@ class PExpressionGenerator {
91 } 93 }
92 } 94 }
93 95
94 def dispatch CharSequence translateExpression(XFeatureCall e, Map<PVariable,String> valueName) { 96 def dispatch CharSequence translateExpression(XFeatureCall e, Map<PVariable,String> valueName, Map<PVariable, PrimitiveTypeReference> variable2Type) {
95 val featureName = e.feature.qualifiedName 97 val featureName = e.feature.qualifiedName
98 val type = variable2Type.entrySet.filter[it.key.name===featureName].head.value
96 val entryWithName = valueName.entrySet.filter[it.key.name == featureName].head 99 val entryWithName = valueName.entrySet.filter[it.key.name == featureName].head
97 if(entryWithName !== null) { 100 if(entryWithName !== null) {
98 return entryWithName.value 101 if(type instanceof RealTypeReference) {
102 return '''(«entryWithName.value».doubleValue)'''
103 } else {
104 return entryWithName.value
105 }
99 } else { 106 } else {
100 throw new IllegalArgumentException('''Feature call reference to unavailable variable "«featureName»"''') 107 throw new IllegalArgumentException('''Feature call reference to unavailable variable "«featureName»"''')
101 } 108 }
102 } 109 }
103 110
104 def dispatch CharSequence translateExpression(XNumberLiteral l, Map<PVariable,String> valueName) '''«l.value»''' 111 def dispatch CharSequence translateExpression(XNumberLiteral l, Map<PVariable,String> valueName, Map<PVariable, PrimitiveTypeReference> variable2Type) '''«l.value»'''
105 112
106 def dispatch CharSequence translateExpression(XExpression expression, Map<PVariable,String> valueName) { 113 def dispatch CharSequence translateExpression(XExpression expression, Map<PVariable,String> valueName, Map<PVariable, PrimitiveTypeReference> variable2Type) {
107 throw new UnsupportedOperationException('''Unsupported expression in check or eval: «expression.class.name», «expression»"''') 114 throw new UnsupportedOperationException('''Unsupported expression in check or eval: «expression.class.name», «expression»"''')
108 } 115 }
109} \ No newline at end of file 116} \ No newline at end of file
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..677170b8 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
26import org.eclipse.xtend.lib.annotations.Accessors 26import org.eclipse.xtend.lib.annotations.Accessors
27 27
28import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* 28import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
29import org.eclipse.xtend.lib.annotations.Data
30import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint
31
32@Data class PatternGeneratorResult {
33 CharSequence patternText
34 HashMap<PConstraint,String> constraint2MustPreconditionName
35 HashMap<PConstraint,String> constraint2CurrentPreconditionName
36}
29 37
30class PatternGenerator { 38class PatternGenerator {
31 @Accessors(PUBLIC_GETTER) val TypeIndexer typeIndexer //= new TypeIndexer(this) 39 @Accessors(PUBLIC_GETTER) val TypeIndexer typeIndexer //= new TypeIndexer(this)
@@ -149,7 +157,7 @@ class PatternGenerator {
149 problem.allTypeReferences.exists[it instanceof StringTypeReference] 157 problem.allTypeReferences.exists[it instanceof StringTypeReference]
150 } 158 }
151 159
152 public def transformBaseProperties( 160 public def PatternGeneratorResult transformBaseProperties(
153 LogicProblem problem, 161 LogicProblem problem,
154 PartialInterpretation emptySolution, 162 PartialInterpretation emptySolution,
155 Map<String,PQuery> fqn2PQuery, 163 Map<String,PQuery> fqn2PQuery,
@@ -207,66 +215,42 @@ class PatternGenerator {
207 find mayExist(problem,interpretation,a); 215 find mayExist(problem,interpretation,a);
208 find mayExist(problem,interpretation,b); 216 find mayExist(problem,interpretation,b);
209 a == b; 217 a == b;
210 } or { 218««« } or {
211 find mayExist(problem,interpretation,a); 219««« find mayExist(problem,interpretation,a);
212 find mayExist(problem,interpretation,b); 220««« find mayExist(problem,interpretation,b);
213 IntegerElement(a); 221««« IntegerElement(a);
214 IntegerElement(b); 222««« IntegerElement(b);
215 PrimitiveElement.valueSet(a,false); 223««« PrimitiveElement.valueSet(a,false);
216 } or { 224««« } or {
217 find mayExist(problem,interpretation,a); 225««« find mayExist(problem,interpretation,a);
218 find mayExist(problem,interpretation,b); 226««« find mayExist(problem,interpretation,b);
219 IntegerElement(a); 227««« IntegerElement(a);
220 IntegerElement(b); 228««« IntegerElement(b);
221 PrimitiveElement.valueSet(b,false); 229««« PrimitiveElement.valueSet(b,false);
222 } or { 230««« } or {
223 find mayExist(problem,interpretation,a); 231««« find mayExist(problem,interpretation,a);
224 find mayExist(problem,interpretation,b); 232««« find mayExist(problem,interpretation,b);
225 RealElement(a); 233««« RealElement(a);
226 RealElement(b); 234««« RealElement(b);
227 PrimitiveElement.valueSet(a,false); 235««« PrimitiveElement.valueSet(a,false);
228 } or { 236««« } or {
229 find mayExist(problem,interpretation,a); 237««« find mayExist(problem,interpretation,a);
230 find mayExist(problem,interpretation,b); 238««« find mayExist(problem,interpretation,b);
231 RealElement(a); 239««« RealElement(a);
232 RealElement(b); 240««« RealElement(b);
233 PrimitiveElement.valueSet(b,false); 241««« PrimitiveElement.valueSet(b,false);
234 } or { 242««« } or {
235 find mayExist(problem,interpretation,a); 243««« find mayExist(problem,interpretation,a);
236 find mayExist(problem,interpretation,b); 244««« find mayExist(problem,interpretation,b);
237 RealElement(a); 245««« StringElement(a);
238 IntegerElement(b); 246««« StringElement(b);
239 PrimitiveElement.valueSet(a,false); 247««« PrimitiveElement.valueSet(a,false);
240 } or { 248««« } or {
241 find mayExist(problem,interpretation,a); 249««« find mayExist(problem,interpretation,a);
242 find mayExist(problem,interpretation,b); 250««« find mayExist(problem,interpretation,b);
243 RealElement(a); 251««« StringElement(a);
244 IntegerElement(b); 252««« StringElement(b);
245 PrimitiveElement.valueSet(b,false); 253««« PrimitiveElement.valueSet(b,false);
246 } or {
247 find mayExist(problem,interpretation,a);
248 find mayExist(problem,interpretation,b);
249 IntegerElement(a);
250 RealElement(b);
251 PrimitiveElement.valueSet(a,false);
252 } or {
253 find mayExist(problem,interpretation,a);
254 find mayExist(problem,interpretation,b);
255 IntegerElement(a);
256 RealElement(b);
257 PrimitiveElement.valueSet(b,false);
258 } or {
259 find mayExist(problem,interpretation,a);
260 find mayExist(problem,interpretation,b);
261 StringElement(a);
262 StringElement(b);
263 PrimitiveElement.valueSet(a,false);
264 } or {
265 find mayExist(problem,interpretation,a);
266 find mayExist(problem,interpretation,b);
267 StringElement(a);
268 StringElement(b);
269 PrimitiveElement.valueSet(b,false);
270 } 254 }
271 255
272 pattern mustEquivalent(problem:LogicProblem, interpretation:PartialInterpretation, a: DefinedElement, b: DefinedElement) { 256 pattern mustEquivalent(problem:LogicProblem, interpretation:PartialInterpretation, a: DefinedElement, b: DefinedElement) {
@@ -274,41 +258,27 @@ class PatternGenerator {
274 find mustExist(problem,interpretation,a); 258 find mustExist(problem,interpretation,a);
275 find mustExist(problem,interpretation,b); 259 find mustExist(problem,interpretation,b);
276 a == b; 260 a == b;
277 } or { 261««« } or {
278 find mustExist(problem,interpretation,a); 262««« find mustExist(problem,interpretation,a);
279 find mustExist(problem,interpretation,b); 263««« find mustExist(problem,interpretation,b);
280 PrimitiveElement.valueSet(a,true); 264««« PrimitiveElement.valueSet(a,true);
281 PrimitiveElement.valueSet(b,true); 265««« PrimitiveElement.valueSet(b,true);
282 IntegerElement.value(a,value); 266««« IntegerElement.value(a,value);
283 IntegerElement.value(b,value); 267««« IntegerElement.value(b,value);
284 } or { 268««« } or {
285 find mustExist(problem,interpretation,a); 269««« find mustExist(problem,interpretation,a);
286 find mustExist(problem,interpretation,b); 270««« find mustExist(problem,interpretation,b);
287 PrimitiveElement.valueSet(a,true); 271««« PrimitiveElement.valueSet(a,true);
288 PrimitiveElement.valueSet(b,true); 272««« PrimitiveElement.valueSet(b,true);
289 RealElement.value(a,value); 273««« RealElement.value(a,value);
290 RealElement.value(b,value); 274««« RealElement.value(b,value);
291 } or { 275««« } or {
292 find mustExist(problem,interpretation,a); 276««« find mustExist(problem,interpretation,a);
293 find mustExist(problem,interpretation,b); 277««« find mustExist(problem,interpretation,b);
294 PrimitiveElement.valueSet(a,true); 278««« PrimitiveElement.valueSet(a,true);
295 PrimitiveElement.valueSet(b,true); 279««« PrimitiveElement.valueSet(b,true);
296 RealElement.value(a,value); 280««« StringElement.value(a,value);
297 IntegerElement.value(b,value); 281««« StringElement.value(b,value);
298 } or {
299 find mustExist(problem,interpretation,a);
300 find mustExist(problem,interpretation,b);
301 PrimitiveElement.valueSet(a,true);
302 PrimitiveElement.valueSet(b,true);
303 IntegerElement.value(a,value);
304 RealElement.value(b,value);
305 } or {
306 find mustExist(problem,interpretation,a);
307 find mustExist(problem,interpretation,b);
308 PrimitiveElement.valueSet(a,true);
309 PrimitiveElement.valueSet(b,true);
310 StringElement.value(a,value);
311 StringElement.value(b,value);
312 } 282 }
313 283
314 ////////// 284 //////////
@@ -398,6 +368,6 @@ class PatternGenerator {
398 ''' 368 '''
399 val up = unitPropagationPreconditionGenerator.generateUnitPropagationRules(problem,problem.relations.filter(RelationDefinition),fqn2PQuery) 369 val up = unitPropagationPreconditionGenerator.generateUnitPropagationRules(problem,problem.relations.filter(RelationDefinition),fqn2PQuery)
400 val second = up.definitions 370 val second = up.definitions
401 return (first+second) -> up.constraint2PreconditionName 371 return new PatternGeneratorResult(first+second,up.constraint2MustPreconditionName,up.constraint2CurrentPreconditionName)
402 } 372 }
403} 373}
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..f3de4ccc 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
@@ -27,11 +27,13 @@ import java.util.HashMap
27@Data class GeneratedPatterns { 27@Data class GeneratedPatterns {
28 public Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidWFQueries 28 public Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidWFQueries
29 public Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWFQueries 29 public Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWFQueries
30 public Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedMulticiplicityQueries 30 public Map<Relation, Pair<IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>,Integer>> unfinishedContainmentMulticiplicityQueries
31 public Map<Relation, Pair<IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>,Integer>> unfinishedNonContainmentMulticiplicityQueries
31 public Map<ObjectCreationPrecondition, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineObjectQueries 32 public Map<ObjectCreationPrecondition, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineObjectQueries
32 public Map<? extends Type, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineTypeQueries 33 public Map<? extends Type, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineTypeQueries
33 public Map<Pair<RelationDeclaration, Relation>, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refinerelationQueries 34 public Map<Pair<RelationDeclaration, Relation>, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refinerelationQueries
34 public Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unitPropagationPreconditionPatterns 35 public Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> mustUnitPropagationPreconditionPatterns
36 public Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> currentUnitPropagationPreconditionPatterns
35 public Collection<IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allQueries 37 public Collection<IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allQueries
36} 38}
37 39
@@ -60,14 +62,15 @@ class PatternProvider {
60 null 62 null
61 } 63 }
62 val patternGeneratorResult = patternGenerator.transformBaseProperties(problem,emptySolution,fqn2Query,typeAnalysisResult) 64 val patternGeneratorResult = patternGenerator.transformBaseProperties(problem,emptySolution,fqn2Query,typeAnalysisResult)
63 val baseIndexerFile = patternGeneratorResult.key 65 val baseIndexerFile = patternGeneratorResult.patternText
64 val unitPropagationTrace = patternGeneratorResult.value 66 val mustUnitPropagationTrace = patternGeneratorResult.constraint2MustPreconditionName
67 val currentUnitPropagationTrace = patternGeneratorResult.constraint2CurrentPreconditionName
65 if(writeToFile) { 68 if(writeToFile) {
66 workspace.writeText('''generated3valued.vql_deactivated''',baseIndexerFile) 69 workspace.writeText('''generated3valued.vql_deactivated''',baseIndexerFile)
67 } 70 }
68 val ParseUtil parseUtil = new ParseUtil 71 val ParseUtil parseUtil = new ParseUtil
69 val generatedQueries = parseUtil.parse(baseIndexerFile) 72 val generatedQueries = parseUtil.parse(baseIndexerFile)
70 val runtimeQueries = calclulateRuntimeQueries(patternGenerator,problem,emptySolution,typeAnalysisResult,unitPropagationTrace,generatedQueries); 73 val runtimeQueries = calclulateRuntimeQueries(patternGenerator,problem,emptySolution,typeAnalysisResult,mustUnitPropagationTrace,currentUnitPropagationTrace,generatedQueries);
71 return runtimeQueries 74 return runtimeQueries
72 } 75 }
73 76
@@ -76,15 +79,33 @@ class PatternProvider {
76 LogicProblem problem, 79 LogicProblem problem,
77 PartialInterpretation emptySolution, 80 PartialInterpretation emptySolution,
78 TypeAnalysisResult typeAnalysisResult, 81 TypeAnalysisResult typeAnalysisResult,
79 HashMap<PConstraint, String> unitPropagationTrace, 82 HashMap<PConstraint, String> mustUnitPropagationTrace,
83 HashMap<PConstraint, String> currentUnitPropagationTrace,
80 Map<String, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> queries 84 Map<String, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> queries
81 ) { 85 ) {
82 val Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> 86 val Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>>
83 invalidWFQueries = patternGenerator.invalidIndexer.getInvalidateByWfQueryNames(problem).mapValues[it.lookup(queries)] 87 invalidWFQueries = patternGenerator.invalidIndexer.getInvalidateByWfQueryNames(problem).mapValues[it.lookup(queries)]
84 val Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> 88 val Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>>
85 unfinishedWFQueries = patternGenerator.unfinishedIndexer.getUnfinishedWFQueryNames(problem).mapValues[it.lookup(queries)] 89 unfinishedWFQueries = patternGenerator.unfinishedIndexer.getUnfinishedWFQueryNames(problem).mapValues[it.lookup(queries)]
86 val Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> 90
87 unfinishedMultiplicityQueries = patternGenerator.unfinishedIndexer.getUnfinishedMultiplicityQueries(problem).mapValues[it.lookup(queries)] 91 val unfinishedMultiplicities = patternGenerator.unfinishedIndexer.getUnfinishedMultiplicityQueries(problem)
92 val unfinishedContainmentMultiplicities = new HashMap
93 val unfinishedNonContainmentMultiplicities = new HashMap
94 for(entry : unfinishedMultiplicities.entrySet) {
95 val relation = entry.key
96 val name = entry.value.key
97 val amount = entry.value.value
98 val query = name.lookup(queries)
99 if(problem.containmentHierarchies.head.containmentRelations.contains(relation)) {
100 unfinishedContainmentMultiplicities.put(relation,query->amount)
101 } else {
102 unfinishedNonContainmentMultiplicities.put(relation,query->amount)
103 }
104 }
105// val Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>>
106// unfinishedMultiplicityQueries = patternGenerator.unfinishedIndexer.getUnfinishedMultiplicityQueries(problem).mapValues[it.lookup(queries)]
107//
108
88 val Map<ObjectCreationPrecondition, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> 109 val Map<ObjectCreationPrecondition, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>>
89 refineObjectsQueries = patternGenerator.typeRefinementGenerator.getRefineObjectQueryNames(problem,emptySolution,typeAnalysisResult).mapValues[it.lookup(queries)] 110 refineObjectsQueries = patternGenerator.typeRefinementGenerator.getRefineObjectQueryNames(problem,emptySolution,typeAnalysisResult).mapValues[it.lookup(queries)]
90 val Map<? extends Type, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> 111 val Map<? extends Type, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>>
@@ -92,15 +113,19 @@ class PatternProvider {
92 val Map<Pair<RelationDeclaration, Relation>, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> 113 val Map<Pair<RelationDeclaration, Relation>, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>>
93 refineRelationQueries = patternGenerator.relationRefinementGenerator.getRefineRelationQueries(problem).mapValues[it.lookup(queries)] 114 refineRelationQueries = patternGenerator.relationRefinementGenerator.getRefineRelationQueries(problem).mapValues[it.lookup(queries)]
94 val Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> 115 val Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>>
95 unitPropagationPreconditionPatterns = unitPropagationTrace.mapValues[it.lookup(queries)] 116 mustUnitPropagationPreconditionPatterns = mustUnitPropagationTrace.mapValues[it.lookup(queries)]
117 val Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>>
118 currentUnitPropagationPreconditionPatterns = currentUnitPropagationTrace.mapValues[it.lookup(queries)]
96 return new GeneratedPatterns( 119 return new GeneratedPatterns(
97 invalidWFQueries, 120 invalidWFQueries,
98 unfinishedWFQueries, 121 unfinishedWFQueries,
99 unfinishedMultiplicityQueries, 122 unfinishedContainmentMultiplicities,
123 unfinishedNonContainmentMultiplicities,
100 refineObjectsQueries, 124 refineObjectsQueries,
101 refineTypeQueries, 125 refineTypeQueries,
102 refineRelationQueries, 126 refineRelationQueries,
103 unitPropagationPreconditionPatterns, 127 mustUnitPropagationPreconditionPatterns,
128 currentUnitPropagationPreconditionPatterns,
104 queries.values 129 queries.values
105 ) 130 )
106 } 131 }
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDeclarationIndexer.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDeclarationIndexer.xtend
index f384cd50..cef707c5 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDeclarationIndexer.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDeclarationIndexer.xtend
@@ -90,13 +90,13 @@ class RelationDeclarationIndexer {
90 // There are "numberOfExistingReferences" currently existing instances of the reference from the source, 90 // There are "numberOfExistingReferences" currently existing instances of the reference from the source,
91 // the upper bound of the multiplicity should be considered. 91 // the upper bound of the multiplicity should be considered.
92 numberOfExistingReferences == count «referRelation(relation,"source","_",Modality.MUST)» 92 numberOfExistingReferences == count «referRelation(relation,"source","_",Modality.MUST)»
93 check(numberOfExistingReferences < «upperMultiplicities.get(relation)»); 93 numberOfExistingReferences != «upperMultiplicities.get(relation)»;
94 «ENDIF» 94 «ENDIF»
95 «IF inverseRelations.containsKey(relation) && upperMultiplicities.containsKey(inverseRelations.get(relation))» 95 «IF inverseRelations.containsKey(relation) && upperMultiplicities.containsKey(inverseRelations.get(relation))»
96 // There are "numberOfExistingReferences" currently existing instances of the reference to the target, 96 // There are "numberOfExistingReferences" currently existing instances of the reference to the target,
97 // the upper bound of the opposite reference multiplicity should be considered. 97 // the upper bound of the opposite reference multiplicity should be considered.
98 numberOfExistingOppositeReferences == count «base.referRelation(inverseRelations.get(relation),"target","_",Modality.MUST,fqn2PQuery)» 98 numberOfExistingOppositeReferences == count «base.referRelation(inverseRelations.get(relation),"target","_",Modality.MUST,fqn2PQuery)»
99 check(numberOfExistingOppositeReferences < «upperMultiplicities.get(inverseRelations.get(relation))»); 99 numberOfExistingOppositeReferences != «upperMultiplicities.get(inverseRelations.get(relation))»;
100 «ENDIF» 100 «ENDIF»
101 «IF containments.contains(relation)» 101 «IF containments.contains(relation)»
102 // The reference is containment, then a new reference cannot be create if: 102 // The reference is containment, then a new reference cannot be create if:
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnfinishedIndexer.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnfinishedIndexer.xtend
index ad1c9033..1df402fa 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnfinishedIndexer.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnfinishedIndexer.xtend
@@ -46,14 +46,14 @@ class UnfinishedIndexer {
46 val lowerMultiplicities = base.lowerMultiplicities(problem) 46 val lowerMultiplicities = base.lowerMultiplicities(problem)
47 return ''' 47 return '''
48 «FOR lowerMultiplicity : lowerMultiplicities» 48 «FOR lowerMultiplicity : lowerMultiplicities»
49 pattern «unfinishedMultiplicityName(lowerMultiplicity)»(problem:LogicProblem, interpretation:PartialInterpretation, relationIterpretation:PartialRelationInterpretation, object:DefinedElement,missingMultiplicity) { 49 pattern «unfinishedMultiplicityName(lowerMultiplicity)»(problem:LogicProblem, interpretation:PartialInterpretation, relationIterpretation:PartialRelationInterpretation, object:DefinedElement,numberOfExistingReferences) {
50 find interpretation(problem,interpretation); 50 find interpretation(problem,interpretation);
51 PartialInterpretation.partialrelationinterpretation(interpretation,relationIterpretation); 51 PartialInterpretation.partialrelationinterpretation(interpretation,relationIterpretation);
52 PartialRelationInterpretation.interpretationOf.name(relationIterpretation,"«lowerMultiplicity.relation.name»"); 52 PartialRelationInterpretation.interpretationOf.name(relationIterpretation,"«lowerMultiplicity.relation.name»");
53 «base.typeIndexer.referInstanceOf(lowerMultiplicity.firstParamTypeOfRelation,Modality::MUST,"object")» 53 «base.typeIndexer.referInstanceOf(lowerMultiplicity.firstParamTypeOfRelation,Modality::MUST,"object")»
54 numberOfExistingReferences == count «base.referRelation(lowerMultiplicity.relation,"object","_",Modality.MUST,fqn2PQuery)» 54 numberOfExistingReferences == count «base.referRelation(lowerMultiplicity.relation,"object","_",Modality.MUST,fqn2PQuery)»
55 check(numberOfExistingReferences < «lowerMultiplicity.lower»); 55««« numberOfExistingReferences < «lowerMultiplicity.lower»;
56 missingMultiplicity == eval(«lowerMultiplicity.lower»-numberOfExistingReferences); 56««« missingMultiplicity == eval(«lowerMultiplicity.lower»-numberOfExistingReferences);
57 } 57 }
58 «ENDFOR» 58 «ENDFOR»
59 ''' 59 '''
@@ -61,8 +61,8 @@ class UnfinishedIndexer {
61 def String unfinishedMultiplicityName(LowerMultiplicityAssertion lowerMultiplicityAssertion) 61 def String unfinishedMultiplicityName(LowerMultiplicityAssertion lowerMultiplicityAssertion)
62 '''unfinishedLowerMultiplicity_«base.canonizeName(lowerMultiplicityAssertion.relation.name)»''' 62 '''unfinishedLowerMultiplicity_«base.canonizeName(lowerMultiplicityAssertion.relation.name)»'''
63 63
64 def public referUnfinishedMultiplicityQuery(LowerMultiplicityAssertion lowerMultiplicityAssertion) 64 //def public referUnfinishedMultiplicityQuery(LowerMultiplicityAssertion lowerMultiplicityAssertion)
65 '''find «unfinishedMultiplicityName(lowerMultiplicityAssertion)»(problem, interpretation ,object, missingMultiplicity);''' 65 // '''find «unfinishedMultiplicityName(lowerMultiplicityAssertion)»(problem, interpretation ,object, missingMultiplicity);'''
66 66
67 def getFirstParamTypeOfRelation(LowerMultiplicityAssertion lowerMultiplicityAssertion) { 67 def getFirstParamTypeOfRelation(LowerMultiplicityAssertion lowerMultiplicityAssertion) {
68 val parameters = lowerMultiplicityAssertion.relation.parameters 68 val parameters = lowerMultiplicityAssertion.relation.parameters
@@ -78,7 +78,7 @@ class UnfinishedIndexer {
78 val lowerMultiplicities = base.lowerMultiplicities(problem) 78 val lowerMultiplicities = base.lowerMultiplicities(problem)
79 val map = new LinkedHashMap 79 val map = new LinkedHashMap
80 for(lowerMultiplicity : lowerMultiplicities) { 80 for(lowerMultiplicity : lowerMultiplicities) {
81 map.put(lowerMultiplicity.relation,unfinishedMultiplicityName(lowerMultiplicity)) 81 map.put(lowerMultiplicity.relation,unfinishedMultiplicityName(lowerMultiplicity)->lowerMultiplicity.lower)
82 } 82 }
83 return map 83 return map
84 } 84 }
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..400f47bc 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 {
61@Data 61@Data
62class UnitPropagationPreconditionFinalResult { 62class UnitPropagationPreconditionFinalResult {
63 CharSequence definitions 63 CharSequence definitions
64 HashMap<PConstraint,String> constraint2PreconditionName 64 HashMap<PConstraint,String> constraint2MustPreconditionName
65 HashMap<PConstraint,String> constraint2CurrentPreconditionName
65} 66}
66 67
67class UnitPropagationPreconditionGenerator { 68class UnitPropagationPreconditionGenerator {
@@ -81,25 +82,34 @@ class UnitPropagationPreconditionGenerator {
81 // Create an empty result 82 // Create an empty result
82 val res = new UnitPropagationPreconditionGenerationResult 83 val res = new UnitPropagationPreconditionGenerationResult
83 val wfs = base.wfQueries(problem)//.map[it.patternPQuery] 84 val wfs = base.wfQueries(problem)//.map[it.patternPQuery]
84 val Map<PConstraint,List<Pair<String,Integer>>> mainPropagationNames = new HashMap 85 val Map<PConstraint,List<Pair<String,Integer>>> mainMustPropagationNames = new HashMap
86 val Map<PConstraint,List<Pair<String,Integer>>> mainCurrentPropagationNames = new HashMap
85 for(wf : wfs) { 87 for(wf : wfs) {
86 val query = wf.patternPQuery as PQuery 88 val query = wf.patternPQuery as PQuery
87 val relation = wf.target 89 val relation = wf.target
88 val allReferredChecks = allReferredConstraints(relation,query).filter(ExpressionEvaluation) 90 val allReferredChecks = allReferredConstraints(relation,query).filter(ExpressionEvaluation)
89 91
90 for(referredCheck : allReferredChecks) { 92 for(referredCheck : allReferredChecks) {
91 val propagationPrecondition = getOrGeneratePropagationRule(res,relation,query,referredCheck,PropagationModality::UP, Modality::MUST) 93 val mustPropagationPrecondition = getOrGeneratePropagationRule(res,relation,query,referredCheck,PropagationModality::UP, Modality::MUST)
92 if(!mainPropagationNames.containsKey(referredCheck)) { 94 val currentPropagationPrecondition = getOrGeneratePropagationRule(res,relation,query,referredCheck,PropagationModality::UP, Modality::CURRENT)
93 mainPropagationNames.put(referredCheck,new LinkedList) 95 if(!mainMustPropagationNames.containsKey(referredCheck)) {
96 mainMustPropagationNames.put(referredCheck,new LinkedList)
94 } 97 }
95 if(propagationPrecondition !== null) { 98 if(!mainCurrentPropagationNames.containsKey(referredCheck)) {
96 mainPropagationNames.get(referredCheck).add(propagationPrecondition->query.parameterNames.size) 99 mainCurrentPropagationNames.put(referredCheck,new LinkedList)
100 }
101 if(mustPropagationPrecondition !== null) {
102 mainMustPropagationNames.get(referredCheck).add(mustPropagationPrecondition->query.parameterNames.size)
103 }
104 if(currentPropagationPrecondition !== null) {
105 mainCurrentPropagationNames.get(referredCheck).add(currentPropagationPrecondition->query.parameterNames.size)
97 } 106 }
98 } 107 }
99 } 108 }
100 val preconditions = new LinkedList 109 val preconditions = new LinkedList
101 val constraint2Precondition = new HashMap 110 val constraint2MustPrecondition = new HashMap
102 for(entry : mainPropagationNames.entrySet) { 111 val constraint2CurrentPrecondition = new HashMap
112 for(entry : mainMustPropagationNames.entrySet) {
103 val name = '''UPMUSTPropagate_«res.getOrGenerateConstraintName(entry.key)»'''; 113 val name = '''UPMUSTPropagate_«res.getOrGenerateConstraintName(entry.key)»''';
104 val def = ''' 114 val def = '''
105 pattern «name»(«FOR index : 1..entry.key.arity SEPARATOR ", "»«canonizeName(index,PropagationModality::UP)»«ENDFOR») 115 pattern «name»(«FOR index : 1..entry.key.arity SEPARATOR ", "»«canonizeName(index,PropagationModality::UP)»«ENDFOR»)
@@ -107,7 +117,17 @@ class UnitPropagationPreconditionGenerator {
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»); } 117 { 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»''' 118 «ENDFOR»'''
109 preconditions+=def 119 preconditions+=def
110 constraint2Precondition.put(entry.key,name) 120 constraint2MustPrecondition.put(entry.key,name)
121 }
122 for(entry : mainCurrentPropagationNames.entrySet) {
123 val name = '''UPCurrentPropagate_«res.getOrGenerateConstraintName(entry.key)»''';
124 val def = '''
125 pattern «name»(«FOR index : 1..entry.key.arity SEPARATOR ", "»«canonizeName(index,PropagationModality::UP)»«ENDFOR»)
126 «FOR propagation : entry.value SEPARATOR " or "»
127 { find «propagation.key»(problem,interpretation,«FOR index : 0..<propagation.value SEPARATOR ','»_«ENDFOR»,«FOR index : 1..entry.key.arity SEPARATOR ", "»«canonizeName(index,PropagationModality::UP)»«ENDFOR»); }
128 «ENDFOR»'''
129 preconditions+=def
130 constraint2CurrentPrecondition.put(entry.key,name)
111 } 131 }
112 132
113 val definitions = ''' 133 val definitions = '''
@@ -121,7 +141,7 @@ class UnitPropagationPreconditionGenerator {
121 «predondition» 141 «predondition»
122 «ENDFOR» 142 «ENDFOR»
123 ''' 143 '''
124 return new UnitPropagationPreconditionFinalResult(definitions,constraint2Precondition) 144 return new UnitPropagationPreconditionFinalResult(definitions,constraint2MustPrecondition,constraint2CurrentPrecondition)
125 } 145 }
126 def allReferredConstraints(Relation relation, PQuery query) { 146 def allReferredConstraints(Relation relation, PQuery query) {
127 val allReferredQueries = query.allReferredQueries 147 val allReferredQueries = query.allReferredQueries
@@ -191,7 +211,7 @@ class UnitPropagationPreconditionGenerator {
191 // Propagation for constraint referred indirectly from this pattern through «referredName» 211 // Propagation for constraint referred indirectly from this pattern through «referredName»
192 find «referredName»(problem, interpretation, 212 find «referredName»(problem, interpretation,
193 «FOR index : 0..<referredPQuery.parameters.size SEPARATOR ", "»«positive.getVariableInTuple(index).canonizeName»«ENDFOR», 213 «FOR index : 0..<referredPQuery.parameters.size SEPARATOR ", "»«positive.getVariableInTuple(index).canonizeName»«ENDFOR»,
194 «FOR index : 0..c.arity SEPARATOR ", "»«canonizeName(index,pm)»«ENDFOR»); 214 «FOR index : 1..c.arity SEPARATOR ", "»«canonizeName(index,pm)»«ENDFOR»);
195 ''' 215 '''
196 } 216 }
197 // Otherwise, if the referred pattern is not satisfiable, this pattern is not satisfiable either 217 // Otherwise, if the referred pattern is not satisfiable, this pattern is not satisfiable either
@@ -214,7 +234,7 @@ class UnitPropagationPreconditionGenerator {
214 // Propagation for constraint referred indirectly from this pattern through «referredName» 234 // Propagation for constraint referred indirectly from this pattern through «referredName»
215 find «referredName»(problem, interpretation, 235 find «referredName»(problem, interpretation,
216 «FOR index : 0..<referredPQuery.parameters.size SEPARATOR ", "»«(negative.actualParametersTuple.get(index) as PVariable).canonizeName»«ENDFOR», 236 «FOR index : 0..<referredPQuery.parameters.size SEPARATOR ", "»«(negative.actualParametersTuple.get(index) as PVariable).canonizeName»«ENDFOR»,
217 «FOR index : 0..c.arity SEPARATOR ", "»«canonizeName(index,pm)»«ENDFOR»); 237 «FOR index : 1..c.arity SEPARATOR ", "»«canonizeName(index,pm)»«ENDFOR»);
218 ''' 238 '''
219 } else { 239 } else {
220 generatedBodies += ''' 240 generatedBodies += '''
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend
index e1be2742..0e8d341a 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend
@@ -1,18 +1,99 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules 1package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules
2 2
3import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.LowerMultiplicityAssertion
4import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference
5import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation
6import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
7import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
3import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.MultiplicityGoalConstraintCalculator 8import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.MultiplicityGoalConstraintCalculator
4import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.GeneratedPatterns 9import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.GeneratedPatterns
5import java.util.ArrayList 10import java.util.ArrayList
11import java.util.HashMap
12import java.util.LinkedList
13import java.util.List
14import java.util.Map
15import org.eclipse.viatra.query.runtime.api.IPatternMatch
16import org.eclipse.viatra.query.runtime.api.IQuerySpecification
17import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher
18
19import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
6 20
7class GoalConstraintProvider { 21class GoalConstraintProvider {
8 def public getUnfinishedMultiplicityQueries(GeneratedPatterns patterns) { 22 val calculateObjectCost = false
9 val multiplicityQueries = patterns.unfinishedMulticiplicityQueries 23
10 val res = new ArrayList(multiplicityQueries.size) 24 def public getUnfinishedMultiplicityQueries(LogicProblem p, GeneratedPatterns patterns) {
11 for(multiplicityQuery : multiplicityQueries.entrySet) { 25 val res = new ArrayList()
26
27 res.addAll(patterns.unfinishedNonContainmentMulticiplicityQueries,false)
28 if(calculateObjectCost) {
29 val missingObjectCost = calculateMissingObjectCost(p)
30 res.addAll(patterns.unfinishedContainmentMulticiplicityQueries,true,missingObjectCost)
31 } else {
32 res.addAll(patterns.unfinishedContainmentMulticiplicityQueries,true)
33 }
34 return res
35 }
36
37 def addAll(ArrayList<MultiplicityGoalConstraintCalculator> res, Map<Relation, Pair<IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>,Integer>> queries, boolean containment) {
38 for(multiplicityQuery : queries.entrySet) {
39 val targetRelationName = multiplicityQuery.key.name
40 val query = multiplicityQuery.value.key
41 val minValue = multiplicityQuery.value.value
42 res += new MultiplicityGoalConstraintCalculator(targetRelationName,query,minValue,containment,1);
43 }
44 }
45 def addAll(
46 ArrayList<MultiplicityGoalConstraintCalculator> res,
47 Map<Relation, Pair<IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>,Integer>> queries,
48 boolean containment,
49 Map<Relation, Integer> cost
50 ) {
51 for(multiplicityQuery : queries.entrySet) {
12 val targetRelationName = multiplicityQuery.key.name 52 val targetRelationName = multiplicityQuery.key.name
13 val query = multiplicityQuery.value 53 val query = multiplicityQuery.value.key
14 res += new MultiplicityGoalConstraintCalculator(targetRelationName,query); 54 val minValue = multiplicityQuery.value.value
55 res += new MultiplicityGoalConstraintCalculator(targetRelationName,query,minValue,containment,multiplicityQuery.key.lookup(cost))
56 }
57 }
58
59 def calculateMissingObjectCost(LogicProblem p) {
60 val containments = p.containmentHierarchies.head.containmentRelations
61 val containment2Lower = containments.toInvertedMap[containment |
62 val lower = p.annotations.filter(LowerMultiplicityAssertion).filter[it.relation === containment].head
63 if(lower !== null) { lower.lower }
64 else { 0 }
65 ]
66 val types = p.types
67 val Map<Type,List<? extends Pair<Type,Integer>>> type2NewCost = new HashMap
68 for(type:types) {
69 val allSupertypes = (#[type] + type.supertypes).toSet
70 val allOutgoingContainments = containments.filter[allSupertypes.contains((it.parameters.get(0) as ComplexTypeReference).referred)]
71 val list = new LinkedList
72 for(outgoingContainment : allOutgoingContainments) {
73 val value = containment2Lower.get(outgoingContainment)
74 if(value>0) {
75 list.add((outgoingContainment.parameters.get(1) as ComplexTypeReference).referred
76 -> value)
77 }
78 }
79 type2NewCost.put(type, list)
80 }
81 val res = new HashMap
82 for(containment : containments) {
83 val key = containment
84 val value = (containment.parameters.get(1) as ComplexTypeReference).referred.count(type2NewCost)
85// println('''«key.name» --> «value» new''')
86 res.put(key,value)
15 } 87 }
16 return res 88 return res
17 } 89 }
90
91 private def int count(Type t, Map<Type,List<? extends Pair<Type,Integer>>> containments) {
92 val list = containments.get(t)
93 var r = 1
94 for(element : list) {
95 r += element.value * element.key.count(containments)
96 }
97 return r
98 }
18} \ No newline at end of file 99} \ No newline at end of file
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 db0e17b9..23ea118b 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
@@ -176,11 +176,16 @@ class RefinementRuleProvider {
176 val number = lowermultiplicities.head.lower 176 val number = lowermultiplicities.head.lower
177 if(number > 0) { 177 if(number > 0) {
178 val sourceTypeInterpretation = getTypeInterpretation(i, relation, 0) as PartialComplexTypeInterpretation 178 val sourceTypeInterpretation = getTypeInterpretation(i, relation, 0) as PartialComplexTypeInterpretation
179 val subtypeInterpretations = i.partialtypeinterpratation.filter(PartialComplexTypeInterpretation).filter[
180 it === sourceTypeInterpretation ||
181 it.supertypeInterpretation.contains(sourceTypeInterpretation)
182 ]
179 183
180 if(containmentReferences.contains(relation)) { 184 if(containmentReferences.contains(relation)) {
181 val targetTypeInterpretation = getTypeInterpretation(i, relation, 1) 185 val targetTypeInterpretation = getTypeInterpretation(i, relation, 1)
182 if(!(targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.isIsAbstract) { 186 val targetType = (targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf
183 val inverseAnnotation = p.assertions.filter(InverseRelationAssertion).filter[it.inverseA === relation || it.inverseB === relation] 187 if((!targetType.isIsAbstract) && (targetType.supertypes.empty)) {
188 val inverseAnnotation = p.annotations.filter(InverseRelationAssertion).filter[it.inverseA === relation || it.inverseB === relation]
184 if(!inverseAnnotation.empty) { 189 if(!inverseAnnotation.empty) {
185 val onlyInverseAnnotation = if(inverseAnnotation.head.inverseA===relation) { 190 val onlyInverseAnnotation = if(inverseAnnotation.head.inverseA===relation) {
186 inverseAnnotation.head.inverseB 191 inverseAnnotation.head.inverseB
@@ -188,41 +193,46 @@ class RefinementRuleProvider {
188 inverseAnnotation.head.inverseA 193 inverseAnnotation.head.inverseA
189 } 194 }
190 val inverseRelationInterpretation = i.partialrelationinterpretation.filter[it.interpretationOf === onlyInverseAnnotation].head 195 val inverseRelationInterpretation = i.partialrelationinterpretation.filter[it.interpretationOf === onlyInverseAnnotation].head
191 for(var times=0; times<number; times++) { 196 for(subTypeInterpretation : subtypeInterpretations) {
192 recursiveObjectCreation.get(sourceTypeInterpretation.interpretationOf) += 197 for(var times=0; times<number; times++) {
193 new ObjectCreationInterpretationData( 198 recursiveObjectCreation.get(subTypeInterpretation.interpretationOf) +=
194 i, 199 new ObjectCreationInterpretationData(
195 targetTypeInterpretation, 200 i,
196 relationInterpretation, 201 targetTypeInterpretation,
197 inverseRelationInterpretation, 202 relationInterpretation,
198 targetTypeInterpretation.getTypeConstructor 203 inverseRelationInterpretation,
199 ) 204 targetTypeInterpretation.getTypeConstructor
205 )
206 }
200 } 207 }
201
202 } else { 208 } else {
203 for(var times=0; times<number; times++) { 209 for(subTypeInterpretation : subtypeInterpretations) {
204 recursiveObjectCreation.get(sourceTypeInterpretation.interpretationOf) += 210 for(var times=0; times<number; times++) {
205 new ObjectCreationInterpretationData( 211 recursiveObjectCreation.get(subTypeInterpretation.interpretationOf) +=
206 i, 212 new ObjectCreationInterpretationData(
207 targetTypeInterpretation, 213 i,
208 relationInterpretation, 214 targetTypeInterpretation,
209 null, 215 relationInterpretation,
210 targetTypeInterpretation.getTypeConstructor 216 null,
211 ) 217 targetTypeInterpretation.getTypeConstructor
218 )
219 }
212 } 220 }
213 } 221 }
214 } 222 }
215 } else if(relation.parameters.get(1) instanceof PrimitiveTypeReference) { 223 } else if(relation.parameters.get(1) instanceof PrimitiveTypeReference) {
216 val targetTypeInterpretation = getTypeInterpretation(i, relation, 1) 224 val targetTypeInterpretation = getTypeInterpretation(i, relation, 1)
217 for(var times=0; times<number; times++) { 225 for(subTypeInterpretation : subtypeInterpretations) {
218 recursiveObjectCreation.get(sourceTypeInterpretation.interpretationOf) += 226 for(var times=0; times<number; times++) {
219 new ObjectCreationInterpretationData( 227 recursiveObjectCreation.get(subTypeInterpretation.interpretationOf) +=
220 i, 228 new ObjectCreationInterpretationData(
221 targetTypeInterpretation, 229 i,
222 relationInterpretation, 230 targetTypeInterpretation,
223 null, 231 relationInterpretation,
224 targetTypeInterpretation.getTypeConstructor 232 null,
225 ) 233 targetTypeInterpretation.getTypeConstructor
234 )
235 }
226 } 236 }
227 } 237 }
228 } 238 }
@@ -403,9 +413,6 @@ class RefinementRuleProvider {
403 newElement.name = '''new «interpretation.newElements.size»''' 413 newElement.name = '''new «interpretation.newElements.size»'''
404 } 414 }
405 415
406 // Existence
407 interpretation.newElements+=newElement
408
409 // Types 416 // Types
410 typeInterpretation.elements += newElement 417 typeInterpretation.elements += newElement
411 if(typeInterpretation instanceof PartialComplexTypeInterpretation) { 418 if(typeInterpretation instanceof PartialComplexTypeInterpretation) {
@@ -421,6 +428,9 @@ class RefinementRuleProvider {
421 // Scope propagation 428 // Scope propagation
422 scopePropagator.propagateAdditionToType(typeInterpretation) 429 scopePropagator.propagateAdditionToType(typeInterpretation)
423 430
431 // Existence
432 interpretation.newElements+=newElement
433
424 // Do recursive object creation 434 // Do recursive object creation
425 for(newConstructor : recursiceObjectCreations) { 435 for(newConstructor : recursiceObjectCreations) {
426 createObjectAction(nameNewElement,newConstructor,newElement,scopePropagator) 436 createObjectAction(nameNewElement,newConstructor,newElement,scopePropagator)
@@ -444,9 +454,6 @@ class RefinementRuleProvider {
444 newElement.name = '''new «interpretation.newElements.size»''' 454 newElement.name = '''new «interpretation.newElements.size»'''
445 } 455 }
446 456
447 // Existence
448 interpretation.newElements+=newElement
449
450 // Types 457 // Types
451 typeInterpretation.elements += newElement 458 typeInterpretation.elements += newElement
452 if(typeInterpretation instanceof PartialComplexTypeInterpretation) { 459 if(typeInterpretation instanceof PartialComplexTypeInterpretation) {
@@ -459,6 +466,9 @@ class RefinementRuleProvider {
459 // Scope propagation 466 // Scope propagation
460 scopePropagator.propagateAdditionToType(typeInterpretation) 467 scopePropagator.propagateAdditionToType(typeInterpretation)
461 468
469 // Existence
470 interpretation.newElements+=newElement
471
462 // Do recursive object creation 472 // Do recursive object creation
463 for(newConstructor : recursiceObjectCreations) { 473 for(newConstructor : recursiceObjectCreations) {
464 createObjectAction(nameNewElement,newConstructor,newElement,scopePropagator) 474 createObjectAction(nameNewElement,newConstructor,newElement,scopePropagator)
@@ -480,9 +490,6 @@ class RefinementRuleProvider {
480 newElement.name = '''new «interpretation.newElements.size»''' 490 newElement.name = '''new «interpretation.newElements.size»'''
481 } 491 }
482 492
483 // Existence
484 interpretation.newElements+=newElement
485
486 // Types 493 // Types
487 typeInterpretation.elements += newElement 494 typeInterpretation.elements += newElement
488 if(typeInterpretation instanceof PartialComplexTypeInterpretation) { 495 if(typeInterpretation instanceof PartialComplexTypeInterpretation) {
@@ -492,6 +499,9 @@ class RefinementRuleProvider {
492 // Scope propagation 499 // Scope propagation
493 scopePropagator.propagateAdditionToType(typeInterpretation) 500 scopePropagator.propagateAdditionToType(typeInterpretation)
494 501
502 // Existence
503 interpretation.newElements+=newElement
504
495 // Do recursive object creation 505 // Do recursive object creation
496 for(newConstructor : recursiceObjectCreations) { 506 for(newConstructor : recursiceObjectCreations) {
497 createObjectAction(nameNewElement,newConstructor,newElement,scopePropagator) 507 createObjectAction(nameNewElement,newConstructor,newElement,scopePropagator)
generated by cgit v1.2.3-70-g09d2 (git 2.46.0) at 2024-09-18 02:36:06 +0000