diff options
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit')
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 | |||
8 | import java.util.Set | 8 | import java.util.Set |
9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialComplexTypeInterpretation | 9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialComplexTypeInterpretation |
10 | import java.util.HashSet | 10 | import java.util.HashSet |
11 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialPrimitiveInterpretation | ||
11 | 12 | ||
12 | class ScopePropagator { | 13 | class 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 | |||
28 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference | 28 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference |
29 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntTypeReference | 29 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntTypeReference |
30 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference | 30 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference |
31 | import java.util.Map | ||
31 | 32 | ||
32 | class PConstraintTransformer { | 33 | class 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 | |||
8 | import org.eclipse.xtext.xbase.XMemberFeatureCall | 8 | import org.eclipse.xtext.xbase.XMemberFeatureCall |
9 | import org.eclipse.xtext.xbase.XNumberLiteral | 9 | import org.eclipse.xtext.xbase.XNumberLiteral |
10 | import org.eclipse.xtext.xbase.XUnaryOperation | 10 | import org.eclipse.xtext.xbase.XUnaryOperation |
11 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.PrimitiveTypeReference | ||
12 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference | ||
11 | 13 | ||
12 | class PExpressionGenerator { | 14 | class 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 | |||
26 | import org.eclipse.xtend.lib.annotations.Accessors | 26 | import org.eclipse.xtend.lib.annotations.Accessors |
27 | 27 | ||
28 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | 28 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* |
29 | import org.eclipse.xtend.lib.annotations.Data | ||
30 | import 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 | ||
30 | class PatternGenerator { | 38 | class 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 |
62 | class UnitPropagationPreconditionFinalResult { | 62 | class 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 | ||
67 | class UnitPropagationPreconditionGenerator { | 68 | class 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 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules | 1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules |
2 | 2 | ||
3 | import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.LowerMultiplicityAssertion | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | ||
3 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.MultiplicityGoalConstraintCalculator | 8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.MultiplicityGoalConstraintCalculator |
4 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.GeneratedPatterns | 9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.GeneratedPatterns |
5 | import java.util.ArrayList | 10 | import java.util.ArrayList |
11 | import java.util.HashMap | ||
12 | import java.util.LinkedList | ||
13 | import java.util.List | ||
14 | import java.util.Map | ||
15 | import org.eclipse.viatra.query.runtime.api.IPatternMatch | ||
16 | import org.eclipse.viatra.query.runtime.api.IQuerySpecification | ||
17 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher | ||
18 | |||
19 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | ||
6 | 20 | ||
7 | class GoalConstraintProvider { | 21 | class 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) |