aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend
diff options
context:
space:
mode:
authorLibravatar Kristóf Marussy <marussy@mit.bme.hu>2020-11-02 02:02:40 +0100
committerLibravatar Kristóf Marussy <marussy@mit.bme.hu>2020-11-02 02:02:40 +0100
commitf06427cd7375551582461f91b3458339a8227f9b (patch)
tree97bc6ec85f4c384e5080a6611b492caf460b6ce9 /Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend
parentMust unit propagation (diff)
downloadVIATRA-Generator-f06427cd7375551582461f91b3458339a8227f9b.tar.gz
VIATRA-Generator-f06427cd7375551582461f91b3458339a8227f9b.tar.zst
VIATRA-Generator-f06427cd7375551582461f91b3458339a8227f9b.zip
Optimizing generator with linear objective functions
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend')
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend226
1 files changed, 0 insertions, 226 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 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 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra
2
3import com.google.common.collect.ImmutableMap
4import com.google.common.collect.ImmutableSet
5import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel
6import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
7import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransfomedViatraQuery
8import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.CbcPolyhedronSolver
9import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearTypeConstraintHint
10import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.MultiplicityGoalConstraintCalculator
11import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronScopePropagator
12import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.RelationConstraintCalculator
13import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagator
14import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy
15import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.TypeHierarchyScopePropagator
16import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Z3PolyhedronSolver
17import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.GeneratedPatterns
18import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.ModalPatternQueries
19import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.PatternProvider
20import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.UnitPropagationPatternGenerator
21import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules.GoalConstraintProvider
22import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules.RefinementRuleProvider
23import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
24import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace
25import java.util.Collection
26import java.util.List
27import java.util.Map
28import java.util.Set
29import org.eclipse.viatra.query.runtime.api.GenericQueryGroup
30import org.eclipse.viatra.query.runtime.api.IPatternMatch
31import org.eclipse.viatra.query.runtime.api.IQuerySpecification
32import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine
33import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher
34import org.eclipse.viatra.query.runtime.emf.EMFScope
35import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint
36import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery
37import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRule
38import org.eclipse.xtend.lib.annotations.Data
39
40class 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
106enum TypeInferenceMethod {
107 Generic,
108 PreliminaryAnalysis
109}
110
111class 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}
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-07-08 09:10:38 +0000