diff options
author | Kristóf Marussy <kris7topher@gmail.com> | 2019-08-01 01:00:12 +0200 |
---|---|---|
committer | Kristóf Marussy <kris7topher@gmail.com> | 2019-08-01 01:00:12 +0200 |
commit | 7021a4d1f2805ebf3145cbc3893761d12f23361f (patch) | |
tree | b75c51136d3b593f94bf517a8552a1dbf8abdd2b /Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu | |
parent | Build Cbc wrapper under Ubuntu 18.04 (diff) | |
download | VIATRA-Generator-7021a4d1f2805ebf3145cbc3893761d12f23361f.tar.gz VIATRA-Generator-7021a4d1f2805ebf3145cbc3893761d12f23361f.tar.zst VIATRA-Generator-7021a4d1f2805ebf3145cbc3893761d12f23361f.zip |
Configurability and better statistics for measurements
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu')
8 files changed, 187 insertions, 53 deletions
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend index 4b278188..8e061b63 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend | |||
@@ -27,6 +27,7 @@ import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher | |||
27 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery | 27 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery |
28 | import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRule | 28 | import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRule |
29 | import org.eclipse.xtend.lib.annotations.Data | 29 | import org.eclipse.xtend.lib.annotations.Data |
30 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Z3PolyhedronSolver | ||
30 | 31 | ||
31 | class ModelGenerationStatistics { | 32 | class ModelGenerationStatistics { |
32 | public var long transformationExecutionTime = 0 | 33 | public var long transformationExecutionTime = 0 |
@@ -35,7 +36,25 @@ class ModelGenerationStatistics { | |||
35 | transformationExecutionTime += amount | 36 | transformationExecutionTime += amount |
36 | } | 37 | } |
37 | 38 | ||
38 | public var long PreliminaryTypeAnalisisTime = 0 | 39 | public var long scopePropagationTime = 0 |
40 | |||
41 | synchronized def addScopePropagationTime(long amount) { | ||
42 | scopePropagationTime += amount | ||
43 | } | ||
44 | |||
45 | public var long preliminaryTypeAnalisisTime = 0 | ||
46 | |||
47 | public var int decisionsTried = 0 | ||
48 | |||
49 | synchronized def incrementDecisionCount() { | ||
50 | decisionsTried++ | ||
51 | } | ||
52 | |||
53 | public var int scopePropagatorInvocations | ||
54 | |||
55 | synchronized def incrementScopePropagationCount() { | ||
56 | scopePropagatorInvocations++ | ||
57 | } | ||
39 | } | 58 | } |
40 | 59 | ||
41 | @Data class ModelGenerationMethod { | 60 | @Data class ModelGenerationMethod { |
@@ -84,12 +103,12 @@ class ModelGenerationMethodProvider { | |||
84 | val relationConstraints = relationConstraintCalculator.calculateRelationConstraints(logicProblem) | 103 | val relationConstraints = relationConstraintCalculator.calculateRelationConstraints(logicProblem) |
85 | val queries = patternProvider.generateQueries(logicProblem, emptySolution, statistics, existingQueries, | 104 | val queries = patternProvider.generateQueries(logicProblem, emptySolution, statistics, existingQueries, |
86 | workspace, typeInferenceMethod, scopePropagatorStrategy, relationConstraints, writeFiles) | 105 | workspace, typeInferenceMethod, scopePropagatorStrategy, relationConstraints, writeFiles) |
87 | val scopePropagator = createScopePropagator(scopePropagatorStrategy, emptySolution, queries) | 106 | val scopePropagator = createScopePropagator(scopePropagatorStrategy, emptySolution, queries, statistics) |
88 | scopePropagator.propagateAllScopeConstraints | 107 | scopePropagator.propagateAllScopeConstraints |
89 | val // LinkedHashMap<Pair<Relation, ? extends Type>, BatchTransformationRule<GenericPatternMatch, ViatraQueryMatcher<GenericPatternMatch>>> | 108 | val objectRefinementRules = refinementRuleProvider.createObjectRefinementRules(queries, scopePropagator, |
90 | objectRefinementRules = refinementRuleProvider.createObjectRefinementRules(queries, scopePropagator, | ||
91 | nameNewElements, statistics) | 109 | nameNewElements, statistics) |
92 | val relationRefinementRules = refinementRuleProvider.createRelationRefinementRules(queries, statistics) | 110 | val relationRefinementRules = refinementRuleProvider.createRelationRefinementRules(queries, scopePropagator, |
111 | statistics) | ||
93 | 112 | ||
94 | val unfinishedMultiplicities = goalConstraintProvider.getUnfinishedMultiplicityQueries(queries) | 113 | val unfinishedMultiplicities = goalConstraintProvider.getUnfinishedMultiplicityQueries(queries) |
95 | val unfinishedWF = queries.getUnfinishedWFQueries.values | 114 | val unfinishedWF = queries.getUnfinishedWFQueries.values |
@@ -118,15 +137,26 @@ class ModelGenerationMethodProvider { | |||
118 | } | 137 | } |
119 | 138 | ||
120 | private def createScopePropagator(ScopePropagatorStrategy scopePropagatorStrategy, | 139 | private def createScopePropagator(ScopePropagatorStrategy scopePropagatorStrategy, |
121 | PartialInterpretation emptySolution, GeneratedPatterns queries) { | 140 | PartialInterpretation emptySolution, GeneratedPatterns queries, ModelGenerationStatistics statistics) { |
122 | switch (scopePropagatorStrategy) { | 141 | switch (scopePropagatorStrategy) { |
123 | case BasicTypeHierarchy: | 142 | case ScopePropagatorStrategy.BasicTypeHierarchy: |
124 | new ScopePropagator(emptySolution) | 143 | new ScopePropagator(emptySolution, statistics) |
125 | case PolyhedralTypeHierarchy, | 144 | ScopePropagatorStrategy.Polyhedral: { |
126 | case PolyhedralRelations: { | ||
127 | val types = queries.refineObjectQueries.keySet.map[newType].toSet | 145 | val types = queries.refineObjectQueries.keySet.map[newType].toSet |
128 | val solver = new CbcPolyhedronSolver | 146 | val solver = switch (scopePropagatorStrategy.solver) { |
129 | new PolyhedronScopePropagator(emptySolution, types, queries.multiplicityConstraintQueries, | 147 | case Z3Integer: |
148 | new Z3PolyhedronSolver(false, scopePropagatorStrategy.timeoutSeconds) | ||
149 | case Z3Real: | ||
150 | new Z3PolyhedronSolver(true, scopePropagatorStrategy.timeoutSeconds) | ||
151 | case Cbc: | ||
152 | new CbcPolyhedronSolver(false, scopePropagatorStrategy.timeoutSeconds, true) | ||
153 | case Clp: | ||
154 | new CbcPolyhedronSolver(true, scopePropagatorStrategy.timeoutSeconds, true) | ||
155 | default: | ||
156 | throw new IllegalArgumentException("Unknown polyhedron solver: " + | ||
157 | scopePropagatorStrategy.solver) | ||
158 | } | ||
159 | new PolyhedronScopePropagator(emptySolution, statistics, types, queries.multiplicityConstraintQueries, | ||
130 | queries.hasElementInContainmentQuery, solver, scopePropagatorStrategy.requiresUpperBoundIndexing) | 160 | queries.hasElementInContainmentQuery, solver, scopePropagatorStrategy.requiresUpperBoundIndexing) |
131 | } | 161 | } |
132 | default: | 162 | default: |
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 | } | ||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend index b10c8e88..eadf0ae0 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternProvider.xtend | |||
@@ -69,7 +69,7 @@ class PatternProvider { | |||
69 | val startTime = System.nanoTime | 69 | val startTime = System.nanoTime |
70 | val result = typeAnalysis.performTypeAnalysis(problem, emptySolution) | 70 | val result = typeAnalysis.performTypeAnalysis(problem, emptySolution) |
71 | val typeAnalysisTime = System.nanoTime - startTime | 71 | val typeAnalysisTime = System.nanoTime - startTime |
72 | statistics.PreliminaryTypeAnalisisTime = typeAnalysisTime | 72 | statistics.preliminaryTypeAnalisisTime = typeAnalysisTime |
73 | result | 73 | result |
74 | } else { | 74 | } else { |
75 | null | 75 | null |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend index 5fefa551..bf816de9 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend | |||
@@ -98,10 +98,12 @@ class RefinementRuleProvider { | |||
98 | val newLink2 = factory2.createBinaryElementRelationLink => [it.param1 = newElement it.param2 = container] | 98 | val newLink2 = factory2.createBinaryElementRelationLink => [it.param1 = newElement it.param2 = container] |
99 | inverseRelationInterpretation.relationlinks+=newLink2 | 99 | inverseRelationInterpretation.relationlinks+=newLink2 |
100 | 100 | ||
101 | val propagatorStartTime = System.nanoTime | ||
102 | statistics.addExecutionTime(propagatorStartTime-startTime) | ||
103 | |||
101 | // Scope propagation | 104 | // Scope propagation |
102 | scopePropagator.propagateAdditionToType(typeInterpretation) | 105 | scopePropagator.propagateAdditionToType(typeInterpretation) |
103 | 106 | statistics.addScopePropagationTime(System.nanoTime-propagatorStartTime) | |
104 | statistics.addExecutionTime(System.nanoTime-startTime) | ||
105 | ] | 107 | ] |
106 | } else { | 108 | } else { |
107 | ruleBuilder.action[match | | 109 | ruleBuilder.action[match | |
@@ -132,10 +134,12 @@ class RefinementRuleProvider { | |||
132 | val newLink = factory2.createBinaryElementRelationLink => [it.param1 = container it.param2 = newElement] | 134 | val newLink = factory2.createBinaryElementRelationLink => [it.param1 = container it.param2 = newElement] |
133 | relationInterpretation.relationlinks+=newLink | 135 | relationInterpretation.relationlinks+=newLink |
134 | 136 | ||
137 | val propagatorStartTime = System.nanoTime | ||
138 | statistics.addExecutionTime(propagatorStartTime-startTime) | ||
139 | |||
135 | // Scope propagation | 140 | // Scope propagation |
136 | scopePropagator.propagateAdditionToType(typeInterpretation) | 141 | scopePropagator.propagateAdditionToType(typeInterpretation) |
137 | 142 | statistics.addScopePropagationTime(System.nanoTime-propagatorStartTime) | |
138 | statistics.addExecutionTime(System.nanoTime-startTime) | ||
139 | ] | 143 | ] |
140 | } | 144 | } |
141 | } else { | 145 | } else { |
@@ -162,29 +166,31 @@ class RefinementRuleProvider { | |||
162 | typeInterpretation.elements += newElement | 166 | typeInterpretation.elements += newElement |
163 | typeInterpretation.supertypeInterpretation.forEach[it.elements += newElement] | 167 | typeInterpretation.supertypeInterpretation.forEach[it.elements += newElement] |
164 | 168 | ||
169 | val propagatorStartTime = System.nanoTime | ||
170 | statistics.addExecutionTime(propagatorStartTime-startTime) | ||
171 | |||
165 | // Scope propagation | 172 | // Scope propagation |
166 | scopePropagator.propagateAdditionToType(typeInterpretation) | 173 | scopePropagator.propagateAdditionToType(typeInterpretation) |
167 | 174 | statistics.addScopePropagationTime(System.nanoTime-propagatorStartTime) | |
168 | statistics.addExecutionTime(System.nanoTime-startTime) | ||
169 | ] | 175 | ] |
170 | } | 176 | } |
171 | return ruleBuilder.build | 177 | return ruleBuilder.build |
172 | } | 178 | } |
173 | 179 | ||
174 | def createRelationRefinementRules(GeneratedPatterns patterns, ModelGenerationStatistics statistics) { | 180 | def createRelationRefinementRules(GeneratedPatterns patterns, ScopePropagator scopePropagator, ModelGenerationStatistics statistics) { |
175 | val res = new LinkedHashMap | 181 | val res = new LinkedHashMap |
176 | for(LHSEntry: patterns.refinerelationQueries.entrySet) { | 182 | for(LHSEntry: patterns.refinerelationQueries.entrySet) { |
177 | val declaration = LHSEntry.key.key | 183 | val declaration = LHSEntry.key.key |
178 | val inverseReference = LHSEntry.key.value | 184 | val inverseReference = LHSEntry.key.value |
179 | val lhs = LHSEntry.value as IQuerySpecification<ViatraQueryMatcher<GenericPatternMatch>> | 185 | val lhs = LHSEntry.value as IQuerySpecification<ViatraQueryMatcher<GenericPatternMatch>> |
180 | val rule = createRelationRefinementRule(declaration,inverseReference,lhs,statistics) | 186 | val rule = createRelationRefinementRule(declaration,inverseReference,lhs,scopePropagator,statistics) |
181 | res.put(LHSEntry.key,rule) | 187 | res.put(LHSEntry.key,rule) |
182 | } | 188 | } |
183 | return res | 189 | return res |
184 | } | 190 | } |
185 | 191 | ||
186 | def private BatchTransformationRule<GenericPatternMatch, ViatraQueryMatcher<GenericPatternMatch>> | 192 | def private BatchTransformationRule<GenericPatternMatch, ViatraQueryMatcher<GenericPatternMatch>> |
187 | createRelationRefinementRule(RelationDeclaration declaration, Relation inverseRelation, IQuerySpecification<ViatraQueryMatcher<GenericPatternMatch>> lhs, ModelGenerationStatistics statistics) | 193 | createRelationRefinementRule(RelationDeclaration declaration, Relation inverseRelation, IQuerySpecification<ViatraQueryMatcher<GenericPatternMatch>> lhs, ScopePropagator scopePropagator, ModelGenerationStatistics statistics) |
188 | { | 194 | { |
189 | val name = '''addRelation_«declaration.name.canonizeName»«IF inverseRelation != null»_and_«inverseRelation.name.canonizeName»«ENDIF»''' | 195 | val name = '''addRelation_«declaration.name.canonizeName»«IF inverseRelation != null»_and_«inverseRelation.name.canonizeName»«ENDIF»''' |
190 | val ruleBuilder = factory.createRule | 196 | val ruleBuilder = factory.createRule |
@@ -201,7 +207,13 @@ class RefinementRuleProvider { | |||
201 | val trg = match.get(4) as DefinedElement | 207 | val trg = match.get(4) as DefinedElement |
202 | val link = createBinaryElementRelationLink => [it.param1 = src it.param2 = trg] | 208 | val link = createBinaryElementRelationLink => [it.param1 = src it.param2 = trg] |
203 | relationInterpretation.relationlinks += link | 209 | relationInterpretation.relationlinks += link |
204 | statistics.addExecutionTime(System.nanoTime-startTime) | 210 | |
211 | val propagatorStartTime = System.nanoTime | ||
212 | statistics.addExecutionTime(propagatorStartTime-startTime) | ||
213 | |||
214 | // Scope propagation | ||
215 | scopePropagator.propagateAdditionToRelation(declaration) | ||
216 | statistics.addScopePropagationTime(System.nanoTime-propagatorStartTime) | ||
205 | ] | 217 | ] |
206 | } else { | 218 | } else { |
207 | ruleBuilder.action [ match | | 219 | ruleBuilder.action [ match | |
@@ -217,7 +229,13 @@ class RefinementRuleProvider { | |||
217 | relationInterpretation.relationlinks += link | 229 | relationInterpretation.relationlinks += link |
218 | val inverseLink = createBinaryElementRelationLink => [it.param1 = trg it.param2 = src] | 230 | val inverseLink = createBinaryElementRelationLink => [it.param1 = trg it.param2 = src] |
219 | inverseInterpretation.relationlinks += inverseLink | 231 | inverseInterpretation.relationlinks += inverseLink |
220 | statistics.addExecutionTime(System.nanoTime-startTime) | 232 | |
233 | val propagatorStartTime = System.nanoTime | ||
234 | statistics.addExecutionTime(propagatorStartTime-startTime) | ||
235 | |||
236 | // Scope propagation | ||
237 | scopePropagator.propagateAdditionToRelation(declaration) | ||
238 | statistics.addScopePropagationTime(System.nanoTime-propagatorStartTime) | ||
221 | ] | 239 | ] |
222 | } | 240 | } |
223 | 241 | ||