diff options
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver')
16 files changed, 923 insertions, 523 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 deleted file mode 100644 index 56beacfa..00000000 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend +++ /dev/null | |||
@@ -1,215 +0,0 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra | ||
2 | |||
3 | import com.google.common.collect.ImmutableMap | ||
4 | import com.google.common.collect.ImmutableSet | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | ||
7 | import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransfomedViatraQuery | ||
8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.CbcPolyhedronSolver | ||
9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearTypeConstraintHint | ||
10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.MultiplicityGoalConstraintCalculator | ||
11 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronScopePropagator | ||
12 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.RelationConstraintCalculator | ||
13 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagator | ||
14 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy | ||
15 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.TypeHierarchyScopePropagator | ||
16 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Z3PolyhedronSolver | ||
17 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.GeneratedPatterns | ||
18 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.ModalPatternQueries | ||
19 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.PatternProvider | ||
20 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules.GoalConstraintProvider | ||
21 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules.RefinementRuleProvider | ||
22 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | ||
23 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace | ||
24 | import java.util.Collection | ||
25 | import java.util.List | ||
26 | import java.util.Map | ||
27 | import java.util.Set | ||
28 | import org.eclipse.viatra.query.runtime.api.GenericQueryGroup | ||
29 | import org.eclipse.viatra.query.runtime.api.IPatternMatch | ||
30 | import org.eclipse.viatra.query.runtime.api.IQuerySpecification | ||
31 | import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine | ||
32 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher | ||
33 | import org.eclipse.viatra.query.runtime.emf.EMFScope | ||
34 | import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint | ||
35 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery | ||
36 | import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRule | ||
37 | import org.eclipse.xtend.lib.annotations.Data | ||
38 | |||
39 | class ModelGenerationStatistics { | ||
40 | public var long transformationExecutionTime = 0 | ||
41 | |||
42 | synchronized def addExecutionTime(long amount) { | ||
43 | transformationExecutionTime += amount | ||
44 | } | ||
45 | |||
46 | public var long scopePropagationTime = 0 | ||
47 | |||
48 | synchronized def addScopePropagationTime(long amount) { | ||
49 | scopePropagationTime += amount | ||
50 | } | ||
51 | |||
52 | public var long preliminaryTypeAnalisisTime = 0 | ||
53 | |||
54 | public var int decisionsTried = 0 | ||
55 | |||
56 | synchronized def incrementDecisionCount() { | ||
57 | decisionsTried++ | ||
58 | } | ||
59 | |||
60 | public var int transformationInvocations | ||
61 | |||
62 | synchronized def incrementTransformationCount() { | ||
63 | transformationInvocations++ | ||
64 | } | ||
65 | |||
66 | public var int scopePropagatorInvocations | ||
67 | |||
68 | synchronized def incrementScopePropagationCount() { | ||
69 | scopePropagatorInvocations++ | ||
70 | } | ||
71 | |||
72 | public var int scopePropagatorSolverInvocations | ||
73 | |||
74 | synchronized def incrementScopePropagationSolverCount() { | ||
75 | scopePropagatorSolverInvocations++ | ||
76 | } | ||
77 | } | ||
78 | |||
79 | @Data class ModelGenerationMethod { | ||
80 | ModelGenerationStatistics statistics | ||
81 | |||
82 | Collection<? extends BatchTransformationRule<?, ?>> objectRefinementRules | ||
83 | Collection<? extends BatchTransformationRule<?, ?>> relationRefinementRules | ||
84 | |||
85 | List<MultiplicityGoalConstraintCalculator> unfinishedMultiplicities | ||
86 | |||
87 | Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWF | ||
88 | |||
89 | Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidWF | ||
90 | |||
91 | Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> mustUnitPropagationPreconditions | ||
92 | Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> currentUnitPropagationPreconditions | ||
93 | |||
94 | Map<String, ModalPatternQueries> modalRelationQueries | ||
95 | |||
96 | Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allPatterns | ||
97 | } | ||
98 | |||
99 | enum TypeInferenceMethod { | ||
100 | Generic, | ||
101 | PreliminaryAnalysis | ||
102 | } | ||
103 | |||
104 | class ModelGenerationMethodProvider { | ||
105 | val PatternProvider patternProvider = new PatternProvider | ||
106 | val RefinementRuleProvider refinementRuleProvider = new RefinementRuleProvider | ||
107 | val GoalConstraintProvider goalConstraintProvider = new GoalConstraintProvider | ||
108 | val relationConstraintCalculator = new RelationConstraintCalculator | ||
109 | |||
110 | def ModelGenerationMethod createModelGenerationMethod( | ||
111 | LogicProblem logicProblem, | ||
112 | PartialInterpretation emptySolution, | ||
113 | ReasonerWorkspace workspace, | ||
114 | boolean nameNewElements, | ||
115 | TypeInferenceMethod typeInferenceMethod, | ||
116 | boolean calculateObjectCreationCosts, | ||
117 | ScopePropagatorStrategy scopePropagatorStrategy, | ||
118 | Collection<LinearTypeConstraintHint> hints, | ||
119 | DocumentationLevel debugLevel | ||
120 | ) { | ||
121 | val statistics = new ModelGenerationStatistics | ||
122 | val writeFiles = (debugLevel === DocumentationLevel.NORMAL || debugLevel === DocumentationLevel.FULL) | ||
123 | |||
124 | val Set<PQuery> existingQueries = logicProblem.relations.map[annotations].flatten.filter(TransfomedViatraQuery). | ||
125 | map[it.patternPQuery as PQuery].toSet | ||
126 | |||
127 | val relationConstraints = relationConstraintCalculator.calculateRelationConstraints(logicProblem) | ||
128 | val queries = patternProvider.generateQueries(logicProblem, emptySolution, statistics, existingQueries, | ||
129 | workspace, typeInferenceMethod, scopePropagatorStrategy, relationConstraints, hints, writeFiles) | ||
130 | |||
131 | val scopePropagator = createScopePropagator(scopePropagatorStrategy, emptySolution, hints, queries, statistics) | ||
132 | scopePropagator.propagateAllScopeConstraints | ||
133 | val objectRefinementRules = refinementRuleProvider.createObjectRefinementRules(logicProblem, emptySolution, | ||
134 | queries, scopePropagator, nameNewElements, statistics) | ||
135 | val relationRefinementRules = refinementRuleProvider.createRelationRefinementRules(queries, scopePropagator, | ||
136 | statistics) | ||
137 | |||
138 | val unfinishedMultiplicities = goalConstraintProvider.getUnfinishedMultiplicityQueries(logicProblem, queries, | ||
139 | calculateObjectCreationCosts) | ||
140 | |||
141 | val unfinishedWF = queries.getUnfinishedWFQueries.values | ||
142 | |||
143 | val modalRelationQueriesBuilder = ImmutableMap.builder | ||
144 | for (entry : queries.modalRelationQueries.entrySet) { | ||
145 | val annotation = entry.key.annotations.filter(TransfomedViatraQuery).head | ||
146 | if (annotation !== null) { | ||
147 | modalRelationQueriesBuilder.put(annotation.patternFullyQualifiedName, entry.value) | ||
148 | } | ||
149 | } | ||
150 | val modalRelationQueries = modalRelationQueriesBuilder.build | ||
151 | |||
152 | val invalidWF = queries.getInvalidWFQueries.values | ||
153 | |||
154 | val mustUnitPropagationPreconditions = queries.getMustUnitPropagationPreconditionPatterns | ||
155 | val currentUnitPropagationPreconditions = queries.getCurrentUnitPropagationPreconditionPatterns | ||
156 | |||
157 | val queriesToPrepare = ImmutableSet.builder.addAll(queries.refineObjectQueries.values).addAll( | ||
158 | queries.refineTypeQueries.values).addAll(queries.refinerelationQueries.values).addAll(queries. | ||
159 | multiplicityConstraintQueries.values.flatMap[allQueries]).addAll(queries.unfinishedWFQueries.values).addAll( | ||
160 | queries.invalidWFQueries.values).addAll(queries.mustUnitPropagationPreconditionPatterns.values).addAll( | ||
161 | queries.currentUnitPropagationPreconditionPatterns.values).add(queries.hasElementInContainmentQuery).build | ||
162 | val queryEngine = ViatraQueryEngine.on(new EMFScope(emptySolution)) | ||
163 | GenericQueryGroup.of(queriesToPrepare).prepare(queryEngine) | ||
164 | |||
165 | return new ModelGenerationMethod( | ||
166 | statistics, | ||
167 | objectRefinementRules.values, | ||
168 | relationRefinementRules.values, | ||
169 | unfinishedMultiplicities, | ||
170 | unfinishedWF, | ||
171 | invalidWF, | ||
172 | mustUnitPropagationPreconditions, | ||
173 | currentUnitPropagationPreconditions, | ||
174 | modalRelationQueries, | ||
175 | queries.allQueries | ||
176 | ) | ||
177 | } | ||
178 | |||
179 | private def createScopePropagator(ScopePropagatorStrategy scopePropagatorStrategy, | ||
180 | PartialInterpretation emptySolution, Collection<LinearTypeConstraintHint> hints, GeneratedPatterns queries, | ||
181 | ModelGenerationStatistics statistics) { | ||
182 | if (!hints.empty && !(scopePropagatorStrategy instanceof ScopePropagatorStrategy.Polyhedral)) { | ||
183 | throw new IllegalArgumentException("Only the Polyhedral scope propagator strategy can use hints.") | ||
184 | } | ||
185 | switch (scopePropagatorStrategy) { | ||
186 | case ScopePropagatorStrategy.None, | ||
187 | case ScopePropagatorStrategy.Basic: | ||
188 | new ScopePropagator(emptySolution, statistics) | ||
189 | case ScopePropagatorStrategy.BasicTypeHierarchy: | ||
190 | new TypeHierarchyScopePropagator(emptySolution, statistics) | ||
191 | ScopePropagatorStrategy.Polyhedral: { | ||
192 | val types = queries.refineObjectQueries.keySet.map[newType].toSet | ||
193 | val allPatternsByName = queries.allQueries.toMap[fullyQualifiedName] | ||
194 | val solver = switch (scopePropagatorStrategy.solver) { | ||
195 | case Z3Integer: | ||
196 | new Z3PolyhedronSolver(false, scopePropagatorStrategy.timeoutSeconds) | ||
197 | case Z3Real: | ||
198 | new Z3PolyhedronSolver(true, scopePropagatorStrategy.timeoutSeconds) | ||
199 | case Cbc: | ||
200 | new CbcPolyhedronSolver(false, scopePropagatorStrategy.timeoutSeconds, true) | ||
201 | case Clp: | ||
202 | new CbcPolyhedronSolver(true, scopePropagatorStrategy.timeoutSeconds, true) | ||
203 | default: | ||
204 | throw new IllegalArgumentException("Unknown polyhedron solver: " + | ||
205 | scopePropagatorStrategy.solver) | ||
206 | } | ||
207 | new PolyhedronScopePropagator(emptySolution, statistics, types, queries.multiplicityConstraintQueries, | ||
208 | queries.hasElementInContainmentQuery, allPatternsByName, hints, solver, | ||
209 | scopePropagatorStrategy.requiresUpperBoundIndexing, scopePropagatorStrategy.updateHeuristic) | ||
210 | } | ||
211 | default: | ||
212 | throw new IllegalArgumentException("Unknown scope propagator strategy: " + scopePropagatorStrategy) | ||
213 | } | ||
214 | } | ||
215 | } | ||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationStatistics.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationStatistics.xtend new file mode 100644 index 00000000..bd5bf807 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationStatistics.xtend | |||
@@ -0,0 +1,47 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra | ||
2 | |||
3 | class ModelGenerationStatistics { | ||
4 | public var long transformationExecutionTime = 0 | ||
5 | |||
6 | synchronized def addExecutionTime(long amount) { | ||
7 | transformationExecutionTime += amount | ||
8 | } | ||
9 | |||
10 | public var long scopePropagationTime = 0 | ||
11 | |||
12 | synchronized def addScopePropagationTime(long amount) { | ||
13 | scopePropagationTime += amount | ||
14 | } | ||
15 | |||
16 | public var long mustRelationPropagationTime = 0 | ||
17 | |||
18 | synchronized def addMustRelationPropagationTime(long amount) { | ||
19 | mustRelationPropagationTime += amount | ||
20 | } | ||
21 | |||
22 | public var long preliminaryTypeAnalisisTime = 0 | ||
23 | |||
24 | public var int decisionsTried = 0 | ||
25 | |||
26 | synchronized def incrementDecisionCount() { | ||
27 | decisionsTried++ | ||
28 | } | ||
29 | |||
30 | public var int transformationInvocations | ||
31 | |||
32 | synchronized def incrementTransformationCount() { | ||
33 | transformationInvocations++ | ||
34 | } | ||
35 | |||
36 | public var int scopePropagatorInvocations | ||
37 | |||
38 | synchronized def incrementScopePropagationCount() { | ||
39 | scopePropagatorInvocations++ | ||
40 | } | ||
41 | |||
42 | public var int scopePropagatorSolverInvocations | ||
43 | |||
44 | synchronized def incrementScopePropagationSolverCount() { | ||
45 | scopePropagatorSolverInvocations++ | ||
46 | } | ||
47 | } | ||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/TypeInferenceMethod.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/TypeInferenceMethod.xtend new file mode 100644 index 00000000..9296a0be --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/TypeInferenceMethod.xtend | |||
@@ -0,0 +1,44 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra | ||
2 | |||
3 | import com.google.common.collect.ImmutableMap | ||
4 | import com.google.common.collect.ImmutableSet | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | ||
7 | import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransfomedViatraQuery | ||
8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.CachingSimplePolyhedronScopePropagatorStrategy | ||
9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.CbcPolyhedronSolver | ||
10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearTypeConstraintHint | ||
11 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.MultiplicityGoalConstraintCalculator | ||
12 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronScopePropagator | ||
13 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.RelationConstraintCalculator | ||
14 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagator | ||
15 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy | ||
16 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.TypeHierarchyScopePropagator | ||
17 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Z3PolyhedronSolver | ||
18 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.GeneratedPatterns | ||
19 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.ModalPatternQueries | ||
20 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.PatternProvider | ||
21 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.UnitPropagationPatternGenerator | ||
22 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules.GoalConstraintProvider | ||
23 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules.RefinementRuleProvider | ||
24 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | ||
25 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace | ||
26 | import java.util.Collection | ||
27 | import java.util.List | ||
28 | import java.util.Map | ||
29 | import java.util.Set | ||
30 | import org.eclipse.viatra.query.runtime.api.GenericQueryGroup | ||
31 | import org.eclipse.viatra.query.runtime.api.IPatternMatch | ||
32 | import org.eclipse.viatra.query.runtime.api.IQuerySpecification | ||
33 | import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine | ||
34 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher | ||
35 | import org.eclipse.viatra.query.runtime.emf.EMFScope | ||
36 | import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint | ||
37 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery | ||
38 | import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRule | ||
39 | import org.eclipse.xtend.lib.annotations.Data | ||
40 | |||
41 | enum TypeInferenceMethod { | ||
42 | Generic, | ||
43 | PreliminaryAnalysis | ||
44 | } \ No newline at end of file | ||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ExtendedLinearExpressionBuilderFactory.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ExtendedLinearExpressionBuilderFactory.xtend new file mode 100644 index 00000000..6054affe --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ExtendedLinearExpressionBuilderFactory.xtend | |||
@@ -0,0 +1,140 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality | ||
2 | |||
3 | import com.google.common.collect.ImmutableList | ||
4 | import com.google.common.collect.ImmutableMap | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
6 | import java.util.ArrayList | ||
7 | import java.util.HashMap | ||
8 | import java.util.HashSet | ||
9 | import java.util.List | ||
10 | import java.util.Map | ||
11 | import java.util.Set | ||
12 | import org.eclipse.viatra.query.runtime.api.IPatternMatch | ||
13 | import org.eclipse.xtend.lib.annotations.Accessors | ||
14 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor | ||
15 | |||
16 | interface BoundSaturationListener { | ||
17 | def void boundsSaturated(Integer lower, Integer upper) | ||
18 | } | ||
19 | |||
20 | interface ExtendedLinearExpressionBuilderFactory { | ||
21 | def ExtendedLinearExpressionBuilder createBuilder() | ||
22 | |||
23 | def Dimension getDimension(IPatternMatch patternMatch) | ||
24 | } | ||
25 | |||
26 | interface ExtendedLinearExpressionBuilder extends LinearTypeExpressionBuilder { | ||
27 | override ExtendedLinearExpressionBuilder add(int scale, Type type) | ||
28 | |||
29 | def ExtendedLinearExpressionBuilder add(int scale, IPatternMatch patternMatch) | ||
30 | |||
31 | def ExtendedLinearExpressionBuilder add(int scale, Dimension dimension) | ||
32 | |||
33 | def LinearBoundedExpression build(BoundSaturationListener listener) | ||
34 | } | ||
35 | |||
36 | class ExtendedPolyhedronBuilder implements ExtendedLinearExpressionBuilderFactory { | ||
37 | val Map<Type, LinearBoundedExpression> typeBounds | ||
38 | val Map<Map<Dimension, Integer>, LinearBoundedExpression> expressionsCache | ||
39 | |||
40 | val ImmutableList.Builder<Dimension> dimensions = ImmutableList.builder | ||
41 | val Set<LinearConstraint> constraints = new HashSet | ||
42 | val Set<LinearBoundedExpression> expressionsToSaturate = new HashSet | ||
43 | val Map<IPatternMatch, Dimension> patternMatchCounts = new HashMap | ||
44 | @Accessors(PUBLIC_GETTER) val List<Pair<LinearBoundedExpression, BoundSaturationListener>> saturationListeners = new ArrayList | ||
45 | |||
46 | new(Polyhedron polyhedron, Map<Type, LinearBoundedExpression> typeBounds, | ||
47 | Map<Map<Dimension, Integer>, LinearBoundedExpression> initialExpressionsCache) { | ||
48 | this.typeBounds = typeBounds | ||
49 | this.expressionsCache = new HashMap(initialExpressionsCache) | ||
50 | dimensions.addAll(polyhedron.dimensions) | ||
51 | constraints.addAll(polyhedron.constraints) | ||
52 | expressionsToSaturate.addAll(polyhedron.expressionsToSaturate) | ||
53 | } | ||
54 | |||
55 | override createBuilder() { | ||
56 | new ExtendedLinearExpressionBuilderImpl(this) | ||
57 | } | ||
58 | |||
59 | override getDimension(IPatternMatch patternMatch) { | ||
60 | patternMatchCounts.computeIfAbsent(patternMatch) [ key | | ||
61 | val dimension = new Dimension(key.toString, 0, null) | ||
62 | dimensions.add(dimension) | ||
63 | dimension | ||
64 | ] | ||
65 | } | ||
66 | |||
67 | def buildPolyhedron() { | ||
68 | new Polyhedron( | ||
69 | dimensions.build, | ||
70 | ImmutableList.copyOf(constraints), | ||
71 | ImmutableList.copyOf(expressionsToSaturate) | ||
72 | ) | ||
73 | } | ||
74 | |||
75 | @FinalFieldsConstructor | ||
76 | private static class ExtendedLinearExpressionBuilderImpl implements ExtendedLinearExpressionBuilder { | ||
77 | val ExtendedPolyhedronBuilder polyhedronBuilder | ||
78 | |||
79 | val Map<Dimension, Integer> coefficients = new HashMap | ||
80 | |||
81 | override add(int scale, Type type) { | ||
82 | val expression = polyhedronBuilder.typeBounds.get(type) | ||
83 | if (expression === null) { | ||
84 | throw new IllegalArgumentException("Unknown Type: " + type) | ||
85 | } | ||
86 | add(scale, expression) | ||
87 | } | ||
88 | |||
89 | override add(int scale, IPatternMatch patternMatch) { | ||
90 | val dimension = polyhedronBuilder.getDimension(patternMatch) | ||
91 | add(scale, dimension) | ||
92 | } | ||
93 | |||
94 | private def add(int scale, LinearBoundedExpression expression) { | ||
95 | switch (expression) { | ||
96 | Dimension: add(scale, expression) | ||
97 | LinearConstraint: add(scale, expression.coefficients) | ||
98 | default: throw new IllegalArgumentException("Unknown LinearBoundedExpression: " + expression) | ||
99 | } | ||
100 | } | ||
101 | |||
102 | private def add(int scale, Map<Dimension, Integer> coefficients) { | ||
103 | for (pair : coefficients.entrySet) { | ||
104 | add(scale * pair.value, pair.key) | ||
105 | } | ||
106 | this | ||
107 | } | ||
108 | |||
109 | override add(int scale, Dimension dimension) { | ||
110 | coefficients.merge(dimension, scale)[a, b|a + b] | ||
111 | this | ||
112 | } | ||
113 | |||
114 | override build() { | ||
115 | val filteredCoefficients = ImmutableMap.copyOf(coefficients.filter [ _, coefficient | | ||
116 | coefficient != 0 | ||
117 | ]) | ||
118 | polyhedronBuilder.expressionsCache.computeIfAbsent(filteredCoefficients) [ map | | ||
119 | if (map.size == 1) { | ||
120 | val pair = map.entrySet.head | ||
121 | if (pair.value == 1) { | ||
122 | return pair.key | ||
123 | } | ||
124 | } | ||
125 | val constraint = new LinearConstraint(map) | ||
126 | polyhedronBuilder.constraints.add(constraint) | ||
127 | constraint | ||
128 | ] | ||
129 | } | ||
130 | |||
131 | override build(BoundSaturationListener listener) { | ||
132 | val expression = build() | ||
133 | if (listener !== null) { | ||
134 | polyhedronBuilder.expressionsToSaturate.add(expression) | ||
135 | polyhedronBuilder.saturationListeners.add(expression -> listener) | ||
136 | } | ||
137 | expression | ||
138 | } | ||
139 | } | ||
140 | } | ||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ExtendedPolyhedronScopePropagatorStrategy.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ExtendedPolyhedronScopePropagatorStrategy.xtend new file mode 100644 index 00000000..32923396 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ExtendedPolyhedronScopePropagatorStrategy.xtend | |||
@@ -0,0 +1,63 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
4 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationStatistics | ||
5 | import java.util.Collection | ||
6 | import java.util.Map | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation | ||
8 | |||
9 | interface PolyhedronExtensionOperator { | ||
10 | def void extendPolyhedron(ExtendedLinearExpressionBuilderFactory factory) | ||
11 | } | ||
12 | |||
13 | class ExtendedPolyhedronScopePropagatorStrategy extends PolyhedronScopePropagatorStrategy { | ||
14 | val PolyhedronSolver solver | ||
15 | val Collection<PolyhedronExtensionOperator> extensionOperators | ||
16 | |||
17 | var Map<Type, LinearBoundedExpression> typeBounds | ||
18 | var Map<Map<Dimension, Integer>, LinearBoundedExpression> initialExpressionsCache | ||
19 | |||
20 | new(PolyhedronSolver solver, Collection<PolyhedronExtensionOperator> extensionOperators, | ||
21 | ModelGenerationStatistics statistics) { | ||
22 | super(statistics) | ||
23 | this.solver = solver | ||
24 | this.extensionOperators = extensionOperators | ||
25 | } | ||
26 | |||
27 | override setPolyhedron(Polyhedron polyhedron, Map<Type, LinearBoundedExpression> typeBounds, | ||
28 | Map<Map<Dimension, Integer>, LinearBoundedExpression> initialExpressionsCache) { | ||
29 | super.setPolyhedron(polyhedron, typeBounds, initialExpressionsCache) | ||
30 | this.typeBounds = typeBounds | ||
31 | this.initialExpressionsCache = initialExpressionsCache | ||
32 | } | ||
33 | |||
34 | override isRelevantRelation(Relation relation) { | ||
35 | true | ||
36 | } | ||
37 | |||
38 | override protected doSaturate() { | ||
39 | val builder = new ExtendedPolyhedronBuilder(polyhedron, typeBounds, initialExpressionsCache) | ||
40 | for (extensionOperator : extensionOperators) { | ||
41 | extensionOperator.extendPolyhedron(builder) | ||
42 | } | ||
43 | val extendedPolyhedron = builder.buildPolyhedron() | ||
44 | val saturationOperator = solver.createSaturationOperator(extendedPolyhedron) | ||
45 | val result = try { | ||
46 | saturationOperator.saturate() | ||
47 | } finally { | ||
48 | saturationOperator.close() | ||
49 | } | ||
50 | if (result == PolyhedronSaturationResult.EMPTY) { | ||
51 | // The partial model cannot be refined any more, we can't provide objective bounds. | ||
52 | for (pair : builder.saturationListeners) { | ||
53 | pair.value.boundsSaturated(null, null) | ||
54 | } | ||
55 | return false | ||
56 | } | ||
57 | for (pair : builder.saturationListeners) { | ||
58 | val expression = pair.key | ||
59 | pair.value.boundsSaturated(expression.lowerBound, expression.upperBound) | ||
60 | } | ||
61 | true | ||
62 | } | ||
63 | } | ||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/LinearTypeConstraintHint.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/LinearTypeConstraintHint.xtend index 8c21ca1d..31f98e36 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/LinearTypeConstraintHint.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/LinearTypeConstraintHint.xtend | |||
@@ -3,8 +3,10 @@ package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality | |||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | 3 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type |
4 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.PatternGenerator | 4 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.PatternGenerator |
5 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | 5 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation |
6 | import java.util.Map | ||
6 | import org.eclipse.viatra.query.runtime.api.IPatternMatch | 7 | import org.eclipse.viatra.query.runtime.api.IPatternMatch |
7 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher | 8 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher |
9 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery | ||
8 | 10 | ||
9 | interface LinearTypeExpressionBuilderFactory { | 11 | interface LinearTypeExpressionBuilderFactory { |
10 | def ViatraQueryMatcher<? extends IPatternMatch> createMatcher(String queryName) | 12 | def ViatraQueryMatcher<? extends IPatternMatch> createMatcher(String queryName) |
@@ -24,7 +26,7 @@ interface RelationConstraintUpdater { | |||
24 | } | 26 | } |
25 | 27 | ||
26 | interface LinearTypeConstraintHint { | 28 | interface LinearTypeConstraintHint { |
27 | def CharSequence getAdditionalPatterns(PatternGenerator patternGenerator) | 29 | def CharSequence getAdditionalPatterns(PatternGenerator patternGenerator, Map<String, PQuery> fqnToPQuery) |
28 | 30 | ||
29 | def RelationConstraintUpdater createConstraintUpdater(LinearTypeExpressionBuilderFactory builderFactory) | 31 | def RelationConstraintUpdater createConstraintUpdater(LinearTypeExpressionBuilderFactory builderFactory) |
30 | } | 32 | } |
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 c28d4caa..ad8f94ab 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend | |||
@@ -1,7 +1,5 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality | 1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality |
2 | 2 | ||
3 | import com.google.common.cache.Cache | ||
4 | import com.google.common.cache.CacheBuilder | ||
5 | import com.google.common.collect.ImmutableList | 3 | import com.google.common.collect.ImmutableList |
6 | import com.google.common.collect.ImmutableMap | 4 | import com.google.common.collect.ImmutableMap |
7 | import com.google.common.collect.ImmutableSet | 5 | import com.google.common.collect.ImmutableSet |
@@ -23,7 +21,6 @@ import java.util.HashSet | |||
23 | import java.util.List | 21 | import java.util.List |
24 | import java.util.Map | 22 | import java.util.Map |
25 | import java.util.Set | 23 | import java.util.Set |
26 | import javax.naming.OperationNotSupportedException | ||
27 | import org.eclipse.viatra.query.runtime.api.IPatternMatch | 24 | import org.eclipse.viatra.query.runtime.api.IPatternMatch |
28 | import org.eclipse.viatra.query.runtime.api.IQuerySpecification | 25 | import org.eclipse.viatra.query.runtime.api.IQuerySpecification |
29 | import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine | 26 | import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine |
@@ -32,31 +29,29 @@ import org.eclipse.viatra.query.runtime.emf.EMFScope | |||
32 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor | 29 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor |
33 | 30 | ||
34 | class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { | 31 | class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { |
35 | static val CACHE_SIZE = 10000 | ||
36 | |||
37 | val boolean updateHeuristic | 32 | val boolean updateHeuristic |
38 | val Map<Scope, LinearBoundedExpression> scopeBounds | 33 | val Map<Scope, LinearBoundedExpression> scopeBounds |
39 | val LinearBoundedExpression topLevelBounds | 34 | val LinearBoundedExpression topLevelBounds |
40 | val Polyhedron polyhedron | 35 | val Polyhedron polyhedron |
41 | val PolyhedronSaturationOperator operator | 36 | val PolyhedronScopePropagatorStrategy strategy |
42 | val Set<Relation> relevantRelations | 37 | val Set<Relation> relevantRelations |
43 | val Cache<PolyhedronSignature, PolyhedronSignature> cache = CacheBuilder.newBuilder.maximumSize(CACHE_SIZE).build | ||
44 | List<RelationConstraintUpdater> updaters = emptyList | 38 | List<RelationConstraintUpdater> updaters = emptyList |
45 | 39 | ||
46 | new(PartialInterpretation p, ModelGenerationStatistics statistics, Set<? extends Type> possibleNewDynamicTypes, | 40 | new(PartialInterpretation p, ModelGenerationStatistics statistics, Set<? extends Type> possibleNewDynamicTypes, |
47 | Map<RelationMultiplicityConstraint, UnifinishedMultiplicityQueries> unfinishedMultiplicityQueries, | 41 | Map<RelationMultiplicityConstraint, UnifinishedMultiplicityQueries> unfinishedMultiplicityQueries, |
48 | IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> hasElementInContainmentQuery, | 42 | IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> hasElementInContainmentQuery, |
49 | Map<String, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allPatternsByName, | 43 | Map<String, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allPatternsByName, |
50 | Collection<LinearTypeConstraintHint> hints, PolyhedronSolver solver, boolean propagateRelations, | 44 | Collection<LinearTypeConstraintHint> hints, PolyhedronScopePropagatorStrategy strategy, |
51 | boolean updateHeuristic) { | 45 | boolean propagateRelations, boolean updateHeuristic) { |
52 | super(p, statistics) | 46 | super(p, statistics) |
53 | this.updateHeuristic = updateHeuristic | 47 | this.updateHeuristic = updateHeuristic |
48 | this.strategy = strategy | ||
54 | val builder = new PolyhedronBuilder(p) | 49 | val builder = new PolyhedronBuilder(p) |
55 | builder.buildPolyhedron(possibleNewDynamicTypes) | 50 | builder.buildPolyhedron(possibleNewDynamicTypes) |
56 | scopeBounds = builder.scopeBounds | 51 | scopeBounds = builder.scopeBounds |
57 | topLevelBounds = builder.topLevelBounds | 52 | topLevelBounds = builder.topLevelBounds |
58 | polyhedron = builder.polyhedron | 53 | polyhedron = builder.polyhedron |
59 | operator = solver.createSaturationOperator(polyhedron) | 54 | strategy.setPolyhedron(polyhedron, builder.typeBounds, builder.expressionsCache) |
60 | propagateAllScopeConstraints() | 55 | propagateAllScopeConstraints() |
61 | if (propagateRelations) { | 56 | if (propagateRelations) { |
62 | val maximumNumberOfNewNodes = topLevelBounds.upperBound | 57 | val maximumNumberOfNewNodes = topLevelBounds.upperBound |
@@ -80,30 +75,10 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { | |||
80 | resetBounds() | 75 | resetBounds() |
81 | populatePolyhedronFromScope() | 76 | populatePolyhedronFromScope() |
82 | // println(polyhedron) | 77 | // println(polyhedron) |
83 | val signature = polyhedron.createSignature | 78 | if (strategy.saturate) { |
84 | val cachedSignature = cache.getIfPresent(signature) | 79 | populateScopesFromPolyhedron() |
85 | switch (cachedSignature) { | 80 | } else { |
86 | case null: { | 81 | setScopesInvalid() |
87 | statistics.incrementScopePropagationSolverCount | ||
88 | val result = operator.saturate() | ||
89 | if (result == PolyhedronSaturationResult.EMPTY) { | ||
90 | cache.put(signature, PolyhedronSignature.EMPTY) | ||
91 | // println("INVALID") | ||
92 | setScopesInvalid() | ||
93 | } else { | ||
94 | val resultSignature = polyhedron.createSignature | ||
95 | cache.put(signature, resultSignature) | ||
96 | populateScopesFromPolyhedron() | ||
97 | } | ||
98 | } | ||
99 | case PolyhedronSignature.EMPTY: | ||
100 | setScopesInvalid() | ||
101 | PolyhedronSignature.Bounds: { | ||
102 | polyhedron.applySignature(signature) | ||
103 | populateScopesFromPolyhedron() | ||
104 | } | ||
105 | default: | ||
106 | throw new IllegalStateException("Unknown polyhedron signature: " + signature) | ||
107 | } | 82 | } |
108 | // println(polyhedron) | 83 | // println(polyhedron) |
109 | if (updateHeuristic) { | 84 | if (updateHeuristic) { |
@@ -112,9 +87,9 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { | |||
112 | } | 87 | } |
113 | 88 | ||
114 | override isPropagationNeededAfterAdditionToRelation(Relation r) { | 89 | override isPropagationNeededAfterAdditionToRelation(Relation r) { |
115 | relevantRelations.contains(r) || super.isPropagationNeededAfterAdditionToRelation(r) | 90 | relevantRelations.contains(r) || strategy.isRelevantRelation(r) || super.isPropagationNeededAfterAdditionToRelation(r) |
116 | } | 91 | } |
117 | 92 | ||
118 | override isQueryEngineFlushRequiredBeforePropagation() { | 93 | override isQueryEngineFlushRequiredBeforePropagation() { |
119 | true | 94 | true |
120 | } | 95 | } |
@@ -253,7 +228,10 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { | |||
253 | } | 228 | } |
254 | buildRelevantRelations(constraints.keySet) | 229 | buildRelevantRelations(constraints.keySet) |
255 | for (hint : hints) { | 230 | for (hint : hints) { |
256 | updatersBuilder.add(hint.createConstraintUpdater(this)) | 231 | val updater = hint.createConstraintUpdater(this) |
232 | if (updater !== null) { | ||
233 | updatersBuilder.add(updater) | ||
234 | } | ||
257 | } | 235 | } |
258 | updaters = updatersBuilder.build | 236 | updaters = updatersBuilder.build |
259 | addCachedConstraintsToPolyhedron() | 237 | addCachedConstraintsToPolyhedron() |
@@ -410,7 +388,7 @@ class PolyhedronScopePropagator extends TypeHierarchyScopePropagator { | |||
410 | for (scope : p.scopes) { | 388 | for (scope : p.scopes) { |
411 | switch (targetTypeInterpretation : scope.targetTypeInterpretation) { | 389 | switch (targetTypeInterpretation : scope.targetTypeInterpretation) { |
412 | PartialPrimitiveInterpretation: | 390 | PartialPrimitiveInterpretation: |
413 | throw new OperationNotSupportedException("Primitive type scopes are not yet implemented") | 391 | throw new IllegalStateException("Primitive type scopes are not yet implemented") |
414 | PartialComplexTypeInterpretation: { | 392 | PartialComplexTypeInterpretation: { |
415 | val complexType = targetTypeInterpretation.interpretationOf | 393 | val complexType = targetTypeInterpretation.interpretationOf |
416 | val typeBound = typeBounds.get(complexType) | 394 | val typeBound = typeBounds.get(complexType) |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagatorStrategy.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagatorStrategy.xtend new file mode 100644 index 00000000..f93dcd18 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagatorStrategy.xtend | |||
@@ -0,0 +1,92 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality | ||
2 | |||
3 | import com.google.common.cache.Cache | ||
4 | import com.google.common.cache.CacheBuilder | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationStatistics | ||
8 | import java.util.Map | ||
9 | import org.eclipse.xtend.lib.annotations.Accessors | ||
10 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor | ||
11 | |||
12 | @FinalFieldsConstructor | ||
13 | abstract class PolyhedronScopePropagatorStrategy { | ||
14 | val ModelGenerationStatistics statistics | ||
15 | |||
16 | @Accessors(PUBLIC_GETTER) var Polyhedron polyhedron | ||
17 | |||
18 | def void setPolyhedron(Polyhedron polyhedron, Map<Type, LinearBoundedExpression> typeBounds, | ||
19 | Map<Map<Dimension, Integer>, LinearBoundedExpression> initialExpressionsCache) { | ||
20 | if (this.polyhedron !== null) { | ||
21 | throw new IllegalStateException("polyhedron was already set") | ||
22 | } | ||
23 | this.polyhedron = polyhedron | ||
24 | initialize() | ||
25 | } | ||
26 | |||
27 | def boolean saturate() { | ||
28 | if (polyhedron === null) { | ||
29 | throw new IllegalStateException("polyhedron was not set") | ||
30 | } | ||
31 | doSaturate() | ||
32 | } | ||
33 | |||
34 | def boolean isRelevantRelation(Relation relation) { | ||
35 | false | ||
36 | } | ||
37 | |||
38 | protected def incrementScopePropagationSolverCount() { | ||
39 | statistics.incrementScopePropagationSolverCount() | ||
40 | } | ||
41 | |||
42 | protected def void initialize() { | ||
43 | } | ||
44 | |||
45 | protected def boolean doSaturate() | ||
46 | } | ||
47 | |||
48 | @FinalFieldsConstructor | ||
49 | class CachingSimplePolyhedronScopePropagatorStrategy extends PolyhedronScopePropagatorStrategy { | ||
50 | static val CACHE_SIZE = 10000 | ||
51 | |||
52 | val PolyhedronSolver solver | ||
53 | |||
54 | val Cache<PolyhedronSignature, PolyhedronSignature> cache = CacheBuilder.newBuilder.maximumSize(CACHE_SIZE).build | ||
55 | var PolyhedronSaturationOperator operator | ||
56 | |||
57 | new(PolyhedronSolver solver, ModelGenerationStatistics statistics) { | ||
58 | super(statistics) | ||
59 | this.solver = solver | ||
60 | } | ||
61 | |||
62 | override protected initialize() { | ||
63 | operator = solver.createSaturationOperator(polyhedron) | ||
64 | } | ||
65 | |||
66 | override protected doSaturate() { | ||
67 | val signature = polyhedron.createSignature | ||
68 | val cachedSignature = cache.getIfPresent(signature) | ||
69 | switch (cachedSignature) { | ||
70 | case null: { | ||
71 | incrementScopePropagationSolverCount() | ||
72 | val result = operator.saturate() | ||
73 | if (result == PolyhedronSaturationResult.EMPTY) { | ||
74 | cache.put(signature, PolyhedronSignature.EMPTY) | ||
75 | false | ||
76 | } else { | ||
77 | val resultSignature = polyhedron.createSignature | ||
78 | cache.put(signature, resultSignature) | ||
79 | true | ||
80 | } | ||
81 | } | ||
82 | case PolyhedronSignature.EMPTY: | ||
83 | false | ||
84 | PolyhedronSignature.Bounds: { | ||
85 | polyhedron.applySignature(signature) | ||
86 | true | ||
87 | } | ||
88 | default: | ||
89 | throw new IllegalStateException("Unknown polyhedron signature: " + signature) | ||
90 | } | ||
91 | } | ||
92 | } | ||
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 4e046190..21bd2d9e 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 | |||
@@ -116,7 +116,7 @@ abstract class PolyhedronSignature { | |||
116 | } | 116 | } |
117 | 117 | ||
118 | @Accessors | 118 | @Accessors |
119 | abstract class LinearBoundedExpression { | 119 | class Bounds { |
120 | var Integer lowerBound | 120 | var Integer lowerBound |
121 | var Integer upperBound | 121 | var Integer upperBound |
122 | 122 | ||
@@ -132,12 +132,19 @@ abstract class LinearBoundedExpression { | |||
132 | } | 132 | } |
133 | } | 133 | } |
134 | 134 | ||
135 | def void assertBetween(Integer tighterLowerBound, Integer tighterUpperBound) { | ||
136 | tightenLowerBound(tighterLowerBound) | ||
137 | tightenUpperBound(tighterUpperBound) | ||
138 | } | ||
139 | |||
135 | def void assertEqualsTo(int bound) { | 140 | def void assertEqualsTo(int bound) { |
136 | tightenLowerBound(bound) | 141 | assertBetween(bound, bound) |
137 | tightenUpperBound(bound) | ||
138 | } | 142 | } |
139 | } | 143 | } |
140 | 144 | ||
145 | abstract class LinearBoundedExpression extends Bounds { | ||
146 | } | ||
147 | |||
141 | @Accessors | 148 | @Accessors |
142 | class Dimension extends LinearBoundedExpression { | 149 | class Dimension extends LinearBoundedExpression { |
143 | val String name | 150 | val String name |
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 93b83577..cacba3c6 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 | |||
@@ -19,6 +19,8 @@ class ScopePropagator { | |||
19 | val Map<PartialTypeInterpratation, Scope> type2Scope | 19 | val Map<PartialTypeInterpratation, Scope> type2Scope |
20 | @Accessors(PROTECTED_GETTER) val Map<Scope, Set<Scope>> superScopes | 20 | @Accessors(PROTECTED_GETTER) val Map<Scope, Set<Scope>> superScopes |
21 | @Accessors(PROTECTED_GETTER) val Map<Scope, Set<Scope>> subScopes | 21 | @Accessors(PROTECTED_GETTER) val Map<Scope, Set<Scope>> subScopes |
22 | |||
23 | @Accessors(PUBLIC_GETTER) var scopePropagationNeeded = false | ||
22 | 24 | ||
23 | new(PartialInterpretation p, ModelGenerationStatistics statistics) { | 25 | new(PartialInterpretation p, ModelGenerationStatistics statistics) { |
24 | partialInterpretation = p | 26 | partialInterpretation = p |
@@ -64,7 +66,8 @@ class ScopePropagator { | |||
64 | copyScopeBoundsToHeuristic() | 66 | copyScopeBoundsToHeuristic() |
65 | } | 67 | } |
66 | 68 | ||
67 | def propagateAllScopeConstraints() { | 69 | def void propagateAllScopeConstraints() { |
70 | scopePropagationNeeded = false | ||
68 | if (!valid) { | 71 | if (!valid) { |
69 | return | 72 | return |
70 | } | 73 | } |
@@ -93,6 +96,7 @@ class ScopePropagator { | |||
93 | if (isPrimitive) { | 96 | if (isPrimitive) { |
94 | return | 97 | return |
95 | } | 98 | } |
99 | scopePropagationNeeded = true | ||
96 | // println('''Adding to «(t as PartialComplexTypeInterpretation).interpretationOf.name»''') | 100 | // println('''Adding to «(t as PartialComplexTypeInterpretation).interpretationOf.name»''') |
97 | val targetScope = type2Scope.get(t) | 101 | val targetScope = type2Scope.get(t) |
98 | if (targetScope !== null) { | 102 | if (targetScope !== null) { |
@@ -117,6 +121,12 @@ class ScopePropagator { | |||
117 | // this.partialInterpretation.scopes.forEach[println(''' «(it.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name»: «it.minNewElements»-«it.maxNewElements»''')] | 121 | // this.partialInterpretation.scopes.forEach[println(''' «(it.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name»: «it.minNewElements»-«it.maxNewElements»''')] |
118 | // println('''All constraints are propagated upon increasing «(t as PartialComplexTypeInterpretation).interpretationOf.name»''') | 122 | // println('''All constraints are propagated upon increasing «(t as PartialComplexTypeInterpretation).interpretationOf.name»''') |
119 | } | 123 | } |
124 | |||
125 | def addedToRelation(Relation r) { | ||
126 | if (isPropagationNeededAfterAdditionToRelation(r)) { | ||
127 | scopePropagationNeeded = true | ||
128 | } | ||
129 | } | ||
120 | 130 | ||
121 | protected def setScopesInvalid() { | 131 | protected def setScopesInvalid() { |
122 | partialInterpretation.minNewElements = Integer.MAX_VALUE | 132 | partialInterpretation.minNewElements = Integer.MAX_VALUE |
@@ -127,7 +137,7 @@ class ScopePropagator { | |||
127 | } | 137 | } |
128 | } | 138 | } |
129 | 139 | ||
130 | def isPropagationNeededAfterAdditionToRelation(Relation r) { | 140 | protected def isPropagationNeededAfterAdditionToRelation(Relation r) { |
131 | false | 141 | false |
132 | } | 142 | } |
133 | 143 | ||
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 80bc3844..edf92343 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 | |||
@@ -25,12 +25,13 @@ import java.util.HashMap | |||
25 | import java.util.Map | 25 | import java.util.Map |
26 | import org.eclipse.emf.ecore.EAttribute | 26 | import org.eclipse.emf.ecore.EAttribute |
27 | import org.eclipse.emf.ecore.EReference | 27 | import org.eclipse.emf.ecore.EReference |
28 | import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint | ||
28 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery | 29 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery |
29 | import org.eclipse.xtend.lib.annotations.Accessors | 30 | import org.eclipse.xtend.lib.annotations.Accessors |
31 | import org.eclipse.xtend.lib.annotations.Data | ||
32 | import org.eclipse.xtend2.lib.StringConcatenationClient | ||
30 | 33 | ||
31 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | 34 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* |
32 | import org.eclipse.xtend.lib.annotations.Data | ||
33 | import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint | ||
34 | 35 | ||
35 | @Data class PatternGeneratorResult { | 36 | @Data class PatternGeneratorResult { |
36 | CharSequence patternText | 37 | CharSequence patternText |
@@ -38,6 +39,14 @@ import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint | |||
38 | HashMap<PConstraint,String> constraint2CurrentPreconditionName | 39 | HashMap<PConstraint,String> constraint2CurrentPreconditionName |
39 | } | 40 | } |
40 | 41 | ||
42 | interface UnitPropagationPatternGenerator { | ||
43 | def Map<Relation, String> getMustPatterns() | ||
44 | |||
45 | def Map<Relation, String> getMustNotPatterns() | ||
46 | |||
47 | def StringConcatenationClient getAdditionalPatterns(PatternGenerator generator, Map<String, PQuery> fqn2PQuery) | ||
48 | } | ||
49 | |||
41 | class PatternGenerator { | 50 | class PatternGenerator { |
42 | @Accessors(PUBLIC_GETTER) val TypeIndexer typeIndexer // = new TypeIndexer(this) | 51 | @Accessors(PUBLIC_GETTER) val TypeIndexer typeIndexer // = new TypeIndexer(this) |
43 | @Accessors(PUBLIC_GETTER) val RelationDeclarationIndexer relationDeclarationIndexer = new RelationDeclarationIndexer( | 52 | @Accessors(PUBLIC_GETTER) val RelationDeclarationIndexer relationDeclarationIndexer = new RelationDeclarationIndexer( |
@@ -157,7 +166,8 @@ class PatternGenerator { | |||
157 | Map<String, PQuery> fqn2PQuery, | 166 | Map<String, PQuery> fqn2PQuery, |
158 | TypeAnalysisResult typeAnalysisResult, | 167 | TypeAnalysisResult typeAnalysisResult, |
159 | RelationConstraints constraints, | 168 | RelationConstraints constraints, |
160 | Collection<LinearTypeConstraintHint> hints | 169 | Collection<LinearTypeConstraintHint> hints, |
170 | Collection<UnitPropagationPatternGenerator> unitPropagationPatternGenerators | ||
161 | ) { | 171 | ) { |
162 | val first = | 172 | val first = |
163 | ''' | 173 | ''' |
@@ -313,7 +323,7 @@ class PatternGenerator { | |||
313 | ////////// | 323 | ////////// |
314 | // 1.2 Relation Declaration Indexers | 324 | // 1.2 Relation Declaration Indexers |
315 | ////////// | 325 | ////////// |
316 | «relationDeclarationIndexer.generateRelationIndexers(problem,problem.relations.filter(RelationDeclaration),fqn2PQuery)» | 326 | «relationDeclarationIndexer.generateRelationIndexers(problem,problem.relations.filter(RelationDeclaration),unitPropagationPatternGenerators,fqn2PQuery)» |
317 | 327 | ||
318 | ////////// | 328 | ////////// |
319 | // 1.3 Relation Definition Indexers | 329 | // 1.3 Relation Definition Indexers |
@@ -359,13 +369,16 @@ class PatternGenerator { | |||
359 | ////////// | 369 | ////////// |
360 | // 4.3 Relation refinement | 370 | // 4.3 Relation refinement |
361 | ////////// | 371 | ////////// |
362 | «relationRefinementGenerator.generateRefineReference(problem)» | 372 | «relationRefinementGenerator.generateRefineReference(problem, unitPropagationPatternGenerators)» |
363 | 373 | ||
364 | ////////// | 374 | ////////// |
365 | // 5 Hints | 375 | // 5 Hints |
366 | ////////// | 376 | ////////// |
367 | «FOR hint : hints» | 377 | «FOR hint : hints» |
368 | «hint.getAdditionalPatterns(this)» | 378 | «hint.getAdditionalPatterns(this, fqn2PQuery)» |
379 | «ENDFOR» | ||
380 | «FOR generator : unitPropagationPatternGenerators» | ||
381 | «generator.getAdditionalPatterns(this, fqn2PQuery)» | ||
369 | «ENDFOR» | 382 | «ENDFOR» |
370 | 383 | ||
371 | ////////// | 384 | ////////// |
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 d57705ce..2e786286 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 | |||
@@ -36,9 +36,10 @@ import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | |||
36 | public Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWFQueries | 36 | public Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWFQueries |
37 | public Map<RelationMultiplicityConstraint, UnifinishedMultiplicityQueries> multiplicityConstraintQueries | 37 | public Map<RelationMultiplicityConstraint, UnifinishedMultiplicityQueries> multiplicityConstraintQueries |
38 | public IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> hasElementInContainmentQuery | 38 | public IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> hasElementInContainmentQuery |
39 | public Map<ObjectCreationPrecondition, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineObjectQueries | 39 | public Map<ObjectCreationPrecondition, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineObjectQueries |
40 | public Map<? extends Type, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineTypeQueries | 40 | public Map<? extends Type, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineTypeQueries |
41 | public Map<Pair<RelationDeclaration, Relation>, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refinerelationQueries | 41 | public Map<Pair<RelationDeclaration, Relation>, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineRelationQueries |
42 | public Map<Pair<RelationDeclaration, Relation>, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> mustRelationPropagationQueries | ||
42 | public Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> mustUnitPropagationPreconditionPatterns | 43 | public Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> mustUnitPropagationPreconditionPatterns |
43 | public Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> currentUnitPropagationPreconditionPatterns | 44 | public Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> currentUnitPropagationPreconditionPatterns |
44 | public Map<RelationDefinition, ModalPatternQueries> modalRelationQueries | 45 | public Map<RelationDefinition, ModalPatternQueries> modalRelationQueries |
@@ -56,7 +57,7 @@ class ModalPatternQueries { | |||
56 | class UnifinishedMultiplicityQueries { | 57 | class UnifinishedMultiplicityQueries { |
57 | val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> existingMultiplicityQuery | 58 | val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> existingMultiplicityQuery |
58 | val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> existingInverseMultiplicityQuery | 59 | val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> existingInverseMultiplicityQuery |
59 | 60 | ||
60 | def Set<IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> getAllQueries() { | 61 | def Set<IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> getAllQueries() { |
61 | val builder = ImmutableSet.builder | 62 | val builder = ImmutableSet.builder |
62 | if (existingMultiplicityQuery !== null) { | 63 | if (existingMultiplicityQuery !== null) { |
@@ -70,13 +71,13 @@ class UnifinishedMultiplicityQueries { | |||
70 | } | 71 | } |
71 | 72 | ||
72 | class PatternProvider { | 73 | class PatternProvider { |
73 | |||
74 | val TypeAnalysis typeAnalysis = new TypeAnalysis | 74 | val TypeAnalysis typeAnalysis = new TypeAnalysis |
75 | 75 | ||
76 | def generateQueries(LogicProblem problem, PartialInterpretation emptySolution, ModelGenerationStatistics statistics, | 76 | def generateQueries(LogicProblem problem, PartialInterpretation emptySolution, ModelGenerationStatistics statistics, |
77 | Set<PQuery> existingQueries, ReasonerWorkspace workspace, TypeInferenceMethod typeInferenceMethod, | 77 | Set<PQuery> existingQueries, ReasonerWorkspace workspace, TypeInferenceMethod typeInferenceMethod, |
78 | ScopePropagatorStrategy scopePropagatorStrategy, RelationConstraints relationConstraints, | 78 | ScopePropagatorStrategy scopePropagatorStrategy, RelationConstraints relationConstraints, |
79 | Collection<LinearTypeConstraintHint> hints, boolean writeToFile) { | 79 | Collection<LinearTypeConstraintHint> hints, |
80 | Collection<UnitPropagationPatternGenerator> unitPropagationPatternGenerators, boolean writeToFile) { | ||
80 | val fqn2Query = existingQueries.toMap[it.fullyQualifiedName] | 81 | val fqn2Query = existingQueries.toMap[it.fullyQualifiedName] |
81 | val PatternGenerator patternGenerator = new PatternGenerator(typeInferenceMethod, scopePropagatorStrategy) | 82 | val PatternGenerator patternGenerator = new PatternGenerator(typeInferenceMethod, scopePropagatorStrategy) |
82 | val typeAnalysisResult = if (patternGenerator.requiresTypeAnalysis) { | 83 | val typeAnalysisResult = if (patternGenerator.requiresTypeAnalysis) { |
@@ -89,15 +90,16 @@ class PatternProvider { | |||
89 | null | 90 | null |
90 | } | 91 | } |
91 | val patternGeneratorResult = patternGenerator.transformBaseProperties(problem, emptySolution, fqn2Query, | 92 | val patternGeneratorResult = patternGenerator.transformBaseProperties(problem, emptySolution, fqn2Query, |
92 | typeAnalysisResult, relationConstraints, hints) | 93 | typeAnalysisResult, relationConstraints, hints, unitPropagationPatternGenerators) |
93 | if (writeToFile) { | 94 | if (writeToFile) { |
94 | workspace.writeText('''generated3valued.vql_deactivated''', patternGeneratorResult.patternText) | 95 | workspace.writeText('''generated3valued.vql_deactivated''', patternGeneratorResult.patternText) |
95 | } | 96 | } |
96 | val ParseUtil parseUtil = new ParseUtil | 97 | val ParseUtil parseUtil = new ParseUtil |
97 | val generatedQueries = parseUtil.parse(patternGeneratorResult.patternText) | 98 | val generatedQueries = parseUtil.parse(patternGeneratorResult.patternText) |
98 | val runtimeQueries = calclulateRuntimeQueries(patternGenerator, problem, emptySolution, typeAnalysisResult, | 99 | val runtimeQueries = calclulateRuntimeQueries(patternGenerator, problem, emptySolution, typeAnalysisResult, |
99 | patternGeneratorResult.constraint2MustPreconditionName, patternGeneratorResult.constraint2CurrentPreconditionName, | 100 | patternGeneratorResult.constraint2MustPreconditionName, |
100 | relationConstraints, generatedQueries) | 101 | patternGeneratorResult.constraint2CurrentPreconditionName, relationConstraints, |
102 | unitPropagationPatternGenerators, generatedQueries) | ||
101 | return runtimeQueries | 103 | return runtimeQueries |
102 | } | 104 | } |
103 | 105 | ||
@@ -109,14 +111,16 @@ class PatternProvider { | |||
109 | HashMap<PConstraint, String> mustUnitPropagationTrace, | 111 | HashMap<PConstraint, String> mustUnitPropagationTrace, |
110 | HashMap<PConstraint, String> currentUnitPropagationTrace, | 112 | HashMap<PConstraint, String> currentUnitPropagationTrace, |
111 | RelationConstraints relationConstraints, | 113 | RelationConstraints relationConstraints, |
114 | Collection<UnitPropagationPatternGenerator> unitPropagationPatternGenerators, | ||
112 | Map<String, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> queries | 115 | Map<String, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> queries |
113 | ) { | 116 | ) { |
114 | val Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> | 117 | val Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidWFQueries = patternGenerator. |
115 | invalidWFQueries = patternGenerator.invalidIndexer.getInvalidateByWfQueryNames(problem).mapValues[it.lookup(queries)] | 118 | invalidIndexer.getInvalidateByWfQueryNames(problem).mapValues[it.lookup(queries)] |
116 | val Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> | 119 | val Map<Relation, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWFQueries = patternGenerator. |
117 | unfinishedWFQueries = patternGenerator.unfinishedIndexer.getUnfinishedWFQueryNames(problem).mapValues[it.lookup(queries)] | 120 | unfinishedIndexer.getUnfinishedWFQueryNames(problem).mapValues[it.lookup(queries)] |
118 | 121 | ||
119 | val unfinishedMultiplicities = patternGenerator.unfinishedIndexer.getUnfinishedMultiplicityQueries(relationConstraints.multiplicityConstraints) | 122 | val unfinishedMultiplicities = patternGenerator.unfinishedIndexer.getUnfinishedMultiplicityQueries( |
123 | relationConstraints.multiplicityConstraints) | ||
120 | val multiplicityConstraintQueries = unfinishedMultiplicities.mapValues [ | 124 | val multiplicityConstraintQueries = unfinishedMultiplicities.mapValues [ |
121 | new UnifinishedMultiplicityQueries(existingMultiplicityQueryName?.lookup(queries), | 125 | new UnifinishedMultiplicityQueries(existingMultiplicityQueryName?.lookup(queries), |
122 | existingInverseMultiplicityQueryName?.lookup(queries)) | 126 | existingInverseMultiplicityQueryName?.lookup(queries)) |
@@ -124,16 +128,22 @@ class PatternProvider { | |||
124 | val hasElementInContainmentQuery = patternGenerator.typeRefinementGenerator.hasElementInContainmentName.lookup( | 128 | val hasElementInContainmentQuery = patternGenerator.typeRefinementGenerator.hasElementInContainmentName.lookup( |
125 | queries) | 129 | queries) |
126 | 130 | ||
127 | val Map<ObjectCreationPrecondition, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> | 131 | val Map<ObjectCreationPrecondition, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineObjectsQueries = patternGenerator. |
128 | refineObjectsQueries = patternGenerator.typeRefinementGenerator.getRefineObjectQueryNames(problem,emptySolution,typeAnalysisResult).mapValues[it.lookup(queries)] | 132 | typeRefinementGenerator.getRefineObjectQueryNames(problem, emptySolution, typeAnalysisResult).mapValues [ |
129 | val Map<? extends Type, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> | 133 | it.lookup(queries) |
130 | refineTypeQueries = patternGenerator.typeRefinementGenerator.getRefineTypeQueryNames(problem,emptySolution,typeAnalysisResult).mapValues[it.lookup(queries)] | 134 | ] |
131 | val Map<Pair<RelationDeclaration, Relation>, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> | 135 | val Map<? extends Type, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineTypeQueries = patternGenerator. |
132 | refineRelationQueries = patternGenerator.relationRefinementGenerator.getRefineRelationQueries(problem).mapValues[it.lookup(queries)] | 136 | typeRefinementGenerator.getRefineTypeQueryNames(problem, emptySolution, typeAnalysisResult).mapValues [ |
133 | val Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> | 137 | it.lookup(queries) |
134 | mustUnitPropagationPreconditionPatterns = mustUnitPropagationTrace.mapValues[it.lookup(queries)] | 138 | ] |
135 | val Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> | 139 | val Map<Pair<RelationDeclaration, Relation>, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> refineRelationQueries = patternGenerator. |
136 | currentUnitPropagationPreconditionPatterns = currentUnitPropagationTrace.mapValues[it.lookup(queries)] | 140 | relationRefinementGenerator.getRefineRelationQueries(problem).mapValues[it.lookup(queries)] |
141 | val Map<Pair<RelationDeclaration, Relation>, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> mustRelationPropagationQueries = patternGenerator. | ||
142 | relationRefinementGenerator.getMustPropagationQueries(problem, unitPropagationPatternGenerators).mapValues[it.lookup(queries)] | ||
143 | val Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> mustUnitPropagationPreconditionPatterns = mustUnitPropagationTrace. | ||
144 | mapValues[it.lookup(queries)] | ||
145 | val Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> currentUnitPropagationPreconditionPatterns = currentUnitPropagationTrace. | ||
146 | mapValues[it.lookup(queries)] | ||
137 | 147 | ||
138 | val modalRelationQueries = problem.relations.filter(RelationDefinition).toMap([it], [ relationDefinition | | 148 | val modalRelationQueries = problem.relations.filter(RelationDefinition).toMap([it], [ relationDefinition | |
139 | val indexer = patternGenerator.relationDefinitionIndexer | 149 | val indexer = patternGenerator.relationDefinitionIndexer |
@@ -143,7 +153,7 @@ class PatternProvider { | |||
143 | indexer.relationDefinitionName(relationDefinition, Modality.CURRENT).lookup(queries) | 153 | indexer.relationDefinitionName(relationDefinition, Modality.CURRENT).lookup(queries) |
144 | ) | 154 | ) |
145 | ]) | 155 | ]) |
146 | 156 | ||
147 | return new GeneratedPatterns( | 157 | return new GeneratedPatterns( |
148 | invalidWFQueries, | 158 | invalidWFQueries, |
149 | unfinishedWFQueries, | 159 | unfinishedWFQueries, |
@@ -152,6 +162,7 @@ class PatternProvider { | |||
152 | refineObjectsQueries, | 162 | refineObjectsQueries, |
153 | refineTypeQueries, | 163 | refineTypeQueries, |
154 | refineRelationQueries, | 164 | refineRelationQueries, |
165 | mustRelationPropagationQueries, | ||
155 | mustUnitPropagationPreconditionPatterns, | 166 | mustUnitPropagationPreconditionPatterns, |
156 | currentUnitPropagationPreconditionPatterns, | 167 | currentUnitPropagationPreconditionPatterns, |
157 | modalRelationQueries, | 168 | modalRelationQueries, |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDeclarationIndexer.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDeclarationIndexer.xtend index b4403979..23ba3cad 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDeclarationIndexer.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDeclarationIndexer.xtend | |||
@@ -1,10 +1,13 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns | 1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns |
2 | 2 | ||
3 | import com.google.common.collect.ImmutableMap | ||
4 | import com.google.common.collect.ImmutableSet | ||
3 | import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.UpperMultiplicityAssertion | 5 | import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.UpperMultiplicityAssertion |
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation | 6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation |
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration | 7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration |
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | 8 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem |
7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality | 9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality |
10 | import java.util.Collection | ||
8 | import java.util.HashMap | 11 | import java.util.HashMap |
9 | import java.util.List | 12 | import java.util.List |
10 | import java.util.Map | 13 | import java.util.Map |
@@ -14,41 +17,40 @@ import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | |||
14 | 17 | ||
15 | class RelationDeclarationIndexer { | 18 | class RelationDeclarationIndexer { |
16 | val PatternGenerator base; | 19 | val PatternGenerator base; |
17 | 20 | ||
18 | new(PatternGenerator base) { | 21 | new(PatternGenerator base) { |
19 | this.base = base | 22 | this.base = base |
20 | } | 23 | } |
21 | 24 | ||
22 | def generateRelationIndexers(LogicProblem problem, Iterable<RelationDeclaration> relations, Map<String,PQuery> fqn2PQuery) { | 25 | def generateRelationIndexers(LogicProblem problem, Iterable<RelationDeclaration> relations, |
26 | Iterable<UnitPropagationPatternGenerator> unitPropagationPatternGenerators, Map<String, PQuery> fqn2PQuery) { | ||
23 | val upperMultiplicities = new HashMap | 27 | val upperMultiplicities = new HashMap |
24 | problem.annotations.filter(UpperMultiplicityAssertion).forEach[ | 28 | problem.annotations.filter(UpperMultiplicityAssertion).forEach [ |
25 | upperMultiplicities.put(it.relation,it.upper) | 29 | upperMultiplicities.put(it.relation, it.upper) |
26 | ] | 30 | ] |
27 | 31 | val mustNotRelations = ImmutableMap.copyOf(unitPropagationPatternGenerators.flatMap[mustNotPatterns.entrySet]. | |
32 | groupBy[key].mapValues[ImmutableSet.copyOf(map[value])]) | ||
33 | |||
28 | return ''' | 34 | return ''' |
29 | «FOR relation : relations» | 35 | «FOR relation : relations» |
30 | «IF base.isDerived(relation)» | 36 | «IF base.isDerived(relation)» |
31 | «generateDerivedMustRelation(problem,relation,base.getDerivedDefinition(relation).patternFullyQualifiedName.lookup(fqn2PQuery))» | 37 | «generateDerivedMustRelation(problem,relation,base.getDerivedDefinition(relation).patternFullyQualifiedName.lookup(fqn2PQuery))» |
32 | «generateDerivedMayRelation(problem,relation,base.getDerivedDefinition(relation).patternFullyQualifiedName.lookup(fqn2PQuery))» | 38 | «generateDerivedMayRelation(problem,relation,base.getDerivedDefinition(relation).patternFullyQualifiedName.lookup(fqn2PQuery))» |
33 | «ELSE» | 39 | «ELSE» |
34 | «generateMustRelation(problem,relation)» | 40 | «generateMustRelation(problem, relation)» |
35 | «generateMayRelation(problem,relation,upperMultiplicities,base.getContainments(problem),base.getInverseRelations(problem),fqn2PQuery)» | 41 | «generateMayRelation(problem, relation, upperMultiplicities, base.getContainments(problem), base.getInverseRelations(problem), mustNotRelations.get(relation) ?: emptySet, fqn2PQuery)» |
36 | «ENDIF» | 42 | «ENDIF» |
37 | «ENDFOR» | 43 | «ENDFOR» |
38 | ''' | 44 | ''' |
39 | } | 45 | } |
40 | 46 | ||
41 | def private patternName(RelationDeclaration r, Modality modality) { | 47 | def private patternName(RelationDeclaration r, Modality modality) { |
42 | '''«modality.name.toLowerCase»InRelation«base.canonizeName(r.name)»''' | 48 | '''«modality.name.toLowerCase»InRelation«base.canonizeName(r.name)»''' |
43 | } | 49 | } |
44 | 50 | ||
45 | def referRelation( | 51 | def referRelation(RelationDeclaration referred, String sourceVariable, String targetVariable, |
46 | RelationDeclaration referred, | 52 | Modality modality) '''find «referred.patternName(modality)»(problem,interpretation,«sourceVariable»,«targetVariable»);''' |
47 | String sourceVariable, | 53 | |
48 | String targetVariable, | ||
49 | Modality modality) | ||
50 | '''find «referred.patternName(modality)»(problem,interpretation,«sourceVariable»,«targetVariable»);''' | ||
51 | |||
52 | def generateMustRelation(LogicProblem problem, RelationDeclaration relation) ''' | 54 | def generateMustRelation(LogicProblem problem, RelationDeclaration relation) ''' |
53 | /** | 55 | /** |
54 | * Matcher for detecting tuples t where []«relation.name»(source,target) | 56 | * Matcher for detecting tuples t where []«relation.name»(source,target) |
@@ -65,59 +67,64 @@ class RelationDeclarationIndexer { | |||
65 | BinaryElementRelationLink.param2(link,target); | 67 | BinaryElementRelationLink.param2(link,target); |
66 | } | 68 | } |
67 | ''' | 69 | ''' |
70 | |||
68 | def generateMayRelation(LogicProblem problem, RelationDeclaration relation, | 71 | def generateMayRelation(LogicProblem problem, RelationDeclaration relation, |
69 | Map<Relation, Integer> upperMultiplicities, | 72 | Map<Relation, Integer> upperMultiplicities, List<Relation> containments, |
70 | List<Relation> containments, | 73 | HashMap<Relation, Relation> inverseRelations, Collection<String> mustNotRelations, |
71 | HashMap<Relation, Relation> inverseRelations, | 74 | Map<String, PQuery> fqn2PQuery) { |
72 | Map<String,PQuery> fqn2PQuery) | ||
73 | { | ||
74 | return ''' | 75 | return ''' |
75 | /** | 76 | /** |
76 | * Matcher for detecting tuples t where <>«relation.name»(source,target) | 77 | * Matcher for detecting tuples t where <>«relation.name»(source,target) |
77 | */ | 78 | */ |
78 | private pattern «relation.patternName(Modality.MAY)»( | 79 | private pattern «relation.patternName(Modality.MAY)»( |
79 | problem:LogicProblem, interpretation:PartialInterpretation, | 80 | problem:LogicProblem, interpretation:PartialInterpretation, |
80 | source: DefinedElement, target:DefinedElement) | 81 | source: DefinedElement, target:DefinedElement) |
81 | { | 82 | { |
82 | find interpretation(problem,interpretation); | 83 | find interpretation(problem,interpretation); |
83 | // The two endpoint of the link have to exist | 84 | // The two endpoint of the link have to exist |
84 | find mayExist(problem, interpretation, source); | 85 | find mayExist(problem, interpretation, source); |
85 | find mayExist(problem, interpretation, target); | 86 | find mayExist(problem, interpretation, target); |
86 | // Type consistency | 87 | // Type consistency |
87 | «base.typeIndexer.referInstanceOfByReference(relation.parameters.get(0),Modality.MAY,"source")» | 88 | «base.typeIndexer.referInstanceOfByReference(relation.parameters.get(0),Modality.MAY,"source")» |
88 | «base.typeIndexer.referInstanceOfByReference(relation.parameters.get(1),Modality.MAY,"target")» | 89 | «base.typeIndexer.referInstanceOfByReference(relation.parameters.get(1),Modality.MAY,"target")» |
89 | «IF upperMultiplicities.containsKey(relation)» | 90 | «IF upperMultiplicities.containsKey(relation)» |
90 | // There are "numberOfExistingReferences" currently existing instances of the reference from the source, | 91 | // There are "numberOfExistingReferences" currently existing instances of the reference from the source, |
91 | // the upper bound of the multiplicity should be considered. | 92 | // the upper bound of the multiplicity should be considered. |
92 | numberOfExistingReferences == count «referRelation(relation,"source","_",Modality.MUST)» | 93 | numberOfExistingReferences == count «referRelation(relation,"source","_",Modality.MUST)» |
93 | numberOfExistingReferences != «upperMultiplicities.get(relation)»; | 94 | numberOfExistingReferences != «upperMultiplicities.get(relation)»; |
94 | «ENDIF» | 95 | «ENDIF» |
95 | «IF inverseRelations.containsKey(relation) && upperMultiplicities.containsKey(inverseRelations.get(relation))» | 96 | «IF inverseRelations.containsKey(relation) && upperMultiplicities.containsKey(inverseRelations.get(relation))» |
96 | // There are "numberOfExistingReferences" currently existing instances of the reference to the target, | 97 | // There are "numberOfExistingReferences" currently existing instances of the reference to the target, |
97 | // the upper bound of the opposite reference multiplicity should be considered. | 98 | // the upper bound of the opposite reference multiplicity should be considered. |
98 | numberOfExistingOppositeReferences == count «base.referRelation(inverseRelations.get(relation),"target","_",Modality.MUST,fqn2PQuery)» | 99 | numberOfExistingOppositeReferences == count «base.referRelation(inverseRelations.get(relation),"target","_",Modality.MUST,fqn2PQuery)» |
99 | numberOfExistingOppositeReferences != «upperMultiplicities.get(inverseRelations.get(relation))»; | 100 | numberOfExistingOppositeReferences != «upperMultiplicities.get(inverseRelations.get(relation))»; |
100 | «ENDIF» | 101 | «ENDIF» |
101 | «IF containments.contains(relation)» | 102 | «IF containments.contains(relation)» |
102 | // The reference is containment, then a new reference cannot be create if: | 103 | // The reference is containment, then a new reference cannot be create if: |
103 | // 1. Multiple parents | 104 | // 1. Multiple parents |
104 | neg «base.containmentIndexer.referMustContaint("_","target")» | 105 | neg «base.containmentIndexer.referMustContaint("_","target")» |
105 | // 2. Circle in the containment hierarchy | 106 | // 2. Circle in the containment hierarchy |
106 | neg «base.containmentIndexer.referTransitiveMustContains("target","source")» | 107 | neg «base.containmentIndexer.referTransitiveMustContains("target","source")» |
107 | «ENDIF» | 108 | «ENDIF» |
108 | «IF inverseRelations.containsKey(relation) && containments.contains(inverseRelations.get(relation))» | 109 | «IF inverseRelations.containsKey(relation) && containments.contains(inverseRelations.get(relation))» |
109 | // The eOpposite of the reference is containment, then a referene cannot be created if | 110 | // The eOpposite of the reference is containment, then a referene cannot be created if |
110 | // 1. Multiple parents | 111 | // 1. Multiple parents |
111 | neg «base.containmentIndexer.referMustContaint("source","_")» | 112 | neg «base.containmentIndexer.referMustContaint("source","_")» |
112 | // 2. Circle in the containment hierarchy | 113 | // 2. Circle in the containment hierarchy |
113 | neg «base.containmentIndexer.referTransitiveMustContains("source","target")» | 114 | neg «base.containmentIndexer.referTransitiveMustContains("source","target")» |
114 | «ENDIF» | 115 | «ENDIF» |
115 | } or { | 116 | «IF !mustNotRelations.empty» |
116 | «relation.referRelation("source","target",Modality.MUST)» | 117 | // ![] unit propagation relations |
117 | } | 118 | «FOR mustNotRelation : mustNotRelations» |
118 | ''' | 119 | neg find «mustNotRelation»(problem, interpretation, source, target); |
120 | «ENDFOR» | ||
121 | «ENDIF» | ||
122 | } or { | ||
123 | «relation.referRelation("source","target",Modality.MUST)» | ||
124 | } | ||
125 | ''' | ||
119 | } | 126 | } |
120 | 127 | ||
121 | def generateDerivedMustRelation(LogicProblem problem, RelationDeclaration relation, PQuery definition) ''' | 128 | def generateDerivedMustRelation(LogicProblem problem, RelationDeclaration relation, PQuery definition) ''' |
122 | /** | 129 | /** |
123 | * Matcher for detecting tuples t where []«relation.name»(source,target) | 130 | * Matcher for detecting tuples t where []«relation.name»(source,target) |
@@ -129,6 +136,7 @@ class RelationDeclarationIndexer { | |||
129 | «base.relationDefinitionIndexer.referPattern(definition,#["source","target"],Modality::MUST,true,false)» | 136 | «base.relationDefinitionIndexer.referPattern(definition,#["source","target"],Modality::MUST,true,false)» |
130 | } | 137 | } |
131 | ''' | 138 | ''' |
139 | |||
132 | def generateDerivedMayRelation(LogicProblem problem, RelationDeclaration relation, PQuery definition) ''' | 140 | def generateDerivedMayRelation(LogicProblem problem, RelationDeclaration relation, PQuery definition) ''' |
133 | /** | 141 | /** |
134 | * Matcher for detecting tuples t where []«relation.name»(source,target) | 142 | * Matcher for detecting tuples t where []«relation.name»(source,target) |
@@ -140,4 +148,4 @@ class RelationDeclarationIndexer { | |||
140 | «base.relationDefinitionIndexer.referPattern(definition,#["source","target"],Modality::MAY,true,false)» | 148 | «base.relationDefinitionIndexer.referPattern(definition,#["source","target"],Modality::MAY,true,false)» |
141 | } | 149 | } |
142 | ''' | 150 | ''' |
143 | } \ No newline at end of file | 151 | } |
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 783cd36b..6f5f2402 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 | |||
@@ -1,10 +1,17 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns | 1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns |
2 | 2 | ||
3 | import com.google.common.collect.ImmutableList | ||
4 | import com.google.common.collect.ImmutableMap | ||
5 | import com.google.common.collect.ImmutableSet | ||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation | 6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation |
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration | 7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration |
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | 8 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem |
6 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality | 9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality |
10 | import java.util.Collection | ||
7 | import java.util.LinkedList | 11 | import java.util.LinkedList |
12 | import java.util.Map | ||
13 | import java.util.Set | ||
14 | import org.eclipse.xtend2.lib.StringConcatenationClient | ||
8 | 15 | ||
9 | class RelationRefinementGenerator { | 16 | class RelationRefinementGenerator { |
10 | PatternGenerator base; | 17 | PatternGenerator base; |
@@ -13,53 +20,61 @@ class RelationRefinementGenerator { | |||
13 | this.base = base | 20 | this.base = base |
14 | } | 21 | } |
15 | 22 | ||
16 | def CharSequence generateRefineReference(LogicProblem p) ''' | 23 | def CharSequence generateRefineReference(LogicProblem p, |
17 | «FOR relationRefinement : this.getRelationRefinements(p)» | 24 | Collection<UnitPropagationPatternGenerator> unitPropagationPatternGenerators) { |
18 | pattern «relationRefinementQueryName(relationRefinement.key,relationRefinement.value)»( | 25 | val mustRelations = getMustRelations(unitPropagationPatternGenerators) |
19 | problem:LogicProblem, interpretation:PartialInterpretation, | 26 | |
20 | relationIterpretation:PartialRelationInterpretation«IF relationRefinement.value !== null», oppositeInterpretation:PartialRelationInterpretation«ENDIF», | 27 | ''' |
21 | from: DefinedElement, to: DefinedElement) | 28 | «FOR relationRefinement : this.getRelationRefinements(p)» |
22 | { | 29 | pattern «relationRefinementQueryName(relationRefinement.key,relationRefinement.value)»( |
23 | find interpretation(problem,interpretation); | 30 | problem:LogicProblem, interpretation:PartialInterpretation, |
24 | PartialInterpretation.partialrelationinterpretation(interpretation,relationIterpretation); | 31 | relationIterpretation:PartialRelationInterpretation«IF relationRefinement.value !== null», oppositeInterpretation:PartialRelationInterpretation«ENDIF», |
25 | PartialRelationInterpretation.interpretationOf.name(relationIterpretation,"«relationRefinement.key.name»"); | 32 | from: DefinedElement, to: DefinedElement) |
26 | «IF relationRefinement.value !== null» | 33 | { |
27 | PartialInterpretation.partialrelationinterpretation(interpretation,oppositeInterpretation); | 34 | find interpretation(problem,interpretation); |
28 | PartialRelationInterpretation.interpretationOf.name(oppositeInterpretation,"«relationRefinement.value.name»"); | 35 | PartialInterpretation.partialrelationinterpretation(interpretation,relationIterpretation); |
36 | PartialRelationInterpretation.interpretationOf.name(relationIterpretation,"«relationRefinement.key.name»"); | ||
37 | «IF relationRefinement.value !== null» | ||
38 | PartialInterpretation.partialrelationinterpretation(interpretation,oppositeInterpretation); | ||
39 | PartialRelationInterpretation.interpretationOf.name(oppositeInterpretation,"«relationRefinement.value.name»"); | ||
40 | «ENDIF» | ||
41 | find mustExist(problem, interpretation, from); | ||
42 | find mustExist(problem, interpretation, to); | ||
43 | «base.typeIndexer.referInstanceOfByReference(relationRefinement.key.parameters.get(0), Modality::MUST,"from")» | ||
44 | «base.typeIndexer.referInstanceOfByReference(relationRefinement.key.parameters.get(1), Modality::MUST,"to")» | ||
45 | «base.relationDeclarationIndexer.referRelation(relationRefinement.key,"from","to",Modality.MAY)» | ||
46 | neg «base.relationDeclarationIndexer.referRelation(relationRefinement.key,"from","to",Modality.MUST)» | ||
47 | } | ||
48 | |||
49 | «IF isMustPropagationQueryNeeded(relationRefinement.key, relationRefinement.value, mustRelations)» | ||
50 | pattern «mustPropagationQueryName(relationRefinement.key)»( | ||
51 | problem:LogicProblem, interpretation:PartialInterpretation, | ||
52 | relationIterpretation:PartialRelationInterpretation«IF relationRefinement.value !== null», oppositeInterpretation:PartialRelationInterpretation«ENDIF», | ||
53 | from: DefinedElement, to: DefinedElement) | ||
54 | «FOR body : getMustPropagationBodies(relationRefinement.key, relationRefinement.value, mustRelations) SEPARATOR " or "» | ||
55 | { | ||
56 | «referRefinementQuery(relationRefinement.key, relationRefinement.value, "relationIterpretation", "oppositeInterpretation", "from", "to")» | ||
57 | «body» | ||
58 | } | ||
59 | «ENDFOR» | ||
29 | «ENDIF» | 60 | «ENDIF» |
30 | find mustExist(problem, interpretation, from); | 61 | «ENDFOR» |
31 | find mustExist(problem, interpretation, to); | 62 | ''' |
32 | «base.typeIndexer.referInstanceOfByReference(relationRefinement.key.parameters.get(0), Modality::MUST,"from")» | 63 | } |
33 | «base.typeIndexer.referInstanceOfByReference(relationRefinement.key.parameters.get(1), Modality::MUST,"to")» | ||
34 | «base.relationDeclarationIndexer.referRelation(relationRefinement.key,"from","to",Modality.MAY)» | ||
35 | neg «base.relationDeclarationIndexer.referRelation(relationRefinement.key,"from","to",Modality.MUST)» | ||
36 | } | ||
37 | «ENDFOR» | ||
38 | ''' | ||
39 | 64 | ||
40 | def String relationRefinementQueryName(RelationDeclaration relation, Relation inverseRelation) { | 65 | def String relationRefinementQueryName(RelationDeclaration relation, Relation inverseRelation) { |
41 | '''«IF inverseRelation !== null»refineRelation_«base.canonizeName(relation.name)»_and_«base.canonizeName(inverseRelation.name)»«ELSE»refineRelation_«base.canonizeName(relation.name)»«ENDIF»''' | 66 | '''«IF inverseRelation !== null»refineRelation_«base.canonizeName(relation.name)»_and_«base.canonizeName(inverseRelation.name)»«ELSE»refineRelation_«base.canonizeName(relation.name)»«ENDIF»''' |
42 | } | 67 | } |
43 | 68 | ||
69 | def String mustPropagationQueryName(RelationDeclaration relation) { | ||
70 | '''mustPropagation_«base.canonizeName(relation.name)»''' | ||
71 | } | ||
72 | |||
44 | def referRefinementQuery(RelationDeclaration relation, Relation inverseRelation, String relInterpretationName, | 73 | def referRefinementQuery(RelationDeclaration relation, Relation inverseRelation, String relInterpretationName, |
45 | String inverseInterpretationName, String sourceName, | 74 | String inverseInterpretationName, String sourceName, |
46 | String targetName) '''find «this.relationRefinementQueryName(relation,inverseRelation)»(problem, interpretation, «relInterpretationName», «IF inverseRelation !== null»«inverseInterpretationName», «ENDIF»«sourceName», «targetName»);''' | 75 | String targetName) '''find «this.relationRefinementQueryName(relation,inverseRelation)»(problem, interpretation, «relInterpretationName», «IF inverseRelation !== null»«inverseInterpretationName», «ENDIF»«sourceName», «targetName»);''' |
47 | 76 | ||
48 | def getRefineRelationQueries(LogicProblem p) { | 77 | def getRefineRelationQueries(LogicProblem p) { |
49 | // val containmentRelations = p.containmentHierarchies.map[containmentRelations].flatten.toSet | ||
50 | // p.relations.filter(RelationDeclaration).filter[!containmentRelations.contains(it)].toInvertedMap['''refineRelation_«base.canonizeName(it.name)»'''] | ||
51 | /* | ||
52 | * val res = new LinkedHashMap | ||
53 | * for(relation: getRelationRefinements(p)) { | ||
54 | * if(inverseRelations.containsKey(relation)) { | ||
55 | * val name = '''refineRelation_«base.canonizeName(relation.name)»_and_«base.canonizeName(inverseRelations.get(relation).name)»''' | ||
56 | * res.put(relation -> inverseRelations.get(relation),name) | ||
57 | * } else { | ||
58 | * val name = '''refineRelation_«base.canonizeName(relation.name)»''' | ||
59 | * res.put(relation -> null,name) | ||
60 | * } | ||
61 | * } | ||
62 | return res*/ | ||
63 | getRelationRefinements(p).toInvertedMap[relationRefinementQueryName(it.key, it.value)] | 78 | getRelationRefinements(p).toInvertedMap[relationRefinementQueryName(it.key, it.value)] |
64 | } | 79 | } |
65 | 80 | ||
@@ -83,4 +98,54 @@ class RelationRefinementGenerator { | |||
83 | } | 98 | } |
84 | return list | 99 | return list |
85 | } | 100 | } |
101 | |||
102 | def getMustPropagationQueries(LogicProblem p, | ||
103 | Collection<UnitPropagationPatternGenerator> unitPropagationPatternGenerators) { | ||
104 | val refinements = getRelationRefinements(p) | ||
105 | val mustRelations = getMustRelations(unitPropagationPatternGenerators) | ||
106 | refinements.filter[isMustPropagationQueryNeeded(key, value, mustRelations)].toInvertedMap [ | ||
107 | mustPropagationQueryName(key) | ||
108 | ] | ||
109 | } | ||
110 | |||
111 | private def getMustRelations(Collection<UnitPropagationPatternGenerator> unitPropagationPatternGenerators) { | ||
112 | ImmutableMap.copyOf(unitPropagationPatternGenerators.flatMap[mustPatterns.entrySet].groupBy[key].mapValues [ | ||
113 | ImmutableSet.copyOf(map[value]) | ||
114 | ]) | ||
115 | } | ||
116 | |||
117 | private def isMustPropagationQueryNeeded(Relation relation, Relation inverseRelation, | ||
118 | Map<Relation, ? extends Set<String>> mustRelations) { | ||
119 | val mustSet = mustRelations.get(relation) | ||
120 | if (mustSet !== null && !mustSet.empty) { | ||
121 | return true | ||
122 | } | ||
123 | if (inverseRelation !== null) { | ||
124 | val inverseMustSet = mustRelations.get(inverseRelation) | ||
125 | if (inverseMustSet !== null && !inverseMustSet.empty) { | ||
126 | return true | ||
127 | } | ||
128 | } | ||
129 | false | ||
130 | } | ||
131 | |||
132 | private def getMustPropagationBodies(Relation relation, Relation inverseRelation, | ||
133 | Map<Relation, ? extends Set<String>> mustRelations) { | ||
134 | val builder = ImmutableList.<StringConcatenationClient>builder() | ||
135 | val mustSet = mustRelations.get(relation) | ||
136 | if (mustSet !== null) { | ||
137 | for (refinementQuery : mustSet) { | ||
138 | builder.add('''find «refinementQuery»(problem, interpretation, from, to);''') | ||
139 | } | ||
140 | } | ||
141 | if (inverseRelation !== null && inverseRelation != relation) { | ||
142 | val inverseMustSet = mustRelations.get(inverseRelation) | ||
143 | if (inverseMustSet !== null) { | ||
144 | for (refinementQuery : inverseMustSet) { | ||
145 | builder.add('''find «refinementQuery»(problem, interpretation, to, from);''') | ||
146 | } | ||
147 | } | ||
148 | } | ||
149 | builder.build | ||
150 | } | ||
86 | } | 151 | } |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend index f7fe97a3..dca10baf 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend | |||
@@ -1,5 +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 com.google.common.collect.ImmutableList | ||
3 | import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.InverseRelationAssertion | 4 | 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.ecore2logic.ecore2logicannotations.LowerMultiplicityAssertion |
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference | 6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference |
@@ -29,12 +30,14 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.par | |||
29 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialinterpretationFactory | 30 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialinterpretationFactory |
30 | import java.lang.reflect.Field | 31 | import java.lang.reflect.Field |
31 | import java.util.HashMap | 32 | import java.util.HashMap |
33 | import java.util.Iterator | ||
32 | import java.util.LinkedHashMap | 34 | import java.util.LinkedHashMap |
33 | import java.util.LinkedList | 35 | import java.util.LinkedList |
34 | import java.util.List | 36 | import java.util.List |
35 | import java.util.Map | 37 | import java.util.Map |
36 | import org.eclipse.viatra.query.runtime.api.AdvancedViatraQueryEngine | 38 | import org.eclipse.viatra.query.runtime.api.AdvancedViatraQueryEngine |
37 | import org.eclipse.viatra.query.runtime.api.GenericPatternMatch | 39 | import org.eclipse.viatra.query.runtime.api.GenericPatternMatch |
40 | import org.eclipse.viatra.query.runtime.api.IPatternMatch | ||
38 | import org.eclipse.viatra.query.runtime.api.IQuerySpecification | 41 | import org.eclipse.viatra.query.runtime.api.IQuerySpecification |
39 | import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine | 42 | import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine |
40 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher | 43 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher |
@@ -43,6 +46,7 @@ import org.eclipse.viatra.query.runtime.rete.matcher.ReteBackendFactory | |||
43 | import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRule | 46 | import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRule |
44 | import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRuleFactory | 47 | import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRuleFactory |
45 | import org.eclipse.xtend.lib.annotations.Data | 48 | import org.eclipse.xtend.lib.annotations.Data |
49 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor | ||
46 | import org.eclipse.xtext.xbase.lib.Functions.Function0 | 50 | import org.eclipse.xtext.xbase.lib.Functions.Function0 |
47 | 51 | ||
48 | class RefinementRuleProvider { | 52 | class RefinementRuleProvider { |
@@ -50,57 +54,55 @@ class RefinementRuleProvider { | |||
50 | val extension PartialinterpretationFactory factory2 = PartialinterpretationFactory.eINSTANCE | 54 | val extension PartialinterpretationFactory factory2 = PartialinterpretationFactory.eINSTANCE |
51 | val extension LogiclanguageFactory factory3 = LogiclanguageFactory.eINSTANCE | 55 | val extension LogiclanguageFactory factory3 = LogiclanguageFactory.eINSTANCE |
52 | 56 | ||
53 | var AdvancedViatraQueryEngine queryEngine | ||
54 | var Field delayMessageDelivery | ||
55 | |||
56 | def canonizeName(String name) { | 57 | def canonizeName(String name) { |
57 | return name.replace(' ', '_') | 58 | return name.replace(' ', '_') |
58 | } | 59 | } |
59 | 60 | ||
61 | def createUnitPrulePropagator(LogicProblem p, PartialInterpretation i, GeneratedPatterns patterns, | ||
62 | ScopePropagator scopePropagator, ModelGenerationStatistics statistics) { | ||
63 | new UnitRulePropagator(p, i, this, scopePropagator, patterns.mustRelationPropagationQueries, statistics) | ||
64 | } | ||
65 | |||
60 | def LinkedHashMap<ObjectCreationPrecondition, BatchTransformationRule<GenericPatternMatch, ViatraQueryMatcher<GenericPatternMatch>>> createObjectRefinementRules( | 66 | def LinkedHashMap<ObjectCreationPrecondition, BatchTransformationRule<GenericPatternMatch, ViatraQueryMatcher<GenericPatternMatch>>> createObjectRefinementRules( |
61 | LogicProblem p, | 67 | LogicProblem p, |
62 | PartialInterpretation i, | 68 | PartialInterpretation i, |
63 | GeneratedPatterns patterns, | 69 | GeneratedPatterns patterns, |
64 | ScopePropagator scopePropagator, | 70 | UnitRulePropagator unitRulePropagator, |
65 | boolean nameNewElement, | 71 | boolean nameNewElement, |
66 | ModelGenerationStatistics statistics | 72 | ModelGenerationStatistics statistics |
67 | ) { | 73 | ) { |
68 | val res = new LinkedHashMap | 74 | val res = new LinkedHashMap |
69 | val recursiveObjectCreation = recursiveObjectCreation(p, i) | 75 | val recursiveObjectCreation = recursiveObjectCreation(p, i) |
70 | queryEngine = ViatraQueryEngine.on(new EMFScope(i)) as AdvancedViatraQueryEngine | ||
71 | delayMessageDelivery = queryEngine.class.getDeclaredField("delayMessageDelivery") | ||
72 | delayMessageDelivery.accessible = true | ||
73 | for (LHSEntry : patterns.refineObjectQueries.entrySet) { | 76 | for (LHSEntry : patterns.refineObjectQueries.entrySet) { |
74 | val containmentRelation = LHSEntry.key.containmentRelation | 77 | val containmentRelation = LHSEntry.key.containmentRelation |
75 | val inverseRelation = LHSEntry.key.inverseContainment | 78 | val inverseRelation = LHSEntry.key.inverseContainment |
76 | val type = LHSEntry.key.newType | 79 | val type = LHSEntry.key.newType |
77 | val lhs = LHSEntry.value as IQuerySpecification<ViatraQueryMatcher<GenericPatternMatch>> | 80 | val lhs = LHSEntry.value as IQuerySpecification<ViatraQueryMatcher<GenericPatternMatch>> |
78 | val rule = createObjectCreationRule(p, containmentRelation, inverseRelation, type, | 81 | val rule = createObjectCreationRule(p, containmentRelation, inverseRelation, type, |
79 | recursiveObjectCreation.get(type), lhs, nameNewElement, scopePropagator, statistics) | 82 | recursiveObjectCreation.get(type), lhs, nameNewElement, unitRulePropagator, statistics) |
80 | res.put(LHSEntry.key, rule) | 83 | res.put(LHSEntry.key, rule) |
81 | } | 84 | } |
82 | return res | 85 | return res |
83 | } | 86 | } |
84 | 87 | ||
85 | def private createObjectCreationRule(LogicProblem p, Relation containmentRelation, Relation inverseRelation, | 88 | def private createObjectCreationRule(LogicProblem p, Relation containmentRelation, Relation inverseRelation, |
86 | Type type, List<ObjectCreationInterpretationData> recursiceObjectCreations, | 89 | Type type, List<ObjectCreationInterpretationData> recursiveObjectCreations, |
87 | IQuerySpecification<ViatraQueryMatcher<GenericPatternMatch>> lhs, boolean nameNewElement, | 90 | IQuerySpecification<ViatraQueryMatcher<GenericPatternMatch>> lhs, boolean nameNewElement, |
88 | ScopePropagator scopePropagator, ModelGenerationStatistics statistics) { | 91 | UnitRulePropagator unitRulePropagator, ModelGenerationStatistics statistics) { |
89 | val name = '''addObject_«type.name.canonizeName»«IF containmentRelation!==null»_by_«containmentRelation.name.canonizeName»«ENDIF»''' | 92 | val name = '''addObject_«type.name.canonizeName»«IF containmentRelation!==null»_by_«containmentRelation.name.canonizeName»«ENDIF»''' |
90 | val ruleBuilder = factory.createRule(lhs).name(name) | 93 | val ruleBuilder = factory.createRule(lhs).name(name) |
91 | if (containmentRelation !== null) { | 94 | if (containmentRelation !== null) { |
92 | if (inverseRelation !== null) { | 95 | if (inverseRelation !== null) { |
93 | ruleBuilder.action [ match | | 96 | ruleBuilder.action [ match | |
94 | statistics.incrementTransformationCount | 97 | statistics.incrementTransformationCount |
95 | // println(name) | 98 | // println(name) |
99 | val startTime = System.nanoTime | ||
96 | // val problem = match.get(0) as LogicProblem | 100 | // val problem = match.get(0) as LogicProblem |
97 | val interpretation = match.get(1) as PartialInterpretation | 101 | val interpretation = match.get(1) as PartialInterpretation |
98 | val relationInterpretation = match.get(2) as PartialRelationInterpretation | 102 | val relationInterpretation = match.get(2) as PartialRelationInterpretation |
99 | val inverseRelationInterpretation = match.get(3) as PartialRelationInterpretation | 103 | val inverseRelationInterpretation = match.get(3) as PartialRelationInterpretation |
100 | val typeInterpretation = match.get(4) as PartialComplexTypeInterpretation | 104 | val typeInterpretation = match.get(4) as PartialComplexTypeInterpretation |
101 | val container = match.get(5) as DefinedElement | 105 | val container = match.get(5) as DefinedElement |
102 | |||
103 | val startTime = System.nanoTime | ||
104 | createObjectActionWithContainmentAndInverse( | 106 | createObjectActionWithContainmentAndInverse( |
105 | nameNewElement, | 107 | nameNewElement, |
106 | interpretation, | 108 | interpretation, |
@@ -109,29 +111,24 @@ class RefinementRuleProvider { | |||
109 | relationInterpretation, | 111 | relationInterpretation, |
110 | inverseRelationInterpretation, | 112 | inverseRelationInterpretation, |
111 | [createDefinedElement], | 113 | [createDefinedElement], |
112 | recursiceObjectCreations, | 114 | recursiveObjectCreations, |
113 | scopePropagator | 115 | unitRulePropagator |
114 | ) | 116 | ) |
115 | statistics.addExecutionTime(System.nanoTime - startTime) | 117 | statistics.addExecutionTime(System.nanoTime - startTime) |
116 | 118 | ||
117 | flushQueryEngine(scopePropagator) | 119 | unitRulePropagator.propagate |
118 | |||
119 | // Scope propagation | ||
120 | val propagatorStartTime = System.nanoTime | ||
121 | scopePropagator.propagateAllScopeConstraints() | ||
122 | statistics.addScopePropagationTime(System.nanoTime - propagatorStartTime) | ||
123 | ] | 120 | ] |
124 | } else { | 121 | } else { |
125 | ruleBuilder.action [ match | | 122 | ruleBuilder.action [ match | |
126 | statistics.incrementTransformationCount | 123 | statistics.incrementTransformationCount |
127 | // println(name) | 124 | // println(name) |
125 | val startTime = System.nanoTime | ||
128 | // val problem = match.get(0) as LogicProblem | 126 | // val problem = match.get(0) as LogicProblem |
129 | val interpretation = match.get(1) as PartialInterpretation | 127 | val interpretation = match.get(1) as PartialInterpretation |
130 | val relationInterpretation = match.get(2) as PartialRelationInterpretation | 128 | val relationInterpretation = match.get(2) as PartialRelationInterpretation |
131 | val typeInterpretation = match.get(3) as PartialComplexTypeInterpretation | 129 | val typeInterpretation = match.get(3) as PartialComplexTypeInterpretation |
132 | val container = match.get(4) as DefinedElement | 130 | val container = match.get(4) as DefinedElement |
133 | 131 | ||
134 | val startTime = System.nanoTime | ||
135 | createObjectActionWithContainment( | 132 | createObjectActionWithContainment( |
136 | nameNewElement, | 133 | nameNewElement, |
137 | interpretation, | 134 | interpretation, |
@@ -139,44 +136,34 @@ class RefinementRuleProvider { | |||
139 | container, | 136 | container, |
140 | relationInterpretation, | 137 | relationInterpretation, |
141 | [createDefinedElement], | 138 | [createDefinedElement], |
142 | recursiceObjectCreations, | 139 | recursiveObjectCreations, |
143 | scopePropagator | 140 | unitRulePropagator |
144 | ) | 141 | ) |
145 | statistics.addExecutionTime(System.nanoTime - startTime) | 142 | statistics.addExecutionTime(System.nanoTime - startTime) |
146 | 143 | ||
147 | flushQueryEngine(scopePropagator) | 144 | unitRulePropagator.propagate |
148 | |||
149 | // Scope propagation | ||
150 | val propagatorStartTime = System.nanoTime | ||
151 | scopePropagator.propagateAllScopeConstraints() | ||
152 | statistics.addScopePropagationTime(System.nanoTime - propagatorStartTime) | ||
153 | ] | 145 | ] |
154 | } | 146 | } |
155 | } else { | 147 | } else { |
156 | ruleBuilder.action [ match | | 148 | ruleBuilder.action [ match | |
157 | statistics.incrementTransformationCount | 149 | statistics.incrementTransformationCount |
158 | // println(name) | 150 | // println(name) |
151 | val startTime = System.nanoTime | ||
159 | // val problem = match.get(0) as LogicProblem | 152 | // val problem = match.get(0) as LogicProblem |
160 | val interpretation = match.get(1) as PartialInterpretation | 153 | val interpretation = match.get(1) as PartialInterpretation |
161 | val typeInterpretation = match.get(2) as PartialComplexTypeInterpretation | 154 | val typeInterpretation = match.get(2) as PartialComplexTypeInterpretation |
162 | 155 | ||
163 | val startTime = System.nanoTime | ||
164 | createObjectAction( | 156 | createObjectAction( |
165 | nameNewElement, | 157 | nameNewElement, |
166 | interpretation, | 158 | interpretation, |
167 | typeInterpretation, | 159 | typeInterpretation, |
168 | [createDefinedElement], | 160 | [createDefinedElement], |
169 | recursiceObjectCreations, | 161 | recursiveObjectCreations, |
170 | scopePropagator | 162 | unitRulePropagator |
171 | ) | 163 | ) |
172 | statistics.addExecutionTime(System.nanoTime - startTime) | 164 | statistics.addExecutionTime(System.nanoTime - startTime) |
173 | 165 | ||
174 | flushQueryEngine(scopePropagator) | 166 | unitRulePropagator.propagate |
175 | |||
176 | // Scope propagation | ||
177 | val propagatorStartTime = System.nanoTime | ||
178 | scopePropagator.propagateAllScopeConstraints() | ||
179 | statistics.addScopePropagationTime(System.nanoTime - propagatorStartTime) | ||
180 | ] | 167 | ] |
181 | } | 168 | } |
182 | return ruleBuilder.build | 169 | return ruleBuilder.build |
@@ -342,14 +329,14 @@ class RefinementRuleProvider { | |||
342 | [createStringElement] | 329 | [createStringElement] |
343 | } | 330 | } |
344 | 331 | ||
345 | def createRelationRefinementRules(GeneratedPatterns patterns, ScopePropagator scopePropagator, | 332 | def createRelationRefinementRules(GeneratedPatterns patterns, UnitRulePropagator unitRulePropagator, |
346 | ModelGenerationStatistics statistics) { | 333 | ModelGenerationStatistics statistics) { |
347 | val res = new LinkedHashMap | 334 | val res = new LinkedHashMap |
348 | for (LHSEntry : patterns.refinerelationQueries.entrySet) { | 335 | for (LHSEntry : patterns.refineRelationQueries.entrySet) { |
349 | val declaration = LHSEntry.key.key | 336 | val declaration = LHSEntry.key.key |
350 | val inverseReference = LHSEntry.key.value | 337 | val inverseReference = LHSEntry.key.value |
351 | val lhs = LHSEntry.value as IQuerySpecification<ViatraQueryMatcher<GenericPatternMatch>> | 338 | val lhs = LHSEntry.value as IQuerySpecification<ViatraQueryMatcher<GenericPatternMatch>> |
352 | val rule = createRelationRefinementRule(declaration, inverseReference, lhs, scopePropagator, statistics) | 339 | val rule = createRelationRefinementRule(declaration, inverseReference, lhs, unitRulePropagator, statistics) |
353 | res.put(LHSEntry.key, rule) | 340 | res.put(LHSEntry.key, rule) |
354 | } | 341 | } |
355 | return res | 342 | return res |
@@ -357,59 +344,29 @@ class RefinementRuleProvider { | |||
357 | 344 | ||
358 | def private BatchTransformationRule<GenericPatternMatch, ViatraQueryMatcher<GenericPatternMatch>> createRelationRefinementRule( | 345 | def private BatchTransformationRule<GenericPatternMatch, ViatraQueryMatcher<GenericPatternMatch>> createRelationRefinementRule( |
359 | RelationDeclaration declaration, Relation inverseRelation, | 346 | RelationDeclaration declaration, Relation inverseRelation, |
360 | IQuerySpecification<ViatraQueryMatcher<GenericPatternMatch>> lhs, ScopePropagator scopePropagator, | 347 | IQuerySpecification<ViatraQueryMatcher<GenericPatternMatch>> lhs, UnitRulePropagator unitRulePropagator, |
361 | ModelGenerationStatistics statistics) { | 348 | ModelGenerationStatistics statistics) { |
362 | val name = '''addRelation_«declaration.name.canonizeName»«IF inverseRelation !== null»_and_«inverseRelation.name.canonizeName»«ENDIF»''' | 349 | val name = '''addRelation_«declaration.name.canonizeName»«IF inverseRelation !== null»_and_«inverseRelation.name.canonizeName»«ENDIF»''' |
363 | val ruleBuilder = factory.createRule(lhs).name(name) | 350 | val ruleBuilder = factory.createRule(lhs).name(name) |
364 | if (inverseRelation === null) { | 351 | if (inverseRelation === null) { |
365 | ruleBuilder.action [ match | | 352 | ruleBuilder.action [ match | |
366 | statistics.incrementTransformationCount | 353 | statistics.incrementTransformationCount |
367 | |||
368 | // println(name) | 354 | // println(name) |
369 | // val problem = match.get(0) as LogicProblem | 355 | val startTime = System.nanoTime |
370 | // val interpretation = match.get(1) as PartialInterpretation | 356 | createRelationLinkAction(match, unitRulePropagator) |
371 | val relationInterpretation = match.get(2) as PartialRelationInterpretation | 357 | statistics.addExecutionTime(System.nanoTime - startTime) |
372 | val src = match.get(3) as DefinedElement | ||
373 | val trg = match.get(4) as DefinedElement | ||
374 | |||
375 | queryEngine.delayUpdatePropagation [ | ||
376 | val startTime = System.nanoTime | ||
377 | createRelationLinkAction(src, trg, relationInterpretation) | ||
378 | statistics.addExecutionTime(System.nanoTime - startTime) | ||
379 | ] | ||
380 | 358 | ||
381 | // Scope propagation | 359 | unitRulePropagator.propagate |
382 | if (scopePropagator.isPropagationNeededAfterAdditionToRelation(declaration)) { | ||
383 | queryEngine.delayUpdatePropagation [ | ||
384 | val propagatorStartTime = System.nanoTime | ||
385 | scopePropagator.propagateAllScopeConstraints() | ||
386 | statistics.addScopePropagationTime(System.nanoTime - propagatorStartTime) | ||
387 | ] | ||
388 | } | ||
389 | ] | 360 | ] |
390 | } else { | 361 | } else { |
391 | ruleBuilder.action [ match | | 362 | ruleBuilder.action [ match | |
392 | statistics.incrementTransformationCount | 363 | statistics.incrementTransformationCount |
393 | // println(name) | 364 | // println(name) |
394 | // val problem = match.get(0) as LogicProblem | ||
395 | // val interpretation = match.get(1) as PartialInterpretation | ||
396 | val relationInterpretation = match.get(2) as PartialRelationInterpretation | ||
397 | val inverseInterpretation = match.get(3) as PartialRelationInterpretation | ||
398 | val src = match.get(4) as DefinedElement | ||
399 | val trg = match.get(5) as DefinedElement | ||
400 | |||
401 | val startTime = System.nanoTime | 365 | val startTime = System.nanoTime |
402 | createRelationLinkWithInverse(src, trg, relationInterpretation, inverseInterpretation) | 366 | createRelationLinkWithInverse(match, unitRulePropagator) |
403 | statistics.addExecutionTime(System.nanoTime - startTime) | 367 | statistics.addExecutionTime(System.nanoTime - startTime) |
404 | 368 | ||
405 | // Scope propagation | 369 | unitRulePropagator.propagate |
406 | if (scopePropagator.isPropagationNeededAfterAdditionToRelation(declaration)) { | ||
407 | flushQueryEngine(scopePropagator) | ||
408 | |||
409 | val propagatorStartTime = System.nanoTime | ||
410 | scopePropagator.propagateAllScopeConstraints() | ||
411 | statistics.addScopePropagationTime(System.nanoTime - propagatorStartTime) | ||
412 | } | ||
413 | ] | 370 | ] |
414 | } | 371 | } |
415 | 372 | ||
@@ -420,7 +377,7 @@ class RefinementRuleProvider { | |||
420 | // Actions | 377 | // Actions |
421 | // /////////////////////// | 378 | // /////////////////////// |
422 | protected def void createObjectAction(boolean nameNewElement, ObjectCreationInterpretationData data, | 379 | protected def void createObjectAction(boolean nameNewElement, ObjectCreationInterpretationData data, |
423 | DefinedElement container, ScopePropagator scopePropagator) { | 380 | DefinedElement container, UnitRulePropagator unitRulePropagator) { |
424 | if (data.containerInterpretation !== null) { | 381 | if (data.containerInterpretation !== null) { |
425 | if (data.containerInverseInterpretation !== null) { | 382 | if (data.containerInverseInterpretation !== null) { |
426 | createObjectActionWithContainmentAndInverse( | 383 | createObjectActionWithContainmentAndInverse( |
@@ -432,7 +389,7 @@ class RefinementRuleProvider { | |||
432 | data.containerInverseInterpretation, | 389 | data.containerInverseInterpretation, |
433 | data.constructor, | 390 | data.constructor, |
434 | data.recursiveConstructors, | 391 | data.recursiveConstructors, |
435 | scopePropagator | 392 | unitRulePropagator |
436 | ) | 393 | ) |
437 | } else { | 394 | } else { |
438 | createObjectActionWithContainment( | 395 | createObjectActionWithContainment( |
@@ -443,7 +400,7 @@ class RefinementRuleProvider { | |||
443 | data.containerInterpretation, | 400 | data.containerInterpretation, |
444 | data.constructor, | 401 | data.constructor, |
445 | data.recursiveConstructors, | 402 | data.recursiveConstructors, |
446 | scopePropagator | 403 | unitRulePropagator |
447 | ) | 404 | ) |
448 | } | 405 | } |
449 | } else { | 406 | } else { |
@@ -453,7 +410,7 @@ class RefinementRuleProvider { | |||
453 | data.typeInterpretation, | 410 | data.typeInterpretation, |
454 | data.constructor, | 411 | data.constructor, |
455 | data.recursiveConstructors, | 412 | data.recursiveConstructors, |
456 | scopePropagator | 413 | unitRulePropagator |
457 | ) | 414 | ) |
458 | } | 415 | } |
459 | 416 | ||
@@ -468,7 +425,7 @@ class RefinementRuleProvider { | |||
468 | PartialRelationInterpretation inverseRelationInterpretation, | 425 | PartialRelationInterpretation inverseRelationInterpretation, |
469 | Function0<DefinedElement> constructor, | 426 | Function0<DefinedElement> constructor, |
470 | List<ObjectCreationInterpretationData> recursiceObjectCreations, | 427 | List<ObjectCreationInterpretationData> recursiceObjectCreations, |
471 | ScopePropagator scopePropagator | 428 | UnitRulePropagator unitRulePropagator |
472 | ) { | 429 | ) { |
473 | val newElement = constructor.apply | 430 | val newElement = constructor.apply |
474 | if (nameNewElement) { | 431 | if (nameNewElement) { |
@@ -488,14 +445,16 @@ class RefinementRuleProvider { | |||
488 | inverseRelationInterpretation.relationlinks += newLink2 | 445 | inverseRelationInterpretation.relationlinks += newLink2 |
489 | 446 | ||
490 | // Scope propagation | 447 | // Scope propagation |
491 | scopePropagator.decrementTypeScope(typeInterpretation) | 448 | unitRulePropagator.decrementTypeScope(typeInterpretation) |
449 | unitRulePropagator.addedToRelation(relationInterpretation.interpretationOf) | ||
450 | unitRulePropagator.addedToRelation(inverseRelationInterpretation.interpretationOf) | ||
492 | 451 | ||
493 | // Existence | 452 | // Existence |
494 | interpretation.newElements += newElement | 453 | interpretation.newElements += newElement |
495 | 454 | ||
496 | // Do recursive object creation | 455 | // Do recursive object creation |
497 | for (newConstructor : recursiceObjectCreations) { | 456 | for (newConstructor : recursiceObjectCreations) { |
498 | createObjectAction(nameNewElement, newConstructor, newElement, scopePropagator) | 457 | createObjectAction(nameNewElement, newConstructor, newElement, unitRulePropagator) |
499 | } | 458 | } |
500 | 459 | ||
501 | return newElement | 460 | return newElement |
@@ -509,7 +468,7 @@ class RefinementRuleProvider { | |||
509 | PartialRelationInterpretation relationInterpretation, | 468 | PartialRelationInterpretation relationInterpretation, |
510 | Function0<DefinedElement> constructor, | 469 | Function0<DefinedElement> constructor, |
511 | List<ObjectCreationInterpretationData> recursiceObjectCreations, | 470 | List<ObjectCreationInterpretationData> recursiceObjectCreations, |
512 | ScopePropagator scopePropagator | 471 | UnitRulePropagator unitRulePropagator |
513 | ) { | 472 | ) { |
514 | val newElement = constructor.apply | 473 | val newElement = constructor.apply |
515 | if (nameNewElement) { | 474 | if (nameNewElement) { |
@@ -524,16 +483,17 @@ class RefinementRuleProvider { | |||
524 | // ContainmentRelation | 483 | // ContainmentRelation |
525 | val newLink = factory2.createBinaryElementRelationLink => [it.param1 = container it.param2 = newElement] | 484 | val newLink = factory2.createBinaryElementRelationLink => [it.param1 = container it.param2 = newElement] |
526 | relationInterpretation.relationlinks += newLink | 485 | relationInterpretation.relationlinks += newLink |
486 | unitRulePropagator.addedToRelation(relationInterpretation.interpretationOf) | ||
527 | 487 | ||
528 | // Scope propagation | 488 | // Scope propagation |
529 | scopePropagator.decrementTypeScope(typeInterpretation) | 489 | unitRulePropagator.decrementTypeScope(typeInterpretation) |
530 | 490 | ||
531 | // Existence | 491 | // Existence |
532 | interpretation.newElements += newElement | 492 | interpretation.newElements += newElement |
533 | 493 | ||
534 | // Do recursive object creation | 494 | // Do recursive object creation |
535 | for (newConstructor : recursiceObjectCreations) { | 495 | for (newConstructor : recursiceObjectCreations) { |
536 | createObjectAction(nameNewElement, newConstructor, newElement, scopePropagator) | 496 | createObjectAction(nameNewElement, newConstructor, newElement, unitRulePropagator) |
537 | } | 497 | } |
538 | 498 | ||
539 | return newElement | 499 | return newElement |
@@ -541,7 +501,7 @@ class RefinementRuleProvider { | |||
541 | 501 | ||
542 | protected def createObjectAction(boolean nameNewElement, PartialInterpretation interpretation, | 502 | protected def createObjectAction(boolean nameNewElement, PartialInterpretation interpretation, |
543 | PartialTypeInterpratation typeInterpretation, Function0<DefinedElement> constructor, | 503 | PartialTypeInterpratation typeInterpretation, Function0<DefinedElement> constructor, |
544 | List<ObjectCreationInterpretationData> recursiceObjectCreations, ScopePropagator scopePropagator) { | 504 | List<ObjectCreationInterpretationData> recursiceObjectCreations, UnitRulePropagator unitRulePropagator) { |
545 | val newElement = constructor.apply | 505 | val newElement = constructor.apply |
546 | if (nameNewElement) { | 506 | if (nameNewElement) { |
547 | newElement.name = '''new «interpretation.newElements.size»''' | 507 | newElement.name = '''new «interpretation.newElements.size»''' |
@@ -554,38 +514,220 @@ class RefinementRuleProvider { | |||
554 | } | 514 | } |
555 | 515 | ||
556 | // Scope propagation | 516 | // Scope propagation |
557 | scopePropagator.decrementTypeScope(typeInterpretation) | 517 | unitRulePropagator.decrementTypeScope(typeInterpretation) |
558 | 518 | ||
559 | // Existence | 519 | // Existence |
560 | interpretation.newElements += newElement | 520 | interpretation.newElements += newElement |
561 | 521 | ||
562 | // Do recursive object creation | 522 | // Do recursive object creation |
563 | for (newConstructor : recursiceObjectCreations) { | 523 | for (newConstructor : recursiceObjectCreations) { |
564 | createObjectAction(nameNewElement, newConstructor, newElement, scopePropagator) | 524 | createObjectAction(nameNewElement, newConstructor, newElement, unitRulePropagator) |
565 | } | 525 | } |
566 | 526 | ||
567 | return newElement | 527 | return newElement |
568 | } | 528 | } |
569 | 529 | ||
570 | protected def boolean createRelationLinkAction(DefinedElement src, DefinedElement trg, | 530 | protected def createRelationLinkAction(IPatternMatch match, UnitRulePropagator unitRulePropagator) { |
571 | PartialRelationInterpretation relationInterpretation) { | 531 | // val problem = match.get(0) as LogicProblem |
532 | // val interpretation = match.get(1) as PartialInterpretation | ||
533 | val relationInterpretation = match.get(2) as PartialRelationInterpretation | ||
534 | val src = match.get(3) as DefinedElement | ||
535 | val trg = match.get(4) as DefinedElement | ||
536 | createRelationLinkAction(src, trg, relationInterpretation, unitRulePropagator) | ||
537 | } | ||
538 | |||
539 | protected def void createRelationLinkAction(DefinedElement src, DefinedElement trg, | ||
540 | PartialRelationInterpretation relationInterpretation, UnitRulePropagator unitRulePropagator) { | ||
572 | val link = createBinaryElementRelationLink => [it.param1 = src it.param2 = trg] | 541 | val link = createBinaryElementRelationLink => [it.param1 = src it.param2 = trg] |
573 | relationInterpretation.relationlinks += link | 542 | relationInterpretation.relationlinks += link |
543 | unitRulePropagator.addedToRelation(relationInterpretation.interpretationOf) | ||
574 | } | 544 | } |
575 | 545 | ||
576 | protected def boolean createRelationLinkWithInverse(DefinedElement src, DefinedElement trg, | 546 | protected def void createRelationLinkWithInverse(IPatternMatch match, UnitRulePropagator unitRulePropagator) { |
577 | PartialRelationInterpretation relationInterpretation, PartialRelationInterpretation inverseInterpretation) { | 547 | // val problem = match.get(0) as LogicProblem |
548 | // val interpretation = match.get(1) as PartialInterpretation | ||
549 | val relationInterpretation = match.get(2) as PartialRelationInterpretation | ||
550 | val inverseInterpretation = match.get(3) as PartialRelationInterpretation | ||
551 | val src = match.get(4) as DefinedElement | ||
552 | val trg = match.get(5) as DefinedElement | ||
553 | createRelationLinkWithInverse(src, trg, relationInterpretation, inverseInterpretation, unitRulePropagator) | ||
554 | } | ||
555 | |||
556 | protected def void createRelationLinkWithInverse(DefinedElement src, DefinedElement trg, | ||
557 | PartialRelationInterpretation relationInterpretation, PartialRelationInterpretation inverseInterpretation, | ||
558 | UnitRulePropagator unitRulePropagator) { | ||
578 | val link = createBinaryElementRelationLink => [it.param1 = src it.param2 = trg] | 559 | val link = createBinaryElementRelationLink => [it.param1 = src it.param2 = trg] |
579 | relationInterpretation.relationlinks += link | 560 | relationInterpretation.relationlinks += link |
580 | val inverseLink = createBinaryElementRelationLink => [it.param1 = trg it.param2 = src] | 561 | val inverseLink = createBinaryElementRelationLink => [it.param1 = trg it.param2 = src] |
581 | inverseInterpretation.relationlinks += inverseLink | 562 | inverseInterpretation.relationlinks += inverseLink |
563 | unitRulePropagator.addedToRelation(relationInterpretation.interpretationOf) | ||
564 | unitRulePropagator.addedToRelation(inverseInterpretation.interpretationOf) | ||
582 | } | 565 | } |
583 | 566 | ||
584 | protected def flushQueryEngine(ScopePropagator scopePropagator) { | 567 | static class UnitRulePropagator { |
585 | if (scopePropagator.queryEngineFlushRequiredBeforePropagation && queryEngine.updatePropagationDelayed) { | 568 | val LogicProblem p |
586 | delayMessageDelivery.setBoolean(queryEngine, false) | 569 | val PartialInterpretation i |
587 | queryEngine.getQueryBackend(ReteBackendFactory.INSTANCE).flushUpdates | 570 | val RefinementRuleProvider refinementRuleProvider |
588 | delayMessageDelivery.setBoolean(queryEngine, true) | 571 | var AdvancedViatraQueryEngine queryEngine |
572 | var Field delayMessageDelivery | ||
573 | val ScopePropagator scopePropagator | ||
574 | val List<AbstractMustRelationPropagator<? extends IPatternMatch>> propagators | ||
575 | val ModelGenerationStatistics statistics | ||
576 | |||
577 | new(LogicProblem p, PartialInterpretation i, RefinementRuleProvider refinementRuleProvider, | ||
578 | ScopePropagator scopePropagator, | ||
579 | Map<Pair<RelationDeclaration, Relation>, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> mustRelationPropagationQueries, | ||
580 | ModelGenerationStatistics statistics) { | ||
581 | this.p = p | ||
582 | this.i = i | ||
583 | this.refinementRuleProvider = refinementRuleProvider | ||
584 | queryEngine = ViatraQueryEngine.on(new EMFScope(i)) as AdvancedViatraQueryEngine | ||
585 | delayMessageDelivery = queryEngine.class.getDeclaredField("delayMessageDelivery") | ||
586 | delayMessageDelivery.accessible = true | ||
587 | this.scopePropagator = scopePropagator | ||
588 | propagators = ImmutableList.copyOf(mustRelationPropagationQueries.entrySet.map [ entry | | ||
589 | val matcher = queryEngine.getMatcher(entry.value) | ||
590 | getPropagator(entry.key.key, entry.key.value, matcher) | ||
591 | ]) | ||
592 | this.statistics = statistics | ||
593 | } | ||
594 | |||
595 | def decrementTypeScope(PartialTypeInterpratation partialTypeInterpratation) { | ||
596 | scopePropagator.decrementTypeScope(partialTypeInterpratation) | ||
597 | } | ||
598 | |||
599 | def addedToRelation(Relation r) { | ||
600 | scopePropagator.addedToRelation(r) | ||
601 | } | ||
602 | |||
603 | def propagate() { | ||
604 | var boolean changed | ||
605 | do { | ||
606 | val scopeChanged = propagateScope() | ||
607 | val mustChanged = propagateMustRelations() | ||
608 | changed = scopeChanged || mustChanged | ||
609 | } while (changed) | ||
610 | } | ||
611 | |||
612 | protected def flushQueryEngine() { | ||
613 | if (queryEngine.updatePropagationDelayed) { | ||
614 | delayMessageDelivery.setBoolean(queryEngine, false) | ||
615 | queryEngine.getQueryBackend(ReteBackendFactory.INSTANCE).flushUpdates | ||
616 | delayMessageDelivery.setBoolean(queryEngine, true) | ||
617 | } | ||
618 | } | ||
619 | |||
620 | protected def propagateScope() { | ||
621 | if (scopePropagator.scopePropagationNeeded) { | ||
622 | if (scopePropagator.queryEngineFlushRequiredBeforePropagation) { | ||
623 | flushQueryEngine() | ||
624 | } | ||
625 | val propagatorStartTime = System.nanoTime | ||
626 | scopePropagator.propagateAllScopeConstraints() | ||
627 | statistics.addScopePropagationTime(System.nanoTime - propagatorStartTime) | ||
628 | true | ||
629 | } else { | ||
630 | false | ||
631 | } | ||
632 | } | ||
633 | |||
634 | protected def propagateMustRelations() { | ||
635 | if (propagators.empty) { | ||
636 | return false | ||
637 | } | ||
638 | flushQueryEngine() | ||
639 | val propagatorStartTime = System.nanoTime | ||
640 | var changed = false | ||
641 | for (propagator : propagators) { | ||
642 | changed = propagator.propagate(p, i, refinementRuleProvider, this) || changed | ||
643 | } | ||
644 | statistics.addMustRelationPropagationTime(System.nanoTime - propagatorStartTime) | ||
645 | changed | ||
646 | } | ||
647 | |||
648 | private static def <T extends IPatternMatch> getPropagator(Relation relation, Relation inverseRelation, | ||
649 | ViatraQueryMatcher<T> matcher) { | ||
650 | if (inverseRelation === null) { | ||
651 | new MustRelationPropagator(matcher) | ||
652 | } else if (relation == inverseRelation) { | ||
653 | new MustRelationPropagatorWithSelfInverse(matcher) | ||
654 | } else { | ||
655 | new MustRelationPropagatorWithInverse(matcher) | ||
656 | } | ||
657 | } | ||
658 | |||
659 | @FinalFieldsConstructor | ||
660 | private static abstract class AbstractMustRelationPropagator<T extends IPatternMatch> { | ||
661 | val ViatraQueryMatcher<T> matcher | ||
662 | |||
663 | def propagate(LogicProblem p, PartialInterpretation i, RefinementRuleProvider refinementRuleProvider, | ||
664 | UnitRulePropagator unitRulePropagator) { | ||
665 | val iterator = getIterator(p, i) | ||
666 | if (!iterator.hasNext) { | ||
667 | return false | ||
668 | } | ||
669 | iterate(iterator, refinementRuleProvider, unitRulePropagator) | ||
670 | true | ||
671 | } | ||
672 | |||
673 | def iterate(Iterator<T> iterator, RefinementRuleProvider refinementRuleProvider, | ||
674 | UnitRulePropagator unitRulePropagator) { | ||
675 | while (iterator.hasNext) { | ||
676 | doPropagate(iterator.next, refinementRuleProvider, unitRulePropagator) | ||
677 | } | ||
678 | } | ||
679 | |||
680 | protected def getIterator(LogicProblem p, PartialInterpretation i) { | ||
681 | val partialMatch = matcher.newEmptyMatch | ||
682 | partialMatch.set(0, p) | ||
683 | partialMatch.set(1, i) | ||
684 | matcher.streamAllMatches(partialMatch).iterator | ||
685 | } | ||
686 | |||
687 | protected def void doPropagate(T match, RefinementRuleProvider refinementRuleProvider, | ||
688 | UnitRulePropagator unitRulePropagator) | ||
689 | } | ||
690 | |||
691 | private static class MustRelationPropagator<T extends IPatternMatch> extends AbstractMustRelationPropagator<T> { | ||
692 | new(ViatraQueryMatcher<T> matcher) { | ||
693 | super(matcher) | ||
694 | } | ||
695 | |||
696 | override protected doPropagate(T match, RefinementRuleProvider refinementRuleProvider, | ||
697 | UnitRulePropagator unitRulePropagator) { | ||
698 | refinementRuleProvider.createRelationLinkAction(match, unitRulePropagator) | ||
699 | } | ||
700 | } | ||
701 | |||
702 | private static class MustRelationPropagatorWithInverse<T extends IPatternMatch> extends AbstractMustRelationPropagator<T> { | ||
703 | new(ViatraQueryMatcher<T> matcher) { | ||
704 | super(matcher) | ||
705 | } | ||
706 | |||
707 | override protected doPropagate(T match, RefinementRuleProvider refinementRuleProvider, | ||
708 | UnitRulePropagator unitRulePropagator) { | ||
709 | refinementRuleProvider.createRelationLinkWithInverse(match, unitRulePropagator) | ||
710 | } | ||
711 | } | ||
712 | |||
713 | private static class MustRelationPropagatorWithSelfInverse<T extends IPatternMatch> extends MustRelationPropagatorWithInverse<T> { | ||
714 | new(ViatraQueryMatcher<T> matcher) { | ||
715 | super(matcher) | ||
716 | } | ||
717 | |||
718 | override iterate(Iterator<T> iterator, RefinementRuleProvider refinementRuleProvider, | ||
719 | UnitRulePropagator unitRulePropagator) { | ||
720 | val pairs = newHashSet | ||
721 | while (iterator.hasNext) { | ||
722 | val match = iterator.next | ||
723 | val src = match.get(4) as DefinedElement | ||
724 | val trg = match.get(5) as DefinedElement | ||
725 | if (!pairs.contains(trg -> src)) { | ||
726 | pairs.add(src -> trg) | ||
727 | doPropagate(match, refinementRuleProvider, unitRulePropagator) | ||
728 | } | ||
729 | } | ||
730 | } | ||
589 | } | 731 | } |
590 | } | 732 | } |
591 | } | 733 | } |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/util/ParseUtil.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/util/ParseUtil.xtend index 26ec7091..69b54b8a 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/util/ParseUtil.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/util/ParseUtil.xtend | |||
@@ -6,7 +6,6 @@ import com.google.inject.Inject | |||
6 | import com.google.inject.Injector | 6 | import com.google.inject.Injector |
7 | import com.google.inject.multibindings.Multibinder | 7 | import com.google.inject.multibindings.Multibinder |
8 | import com.google.inject.name.Names | 8 | import com.google.inject.name.Names |
9 | import com.google.inject.util.Modules | ||
10 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguagePackage | 9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguagePackage |
11 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage | 10 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage |
12 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialinterpretationPackage | 11 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialinterpretationPackage |
@@ -46,7 +45,6 @@ import org.eclipse.xtext.scoping.IScope | |||
46 | import org.eclipse.xtext.scoping.IScopeProvider | 45 | import org.eclipse.xtext.scoping.IScopeProvider |
47 | import org.eclipse.xtext.scoping.impl.AbstractDeclarativeScopeProvider | 46 | import org.eclipse.xtext.scoping.impl.AbstractDeclarativeScopeProvider |
48 | import org.eclipse.xtext.scoping.impl.SimpleScope | 47 | import org.eclipse.xtext.scoping.impl.SimpleScope |
49 | import org.eclipse.xtext.service.AbstractGenericModule | ||
50 | import org.eclipse.xtext.service.SingletonBinding | 48 | import org.eclipse.xtext.service.SingletonBinding |
51 | import org.eclipse.xtext.workspace.IProjectConfigProvider | 49 | import org.eclipse.xtext.workspace.IProjectConfigProvider |
52 | 50 | ||
@@ -65,35 +63,32 @@ package class StandaloneParserWithFixedMetamodelProviderModule extends Standalon | |||
65 | Multibinder::newSetBinder(binder, IMetamodelProviderInstance); | 63 | Multibinder::newSetBinder(binder, IMetamodelProviderInstance); |
66 | } | 64 | } |
67 | 65 | ||
68 | } | 66 | @SingletonBinding |
69 | 67 | override IResourceServiceProvider.Registry bindIResourceServiceProvider$Registry() { | |
70 | package class StandaloneParserOverridesModule extends AbstractGenericModule { | 68 | new VqlDeactivatedServiceProviderRegistry |
71 | 69 | } | |
72 | def Class<? extends IMetamodelProvider> bindIMetamodelProvider() { | 70 | |
71 | override Class<? extends IMetamodelProvider> bindIMetamodelProvider() { | ||
73 | FixedMetamodelProvider | 72 | FixedMetamodelProvider |
74 | } | 73 | } |
75 | 74 | ||
76 | def Class<? extends IProjectConfigProvider> bindProjectConfigProvider() { | 75 | override Class<? extends IProjectConfigProvider> bindProjectConfigProvider() { |
77 | NullProjectConfigProvider | 76 | NullProjectConfigProvider |
78 | } | 77 | } |
79 | 78 | ||
80 | @SingletonBinding | 79 | @SingletonBinding |
81 | def Class<? extends IResourceServiceProvider.Registry> bindIResourceServiceProvider$Registry() { | 80 | override EValidator.Registry bindEValidatorRegistry() { |
82 | VqlDeactivatedServiceProviderRegistry | ||
83 | } | ||
84 | |||
85 | def EValidator.Registry bindEValidator$Registry() { | ||
86 | // org.eclipse.xtext.validation.EValidatorRegistrar modifies EValidators already in the registry, | 81 | // org.eclipse.xtext.validation.EValidatorRegistrar modifies EValidators already in the registry, |
87 | // so it is not safe to populate the registry from the EValidator.Registry.INSTANCE singleton. | 82 | // so it is not safe to populate the registry from the EValidator.Registry.INSTANCE singleton. |
88 | // There is no need to execute any EValiator other than EMFPatternLanguageValidator, | 83 | // There is no need to execute any EValiator other than EMFPatternLanguageValidator, |
89 | // so we can start with a blank registry instead. | 84 | // so we can start with a blank registry instead. |
90 | new EValidatorRegistryImpl() | 85 | new EValidatorRegistryImpl |
91 | } | 86 | } |
92 | 87 | ||
93 | def EPackage.Registry bindEPackage$Registry() { | 88 | @SingletonBinding |
89 | override EPackage.Registry bindEPackageRegistry() { | ||
94 | new EPackageRegistryImpl(EPackage.Registry.INSTANCE) | 90 | new EPackageRegistryImpl(EPackage.Registry.INSTANCE) |
95 | } | 91 | } |
96 | |||
97 | } | 92 | } |
98 | 93 | ||
99 | package class NullProjectConfigProvider implements IProjectConfigProvider { | 94 | package class NullProjectConfigProvider implements IProjectConfigProvider { |
@@ -136,10 +131,8 @@ class ParseUtil { | |||
136 | 131 | ||
137 | def protected Injector internalCreateInjector() { | 132 | def protected Injector internalCreateInjector() { |
138 | ensureViatraInitialized(); | 133 | ensureViatraInitialized(); |
139 | val runtimeModulemodule = new StandaloneParserWithFixedMetamodelProviderModule | 134 | val runtimeModule = new StandaloneParserWithFixedMetamodelProviderModule |
140 | val overridesModule = new StandaloneParserOverridesModule | 135 | val newInjector = Guice.createInjector(runtimeModule) |
141 | val module = Modules.override(runtimeModulemodule).with(overridesModule) | ||
142 | val newInjector = Guice.createInjector(module) | ||
143 | return newInjector | 136 | return newInjector |
144 | } | 137 | } |
145 | 138 | ||