diff options
author | Kristóf Marussy <kris7topher@gmail.com> | 2019-07-14 20:48:09 +0200 |
---|---|---|
committer | Kristóf Marussy <kris7topher@gmail.com> | 2019-07-14 20:48:09 +0200 |
commit | c420930fbd57421e8accaf3d6af9baa3e868213b (patch) | |
tree | ebb666abf91246715889a39f61115bc1a387482e /Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu | |
parent | Polyhedron abstraction with Z3 for cardinality propagation (diff) | |
download | VIATRA-Generator-c420930fbd57421e8accaf3d6af9baa3e868213b.tar.gz VIATRA-Generator-c420930fbd57421e8accaf3d6af9baa3e868213b.tar.zst VIATRA-Generator-c420930fbd57421e8accaf3d6af9baa3e868213b.zip |
Transitive closure of type hierarchy in ScopePropagator
This does not mappter for propagateAllScopeConstraints(),
but propagateAdditionToType gets more exact this way.
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu')
2 files changed, 15 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/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 8f210ffb..cebd89da 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 | |||
@@ -27,6 +27,7 @@ class PolyhedronScopePropagator extends ScopePropagator { | |||
27 | // Dimensions for instantiable types were created according to the type analysis, | 27 | // Dimensions for instantiable types were created according to the type analysis, |
28 | // but for any possible primitive types, we create them on demand, | 28 | // but for any possible primitive types, we create them on demand, |
29 | // as there is no Type directly associated with a PartialPrimitiveInterpretation. | 29 | // as there is no Type directly associated with a PartialPrimitiveInterpretation. |
30 | // Below we will assume that each PartialTypeInterpretation has at most one Scope. | ||
30 | for (scope : p.scopes) { | 31 | for (scope : p.scopes) { |
31 | switch (targetTypeInterpretation : scope.targetTypeInterpretation) { | 32 | switch (targetTypeInterpretation : scope.targetTypeInterpretation) { |
32 | PartialPrimitiveInterpretation: { | 33 | PartialPrimitiveInterpretation: { |
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 index c8fb3409..f0494214 100644 --- 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 | |||
@@ -47,6 +47,20 @@ class ScopePropagator { | |||
47 | } | 47 | } |
48 | } | 48 | } |
49 | } | 49 | } |
50 | var boolean changed | ||
51 | do { | ||
52 | changed = false | ||
53 | for (scope : p.scopes) { | ||
54 | val subScopeSet = subScopes.get(scope) | ||
55 | val superScopeSet = superScopes.get(scope) | ||
56 | for (subScope : subScopeSet) { | ||
57 | changed = changed || superScopes.get(subScope).addAll(superScopeSet) | ||
58 | } | ||
59 | for (superScope : superScopeSet) { | ||
60 | changed = changed || subScopes.get(superScope).addAll(subScopeSet) | ||
61 | } | ||
62 | } | ||
63 | } while (changed) | ||
50 | } | 64 | } |
51 | 65 | ||
52 | def propagateAllScopeConstraints() { | 66 | def propagateAllScopeConstraints() { |