diff options
author | Kristóf Marussy <kris7topher@gmail.com> | 2019-08-14 18:26:33 +0200 |
---|---|---|
committer | Kristóf Marussy <kris7topher@gmail.com> | 2019-08-14 18:26:33 +0200 |
commit | fc84d3fe670331bc89fb1e4c44104bc1fc811438 (patch) | |
tree | 466da8333151c51d2e17075600f9452ed35835da /Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu | |
parent | Be more lenient with rounding IP solver results (diff) | |
download | VIATRA-Generator-fc84d3fe670331bc89fb1e4c44104bc1fc811438.tar.gz VIATRA-Generator-fc84d3fe670331bc89fb1e4c44104bc1fc811438.tar.zst VIATRA-Generator-fc84d3fe670331bc89fb1e4c44104bc1fc811438.zip |
Measurements WIP
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu')
14 files changed, 329 insertions, 74 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 23632d4d..e45ec1c8 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 | |||
@@ -5,6 +5,7 @@ import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel | |||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | 5 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem |
6 | import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransfomedViatraQuery | 6 | import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransfomedViatraQuery |
7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.CbcPolyhedronSolver | 7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.CbcPolyhedronSolver |
8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearTypeConstraintHint | ||
8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.MultiplicityGoalConstraintCalculator | 9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.MultiplicityGoalConstraintCalculator |
9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronScopePropagator | 10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronScopePropagator |
10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.RelationConstraintCalculator | 11 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.RelationConstraintCalculator |
@@ -46,16 +47,28 @@ class ModelGenerationStatistics { | |||
46 | public var long preliminaryTypeAnalisisTime = 0 | 47 | public var long preliminaryTypeAnalisisTime = 0 |
47 | 48 | ||
48 | public var int decisionsTried = 0 | 49 | public var int decisionsTried = 0 |
49 | 50 | ||
50 | synchronized def incrementDecisionCount() { | 51 | synchronized def incrementDecisionCount() { |
51 | decisionsTried++ | 52 | decisionsTried++ |
52 | } | 53 | } |
54 | |||
55 | public var int transformationInvocations | ||
53 | 56 | ||
57 | synchronized def incrementTransformationCount() { | ||
58 | transformationInvocations++ | ||
59 | } | ||
60 | |||
54 | public var int scopePropagatorInvocations | 61 | public var int scopePropagatorInvocations |
55 | 62 | ||
56 | synchronized def incrementScopePropagationCount() { | 63 | synchronized def incrementScopePropagationCount() { |
57 | scopePropagatorInvocations++ | 64 | scopePropagatorInvocations++ |
58 | } | 65 | } |
66 | |||
67 | public var int scopePropagatorSolverInvocations | ||
68 | |||
69 | synchronized def incrementScopePropagationSolverCount() { | ||
70 | scopePropagatorSolverInvocations++ | ||
71 | } | ||
59 | } | 72 | } |
60 | 73 | ||
61 | @Data class ModelGenerationMethod { | 74 | @Data class ModelGenerationMethod { |
@@ -93,6 +106,7 @@ class ModelGenerationMethodProvider { | |||
93 | boolean nameNewElements, | 106 | boolean nameNewElements, |
94 | TypeInferenceMethod typeInferenceMethod, | 107 | TypeInferenceMethod typeInferenceMethod, |
95 | ScopePropagatorStrategy scopePropagatorStrategy, | 108 | ScopePropagatorStrategy scopePropagatorStrategy, |
109 | Collection<LinearTypeConstraintHint> hints, | ||
96 | DocumentationLevel debugLevel | 110 | DocumentationLevel debugLevel |
97 | ) { | 111 | ) { |
98 | val statistics = new ModelGenerationStatistics | 112 | val statistics = new ModelGenerationStatistics |
@@ -103,8 +117,8 @@ class ModelGenerationMethodProvider { | |||
103 | 117 | ||
104 | val relationConstraints = relationConstraintCalculator.calculateRelationConstraints(logicProblem) | 118 | val relationConstraints = relationConstraintCalculator.calculateRelationConstraints(logicProblem) |
105 | val queries = patternProvider.generateQueries(logicProblem, emptySolution, statistics, existingQueries, | 119 | val queries = patternProvider.generateQueries(logicProblem, emptySolution, statistics, existingQueries, |
106 | workspace, typeInferenceMethod, scopePropagatorStrategy, relationConstraints, writeFiles) | 120 | workspace, typeInferenceMethod, scopePropagatorStrategy, relationConstraints, hints, writeFiles) |
107 | val scopePropagator = createScopePropagator(scopePropagatorStrategy, emptySolution, queries, statistics) | 121 | val scopePropagator = createScopePropagator(scopePropagatorStrategy, emptySolution, hints, queries, statistics) |
108 | scopePropagator.propagateAllScopeConstraints | 122 | scopePropagator.propagateAllScopeConstraints |
109 | val objectRefinementRules = refinementRuleProvider.createObjectRefinementRules(queries, scopePropagator, | 123 | val objectRefinementRules = refinementRuleProvider.createObjectRefinementRules(queries, scopePropagator, |
110 | nameNewElements, statistics) | 124 | nameNewElements, statistics) |
@@ -138,14 +152,20 @@ class ModelGenerationMethodProvider { | |||
138 | } | 152 | } |
139 | 153 | ||
140 | private def createScopePropagator(ScopePropagatorStrategy scopePropagatorStrategy, | 154 | private def createScopePropagator(ScopePropagatorStrategy scopePropagatorStrategy, |
141 | PartialInterpretation emptySolution, GeneratedPatterns queries, ModelGenerationStatistics statistics) { | 155 | PartialInterpretation emptySolution, Collection<LinearTypeConstraintHint> hints, GeneratedPatterns queries, |
156 | ModelGenerationStatistics statistics) { | ||
157 | if (!hints.empty && !(scopePropagatorStrategy instanceof ScopePropagatorStrategy.Polyhedral)) { | ||
158 | throw new IllegalArgumentException("Only the Polyhedral scope propagator strategy can use hints.") | ||
159 | } | ||
142 | switch (scopePropagatorStrategy) { | 160 | switch (scopePropagatorStrategy) { |
143 | case ScopePropagatorStrategy.Count: | 161 | case ScopePropagatorStrategy.None, |
162 | case ScopePropagatorStrategy.Basic: | ||
144 | new ScopePropagator(emptySolution, statistics) | 163 | new ScopePropagator(emptySolution, statistics) |
145 | case ScopePropagatorStrategy.BasicTypeHierarchy: | 164 | case ScopePropagatorStrategy.BasicTypeHierarchy: |
146 | new TypeHierarchyScopePropagator(emptySolution, statistics) | 165 | new TypeHierarchyScopePropagator(emptySolution, statistics) |
147 | ScopePropagatorStrategy.Polyhedral: { | 166 | ScopePropagatorStrategy.Polyhedral: { |
148 | val types = queries.refineObjectQueries.keySet.map[newType].toSet | 167 | val types = queries.refineObjectQueries.keySet.map[newType].toSet |
168 | val allPatternsByName = queries.allQueries.toMap[fullyQualifiedName] | ||
149 | val solver = switch (scopePropagatorStrategy.solver) { | 169 | val solver = switch (scopePropagatorStrategy.solver) { |
150 | case Z3Integer: | 170 | case Z3Integer: |
151 | new Z3PolyhedronSolver(false, scopePropagatorStrategy.timeoutSeconds) | 171 | new Z3PolyhedronSolver(false, scopePropagatorStrategy.timeoutSeconds) |
@@ -160,7 +180,8 @@ class ModelGenerationMethodProvider { | |||
160 | scopePropagatorStrategy.solver) | 180 | scopePropagatorStrategy.solver) |
161 | } | 181 | } |
162 | new PolyhedronScopePropagator(emptySolution, statistics, types, queries.multiplicityConstraintQueries, | 182 | new PolyhedronScopePropagator(emptySolution, statistics, types, queries.multiplicityConstraintQueries, |
163 | queries.hasElementInContainmentQuery, solver, scopePropagatorStrategy.requiresUpperBoundIndexing) | 183 | queries.hasElementInContainmentQuery, allPatternsByName, hints, solver, |
184 | scopePropagatorStrategy.requiresUpperBoundIndexing, scopePropagatorStrategy.updateHeuristic) | ||
164 | } | 185 | } |
165 | default: | 186 | default: |
166 | throw new IllegalArgumentException("Unknown scope propagator strategy: " + scopePropagatorStrategy) | 187 | throw new IllegalArgumentException("Unknown scope propagator strategy: " + scopePropagatorStrategy) |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/LinearTypeConstraintHint.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/LinearTypeConstraintHint.xtend new file mode 100644 index 00000000..8c21ca1d --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/LinearTypeConstraintHint.xtend | |||
@@ -0,0 +1,30 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
4 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.PatternGenerator | ||
5 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | ||
6 | import org.eclipse.viatra.query.runtime.api.IPatternMatch | ||
7 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher | ||
8 | |||
9 | interface LinearTypeExpressionBuilderFactory { | ||
10 | def ViatraQueryMatcher<? extends IPatternMatch> createMatcher(String queryName) | ||
11 | |||
12 | def LinearTypeExpressionBuilder createBuilder() | ||
13 | } | ||
14 | |||
15 | interface LinearTypeExpressionBuilder { | ||
16 | def LinearTypeExpressionBuilder add(int scale, Type type) | ||
17 | |||
18 | def LinearBoundedExpression build() | ||
19 | } | ||
20 | |||
21 | @FunctionalInterface | ||
22 | interface RelationConstraintUpdater { | ||
23 | def void update(PartialInterpretation p) | ||
24 | } | ||
25 | |||
26 | interface LinearTypeConstraintHint { | ||
27 | def CharSequence getAdditionalPatterns(PatternGenerator patternGenerator) | ||
28 | |||
29 | def RelationConstraintUpdater createConstraintUpdater(LinearTypeExpressionBuilderFactory builderFactory) | ||
30 | } | ||
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 7c05e818..51dba244 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 | |||
@@ -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 com.google.common.cache.Cache | ||
4 | import com.google.common.cache.CacheBuilder | ||
3 | import com.google.common.collect.ImmutableList | 5 | import com.google.common.collect.ImmutableList |
4 | import com.google.common.collect.ImmutableMap | 6 | import com.google.common.collect.ImmutableMap |
5 | import com.google.common.collect.ImmutableSet | 7 | import com.google.common.collect.ImmutableSet |
@@ -15,6 +17,7 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.par | |||
15 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.Scope | 17 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.Scope |
16 | import java.util.ArrayDeque | 18 | import java.util.ArrayDeque |
17 | import java.util.ArrayList | 19 | import java.util.ArrayList |
20 | import java.util.Collection | ||
18 | import java.util.HashMap | 21 | import java.util.HashMap |
19 | import java.util.HashSet | 22 | import java.util.HashSet |
20 | import java.util.List | 23 | import java.util.List |
@@ -29,26 +32,33 @@ import org.eclipse.viatra.query.runtime.emf.EMFScope | |||
29 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor | 32 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor |
30 | 33 | ||
31 | class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { | 34 | class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { |
35 | static val CACHE_SIZE = 10000 | ||
36 | |||
37 | val boolean updateHeuristic | ||
32 | val Map<Scope, LinearBoundedExpression> scopeBounds | 38 | val Map<Scope, LinearBoundedExpression> scopeBounds |
33 | val LinearBoundedExpression topLevelBounds | 39 | val LinearBoundedExpression topLevelBounds |
34 | val Polyhedron polyhedron | 40 | val Polyhedron polyhedron |
35 | val PolyhedronSaturationOperator operator | 41 | val PolyhedronSaturationOperator operator |
36 | val Set<Relation> relevantRelations | 42 | val Set<Relation> relevantRelations |
43 | val Cache<PolyhedronSignature, PolyhedronSignature> cache = CacheBuilder.newBuilder.maximumSize(CACHE_SIZE).build | ||
37 | List<RelationConstraintUpdater> updaters = emptyList | 44 | List<RelationConstraintUpdater> updaters = emptyList |
38 | 45 | ||
39 | new(PartialInterpretation p, ModelGenerationStatistics statistics, Set<? extends Type> possibleNewDynamicTypes, | 46 | new(PartialInterpretation p, ModelGenerationStatistics statistics, Set<? extends Type> possibleNewDynamicTypes, |
40 | Map<RelationMultiplicityConstraint, UnifinishedMultiplicityQueries> unfinishedMultiplicityQueries, | 47 | Map<RelationMultiplicityConstraint, UnifinishedMultiplicityQueries> unfinishedMultiplicityQueries, |
41 | IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> hasElementInContainmentQuery, | 48 | IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> hasElementInContainmentQuery, |
42 | PolyhedronSolver solver, boolean propagateRelations) { | 49 | Map<String, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allPatternsByName, |
50 | Collection<LinearTypeConstraintHint> hints, PolyhedronSolver solver, boolean propagateRelations, | ||
51 | boolean updateHeuristic) { | ||
43 | super(p, statistics) | 52 | super(p, statistics) |
53 | this.updateHeuristic = updateHeuristic | ||
44 | val builder = new PolyhedronBuilder(p) | 54 | val builder = new PolyhedronBuilder(p) |
45 | builder.buildPolyhedron(possibleNewDynamicTypes) | 55 | builder.buildPolyhedron(possibleNewDynamicTypes) |
46 | scopeBounds = builder.scopeBounds | 56 | scopeBounds = builder.scopeBounds |
47 | topLevelBounds = builder.topLevelBounds | 57 | topLevelBounds = builder.topLevelBounds |
48 | polyhedron = builder.polyhedron | 58 | polyhedron = builder.polyhedron |
49 | operator = solver.createSaturationOperator(polyhedron) | 59 | operator = solver.createSaturationOperator(polyhedron) |
60 | propagateAllScopeConstraints() | ||
50 | if (propagateRelations) { | 61 | if (propagateRelations) { |
51 | propagateAllScopeConstraints() | ||
52 | val maximumNumberOfNewNodes = topLevelBounds.upperBound | 62 | val maximumNumberOfNewNodes = topLevelBounds.upperBound |
53 | if (maximumNumberOfNewNodes === null) { | 63 | if (maximumNumberOfNewNodes === null) { |
54 | throw new IllegalStateException("Could not determine maximum number of new nodes, it may be unbounded") | 64 | throw new IllegalStateException("Could not determine maximum number of new nodes, it may be unbounded") |
@@ -57,7 +67,7 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { | |||
57 | throw new IllegalStateException("Maximum number of new nodes is not positive") | 67 | throw new IllegalStateException("Maximum number of new nodes is not positive") |
58 | } | 68 | } |
59 | builder.buildMultiplicityConstraints(unfinishedMultiplicityQueries, hasElementInContainmentQuery, | 69 | builder.buildMultiplicityConstraints(unfinishedMultiplicityQueries, hasElementInContainmentQuery, |
60 | maximumNumberOfNewNodes) | 70 | allPatternsByName, hints, maximumNumberOfNewNodes) |
61 | relevantRelations = builder.relevantRelations | 71 | relevantRelations = builder.relevantRelations |
62 | updaters = builder.updaters | 72 | updaters = builder.updaters |
63 | } else { | 73 | } else { |
@@ -66,21 +76,40 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { | |||
66 | } | 76 | } |
67 | 77 | ||
68 | override void doPropagateAllScopeConstraints() { | 78 | override void doPropagateAllScopeConstraints() { |
79 | super.doPropagateAllScopeConstraints() | ||
69 | resetBounds() | 80 | resetBounds() |
70 | populatePolyhedronFromScope() | 81 | populatePolyhedronFromScope() |
71 | // println(polyhedron) | 82 | // println(polyhedron) |
72 | val result = operator.saturate() | 83 | val signature = polyhedron.createSignature |
73 | // println(polyhedron) | 84 | val cachedSignature = cache.getIfPresent(signature) |
74 | if (result == PolyhedronSaturationResult.EMPTY) { | 85 | switch (cachedSignature) { |
75 | setScopesInvalid() | 86 | case null: { |
76 | } else { | 87 | statistics.incrementScopePropagationSolverCount |
77 | populateScopesFromPolyhedron() | 88 | val result = operator.saturate() |
78 | if (result != PolyhedronSaturationResult.SATURATED) { | 89 | if (result == PolyhedronSaturationResult.EMPTY) { |
79 | super.propagateAllScopeConstraints() | 90 | cache.put(signature, PolyhedronSignature.EMPTY) |
91 | setScopesInvalid() | ||
92 | } else { | ||
93 | val resultSignature = polyhedron.createSignature | ||
94 | cache.put(signature, resultSignature) | ||
95 | populateScopesFromPolyhedron() | ||
96 | } | ||
80 | } | 97 | } |
98 | case PolyhedronSignature.EMPTY: | ||
99 | setScopesInvalid() | ||
100 | PolyhedronSignature.Bounds: { | ||
101 | polyhedron.applySignature(signature) | ||
102 | populateScopesFromPolyhedron() | ||
103 | } | ||
104 | default: | ||
105 | throw new IllegalStateException("Unknown polyhedron signature: " + signature) | ||
106 | } | ||
107 | // println(polyhedron) | ||
108 | if (updateHeuristic) { | ||
109 | copyScopeBoundsToHeuristic() | ||
81 | } | 110 | } |
82 | } | 111 | } |
83 | 112 | ||
84 | override propagateAdditionToRelation(Relation r) { | 113 | override propagateAdditionToRelation(Relation r) { |
85 | super.propagateAdditionToRelation(r) | 114 | super.propagateAdditionToRelation(r) |
86 | if (relevantRelations.contains(r)) { | 115 | if (relevantRelations.contains(r)) { |
@@ -186,7 +215,7 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { | |||
186 | } | 215 | } |
187 | 216 | ||
188 | @FinalFieldsConstructor | 217 | @FinalFieldsConstructor |
189 | private static class PolyhedronBuilder { | 218 | private static class PolyhedronBuilder implements LinearTypeExpressionBuilderFactory { |
190 | static val INFINITY_SCALE = 10 | 219 | static val INFINITY_SCALE = 10 |
191 | 220 | ||
192 | val PartialInterpretation p | 221 | val PartialInterpretation p |
@@ -197,6 +226,7 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { | |||
197 | Map<Type, LinearBoundedExpression> typeBounds | 226 | Map<Type, LinearBoundedExpression> typeBounds |
198 | int infinity | 227 | int infinity |
199 | ViatraQueryEngine queryEngine | 228 | ViatraQueryEngine queryEngine |
229 | Map<String, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allPatternsByName | ||
200 | ImmutableList.Builder<RelationConstraintUpdater> updatersBuilder | 230 | ImmutableList.Builder<RelationConstraintUpdater> updatersBuilder |
201 | 231 | ||
202 | Map<Scope, LinearBoundedExpression> scopeBounds | 232 | Map<Scope, LinearBoundedExpression> scopeBounds |
@@ -222,9 +252,11 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { | |||
222 | def buildMultiplicityConstraints( | 252 | def buildMultiplicityConstraints( |
223 | Map<RelationMultiplicityConstraint, UnifinishedMultiplicityQueries> constraints, | 253 | Map<RelationMultiplicityConstraint, UnifinishedMultiplicityQueries> constraints, |
224 | IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> hasElementInContainmentQuery, | 254 | IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> hasElementInContainmentQuery, |
225 | int maximumNuberOfNewNodes) { | 255 | Map<String, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allPatternsByName, |
256 | Collection<LinearTypeConstraintHint> hints, int maximumNuberOfNewNodes) { | ||
226 | infinity = maximumNuberOfNewNodes * INFINITY_SCALE | 257 | infinity = maximumNuberOfNewNodes * INFINITY_SCALE |
227 | queryEngine = ViatraQueryEngine.on(new EMFScope(p)) | 258 | queryEngine = ViatraQueryEngine.on(new EMFScope(p)) |
259 | this.allPatternsByName = allPatternsByName | ||
228 | updatersBuilder = ImmutableList.builder | 260 | updatersBuilder = ImmutableList.builder |
229 | val containmentConstraints = constraints.entrySet.filter[key.containment].groupBy[key.targetType] | 261 | val containmentConstraints = constraints.entrySet.filter[key.containment].groupBy[key.targetType] |
230 | for (pair : containmentConstraints.entrySet) { | 262 | for (pair : containmentConstraints.entrySet) { |
@@ -238,10 +270,13 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { | |||
238 | } | 270 | } |
239 | } | 271 | } |
240 | buildRelevantRelations(constraints.keySet) | 272 | buildRelevantRelations(constraints.keySet) |
273 | for (hint : hints) { | ||
274 | updatersBuilder.add(hint.createConstraintUpdater(this)) | ||
275 | } | ||
241 | updaters = updatersBuilder.build | 276 | updaters = updatersBuilder.build |
242 | addCachedConstraintsToPolyhedron() | 277 | addCachedConstraintsToPolyhedron() |
243 | } | 278 | } |
244 | 279 | ||
245 | private def buildRelevantRelations(Set<RelationMultiplicityConstraint> constraints) { | 280 | private def buildRelevantRelations(Set<RelationMultiplicityConstraint> constraints) { |
246 | val builder = ImmutableSet.builder | 281 | val builder = ImmutableSet.builder |
247 | for (constraint : constraints) { | 282 | for (constraint : constraints) { |
@@ -345,7 +380,7 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { | |||
345 | } | 380 | } |
346 | } | 381 | } |
347 | 382 | ||
348 | private def addCoefficients(Map<Dimension, Integer> accumulator, int scale, Map<Dimension, Integer> a) { | 383 | private static def addCoefficients(Map<Dimension, Integer> accumulator, int scale, Map<Dimension, Integer> a) { |
349 | for (pair : a.entrySet) { | 384 | for (pair : a.entrySet) { |
350 | val dimension = pair.key | 385 | val dimension = pair.key |
351 | val currentValue = accumulator.get(pair.key) ?: 0 | 386 | val currentValue = accumulator.get(pair.key) ?: 0 |
@@ -411,14 +446,41 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { | |||
411 | } | 446 | } |
412 | scopeBoundsBuilder.build | 447 | scopeBoundsBuilder.build |
413 | } | 448 | } |
449 | |||
450 | override createMatcher(String queryName) { | ||
451 | val querySpecification = allPatternsByName.get(queryName) | ||
452 | if (querySpecification === null) { | ||
453 | throw new IllegalArgumentException("Unknown pattern: " + queryName) | ||
454 | } | ||
455 | querySpecification.getMatcher(queryEngine) | ||
456 | } | ||
457 | |||
458 | override createBuilder() { | ||
459 | new PolyhedronBuilderLinearTypeExpressionBuilder(this) | ||
460 | } | ||
414 | } | 461 | } |
415 | 462 | ||
416 | private static interface RelationConstraintUpdater { | 463 | @FinalFieldsConstructor |
417 | def void update(PartialInterpretation p) | 464 | private static class PolyhedronBuilderLinearTypeExpressionBuilder implements LinearTypeExpressionBuilder { |
465 | val PolyhedronBuilder polyhedronBuilder | ||
466 | val Map<Dimension, Integer> coefficients = new HashMap | ||
467 | |||
468 | override add(int scale, Type type) { | ||
469 | val typeCoefficients = polyhedronBuilder.subtypeDimensions.get(type) | ||
470 | if (typeCoefficients === null) { | ||
471 | throw new IllegalArgumentException("Unknown type: " + type) | ||
472 | } | ||
473 | PolyhedronBuilder.addCoefficients(coefficients, scale, typeCoefficients) | ||
474 | this | ||
475 | } | ||
476 | |||
477 | override build() { | ||
478 | polyhedronBuilder.toExpression(coefficients) | ||
479 | } | ||
418 | } | 480 | } |
419 | 481 | ||
420 | @FinalFieldsConstructor | 482 | @FinalFieldsConstructor |
421 | static class ContainmentConstraintUpdater implements RelationConstraintUpdater { | 483 | private static class ContainmentConstraintUpdater implements RelationConstraintUpdater { |
422 | val String name | 484 | val String name |
423 | val LinearBoundedExpression orphansLowerBound | 485 | val LinearBoundedExpression orphansLowerBound |
424 | val LinearBoundedExpression orphansUpperBound | 486 | val LinearBoundedExpression orphansUpperBound |
@@ -460,7 +522,7 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { | |||
460 | } | 522 | } |
461 | 523 | ||
462 | @FinalFieldsConstructor | 524 | @FinalFieldsConstructor |
463 | static class ContainmentRootConstraintUpdater implements RelationConstraintUpdater { | 525 | private static class ContainmentRootConstraintUpdater implements RelationConstraintUpdater { |
464 | val LinearBoundedExpression typeCardinality | 526 | val LinearBoundedExpression typeCardinality |
465 | val ViatraQueryMatcher<? extends IPatternMatch> hasElementInContainmentMatcher | 527 | val ViatraQueryMatcher<? extends IPatternMatch> hasElementInContainmentMatcher |
466 | 528 | ||
@@ -479,7 +541,7 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { | |||
479 | } | 541 | } |
480 | 542 | ||
481 | @FinalFieldsConstructor | 543 | @FinalFieldsConstructor |
482 | static class UnfinishedMultiplicityConstraintUpdater implements RelationConstraintUpdater { | 544 | private static class UnfinishedMultiplicityConstraintUpdater implements RelationConstraintUpdater { |
483 | val String name | 545 | val String name |
484 | val LinearBoundedExpression availableMultiplicityExpression | 546 | val LinearBoundedExpression availableMultiplicityExpression |
485 | val ViatraQueryMatcher<? extends IPatternMatch> unfinishedMultiplicityMatcher | 547 | val ViatraQueryMatcher<? extends IPatternMatch> unfinishedMultiplicityMatcher |
@@ -500,7 +562,7 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { | |||
500 | } | 562 | } |
501 | 563 | ||
502 | @FinalFieldsConstructor | 564 | @FinalFieldsConstructor |
503 | static class UnrepairableMultiplicityConstraintUpdater implements RelationConstraintUpdater { | 565 | private static class UnrepairableMultiplicityConstraintUpdater implements RelationConstraintUpdater { |
504 | val String name | 566 | val String name |
505 | val LinearBoundedExpression targetCardinalityExpression | 567 | val LinearBoundedExpression targetCardinalityExpression |
506 | val ViatraQueryMatcher<? extends IPatternMatch> unrepairableMultiplicityMatcher | 568 | val ViatraQueryMatcher<? extends IPatternMatch> unrepairableMultiplicityMatcher |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronSolver.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronSolver.xtend index 9c6cb82e..4e046190 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronSolver.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronSolver.xtend | |||
@@ -3,6 +3,7 @@ package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality | |||
3 | import java.util.List | 3 | import java.util.List |
4 | import java.util.Map | 4 | import java.util.Map |
5 | import org.eclipse.xtend.lib.annotations.Accessors | 5 | import org.eclipse.xtend.lib.annotations.Accessors |
6 | import org.eclipse.xtend.lib.annotations.Data | ||
6 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor | 7 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor |
7 | 8 | ||
8 | interface PolyhedronSolver { | 9 | interface PolyhedronSolver { |
@@ -52,16 +53,66 @@ class Polyhedron { | |||
52 | val List<LinearBoundedExpression> expressionsToSaturate | 53 | val List<LinearBoundedExpression> expressionsToSaturate |
53 | 54 | ||
54 | override toString() ''' | 55 | override toString() ''' |
55 | Dimensions: | 56 | Dimensions: |
56 | «FOR dimension : dimensions» | 57 | «FOR dimension : dimensions» |
57 | «dimension» | 58 | «dimension» |
58 | «ENDFOR» | 59 | «ENDFOR» |
59 | Constraints: | 60 | Constraints: |
60 | «FOR constraint : constraints» | 61 | «FOR constraint : constraints» |
61 | «constraint» | 62 | «constraint» |
62 | «ENDFOR» | 63 | «ENDFOR» |
63 | ''' | 64 | ''' |
64 | 65 | ||
66 | def createSignature() { | ||
67 | val size = dimensions.size + constraints.size | ||
68 | val lowerBounds = newArrayOfSize(size) | ||
69 | val upperBounds = newArrayOfSize(size) | ||
70 | var int i = 0 | ||
71 | for (dimension : dimensions) { | ||
72 | lowerBounds.set(i, dimension.lowerBound) | ||
73 | upperBounds.set(i, dimension.upperBound) | ||
74 | i++ | ||
75 | } | ||
76 | for (constraint : constraints) { | ||
77 | lowerBounds.set(i, constraint.lowerBound) | ||
78 | upperBounds.set(i, constraint.upperBound) | ||
79 | i++ | ||
80 | } | ||
81 | new PolyhedronSignature.Bounds(lowerBounds, upperBounds) | ||
82 | } | ||
83 | |||
84 | def applySignature(PolyhedronSignature.Bounds signature) { | ||
85 | val lowerBounds = signature.lowerBounds | ||
86 | val upperBounds = signature.upperBounds | ||
87 | var int i = 0 | ||
88 | for (dimension : dimensions) { | ||
89 | dimension.lowerBound = lowerBounds.get(i) | ||
90 | dimension.upperBound = upperBounds.get(i) | ||
91 | i++ | ||
92 | } | ||
93 | for (constraint : constraints) { | ||
94 | constraint.lowerBound = lowerBounds.get(i) | ||
95 | constraint.upperBound = upperBounds.get(i) | ||
96 | i++ | ||
97 | } | ||
98 | } | ||
99 | } | ||
100 | |||
101 | abstract class PolyhedronSignature { | ||
102 | public static val EMPTY = new PolyhedronSignature { | ||
103 | override toString() { | ||
104 | "PolyhedronSignature.EMPTY" | ||
105 | } | ||
106 | } | ||
107 | |||
108 | private new() { | ||
109 | } | ||
110 | |||
111 | @Data | ||
112 | static class Bounds extends PolyhedronSignature { | ||
113 | val Integer[] lowerBounds | ||
114 | val Integer[] upperBounds | ||
115 | } | ||
65 | } | 116 | } |
66 | 117 | ||
67 | @Accessors | 118 | @Accessors |
@@ -80,6 +131,11 @@ abstract class LinearBoundedExpression { | |||
80 | upperBound = tighterBound | 131 | upperBound = tighterBound |
81 | } | 132 | } |
82 | } | 133 | } |
134 | |||
135 | def void assertEqualsTo(int bound) { | ||
136 | tightenLowerBound(bound) | ||
137 | tightenUpperBound(bound) | ||
138 | } | ||
83 | } | 139 | } |
84 | 140 | ||
85 | @Accessors | 141 | @Accessors |
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 52a390a8..013e53e1 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 | |||
@@ -117,9 +117,12 @@ class RelationConstraintCalculator { | |||
117 | var inverseUpperMultiplicity = -1 | 117 | var inverseUpperMultiplicity = -1 |
118 | val inverseRelation = inverseRelations.get(relation) | 118 | val inverseRelation = inverseRelations.get(relation) |
119 | if (inverseRelation !== null) { | 119 | if (inverseRelation !== null) { |
120 | inverseUpperMultiplicity = upperMultiplicities.get(relation) | 120 | inverseUpperMultiplicity = upperMultiplicities.get(inverseRelation) |
121 | container = containmentRelations.contains(inverseRelation) | 121 | container = containmentRelations.contains(inverseRelation) |
122 | } | 122 | } |
123 | if (containment) { | ||
124 | inverseUpperMultiplicity = 1 | ||
125 | } | ||
123 | val constraint = new RelationMultiplicityConstraint(relation, inverseRelation, containment, container, | 126 | val constraint = new RelationMultiplicityConstraint(relation, inverseRelation, containment, container, |
124 | lowerMultiplicity, upperMultiplicity, inverseUpperMultiplicity) | 127 | lowerMultiplicity, upperMultiplicity, inverseUpperMultiplicity) |
125 | if (constraint.isActive) { | 128 | if (constraint.isActive) { |
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 0bdb202e..2376fb38 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 | |||
@@ -14,7 +14,7 @@ import org.eclipse.xtend.lib.annotations.Accessors | |||
14 | 14 | ||
15 | class ScopePropagator { | 15 | class ScopePropagator { |
16 | @Accessors(PROTECTED_GETTER) val PartialInterpretation partialInterpretation | 16 | @Accessors(PROTECTED_GETTER) val PartialInterpretation partialInterpretation |
17 | val ModelGenerationStatistics statistics | 17 | @Accessors(PROTECTED_GETTER) val ModelGenerationStatistics statistics |
18 | val Map<PartialTypeInterpratation, Scope> type2Scope | 18 | val Map<PartialTypeInterpratation, Scope> type2Scope |
19 | @Accessors(PROTECTED_GETTER) val Map<Scope, Set<Scope>> superScopes | 19 | @Accessors(PROTECTED_GETTER) val Map<Scope, Set<Scope>> superScopes |
20 | @Accessors(PROTECTED_GETTER) val Map<Scope, Set<Scope>> subScopes | 20 | @Accessors(PROTECTED_GETTER) val Map<Scope, Set<Scope>> subScopes |
@@ -59,12 +59,21 @@ class ScopePropagator { | |||
59 | } | 59 | } |
60 | } | 60 | } |
61 | } while (changed) | 61 | } while (changed) |
62 | |||
63 | copyScopeBoundsToHeuristic() | ||
62 | } | 64 | } |
63 | 65 | ||
64 | def propagateAllScopeConstraints() { | 66 | def propagateAllScopeConstraints() { |
65 | statistics.incrementScopePropagationCount() | 67 | statistics.incrementScopePropagationCount() |
66 | doPropagateAllScopeConstraints() | 68 | doPropagateAllScopeConstraints() |
67 | } | 69 | } |
70 | |||
71 | protected def copyScopeBoundsToHeuristic() { | ||
72 | partialInterpretation.minNewElementsHeuristic = partialInterpretation.minNewElements | ||
73 | for (scope : partialInterpretation.scopes) { | ||
74 | scope.minNewElementsHeuristic = scope.minNewElements | ||
75 | } | ||
76 | } | ||
68 | 77 | ||
69 | protected def void doPropagateAllScopeConstraints() { | 78 | protected def void doPropagateAllScopeConstraints() { |
70 | // Nothing to propagate. | 79 | // Nothing to propagate. |
@@ -73,12 +82,17 @@ class ScopePropagator { | |||
73 | def propagateAdditionToType(PartialTypeInterpratation t) { | 82 | def propagateAdditionToType(PartialTypeInterpratation t) { |
74 | // println('''Adding to «(t as PartialComplexTypeInterpretation).interpretationOf.name»''') | 83 | // println('''Adding to «(t as PartialComplexTypeInterpretation).interpretationOf.name»''') |
75 | val targetScope = type2Scope.get(t) | 84 | val targetScope = type2Scope.get(t) |
76 | targetScope.removeOne | 85 | if (targetScope !== null) { |
77 | val sups = superScopes.get(targetScope) | 86 | targetScope.removeOne |
78 | sups.forEach[removeOne] | 87 | val sups = superScopes.get(targetScope) |
88 | sups.forEach[removeOne] | ||
89 | } | ||
79 | if (this.partialInterpretation.minNewElements > 0) { | 90 | if (this.partialInterpretation.minNewElements > 0) { |
80 | this.partialInterpretation.minNewElements = this.partialInterpretation.minNewElements - 1 | 91 | this.partialInterpretation.minNewElements = this.partialInterpretation.minNewElements - 1 |
81 | } | 92 | } |
93 | if (this.partialInterpretation.minNewElementsHeuristic > 0) { | ||
94 | this.partialInterpretation.minNewElementsHeuristic = this.partialInterpretation.minNewElementsHeuristic - 1 | ||
95 | } | ||
82 | if (this.partialInterpretation.maxNewElements > 0) { | 96 | if (this.partialInterpretation.maxNewElements > 0) { |
83 | this.partialInterpretation.maxNewElements = this.partialInterpretation.maxNewElements - 1 | 97 | this.partialInterpretation.maxNewElements = this.partialInterpretation.maxNewElements - 1 |
84 | } else if (this.partialInterpretation.maxNewElements === 0) { | 98 | } else if (this.partialInterpretation.maxNewElements === 0) { |
@@ -105,5 +119,8 @@ class ScopePropagator { | |||
105 | if (scope.minNewElements > 0) { | 119 | if (scope.minNewElements > 0) { |
106 | scope.minNewElements = scope.minNewElements - 1 | 120 | scope.minNewElements = scope.minNewElements - 1 |
107 | } | 121 | } |
122 | if (scope.minNewElementsHeuristic > 0) { | ||
123 | scope.minNewElementsHeuristic = scope.minNewElementsHeuristic - 1 | ||
124 | } | ||
108 | } | 125 | } |
109 | } | 126 | } |
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 index b0ed75cb..3165917a 100644 --- 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 | |||
@@ -16,7 +16,9 @@ enum PolyhedralScopePropagatorSolver { | |||
16 | } | 16 | } |
17 | 17 | ||
18 | abstract class ScopePropagatorStrategy { | 18 | abstract class ScopePropagatorStrategy { |
19 | public static val Count = new Simple("Count") | 19 | public static val None = new Simple("None") |
20 | |||
21 | public static val Basic = new Simple("Basic") | ||
20 | 22 | ||
21 | public static val BasicTypeHierarchy = new Simple("BasicTypeHierarchy") | 23 | public static val BasicTypeHierarchy = new Simple("BasicTypeHierarchy") |
22 | 24 | ||
@@ -47,14 +49,19 @@ abstract class ScopePropagatorStrategy { | |||
47 | 49 | ||
48 | val PolyhedralScopePropagatorConstraints constraints | 50 | val PolyhedralScopePropagatorConstraints constraints |
49 | val PolyhedralScopePropagatorSolver solver | 51 | val PolyhedralScopePropagatorSolver solver |
52 | val boolean updateHeuristic | ||
50 | val double timeoutSeconds | 53 | val double timeoutSeconds |
51 | 54 | ||
52 | @FinalFieldsConstructor | 55 | @FinalFieldsConstructor |
53 | new() { | 56 | new() { |
54 | } | 57 | } |
55 | 58 | ||
59 | new(PolyhedralScopePropagatorConstraints constraints, PolyhedralScopePropagatorSolver solver, boolean updateHeuristic) { | ||
60 | this(constraints, solver, updateHeuristic, UNLIMITED_TIME) | ||
61 | } | ||
62 | |||
56 | new(PolyhedralScopePropagatorConstraints constraints, PolyhedralScopePropagatorSolver solver) { | 63 | new(PolyhedralScopePropagatorConstraints constraints, PolyhedralScopePropagatorSolver solver) { |
57 | this(constraints, solver, UNLIMITED_TIME) | 64 | this(constraints, solver, true) |
58 | } | 65 | } |
59 | 66 | ||
60 | override requiresUpperBoundIndexing() { | 67 | override requiresUpperBoundIndexing() { |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/TypeHierarchyScopePropagator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/TypeHierarchyScopePropagator.xtend index be8ef00a..d1704b39 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/TypeHierarchyScopePropagator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/TypeHierarchyScopePropagator.xtend | |||
@@ -27,12 +27,16 @@ class TypeHierarchyScopePropagator extends ScopePropagator { | |||
27 | } | 27 | } |
28 | 28 | ||
29 | private def propagateLowerLimitUp(Scope subScope, Scope superScope) { | 29 | private def propagateLowerLimitUp(Scope subScope, Scope superScope) { |
30 | var changed = false | ||
30 | if (subScope.minNewElements > superScope.minNewElements) { | 31 | if (subScope.minNewElements > superScope.minNewElements) { |
31 | superScope.minNewElements = subScope.minNewElements | 32 | superScope.minNewElements = subScope.minNewElements |
32 | return true | 33 | changed = true |
33 | } else { | 34 | } |
34 | return false | 35 | if (subScope.minNewElementsHeuristic > superScope.minNewElementsHeuristic) { |
36 | superScope.minNewElementsHeuristic = subScope.minNewElementsHeuristic | ||
37 | changed = true | ||
35 | } | 38 | } |
39 | changed | ||
36 | } | 40 | } |
37 | 41 | ||
38 | private def propagateUpperLimitDown(Scope subScope, Scope superScope) { | 42 | private def propagateUpperLimitDown(Scope subScope, Scope superScope) { |
@@ -50,16 +54,20 @@ class TypeHierarchyScopePropagator extends ScopePropagator { | |||
50 | } | 54 | } |
51 | 55 | ||
52 | private def propagateLowerLimitUp(Scope subScope, PartialInterpretation p) { | 56 | private def propagateLowerLimitUp(Scope subScope, PartialInterpretation p) { |
57 | var changed = false | ||
53 | if (subScope.minNewElements > p.minNewElements) { | 58 | if (subScope.minNewElements > p.minNewElements) { |
54 | // println(''' | 59 | // println(''' |
55 | // «(subScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» -> nodes | 60 | // «(subScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» -> nodes |
56 | // p.minNewElements «p.minNewElements» = subScope.minNewElements «subScope.minNewElements» | 61 | // p.minNewElements «p.minNewElements» = subScope.minNewElements «subScope.minNewElements» |
57 | // ''') | 62 | // ''') |
58 | p.minNewElements = subScope.minNewElements | 63 | p.minNewElements = subScope.minNewElements |
59 | return true | 64 | changed = true |
60 | } else { | 65 | } |
61 | return false | 66 | if (subScope.minNewElementsHeuristic > p.minNewElementsHeuristic) { |
67 | p.minNewElementsHeuristic = subScope.minNewElementsHeuristic | ||
68 | changed = true | ||
62 | } | 69 | } |
70 | changed | ||
63 | } | 71 | } |
64 | 72 | ||
65 | private def propagateUpperLimitDown(Scope subScope, PartialInterpretation p) { | 73 | private def propagateUpperLimitDown(Scope subScope, PartialInterpretation p) { |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/Z3PolyhedronSolver.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/Z3PolyhedronSolver.xtend index 23444956..3b831433 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/Z3PolyhedronSolver.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/Z3PolyhedronSolver.xtend | |||
@@ -13,6 +13,7 @@ import java.math.BigDecimal | |||
13 | import java.math.MathContext | 13 | import java.math.MathContext |
14 | import java.math.RoundingMode | 14 | import java.math.RoundingMode |
15 | import java.util.Map | 15 | import java.util.Map |
16 | import org.eclipse.xtend.lib.annotations.Accessors | ||
16 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor | 17 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor |
17 | 18 | ||
18 | class Z3PolyhedronSolver implements PolyhedronSolver { | 19 | class Z3PolyhedronSolver implements PolyhedronSolver { |
@@ -28,10 +29,33 @@ class Z3PolyhedronSolver implements PolyhedronSolver { | |||
28 | } | 29 | } |
29 | 30 | ||
30 | override createSaturationOperator(Polyhedron polyhedron) { | 31 | override createSaturationOperator(Polyhedron polyhedron) { |
32 | new DisposingZ3SaturationOperator(this, polyhedron) | ||
33 | } | ||
34 | |||
35 | def createPersistentSaturationOperator(Polyhedron polyhedron) { | ||
31 | new Z3SaturationOperator(polyhedron, lpRelaxation, timeoutSeconds) | 36 | new Z3SaturationOperator(polyhedron, lpRelaxation, timeoutSeconds) |
32 | } | 37 | } |
33 | } | 38 | } |
34 | 39 | ||
40 | @FinalFieldsConstructor | ||
41 | class DisposingZ3SaturationOperator implements PolyhedronSaturationOperator { | ||
42 | val Z3PolyhedronSolver solver | ||
43 | @Accessors val Polyhedron polyhedron | ||
44 | |||
45 | override saturate() { | ||
46 | val persistentOperator = solver.createPersistentSaturationOperator(polyhedron) | ||
47 | try { | ||
48 | persistentOperator.saturate | ||
49 | } finally { | ||
50 | persistentOperator.close | ||
51 | } | ||
52 | } | ||
53 | |||
54 | override close() throws Exception { | ||
55 | // Nothing to close. | ||
56 | } | ||
57 | } | ||
58 | |||
35 | class Z3SaturationOperator extends AbstractPolyhedronSaturationOperator { | 59 | class Z3SaturationOperator extends AbstractPolyhedronSaturationOperator { |
36 | static val INFINITY_SYMBOL_NAME = "oo" | 60 | static val INFINITY_SYMBOL_NAME = "oo" |
37 | static val MULT_SYMBOL_NAME = "*" | 61 | static val MULT_SYMBOL_NAME = "*" |
@@ -106,9 +130,9 @@ class Z3SaturationOperator extends AbstractPolyhedronSaturationOperator { | |||
106 | IntNum: | 130 | IntNum: |
107 | resultExpr.getInt() | 131 | resultExpr.getInt() |
108 | RatNum: | 132 | RatNum: |
109 | floor(resultExpr) | 133 | ceil(resultExpr) |
110 | AlgebraicNum: | 134 | AlgebraicNum: |
111 | floor(resultExpr.toLower(ALGEBRAIC_NUMBER_ROUNDING)) | 135 | ceil(resultExpr.toUpper(ALGEBRAIC_NUMBER_ROUNDING)) |
112 | default: | 136 | default: |
113 | if (isNegativeInfinity(resultExpr)) { | 137 | if (isNegativeInfinity(resultExpr)) { |
114 | null | 138 | null |
@@ -136,9 +160,9 @@ class Z3SaturationOperator extends AbstractPolyhedronSaturationOperator { | |||
136 | IntNum: | 160 | IntNum: |
137 | resultExpr.getInt() | 161 | resultExpr.getInt() |
138 | RatNum: | 162 | RatNum: |
139 | ceil(resultExpr) | 163 | floor(resultExpr) |
140 | AlgebraicNum: | 164 | AlgebraicNum: |
141 | ceil(resultExpr.toUpper(ALGEBRAIC_NUMBER_ROUNDING)) | 165 | floor(resultExpr.toLower(ALGEBRAIC_NUMBER_ROUNDING)) |
142 | default: | 166 | default: |
143 | if (isPositiveInfinity(resultExpr)) { | 167 | if (isPositiveInfinity(resultExpr)) { |
144 | null | 168 | null |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend index 1b0db90e..5c35fb54 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend | |||
@@ -16,8 +16,11 @@ import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.Transform | |||
16 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality | 16 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality |
17 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysisResult | 17 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysisResult |
18 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeInferenceMethod | 18 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeInferenceMethod |
19 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearTypeConstraintHint | ||
19 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.RelationConstraints | 20 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.RelationConstraints |
21 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy | ||
20 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | 22 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation |
23 | import java.util.Collection | ||
21 | import java.util.HashMap | 24 | import java.util.HashMap |
22 | import java.util.Map | 25 | import java.util.Map |
23 | import org.eclipse.emf.ecore.EAttribute | 26 | import org.eclipse.emf.ecore.EAttribute |
@@ -26,7 +29,6 @@ import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery | |||
26 | import org.eclipse.xtend.lib.annotations.Accessors | 29 | import org.eclipse.xtend.lib.annotations.Accessors |
27 | 30 | ||
28 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | 31 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* |
29 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy | ||
30 | 32 | ||
31 | class PatternGenerator { | 33 | class PatternGenerator { |
32 | @Accessors(PUBLIC_GETTER) val TypeIndexer typeIndexer // = new TypeIndexer(this) | 34 | @Accessors(PUBLIC_GETTER) val TypeIndexer typeIndexer // = new TypeIndexer(this) |
@@ -104,7 +106,9 @@ class PatternGenerator { | |||
104 | } | 106 | } |
105 | 107 | ||
106 | def isRepresentative(Relation relation, Relation inverse) { | 108 | def isRepresentative(Relation relation, Relation inverse) { |
107 | if (inverse === null) { | 109 | if (relation === null) { |
110 | return false | ||
111 | } else if (inverse === null) { | ||
108 | return true | 112 | return true |
109 | } else { | 113 | } else { |
110 | relation.name.compareTo(inverse.name) < 1 | 114 | relation.name.compareTo(inverse.name) < 1 |
@@ -144,7 +148,8 @@ class PatternGenerator { | |||
144 | PartialInterpretation emptySolution, | 148 | PartialInterpretation emptySolution, |
145 | Map<String, PQuery> fqn2PQuery, | 149 | Map<String, PQuery> fqn2PQuery, |
146 | TypeAnalysisResult typeAnalysisResult, | 150 | TypeAnalysisResult typeAnalysisResult, |
147 | RelationConstraints constraints | 151 | RelationConstraints constraints, |
152 | Collection<LinearTypeConstraintHint> hints | ||
148 | ) { | 153 | ) { |
149 | 154 | ||
150 | return ''' | 155 | return ''' |
@@ -294,6 +299,13 @@ class PatternGenerator { | |||
294 | // 4.3 Relation refinement | 299 | // 4.3 Relation refinement |
295 | ////////// | 300 | ////////// |
296 | «relationRefinementGenerator.generateRefineReference(problem)» | 301 | «relationRefinementGenerator.generateRefineReference(problem)» |
302 | |||
303 | ////////// | ||
304 | // 5 Hints | ||
305 | ////////// | ||
306 | «FOR hint : hints» | ||
307 | «hint.getAdditionalPatterns(this)» | ||
308 | «ENDFOR» | ||
297 | ''' | 309 | ''' |
298 | } | 310 | } |
299 | } | 311 | } |
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 eadf0ae0..f5c85524 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 | |||
@@ -26,6 +26,7 @@ import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery | |||
26 | import org.eclipse.xtend.lib.annotations.Data | 26 | import org.eclipse.xtend.lib.annotations.Data |
27 | 27 | ||
28 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | 28 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* |
29 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearTypeConstraintHint | ||
29 | 30 | ||
30 | @Data | 31 | @Data |
31 | class GeneratedPatterns { | 32 | class GeneratedPatterns { |
@@ -62,7 +63,8 @@ class PatternProvider { | |||
62 | 63 | ||
63 | def generateQueries(LogicProblem problem, PartialInterpretation emptySolution, ModelGenerationStatistics statistics, | 64 | def generateQueries(LogicProblem problem, PartialInterpretation emptySolution, ModelGenerationStatistics statistics, |
64 | Set<PQuery> existingQueries, ReasonerWorkspace workspace, TypeInferenceMethod typeInferenceMethod, | 65 | Set<PQuery> existingQueries, ReasonerWorkspace workspace, TypeInferenceMethod typeInferenceMethod, |
65 | ScopePropagatorStrategy scopePropagatorStrategy, RelationConstraints relationConstraints, boolean writeToFile) { | 66 | ScopePropagatorStrategy scopePropagatorStrategy, RelationConstraints relationConstraints, |
67 | Collection<LinearTypeConstraintHint> hints, boolean writeToFile) { | ||
66 | val fqn2Query = existingQueries.toMap[it.fullyQualifiedName] | 68 | val fqn2Query = existingQueries.toMap[it.fullyQualifiedName] |
67 | val PatternGenerator patternGenerator = new PatternGenerator(typeInferenceMethod, scopePropagatorStrategy) | 69 | val PatternGenerator patternGenerator = new PatternGenerator(typeInferenceMethod, scopePropagatorStrategy) |
68 | val typeAnalysisResult = if (patternGenerator.requiresTypeAnalysis) { | 70 | val typeAnalysisResult = if (patternGenerator.requiresTypeAnalysis) { |
@@ -75,7 +77,7 @@ class PatternProvider { | |||
75 | null | 77 | null |
76 | } | 78 | } |
77 | val baseIndexerFile = patternGenerator.transformBaseProperties(problem, emptySolution, fqn2Query, | 79 | val baseIndexerFile = patternGenerator.transformBaseProperties(problem, emptySolution, fqn2Query, |
78 | typeAnalysisResult, relationConstraints) | 80 | typeAnalysisResult, relationConstraints, hints) |
79 | if (writeToFile) { | 81 | if (writeToFile) { |
80 | workspace.writeText('''generated3valued.vql_deactivated''', baseIndexerFile) | 82 | workspace.writeText('''generated3valued.vql_deactivated''', baseIndexerFile) |
81 | } | 83 | } |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationRefinementGenerator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationRefinementGenerator.xtend index fa73c861..d915d47e 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationRefinementGenerator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationRefinementGenerator.xtend | |||
@@ -44,7 +44,7 @@ class RelationRefinementGenerator { | |||
44 | 44 | ||
45 | def referRefinementQuery(RelationDeclaration relation, Relation inverseRelation, String relInterpretationName, | 45 | def referRefinementQuery(RelationDeclaration relation, Relation inverseRelation, String relInterpretationName, |
46 | String inverseInterpretationName, String sourceName, | 46 | String inverseInterpretationName, String sourceName, |
47 | String targetName) '''find «this.relationRefinementQueryName(relation,inverseRelation)»(problem, interpretation, «relInterpretationName», «IF inverseRelation !== null»inverseInterpretationName, «ENDIF»«sourceName», «targetName»);''' | 47 | String targetName) '''find «this.relationRefinementQueryName(relation,inverseRelation)»(problem, interpretation, «relInterpretationName», «IF inverseRelation !== null»«inverseInterpretationName», «ENDIF»«sourceName», «targetName»);''' |
48 | 48 | ||
49 | def getRefineRelationQueries(LogicProblem p) { | 49 | def getRefineRelationQueries(LogicProblem p) { |
50 | // val containmentRelations = p.containmentHierarchies.map[containmentRelations].flatten.toSet | 50 | // val containmentRelations = p.containmentHierarchies.map[containmentRelations].flatten.toSet |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnfinishedIndexer.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnfinishedIndexer.xtend index 15b5a047..a8a07756 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnfinishedIndexer.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/UnfinishedIndexer.xtend | |||
@@ -1,5 +1,6 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns | 1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns |
2 | 2 | ||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration | ||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | 4 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem |
4 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality | 5 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality |
5 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.RelationMultiplicityConstraint | 6 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.RelationMultiplicityConstraint |
@@ -76,21 +77,26 @@ class UnfinishedIndexer { | |||
76 | «IF indexUpperMultiplicities» | 77 | «IF indexUpperMultiplicities» |
77 | «IF constraint.constrainsUnrepairable || constraint.constrainsRemainingInverse» | 78 | «IF constraint.constrainsUnrepairable || constraint.constrainsRemainingInverse» |
78 | private pattern «repairMatchName(constraint)»(problem:LogicProblem, interpretation:PartialInterpretation, source:DefinedElement, target:DefinedElement) { | 79 | private pattern «repairMatchName(constraint)»(problem:LogicProblem, interpretation:PartialInterpretation, source:DefinedElement, target:DefinedElement) { |
79 | find interpretation(problem,interpretation); | 80 | «IF base.isRepresentative(constraint.relation, constraint.inverseRelation) && constraint.relation instanceof RelationDeclaration» |
80 | find mustExist(problem,interpretation,source); | 81 | «base.relationRefinementGenerator.referRefinementQuery(constraint.relation as RelationDeclaration, constraint.inverseRelation, "_", "_", "source", "target")» |
81 | «base.typeIndexer.referInstanceOf(constraint.sourceType,Modality::MUST,"source")» | 82 | «ELSE» |
82 | find mustExist(problem,interpretation,target); | 83 | «IF base.isRepresentative(constraint.inverseRelation, constraint.relation) && constraint.inverseRelation instanceof RelationDeclaration» |
83 | «base.typeIndexer.referInstanceOf(constraint.targetType,Modality::MUST,"target")» | 84 | «base.relationRefinementGenerator.referRefinementQuery(constraint.inverseRelation as RelationDeclaration, constraint.relation, "_", "_", "target", "source")» |
84 | neg «base.referRelation(constraint.relation,"source","target",Modality.MUST,fqn2PQuery)» | 85 | «ELSE» |
85 | «base.referRelation(constraint.relation,"source","target",Modality.MAY,fqn2PQuery)» | 86 | find interpretation(problem,interpretation); |
87 | find mustExist(problem,interpretation,source); | ||
88 | «base.typeIndexer.referInstanceOf(constraint.sourceType,Modality::MUST,"source")» | ||
89 | find mustExist(problem,interpretation,target); | ||
90 | «base.typeIndexer.referInstanceOf(constraint.targetType,Modality::MUST,"target")» | ||
91 | neg «base.referRelation(constraint.relation,"source","target",Modality.MUST,fqn2PQuery)» | ||
92 | «base.referRelation(constraint.relation,"source","target",Modality.MAY,fqn2PQuery)» | ||
93 | «ENDIF» | ||
94 | «ENDIF» | ||
86 | } | 95 | } |
87 | «ENDIF» | 96 | «ENDIF» |
88 | 97 | ||
89 | «IF constraint.constrainsUnrepairable» | 98 | «IF constraint.constrainsUnrepairable» |
90 | private pattern «unrepairableMultiplicityName(constraint)»_helper(problem:LogicProblem, interpretation:PartialInterpretation, object:DefinedElement, unrepairableMultiplicity:java Integer) { | 99 | private pattern «unrepairableMultiplicityName(constraint)»_helper(problem:LogicProblem, interpretation:PartialInterpretation, object:DefinedElement, unrepairableMultiplicity:java Integer) { |
91 | find interpretation(problem,interpretation); | ||
92 | find mustExist(problem,interpretation,object); | ||
93 | «base.typeIndexer.referInstanceOf(constraint.sourceType,Modality::MUST,"object")» | ||
94 | find «unfinishedMultiplicityName(constraint)»_helper(problem, interpretation, object, missingMultiplicity); | 100 | find «unfinishedMultiplicityName(constraint)»_helper(problem, interpretation, object, missingMultiplicity); |
95 | numberOfRepairMatches == count find «repairMatchName(constraint)»(problem, interpretation, object, _); | 101 | numberOfRepairMatches == count find «repairMatchName(constraint)»(problem, interpretation, object, _); |
96 | check(numberOfRepairMatches < missingMultiplicity); | 102 | check(numberOfRepairMatches < missingMultiplicity); |
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 bf816de9..7891ebd8 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 | |||
@@ -67,7 +67,8 @@ class RefinementRuleProvider { | |||
67 | if(containmentRelation != null) { | 67 | if(containmentRelation != null) { |
68 | if(inverseRelation!= null) { | 68 | if(inverseRelation!= null) { |
69 | ruleBuilder.action[match | | 69 | ruleBuilder.action[match | |
70 | //println(name) | 70 | statistics.incrementTransformationCount |
71 | // println(name) | ||
71 | val startTime = System.nanoTime | 72 | val startTime = System.nanoTime |
72 | //val problem = match.get(0) as LogicProblem | 73 | //val problem = match.get(0) as LogicProblem |
73 | val interpretation = match.get(1) as PartialInterpretation | 74 | val interpretation = match.get(1) as PartialInterpretation |
@@ -107,7 +108,8 @@ class RefinementRuleProvider { | |||
107 | ] | 108 | ] |
108 | } else { | 109 | } else { |
109 | ruleBuilder.action[match | | 110 | ruleBuilder.action[match | |
110 | //println(name) | 111 | statistics.incrementTransformationCount |
112 | // println(name) | ||
111 | val startTime = System.nanoTime | 113 | val startTime = System.nanoTime |
112 | //val problem = match.get(0) as LogicProblem | 114 | //val problem = match.get(0) as LogicProblem |
113 | val interpretation = match.get(1) as PartialInterpretation | 115 | val interpretation = match.get(1) as PartialInterpretation |
@@ -144,6 +146,9 @@ class RefinementRuleProvider { | |||
144 | } | 146 | } |
145 | } else { | 147 | } else { |
146 | ruleBuilder.action[match | | 148 | ruleBuilder.action[match | |
149 | statistics.incrementTransformationCount | ||
150 | // println(name) | ||
151 | |||
147 | val startTime = System.nanoTime | 152 | val startTime = System.nanoTime |
148 | //val problem = match.get(0) as LogicProblem | 153 | //val problem = match.get(0) as LogicProblem |
149 | val interpretation = match.get(1) as PartialInterpretation | 154 | val interpretation = match.get(1) as PartialInterpretation |
@@ -198,8 +203,9 @@ class RefinementRuleProvider { | |||
198 | .precondition(lhs) | 203 | .precondition(lhs) |
199 | if (inverseRelation == null) { | 204 | if (inverseRelation == null) { |
200 | ruleBuilder.action [ match | | 205 | ruleBuilder.action [ match | |
206 | statistics.incrementTransformationCount | ||
201 | val startTime = System.nanoTime | 207 | val startTime = System.nanoTime |
202 | //println(name) | 208 | // println(name) |
203 | // val problem = match.get(0) as LogicProblem | 209 | // val problem = match.get(0) as LogicProblem |
204 | // val interpretation = match.get(1) as PartialInterpretation | 210 | // val interpretation = match.get(1) as PartialInterpretation |
205 | val relationInterpretation = match.get(2) as PartialRelationInterpretation | 211 | val relationInterpretation = match.get(2) as PartialRelationInterpretation |
@@ -217,8 +223,9 @@ class RefinementRuleProvider { | |||
217 | ] | 223 | ] |
218 | } else { | 224 | } else { |
219 | ruleBuilder.action [ match | | 225 | ruleBuilder.action [ match | |
226 | statistics.incrementTransformationCount | ||
220 | val startTime = System.nanoTime | 227 | val startTime = System.nanoTime |
221 | //println(name) | 228 | // println(name) |
222 | // val problem = match.get(0) as LogicProblem | 229 | // val problem = match.get(0) as LogicProblem |
223 | // val interpretation = match.get(1) as PartialInterpretation | 230 | // val interpretation = match.get(1) as PartialInterpretation |
224 | val relationInterpretation = match.get(2) as PartialRelationInterpretation | 231 | val relationInterpretation = match.get(2) as PartialRelationInterpretation |