diff options
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality')
5 files changed, 115 insertions, 29 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 f6b101b6..e7e40ab0 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 | |||
@@ -2,9 +2,12 @@ package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality | |||
2 | 2 | ||
3 | import com.google.common.collect.ImmutableList | 3 | import com.google.common.collect.ImmutableList |
4 | import com.google.common.collect.ImmutableMap | 4 | import com.google.common.collect.ImmutableMap |
5 | import com.google.common.collect.ImmutableSet | ||
5 | import com.google.common.collect.Maps | 6 | import com.google.common.collect.Maps |
6 | import com.google.common.collect.Sets | 7 | import com.google.common.collect.Sets |
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | 9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type |
10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationStatistics | ||
8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.UnifinishedMultiplicityQueries | 11 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.UnifinishedMultiplicityQueries |
9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialComplexTypeInterpretation | 12 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialComplexTypeInterpretation |
10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | 13 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation |
@@ -30,13 +33,14 @@ class PolyhedronScopePropagator extends ScopePropagator { | |||
30 | val LinearBoundedExpression topLevelBounds | 33 | val LinearBoundedExpression topLevelBounds |
31 | val Polyhedron polyhedron | 34 | val Polyhedron polyhedron |
32 | val PolyhedronSaturationOperator operator | 35 | val PolyhedronSaturationOperator operator |
36 | val Set<Relation> relevantRelations | ||
33 | List<RelationConstraintUpdater> updaters = emptyList | 37 | List<RelationConstraintUpdater> updaters = emptyList |
34 | 38 | ||
35 | new(PartialInterpretation p, Set<? extends Type> possibleNewDynamicTypes, | 39 | new(PartialInterpretation p, ModelGenerationStatistics statistics, Set<? extends Type> possibleNewDynamicTypes, |
36 | Map<RelationMultiplicityConstraint, UnifinishedMultiplicityQueries> unfinishedMultiplicityQueries, | 40 | Map<RelationMultiplicityConstraint, UnifinishedMultiplicityQueries> unfinishedMultiplicityQueries, |
37 | IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> hasElementInContainmentQuery, | 41 | IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> hasElementInContainmentQuery, |
38 | PolyhedronSolver solver, boolean propagateRelations) { | 42 | PolyhedronSolver solver, boolean propagateRelations) { |
39 | super(p) | 43 | super(p, statistics) |
40 | val builder = new PolyhedronBuilder(p) | 44 | val builder = new PolyhedronBuilder(p) |
41 | builder.buildPolyhedron(possibleNewDynamicTypes) | 45 | builder.buildPolyhedron(possibleNewDynamicTypes) |
42 | scopeBounds = builder.scopeBounds | 46 | scopeBounds = builder.scopeBounds |
@@ -54,11 +58,14 @@ class PolyhedronScopePropagator extends ScopePropagator { | |||
54 | } | 58 | } |
55 | builder.buildMultiplicityConstraints(unfinishedMultiplicityQueries, hasElementInContainmentQuery, | 59 | builder.buildMultiplicityConstraints(unfinishedMultiplicityQueries, hasElementInContainmentQuery, |
56 | maximumNumberOfNewNodes) | 60 | maximumNumberOfNewNodes) |
61 | relevantRelations = builder.relevantRelations | ||
57 | updaters = builder.updaters | 62 | updaters = builder.updaters |
63 | } else { | ||
64 | relevantRelations = emptySet | ||
58 | } | 65 | } |
59 | } | 66 | } |
60 | 67 | ||
61 | override void propagateAllScopeConstraints() { | 68 | override void doPropagateAllScopeConstraints() { |
62 | resetBounds() | 69 | resetBounds() |
63 | populatePolyhedronFromScope() | 70 | populatePolyhedronFromScope() |
64 | // println(polyhedron) | 71 | // println(polyhedron) |
@@ -73,6 +80,13 @@ class PolyhedronScopePropagator extends ScopePropagator { | |||
73 | } | 80 | } |
74 | } | 81 | } |
75 | } | 82 | } |
83 | |||
84 | override propagateAdditionToRelation(Relation r) { | ||
85 | super.propagateAdditionToRelation(r) | ||
86 | if (relevantRelations.contains(r)) { | ||
87 | propagateAllScopeConstraints() | ||
88 | } | ||
89 | } | ||
76 | 90 | ||
77 | def resetBounds() { | 91 | def resetBounds() { |
78 | for (dimension : polyhedron.dimensions) { | 92 | for (dimension : polyhedron.dimensions) { |
@@ -188,6 +202,7 @@ class PolyhedronScopePropagator extends ScopePropagator { | |||
188 | Map<Scope, LinearBoundedExpression> scopeBounds | 202 | Map<Scope, LinearBoundedExpression> scopeBounds |
189 | LinearBoundedExpression topLevelBounds | 203 | LinearBoundedExpression topLevelBounds |
190 | Polyhedron polyhedron | 204 | Polyhedron polyhedron |
205 | Set<Relation> relevantRelations | ||
191 | List<RelationConstraintUpdater> updaters | 206 | List<RelationConstraintUpdater> updaters |
192 | 207 | ||
193 | def buildPolyhedron(Set<? extends Type> possibleNewDynamicTypes) { | 208 | def buildPolyhedron(Set<? extends Type> possibleNewDynamicTypes) { |
@@ -222,9 +237,21 @@ class PolyhedronScopePropagator extends ScopePropagator { | |||
222 | buildNonContainmentConstraints(constraint, pair.value) | 237 | buildNonContainmentConstraints(constraint, pair.value) |
223 | } | 238 | } |
224 | } | 239 | } |
240 | buildRelevantRelations(constraints.keySet) | ||
225 | updaters = updatersBuilder.build | 241 | updaters = updatersBuilder.build |
226 | addCachedConstraintsToPolyhedron() | 242 | addCachedConstraintsToPolyhedron() |
227 | } | 243 | } |
244 | |||
245 | private def buildRelevantRelations(Set<RelationMultiplicityConstraint> constraints) { | ||
246 | val builder = ImmutableSet.builder | ||
247 | for (constraint : constraints) { | ||
248 | builder.add(constraint.relation) | ||
249 | if (constraint.inverseRelation !== null) { | ||
250 | builder.add(constraint.inverseRelation) | ||
251 | } | ||
252 | } | ||
253 | relevantRelations = builder.build | ||
254 | } | ||
228 | 255 | ||
229 | private def addCachedConstraintsToPolyhedron() { | 256 | private def addCachedConstraintsToPolyhedron() { |
230 | val constraints = new HashSet | 257 | val constraints = new HashSet |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/RelationConstraintCalculator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/RelationConstraintCalculator.xtend index ffa9e6e6..52a390a8 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/RelationConstraintCalculator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/RelationConstraintCalculator.xtend | |||
@@ -20,6 +20,7 @@ class RelationConstraints { | |||
20 | @Data | 20 | @Data |
21 | class RelationMultiplicityConstraint { | 21 | class RelationMultiplicityConstraint { |
22 | Relation relation | 22 | Relation relation |
23 | Relation inverseRelation | ||
23 | boolean containment | 24 | boolean containment |
24 | boolean container | 25 | boolean container |
25 | int lowerBound | 26 | int lowerBound |
@@ -47,7 +48,7 @@ class RelationMultiplicityConstraint { | |||
47 | } | 48 | } |
48 | 49 | ||
49 | def constrainsRemainingInverse() { | 50 | def constrainsRemainingInverse() { |
50 | !containment && inverseUpperBoundFinite | 51 | lowerBound >= 1 && !containment && inverseUpperBoundFinite |
51 | } | 52 | } |
52 | 53 | ||
53 | def constrainsRemainingContents() { | 54 | def constrainsRemainingContents() { |
@@ -119,8 +120,8 @@ class RelationConstraintCalculator { | |||
119 | inverseUpperMultiplicity = upperMultiplicities.get(relation) | 120 | inverseUpperMultiplicity = upperMultiplicities.get(relation) |
120 | container = containmentRelations.contains(inverseRelation) | 121 | container = containmentRelations.contains(inverseRelation) |
121 | } | 122 | } |
122 | val constraint = new RelationMultiplicityConstraint(relation, containment, container, lowerMultiplicity, | 123 | val constraint = new RelationMultiplicityConstraint(relation, inverseRelation, containment, container, |
123 | upperMultiplicity, inverseUpperMultiplicity) | 124 | lowerMultiplicity, upperMultiplicity, inverseUpperMultiplicity) |
124 | if (constraint.isActive) { | 125 | if (constraint.isActive) { |
125 | if (relation.parameters.size != 2) { | 126 | if (relation.parameters.size != 2) { |
126 | throw new IllegalArgumentException('''Relation «relation.name» has multiplicity or containment constraints, but it is not binary''') | 127 | throw new IllegalArgumentException('''Relation «relation.name» has multiplicity or containment constraints, but it is not binary''') |
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 3b442cd3..7be6635c 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 | |||
@@ -1,5 +1,7 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality | 1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality |
2 | 2 | ||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation | ||
4 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationStatistics | ||
3 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialComplexTypeInterpretation | 5 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialComplexTypeInterpretation |
4 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | 6 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation |
5 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialTypeInterpratation | 7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialTypeInterpratation |
@@ -11,14 +13,15 @@ import java.util.Set | |||
11 | import org.eclipse.xtend.lib.annotations.Accessors | 13 | import org.eclipse.xtend.lib.annotations.Accessors |
12 | 14 | ||
13 | class ScopePropagator { | 15 | class ScopePropagator { |
14 | @Accessors(PROTECTED_GETTER) PartialInterpretation partialInterpretation | 16 | @Accessors(PROTECTED_GETTER) val PartialInterpretation partialInterpretation |
15 | Map<PartialTypeInterpratation, Scope> type2Scope | 17 | val ModelGenerationStatistics statistics |
16 | 18 | val Map<PartialTypeInterpratation, Scope> type2Scope | |
17 | val Map<Scope, Set<Scope>> superScopes | 19 | val Map<Scope, Set<Scope>> superScopes |
18 | val Map<Scope, Set<Scope>> subScopes | 20 | val Map<Scope, Set<Scope>> subScopes |
19 | 21 | ||
20 | new(PartialInterpretation p) { | 22 | new(PartialInterpretation p, ModelGenerationStatistics statistics) { |
21 | partialInterpretation = p | 23 | partialInterpretation = p |
24 | this.statistics = statistics | ||
22 | type2Scope = new HashMap | 25 | type2Scope = new HashMap |
23 | for (scope : p.scopes) { | 26 | for (scope : p.scopes) { |
24 | type2Scope.put(scope.targetTypeInterpretation, scope) | 27 | type2Scope.put(scope.targetTypeInterpretation, scope) |
@@ -57,8 +60,13 @@ class ScopePropagator { | |||
57 | } | 60 | } |
58 | } while (changed) | 61 | } while (changed) |
59 | } | 62 | } |
60 | 63 | ||
61 | def propagateAllScopeConstraints() { | 64 | def propagateAllScopeConstraints() { |
65 | statistics.incrementScopePropagationCount() | ||
66 | doPropagateAllScopeConstraints() | ||
67 | } | ||
68 | |||
69 | protected def doPropagateAllScopeConstraints() { | ||
62 | var boolean hadChanged | 70 | var boolean hadChanged |
63 | do { | 71 | do { |
64 | hadChanged = false | 72 | hadChanged = false |
@@ -95,6 +103,10 @@ class ScopePropagator { | |||
95 | // this.partialInterpretation.scopes.forEach[println(''' «(it.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name»: «it.minNewElements»-«it.maxNewElements»''')] | 103 | // this.partialInterpretation.scopes.forEach[println(''' «(it.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name»: «it.minNewElements»-«it.maxNewElements»''')] |
96 | // println('''All constraints are propagated upon increasing «(t as PartialComplexTypeInterpretation).interpretationOf.name»''') | 104 | // println('''All constraints are propagated upon increasing «(t as PartialComplexTypeInterpretation).interpretationOf.name»''') |
97 | } | 105 | } |
106 | |||
107 | def void propagateAdditionToRelation(Relation r) { | ||
108 | // Nothing to propagate. | ||
109 | } | ||
98 | 110 | ||
99 | private def propagateLowerLimitUp(Scope subScope, Scope superScope) { | 111 | private def propagateLowerLimitUp(Scope subScope, Scope superScope) { |
100 | if (subScope.minNewElements > superScope.minNewElements) { | 112 | if (subScope.minNewElements > superScope.minNewElements) { |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagatorStrategy.java b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagatorStrategy.java deleted file mode 100644 index b1c5a658..00000000 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagatorStrategy.java +++ /dev/null | |||
@@ -1,18 +0,0 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality; | ||
2 | |||
3 | public enum ScopePropagatorStrategy { | ||
4 | BasicTypeHierarchy, | ||
5 | |||
6 | PolyhedralTypeHierarchy, | ||
7 | |||
8 | PolyhedralRelations { | ||
9 | @Override | ||
10 | public boolean requiresUpperBoundIndexing() { | ||
11 | return true; | ||
12 | } | ||
13 | }; | ||
14 | |||
15 | public boolean requiresUpperBoundIndexing() { | ||
16 | return false; | ||
17 | } | ||
18 | } | ||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagatorStrategy.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagatorStrategy.xtend new file mode 100644 index 00000000..37e56c9a --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagatorStrategy.xtend | |||
@@ -0,0 +1,64 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality | ||
2 | |||
3 | import org.eclipse.xtend.lib.annotations.Data | ||
4 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor | ||
5 | |||
6 | enum PolyhedralScopePropagatorConstraints { | ||
7 | TypeHierarchy, | ||
8 | Relational | ||
9 | } | ||
10 | |||
11 | enum PolyhedralScopePropagatorSolver { | ||
12 | Z3Real, | ||
13 | Z3Integer, | ||
14 | Cbc, | ||
15 | Clp | ||
16 | } | ||
17 | |||
18 | abstract class ScopePropagatorStrategy { | ||
19 | public static val BasicCount = new Simple("BasicCount") | ||
20 | |||
21 | public static val BasicTypeHierarchy = new Simple("BasicTypeHierarchy") | ||
22 | |||
23 | private new() { | ||
24 | } | ||
25 | |||
26 | def boolean requiresUpperBoundIndexing() | ||
27 | |||
28 | static class Simple extends ScopePropagatorStrategy { | ||
29 | val String name | ||
30 | |||
31 | @FinalFieldsConstructor | ||
32 | private new() { | ||
33 | } | ||
34 | |||
35 | override requiresUpperBoundIndexing() { | ||
36 | false | ||
37 | } | ||
38 | |||
39 | override toString() { | ||
40 | name | ||
41 | } | ||
42 | } | ||
43 | |||
44 | @Data | ||
45 | static class Polyhedral extends ScopePropagatorStrategy { | ||
46 | public static val UNLIMITED_TIME = -1 | ||
47 | |||
48 | val PolyhedralScopePropagatorConstraints constraints | ||
49 | val PolyhedralScopePropagatorSolver solver | ||
50 | val double timeoutSeconds | ||
51 | |||
52 | @FinalFieldsConstructor | ||
53 | new() { | ||
54 | } | ||
55 | |||
56 | new(PolyhedralScopePropagatorConstraints constraints, PolyhedralScopePropagatorSolver solver) { | ||
57 | this(constraints, solver, UNLIMITED_TIME) | ||
58 | } | ||
59 | |||
60 | override requiresUpperBoundIndexing() { | ||
61 | constraints == PolyhedralScopePropagatorConstraints.Relational | ||
62 | } | ||
63 | } | ||
64 | } | ||