diff options
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ModelGenerationMethodProvider.xtend')
-rw-r--r-- | Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ModelGenerationMethodProvider.xtend | 201 |
1 files changed, 201 insertions, 0 deletions
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ModelGenerationMethodProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ModelGenerationMethodProvider.xtend new file mode 100644 index 00000000..25137eba --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ModelGenerationMethodProvider.xtend | |||
@@ -0,0 +1,201 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner | ||
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.ModelGenerationStatistics | ||
9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.CachingSimplePolyhedronScopePropagatorStrategy | ||
10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.CbcPolyhedronSolver | ||
11 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearTypeConstraintHint | ||
12 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.MultiplicityGoalConstraintCalculator | ||
13 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronExtensionOperator | ||
14 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronScopePropagator | ||
15 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.RelationConstraintCalculator | ||
16 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagator | ||
17 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy | ||
18 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.TypeHierarchyScopePropagator | ||
19 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Z3PolyhedronSolver | ||
20 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.GeneratedPatterns | ||
21 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.ModalPatternQueries | ||
22 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.PatternProvider | ||
23 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules.GoalConstraintProvider | ||
24 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules.RefinementRuleProvider | ||
25 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | ||
26 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.DiversityChecker | ||
27 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ViatraReasonerSolutionSaver | ||
28 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ThreeValuedCostObjectiveProvider | ||
29 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace | ||
30 | import java.util.Collection | ||
31 | import java.util.List | ||
32 | import java.util.Map | ||
33 | import java.util.Set | ||
34 | import org.eclipse.viatra.dse.objectives.IObjective | ||
35 | import org.eclipse.viatra.query.runtime.api.GenericQueryGroup | ||
36 | import org.eclipse.viatra.query.runtime.api.IPatternMatch | ||
37 | import org.eclipse.viatra.query.runtime.api.IQuerySpecification | ||
38 | import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine | ||
39 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher | ||
40 | import org.eclipse.viatra.query.runtime.emf.EMFScope | ||
41 | import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint | ||
42 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery | ||
43 | import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRule | ||
44 | import org.eclipse.xtend.lib.annotations.Data | ||
45 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ExtendedPolyhedronScopePropagatorStrategy | ||
46 | |||
47 | @Data class ModelGenerationMethod { | ||
48 | ModelGenerationStatistics statistics | ||
49 | |||
50 | Collection<? extends BatchTransformationRule<?, ?>> objectRefinementRules | ||
51 | Collection<? extends BatchTransformationRule<?, ?>> relationRefinementRules | ||
52 | |||
53 | List<MultiplicityGoalConstraintCalculator> unfinishedMultiplicities | ||
54 | |||
55 | Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWF | ||
56 | |||
57 | Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidWF | ||
58 | |||
59 | Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> mustUnitPropagationPreconditions | ||
60 | Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> currentUnitPropagationPreconditions | ||
61 | |||
62 | Map<String, ModalPatternQueries> modalRelationQueries | ||
63 | |||
64 | Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allPatterns | ||
65 | |||
66 | Collection<IObjective> costObjectives | ||
67 | boolean optimizationProblem | ||
68 | ViatraReasonerSolutionSaver solutionSaver | ||
69 | } | ||
70 | |||
71 | class ModelGenerationMethodProvider { | ||
72 | val PatternProvider patternProvider = new PatternProvider | ||
73 | val RefinementRuleProvider refinementRuleProvider = new RefinementRuleProvider | ||
74 | val GoalConstraintProvider goalConstraintProvider = new GoalConstraintProvider | ||
75 | val relationConstraintCalculator = new RelationConstraintCalculator | ||
76 | |||
77 | def ModelGenerationMethod createModelGenerationMethod( | ||
78 | LogicProblem logicProblem, | ||
79 | PartialInterpretation emptySolution, | ||
80 | ReasonerWorkspace workspace, | ||
81 | ViatraReasonerConfiguration config | ||
82 | ) { | ||
83 | val statistics = new ModelGenerationStatistics | ||
84 | val debugLevel = config.documentationLevel | ||
85 | val writeFiles = (debugLevel === DocumentationLevel.NORMAL || debugLevel === DocumentationLevel.FULL) | ||
86 | |||
87 | val Set<PQuery> existingQueries = logicProblem.relations.map[annotations].flatten.filter(TransfomedViatraQuery). | ||
88 | map[it.patternPQuery as PQuery].toSet | ||
89 | |||
90 | val relationConstraints = relationConstraintCalculator.calculateRelationConstraints(logicProblem) | ||
91 | val queries = patternProvider.generateQueries(logicProblem, emptySolution, statistics, existingQueries, | ||
92 | workspace, config.typeInferenceMethod, config.scopePropagatorStrategy, relationConstraints, config.hints, | ||
93 | config.unitPropagationPatternGenerators, writeFiles) | ||
94 | |||
95 | val unfinishedMultiplicities = goalConstraintProvider.getUnfinishedMultiplicityQueries(logicProblem, queries, | ||
96 | config.calculateObjectCreationCosts) | ||
97 | val unfinishedWF = queries.getUnfinishedWFQueries.values | ||
98 | val modalRelationQueriesBuilder = ImmutableMap.builder | ||
99 | for (entry : queries.modalRelationQueries.entrySet) { | ||
100 | val annotation = entry.key.annotations.filter(TransfomedViatraQuery).head | ||
101 | if (annotation !== null) { | ||
102 | modalRelationQueriesBuilder.put(annotation.patternFullyQualifiedName, entry.value) | ||
103 | } | ||
104 | } | ||
105 | val modalRelationQueries = modalRelationQueriesBuilder.build | ||
106 | val invalidWF = queries.getInvalidWFQueries.values | ||
107 | val mustUnitPropagationPreconditions = queries.getMustUnitPropagationPreconditionPatterns | ||
108 | val currentUnitPropagationPreconditions = queries.getCurrentUnitPropagationPreconditionPatterns | ||
109 | val queriesToPrepare = ImmutableSet.builder.addAll(queries.refineObjectQueries.values).addAll( | ||
110 | queries.refineTypeQueries.values).addAll(queries.refineRelationQueries.values).addAll( | ||
111 | queries.mustRelationPropagationQueries.values).addAll(queries.multiplicityConstraintQueries.values.flatMap [ | ||
112 | allQueries | ||
113 | ]).addAll(queries.unfinishedWFQueries.values).addAll(queries.invalidWFQueries.values).addAll( | ||
114 | queries.mustUnitPropagationPreconditionPatterns.values).addAll( | ||
115 | queries.currentUnitPropagationPreconditionPatterns.values).add(queries.hasElementInContainmentQuery).build | ||
116 | val queryEngine = ViatraQueryEngine.on(new EMFScope(emptySolution)) | ||
117 | GenericQueryGroup.of(queriesToPrepare).prepare(queryEngine) | ||
118 | |||
119 | val objectiveProvider = new ThreeValuedCostObjectiveProvider(queryEngine, emptySolution, modalRelationQueries) | ||
120 | val transformedObjectives = objectiveProvider.getCostObjectives(config.costObjectives) | ||
121 | |||
122 | val solutionSaver = new ViatraReasonerSolutionSaver(transformedObjectives.leveledExtremalObjectives, | ||
123 | config.solutionScope.numberOfRequiredSolutions, DiversityChecker.of(config.diversityRequirement)) | ||
124 | |||
125 | val allHints = ImmutableSet.builder | ||
126 | allHints.addAll(config.hints) | ||
127 | for (hint : transformedObjectives.hints) { | ||
128 | hint.boundsProvider = solutionSaver | ||
129 | allHints.add(hint) | ||
130 | } | ||
131 | |||
132 | val scopePropagator = createScopePropagator(config.scopePropagatorStrategy, emptySolution, allHints.build, | ||
133 | transformedObjectives.extensionOperators, queries, statistics) | ||
134 | scopePropagator.propagateAllScopeConstraints | ||
135 | val unitRulePropagator = refinementRuleProvider.createUnitPrulePropagator(logicProblem, emptySolution, queries, | ||
136 | scopePropagator, statistics) | ||
137 | val objectRefinementRules = refinementRuleProvider.createObjectRefinementRules(logicProblem, emptySolution, | ||
138 | queries, unitRulePropagator, config.nameNewElements, statistics) | ||
139 | val relationRefinementRules = refinementRuleProvider.createRelationRefinementRules(queries, unitRulePropagator, | ||
140 | statistics) | ||
141 | |||
142 | return new ModelGenerationMethod( | ||
143 | statistics, | ||
144 | objectRefinementRules.values, | ||
145 | relationRefinementRules.values, | ||
146 | unfinishedMultiplicities, | ||
147 | unfinishedWF, | ||
148 | invalidWF, | ||
149 | mustUnitPropagationPreconditions, | ||
150 | currentUnitPropagationPreconditions, | ||
151 | modalRelationQueries, | ||
152 | queries.allQueries, | ||
153 | transformedObjectives.objectives, | ||
154 | transformedObjectives.optimizationProblem, | ||
155 | solutionSaver | ||
156 | ) | ||
157 | } | ||
158 | |||
159 | private def createScopePropagator(ScopePropagatorStrategy scopePropagatorStrategy, | ||
160 | PartialInterpretation emptySolution, Collection<LinearTypeConstraintHint> hints, | ||
161 | Collection<PolyhedronExtensionOperator> extensionOperators, GeneratedPatterns queries, | ||
162 | ModelGenerationStatistics statistics) { | ||
163 | if (!hints.empty && !(scopePropagatorStrategy instanceof ScopePropagatorStrategy.Polyhedral)) { | ||
164 | throw new IllegalArgumentException("Only the Polyhedral scope propagator strategy can use hints.") | ||
165 | } | ||
166 | switch (scopePropagatorStrategy) { | ||
167 | case ScopePropagatorStrategy.None, | ||
168 | case ScopePropagatorStrategy.Basic: | ||
169 | new ScopePropagator(emptySolution, statistics) | ||
170 | case ScopePropagatorStrategy.BasicTypeHierarchy: | ||
171 | new TypeHierarchyScopePropagator(emptySolution, statistics) | ||
172 | ScopePropagatorStrategy.Polyhedral: { | ||
173 | val types = queries.refineObjectQueries.keySet.map[newType].toSet | ||
174 | val allPatternsByName = queries.allQueries.toMap[fullyQualifiedName] | ||
175 | val solver = switch (scopePropagatorStrategy.solver) { | ||
176 | case Z3Integer: | ||
177 | new Z3PolyhedronSolver(false, scopePropagatorStrategy.timeoutSeconds) | ||
178 | case Z3Real: | ||
179 | new Z3PolyhedronSolver(true, scopePropagatorStrategy.timeoutSeconds) | ||
180 | case Cbc: | ||
181 | new CbcPolyhedronSolver(false, scopePropagatorStrategy.timeoutSeconds, true) | ||
182 | case Clp: | ||
183 | new CbcPolyhedronSolver(true, scopePropagatorStrategy.timeoutSeconds, true) | ||
184 | default: | ||
185 | throw new IllegalArgumentException("Unknown polyhedron solver: " + | ||
186 | scopePropagatorStrategy.solver) | ||
187 | } | ||
188 | val strategy = if (extensionOperators.empty) { | ||
189 | new CachingSimplePolyhedronScopePropagatorStrategy(solver, statistics) | ||
190 | } else { | ||
191 | new ExtendedPolyhedronScopePropagatorStrategy(solver, extensionOperators, statistics) | ||
192 | } | ||
193 | new PolyhedronScopePropagator(emptySolution, statistics, types, queries.multiplicityConstraintQueries, | ||
194 | queries.hasElementInContainmentQuery, allPatternsByName, hints, strategy, | ||
195 | scopePropagatorStrategy.requiresUpperBoundIndexing, scopePropagatorStrategy.updateHeuristic) | ||
196 | } | ||
197 | default: | ||
198 | throw new IllegalArgumentException("Unknown scope propagator strategy: " + scopePropagatorStrategy) | ||
199 | } | ||
200 | } | ||
201 | } | ||