diff options
author | Kristóf Marussy <kris7topher@gmail.com> | 2019-07-30 18:57:01 +0200 |
---|---|---|
committer | Kristóf Marussy <kris7topher@gmail.com> | 2019-07-30 18:57:01 +0200 |
commit | 4cb0aa5a0b9adac2bb8d4a995be015651bdd5628 (patch) | |
tree | 5c917ffa6f334e6b4c268b94fb0bd8910cf892b2 /Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu | |
parent | Allow infiite upper scope bound in PolyhedronScopePropagator (diff) | |
download | VIATRA-Generator-4cb0aa5a0b9adac2bb8d4a995be015651bdd5628.tar.gz VIATRA-Generator-4cb0aa5a0b9adac2bb8d4a995be015651bdd5628.tar.zst VIATRA-Generator-4cb0aa5a0b9adac2bb8d4a995be015651bdd5628.zip |
Polyhedron scope propagator for non-containment references
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu')
7 files changed, 477 insertions, 420 deletions
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/Modality.java b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/Modality.java index d2132cea..f3a6ec32 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/Modality.java +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/Modality.java | |||
@@ -2,21 +2,46 @@ package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra; | |||
2 | 2 | ||
3 | public enum Modality { | 3 | public enum Modality { |
4 | MUST, MAY, CURRENT; | 4 | MUST, MAY, CURRENT; |
5 | |||
5 | public boolean isMust() { | 6 | public boolean isMust() { |
6 | return this == MUST; | 7 | return this == MUST; |
7 | } | 8 | } |
9 | |||
8 | public boolean isMay() { | 10 | public boolean isMay() { |
9 | return this == MAY; | 11 | return this == MAY; |
10 | } | 12 | } |
13 | |||
11 | public boolean isCurrent() { | 14 | public boolean isCurrent() { |
12 | return this == CURRENT; | 15 | return this == CURRENT; |
13 | } | 16 | } |
17 | |||
14 | public boolean isMustOrCurrent() { | 18 | public boolean isMustOrCurrent() { |
15 | return isMust() || isCurrent(); | 19 | return isMust() || isCurrent(); |
16 | } | 20 | } |
21 | |||
17 | public Modality getDual() { | 22 | public Modality getDual() { |
18 | if(this.isCurrent()) return CURRENT; | 23 | switch (this) { |
19 | else if(this.isMust())return MAY; | 24 | case CURRENT: |
20 | else return MUST; | 25 | return CURRENT; |
26 | case MUST: | ||
27 | return MAY; | ||
28 | case MAY: | ||
29 | return MUST; | ||
30 | default: | ||
31 | throw new UnsupportedOperationException("Unknown Modality: " + this); | ||
32 | } | ||
33 | } | ||
34 | |||
35 | public Modality toBase() { | ||
36 | if (this.isCurrent()) { | ||
37 | return MUST; | ||
38 | } else { | ||
39 | return this; | ||
40 | } | ||
41 | } | ||
42 | |||
43 | @Override | ||
44 | public String toString() { | ||
45 | return super.toString().toLowerCase(); | ||
21 | } | 46 | } |
22 | } | 47 | } |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend index e9c155f5..f6b101b6 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend | |||
@@ -50,7 +50,7 @@ class PolyhedronScopePropagator extends ScopePropagator { | |||
50 | throw new IllegalStateException("Could not determine maximum number of new nodes, it may be unbounded") | 50 | throw new IllegalStateException("Could not determine maximum number of new nodes, it may be unbounded") |
51 | } | 51 | } |
52 | if (maximumNumberOfNewNodes <= 0) { | 52 | if (maximumNumberOfNewNodes <= 0) { |
53 | throw new IllegalStateException("Maximum number of new nodes is negative") | 53 | throw new IllegalStateException("Maximum number of new nodes is not positive") |
54 | } | 54 | } |
55 | builder.buildMultiplicityConstraints(unfinishedMultiplicityQueries, hasElementInContainmentQuery, | 55 | builder.buildMultiplicityConstraints(unfinishedMultiplicityQueries, hasElementInContainmentQuery, |
56 | maximumNumberOfNewNodes) | 56 | maximumNumberOfNewNodes) |
@@ -65,7 +65,7 @@ class PolyhedronScopePropagator extends ScopePropagator { | |||
65 | val result = operator.saturate() | 65 | val result = operator.saturate() |
66 | // println(polyhedron) | 66 | // println(polyhedron) |
67 | if (result == PolyhedronSaturationResult.EMPTY) { | 67 | if (result == PolyhedronSaturationResult.EMPTY) { |
68 | throw new IllegalStateException("Scope bounds cannot be satisfied") | 68 | setScopesInvalid() |
69 | } else { | 69 | } else { |
70 | populateScopesFromPolyhedron() | 70 | populateScopesFromPolyhedron() |
71 | if (result != PolyhedronSaturationResult.SATURATED) { | 71 | if (result != PolyhedronSaturationResult.SATURATED) { |
@@ -146,6 +146,15 @@ class PolyhedronScopePropagator extends ScopePropagator { | |||
146 | } | 146 | } |
147 | } | 147 | } |
148 | 148 | ||
149 | private def setScopesInvalid() { | ||
150 | partialInterpretation.minNewElements = Integer.MAX_VALUE | ||
151 | partialInterpretation.maxNewElements = 0 | ||
152 | for (scope : partialInterpretation.scopes) { | ||
153 | scope.minNewElements = Integer.MAX_VALUE | ||
154 | scope.maxNewElements = 0 | ||
155 | } | ||
156 | } | ||
157 | |||
149 | private static def <T extends IPatternMatch> getCalculatedMultiplicity(ViatraQueryMatcher<T> matcher, | 158 | private static def <T extends IPatternMatch> getCalculatedMultiplicity(ViatraQueryMatcher<T> matcher, |
150 | PartialInterpretation p) { | 159 | PartialInterpretation p) { |
151 | val match = matcher.newEmptyMatch | 160 | val match = matcher.newEmptyMatch |
@@ -276,6 +285,37 @@ class PolyhedronScopePropagator extends ScopePropagator { | |||
276 | 285 | ||
277 | private def buildNonContainmentConstraints(RelationMultiplicityConstraint constraint, | 286 | private def buildNonContainmentConstraints(RelationMultiplicityConstraint constraint, |
278 | UnifinishedMultiplicityQueries queries) { | 287 | UnifinishedMultiplicityQueries queries) { |
288 | if (constraint.constrainsRemainingInverse) { | ||
289 | if (queries.unfinishedMultiplicityQuery === null) { | ||
290 | throw new IllegalArgumentException("Reference constraints need unfinished multiplicity queries") | ||
291 | } | ||
292 | val unfinishedMultiplicityMatcher = queries.unfinishedMultiplicityQuery.getMatcher(queryEngine) | ||
293 | if (queries.remainingInverseMultiplicityQuery === null) { | ||
294 | throw new IllegalArgumentException( | ||
295 | "Reference constraints need remaining inverse multiplicity queries") | ||
296 | } | ||
297 | val remainingInverseMultiplicityMatcher = queries.remainingInverseMultiplicityQuery.getMatcher( | ||
298 | queryEngine) | ||
299 | val availableMultiplicityCoefficients = new HashMap | ||
300 | availableMultiplicityCoefficients.addCoefficients(constraint.inverseUpperBound, | ||
301 | subtypeDimensions.get(constraint.targetType)) | ||
302 | availableMultiplicityCoefficients.addCoefficients(-constraint.lowerBound, | ||
303 | subtypeDimensions.get(constraint.targetType)) | ||
304 | val availableMultiplicity = availableMultiplicityCoefficients.toExpression | ||
305 | updatersBuilder.add( | ||
306 | new UnfinishedMultiplicityConstraintUpdater(constraint.relation.name, availableMultiplicity, | ||
307 | unfinishedMultiplicityMatcher, remainingInverseMultiplicityMatcher)) | ||
308 | } | ||
309 | if (constraint.constrainsUnrepairable) { | ||
310 | if (queries.unrepairableMultiplicityQuery === null) { | ||
311 | throw new IllegalArgumentException("Reference constraints need unrepairable multiplicity queries") | ||
312 | } | ||
313 | val unrepairableMultiplicityMatcher = queries.unrepairableMultiplicityQuery.getMatcher(queryEngine) | ||
314 | val targetTypeCardinality = typeBounds.get(constraint.targetType) | ||
315 | updatersBuilder.add( | ||
316 | new UnrepairableMultiplicityConstraintUpdater(constraint.relation.name, targetTypeCardinality, | ||
317 | unrepairableMultiplicityMatcher)) | ||
318 | } | ||
279 | } | 319 | } |
280 | 320 | ||
281 | private def addCoefficients(Map<Dimension, Integer> accumulator, int scale, Map<Dimension, Integer> a) { | 321 | private def addCoefficients(Map<Dimension, Integer> accumulator, int scale, Map<Dimension, Integer> a) { |
@@ -410,4 +450,40 @@ class PolyhedronScopePropagator extends ScopePropagator { | |||
410 | matcher.countMatches(match) != 0 | 450 | matcher.countMatches(match) != 0 |
411 | } | 451 | } |
412 | } | 452 | } |
453 | |||
454 | @FinalFieldsConstructor | ||
455 | static class UnfinishedMultiplicityConstraintUpdater implements RelationConstraintUpdater { | ||
456 | val String name | ||
457 | val LinearBoundedExpression availableMultiplicityExpression | ||
458 | val ViatraQueryMatcher<? extends IPatternMatch> unfinishedMultiplicityMatcher | ||
459 | val ViatraQueryMatcher<? extends IPatternMatch> remainingInverseMultiplicityMatcher | ||
460 | |||
461 | override update(PartialInterpretation p) { | ||
462 | val unfinishedMultiplicity = unfinishedMultiplicityMatcher.getCalculatedMultiplicity(p) | ||
463 | if (unfinishedMultiplicity === null) { | ||
464 | throw new IllegalArgumentException("Unfinished multiplicity is missing for " + name) | ||
465 | } | ||
466 | val remainingInverseMultiplicity = remainingInverseMultiplicityMatcher.getCalculatedMultiplicity(p) | ||
467 | if (remainingInverseMultiplicity === null) { | ||
468 | throw new IllegalArgumentException("Remaining inverse multiplicity is missing for " + name) | ||
469 | } | ||
470 | val int requiredMultiplicity = unfinishedMultiplicity - remainingInverseMultiplicity | ||
471 | availableMultiplicityExpression.tightenLowerBound(requiredMultiplicity) | ||
472 | } | ||
473 | } | ||
474 | |||
475 | @FinalFieldsConstructor | ||
476 | static class UnrepairableMultiplicityConstraintUpdater implements RelationConstraintUpdater { | ||
477 | val String name | ||
478 | val LinearBoundedExpression targetCardinalityExpression | ||
479 | val ViatraQueryMatcher<? extends IPatternMatch> unrepairableMultiplicityMatcher | ||
480 | |||
481 | override update(PartialInterpretation p) { | ||
482 | val value = unrepairableMultiplicityMatcher.getCalculatedMultiplicity(p) | ||
483 | if (value === null) { | ||
484 | throw new IllegalArgumentException("Unrepairable multiplicity is missing for " + name) | ||
485 | } | ||
486 | targetCardinalityExpression.tightenLowerBound(value) | ||
487 | } | ||
488 | } | ||
413 | } | 489 | } |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/GenericTypeIndexer.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/GenericTypeIndexer.xtend index d6a15c1a..0e0f1f02 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/GenericTypeIndexer.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/GenericTypeIndexer.xtend | |||
@@ -1,209 +1,150 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns | 1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns |
2 | 2 | ||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | 3 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type |
5 | import org.eclipse.emf.ecore.EClass | 4 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem |
6 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality | 5 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality |
7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | ||
8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysisResult | 6 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysisResult |
9 | 7 | ||
10 | class GenericTypeIndexer extends TypeIndexer { | 8 | class GenericTypeIndexer extends TypeIndexer { |
11 | val PatternGenerator base; | ||
12 | |||
13 | new(PatternGenerator base) { | 9 | new(PatternGenerator base) { |
14 | this.base = base | 10 | super(base) |
15 | } | 11 | } |
12 | |||
16 | override requiresTypeAnalysis() { false } | 13 | override requiresTypeAnalysis() { false } |
17 | 14 | ||
18 | public override getRequiredQueries() ''' | 15 | override getRequiredQueries() ''' |
19 | private pattern newELement(interpretation: PartialInterpretation, element: DefinedElement) { | 16 | «super.requiredQueries» |
20 | PartialInterpretation.newElements(interpretation,element); | 17 | |
21 | } | 18 | /** |
22 | 19 | * Direct supertypes of a type. | |
23 | private pattern typeInterpretation(problem:LogicProblem, interpetation:PartialInterpretation, type:TypeDeclaration, typeInterpretation:PartialComplexTypeInterpretation) { | 20 | */ |
24 | find interpretation(problem,interpetation); | 21 | private pattern supertypeDirect(subtype : Type, supertype : Type) { |
25 | LogicProblem.types(problem,type); | 22 | Type.supertypes(subtype, supertype); |
26 | PartialInterpretation.partialtypeinterpratation(interpetation,typeInterpretation); | 23 | } |
27 | PartialComplexTypeInterpretation.interpretationOf(typeInterpretation,type); | 24 | |
28 | } | 25 | /** |
29 | 26 | * All supertypes of a type. | |
30 | private pattern directInstanceOf(problem:LogicProblem, interpetation:PartialInterpretation, element:DefinedElement, type:Type) { | 27 | */ |
31 | find interpretation(problem,interpetation); | 28 | private pattern supertypeStar(subtype: Type, supertype: Type) { |
32 | find mustExist(problem,interpetation,element); | 29 | subtype == supertype; |
33 | LogicProblem.types(problem,type); | 30 | } or { |
34 | TypeDefinition.elements(type,element); | 31 | find supertypeDirect+(subtype,supertype); |
35 | } or { | 32 | } |
36 | find mustExist(problem,interpetation,element); | 33 | |
37 | find typeInterpretation(problem,interpetation,type,typeInterpretation); | 34 | /// Complex type reasoning patterns /// |
38 | PartialComplexTypeInterpretation.elements(typeInterpretation,element); | 35 | // |
39 | } | 36 | // In a valid type system, for each element e there is exactly one type T where |
40 | 37 | // 1: T(e) - but we dont know this for type declaration | |
41 | /** | 38 | // 2: For the dynamic type D and another type T, where D(e) && D-->T, T(e) is true. |
42 | * Direct supertypes of a type. | 39 | // 2e: A type hierarchy is invalid, if there is a supertype T for a dynamic type D which does no contains e: |
43 | */ | 40 | // D(e) && D-->T && !T(e) |
44 | private pattern supertypeDirect(subtype : Type, supertype : Type) { | 41 | // 3: There is no T' that T'->T and T'(e) |
45 | Type.supertypes(subtype, supertype); | 42 | // 3e: A type hierarcy is invalid, if there is a type T for a dynamic type D, which contains e, but not subtype of T: |
46 | } | 43 | // D(e) && ![T--->D] && T(e) |
47 | |||
48 | /** | ||
49 | * All supertypes of a type. | ||
50 | */ | ||
51 | private pattern supertypeStar(subtype: Type, supertype: Type) { | ||
52 | subtype == supertype; | ||
53 | } or { | ||
54 | find supertypeDirect+(subtype,supertype); | ||
55 | } | ||
56 | |||
57 | /// Complex type reasoning patterns /// | ||
58 | // | ||
59 | // In a valid type system, for each element e there is exactly one type T where | ||
60 | // 1: T(e) - but we dont know this for type declaration | ||
61 | // 2: For the dynamic type D and another type T, where D(e) && D-->T, T(e) is true. | ||
62 | // 2e: A type hierarchy is invalid, if there is a supertype T for a dynamic type D which does no contains e: | ||
63 | // D(e) && D-->T && !T(e) | ||
64 | // 3: There is no T' that T'->T and T'(e) | ||
65 | // 3e: A type hierarcy is invalid, if there is a type T for a dynamic type D, which contains e, but not subtype of T: | ||
66 | // D(e) && ![T--->D] && T(e) | ||
67 | // 4: T is not abstract | ||
68 | // Such type T is called Dynamic type of e, while other types are called static types. | ||
69 | // | ||
70 | // The following patterns checks the possible dynamic types for an element | ||
71 | |||
72 | private pattern wellformedType(problem: LogicProblem, interpretation:PartialInterpretation, dynamic:Type, element:DefinedElement) { | ||
73 | // 1: T(e) | ||
74 | find directInstanceOf(problem,interpretation,element,dynamic); | ||
75 | // 2e is not true: D(e) && D-->T && !T(e) | ||
76 | neg find dynamicTypeNotSubtypeOfADefinition(problem,interpretation,element,dynamic); | ||
77 | // 3e is not true: D(e) && ![T--->D] && T(e) | ||
78 | neg find dynamicTypeIsSubtypeOfANonDefinition(problem,interpretation,element,dynamic); | ||
79 | // 4: T is not abstract | ||
80 | Type.isAbstract(dynamic,false); | ||
81 | } | ||
82 | |||
83 | |||
84 | private pattern isPrimitive(element: PrimitiveElement) { | ||
85 | PrimitiveElement(element); | ||
86 | } | ||
87 | |||
88 | private pattern possibleDynamicType(problem: LogicProblem, interpretation:PartialInterpretation, dynamic:Type, element:DefinedElement) | ||
89 | // case 1: element is defined at least once | ||
90 | { | ||
91 | LogicProblem.types(problem,dynamic); | ||
92 | // select a random definition 'randomType' | ||
93 | find directInstanceOf(problem,interpretation,element,randomType); | ||
94 | // dynamic is a subtype of 'randomType' | ||
95 | find supertypeStar(dynamic,randomType); | ||
96 | // 2e is not true: D(e) && D-->T && !T(e) | ||
97 | neg find dynamicTypeNotSubtypeOfADefinition(problem,interpretation,element,dynamic); | ||
98 | // 3e is not true: D(e) && ![T--->D] && T(e) | ||
99 | neg find dynamicTypeIsSubtypeOfANonDefinition(problem,interpretation,element,dynamic); | ||
100 | // 4: T is not abstract | ||
101 | Type.isAbstract(dynamic,false); | ||
102 | // 5. element is not primitive datatype | ||
103 | neg find isPrimitive(element); | ||
104 | } or | ||
105 | // case 2: element is not defined anywhere | ||
106 | { | ||
107 | find mayExist(problem,interpretation,element); | ||
108 | // there is no definition | ||
109 | neg find directInstanceOf(problem,interpretation,element,_); | ||
110 | // 2e is not true: D(e) && D-->T && !T(e) | ||
111 | // because non of the definition contains element, the type cannot have defined supertype | ||
112 | LogicProblem.types(problem,dynamic); | ||
113 | PartialInterpretation.problem(interpretation,problem); | ||
114 | neg find typeWithDefinedSupertype(dynamic); | ||
115 | // 3e is not true: D(e) && ![T--->D] && T(e) | ||
116 | // because there is no definition, dynamic covers all definition | ||
117 | // 4: T is not abstract | 44 | // 4: T is not abstract |
118 | Type.isAbstract(dynamic,false); | 45 | // Such type T is called Dynamic type of e, while other types are called static types. |
119 | // 5. element is not primitive datatype | 46 | // |
120 | neg find isPrimitive(element); | 47 | // The following patterns checks the possible dynamic types for an element |
121 | } | 48 | |
122 | 49 | private pattern wellformedType(problem: LogicProblem, interpretation:PartialInterpretation, dynamic:Type, element:DefinedElement) { | |
123 | /** | 50 | // 1: T(e) |
124 | * supertype -------> element <------- otherSupertype | 51 | find directInstanceOf(problem,interpretation,element,dynamic); |
125 | * A A | 52 | // 2e is not true: D(e) && D-->T && !T(e) |
126 | * | | | 53 | neg find dynamicTypeNotSubtypeOfADefinition(problem,interpretation,element,dynamic); |
127 | * wrongDynamic -----------------------------X | 54 | // 3e is not true: D(e) && ![T--->D] && T(e) |
128 | */ | 55 | neg find dynamicTypeIsSubtypeOfANonDefinition(problem,interpretation,element,dynamic); |
129 | private pattern dynamicTypeNotSubtypeOfADefinition(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement, wrongDynamic : Type) { | 56 | // 4: T is not abstract |
130 | find directInstanceOf(problem,interpretation,element,supertype); | 57 | Type.isAbstract(dynamic,false); |
131 | find directInstanceOf(problem,interpretation,element,otherSupertype); | 58 | } |
132 | find supertypeStar(wrongDynamic,supertype); | 59 | |
133 | neg find supertypeStar(wrongDynamic,otherSupertype); | 60 | private pattern possibleDynamicType(problem: LogicProblem, interpretation:PartialInterpretation, dynamic:Type, element:DefinedElement) |
134 | } | 61 | // case 1: element is defined at least once |
135 | 62 | { | |
136 | /** | 63 | LogicProblem.types(problem,dynamic); |
137 | * supertype -------> element <---X--- otherSupertype | 64 | // select a random definition 'randomType' |
138 | * A A | 65 | find directInstanceOf(problem,interpretation,element,randomType); |
139 | * | | | 66 | // dynamic is a subtype of 'randomType' |
140 | * wrongDynamic -----------------------------+ | 67 | find supertypeStar(dynamic,randomType); |
141 | */ | 68 | // 2e is not true: D(e) && D-->T && !T(e) |
142 | private pattern dynamicTypeIsSubtypeOfANonDefinition(problem: LogicProblem, interpretation:PartialInterpretation, element:DefinedElement, wrongDynamic:Type) { | 69 | neg find dynamicTypeNotSubtypeOfADefinition(problem,interpretation,element,dynamic); |
143 | find directInstanceOf(problem,interpretation,element,supertype); | 70 | // 3e is not true: D(e) && ![T--->D] && T(e) |
144 | neg find elementInTypeDefinition(element,otherSupertype); | 71 | neg find dynamicTypeIsSubtypeOfANonDefinition(problem,interpretation,element,dynamic); |
145 | TypeDefinition(otherSupertype); | 72 | // 4: T is not abstract |
146 | find supertypeStar(wrongDynamic, supertype); | 73 | Type.isAbstract(dynamic,false); |
147 | find supertypeStar(wrongDynamic, otherSupertype); | 74 | // 5. element is not primitive datatype |
148 | } | 75 | neg find isPrimitive(element); |
149 | 76 | } or | |
150 | private pattern elementInTypeDefinition(element:DefinedElement, definition:TypeDefinition) { | 77 | // case 2: element is not defined anywhere |
151 | TypeDefinition.elements(definition,element); | 78 | { |
152 | } | 79 | find mayExist(problem,interpretation,element); |
153 | 80 | // there is no definition | |
154 | private pattern typeWithDefinedSupertype(type:Type) { | 81 | neg find directInstanceOf(problem,interpretation,element,_); |
155 | find supertypeStar(type,definedSupertype); | 82 | // 2e is not true: D(e) && D-->T && !T(e) |
156 | TypeDefinition(definedSupertype); | 83 | // because non of the definition contains element, the type cannot have defined supertype |
157 | } | 84 | LogicProblem.types(problem,dynamic); |
158 | 85 | PartialInterpretation.problem(interpretation,problem); | |
159 | private pattern scopeDisallowsNewElementsFromType(typeInterpretation:PartialComplexTypeInterpretation) { | 86 | neg find typeWithDefinedSupertype(dynamic); |
160 | Scope.targetTypeInterpretation(scope,typeInterpretation); | 87 | // 3e is not true: D(e) && ![T--->D] && T(e) |
161 | Scope.maxNewElements(scope,0); | 88 | // because there is no definition, dynamic covers all definition |
162 | } | 89 | // 4: T is not abstract |
163 | ''' | 90 | Type.isAbstract(dynamic,false); |
164 | 91 | // 5. element is not primitive datatype | |
165 | public override generateInstanceOfQueries(LogicProblem problem, PartialInterpretation emptySolution,TypeAnalysisResult typeAnalysisResult) { | 92 | neg find isPrimitive(element); |
166 | ''' | 93 | } |
167 | «FOR type:problem.types» | 94 | |
168 | «problem.generateMustInstenceOf(type)» | ||
169 | «problem.generateMayInstanceOf(type)» | ||
170 | «ENDFOR» | ||
171 | ''' | ||
172 | } | ||
173 | |||
174 | private def patternName(Type type, Modality modality) | ||
175 | '''«modality.toString.toLowerCase»InstanceOf«base.canonizeName(type.name)»''' | ||
176 | |||
177 | private def generateMustInstenceOf(LogicProblem problem, Type type) { | ||
178 | ''' | ||
179 | /** | 95 | /** |
180 | * An element must be an instance of type "«type.name»". | 96 | * supertype -------> element <------- otherSupertype |
97 | * A A | ||
98 | * | | | ||
99 | * wrongDynamic -----------------------------X | ||
181 | */ | 100 | */ |
182 | private pattern «patternName(type,Modality.MUST)»(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) { | 101 | private pattern dynamicTypeNotSubtypeOfADefinition(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement, wrongDynamic : Type) { |
183 | Type.name(type,"«type.name»"); | 102 | find directInstanceOf(problem,interpretation,element,supertype); |
184 | find directInstanceOf(problem,interpretation,element,type); | 103 | find directInstanceOf(problem,interpretation,element,otherSupertype); |
104 | find supertypeStar(wrongDynamic,supertype); | ||
105 | neg find supertypeStar(wrongDynamic,otherSupertype); | ||
185 | } | 106 | } |
186 | ''' | 107 | |
187 | } | ||
188 | |||
189 | private def generateMayInstanceOf(LogicProblem problem, Type type) { | ||
190 | ''' | ||
191 | /** | 108 | /** |
192 | * An element may be an instance of type "«type.name»". | 109 | * supertype -------> element <---X--- otherSupertype |
110 | * A A | ||
111 | * | | | ||
112 | * wrongDynamic -----------------------------+ | ||
193 | */ | 113 | */ |
194 | private pattern «patternName(type,Modality.MAY)»(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) { | 114 | private pattern dynamicTypeIsSubtypeOfANonDefinition(problem: LogicProblem, interpretation:PartialInterpretation, element:DefinedElement, wrongDynamic:Type) { |
195 | Type.name(type,"«type.name»"); | 115 | find directInstanceOf(problem,interpretation,element,supertype); |
196 | find possibleDynamicType(problem,interpretation,dynamic,element); | 116 | neg find elementInTypeDefinition(element,otherSupertype); |
197 | find supertypeStar(dynamic,type); | 117 | TypeDefinition(otherSupertype); |
198 | neg find scopeDisallowsNewElementsFromType(dynamic); | 118 | find supertypeStar(wrongDynamic, supertype); |
119 | find supertypeStar(wrongDynamic, otherSupertype); | ||
120 | } | ||
121 | |||
122 | private pattern elementInTypeDefinition(element:DefinedElement, definition:TypeDefinition) { | ||
123 | TypeDefinition.elements(definition,element); | ||
124 | } | ||
125 | |||
126 | private pattern typeWithDefinedSupertype(type:Type) { | ||
127 | find supertypeStar(type,definedSupertype); | ||
128 | TypeDefinition(definedSupertype); | ||
129 | } | ||
130 | |||
131 | private pattern scopeDisallowsNewElementsFromType(typeInterpretation:PartialComplexTypeInterpretation) { | ||
132 | Scope.targetTypeInterpretation(scope,typeInterpretation); | ||
133 | Scope.maxNewElements(scope,0); | ||
199 | } | 134 | } |
135 | ''' | ||
136 | |||
137 | protected override generateMayInstanceOf(LogicProblem problem, Type type, TypeAnalysisResult typeAnalysisResult) { | ||
138 | ''' | ||
139 | /** | ||
140 | * An element may be an instance of type "«type.name»". | ||
141 | */ | ||
142 | private pattern «patternName(type,Modality.MAY)»(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) { | ||
143 | Type.name(type,"«type.name»"); | ||
144 | find possibleDynamicType(problem,interpretation,dynamic,element); | ||
145 | find supertypeStar(dynamic,type); | ||
146 | neg find scopeDisallowsNewElementsFromType(dynamic); | ||
147 | } | ||
200 | ''' | 148 | ''' |
201 | } | 149 | } |
202 | 150 | } | |
203 | public override referInstanceOf(Type type, Modality modality, String variableName) { | ||
204 | '''find «patternName(type,modality)»(problem,interpretation,«variableName»);''' | ||
205 | } | ||
206 | public override referInstanceOf(EClass type, Modality modality, String variableName) { | ||
207 | '''find «modality.toString.toLowerCase»InstanceOf«base.canonizeName('''«type.name» class''')»(problem,interpretation,«variableName»);''' | ||
208 | } | ||
209 | } \ 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/GenericTypeRefinementGenerator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/GenericTypeRefinementGenerator.xtend index c9f6abce..52f0cbea 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/GenericTypeRefinementGenerator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/GenericTypeRefinementGenerator.xtend | |||
@@ -14,107 +14,111 @@ class GenericTypeRefinementGenerator extends TypeRefinementGenerator { | |||
14 | new(PatternGenerator base) { | 14 | new(PatternGenerator base) { |
15 | super(base) | 15 | super(base) |
16 | } | 16 | } |
17 | |||
17 | override requiresTypeAnalysis() { false } | 18 | override requiresTypeAnalysis() { false } |
18 | 19 | ||
19 | override generateRefineObjectQueries(LogicProblem p, PartialInterpretation emptySolution, TypeAnalysisResult typeAnalysisResult) { | 20 | override generateRefineObjectQueries(LogicProblem p, PartialInterpretation emptySolution, |
21 | TypeAnalysisResult typeAnalysisResult) { | ||
20 | val containment = p.containmentHierarchies.head | 22 | val containment = p.containmentHierarchies.head |
21 | val newObjectTypes = p.types.filter(TypeDeclaration).filter[!isAbstract] | 23 | val newObjectTypes = p.types.filter(TypeDeclaration).filter[!isAbstract] |
22 | val inverseRelations = new HashMap | 24 | val inverseRelations = new HashMap |
23 | p.annotations.filter(InverseRelationAssertion).forEach[ | 25 | p.annotations.filter(InverseRelationAssertion).forEach [ |
24 | inverseRelations.put(it.inverseA,it.inverseB) | 26 | inverseRelations.put(it.inverseA, it.inverseB) |
25 | inverseRelations.put(it.inverseB,it.inverseA) | 27 | inverseRelations.put(it.inverseB, it.inverseA) |
26 | ] | 28 | ] |
27 | return ''' | 29 | return ''' |
28 | pattern «hasElementInContainmentName»(problem:LogicProblem, interpretation:PartialInterpretation) | 30 | pattern «hasElementInContainmentName»(problem:LogicProblem, interpretation:PartialInterpretation) |
29 | «FOR type :containment.typesOrderedInHierarchy SEPARATOR "or"»{ | 31 | «FOR type : containment.typesOrderedInHierarchy SEPARATOR "or"»{ |
30 | find interpretation(problem,interpretation); | ||
31 | «base.typeIndexer.referInstanceOf(type,Modality.MUST,"root")» | ||
32 | find mustExist(problem, interpretation, root); | ||
33 | }«ENDFOR» | ||
34 | «FOR type:newObjectTypes» | ||
35 | «IF(containment.typesOrderedInHierarchy.contains(type))» | ||
36 | «FOR containmentRelation : containment.containmentRelations.filter[canBeContainedByRelation(it,type)]» | ||
37 | «IF inverseRelations.containsKey(containmentRelation)» | ||
38 | pattern «this.patternName(containmentRelation,inverseRelations.get(containmentRelation),type)»( | ||
39 | problem:LogicProblem, interpretation:PartialInterpretation, | ||
40 | relationInterpretation:PartialRelationInterpretation, inverseInterpretation:PartialRelationInterpretation ,typeInterpretation:PartialComplexTypeInterpretation, | ||
41 | container:DefinedElement) | ||
42 | { | ||
43 | find interpretation(problem,interpretation); | ||
44 | PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation); | ||
45 | PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"«type.name»"); | ||
46 | PartialInterpretation.partialrelationinterpretation(interpretation,relationInterpretation); | ||
47 | PartialRelationInterpretation.interpretationOf.name(relationInterpretation,"«containmentRelation.name»"); | ||
48 | PartialInterpretation.partialrelationinterpretation(interpretation,inverseInterpretation); | ||
49 | PartialRelationInterpretation.interpretationOf.name(inverseInterpretation,"«inverseRelations.get(containmentRelation).name»"); | ||
50 | «base.typeIndexer.referInstanceOf((containmentRelation.parameters.get(0) as ComplexTypeReference).referred,Modality.MUST,"container")» | ||
51 | «base.typeIndexer.referInstanceOf(type,Modality.MAY,"newObject")» | ||
52 | «base.relationDeclarationIndexer.referRelation(containmentRelation as RelationDeclaration,"container","newObject",Modality.MAY)» | ||
53 | find mustExist(problem, interpretation, container); | ||
54 | neg find mustExist(problem, interpretation, newObject); | ||
55 | } | ||
56 | «ELSE» | ||
57 | pattern «this.patternName(containmentRelation,null,type)»( | ||
58 | problem:LogicProblem, interpretation:PartialInterpretation, | ||
59 | relationInterpretation:PartialRelationInterpretation, typeInterpretation:PartialComplexTypeInterpretation, | ||
60 | container:DefinedElement) | ||
61 | { | ||
62 | find interpretation(problem,interpretation); | ||
63 | PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation); | ||
64 | PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"«type.name»"); | ||
65 | PartialInterpretation.partialrelationinterpretation(interpretation,relationInterpretation); | ||
66 | PartialRelationInterpretation.interpretationOf.name(relationInterpretation,"«containmentRelation.name»"); | ||
67 | «base.typeIndexer.referInstanceOf((containmentRelation.parameters.get(0) as ComplexTypeReference).referred,Modality.MUST,"container")» | ||
68 | «base.typeIndexer.referInstanceOf(type,Modality.MAY,"newObject")» | ||
69 | «base.relationDeclarationIndexer.referRelation(containmentRelation as RelationDeclaration,"container","newObject",Modality.MAY)» | ||
70 | find mustExist(problem, interpretation, container); | ||
71 | neg find mustExist(problem, interpretation, newObject); | ||
72 | } | ||
73 | «ENDIF» | ||
74 | «ENDFOR» | ||
75 | pattern «patternName(null,null,type)»( | ||
76 | problem:LogicProblem, interpretation:PartialInterpretation, | ||
77 | typeInterpretation:PartialComplexTypeInterpretation) | ||
78 | { | ||
79 | find interpretation(problem,interpretation); | 32 | find interpretation(problem,interpretation); |
80 | neg find «hasElementInContainmentName»(problem,interpretation); | 33 | «base.typeIndexer.referInstanceOf(type,Modality.MUST,"root")» |
81 | PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation); | 34 | find mustExist(problem, interpretation, root); |
82 | PartialComplexTypeInterpretation.interpretationOf.name(type,"«type.name»"); | 35 | }«ENDFOR» |
83 | «base.typeIndexer.referInstanceOf(type,Modality.MAY,"newObject")» | 36 | «FOR type : newObjectTypes» |
84 | find mayExist(problem, interpretation, newObject); | 37 | «IF(containment.typesOrderedInHierarchy.contains(type))» |
85 | neg find mustExist(problem, interpretation, newObject); | 38 | «FOR containmentRelation : containment.containmentRelations.filter[canBeContainedByRelation(it,type)]» |
86 | } | 39 | «IF inverseRelations.containsKey(containmentRelation)» |
87 | «ELSE» | 40 | pattern «this.patternName(containmentRelation,inverseRelations.get(containmentRelation),type)»( |
88 | pattern createObject_«this.patternName(null,null,type)»( | 41 | problem:LogicProblem, interpretation:PartialInterpretation, |
89 | problem:LogicProblem, interpretation:PartialInterpretation, | 42 | relationInterpretation:PartialRelationInterpretation, inverseInterpretation:PartialRelationInterpretation ,typeInterpretation:PartialComplexTypeInterpretation, |
90 | typeInterpretation:PartialComplexTypeInterpretation) | 43 | container:DefinedElement) |
91 | { | 44 | { |
92 | find interpretation(problem,interpretation); | 45 | find interpretation(problem,interpretation); |
93 | PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation); | 46 | PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation); |
94 | PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"«type.name»"); | 47 | PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"«type.name»"); |
95 | «base.typeIndexer.referInstanceOf(type,Modality.MAY,"newObject")» | 48 | PartialInterpretation.partialrelationinterpretation(interpretation,relationInterpretation); |
96 | find mayExist(problem, interpretation, newObject); | 49 | PartialRelationInterpretation.interpretationOf.name(relationInterpretation,"«containmentRelation.name»"); |
97 | neg find mustExist(problem, interpretation, newObject); | 50 | PartialInterpretation.partialrelationinterpretation(interpretation,inverseInterpretation); |
98 | } | 51 | PartialRelationInterpretation.interpretationOf.name(inverseInterpretation,"«inverseRelations.get(containmentRelation).name»"); |
99 | «ENDIF» | 52 | «base.typeIndexer.referInstanceOf((containmentRelation.parameters.get(0) as ComplexTypeReference).referred,Modality.MUST,"container")» |
100 | «ENDFOR» | 53 | «base.typeIndexer.referInstanceOf(type,Modality.MAY,"newObject")» |
54 | «base.relationDeclarationIndexer.referRelation(containmentRelation as RelationDeclaration,"container","newObject",Modality.MAY)» | ||
55 | find mustExist(problem, interpretation, container); | ||
56 | neg find mustExist(problem, interpretation, newObject); | ||
57 | } | ||
58 | «ELSE» | ||
59 | pattern «this.patternName(containmentRelation,null,type)»( | ||
60 | problem:LogicProblem, interpretation:PartialInterpretation, | ||
61 | relationInterpretation:PartialRelationInterpretation, typeInterpretation:PartialComplexTypeInterpretation, | ||
62 | container:DefinedElement) | ||
63 | { | ||
64 | find interpretation(problem,interpretation); | ||
65 | PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation); | ||
66 | PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"«type.name»"); | ||
67 | PartialInterpretation.partialrelationinterpretation(interpretation,relationInterpretation); | ||
68 | PartialRelationInterpretation.interpretationOf.name(relationInterpretation,"«containmentRelation.name»"); | ||
69 | «base.typeIndexer.referInstanceOf((containmentRelation.parameters.get(0) as ComplexTypeReference).referred,Modality.MUST,"container")» | ||
70 | «base.typeIndexer.referInstanceOf(type,Modality.MAY,"newObject")» | ||
71 | «base.relationDeclarationIndexer.referRelation(containmentRelation as RelationDeclaration,"container","newObject",Modality.MAY)» | ||
72 | find mustExist(problem, interpretation, container); | ||
73 | neg find mustExist(problem, interpretation, newObject); | ||
74 | } | ||
75 | «ENDIF» | ||
76 | «ENDFOR» | ||
77 | pattern «patternName(null,null,type)»( | ||
78 | problem:LogicProblem, interpretation:PartialInterpretation, | ||
79 | typeInterpretation:PartialComplexTypeInterpretation) | ||
80 | { | ||
81 | find interpretation(problem,interpretation); | ||
82 | neg find «hasElementInContainmentName»(problem,interpretation); | ||
83 | PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation); | ||
84 | PartialComplexTypeInterpretation.interpretationOf.name(type,"«type.name»"); | ||
85 | «base.typeIndexer.referInstanceOf(type,Modality.MAY,"newObject")» | ||
86 | find mayExist(problem, interpretation, newObject); | ||
87 | neg find mustExist(problem, interpretation, newObject); | ||
88 | } | ||
89 | «ELSE» | ||
90 | pattern createObject_«this.patternName(null,null,type)»( | ||
91 | problem:LogicProblem, interpretation:PartialInterpretation, | ||
92 | typeInterpretation:PartialComplexTypeInterpretation) | ||
93 | { | ||
94 | find interpretation(problem,interpretation); | ||
95 | PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation); | ||
96 | PartialComplexTypeInterpretation.interpretationOf.name(typeInterpretation,"«type.name»"); | ||
97 | «base.typeIndexer.referInstanceOf(type,Modality.MAY,"newObject")» | ||
98 | find mayExist(problem, interpretation, newObject); | ||
99 | neg find mustExist(problem, interpretation, newObject); | ||
100 | } | ||
101 | «ENDIF» | ||
102 | «ENDFOR» | ||
101 | ''' | 103 | ''' |
102 | } | 104 | } |
103 | 105 | ||
104 | override generateRefineTypeQueries(LogicProblem p, PartialInterpretation emptySolution, TypeAnalysisResult typeAnalysisResult) { | 106 | override generateRefineTypeQueries(LogicProblem p, PartialInterpretation emptySolution, |
107 | TypeAnalysisResult typeAnalysisResult) { | ||
105 | return ''' | 108 | return ''' |
106 | «FOR type : p.types.filter(TypeDeclaration).filter[!it.isAbstract]» | 109 | «FOR type : p.types.filter(TypeDeclaration).filter[!it.isAbstract]» |
107 | pattern refineTypeTo_«base.canonizeName(type.name)»(problem:LogicProblem, interpretation:PartialInterpretation, object: DefinedElement) { | 110 | pattern refineTypeTo_«base.canonizeName(type.name)»(problem:LogicProblem, interpretation:PartialInterpretation, object: DefinedElement) { |
108 | find interpretation(problem,interpretation); | 111 | find interpretation(problem,interpretation); |
109 | find mustExist(problem, interpretation, object); | 112 | find mustExist(problem, interpretation, object); |
110 | «base.typeIndexer.referInstanceOf(type,Modality.MAY,"object")» | 113 | «base.typeIndexer.referInstanceOf(type,Modality.MAY,"object")» |
111 | neg «base.typeIndexer.referInstanceOf(type,Modality.MUST,"object")» | 114 | neg «base.typeIndexer.referInstanceOf(type,Modality.MUST,"object")» |
112 | } | 115 | } |
113 | «ENDFOR» | 116 | «ENDFOR» |
114 | ''' | 117 | ''' |
115 | } | 118 | } |
116 | 119 | ||
117 | override getRefineTypeQueryNames(LogicProblem p, PartialInterpretation emptySolution, TypeAnalysisResult typeAnalysisResult) { | 120 | override getRefineTypeQueryNames(LogicProblem p, PartialInterpretation emptySolution, |
121 | TypeAnalysisResult typeAnalysisResult) { | ||
118 | p.types.filter(TypeDeclaration).toInvertedMap['''refineTypeTo_«base.canonizeName(it.name)»'''] | 122 | p.types.filter(TypeDeclaration).toInvertedMap['''refineTypeTo_«base.canonizeName(it.name)»'''] |
119 | } | 123 | } |
120 | } \ No newline at end of file | 124 | } |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeIndexer.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeIndexer.xtend index d1d57189..7d687e99 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeIndexer.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeIndexer.xtend | |||
@@ -1,52 +1,122 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns | 1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns |
2 | 2 | ||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
5 | import org.eclipse.emf.ecore.EClass | ||
6 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality | ||
7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | ||
8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysisResult | ||
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference | ||
10 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference | 3 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference |
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference | ||
11 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntTypeReference | 5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntTypeReference |
12 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference | 6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference |
13 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.StringTypeReference | 7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.StringTypeReference |
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | ||
10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality | ||
11 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysisResult | ||
12 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | ||
14 | import java.math.BigDecimal | 13 | import java.math.BigDecimal |
14 | import org.eclipse.emf.ecore.EClass | ||
15 | import org.eclipse.xtend.lib.annotations.Accessors | ||
16 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor | ||
15 | 17 | ||
18 | @FinalFieldsConstructor | ||
16 | abstract class TypeIndexer { | 19 | abstract class TypeIndexer { |
17 | public def CharSequence getRequiredQueries() | 20 | @Accessors(PROTECTED_GETTER) val PatternGenerator base |
18 | public def boolean requiresTypeAnalysis() | 21 | |
19 | public def CharSequence generateInstanceOfQueries(LogicProblem problem,PartialInterpretation emptySolution,TypeAnalysisResult typeAnalysisResult) | 22 | def CharSequence getRequiredQueries() ''' |
20 | public def CharSequence referInstanceOf(Type type, Modality modality, String variableName) | 23 | private pattern typeInterpretation(problem:LogicProblem, interpretation:PartialInterpretation, type:TypeDeclaration, typeInterpretation:PartialComplexTypeInterpretation) { |
21 | public def CharSequence referInstanceOf(EClass type, Modality modality, String variableName) | 24 | find interpretation(problem,interpretation); |
22 | 25 | LogicProblem.types(problem,type); | |
23 | public def dispatch CharSequence referInstanceOfByReference(ComplexTypeReference reference, Modality modality, String variableName) { | 26 | PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation); |
24 | reference.referred.referInstanceOf(modality,variableName) | 27 | PartialComplexTypeInterpretation.interpretationOf(typeInterpretation,type); |
25 | } | 28 | } |
26 | public def dispatch CharSequence referInstanceOfByReference(BoolTypeReference reference, Modality modality, String variableName) { | 29 | |
30 | private pattern directInstanceOf(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement, type:Type) { | ||
31 | find interpretation(problem,interpretation); | ||
32 | LogicProblem.types(problem,type); | ||
33 | TypeDefinition.elements(type,element); | ||
34 | } or { | ||
35 | find interpretation(problem,interpretation); | ||
36 | find typeInterpretation(problem,interpretation,type,typeInterpretation); | ||
37 | PartialComplexTypeInterpretation.elements(typeInterpretation,element); | ||
38 | } | ||
39 | |||
40 | private pattern isPrimitive(element: PrimitiveElement) { | ||
41 | PrimitiveElement(element); | ||
42 | } | ||
43 | ''' | ||
44 | |||
45 | def boolean requiresTypeAnalysis() | ||
46 | |||
47 | def CharSequence generateInstanceOfQueries(LogicProblem problem, PartialInterpretation emptySolution, | ||
48 | TypeAnalysisResult typeAnalysisResult) ''' | ||
49 | «FOR type : problem.types» | ||
50 | «problem.generateMustInstenceOf(type, typeAnalysisResult)» | ||
51 | «problem.generateMayInstanceOf(type, typeAnalysisResult)» | ||
52 | «ENDFOR» | ||
53 | ''' | ||
54 | |||
55 | protected def CharSequence generateMustInstenceOf(LogicProblem problem, Type type, | ||
56 | TypeAnalysisResult typeAnalysisResult) ''' | ||
57 | /** | ||
58 | * An element must be an instance of type "«type.name»". | ||
59 | */ | ||
60 | private pattern «patternName(type,Modality.MUST)»(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) { | ||
61 | Type.name(type,"«type.name»"); | ||
62 | find directInstanceOf(problem,interpretation,element,type); | ||
63 | } | ||
64 | ''' | ||
65 | |||
66 | protected def CharSequence generateMayInstanceOf(LogicProblem problem, Type type, | ||
67 | TypeAnalysisResult typeAnalysisResult) | ||
68 | |||
69 | protected def patternName(Type type, | ||
70 | Modality modality) '''«modality.toBase»InstanceOf«base.canonizeName(type.name)»''' | ||
71 | |||
72 | def referInstanceOf(Type type, Modality modality, String variableName) { | ||
73 | '''find «patternName(type,modality)»(problem,interpretation,«variableName»);''' | ||
74 | } | ||
75 | |||
76 | def referInstanceOf(EClass type, Modality modality, String variableName) { | ||
77 | '''find «modality.toBase»InstanceOf«base.canonizeName('''«type.name» class''')»(problem,interpretation,«variableName»);''' | ||
78 | } | ||
79 | |||
80 | def dispatch CharSequence referInstanceOfByReference(ComplexTypeReference reference, Modality modality, | ||
81 | String variableName) { | ||
82 | reference.referred.referInstanceOf(modality, variableName) | ||
83 | } | ||
84 | |||
85 | def dispatch CharSequence referInstanceOfByReference(BoolTypeReference reference, Modality modality, | ||
86 | String variableName) { | ||
27 | '''BooleanElement(«variableName»);''' | 87 | '''BooleanElement(«variableName»);''' |
28 | } | 88 | } |
29 | public def dispatch CharSequence referInstanceOfByReference(IntTypeReference reference, Modality modality, String variableName) { | 89 | |
90 | def dispatch CharSequence referInstanceOfByReference(IntTypeReference reference, Modality modality, | ||
91 | String variableName) { | ||
30 | '''IntegerElement(«variableName»);''' | 92 | '''IntegerElement(«variableName»);''' |
31 | } | 93 | } |
32 | public def dispatch CharSequence referInstanceOfByReference(RealTypeReference reference, Modality modality, String variableName) { | 94 | |
95 | def dispatch CharSequence referInstanceOfByReference(RealTypeReference reference, Modality modality, | ||
96 | String variableName) { | ||
33 | '''RealElement(«variableName»);''' | 97 | '''RealElement(«variableName»);''' |
34 | } | 98 | } |
35 | public def dispatch CharSequence referInstanceOfByReference(StringTypeReference reference, Modality modality, String variableName) { | 99 | |
100 | def dispatch CharSequence referInstanceOfByReference(StringTypeReference reference, Modality modality, | ||
101 | String variableName) { | ||
36 | '''StringElement(«variableName»);''' | 102 | '''StringElement(«variableName»);''' |
37 | } | 103 | } |
38 | public def dispatch CharSequence referPrimitiveValue(String variableName, Boolean value) { | 104 | |
105 | def dispatch CharSequence referPrimitiveValue(String variableName, Boolean value) { | ||
39 | '''BooleanElement.value(«variableName»,«value»);''' | 106 | '''BooleanElement.value(«variableName»,«value»);''' |
40 | } | 107 | } |
41 | public def dispatch CharSequence referPrimitiveValue(String variableName, Integer value) { | 108 | |
109 | def dispatch CharSequence referPrimitiveValue(String variableName, Integer value) { | ||
42 | '''IntegerElement.value(«variableName»,«value»);''' | 110 | '''IntegerElement.value(«variableName»,«value»);''' |
43 | } | 111 | } |
44 | public def dispatch CharSequence referPrimitiveValue(String variableName, BigDecimal value) { | 112 | |
113 | def dispatch CharSequence referPrimitiveValue(String variableName, BigDecimal value) { | ||
45 | '''RealElement.value(«variableName»,«value»);''' | 114 | '''RealElement.value(«variableName»,«value»);''' |
46 | } | 115 | } |
47 | ///TODO: de-escaping string literals | 116 | |
48 | public def dispatch CharSequence referPrimitiveValue(String variableName, String value) { | 117 | def dispatch CharSequence referPrimitiveValue(String variableName, String value) { |
118 | // /TODO: de-escaping string literals | ||
49 | '''StringElement.value(«variableName»,"«value»");''' | 119 | '''StringElement.value(«variableName»,"«value»");''' |
50 | } | 120 | } |
51 | 121 | ||
52 | } \ No newline at end of file | 122 | } |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeIndexerWithPreliminaryTypeAnalysis.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeIndexerWithPreliminaryTypeAnalysis.xtend index d3af0426..0393b803 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeIndexerWithPreliminaryTypeAnalysis.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeIndexerWithPreliminaryTypeAnalysis.xtend | |||
@@ -4,113 +4,51 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | |||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | 4 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem |
5 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality | 5 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality |
6 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysisResult | 6 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysisResult |
7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeRefinementPrecondition | ||
8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | ||
9 | import org.eclipse.emf.ecore.EClass | ||
10 | 7 | ||
11 | class TypeIndexerWithPreliminaryTypeAnalysis extends TypeIndexer{ | 8 | class TypeIndexerWithPreliminaryTypeAnalysis extends TypeIndexer { |
12 | val PatternGenerator base; | ||
13 | |||
14 | new(PatternGenerator base) { | 9 | new(PatternGenerator base) { |
15 | this.base = base | 10 | super(base) |
16 | } | 11 | } |
12 | |||
17 | override requiresTypeAnalysis() { true } | 13 | override requiresTypeAnalysis() { true } |
18 | 14 | ||
19 | override getRequiredQueries() ''' | 15 | protected override generateMayInstanceOf(LogicProblem problem, Type type, TypeAnalysisResult typeAnalysisResult) { |
20 | private pattern typeInterpretation(problem:LogicProblem, interpretation:PartialInterpretation, type:TypeDeclaration, typeInterpretation:PartialComplexTypeInterpretation) { | 16 | val precondition = typeAnalysisResult?.mayNewTypePreconditions?.get(type) |
21 | find interpretation(problem,interpretation); | 17 | val inhibitorTypes = precondition?.inhibitorTypes |
22 | LogicProblem.types(problem,type); | ||
23 | PartialInterpretation.partialtypeinterpratation(interpretation,typeInterpretation); | ||
24 | PartialComplexTypeInterpretation.interpretationOf(typeInterpretation,type); | ||
25 | } | ||
26 | |||
27 | private pattern directInstanceOf(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement, type:Type) { | ||
28 | find interpretation(problem,interpretation); | ||
29 | LogicProblem.types(problem,type); | ||
30 | TypeDefinition.elements(type,element); | ||
31 | } or { | ||
32 | find interpretation(problem,interpretation); | ||
33 | find typeInterpretation(problem,interpretation,type,typeInterpretation); | ||
34 | PartialComplexTypeInterpretation.elements(typeInterpretation,element); | ||
35 | } | ||
36 | |||
37 | private pattern isPrimitive(element: PrimitiveElement) { | ||
38 | PrimitiveElement(element); | ||
39 | } | ||
40 | ''' | ||
41 | |||
42 | override generateInstanceOfQueries(LogicProblem problem, PartialInterpretation emptySolution, TypeAnalysisResult typeAnalysisResult) { | ||
43 | val mayNewTypePreconditions = typeAnalysisResult.mayNewTypePreconditions | ||
44 | |||
45 | return ''' | ||
46 | «FOR type:problem.types» | ||
47 | «problem.generateMustInstenceOf(type)» | ||
48 | «problem.generateMayInstanceOf(type,mayNewTypePreconditions.get(type))» | ||
49 | «ENDFOR» | ||
50 | ''' | ||
51 | } | ||
52 | |||
53 | private def patternName(Type type, Modality modality) | ||
54 | '''«modality.toString.toLowerCase»InstanceOf«base.canonizeName(type.name)»''' | ||
55 | |||
56 | private def generateMustInstenceOf(LogicProblem problem, Type type) { | ||
57 | ''' | ||
58 | /** | ||
59 | * An element must be an instance of type "«type.name»". | ||
60 | */ | ||
61 | private pattern «patternName(type,Modality.MUST)»(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) { | ||
62 | Type.name(type,"«type.name»"); | ||
63 | find directInstanceOf(problem,interpretation,element,type); | ||
64 | } | ||
65 | ''' | ||
66 | } | ||
67 | |||
68 | private def generateMayInstanceOf(LogicProblem problem, Type type, TypeRefinementPrecondition precondition) { | ||
69 | val inhibitorTypes = if(precondition!=null) { | ||
70 | precondition.inhibitorTypes | ||
71 | } else { | ||
72 | null | ||
73 | } | ||
74 | ''' | 18 | ''' |
75 | private pattern scopeDisallowsNew«base.canonizeName(type.name)»(problem:LogicProblem, interpretation:PartialInterpretation) { | 19 | private pattern scopeDisallowsNew«base.canonizeName(type.name)»(problem:LogicProblem, interpretation:PartialInterpretation) { |
76 | find interpretation(problem,interpretation); | 20 | find interpretation(problem,interpretation); |
77 | PartialInterpretation.scopes(interpretation,scope); | 21 | PartialInterpretation.scopes(interpretation,scope); |
78 | Scope.targetTypeInterpretation(scope,typeInterpretation); | 22 | Scope.targetTypeInterpretation(scope,typeInterpretation); |
79 | Scope.maxNewElements(scope,0); | 23 | Scope.maxNewElements(scope,0); |
80 | PartialComplexTypeInterpretation.interpretationOf(typeInterpretation,type); | 24 | PartialComplexTypeInterpretation.interpretationOf(typeInterpretation,type); |
81 | Type.name(type,"«type.name»"); | 25 | Type.name(type,"«type.name»"); |
82 | } | 26 | } |
83 | 27 | ||
84 | /** | 28 | /** |
85 | * An element may be an instance of type "«type.name»". | 29 | * An element may be an instance of type "«type.name»". |
86 | */ | 30 | */ |
87 | private pattern «patternName(type,Modality.MAY)»(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) | 31 | private pattern «patternName(type,Modality.MAY)»(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) |
88 | «IF inhibitorTypes !== null»{ | 32 | «IF inhibitorTypes !== null» |
89 | find interpretation(problem,interpretation); | 33 | { |
90 | PartialInterpretation.newElements(interpretation,element); | 34 | find interpretation(problem,interpretation); |
91 | «FOR inhibitorType : inhibitorTypes» | 35 | PartialInterpretation.newElements(interpretation,element); |
92 | neg «referInstanceOf(inhibitorType,Modality.MUST,"element")» | 36 | «FOR inhibitorType : inhibitorTypes» |
93 | «ENDFOR» | 37 | neg «referInstanceOf(inhibitorType,Modality.MUST,"element")» |
94 | neg find scopeDisallowsNew«base.canonizeName(type.name)»(problem, interpretation); | 38 | «ENDFOR» |
95 | neg find isPrimitive(element); | 39 | neg find scopeDisallowsNew«base.canonizeName(type.name)»(problem, interpretation); |
96 | } or { | 40 | neg find isPrimitive(element); |
97 | find interpretation(problem,interpretation); | 41 | } or { |
98 | PartialInterpretation.openWorldElements(interpretation,element); | 42 | find interpretation(problem,interpretation); |
99 | «FOR inhibitorType : inhibitorTypes» | 43 | PartialInterpretation.openWorldElements(interpretation,element); |
100 | neg «referInstanceOf(inhibitorType,Modality.MUST,"element")» | 44 | «FOR inhibitorType : inhibitorTypes» |
101 | «ENDFOR» | 45 | neg «referInstanceOf(inhibitorType,Modality.MUST,"element")» |
102 | neg find scopeDisallowsNew«base.canonizeName(type.name)»(problem, interpretation); | 46 | «ENDFOR» |
103 | neg find isPrimitive(element); | 47 | neg find scopeDisallowsNew«base.canonizeName(type.name)»(problem, interpretation); |
104 | } or | 48 | neg find isPrimitive(element); |
105 | «ENDIF» | 49 | } or |
106 | { «referInstanceOf(type,Modality.MUST,"element")» } | 50 | «ENDIF» |
51 | { «referInstanceOf(type,Modality.MUST,"element")» } | ||
107 | ''' | 52 | ''' |
108 | } | 53 | } |
109 | 54 | } | |
110 | public override referInstanceOf(Type type, Modality modality, String variableName) { | ||
111 | '''find «patternName(type,modality)»(problem,interpretation,«variableName»);''' | ||
112 | } | ||
113 | public override referInstanceOf(EClass type, Modality modality, String variableName) { | ||
114 | '''find «modality.toString.toLowerCase»InstanceOf«base.canonizeName('''«type.name» class''')»(problem,interpretation,«variableName»);''' | ||
115 | } | ||
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/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 286756a8..15b5a047 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 | |||
@@ -74,7 +74,7 @@ class UnfinishedIndexer { | |||
74 | «ENDIF» | 74 | «ENDIF» |
75 | 75 | ||
76 | «IF indexUpperMultiplicities» | 76 | «IF indexUpperMultiplicities» |
77 | «IF constraint.constrainsUnrepairable» | 77 | «IF constraint.constrainsUnrepairable || constraint.constrainsRemainingInverse» |
78 | private pattern «repairMatchName(constraint)»(problem:LogicProblem, interpretation:PartialInterpretation, source:DefinedElement, target:DefinedElement) { | 78 | private pattern «repairMatchName(constraint)»(problem:LogicProblem, interpretation:PartialInterpretation, source:DefinedElement, target:DefinedElement) { |
79 | find interpretation(problem,interpretation); | 79 | find interpretation(problem,interpretation); |
80 | find mustExist(problem,interpretation,source); | 80 | find mustExist(problem,interpretation,source); |
@@ -84,15 +84,17 @@ class UnfinishedIndexer { | |||
84 | neg «base.referRelation(constraint.relation,"source","target",Modality.MUST,fqn2PQuery)» | 84 | neg «base.referRelation(constraint.relation,"source","target",Modality.MUST,fqn2PQuery)» |
85 | «base.referRelation(constraint.relation,"source","target",Modality.MAY,fqn2PQuery)» | 85 | «base.referRelation(constraint.relation,"source","target",Modality.MAY,fqn2PQuery)» |
86 | } | 86 | } |
87 | 87 | «ENDIF» | |
88 | |||
89 | «IF constraint.constrainsUnrepairable» | ||
88 | private pattern «unrepairableMultiplicityName(constraint)»_helper(problem:LogicProblem, interpretation:PartialInterpretation, object:DefinedElement, unrepairableMultiplicity:java Integer) { | 90 | private pattern «unrepairableMultiplicityName(constraint)»_helper(problem:LogicProblem, interpretation:PartialInterpretation, object:DefinedElement, unrepairableMultiplicity:java Integer) { |
89 | find interpretation(problem,interpretation); | 91 | find interpretation(problem,interpretation); |
90 | find mustExist(problem,interpretation,object); | 92 | find mustExist(problem,interpretation,object); |
91 | «base.typeIndexer.referInstanceOf(constraint.sourceType,Modality::MUST,"object")» | 93 | «base.typeIndexer.referInstanceOf(constraint.sourceType,Modality::MUST,"object")» |
92 | find «unfinishedMultiplicityName(constraint)»_helper(problem, interpretation, object, missingMultiplicity); | 94 | find «unfinishedMultiplicityName(constraint)»_helper(problem, interpretation, object, missingMultiplicity); |
93 | numerOfRepairMatches == count find «repairMatchName(constraint)»(problem, interpretation, object, _); | 95 | numberOfRepairMatches == count find «repairMatchName(constraint)»(problem, interpretation, object, _); |
94 | check(numerOfRepairMatches < missingMultiplicity); | 96 | check(numberOfRepairMatches < missingMultiplicity); |
95 | unrepairableMultiplicity == eval(missingMultiplicity-numerOfRepairMatches); | 97 | unrepairableMultiplicity == eval(missingMultiplicity-numberOfRepairMatches); |
96 | } | 98 | } |
97 | 99 | ||
98 | private pattern «unrepairableMultiplicityName(constraint)»(problem:LogicProblem, interpretation:PartialInterpretation, unrepairableMultiplicity:java Integer) { | 100 | private pattern «unrepairableMultiplicityName(constraint)»(problem:LogicProblem, interpretation:PartialInterpretation, unrepairableMultiplicity:java Integer) { |
@@ -112,7 +114,8 @@ class UnfinishedIndexer { | |||
112 | «base.typeIndexer.referInstanceOf(constraint.targetType,Modality::MUST,"object")» | 114 | «base.typeIndexer.referInstanceOf(constraint.targetType,Modality::MUST,"object")» |
113 | numberOfExistingReferences == count «base.referRelation(constraint.relation,"_","object",Modality.MUST,fqn2PQuery)» | 115 | numberOfExistingReferences == count «base.referRelation(constraint.relation,"_","object",Modality.MUST,fqn2PQuery)» |
114 | check(numberOfExistingReferences < «constraint.inverseUpperBound»); | 116 | check(numberOfExistingReferences < «constraint.inverseUpperBound»); |
115 | remainingMultiplicity == eval(«constraint.inverseUpperBound»-numberOfExistingReferences); | 117 | numberOfRepairMatches == count find «repairMatchName(constraint)»(problem, interpretation, _, object); |
118 | remainingMultiplicity == eval(Math.min(«constraint.inverseUpperBound»-numberOfExistingReferences, numberOfRepairMatches)); | ||
116 | } | 119 | } |
117 | 120 | ||
118 | pattern «remainingMultiplicityName(constraint)»(problem:LogicProblem, interpretation:PartialInterpretation, remainingMultiplicity:java Integer) { | 121 | pattern «remainingMultiplicityName(constraint)»(problem:LogicProblem, interpretation:PartialInterpretation, remainingMultiplicity:java Integer) { |