diff options
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra')
9 files changed, 414 insertions, 268 deletions
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/META-INF/MANIFEST.MF b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/META-INF/MANIFEST.MF index b9da0f0b..ec1557e8 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/META-INF/MANIFEST.MF +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/META-INF/MANIFEST.MF | |||
@@ -8,7 +8,8 @@ Export-Package: hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra, | |||
8 | hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.interval, | 8 | hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.interval, |
9 | hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.interval.aggregators, | 9 | hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.interval.aggregators, |
10 | hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns, | 10 | hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns, |
11 | hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries | 11 | hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries, |
12 | hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules | ||
12 | Require-Bundle: hu.bme.mit.inf.dslreasoner.logic.model;bundle-version="1.0.0", | 13 | Require-Bundle: hu.bme.mit.inf.dslreasoner.logic.model;bundle-version="1.0.0", |
13 | hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage;bundle-version="1.0.0", | 14 | hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage;bundle-version="1.0.0", |
14 | hu.bme.mit.inf.dslreasoner.ecore2logic;bundle-version="1.0.0", | 15 | hu.bme.mit.inf.dslreasoner.ecore2logic;bundle-version="1.0.0", |
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 3bcd9116..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,226 +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.patterns.UnitPropagationPatternGenerator | ||
21 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules.GoalConstraintProvider | ||
22 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules.RefinementRuleProvider | ||
23 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | ||
24 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace | ||
25 | import java.util.Collection | ||
26 | import java.util.List | ||
27 | import java.util.Map | ||
28 | import java.util.Set | ||
29 | import org.eclipse.viatra.query.runtime.api.GenericQueryGroup | ||
30 | import org.eclipse.viatra.query.runtime.api.IPatternMatch | ||
31 | import org.eclipse.viatra.query.runtime.api.IQuerySpecification | ||
32 | import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine | ||
33 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher | ||
34 | import org.eclipse.viatra.query.runtime.emf.EMFScope | ||
35 | import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint | ||
36 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery | ||
37 | import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRule | ||
38 | import org.eclipse.xtend.lib.annotations.Data | ||
39 | |||
40 | class ModelGenerationStatistics { | ||
41 | public var long transformationExecutionTime = 0 | ||
42 | |||
43 | synchronized def addExecutionTime(long amount) { | ||
44 | transformationExecutionTime += amount | ||
45 | } | ||
46 | |||
47 | public var long scopePropagationTime = 0 | ||
48 | |||
49 | synchronized def addScopePropagationTime(long amount) { | ||
50 | scopePropagationTime += amount | ||
51 | } | ||
52 | |||
53 | public var long mustRelationPropagationTime = 0 | ||
54 | |||
55 | synchronized def addMustRelationPropagationTime(long amount) { | ||
56 | mustRelationPropagationTime += amount | ||
57 | } | ||
58 | |||
59 | public var long preliminaryTypeAnalisisTime = 0 | ||
60 | |||
61 | public var int decisionsTried = 0 | ||
62 | |||
63 | synchronized def incrementDecisionCount() { | ||
64 | decisionsTried++ | ||
65 | } | ||
66 | |||
67 | public var int transformationInvocations | ||
68 | |||
69 | synchronized def incrementTransformationCount() { | ||
70 | transformationInvocations++ | ||
71 | } | ||
72 | |||
73 | public var int scopePropagatorInvocations | ||
74 | |||
75 | synchronized def incrementScopePropagationCount() { | ||
76 | scopePropagatorInvocations++ | ||
77 | } | ||
78 | |||
79 | public var int scopePropagatorSolverInvocations | ||
80 | |||
81 | synchronized def incrementScopePropagationSolverCount() { | ||
82 | scopePropagatorSolverInvocations++ | ||
83 | } | ||
84 | } | ||
85 | |||
86 | @Data class ModelGenerationMethod { | ||
87 | ModelGenerationStatistics statistics | ||
88 | |||
89 | Collection<? extends BatchTransformationRule<?, ?>> objectRefinementRules | ||
90 | Collection<? extends BatchTransformationRule<?, ?>> relationRefinementRules | ||
91 | |||
92 | List<MultiplicityGoalConstraintCalculator> unfinishedMultiplicities | ||
93 | |||
94 | Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWF | ||
95 | |||
96 | Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidWF | ||
97 | |||
98 | Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> mustUnitPropagationPreconditions | ||
99 | Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> currentUnitPropagationPreconditions | ||
100 | |||
101 | Map<String, ModalPatternQueries> modalRelationQueries | ||
102 | |||
103 | Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allPatterns | ||
104 | } | ||
105 | |||
106 | enum TypeInferenceMethod { | ||
107 | Generic, | ||
108 | PreliminaryAnalysis | ||
109 | } | ||
110 | |||
111 | class ModelGenerationMethodProvider { | ||
112 | val PatternProvider patternProvider = new PatternProvider | ||
113 | val RefinementRuleProvider refinementRuleProvider = new RefinementRuleProvider | ||
114 | val GoalConstraintProvider goalConstraintProvider = new GoalConstraintProvider | ||
115 | val relationConstraintCalculator = new RelationConstraintCalculator | ||
116 | |||
117 | def ModelGenerationMethod createModelGenerationMethod( | ||
118 | LogicProblem logicProblem, | ||
119 | PartialInterpretation emptySolution, | ||
120 | ReasonerWorkspace workspace, | ||
121 | boolean nameNewElements, | ||
122 | TypeInferenceMethod typeInferenceMethod, | ||
123 | boolean calculateObjectCreationCosts, | ||
124 | ScopePropagatorStrategy scopePropagatorStrategy, | ||
125 | Collection<LinearTypeConstraintHint> hints, | ||
126 | Collection<UnitPropagationPatternGenerator> unitPropagationPatternGenerators, | ||
127 | DocumentationLevel debugLevel | ||
128 | ) { | ||
129 | val statistics = new ModelGenerationStatistics | ||
130 | val writeFiles = (debugLevel === DocumentationLevel.NORMAL || debugLevel === DocumentationLevel.FULL) | ||
131 | |||
132 | val Set<PQuery> existingQueries = logicProblem.relations.map[annotations].flatten.filter(TransfomedViatraQuery). | ||
133 | map[it.patternPQuery as PQuery].toSet | ||
134 | |||
135 | val relationConstraints = relationConstraintCalculator.calculateRelationConstraints(logicProblem) | ||
136 | val queries = patternProvider.generateQueries(logicProblem, emptySolution, statistics, existingQueries, | ||
137 | workspace, typeInferenceMethod, scopePropagatorStrategy, relationConstraints, hints, | ||
138 | unitPropagationPatternGenerators, writeFiles) | ||
139 | |||
140 | val scopePropagator = createScopePropagator(scopePropagatorStrategy, emptySolution, hints, queries, statistics) | ||
141 | scopePropagator.propagateAllScopeConstraints | ||
142 | val unitRulePropagator = refinementRuleProvider.createUnitPrulePropagator(logicProblem, emptySolution, | ||
143 | queries, scopePropagator, statistics) | ||
144 | val objectRefinementRules = refinementRuleProvider.createObjectRefinementRules(logicProblem, emptySolution, | ||
145 | queries, unitRulePropagator, nameNewElements, statistics) | ||
146 | val relationRefinementRules = refinementRuleProvider.createRelationRefinementRules(queries, unitRulePropagator, | ||
147 | statistics) | ||
148 | |||
149 | val unfinishedMultiplicities = goalConstraintProvider.getUnfinishedMultiplicityQueries(logicProblem, queries, | ||
150 | calculateObjectCreationCosts) | ||
151 | |||
152 | val unfinishedWF = queries.getUnfinishedWFQueries.values | ||
153 | |||
154 | val modalRelationQueriesBuilder = ImmutableMap.builder | ||
155 | for (entry : queries.modalRelationQueries.entrySet) { | ||
156 | val annotation = entry.key.annotations.filter(TransfomedViatraQuery).head | ||
157 | if (annotation !== null) { | ||
158 | modalRelationQueriesBuilder.put(annotation.patternFullyQualifiedName, entry.value) | ||
159 | } | ||
160 | } | ||
161 | val modalRelationQueries = modalRelationQueriesBuilder.build | ||
162 | |||
163 | val invalidWF = queries.getInvalidWFQueries.values | ||
164 | |||
165 | val mustUnitPropagationPreconditions = queries.getMustUnitPropagationPreconditionPatterns | ||
166 | val currentUnitPropagationPreconditions = queries.getCurrentUnitPropagationPreconditionPatterns | ||
167 | |||
168 | val queriesToPrepare = ImmutableSet.builder.addAll(queries.refineObjectQueries.values).addAll( | ||
169 | queries.refineTypeQueries.values).addAll(queries.refineRelationQueries.values).addAll(queries. | ||
170 | multiplicityConstraintQueries.values.flatMap[allQueries]).addAll(queries.unfinishedWFQueries.values).addAll( | ||
171 | queries.invalidWFQueries.values).addAll(queries.mustUnitPropagationPreconditionPatterns.values).addAll( | ||
172 | queries.currentUnitPropagationPreconditionPatterns.values).add(queries.hasElementInContainmentQuery).build | ||
173 | val queryEngine = ViatraQueryEngine.on(new EMFScope(emptySolution)) | ||
174 | GenericQueryGroup.of(queriesToPrepare).prepare(queryEngine) | ||
175 | |||
176 | return new ModelGenerationMethod( | ||
177 | statistics, | ||
178 | objectRefinementRules.values, | ||
179 | relationRefinementRules.values, | ||
180 | unfinishedMultiplicities, | ||
181 | unfinishedWF, | ||
182 | invalidWF, | ||
183 | mustUnitPropagationPreconditions, | ||
184 | currentUnitPropagationPreconditions, | ||
185 | modalRelationQueries, | ||
186 | queries.allQueries | ||
187 | ) | ||
188 | } | ||
189 | |||
190 | private def createScopePropagator(ScopePropagatorStrategy scopePropagatorStrategy, | ||
191 | PartialInterpretation emptySolution, Collection<LinearTypeConstraintHint> hints, GeneratedPatterns queries, | ||
192 | ModelGenerationStatistics statistics) { | ||
193 | if (!hints.empty && !(scopePropagatorStrategy instanceof ScopePropagatorStrategy.Polyhedral)) { | ||
194 | throw new IllegalArgumentException("Only the Polyhedral scope propagator strategy can use hints.") | ||
195 | } | ||
196 | switch (scopePropagatorStrategy) { | ||
197 | case ScopePropagatorStrategy.None, | ||
198 | case ScopePropagatorStrategy.Basic: | ||
199 | new ScopePropagator(emptySolution, statistics) | ||
200 | case ScopePropagatorStrategy.BasicTypeHierarchy: | ||
201 | new TypeHierarchyScopePropagator(emptySolution, statistics) | ||
202 | ScopePropagatorStrategy.Polyhedral: { | ||
203 | val types = queries.refineObjectQueries.keySet.map[newType].toSet | ||
204 | val allPatternsByName = queries.allQueries.toMap[fullyQualifiedName] | ||
205 | val solver = switch (scopePropagatorStrategy.solver) { | ||
206 | case Z3Integer: | ||
207 | new Z3PolyhedronSolver(false, scopePropagatorStrategy.timeoutSeconds) | ||
208 | case Z3Real: | ||
209 | new Z3PolyhedronSolver(true, scopePropagatorStrategy.timeoutSeconds) | ||
210 | case Cbc: | ||
211 | new CbcPolyhedronSolver(false, scopePropagatorStrategy.timeoutSeconds, true) | ||
212 | case Clp: | ||
213 | new CbcPolyhedronSolver(true, scopePropagatorStrategy.timeoutSeconds, true) | ||
214 | default: | ||
215 | throw new IllegalArgumentException("Unknown polyhedron solver: " + | ||
216 | scopePropagatorStrategy.solver) | ||
217 | } | ||
218 | new PolyhedronScopePropagator(emptySolution, statistics, types, queries.multiplicityConstraintQueries, | ||
219 | queries.hasElementInContainmentQuery, allPatternsByName, hints, solver, | ||
220 | scopePropagatorStrategy.requiresUpperBoundIndexing, scopePropagatorStrategy.updateHeuristic) | ||
221 | } | ||
222 | default: | ||
223 | throw new IllegalArgumentException("Unknown scope propagator strategy: " + scopePropagatorStrategy) | ||
224 | } | ||
225 | } | ||
226 | } | ||
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/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 |