diff options
author | 2019-07-24 10:59:02 +0200 | |
---|---|---|
committer | 2019-07-24 10:59:02 +0200 | |
commit | 64138e8d91bc8d7bb54d9b042f872b43550dec16 (patch) | |
tree | 73c9574a26b83eac91cd0bdb18f2c61b6b212871 /Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra | |
parent | Implement Coin-OR CBC polyhedron saturation operator (diff) | |
download | VIATRA-Generator-64138e8d91bc8d7bb54d9b042f872b43550dec16.tar.gz VIATRA-Generator-64138e8d91bc8d7bb54d9b042f872b43550dec16.tar.zst VIATRA-Generator-64138e8d91bc8d7bb54d9b042f872b43550dec16.zip |
Cardinality propagator WIP
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra')
13 files changed, 828 insertions, 328 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 0ceb5b2e..3a99d3bf 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,7 +5,9 @@ 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.MultiplicityGoalConstraintCalculator | ||
8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronScopePropagator | 9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronScopePropagator |
10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.RelationConstraintCalculator | ||
9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagator | 11 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagator |
10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy | 12 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy |
11 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.GeneratedPatterns | 13 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.GeneratedPatterns |
@@ -61,6 +63,7 @@ class ModelGenerationMethodProvider { | |||
61 | val PatternProvider patternProvider = new PatternProvider | 63 | val PatternProvider patternProvider = new PatternProvider |
62 | val RefinementRuleProvider refinementRuleProvider = new RefinementRuleProvider | 64 | val RefinementRuleProvider refinementRuleProvider = new RefinementRuleProvider |
63 | val GoalConstraintProvider goalConstraintProvider = new GoalConstraintProvider | 65 | val GoalConstraintProvider goalConstraintProvider = new GoalConstraintProvider |
66 | val relationConstraintCalculator = new RelationConstraintCalculator | ||
64 | 67 | ||
65 | def ModelGenerationMethod createModelGenerationMethod( | 68 | def ModelGenerationMethod createModelGenerationMethod( |
66 | LogicProblem logicProblem, | 69 | LogicProblem logicProblem, |
@@ -77,8 +80,9 @@ class ModelGenerationMethodProvider { | |||
77 | val Set<PQuery> existingQueries = logicProblem.relations.map[annotations].flatten.filter(TransfomedViatraQuery). | 80 | val Set<PQuery> existingQueries = logicProblem.relations.map[annotations].flatten.filter(TransfomedViatraQuery). |
78 | map[it.patternPQuery as PQuery].toSet | 81 | map[it.patternPQuery as PQuery].toSet |
79 | 82 | ||
83 | val relationConstraints = relationConstraintCalculator.calculateRelationConstraints(logicProblem) | ||
80 | val queries = patternProvider.generateQueries(logicProblem, emptySolution, statistics, existingQueries, | 84 | val queries = patternProvider.generateQueries(logicProblem, emptySolution, statistics, existingQueries, |
81 | workspace, typeInferenceMethod, writeFiles) | 85 | workspace, typeInferenceMethod, scopePropagatorStrategy, relationConstraints, writeFiles) |
82 | val scopePropagator = createScopePropagator(scopePropagatorStrategy, emptySolution, queries) | 86 | val scopePropagator = createScopePropagator(scopePropagatorStrategy, emptySolution, queries) |
83 | scopePropagator.propagateAllScopeConstraints | 87 | scopePropagator.propagateAllScopeConstraints |
84 | val // LinkedHashMap<Pair<Relation, ? extends Type>, BatchTransformationRule<GenericPatternMatch, ViatraQueryMatcher<GenericPatternMatch>>> | 88 | val // LinkedHashMap<Pair<Relation, ? extends Type>, BatchTransformationRule<GenericPatternMatch, ViatraQueryMatcher<GenericPatternMatch>>> |
@@ -117,10 +121,12 @@ class ModelGenerationMethodProvider { | |||
117 | switch (scopePropagatorStrategy) { | 121 | switch (scopePropagatorStrategy) { |
118 | case BasicTypeHierarchy: | 122 | case BasicTypeHierarchy: |
119 | new ScopePropagator(emptySolution) | 123 | new ScopePropagator(emptySolution) |
120 | case PolyhedralTypeHierarchy: { | 124 | case PolyhedralTypeHierarchy, |
125 | case PolyhedralRelations: { | ||
121 | val types = queries.refineObjectQueries.keySet.map[newType].toSet | 126 | val types = queries.refineObjectQueries.keySet.map[newType].toSet |
122 | val solver = new CbcPolyhedronSolver | 127 | val solver = new CbcPolyhedronSolver |
123 | new PolyhedronScopePropagator(emptySolution, types, solver) | 128 | new PolyhedronScopePropagator(emptySolution, types, queries.multiplicityConstraintQueries, solver, |
129 | scopePropagatorStrategy.requiresUpperBoundIndexing) | ||
124 | } | 130 | } |
125 | default: | 131 | default: |
126 | throw new IllegalArgumentException("Unknown scope propagator strategy: " + scopePropagatorStrategy) | 132 | 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/MultiplicityGoalConstraintCalculator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/MultiplicityGoalConstraintCalculator.xtend index 4b9629df..86a59aa1 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/MultiplicityGoalConstraintCalculator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/MultiplicityGoalConstraintCalculator.xtend | |||
@@ -1,4 +1,4 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra | 1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality |
2 | 2 | ||
3 | import org.eclipse.emf.common.notify.Notifier | 3 | import org.eclipse.emf.common.notify.Notifier |
4 | import org.eclipse.viatra.query.runtime.api.IQuerySpecification | 4 | import org.eclipse.viatra.query.runtime.api.IQuerySpecification |
@@ -37,10 +37,10 @@ class MultiplicityGoalConstraintCalculator { | |||
37 | val allMatches = this.matcher.allMatches | 37 | val allMatches = this.matcher.allMatches |
38 | for(match : allMatches) { | 38 | for(match : allMatches) { |
39 | //println(targetRelationName+ " missing multiplicity: "+match.get(3)) | 39 | //println(targetRelationName+ " missing multiplicity: "+match.get(3)) |
40 | val missingMultiplicity = match.get(4) as Integer | 40 | val missingMultiplicity = match.get(2) as Integer |
41 | res += missingMultiplicity | 41 | res += missingMultiplicity |
42 | } | 42 | } |
43 | //println(targetRelationName+ " all missing multiplicities: "+res) | 43 | //println(targetRelationName+ " all missing multiplicities: "+res) |
44 | return res | 44 | return res |
45 | } | 45 | } |
46 | } \ No newline at end of file | 46 | } |
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 cebd89da..4f0c8f20 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,90 +2,60 @@ 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.Maps | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | 6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type |
7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.UnifinishedMultiplicityQueries | ||
6 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialComplexTypeInterpretation | 8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialComplexTypeInterpretation |
7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | 9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation |
8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialPrimitiveInterpretation | 10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialPrimitiveInterpretation |
9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.Scope | 11 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.Scope |
10 | import java.util.ArrayDeque | 12 | import java.util.ArrayDeque |
13 | import java.util.ArrayList | ||
11 | import java.util.HashMap | 14 | import java.util.HashMap |
12 | import java.util.HashSet | 15 | import java.util.HashSet |
16 | import java.util.List | ||
13 | import java.util.Map | 17 | import java.util.Map |
14 | import java.util.Set | 18 | import java.util.Set |
19 | import javax.naming.OperationNotSupportedException | ||
20 | import org.eclipse.viatra.query.runtime.api.IPatternMatch | ||
21 | import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine | ||
22 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher | ||
23 | import org.eclipse.viatra.query.runtime.emf.EMFScope | ||
24 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor | ||
15 | 25 | ||
16 | class PolyhedronScopePropagator extends ScopePropagator { | 26 | class PolyhedronScopePropagator extends ScopePropagator { |
17 | val Map<Scope, LinearBoundedExpression> scopeBounds | 27 | val Map<Scope, LinearBoundedExpression> scopeBounds |
18 | val LinearConstraint topLevelBounds | 28 | val LinearBoundedExpression topLevelBounds |
29 | val Polyhedron polyhedron | ||
19 | val PolyhedronSaturationOperator operator | 30 | val PolyhedronSaturationOperator operator |
31 | List<RelationConstraintUpdater> updaters = emptyList | ||
20 | 32 | ||
21 | new(PartialInterpretation p, Set<? extends Type> possibleNewDynamicTypes, PolyhedronSolver solver) { | 33 | new(PartialInterpretation p, Set<? extends Type> possibleNewDynamicTypes, |
34 | Map<RelationMultiplicityConstraint, UnifinishedMultiplicityQueries> unfinishedMultiplicityQueries, | ||
35 | PolyhedronSolver solver, boolean propagateRelations) { | ||
22 | super(p) | 36 | super(p) |
23 | val instanceCounts = possibleNewDynamicTypes.toInvertedMap[new Dimension(name, 0, null)] | 37 | val builder = new PolyhedronBuilder(p) |
24 | val primitiveDimensions = new HashMap | 38 | builder.buildPolyhedron(possibleNewDynamicTypes) |
25 | val constraintsBuilder = ImmutableList.builder | 39 | scopeBounds = builder.scopeBounds |
26 | val scopeBoundsBuilder = ImmutableMap.builder | 40 | topLevelBounds = builder.topLevelBounds |
27 | // Dimensions for instantiable types were created according to the type analysis, | 41 | polyhedron = builder.polyhedron |
28 | // but for any possible primitive types, we create them on demand, | ||
29 | // as there is no Type directly associated with a PartialPrimitiveInterpretation. | ||
30 | // Below we will assume that each PartialTypeInterpretation has at most one Scope. | ||
31 | for (scope : p.scopes) { | ||
32 | switch (targetTypeInterpretation : scope.targetTypeInterpretation) { | ||
33 | PartialPrimitiveInterpretation: { | ||
34 | val dimension = primitiveDimensions.computeIfAbsent(targetTypeInterpretation) [ interpretation | | ||
35 | new Dimension(interpretation.eClass.name, 0, null) | ||
36 | ] | ||
37 | scopeBoundsBuilder.put(scope, dimension) | ||
38 | } | ||
39 | PartialComplexTypeInterpretation: { | ||
40 | val complexType = targetTypeInterpretation.interpretationOf | ||
41 | val dimensions = findSubtypeDimensions(complexType, instanceCounts) | ||
42 | switch (dimensions.size) { | ||
43 | case 0: | ||
44 | if (scope.minNewElements > 0) { | ||
45 | throw new IllegalArgumentException("Found scope for " + complexType.name + | ||
46 | ", but the type cannot be instantiated") | ||
47 | } | ||
48 | case 1: | ||
49 | scopeBoundsBuilder.put(scope, dimensions.head) | ||
50 | default: { | ||
51 | val constraint = new LinearConstraint(dimensions.toInvertedMap[1], null, null) | ||
52 | constraintsBuilder.add(constraint) | ||
53 | scopeBoundsBuilder.put(scope, constraint) | ||
54 | } | ||
55 | } | ||
56 | } | ||
57 | default: | ||
58 | throw new IllegalArgumentException("Unknown PartialTypeInterpretation: " + targetTypeInterpretation) | ||
59 | } | ||
60 | } | ||
61 | val allDimensions = ImmutableList.builder.addAll(instanceCounts.values).addAll(primitiveDimensions.values).build | ||
62 | scopeBounds = scopeBoundsBuilder.build | ||
63 | topLevelBounds = new LinearConstraint(allDimensions.toInvertedMap[1], null, null) | ||
64 | constraintsBuilder.add(topLevelBounds) | ||
65 | val expressionsToSaturate = ImmutableList.builder.addAll(scopeBounds.values).add(topLevelBounds).build | ||
66 | val polyhedron = new Polyhedron(allDimensions, constraintsBuilder.build, expressionsToSaturate) | ||
67 | operator = solver.createSaturationOperator(polyhedron) | 42 | operator = solver.createSaturationOperator(polyhedron) |
68 | } | 43 | if (propagateRelations) { |
69 | 44 | propagateAllScopeConstraints() | |
70 | private def findSubtypeDimensions(Type type, Map<Type, Dimension> instanceCounts) { | 45 | val maximumNumberOfNewNodes = topLevelBounds.upperBound |
71 | val subtypes = new HashSet | 46 | if (maximumNumberOfNewNodes === null) { |
72 | val dimensions = new HashSet | 47 | throw new IllegalStateException("Could not determine maximum number of new nodes, it may be unbounded") |
73 | val stack = new ArrayDeque | 48 | } |
74 | stack.addLast(type) | 49 | if (maximumNumberOfNewNodes <= 0) { |
75 | while (!stack.empty) { | 50 | throw new IllegalStateException("Maximum number of new nodes is negative") |
76 | val subtype = stack.removeLast | ||
77 | if (subtypes.add(subtype)) { | ||
78 | val dimension = instanceCounts.get(subtype) | ||
79 | if (dimension !== null) { | ||
80 | dimensions.add(dimension) | ||
81 | } | ||
82 | stack.addAll(subtype.subtypes) | ||
83 | } | 51 | } |
52 | builder.buildMultiplicityConstraints(unfinishedMultiplicityQueries, maximumNumberOfNewNodes) | ||
53 | updaters = builder.updaters | ||
84 | } | 54 | } |
85 | dimensions | ||
86 | } | 55 | } |
87 | 56 | ||
88 | override void propagateAllScopeConstraints() { | 57 | override void propagateAllScopeConstraints() { |
58 | resetBounds() | ||
89 | populatePolyhedronFromScope() | 59 | populatePolyhedronFromScope() |
90 | val result = operator.saturate() | 60 | val result = operator.saturate() |
91 | if (result == PolyhedronSaturationResult.EMPTY) { | 61 | if (result == PolyhedronSaturationResult.EMPTY) { |
@@ -96,21 +66,36 @@ class PolyhedronScopePropagator extends ScopePropagator { | |||
96 | super.propagateAllScopeConstraints() | 66 | super.propagateAllScopeConstraints() |
97 | } | 67 | } |
98 | } | 68 | } |
69 | // println(polyhedron) | ||
70 | } | ||
71 | |||
72 | def resetBounds() { | ||
73 | for (dimension : polyhedron.dimensions) { | ||
74 | dimension.lowerBound = 0 | ||
75 | dimension.upperBound = null | ||
76 | } | ||
77 | for (constraint : polyhedron.constraints) { | ||
78 | constraint.lowerBound = null | ||
79 | constraint.upperBound = null | ||
80 | } | ||
99 | } | 81 | } |
100 | 82 | ||
101 | private def populatePolyhedronFromScope() { | 83 | private def populatePolyhedronFromScope() { |
102 | topLevelBounds.lowerBound = partialInterpretation.minNewElements | 84 | topLevelBounds.tightenLowerBound(partialInterpretation.minNewElements) |
103 | if (partialInterpretation.maxNewElements >= 0) { | 85 | if (partialInterpretation.maxNewElements >= 0) { |
104 | topLevelBounds.upperBound = partialInterpretation.maxNewElements | 86 | topLevelBounds.tightenUpperBound(partialInterpretation.maxNewElements) |
105 | } | 87 | } |
106 | for (pair : scopeBounds.entrySet) { | 88 | for (pair : scopeBounds.entrySet) { |
107 | val scope = pair.key | 89 | val scope = pair.key |
108 | val bounds = pair.value | 90 | val bounds = pair.value |
109 | bounds.lowerBound = scope.minNewElements | 91 | bounds.tightenLowerBound(scope.minNewElements) |
110 | if (scope.maxNewElements >= 0) { | 92 | if (scope.maxNewElements >= 0) { |
111 | bounds.upperBound = scope.maxNewElements | 93 | bounds.tightenUpperBound(scope.maxNewElements) |
112 | } | 94 | } |
113 | } | 95 | } |
96 | for (updater : updaters) { | ||
97 | updater.update(partialInterpretation) | ||
98 | } | ||
114 | } | 99 | } |
115 | 100 | ||
116 | private def populateScopesFromPolyhedron() { | 101 | private def populateScopesFromPolyhedron() { |
@@ -151,4 +136,242 @@ class PolyhedronScopePropagator extends ScopePropagator { | |||
151 | throw new IllegalArgumentException("Infinite upper bound: " + bounds) | 136 | throw new IllegalArgumentException("Infinite upper bound: " + bounds) |
152 | } | 137 | } |
153 | } | 138 | } |
139 | |||
140 | private static def <T extends IPatternMatch> getCalculatedMultiplicity(ViatraQueryMatcher<T> matcher, | ||
141 | PartialInterpretation p) { | ||
142 | val match = matcher.newEmptyMatch | ||
143 | match.set(0, p.problem) | ||
144 | match.set(1, p) | ||
145 | val iterator = matcher.streamAllMatches(match).iterator | ||
146 | if (!iterator.hasNext) { | ||
147 | return null | ||
148 | } | ||
149 | val value = iterator.next.get(2) as Integer | ||
150 | if (iterator.hasNext) { | ||
151 | throw new IllegalArgumentException("Multiplicity calculation query has more than one match") | ||
152 | } | ||
153 | value | ||
154 | } | ||
155 | |||
156 | @FinalFieldsConstructor | ||
157 | private static class PolyhedronBuilder { | ||
158 | static val INFINITY_SCALE = 10 | ||
159 | |||
160 | val PartialInterpretation p | ||
161 | |||
162 | Map<Type, Dimension> instanceCounts | ||
163 | Map<Type, Map<Dimension, Integer>> subtypeDimensions | ||
164 | Map<Map<Dimension, Integer>, LinearBoundedExpression> expressionsCache | ||
165 | Map<Type, LinearBoundedExpression> typeBounds | ||
166 | int infinity | ||
167 | ViatraQueryEngine queryEngine | ||
168 | ImmutableList.Builder<RelationConstraintUpdater> updatersBuilder | ||
169 | |||
170 | Map<Scope, LinearBoundedExpression> scopeBounds | ||
171 | LinearBoundedExpression topLevelBounds | ||
172 | Polyhedron polyhedron | ||
173 | List<RelationConstraintUpdater> updaters | ||
174 | |||
175 | def buildPolyhedron(Set<? extends Type> possibleNewDynamicTypes) { | ||
176 | instanceCounts = possibleNewDynamicTypes.toInvertedMap[new Dimension(name, 0, null)] | ||
177 | val types = p.problem.types | ||
178 | expressionsCache = Maps.newHashMapWithExpectedSize(types.size) | ||
179 | subtypeDimensions = types.toInvertedMap[findSubtypeDimensions.toInvertedMap[1]] | ||
180 | typeBounds = ImmutableMap.copyOf(subtypeDimensions.mapValues[toExpression]) | ||
181 | scopeBounds = buildScopeBounds | ||
182 | topLevelBounds = instanceCounts.values.toInvertedMap[1].toExpression | ||
183 | val dimensions = ImmutableList.copyOf(instanceCounts.values) | ||
184 | val expressionsToSaturate = ImmutableList.copyOf(scopeBounds.values) | ||
185 | polyhedron = new Polyhedron(dimensions, new ArrayList, expressionsToSaturate) | ||
186 | addCachedConstraintsToPolyhedron() | ||
187 | } | ||
188 | |||
189 | def buildMultiplicityConstraints( | ||
190 | Map<RelationMultiplicityConstraint, UnifinishedMultiplicityQueries> constraints, | ||
191 | int maximumNuberOfNewNodes) { | ||
192 | infinity = maximumNuberOfNewNodes * INFINITY_SCALE | ||
193 | queryEngine = ViatraQueryEngine.on(new EMFScope(p)) | ||
194 | updatersBuilder = ImmutableList.builder | ||
195 | for (pair : constraints.entrySet.filter[key.containment].groupBy[key.targetType].entrySet) { | ||
196 | buildContainmentConstraints(pair.key, pair.value) | ||
197 | } | ||
198 | for (pair : constraints.entrySet) { | ||
199 | val constraint = pair.key | ||
200 | if (!constraint.containment) { | ||
201 | buildNonContainmentConstraints(constraint, pair.value) | ||
202 | } | ||
203 | } | ||
204 | updaters = updatersBuilder.build | ||
205 | addCachedConstraintsToPolyhedron() | ||
206 | } | ||
207 | |||
208 | private def addCachedConstraintsToPolyhedron() { | ||
209 | val constraints = new HashSet | ||
210 | constraints.addAll(expressionsCache.values.filter(LinearConstraint)) | ||
211 | constraints.removeAll(polyhedron.constraints) | ||
212 | polyhedron.constraints.addAll(constraints) | ||
213 | } | ||
214 | |||
215 | private def buildContainmentConstraints(Type containedType, | ||
216 | List<Map.Entry<RelationMultiplicityConstraint, UnifinishedMultiplicityQueries>> constraints) { | ||
217 | val typeCoefficients = subtypeDimensions.get(containedType) | ||
218 | val orphansLowerBoundCoefficients = new HashMap(typeCoefficients) | ||
219 | val orphansUpperBoundCoefficients = new HashMap(typeCoefficients) | ||
220 | val unfinishedMultiplicitiesMatchersBuilder = ImmutableList.builder | ||
221 | val remainingContentsQueriesBuilder = ImmutableList.builder | ||
222 | for (pair : constraints) { | ||
223 | val constraint = pair.key | ||
224 | val containerCoefficients = subtypeDimensions.get(constraint.sourceType) | ||
225 | if (constraint.isUpperBoundFinite) { | ||
226 | orphansLowerBoundCoefficients.addCoefficients(-constraint.upperBound, containerCoefficients) | ||
227 | } else { | ||
228 | orphansLowerBoundCoefficients.addCoefficients(-infinity, containerCoefficients) | ||
229 | } | ||
230 | orphansUpperBoundCoefficients.addCoefficients(-constraint.lowerBound, containerCoefficients) | ||
231 | val queries = pair.value | ||
232 | if (constraint.constrainsUnfinished) { | ||
233 | if (queries.unfinishedMultiplicityQuery === null) { | ||
234 | throw new IllegalArgumentException( | ||
235 | "Containment constraints need unfinished multiplicity queries") | ||
236 | } | ||
237 | unfinishedMultiplicitiesMatchersBuilder.add( | ||
238 | queries.unfinishedMultiplicityQuery.getMatcher(queryEngine)) | ||
239 | } | ||
240 | if (queries.remainingContentsQuery === null) { | ||
241 | throw new IllegalArgumentException("Containment constraints need remaining contents queries") | ||
242 | } | ||
243 | remainingContentsQueriesBuilder.add(queries.remainingContentsQuery.getMatcher(queryEngine)) | ||
244 | } | ||
245 | val orphanLowerBound = orphansLowerBoundCoefficients.toExpression | ||
246 | val orphanUpperBound = orphansUpperBoundCoefficients.toExpression | ||
247 | val updater = new ContainmentConstraintUpdater(containedType.name, orphanLowerBound, orphanUpperBound, | ||
248 | unfinishedMultiplicitiesMatchersBuilder.build, remainingContentsQueriesBuilder.build) | ||
249 | updatersBuilder.add(updater) | ||
250 | } | ||
251 | |||
252 | private def buildNonContainmentConstraints(RelationMultiplicityConstraint constraint, | ||
253 | UnifinishedMultiplicityQueries queries) { | ||
254 | } | ||
255 | |||
256 | private def addCoefficients(Map<Dimension, Integer> accumulator, int scale, Map<Dimension, Integer> a) { | ||
257 | for (pair : a.entrySet) { | ||
258 | val dimension = pair.key | ||
259 | val currentValue = accumulator.get(pair.key) ?: 0 | ||
260 | val newValue = currentValue + scale * pair.value | ||
261 | if (newValue == 0) { | ||
262 | accumulator.remove(dimension) | ||
263 | } else { | ||
264 | accumulator.put(dimension, newValue) | ||
265 | } | ||
266 | } | ||
267 | } | ||
268 | |||
269 | private def findSubtypeDimensions(Type type) { | ||
270 | val subtypes = new HashSet | ||
271 | val dimensions = new HashSet | ||
272 | val stack = new ArrayDeque | ||
273 | stack.addLast(type) | ||
274 | while (!stack.empty) { | ||
275 | val subtype = stack.removeLast | ||
276 | if (subtypes.add(subtype)) { | ||
277 | val dimension = instanceCounts.get(subtype) | ||
278 | if (dimension !== null) { | ||
279 | dimensions.add(dimension) | ||
280 | } | ||
281 | stack.addAll(subtype.subtypes) | ||
282 | } | ||
283 | } | ||
284 | dimensions | ||
285 | } | ||
286 | |||
287 | private def toExpression(Map<Dimension, Integer> coefficients) { | ||
288 | expressionsCache.computeIfAbsent(coefficients) [ c | | ||
289 | if (c.size == 1 && c.entrySet.head.value == 1) { | ||
290 | c.entrySet.head.key | ||
291 | } else { | ||
292 | new LinearConstraint(c, null, null) | ||
293 | } | ||
294 | ] | ||
295 | } | ||
296 | |||
297 | private def buildScopeBounds() { | ||
298 | val scopeBoundsBuilder = ImmutableMap.builder | ||
299 | for (scope : p.scopes) { | ||
300 | switch (targetTypeInterpretation : scope.targetTypeInterpretation) { | ||
301 | PartialPrimitiveInterpretation: | ||
302 | throw new OperationNotSupportedException("Primitive type scopes are not yet implemented") | ||
303 | PartialComplexTypeInterpretation: { | ||
304 | val complexType = targetTypeInterpretation.interpretationOf | ||
305 | val typeBound = typeBounds.get(complexType) | ||
306 | if (typeBound === null) { | ||
307 | if (scope.minNewElements > 0) { | ||
308 | throw new IllegalArgumentException("Found scope for " + complexType.name + | ||
309 | ", but the type cannot be instantiated") | ||
310 | } | ||
311 | } else { | ||
312 | scopeBoundsBuilder.put(scope, typeBound) | ||
313 | } | ||
314 | } | ||
315 | default: | ||
316 | throw new IllegalArgumentException("Unknown PartialTypeInterpretation: " + | ||
317 | targetTypeInterpretation) | ||
318 | } | ||
319 | } | ||
320 | scopeBoundsBuilder.build | ||
321 | } | ||
322 | } | ||
323 | |||
324 | private static interface RelationConstraintUpdater { | ||
325 | def void update(PartialInterpretation p) | ||
326 | } | ||
327 | |||
328 | @FinalFieldsConstructor | ||
329 | static class ContainmentConstraintUpdater implements RelationConstraintUpdater { | ||
330 | val String name | ||
331 | val LinearBoundedExpression orphansLowerBound | ||
332 | val LinearBoundedExpression orphansUpperBound | ||
333 | val List<ViatraQueryMatcher<? extends IPatternMatch>> unfinishedMultiplicitiesMatchers | ||
334 | val List<ViatraQueryMatcher<? extends IPatternMatch>> remainingContentsQueries | ||
335 | |||
336 | override update(PartialInterpretation p) { | ||
337 | tightenLowerBound(p) | ||
338 | tightenUpperBound(p) | ||
339 | } | ||
340 | |||
341 | private def tightenLowerBound(PartialInterpretation p) { | ||
342 | var int sum = 0 | ||
343 | for (matcher : remainingContentsQueries) { | ||
344 | val value = matcher.getCalculatedMultiplicity(p) | ||
345 | if (value === null) { | ||
346 | throw new IllegalArgumentException("Remaining contents count is missing for " + name) | ||
347 | } | ||
348 | if (value == -1) { | ||
349 | // Infinite upper bound, no need to tighten. | ||
350 | return | ||
351 | } | ||
352 | sum += value | ||
353 | } | ||
354 | orphansLowerBound.tightenUpperBound(sum) | ||
355 | } | ||
356 | |||
357 | private def tightenUpperBound(PartialInterpretation p) { | ||
358 | var int sum = 0 | ||
359 | for (matcher : unfinishedMultiplicitiesMatchers) { | ||
360 | val value = matcher.getCalculatedMultiplicity(p) | ||
361 | if (value === null) { | ||
362 | throw new IllegalArgumentException("Unfinished multiplicity is missing for " + name) | ||
363 | } | ||
364 | sum += value | ||
365 | } | ||
366 | orphansUpperBound.tightenLowerBound(sum) | ||
367 | } | ||
368 | } | ||
369 | |||
370 | @FinalFieldsConstructor | ||
371 | static class ContainmentRootConstraintUpdater implements RelationConstraintUpdater { | ||
372 | |||
373 | override update(PartialInterpretation p) { | ||
374 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | ||
375 | } | ||
376 | } | ||
154 | } | 377 | } |
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 08bf25b9..9c6cb82e 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 | |||
@@ -52,18 +52,14 @@ class Polyhedron { | |||
52 | val List<LinearBoundedExpression> expressionsToSaturate | 52 | val List<LinearBoundedExpression> expressionsToSaturate |
53 | 53 | ||
54 | override toString() ''' | 54 | override toString() ''' |
55 | Dimensions: | 55 | Dimensions: |
56 | «FOR dimension : dimensions» | 56 | «FOR dimension : dimensions» |
57 | «dimension» | 57 | «dimension» |
58 | «ENDFOR» | 58 | «ENDFOR» |
59 | Constraints: | 59 | Constraints: |
60 | «FOR constraint : constraints» | 60 | «FOR constraint : constraints» |
61 | «constraint» | 61 | «constraint» |
62 | «ENDFOR» | 62 | «ENDFOR» |
63 | ««« Saturate: | ||
64 | ««« «FOR expression : expressionsToSaturate» | ||
65 | ««« «IF expression instanceof Dimension»dimension«ELSEIF expression instanceof LinearConstraint»constraint«ELSE»unknown«ENDIF» «expression» | ||
66 | ««« «ENDFOR» | ||
67 | ''' | 63 | ''' |
68 | 64 | ||
69 | } | 65 | } |
@@ -72,6 +68,18 @@ class Polyhedron { | |||
72 | abstract class LinearBoundedExpression { | 68 | abstract class LinearBoundedExpression { |
73 | var Integer lowerBound | 69 | var Integer lowerBound |
74 | var Integer upperBound | 70 | var Integer upperBound |
71 | |||
72 | def void tightenLowerBound(Integer tighterBound) { | ||
73 | if (lowerBound === null || (tighterBound !== null && lowerBound < tighterBound)) { | ||
74 | lowerBound = tighterBound | ||
75 | } | ||
76 | } | ||
77 | |||
78 | def void tightenUpperBound(Integer tighterBound) { | ||
79 | if (upperBound === null || (tighterBound !== null && upperBound > tighterBound)) { | ||
80 | upperBound = tighterBound | ||
81 | } | ||
82 | } | ||
75 | } | 83 | } |
76 | 84 | ||
77 | @Accessors | 85 | @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 new file mode 100644 index 00000000..ffa9e6e6 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/RelationConstraintCalculator.xtend | |||
@@ -0,0 +1,133 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality | ||
2 | |||
3 | import com.google.common.collect.ImmutableList | ||
4 | import com.google.common.collect.ImmutableSet | ||
5 | import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.InverseRelationAssertion | ||
6 | import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.LowerMultiplicityAssertion | ||
7 | import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.UpperMultiplicityAssertion | ||
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference | ||
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation | ||
10 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | ||
11 | import java.util.HashMap | ||
12 | import java.util.List | ||
13 | import org.eclipse.xtend.lib.annotations.Data | ||
14 | |||
15 | @Data | ||
16 | class RelationConstraints { | ||
17 | val List<RelationMultiplicityConstraint> multiplicityConstraints | ||
18 | } | ||
19 | |||
20 | @Data | ||
21 | class RelationMultiplicityConstraint { | ||
22 | Relation relation | ||
23 | boolean containment | ||
24 | boolean container | ||
25 | int lowerBound | ||
26 | int upperBound | ||
27 | int inverseUpperBound | ||
28 | |||
29 | def isUpperBoundFinite() { | ||
30 | upperBound >= 0 | ||
31 | } | ||
32 | |||
33 | private def isInverseUpperBoundFinite() { | ||
34 | inverseUpperBound >= 0 | ||
35 | } | ||
36 | |||
37 | private def canHaveMultipleSourcesPerTarget() { | ||
38 | inverseUpperBound != 1 | ||
39 | } | ||
40 | |||
41 | def constrainsUnfinished() { | ||
42 | lowerBound >= 1 && (!container || lowerBound >= 2) | ||
43 | } | ||
44 | |||
45 | def constrainsUnrepairable() { | ||
46 | constrainsUnfinished && canHaveMultipleSourcesPerTarget | ||
47 | } | ||
48 | |||
49 | def constrainsRemainingInverse() { | ||
50 | !containment && inverseUpperBoundFinite | ||
51 | } | ||
52 | |||
53 | def constrainsRemainingContents() { | ||
54 | containment | ||
55 | } | ||
56 | |||
57 | def isActive() { | ||
58 | constrainsUnfinished || constrainsUnrepairable || constrainsRemainingInverse || constrainsRemainingContents | ||
59 | } | ||
60 | |||
61 | def getSourceType() { | ||
62 | getParamType(0) | ||
63 | } | ||
64 | |||
65 | def getTargetType() { | ||
66 | getParamType(1) | ||
67 | } | ||
68 | |||
69 | private def getParamType(int i) { | ||
70 | val parameters = relation.parameters | ||
71 | if (i < parameters.size) { | ||
72 | val firstParam = parameters.get(i) | ||
73 | if (firstParam instanceof ComplexTypeReference) { | ||
74 | return firstParam.referred | ||
75 | } | ||
76 | } | ||
77 | throw new IllegalArgumentException("Constraint with unknown source type") | ||
78 | } | ||
79 | } | ||
80 | |||
81 | class RelationConstraintCalculator { | ||
82 | def calculateRelationConstraints(LogicProblem problem) { | ||
83 | val containmentRelations = switch (problem.containmentHierarchies.size) { | ||
84 | case 0: | ||
85 | <Relation>emptySet | ||
86 | case 1: | ||
87 | ImmutableSet.copyOf(problem.containmentHierarchies.head.containmentRelations) | ||
88 | default: | ||
89 | throw new IllegalArgumentException("Only a single containment hierarchy is supported") | ||
90 | } | ||
91 | val inverseRelations = new HashMap<Relation, Relation> | ||
92 | val lowerMultiplicities = new HashMap<Relation, Integer> | ||
93 | val upperMultiplicities = new HashMap<Relation, Integer> | ||
94 | for (relation : problem.relations) { | ||
95 | lowerMultiplicities.put(relation, 0) | ||
96 | upperMultiplicities.put(relation, -1) | ||
97 | } | ||
98 | for (annotation : problem.annotations) { | ||
99 | switch (annotation) { | ||
100 | InverseRelationAssertion: { | ||
101 | inverseRelations.put(annotation.inverseA, annotation.inverseB) | ||
102 | inverseRelations.put(annotation.inverseB, annotation.inverseA) | ||
103 | } | ||
104 | LowerMultiplicityAssertion: | ||
105 | lowerMultiplicities.put(annotation.relation, annotation.lower) | ||
106 | UpperMultiplicityAssertion: | ||
107 | upperMultiplicities.put(annotation.relation, annotation.upper) | ||
108 | } | ||
109 | } | ||
110 | val multiplicityConstraintsBuilder = ImmutableList.builder() | ||
111 | for (relation : problem.relations) { | ||
112 | val containment = containmentRelations.contains(relation) | ||
113 | val lowerMultiplicity = lowerMultiplicities.get(relation) | ||
114 | val upperMultiplicity = upperMultiplicities.get(relation) | ||
115 | var container = false | ||
116 | var inverseUpperMultiplicity = -1 | ||
117 | val inverseRelation = inverseRelations.get(relation) | ||
118 | if (inverseRelation !== null) { | ||
119 | inverseUpperMultiplicity = upperMultiplicities.get(relation) | ||
120 | container = containmentRelations.contains(inverseRelation) | ||
121 | } | ||
122 | val constraint = new RelationMultiplicityConstraint(relation, containment, container, lowerMultiplicity, | ||
123 | upperMultiplicity, inverseUpperMultiplicity) | ||
124 | if (constraint.isActive) { | ||
125 | if (relation.parameters.size != 2) { | ||
126 | throw new IllegalArgumentException('''Relation «relation.name» has multiplicity or containment constraints, but it is not binary''') | ||
127 | } | ||
128 | multiplicityConstraintsBuilder.add(constraint) | ||
129 | } | ||
130 | } | ||
131 | new RelationConstraints(multiplicityConstraintsBuilder.build) | ||
132 | } | ||
133 | } | ||
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 f0494214..3b442cd3 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 | |||
@@ -10,11 +10,6 @@ import java.util.Map | |||
10 | import java.util.Set | 10 | import java.util.Set |
11 | import org.eclipse.xtend.lib.annotations.Accessors | 11 | import org.eclipse.xtend.lib.annotations.Accessors |
12 | 12 | ||
13 | enum ScopePropagatorStrategy { | ||
14 | BasicTypeHierarchy, | ||
15 | PolyhedralTypeHierarchy | ||
16 | } | ||
17 | |||
18 | class ScopePropagator { | 13 | class ScopePropagator { |
19 | @Accessors(PROTECTED_GETTER) PartialInterpretation partialInterpretation | 14 | @Accessors(PROTECTED_GETTER) PartialInterpretation partialInterpretation |
20 | Map<PartialTypeInterpratation, Scope> type2Scope | 15 | Map<PartialTypeInterpratation, Scope> type2Scope |
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 new file mode 100644 index 00000000..b1c5a658 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagatorStrategy.java | |||
@@ -0,0 +1,18 @@ | |||
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/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 24b3e870..1b0db90e 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 | |||
@@ -1,7 +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.ecore2logic.ecore2logicannotations.InverseRelationAssertion | 3 | import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.InverseRelationAssertion |
4 | import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.LowerMultiplicityAssertion | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference | 4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference |
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntTypeReference | 5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntTypeReference |
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference | 6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference |
@@ -17,6 +16,7 @@ import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.Transform | |||
17 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality | 16 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality |
18 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysisResult | 17 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysisResult |
19 | 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.RelationConstraints | ||
20 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | 20 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation |
21 | import java.util.HashMap | 21 | import java.util.HashMap |
22 | import java.util.Map | 22 | import java.util.Map |
@@ -26,22 +26,26 @@ import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery | |||
26 | import org.eclipse.xtend.lib.annotations.Accessors | 26 | import org.eclipse.xtend.lib.annotations.Accessors |
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.ScopePropagatorStrategy | ||
29 | 30 | ||
30 | class PatternGenerator { | 31 | class PatternGenerator { |
31 | @Accessors(PUBLIC_GETTER) val TypeIndexer typeIndexer //= new TypeIndexer(this) | 32 | @Accessors(PUBLIC_GETTER) val TypeIndexer typeIndexer // = new TypeIndexer(this) |
32 | @Accessors(PUBLIC_GETTER) val RelationDeclarationIndexer relationDeclarationIndexer = new RelationDeclarationIndexer(this) | 33 | @Accessors(PUBLIC_GETTER) val RelationDeclarationIndexer relationDeclarationIndexer = new RelationDeclarationIndexer( |
33 | @Accessors(PUBLIC_GETTER) val RelationDefinitionIndexer relationDefinitionIndexer = new RelationDefinitionIndexer(this) | 34 | this) |
35 | @Accessors(PUBLIC_GETTER) val RelationDefinitionIndexer relationDefinitionIndexer = new RelationDefinitionIndexer( | ||
36 | this) | ||
34 | @Accessors(PUBLIC_GETTER) val ContainmentIndexer containmentIndexer = new ContainmentIndexer(this) | 37 | @Accessors(PUBLIC_GETTER) val ContainmentIndexer containmentIndexer = new ContainmentIndexer(this) |
35 | @Accessors(PUBLIC_GETTER) val InvalidIndexer invalidIndexer = new InvalidIndexer(this) | 38 | @Accessors(PUBLIC_GETTER) val InvalidIndexer invalidIndexer = new InvalidIndexer(this) |
36 | @Accessors(PUBLIC_GETTER) val UnfinishedIndexer unfinishedIndexer = new UnfinishedIndexer(this) | 39 | @Accessors(PUBLIC_GETTER) val UnfinishedIndexer unfinishedIndexer |
37 | @Accessors(PUBLIC_GETTER) val TypeRefinementGenerator typeRefinementGenerator //= new RefinementGenerator(this) | 40 | @Accessors(PUBLIC_GETTER) val TypeRefinementGenerator typeRefinementGenerator // = new RefinementGenerator(this) |
38 | @Accessors(PUBLIC_GETTER) val RelationRefinementGenerator relationRefinementGenerator = new RelationRefinementGenerator(this) | 41 | @Accessors(PUBLIC_GETTER) val RelationRefinementGenerator relationRefinementGenerator = new RelationRefinementGenerator( |
39 | 42 | this) | |
40 | public new(TypeInferenceMethod typeInferenceMethod) { | 43 | |
41 | if(typeInferenceMethod == TypeInferenceMethod.Generic) { | 44 | new(TypeInferenceMethod typeInferenceMethod, ScopePropagatorStrategy scopePropagatorStrategy) { |
45 | if (typeInferenceMethod == TypeInferenceMethod.Generic) { | ||
42 | this.typeIndexer = new GenericTypeIndexer(this) | 46 | this.typeIndexer = new GenericTypeIndexer(this) |
43 | this.typeRefinementGenerator = new GenericTypeRefinementGenerator(this) | 47 | this.typeRefinementGenerator = new GenericTypeRefinementGenerator(this) |
44 | } else if(typeInferenceMethod == TypeInferenceMethod.PreliminaryAnalysis) { | 48 | } else if (typeInferenceMethod == TypeInferenceMethod.PreliminaryAnalysis) { |
45 | this.typeIndexer = new TypeIndexerWithPreliminaryTypeAnalysis(this) | 49 | this.typeIndexer = new TypeIndexerWithPreliminaryTypeAnalysis(this) |
46 | this.typeRefinementGenerator = new TypeRefinementWithPreliminaryTypeAnalysis(this) | 50 | this.typeRefinementGenerator = new TypeRefinementWithPreliminaryTypeAnalysis(this) |
47 | } else { | 51 | } else { |
@@ -49,112 +53,100 @@ class PatternGenerator { | |||
49 | this.typeRefinementGenerator = null | 53 | this.typeRefinementGenerator = null |
50 | throw new IllegalArgumentException('''Unknown type indexing technique : «typeInferenceMethod.name»''') | 54 | throw new IllegalArgumentException('''Unknown type indexing technique : «typeInferenceMethod.name»''') |
51 | } | 55 | } |
56 | this.unfinishedIndexer = new UnfinishedIndexer(this, scopePropagatorStrategy.requiresUpperBoundIndexing) | ||
52 | } | 57 | } |
53 | 58 | ||
54 | public def requiresTypeAnalysis() { | 59 | def requiresTypeAnalysis() { |
55 | typeIndexer.requiresTypeAnalysis || typeRefinementGenerator.requiresTypeAnalysis | 60 | typeIndexer.requiresTypeAnalysis || typeRefinementGenerator.requiresTypeAnalysis |
56 | } | 61 | } |
57 | 62 | ||
58 | public dispatch def CharSequence referRelation( | 63 | dispatch def CharSequence referRelation(RelationDeclaration referred, String sourceVariable, String targetVariable, |
59 | RelationDeclaration referred, | 64 | Modality modality, Map<String, PQuery> fqn2PQuery) { |
60 | String sourceVariable, | 65 | return this.relationDeclarationIndexer.referRelation(referred, sourceVariable, targetVariable, modality) |
61 | String targetVariable, | ||
62 | Modality modality, | ||
63 | Map<String,PQuery> fqn2PQuery) | ||
64 | { | ||
65 | return this.relationDeclarationIndexer.referRelation(referred,sourceVariable,targetVariable,modality) | ||
66 | } | 66 | } |
67 | public dispatch def CharSequence referRelation( | 67 | |
68 | RelationDefinition referred, | 68 | dispatch def CharSequence referRelation(RelationDefinition referred, String sourceVariable, String targetVariable, |
69 | String sourceVariable, | 69 | Modality modality, Map<String, PQuery> fqn2PQuery) { |
70 | String targetVariable, | 70 | val pattern = referred.annotations.filter(TransfomedViatraQuery).head.patternFullyQualifiedName.lookup( |
71 | Modality modality, | 71 | fqn2PQuery) |
72 | Map<String,PQuery> fqn2PQuery) | 72 | return this.relationDefinitionIndexer.referPattern(pattern, #[sourceVariable, targetVariable], modality, true, |
73 | { | 73 | false) |
74 | val pattern = referred.annotations.filter(TransfomedViatraQuery).head.patternFullyQualifiedName.lookup(fqn2PQuery) | ||
75 | return this.relationDefinitionIndexer.referPattern(pattern,#[sourceVariable,targetVariable],modality,true,false) | ||
76 | } | 74 | } |
77 | 75 | ||
78 | def public referRelationByName(EReference reference, | 76 | def referRelationByName(EReference reference, String sourceVariable, String targetVariable, Modality modality) { |
79 | String sourceVariable, | 77 | '''find «modality.name.toLowerCase»InRelation«canonizeName('''«reference.name» reference «reference.EContainingClass.name»''')»(problem,interpretation,«sourceVariable»,«targetVariable»);''' |
80 | String targetVariable, | ||
81 | Modality modality) | ||
82 | { | ||
83 | '''find «modality.name.toLowerCase»InRelation«canonizeName('''«reference.name» reference «reference.EContainingClass.name»''') | ||
84 | »(problem,interpretation,«sourceVariable»,«targetVariable»);''' | ||
85 | } | 78 | } |
86 | 79 | ||
87 | def public CharSequence referAttributeByName(EAttribute attribute, | 80 | def CharSequence referAttributeByName(EAttribute attribute, String sourceVariable, String targetVariable, |
88 | String sourceVariable, | 81 | Modality modality) { |
89 | String targetVariable, | 82 | '''find «modality.name.toLowerCase»InRelation«canonizeName('''«attribute.name» attribute «attribute.EContainingClass.name»''')»(problem,interpretation,«sourceVariable»,«targetVariable»);''' |
90 | Modality modality) | ||
91 | { | ||
92 | '''find «modality.name.toLowerCase»InRelation«canonizeName('''«attribute.name» attribute «attribute.EContainingClass.name»''') | ||
93 | »(problem,interpretation,«sourceVariable»,«targetVariable»);''' | ||
94 | } | 83 | } |
95 | 84 | ||
96 | public def canonizeName(String name) { | 85 | def canonizeName(String name) { |
97 | name.split(' ').join('_') | 86 | name.split(' ').join('_') |
98 | } | 87 | } |
99 | 88 | ||
100 | public def lowerMultiplicities(LogicProblem problem) { | 89 | def wfQueries(LogicProblem problem) { |
101 | problem.assertions.map[annotations].flatten.filter(LowerMultiplicityAssertion).filter[!it.relation.isDerived] | 90 | problem.assertions.map[it.annotations].flatten.filter(TransformedViatraWellformednessConstraint).map[it.query] |
102 | } | ||
103 | public def wfQueries(LogicProblem problem) { | ||
104 | problem.assertions.map[it.annotations] | ||
105 | .flatten | ||
106 | .filter(TransformedViatraWellformednessConstraint) | ||
107 | .map[it.query] | ||
108 | } | 91 | } |
109 | public def getContainments(LogicProblem p) { | 92 | |
93 | def getContainments(LogicProblem p) { | ||
110 | return p.containmentHierarchies.head.containmentRelations | 94 | return p.containmentHierarchies.head.containmentRelations |
111 | } | 95 | } |
112 | public def getInverseRelations(LogicProblem p) { | 96 | |
97 | def getInverseRelations(LogicProblem p) { | ||
113 | val inverseRelations = new HashMap | 98 | val inverseRelations = new HashMap |
114 | p.annotations.filter(InverseRelationAssertion).forEach[ | 99 | p.annotations.filter(InverseRelationAssertion).forEach [ |
115 | inverseRelations.put(it.inverseA,it.inverseB) | 100 | inverseRelations.put(it.inverseA, it.inverseB) |
116 | inverseRelations.put(it.inverseB,it.inverseA) | 101 | inverseRelations.put(it.inverseB, it.inverseA) |
117 | ] | 102 | ] |
118 | return inverseRelations | 103 | return inverseRelations |
119 | } | 104 | } |
120 | public def isRepresentative(Relation relation, Relation inverse) { | 105 | |
121 | if(inverse == null) { | 106 | def isRepresentative(Relation relation, Relation inverse) { |
107 | if (inverse === null) { | ||
122 | return true | 108 | return true |
123 | } else { | 109 | } else { |
124 | relation.name.compareTo(inverse.name)<1 | 110 | relation.name.compareTo(inverse.name) < 1 |
125 | } | 111 | } |
126 | } | 112 | } |
127 | 113 | ||
128 | public def isDerived(Relation relation) { | 114 | def isDerived(Relation relation) { |
129 | relation.annotations.exists[it instanceof DefinedByDerivedFeature] | 115 | relation.annotations.exists[it instanceof DefinedByDerivedFeature] |
130 | } | 116 | } |
131 | public def getDerivedDefinition(RelationDeclaration relation) { | 117 | |
118 | def getDerivedDefinition(RelationDeclaration relation) { | ||
132 | relation.annotations.filter(DefinedByDerivedFeature).head.query | 119 | relation.annotations.filter(DefinedByDerivedFeature).head.query |
133 | } | 120 | } |
134 | 121 | ||
135 | private def allTypeReferences(LogicProblem problem) { | 122 | private def allTypeReferences(LogicProblem problem) { |
136 | problem.eAllContents.filter(TypeReference).toIterable | 123 | problem.eAllContents.filter(TypeReference).toIterable |
137 | } | 124 | } |
125 | |||
138 | protected def hasBoolean(LogicProblem problem) { | 126 | protected def hasBoolean(LogicProblem problem) { |
139 | problem.allTypeReferences.exists[it instanceof BoolTypeReference] | 127 | problem.allTypeReferences.exists[it instanceof BoolTypeReference] |
140 | } | 128 | } |
129 | |||
141 | protected def hasInteger(LogicProblem problem) { | 130 | protected def hasInteger(LogicProblem problem) { |
142 | problem.allTypeReferences.exists[it instanceof IntTypeReference] | 131 | problem.allTypeReferences.exists[it instanceof IntTypeReference] |
143 | } | 132 | } |
133 | |||
144 | protected def hasReal(LogicProblem problem) { | 134 | protected def hasReal(LogicProblem problem) { |
145 | problem.allTypeReferences.exists[it instanceof RealTypeReference] | 135 | problem.allTypeReferences.exists[it instanceof RealTypeReference] |
146 | } | 136 | } |
137 | |||
147 | protected def hasString(LogicProblem problem) { | 138 | protected def hasString(LogicProblem problem) { |
148 | problem.allTypeReferences.exists[it instanceof StringTypeReference] | 139 | problem.allTypeReferences.exists[it instanceof StringTypeReference] |
149 | } | 140 | } |
150 | 141 | ||
151 | public def transformBaseProperties( | 142 | def transformBaseProperties( |
152 | LogicProblem problem, | 143 | LogicProblem problem, |
153 | PartialInterpretation emptySolution, | 144 | PartialInterpretation emptySolution, |
154 | Map<String,PQuery> fqn2PQuery, | 145 | Map<String, PQuery> fqn2PQuery, |
155 | TypeAnalysisResult typeAnalysisResult | 146 | TypeAnalysisResult typeAnalysisResult, |
147 | RelationConstraints constraints | ||
156 | ) { | 148 | ) { |
157 | 149 | ||
158 | return ''' | 150 | return ''' |
159 | import epackage "http://www.bme.hu/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage" | 151 | import epackage "http://www.bme.hu/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage" |
160 | import epackage "http://www.bme.hu/mit/inf/dslreasoner/logic/model/problem" | 152 | import epackage "http://www.bme.hu/mit/inf/dslreasoner/logic/model/problem" |
@@ -188,7 +180,7 @@ class PatternGenerator { | |||
188 | 180 | ||
189 | private pattern elementCloseWorld(element:DefinedElement) { | 181 | private pattern elementCloseWorld(element:DefinedElement) { |
190 | PartialInterpretation.openWorldElements(i,element); | 182 | PartialInterpretation.openWorldElements(i,element); |
191 | PartialInterpretation.maxNewElements(i,0); | 183 | PartialInterpretation.maxNewElements(i,0); |
192 | } or { | 184 | } or { |
193 | Scope.targetTypeInterpretation(scope,interpretation); | 185 | Scope.targetTypeInterpretation(scope,interpretation); |
194 | PartialTypeInterpratation.elements(interpretation,element); | 186 | PartialTypeInterpratation.elements(interpretation,element); |
@@ -221,7 +213,7 @@ class PatternGenerator { | |||
221 | ////////// | 213 | ////////// |
222 | // 1.1.1 primitive Type Indexers | 214 | // 1.1.1 primitive Type Indexers |
223 | ////////// | 215 | ////////// |
224 | ««« pattern instanceofBoolean(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) { | 216 | ««« pattern instanceofBoolean(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) { |
225 | ««« find interpretation(problem,interpretation); | 217 | ««« find interpretation(problem,interpretation); |
226 | ««« PartialInterpretation.booleanelements(interpretation,element); | 218 | ««« PartialInterpretation.booleanelements(interpretation,element); |
227 | ««« } | 219 | ««« } |
@@ -279,7 +271,7 @@ class PatternGenerator { | |||
279 | ////////// | 271 | ////////// |
280 | // 3.1 Unfinishedness Measured by Multiplicity | 272 | // 3.1 Unfinishedness Measured by Multiplicity |
281 | ////////// | 273 | ////////// |
282 | «unfinishedIndexer.generateUnfinishedMultiplicityQueries(problem,fqn2PQuery)» | 274 | «unfinishedIndexer.generateUnfinishedMultiplicityQueries(constraints.multiplicityConstraints,fqn2PQuery)» |
283 | 275 | ||
284 | ////////// | 276 | ////////// |
285 | // 3.2 Unfinishedness Measured by WF Queries | 277 | // 3.2 Unfinishedness Measured by WF Queries |
@@ -302,6 +294,6 @@ class PatternGenerator { | |||
302 | // 4.3 Relation refinement | 294 | // 4.3 Relation refinement |
303 | ////////// | 295 | ////////// |
304 | «relationRefinementGenerator.generateRefineReference(problem)» | 296 | «relationRefinementGenerator.generateRefineReference(problem)» |
305 | ''' | 297 | ''' |
306 | } | 298 | } |
307 | } | 299 | } |
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 e87f52af..90f79810 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 | |||
@@ -10,6 +10,8 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationStati | |||
10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysis | 10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysis |
11 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysisResult | 11 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysisResult |
12 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeInferenceMethod | 12 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeInferenceMethod |
13 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.RelationConstraints | ||
14 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.RelationMultiplicityConstraint | ||
13 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.util.ParseUtil | 15 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.util.ParseUtil |
14 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | 16 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation |
15 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace | 17 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace |
@@ -23,78 +25,96 @@ import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery | |||
23 | import org.eclipse.xtend.lib.annotations.Data | 25 | import org.eclipse.xtend.lib.annotations.Data |
24 | 26 | ||
25 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | 27 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* |
28 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy | ||
26 | 29 | ||
27 | @Data class GeneratedPatterns { | 30 | @Data |
28 | public Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidWFQueries | 31 | class GeneratedPatterns { |
29 | public Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWFQueries | 32 | public Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidWFQueries |
30 | public Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedMulticiplicityQueries | 33 | public Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWFQueries |
31 | public Map<ObjectCreationPrecondition, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineObjectQueries | 34 | public Map<RelationMultiplicityConstraint, UnifinishedMultiplicityQueries> multiplicityConstraintQueries |
32 | public Map<? extends Type, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineTypeQueries | 35 | public Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedMulticiplicityQueries |
33 | public Map<Pair<RelationDeclaration, Relation>, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refinerelationQueries | 36 | public Map<ObjectCreationPrecondition, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineObjectQueries |
37 | public Map<? extends Type, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineTypeQueries | ||
38 | public Map<Pair<RelationDeclaration, Relation>, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refinerelationQueries | ||
34 | public Map<RelationDefinition, ModalPatternQueries> modalRelationQueries | 39 | public Map<RelationDefinition, ModalPatternQueries> modalRelationQueries |
35 | public Collection<IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allQueries | 40 | public Collection<IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allQueries |
36 | } | 41 | } |
37 | 42 | ||
38 | @Data class ModalPatternQueries { | 43 | @Data |
44 | class ModalPatternQueries { | ||
39 | val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> mayQuery | 45 | val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> mayQuery |
40 | val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> mustQuery | 46 | val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> mustQuery |
41 | val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> currentQuery | 47 | val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> currentQuery |
42 | } | 48 | } |
43 | 49 | ||
50 | @Data | ||
51 | class UnifinishedMultiplicityQueries { | ||
52 | val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> unfinishedMultiplicityQuery | ||
53 | val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> unrepairableMultiplicityQuery | ||
54 | val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> remainingInverseMultiplicityQuery | ||
55 | val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> remainingContentsQuery | ||
56 | } | ||
57 | |||
44 | class PatternProvider { | 58 | class PatternProvider { |
45 | 59 | ||
46 | val TypeAnalysis typeAnalysis = new TypeAnalysis | 60 | val TypeAnalysis typeAnalysis = new TypeAnalysis |
47 | 61 | ||
48 | public def generateQueries( | 62 | def generateQueries(LogicProblem problem, PartialInterpretation emptySolution, ModelGenerationStatistics statistics, |
49 | LogicProblem problem, | 63 | Set<PQuery> existingQueries, ReasonerWorkspace workspace, TypeInferenceMethod typeInferenceMethod, |
50 | PartialInterpretation emptySolution, | 64 | ScopePropagatorStrategy scopePropagatorStrategy, RelationConstraints relationConstraints, boolean writeToFile) { |
51 | ModelGenerationStatistics statistics, | ||
52 | Set<PQuery> existingQueries, | ||
53 | ReasonerWorkspace workspace, | ||
54 | TypeInferenceMethod typeInferenceMethod, | ||
55 | boolean writeToFile) | ||
56 | { | ||
57 | val fqn2Query = existingQueries.toMap[it.fullyQualifiedName] | 65 | val fqn2Query = existingQueries.toMap[it.fullyQualifiedName] |
58 | val PatternGenerator patternGenerator = new PatternGenerator(typeInferenceMethod) | 66 | val PatternGenerator patternGenerator = new PatternGenerator(typeInferenceMethod, scopePropagatorStrategy) |
59 | val typeAnalysisResult = if(patternGenerator.requiresTypeAnalysis) { | 67 | val typeAnalysisResult = if (patternGenerator.requiresTypeAnalysis) { |
60 | val startTime = System.nanoTime | 68 | val startTime = System.nanoTime |
61 | val result = typeAnalysis.performTypeAnalysis(problem,emptySolution) | 69 | val result = typeAnalysis.performTypeAnalysis(problem, emptySolution) |
62 | val typeAnalysisTime = System.nanoTime - startTime | 70 | val typeAnalysisTime = System.nanoTime - startTime |
63 | statistics.PreliminaryTypeAnalisisTime = typeAnalysisTime | 71 | statistics.PreliminaryTypeAnalisisTime = typeAnalysisTime |
64 | result | 72 | result |
65 | } else { | 73 | } else { |
66 | null | 74 | null |
67 | } | 75 | } |
68 | val baseIndexerFile = patternGenerator.transformBaseProperties(problem,emptySolution,fqn2Query,typeAnalysisResult) | 76 | val baseIndexerFile = patternGenerator.transformBaseProperties(problem, emptySolution, fqn2Query, |
69 | if(writeToFile) { | 77 | typeAnalysisResult, relationConstraints) |
70 | workspace.writeText('''generated3valued.vql_deactivated''',baseIndexerFile) | 78 | if (writeToFile) { |
79 | workspace.writeText('''generated3valued.vql_deactivated''', baseIndexerFile) | ||
71 | } | 80 | } |
72 | val ParseUtil parseUtil = new ParseUtil | 81 | val ParseUtil parseUtil = new ParseUtil |
73 | val generatedQueries = parseUtil.parse(baseIndexerFile) | 82 | val generatedQueries = parseUtil.parse(baseIndexerFile) |
74 | val runtimeQueries = calclulateRuntimeQueries(patternGenerator,problem,emptySolution,typeAnalysisResult,generatedQueries); | 83 | val runtimeQueries = calclulateRuntimeQueries(patternGenerator, problem, emptySolution, typeAnalysisResult, |
84 | relationConstraints, generatedQueries) | ||
75 | return runtimeQueries | 85 | return runtimeQueries |
76 | } | 86 | } |
77 | 87 | ||
78 | private def GeneratedPatterns calclulateRuntimeQueries( | 88 | private def GeneratedPatterns calclulateRuntimeQueries( |
79 | PatternGenerator patternGenerator, | 89 | PatternGenerator patternGenerator, |
80 | LogicProblem problem, | 90 | LogicProblem problem, |
81 | PartialInterpretation emptySolution, | 91 | PartialInterpretation emptySolution, |
82 | TypeAnalysisResult typeAnalysisResult, | 92 | TypeAnalysisResult typeAnalysisResult, |
93 | RelationConstraints relationConstraints, | ||
83 | Map<String, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> queries | 94 | Map<String, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> queries |
84 | ) { | 95 | ) { |
85 | val Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> | 96 | val invalidWFQueries = patternGenerator.invalidIndexer.getInvalidateByWfQueryNames(problem).mapValues [ |
86 | invalidWFQueries = patternGenerator.invalidIndexer.getInvalidateByWfQueryNames(problem).mapValues[it.lookup(queries)] | 97 | it.lookup(queries) |
87 | val Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> | 98 | ] |
88 | unfinishedWFQueries = patternGenerator.unfinishedIndexer.getUnfinishedWFQueryNames(problem).mapValues[it.lookup(queries)] | 99 | val unfinishedWFQueries = patternGenerator.unfinishedIndexer.getUnfinishedWFQueryNames(problem).mapValues [ |
89 | val Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> | 100 | it.lookup(queries) |
90 | unfinishedMultiplicityQueries = patternGenerator.unfinishedIndexer.getUnfinishedMultiplicityQueries(problem).mapValues[it.lookup(queries)] | 101 | ] |
91 | val Map<ObjectCreationPrecondition, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> | 102 | val multiplicityConstraintQueries = patternGenerator.unfinishedIndexer.getUnfinishedMultiplicityQueries( |
92 | refineObjectsQueries = patternGenerator.typeRefinementGenerator.getRefineObjectQueryNames(problem,emptySolution,typeAnalysisResult).mapValues[it.lookup(queries)] | 103 | relationConstraints.multiplicityConstraints).mapValues [ |
93 | val Map<? extends Type, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> | 104 | new UnifinishedMultiplicityQueries(unfinishedMultiplicityQueryName?.lookup(queries), |
94 | refineTypeQueries = patternGenerator.typeRefinementGenerator.getRefineTypeQueryNames(problem,emptySolution,typeAnalysisResult).mapValues[it.lookup(queries)] | 105 | unrepairableMultiplicityQueryName?.lookup(queries), |
95 | val Map<Pair<RelationDeclaration, Relation>, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> | 106 | remainingInverseMultiplicityQueryName?.lookup(queries), remainingContentsQueryName?.lookup(queries)) |
96 | refineRelationQueries = patternGenerator.relationRefinementGenerator.getRefineRelationQueries(problem).mapValues[it.lookup(queries)] | 107 | ] |
97 | val Map<RelationDefinition, ModalPatternQueries> modalRelationQueries = problem.relations.filter(RelationDefinition).toMap([it], [ relationDefinition | | 108 | val unfinishedMultiplicityQueries = multiplicityConstraintQueries.entrySet.filter [ |
109 | value.unfinishedMultiplicityQuery !== null | ||
110 | ].toMap([key.relation], [value.unfinishedMultiplicityQuery]) | ||
111 | val refineObjectsQueries = patternGenerator.typeRefinementGenerator. | ||
112 | getRefineObjectQueryNames(problem, emptySolution, typeAnalysisResult).mapValues[it.lookup(queries)] | ||
113 | val refineTypeQueries = patternGenerator.typeRefinementGenerator.getRefineTypeQueryNames(problem, emptySolution, | ||
114 | typeAnalysisResult).mapValues[it.lookup(queries)] | ||
115 | val refineRelationQueries = patternGenerator.relationRefinementGenerator.getRefineRelationQueries(problem). | ||
116 | mapValues[it.lookup(queries)] | ||
117 | val modalRelationQueries = problem.relations.filter(RelationDefinition).toMap([it], [ relationDefinition | | ||
98 | val indexer = patternGenerator.relationDefinitionIndexer | 118 | val indexer = patternGenerator.relationDefinitionIndexer |
99 | new ModalPatternQueries( | 119 | new ModalPatternQueries( |
100 | indexer.relationDefinitionName(relationDefinition, Modality.MAY).lookup(queries), | 120 | indexer.relationDefinitionName(relationDefinition, Modality.MAY).lookup(queries), |
@@ -105,6 +125,7 @@ class PatternProvider { | |||
105 | return new GeneratedPatterns( | 125 | return new GeneratedPatterns( |
106 | invalidWFQueries, | 126 | invalidWFQueries, |
107 | unfinishedWFQueries, | 127 | unfinishedWFQueries, |
128 | multiplicityConstraintQueries, | ||
108 | unfinishedMultiplicityQueries, | 129 | unfinishedMultiplicityQueries, |
109 | refineObjectsQueries, | 130 | refineObjectsQueries, |
110 | refineTypeQueries, | 131 | refineTypeQueries, |
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 f9e9baea..fa73c861 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 | |||
@@ -9,77 +9,71 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference | |||
9 | 9 | ||
10 | class RelationRefinementGenerator { | 10 | class RelationRefinementGenerator { |
11 | PatternGenerator base; | 11 | PatternGenerator base; |
12 | |||
12 | public new(PatternGenerator base) { | 13 | public new(PatternGenerator base) { |
13 | this.base = base | 14 | this.base = base |
14 | } | 15 | } |
15 | 16 | ||
16 | def CharSequence generateRefineReference(LogicProblem p) { | 17 | def CharSequence generateRefineReference(LogicProblem p) ''' |
17 | return ''' | 18 | «FOR relationRefinement : this.getRelationRefinements(p)» |
18 | «FOR relationRefinement: this.getRelationRefinements(p)» | 19 | pattern «relationRefinementQueryName(relationRefinement.key,relationRefinement.value)»( |
19 | pattern «relationRefinementQueryName(relationRefinement.key,relationRefinement.value)»( | 20 | problem:LogicProblem, interpretation:PartialInterpretation, |
20 | problem:LogicProblem, interpretation:PartialInterpretation, | 21 | relationIterpretation:PartialRelationInterpretation«IF relationRefinement.value !== null», oppositeInterpretation:PartialRelationInterpretation«ENDIF», |
21 | relationIterpretation:PartialRelationInterpretation«IF relationRefinement.value != null», oppositeInterpretation:PartialRelationInterpretation«ENDIF», | 22 | from: DefinedElement, to: DefinedElement) |
22 | from: DefinedElement, to: DefinedElement) | 23 | { |
23 | { | 24 | find interpretation(problem,interpretation); |
24 | find interpretation(problem,interpretation); | 25 | PartialInterpretation.partialrelationinterpretation(interpretation,relationIterpretation); |
25 | PartialInterpretation.partialrelationinterpretation(interpretation,relationIterpretation); | 26 | PartialRelationInterpretation.interpretationOf.name(relationIterpretation,"«relationRefinement.key.name»"); |
26 | PartialRelationInterpretation.interpretationOf.name(relationIterpretation,"«relationRefinement.key.name»"); | 27 | «IF relationRefinement.value !== null» |
27 | «IF relationRefinement.value != null» | 28 | PartialInterpretation.partialrelationinterpretation(interpretation,oppositeInterpretation); |
28 | PartialInterpretation.partialrelationinterpretation(interpretation,oppositeInterpretation); | 29 | PartialRelationInterpretation.interpretationOf.name(oppositeInterpretation,"«relationRefinement.value.name»"); |
29 | PartialRelationInterpretation.interpretationOf.name(oppositeInterpretation,"«relationRefinement.value.name»"); | 30 | «ENDIF» |
30 | «ENDIF» | 31 | find mustExist(problem, interpretation, from); |
31 | find mustExist(problem, interpretation, from); | 32 | find mustExist(problem, interpretation, to); |
32 | find mustExist(problem, interpretation, to); | 33 | «base.typeIndexer.referInstanceOfByReference(relationRefinement.key.parameters.get(0), Modality::MUST,"from")» |
33 | «base.typeIndexer.referInstanceOfByReference(relationRefinement.key.parameters.get(0), Modality::MUST,"from")» | 34 | «base.typeIndexer.referInstanceOfByReference(relationRefinement.key.parameters.get(1), Modality::MUST,"to")» |
34 | «base.typeIndexer.referInstanceOfByReference(relationRefinement.key.parameters.get(1), Modality::MUST,"to")» | 35 | «base.relationDeclarationIndexer.referRelation(relationRefinement.key,"from","to",Modality.MAY)» |
35 | «base.relationDeclarationIndexer.referRelation(relationRefinement.key,"from","to",Modality.MAY)» | 36 | neg «base.relationDeclarationIndexer.referRelation(relationRefinement.key,"from","to",Modality.MUST)» |
36 | neg «base.relationDeclarationIndexer.referRelation(relationRefinement.key,"from","to",Modality.MUST)» | 37 | } |
37 | } | ||
38 | «ENDFOR» | 38 | «ENDFOR» |
39 | ''' | 39 | ''' |
40 | } | 40 | |
41 | |||
42 | def String relationRefinementQueryName(RelationDeclaration relation, Relation inverseRelation) { | 41 | def String relationRefinementQueryName(RelationDeclaration relation, Relation inverseRelation) { |
43 | '''«IF inverseRelation != null | 42 | '''«IF inverseRelation !== null»refineRelation_«base.canonizeName(relation.name)»_and_«base.canonizeName(inverseRelation.name)»«ELSE»refineRelation_«base.canonizeName(relation.name)»«ENDIF»''' |
44 | »refineRelation_«base.canonizeName(relation.name)»_and_«base.canonizeName(inverseRelation.name)»« | ||
45 | ELSE | ||
46 | »refineRelation_«base.canonizeName(relation.name)»«ENDIF»''' | ||
47 | } | 43 | } |
48 | 44 | ||
49 | def referRefinementQuery(RelationDeclaration relation, Relation inverseRelation, String relInterpretationName, | 45 | def referRefinementQuery(RelationDeclaration relation, Relation inverseRelation, String relInterpretationName, |
50 | String inverseInterpretationName, String sourceName, String targetName) | 46 | String inverseInterpretationName, String sourceName, |
51 | '''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»);''' |
52 | 48 | ||
53 | def getRefineRelationQueries(LogicProblem p) { | 49 | def getRefineRelationQueries(LogicProblem p) { |
54 | // val containmentRelations = p.containmentHierarchies.map[containmentRelations].flatten.toSet | 50 | // val containmentRelations = p.containmentHierarchies.map[containmentRelations].flatten.toSet |
55 | // p.relations.filter(RelationDeclaration).filter[!containmentRelations.contains(it)].toInvertedMap['''refineRelation_«base.canonizeName(it.name)»'''] | 51 | // p.relations.filter(RelationDeclaration).filter[!containmentRelations.contains(it)].toInvertedMap['''refineRelation_«base.canonizeName(it.name)»'''] |
56 | /* | 52 | /* |
57 | val res = new LinkedHashMap | 53 | * val res = new LinkedHashMap |
58 | for(relation: getRelationRefinements(p)) { | 54 | * for(relation: getRelationRefinements(p)) { |
59 | if(inverseRelations.containsKey(relation)) { | 55 | * if(inverseRelations.containsKey(relation)) { |
60 | val name = '''refineRelation_«base.canonizeName(relation.name)»_and_«base.canonizeName(inverseRelations.get(relation).name)»''' | 56 | * val name = '''refineRelation_«base.canonizeName(relation.name)»_and_«base.canonizeName(inverseRelations.get(relation).name)»''' |
61 | res.put(relation -> inverseRelations.get(relation),name) | 57 | * res.put(relation -> inverseRelations.get(relation),name) |
62 | } else { | 58 | * } else { |
63 | val name = '''refineRelation_«base.canonizeName(relation.name)»''' | 59 | * val name = '''refineRelation_«base.canonizeName(relation.name)»''' |
64 | res.put(relation -> null,name) | 60 | * res.put(relation -> null,name) |
65 | } | 61 | * } |
66 | } | 62 | * } |
67 | return res*/ | 63 | return res*/ |
68 | 64 | getRelationRefinements(p).toInvertedMap[relationRefinementQueryName(it.key, it.value)] | |
69 | getRelationRefinements(p).toInvertedMap[relationRefinementQueryName(it.key,it.value)] | ||
70 | } | 65 | } |
71 | |||
72 | 66 | ||
73 | def getRelationRefinements(LogicProblem p) { | 67 | def getRelationRefinements(LogicProblem p) { |
74 | val inverses = base.getInverseRelations(p) | 68 | val inverses = base.getInverseRelations(p) |
75 | val containments = base.getContainments(p) | 69 | val containments = base.getContainments(p) |
76 | val list = new LinkedList | 70 | val list = new LinkedList |
77 | for(relation : p.relations.filter(RelationDeclaration)) { | 71 | for (relation : p.relations.filter(RelationDeclaration)) { |
78 | if(!containments.contains(relation)) { | 72 | if (!containments.contains(relation)) { |
79 | if(inverses.containsKey(relation)) { | 73 | if (inverses.containsKey(relation)) { |
80 | val inverse = inverses.get(relation) | 74 | val inverse = inverses.get(relation) |
81 | if(!containments.contains(inverse)) { | 75 | if (!containments.contains(inverse)) { |
82 | if(base.isRepresentative(relation,inverse)) { | 76 | if (base.isRepresentative(relation, inverse)) { |
83 | list += (relation -> inverse) | 77 | list += (relation -> inverse) |
84 | } | 78 | } |
85 | } | 79 | } |
@@ -90,4 +84,4 @@ class RelationRefinementGenerator { | |||
90 | } | 84 | } |
91 | return list | 85 | return list |
92 | } | 86 | } |
93 | } \ No newline at end of file | 87 | } |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeRefinementGenerator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeRefinementGenerator.xtend index 7e3fad91..ee7299cd 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeRefinementGenerator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/TypeRefinementGenerator.xtend | |||
@@ -86,8 +86,8 @@ abstract class TypeRefinementGenerator { | |||
86 | } | 86 | } |
87 | 87 | ||
88 | protected def String patternName(Relation containmentRelation, Relation inverseContainment, Type newType) { | 88 | protected def String patternName(Relation containmentRelation, Relation inverseContainment, Type newType) { |
89 | if(containmentRelation != null) { | 89 | if(containmentRelation !== null) { |
90 | if(inverseContainment != null) { | 90 | if(inverseContainment !== null) { |
91 | '''createObject_«base.canonizeName(newType.name)»_by_«base.canonizeName(containmentRelation.name)»_with_«base.canonizeName(inverseContainment.name)»''' | 91 | '''createObject_«base.canonizeName(newType.name)»_by_«base.canonizeName(containmentRelation.name)»_with_«base.canonizeName(inverseContainment.name)»''' |
92 | } else { | 92 | } else { |
93 | '''createObject_«base.canonizeName(newType.name)»_by_«base.canonizeName(containmentRelation.name)»''' | 93 | '''createObject_«base.canonizeName(newType.name)»_by_«base.canonizeName(containmentRelation.name)»''' |
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 ad1c9033..286756a8 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,85 +1,195 @@ | |||
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.ecore2logic.ecore2logicannotations.LowerMultiplicityAssertion | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | 3 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem |
5 | import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransformedViatraWellformednessConstraint | 4 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality |
5 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.RelationMultiplicityConstraint | ||
6 | import java.util.LinkedHashMap | ||
7 | import java.util.List | ||
6 | import java.util.Map | 8 | import java.util.Map |
7 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery | 9 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery |
10 | import org.eclipse.xtend.lib.annotations.Data | ||
8 | 11 | ||
9 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | 12 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* |
10 | import java.util.LinkedHashMap | 13 | |
11 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality | 14 | @Data |
12 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference | 15 | class UnifinishedMultiplicityQueryNames { |
16 | val String unfinishedMultiplicityQueryName | ||
17 | val String unrepairableMultiplicityQueryName | ||
18 | val String remainingInverseMultiplicityQueryName | ||
19 | val String remainingContentsQueryName | ||
20 | } | ||
13 | 21 | ||
14 | class UnfinishedIndexer { | 22 | class UnfinishedIndexer { |
15 | val PatternGenerator base | 23 | val PatternGenerator base |
16 | 24 | val boolean indexUpperMultiplicities | |
17 | new(PatternGenerator patternGenerator) { | 25 | |
26 | new(PatternGenerator patternGenerator, boolean indexUpperMultiplicities) { | ||
18 | this.base = patternGenerator | 27 | this.base = patternGenerator |
28 | this.indexUpperMultiplicities = indexUpperMultiplicities | ||
19 | } | 29 | } |
20 | 30 | ||
21 | def generateUnfinishedWfQueries(LogicProblem problem, Map<String,PQuery> fqn2PQuery) { | 31 | def generateUnfinishedWfQueries(LogicProblem problem, Map<String, PQuery> fqn2PQuery) { |
22 | val wfQueries = base.wfQueries(problem) | 32 | val wfQueries = base.wfQueries(problem) |
23 | ''' | 33 | ''' |
24 | «FOR wfQuery: wfQueries» | 34 | «FOR wfQuery : wfQueries» |
25 | pattern unfinishedBy_«base.canonizeName(wfQuery.target.name)»(problem:LogicProblem, interpretation:PartialInterpretation, | 35 | pattern unfinishedBy_«base.canonizeName(wfQuery.target.name)»(problem:LogicProblem, interpretation:PartialInterpretation, |
26 | «FOR param : wfQuery.patternFullyQualifiedName.lookup(fqn2PQuery).parameters SEPARATOR ', '»var_«param.name»«ENDFOR») | 36 | «FOR param : wfQuery.patternFullyQualifiedName.lookup(fqn2PQuery).parameters SEPARATOR ', '»var_«param.name»«ENDFOR») |
27 | { | 37 | { |
28 | «base.relationDefinitionIndexer.referPattern( | 38 | «base.relationDefinitionIndexer.referPattern( |
29 | wfQuery.patternFullyQualifiedName.lookup(fqn2PQuery), | 39 | wfQuery.patternFullyQualifiedName.lookup(fqn2PQuery), |
30 | wfQuery.patternFullyQualifiedName.lookup(fqn2PQuery).parameters.map['''var_«it.name»'''], | 40 | wfQuery.patternFullyQualifiedName.lookup(fqn2PQuery).parameters.map['''var_«it.name»'''], |
31 | Modality.CURRENT, | 41 | Modality.CURRENT, |
32 | true,false)» | 42 | true,false)» |
33 | } | 43 | } |
34 | «ENDFOR» | 44 | «ENDFOR» |
35 | ''' | 45 | ''' |
36 | } | 46 | } |
47 | |||
37 | def getUnfinishedWFQueryNames(LogicProblem problem) { | 48 | def getUnfinishedWFQueryNames(LogicProblem problem) { |
38 | val wfQueries = base.wfQueries(problem) | 49 | val wfQueries = base.wfQueries(problem) |
39 | val map = new LinkedHashMap | 50 | val map = new LinkedHashMap |
40 | for(wfQuery : wfQueries) { | 51 | for (wfQuery : wfQueries) { |
41 | map.put(wfQuery.target,'''unfinishedBy_«base.canonizeName(wfQuery.target.name)»''') | 52 | map.put(wfQuery.target, '''unfinishedBy_«base.canonizeName(wfQuery.target.name)»''') |
42 | } | 53 | } |
43 | return map | 54 | return map |
44 | } | 55 | } |
45 | def generateUnfinishedMultiplicityQueries(LogicProblem problem, Map<String,PQuery> fqn2PQuery) { | 56 | |
46 | val lowerMultiplicities = base.lowerMultiplicities(problem) | 57 | def generateUnfinishedMultiplicityQueries(List<RelationMultiplicityConstraint> constraints, |
47 | return ''' | 58 | Map<String, PQuery> fqn2PQuery) ''' |
48 | «FOR lowerMultiplicity : lowerMultiplicities» | 59 | «FOR constraint : constraints» |
49 | pattern «unfinishedMultiplicityName(lowerMultiplicity)»(problem:LogicProblem, interpretation:PartialInterpretation, relationIterpretation:PartialRelationInterpretation, object:DefinedElement,missingMultiplicity) { | 60 | «IF constraint.constrainsUnfinished» |
50 | find interpretation(problem,interpretation); | 61 | private pattern «unfinishedMultiplicityName(constraint)»_helper(problem:LogicProblem, interpretation:PartialInterpretation, object:DefinedElement, missingMultiplicity:java Integer) { |
51 | PartialInterpretation.partialrelationinterpretation(interpretation,relationIterpretation); | 62 | find interpretation(problem,interpretation); |
52 | PartialRelationInterpretation.interpretationOf.name(relationIterpretation,"«lowerMultiplicity.relation.name»"); | 63 | find mustExist(problem,interpretation,object); |
53 | «base.typeIndexer.referInstanceOf(lowerMultiplicity.firstParamTypeOfRelation,Modality::MUST,"object")» | 64 | «base.typeIndexer.referInstanceOf(constraint.sourceType,Modality::MUST,"object")» |
54 | numberOfExistingReferences == count «base.referRelation(lowerMultiplicity.relation,"object","_",Modality.MUST,fqn2PQuery)» | 65 | numberOfExistingReferences == count «base.referRelation(constraint.relation,"object","_",Modality.MUST,fqn2PQuery)» |
55 | check(numberOfExistingReferences < «lowerMultiplicity.lower»); | 66 | check(numberOfExistingReferences < «constraint.lowerBound»); |
56 | missingMultiplicity == eval(«lowerMultiplicity.lower»-numberOfExistingReferences); | 67 | missingMultiplicity == eval(«constraint.lowerBound»-numberOfExistingReferences); |
57 | } | 68 | } |
69 | |||
70 | pattern «unfinishedMultiplicityName(constraint)»(problem:LogicProblem, interpretation:PartialInterpretation, missingMultiplicity:java Integer) { | ||
71 | find interpretation(problem,interpretation); | ||
72 | missingMultiplicity == sum find «unfinishedMultiplicityName(constraint)»_helper(problem, interpretation, _, #_); | ||
73 | } | ||
74 | «ENDIF» | ||
75 | |||
76 | «IF indexUpperMultiplicities» | ||
77 | «IF constraint.constrainsUnrepairable» | ||
78 | private pattern «repairMatchName(constraint)»(problem:LogicProblem, interpretation:PartialInterpretation, source:DefinedElement, target:DefinedElement) { | ||
79 | find interpretation(problem,interpretation); | ||
80 | find mustExist(problem,interpretation,source); | ||
81 | «base.typeIndexer.referInstanceOf(constraint.sourceType,Modality::MUST,"source")» | ||
82 | find mustExist(problem,interpretation,target); | ||
83 | «base.typeIndexer.referInstanceOf(constraint.targetType,Modality::MUST,"target")» | ||
84 | neg «base.referRelation(constraint.relation,"source","target",Modality.MUST,fqn2PQuery)» | ||
85 | «base.referRelation(constraint.relation,"source","target",Modality.MAY,fqn2PQuery)» | ||
86 | } | ||
87 | |||
88 | private pattern «unrepairableMultiplicityName(constraint)»_helper(problem:LogicProblem, interpretation:PartialInterpretation, object:DefinedElement, unrepairableMultiplicity:java Integer) { | ||
89 | find interpretation(problem,interpretation); | ||
90 | find mustExist(problem,interpretation,object); | ||
91 | «base.typeIndexer.referInstanceOf(constraint.sourceType,Modality::MUST,"object")» | ||
92 | find «unfinishedMultiplicityName(constraint)»_helper(problem, interpretation, object, missingMultiplicity); | ||
93 | numerOfRepairMatches == count find «repairMatchName(constraint)»(problem, interpretation, object, _); | ||
94 | check(numerOfRepairMatches < missingMultiplicity); | ||
95 | unrepairableMultiplicity == eval(missingMultiplicity-numerOfRepairMatches); | ||
96 | } | ||
97 | |||
98 | private pattern «unrepairableMultiplicityName(constraint)»(problem:LogicProblem, interpretation:PartialInterpretation, unrepairableMultiplicity:java Integer) { | ||
99 | find interpretation(problem,interpretation); | ||
100 | unrepairableMultiplicity == max find «unrepairableMultiplicityName(constraint)»_helper(problem, interpretation, _, #_); | ||
101 | } or { | ||
102 | find interpretation(problem,interpretation); | ||
103 | neg find «unrepairableMultiplicityName(constraint)»_helper(problem, interpretation, _, _); | ||
104 | unrepairableMultiplicity == 0; | ||
105 | } | ||
106 | «ENDIF» | ||
107 | |||
108 | «IF constraint.constrainsRemainingInverse» | ||
109 | private pattern «remainingMultiplicityName(constraint)»_helper(problem:LogicProblem, interpretation:PartialInterpretation, object:DefinedElement, remainingMultiplicity:java Integer) { | ||
110 | find interpretation(problem,interpretation); | ||
111 | find mustExist(problem,interpretation,object); | ||
112 | «base.typeIndexer.referInstanceOf(constraint.targetType,Modality::MUST,"object")» | ||
113 | numberOfExistingReferences == count «base.referRelation(constraint.relation,"_","object",Modality.MUST,fqn2PQuery)» | ||
114 | check(numberOfExistingReferences < «constraint.inverseUpperBound»); | ||
115 | remainingMultiplicity == eval(«constraint.inverseUpperBound»-numberOfExistingReferences); | ||
116 | } | ||
117 | |||
118 | pattern «remainingMultiplicityName(constraint)»(problem:LogicProblem, interpretation:PartialInterpretation, remainingMultiplicity:java Integer) { | ||
119 | find interpretation(problem,interpretation); | ||
120 | remainingMultiplicity == sum find «remainingMultiplicityName(constraint)»_helper(problem, interpretation, _, #_); | ||
121 | } | ||
122 | «ENDIF» | ||
123 | |||
124 | «IF constraint.constrainsRemainingContents» | ||
125 | «IF constraint.upperBoundFinite» | ||
126 | private pattern «remainingContentsName(constraint)»_helper(problem:LogicProblem, interpretation:PartialInterpretation, object:DefinedElement, remainingMultiplicity:java Integer) { | ||
127 | find interpretation(problem,interpretation); | ||
128 | find mustExist(problem,interpretation,object); | ||
129 | «base.typeIndexer.referInstanceOf(constraint.sourceType,Modality::MUST,"object")» | ||
130 | numberOfExistingReferences == count «base.referRelation(constraint.relation,"object","_",Modality.MUST,fqn2PQuery)» | ||
131 | check(numberOfExistingReferences < «constraint.upperBound»); | ||
132 | remainingMultiplicity == eval(«constraint.upperBound»-numberOfExistingReferences); | ||
133 | } | ||
134 | |||
135 | pattern «remainingContentsName(constraint)»(problem:LogicProblem, interpretation:PartialInterpretation, remainingMultiplicity:java Integer) { | ||
136 | find interpretation(problem,interpretation); | ||
137 | remainingMultiplicity == sum find «remainingContentsName(constraint)»_helper(problem, interpretation, _, #_); | ||
138 | } | ||
139 | «ELSE» | ||
140 | pattern «remainingContentsName(constraint)»_helper(problem:LogicProblem, interpretation:PartialInterpretation) { | ||
141 | find interpretation(problem,interpretation); | ||
142 | find mustExist(problem,interpretation,object); | ||
143 | «base.typeIndexer.referInstanceOf(constraint.sourceType,Modality::MUST,"object")» | ||
144 | } | ||
145 | |||
146 | pattern «remainingContentsName(constraint)»(problem:LogicProblem, interpretation:PartialInterpretation, remainingMultiplicity:java Integer) { | ||
147 | find interpretation(problem,interpretation); | ||
148 | find «remainingContentsName(constraint)»_helper(problem, interpretation); | ||
149 | remainingMultiplicity == -1; | ||
150 | } or { | ||
151 | find interpretation(problem,interpretation); | ||
152 | neg find «remainingContentsName(constraint)»_helper(problem, interpretation); | ||
153 | remainingMultiplicity == 0; | ||
154 | } | ||
155 | «ENDIF» | ||
156 | «ENDIF» | ||
157 | «ENDIF» | ||
58 | «ENDFOR» | 158 | «ENDFOR» |
59 | ''' | 159 | ''' |
60 | } | 160 | |
61 | def String unfinishedMultiplicityName(LowerMultiplicityAssertion lowerMultiplicityAssertion) | 161 | def String unfinishedMultiplicityName( |
62 | '''unfinishedLowerMultiplicity_«base.canonizeName(lowerMultiplicityAssertion.relation.name)»''' | 162 | RelationMultiplicityConstraint constraint) '''unfinishedLowerMultiplicity_«base.canonizeName(constraint.relation.name)»''' |
63 | 163 | ||
64 | def public referUnfinishedMultiplicityQuery(LowerMultiplicityAssertion lowerMultiplicityAssertion) | 164 | def String unrepairableMultiplicityName( |
65 | '''find «unfinishedMultiplicityName(lowerMultiplicityAssertion)»(problem, interpretation ,object, missingMultiplicity);''' | 165 | RelationMultiplicityConstraint constraint) '''unrepairableLowerMultiplicity_«base.canonizeName(constraint.relation.name)»''' |
66 | 166 | ||
67 | def getFirstParamTypeOfRelation(LowerMultiplicityAssertion lowerMultiplicityAssertion) { | 167 | private def String repairMatchName( |
68 | val parameters = lowerMultiplicityAssertion.relation.parameters | 168 | RelationMultiplicityConstraint constraint) '''repair_«base.canonizeName(constraint.relation.name)»''' |
69 | if(parameters.size == 2) { | 169 | |
70 | val firstParam = parameters.get(0) | 170 | def String remainingMultiplicityName( |
71 | if(firstParam instanceof ComplexTypeReference) { | 171 | RelationMultiplicityConstraint constraint) '''remainingInverseUpperMultiplicity_«base.canonizeName(constraint.relation.name)»''' |
72 | return firstParam.referred | 172 | |
73 | } | 173 | def String remainingContentsName( |
74 | } | 174 | RelationMultiplicityConstraint constraint) '''remainingContents_«base.canonizeName(constraint.relation.name)»''' |
75 | } | 175 | |
76 | 176 | def getUnfinishedMultiplicityQueries(List<RelationMultiplicityConstraint> constraints) { | |
77 | def getUnfinishedMultiplicityQueries(LogicProblem problem) { | 177 | constraints.toInvertedMap [ constraint | |
78 | val lowerMultiplicities = base.lowerMultiplicities(problem) | 178 | new UnifinishedMultiplicityQueryNames( |
79 | val map = new LinkedHashMap | 179 | if(constraint.constrainsUnfinished) unfinishedMultiplicityName(constraint) else null, |
80 | for(lowerMultiplicity : lowerMultiplicities) { | 180 | if (indexUpperMultiplicities && constraint.constrainsUnrepairable) |
81 | map.put(lowerMultiplicity.relation,unfinishedMultiplicityName(lowerMultiplicity)) | 181 | unrepairableMultiplicityName(constraint) |
82 | } | 182 | else |
83 | return map | 183 | null, |
184 | if (indexUpperMultiplicities && constraint.constrainsRemainingInverse) | ||
185 | remainingMultiplicityName(constraint) | ||
186 | else | ||
187 | null, | ||
188 | if (indexUpperMultiplicities && constraint.constrainsRemainingContents) | ||
189 | remainingContentsName(constraint) | ||
190 | else | ||
191 | null | ||
192 | ) | ||
193 | ] | ||
84 | } | 194 | } |
85 | } | 195 | } |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend index e1be2742..b6fdbe06 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/GoalConstraintProvider.xtend | |||
@@ -1,6 +1,6 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules | 1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules |
2 | 2 | ||
3 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.MultiplicityGoalConstraintCalculator | 3 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.MultiplicityGoalConstraintCalculator |
4 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.GeneratedPatterns | 4 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.GeneratedPatterns |
5 | import java.util.ArrayList | 5 | import java.util.ArrayList |
6 | 6 | ||