diff options
author | Kristóf Marussy <kris7topher@gmail.com> | 2019-07-14 00:56:19 +0200 |
---|---|---|
committer | Kristóf Marussy <kris7topher@gmail.com> | 2019-07-14 00:56:19 +0200 |
commit | fc505b6b171a2d54c3bad6078031b028b55131d3 (patch) | |
tree | 8eaa033e053e21ca60bd7f958055cc46e93b7cba /Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend | |
parent | Try fix statecode bug (diff) | |
download | VIATRA-Generator-fc505b6b171a2d54c3bad6078031b028b55131d3.tar.gz VIATRA-Generator-fc505b6b171a2d54c3bad6078031b028b55131d3.tar.zst VIATRA-Generator-fc505b6b171a2d54c3bad6078031b028b55131d3.zip |
Polyhedron abstraction with Z3 for cardinality propagation
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend')
-rw-r--r-- | Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend | 149 |
1 files changed, 149 insertions, 0 deletions
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend new file mode 100644 index 00000000..c8fb3409 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend | |||
@@ -0,0 +1,149 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialComplexTypeInterpretation | ||
4 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | ||
5 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialTypeInterpratation | ||
6 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.Scope | ||
7 | import java.util.HashMap | ||
8 | import java.util.HashSet | ||
9 | import java.util.Map | ||
10 | import java.util.Set | ||
11 | import org.eclipse.xtend.lib.annotations.Accessors | ||
12 | |||
13 | enum ScopePropagatorStrategy { | ||
14 | BasicTypeHierarchy, | ||
15 | PolyhedralTypeHierarchy | ||
16 | } | ||
17 | |||
18 | class ScopePropagator { | ||
19 | @Accessors(PROTECTED_GETTER) PartialInterpretation partialInterpretation | ||
20 | Map<PartialTypeInterpratation, Scope> type2Scope | ||
21 | |||
22 | val Map<Scope, Set<Scope>> superScopes | ||
23 | val Map<Scope, Set<Scope>> subScopes | ||
24 | |||
25 | new(PartialInterpretation p) { | ||
26 | partialInterpretation = p | ||
27 | type2Scope = new HashMap | ||
28 | for (scope : p.scopes) { | ||
29 | type2Scope.put(scope.targetTypeInterpretation, scope) | ||
30 | } | ||
31 | |||
32 | superScopes = new HashMap | ||
33 | subScopes = new HashMap | ||
34 | for (scope : p.scopes) { | ||
35 | superScopes.put(scope, new HashSet) | ||
36 | subScopes.put(scope, new HashSet) | ||
37 | } | ||
38 | |||
39 | for (scope : p.scopes) { | ||
40 | val target = scope.targetTypeInterpretation | ||
41 | if (target instanceof PartialComplexTypeInterpretation) { | ||
42 | val supertypeInterpretations = target.supertypeInterpretation | ||
43 | for (supertypeInterpretation : supertypeInterpretations) { | ||
44 | val supertypeScope = type2Scope.get(supertypeInterpretation) | ||
45 | superScopes.get(scope).add(supertypeScope) | ||
46 | subScopes.get(supertypeScope).add(scope) | ||
47 | } | ||
48 | } | ||
49 | } | ||
50 | } | ||
51 | |||
52 | def propagateAllScopeConstraints() { | ||
53 | var boolean hadChanged | ||
54 | do { | ||
55 | hadChanged = false | ||
56 | for (superScopeEntry : superScopes.entrySet) { | ||
57 | val sub = superScopeEntry.key | ||
58 | hadChanged = propagateLowerLimitUp(sub, partialInterpretation) || hadChanged | ||
59 | hadChanged = propagateUpperLimitDown(sub, partialInterpretation) || hadChanged | ||
60 | for (sup : superScopeEntry.value) { | ||
61 | hadChanged = propagateLowerLimitUp(sub, sup) || hadChanged | ||
62 | hadChanged = propagateUpperLimitDown(sub, sup) || hadChanged | ||
63 | } | ||
64 | } | ||
65 | } while (hadChanged) | ||
66 | } | ||
67 | |||
68 | def propagateAdditionToType(PartialTypeInterpratation t) { | ||
69 | // println('''Adding to «(t as PartialComplexTypeInterpretation).interpretationOf.name»''') | ||
70 | val targetScope = type2Scope.get(t) | ||
71 | targetScope.removeOne | ||
72 | val sups = superScopes.get(targetScope) | ||
73 | sups.forEach[removeOne] | ||
74 | if (this.partialInterpretation.minNewElements > 0) { | ||
75 | this.partialInterpretation.minNewElements = this.partialInterpretation.minNewElements - 1 | ||
76 | } | ||
77 | if (this.partialInterpretation.maxNewElements > 0) { | ||
78 | this.partialInterpretation.maxNewElements = this.partialInterpretation.maxNewElements - 1 | ||
79 | } else if (this.partialInterpretation.maxNewElements === 0) { | ||
80 | throw new IllegalArgumentException('''Inconsistent object creation: lower node limit is 0!''') | ||
81 | } | ||
82 | propagateAllScopeConstraints | ||
83 | |||
84 | // println('''Target Scope: «targetScope.minNewElements» - «targetScope.maxNewElements»''') | ||
85 | // println(''' «this.partialInterpretation.minNewElements» - «this.partialInterpretation.maxNewElements»''') | ||
86 | // this.partialInterpretation.scopes.forEach[println(''' «(it.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name»: «it.minNewElements»-«it.maxNewElements»''')] | ||
87 | // println('''All constraints are propagated upon increasing «(t as PartialComplexTypeInterpretation).interpretationOf.name»''') | ||
88 | } | ||
89 | |||
90 | private def propagateLowerLimitUp(Scope subScope, Scope superScope) { | ||
91 | if (subScope.minNewElements > superScope.minNewElements) { | ||
92 | superScope.minNewElements = subScope.minNewElements | ||
93 | return true | ||
94 | } else { | ||
95 | return false | ||
96 | } | ||
97 | } | ||
98 | |||
99 | private def propagateUpperLimitDown(Scope subScope, Scope superScope) { | ||
100 | if (superScope.maxNewElements >= 0 && | ||
101 | (superScope.maxNewElements < subScope.maxNewElements || subScope.maxNewElements < 0)) { | ||
102 | // println(''' | ||
103 | // «(subScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» -> «(superScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» | ||
104 | // subScope.maxNewElements «subScope.maxNewElements» = superScope.maxNewElements «superScope.maxNewElements» | ||
105 | // ''') | ||
106 | subScope.maxNewElements = superScope.maxNewElements | ||
107 | return true | ||
108 | } else { | ||
109 | return false | ||
110 | } | ||
111 | } | ||
112 | |||
113 | private def propagateLowerLimitUp(Scope subScope, PartialInterpretation p) { | ||
114 | if (subScope.minNewElements > p.minNewElements) { | ||
115 | // println(''' | ||
116 | // «(subScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» -> nodes | ||
117 | // p.minNewElements «p.minNewElements» = subScope.minNewElements «subScope.minNewElements» | ||
118 | // ''') | ||
119 | p.minNewElements = subScope.minNewElements | ||
120 | return true | ||
121 | } else { | ||
122 | return false | ||
123 | } | ||
124 | } | ||
125 | |||
126 | private def propagateUpperLimitDown(Scope subScope, PartialInterpretation p) { | ||
127 | if (p.maxNewElements >= 0 && (p.maxNewElements < subScope.maxNewElements || subScope.maxNewElements < 0)) { | ||
128 | // println(''' | ||
129 | // «(subScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» -> nodes | ||
130 | // subScope.maxNewElements «subScope.maxNewElements» = p.maxNewElements «p.maxNewElements» | ||
131 | // ''') | ||
132 | subScope.maxNewElements = p.maxNewElements | ||
133 | return true | ||
134 | } else { | ||
135 | return false | ||
136 | } | ||
137 | } | ||
138 | |||
139 | private def removeOne(Scope scope) { | ||
140 | if (scope.maxNewElements === 0) { | ||
141 | throw new IllegalArgumentException('''Inconsistent object creation: «scope.targetTypeInterpretation»''') | ||
142 | } else if (scope.maxNewElements > 0) { | ||
143 | scope.maxNewElements = scope.maxNewElements - 1 | ||
144 | } | ||
145 | if (scope.minNewElements > 0) { | ||
146 | scope.minNewElements = scope.minNewElements - 1 | ||
147 | } | ||
148 | } | ||
149 | } | ||