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 | |
| 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.
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() { |