diff options
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.xtend | 187 |
1 files changed, 143 insertions, 44 deletions
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend index b63607f7..6fbbc779 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend | |||
@@ -1,8 +1,20 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra | 1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra |
2 | 2 | ||
3 | import com.google.common.collect.ImmutableMap | ||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel | 4 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel |
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | 5 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem |
5 | import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransfomedViatraQuery | 6 | import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransfomedViatraQuery |
7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.CbcPolyhedronSolver | ||
8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearTypeConstraintHint | ||
9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.MultiplicityGoalConstraintCalculator | ||
10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronScopePropagator | ||
11 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.RelationConstraintCalculator | ||
12 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagator | ||
13 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy | ||
14 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.TypeHierarchyScopePropagator | ||
15 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Z3PolyhedronSolver | ||
16 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.GeneratedPatterns | ||
17 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.ModalPatternQueries | ||
6 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.PatternProvider | 18 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.PatternProvider |
7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules.GoalConstraintProvider | 19 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules.GoalConstraintProvider |
8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules.RefinementRuleProvider | 20 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules.RefinementRuleProvider |
@@ -10,82 +22,131 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.par | |||
10 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace | 22 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace |
11 | import java.util.Collection | 23 | import java.util.Collection |
12 | import java.util.List | 24 | import java.util.List |
25 | import java.util.Map | ||
13 | import java.util.Set | 26 | import java.util.Set |
14 | import org.eclipse.viatra.query.runtime.api.IPatternMatch | 27 | import org.eclipse.viatra.query.runtime.api.IPatternMatch |
15 | import org.eclipse.viatra.query.runtime.api.IQuerySpecification | 28 | import org.eclipse.viatra.query.runtime.api.IQuerySpecification |
16 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher | 29 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher |
30 | import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint | ||
17 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery | 31 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery |
18 | import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRule | 32 | import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRule |
19 | import org.eclipse.xtend.lib.annotations.Data | 33 | import org.eclipse.xtend.lib.annotations.Data |
20 | import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint | ||
21 | import java.util.Map | ||
22 | 34 | ||
23 | class ModelGenerationStatistics { | 35 | class ModelGenerationStatistics { |
24 | public var long transformationExecutionTime = 0 | 36 | public var long transformationExecutionTime = 0 |
37 | |||
25 | synchronized def addExecutionTime(long amount) { | 38 | synchronized def addExecutionTime(long amount) { |
26 | transformationExecutionTime+=amount | 39 | transformationExecutionTime += amount |
40 | } | ||
41 | |||
42 | public var long scopePropagationTime = 0 | ||
43 | |||
44 | synchronized def addScopePropagationTime(long amount) { | ||
45 | scopePropagationTime += amount | ||
46 | } | ||
47 | |||
48 | public var long preliminaryTypeAnalisisTime = 0 | ||
49 | |||
50 | public var int decisionsTried = 0 | ||
51 | |||
52 | synchronized def incrementDecisionCount() { | ||
53 | decisionsTried++ | ||
54 | } | ||
55 | |||
56 | public var int transformationInvocations | ||
57 | |||
58 | synchronized def incrementTransformationCount() { | ||
59 | transformationInvocations++ | ||
60 | } | ||
61 | |||
62 | public var int scopePropagatorInvocations | ||
63 | |||
64 | synchronized def incrementScopePropagationCount() { | ||
65 | scopePropagatorInvocations++ | ||
66 | } | ||
67 | |||
68 | public var int scopePropagatorSolverInvocations | ||
69 | |||
70 | synchronized def incrementScopePropagationSolverCount() { | ||
71 | scopePropagatorSolverInvocations++ | ||
27 | } | 72 | } |
28 | public var long PreliminaryTypeAnalisisTime = 0 | ||
29 | } | 73 | } |
74 | |||
30 | @Data class ModelGenerationMethod { | 75 | @Data class ModelGenerationMethod { |
31 | ModelGenerationStatistics statistics | 76 | ModelGenerationStatistics statistics |
32 | 77 | ||
33 | Collection<? extends BatchTransformationRule<?,?>> objectRefinementRules | 78 | Collection<? extends BatchTransformationRule<?, ?>> objectRefinementRules |
34 | Collection<? extends BatchTransformationRule<?,?>> relationRefinementRules | 79 | Collection<? extends BatchTransformationRule<?, ?>> relationRefinementRules |
35 | 80 | ||
36 | List<MultiplicityGoalConstraintCalculator> unfinishedMultiplicities | 81 | List<MultiplicityGoalConstraintCalculator> unfinishedMultiplicities |
37 | Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWF | 82 | |
38 | 83 | Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWF | |
39 | Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidWF | 84 | |
40 | 85 | Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidWF | |
41 | Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> mustUnitPropagationPreconditions | 86 | |
42 | Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> currentUnitPropagationPreconditions | 87 | Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> mustUnitPropagationPreconditions |
43 | 88 | Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> currentUnitPropagationPreconditions | |
44 | Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allPatterns | 89 | |
90 | Map<String, ModalPatternQueries> modalRelationQueries | ||
91 | |||
92 | Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allPatterns | ||
45 | } | 93 | } |
94 | |||
46 | enum TypeInferenceMethod { | 95 | enum TypeInferenceMethod { |
47 | Generic, PreliminaryAnalysis | 96 | Generic, |
97 | PreliminaryAnalysis | ||
48 | } | 98 | } |
49 | 99 | ||
50 | class ModelGenerationMethodProvider { | 100 | class ModelGenerationMethodProvider { |
51 | private val PatternProvider patternProvider = new PatternProvider | 101 | val PatternProvider patternProvider = new PatternProvider |
52 | private val RefinementRuleProvider refinementRuleProvider = new RefinementRuleProvider | 102 | val RefinementRuleProvider refinementRuleProvider = new RefinementRuleProvider |
53 | private val GoalConstraintProvider goalConstraintProvider = new GoalConstraintProvider | 103 | val GoalConstraintProvider goalConstraintProvider = new GoalConstraintProvider |
54 | 104 | val relationConstraintCalculator = new RelationConstraintCalculator | |
55 | public def ModelGenerationMethod createModelGenerationMethod( | 105 | |
106 | def ModelGenerationMethod createModelGenerationMethod( | ||
56 | LogicProblem logicProblem, | 107 | LogicProblem logicProblem, |
57 | PartialInterpretation emptySolution, | 108 | PartialInterpretation emptySolution, |
58 | ReasonerWorkspace workspace, | 109 | ReasonerWorkspace workspace, |
59 | boolean nameNewElements, | 110 | boolean nameNewElements, |
60 | TypeInferenceMethod typeInferenceMethod, | 111 | TypeInferenceMethod typeInferenceMethod, |
61 | ScopePropagator scopePropagator, | 112 | ScopePropagatorStrategy scopePropagatorStrategy, |
62 | DocumentationLevel debugLevel, | 113 | Collection<LinearTypeConstraintHint> hints, |
63 | boolean objectCreationCosts | 114 | DocumentationLevel debugLevel |
64 | ) { | 115 | ) { |
65 | val statistics = new ModelGenerationStatistics | 116 | val statistics = new ModelGenerationStatistics |
66 | val writeFiles = (debugLevel === DocumentationLevel.NORMAL || debugLevel === DocumentationLevel.FULL) | 117 | val writeFiles = (debugLevel === DocumentationLevel.NORMAL || debugLevel === DocumentationLevel.FULL) |
67 | 118 | ||
68 | val Set<PQuery> existingQueries = logicProblem | 119 | val Set<PQuery> existingQueries = logicProblem.relations.map[annotations].flatten.filter(TransfomedViatraQuery). |
69 | .relations | 120 | map[it.patternPQuery as PQuery].toSet |
70 | .map[annotations] | 121 | |
71 | .flatten | 122 | val relationConstraints = relationConstraintCalculator.calculateRelationConstraints(logicProblem) |
72 | .filter(TransfomedViatraQuery) | 123 | val queries = patternProvider.generateQueries(logicProblem, emptySolution, statistics, existingQueries, |
73 | .map[it.patternPQuery as PQuery] | 124 | workspace, typeInferenceMethod, scopePropagatorStrategy, relationConstraints, hints, writeFiles) |
74 | .toSet | 125 | val scopePropagator = createScopePropagator(scopePropagatorStrategy, emptySolution, hints, queries, statistics) |
75 | 126 | scopePropagator.propagateAllScopeConstraints | |
76 | val queries = patternProvider.generateQueries(logicProblem,emptySolution,statistics,existingQueries,workspace,typeInferenceMethod,writeFiles) | 127 | val objectRefinementRules = refinementRuleProvider.createObjectRefinementRules(logicProblem, emptySolution, |
77 | val //LinkedHashMap<Pair<Relation, ? extends Type>, BatchTransformationRule<GenericPatternMatch, ViatraQueryMatcher<GenericPatternMatch>>> | 128 | queries, scopePropagator, nameNewElements, statistics) |
78 | objectRefinementRules = refinementRuleProvider.createObjectRefinementRules(logicProblem, emptySolution, queries,scopePropagator,nameNewElements,statistics) | 129 | val relationRefinementRules = refinementRuleProvider.createRelationRefinementRules(queries, scopePropagator, |
79 | val relationRefinementRules = refinementRuleProvider.createRelationRefinementRules(queries,statistics) | 130 | statistics) |
80 | 131 | ||
81 | val unfinishedMultiplicities = goalConstraintProvider.getUnfinishedMultiplicityQueries(logicProblem,queries,objectCreationCosts) | 132 | val unfinishedMultiplicities = goalConstraintProvider.getUnfinishedMultiplicityQueries(logicProblem,queries) |
133 | |||
82 | val unfinishedWF = queries.getUnfinishedWFQueries.values | 134 | val unfinishedWF = queries.getUnfinishedWFQueries.values |
83 | 135 | ||
136 | val modalRelationQueriesBuilder = ImmutableMap.builder | ||
137 | for (entry : queries.modalRelationQueries.entrySet) { | ||
138 | val annotation = entry.key.annotations.filter(TransfomedViatraQuery).head | ||
139 | if (annotation !== null) { | ||
140 | modalRelationQueriesBuilder.put(annotation.patternFullyQualifiedName, entry.value) | ||
141 | } | ||
142 | } | ||
143 | val modalRelationQueries = modalRelationQueriesBuilder.build | ||
144 | |||
84 | val invalidWF = queries.getInvalidWFQueries.values | 145 | val invalidWF = queries.getInvalidWFQueries.values |
85 | 146 | ||
86 | val mustUnitPropagationPreconditions = queries.getMustUnitPropagationPreconditionPatterns | 147 | val mustUnitPropagationPreconditions = queries.getMustUnitPropagationPreconditionPatterns |
87 | val currentUnitPropagationPreconditions = queries.getCurrentUnitPropagationPreconditionPatterns | 148 | val currentUnitPropagationPreconditions = queries.getCurrentUnitPropagationPreconditionPatterns |
88 | 149 | ||
89 | return new ModelGenerationMethod( | 150 | return new ModelGenerationMethod( |
90 | statistics, | 151 | statistics, |
91 | objectRefinementRules.values, | 152 | objectRefinementRules.values, |
@@ -95,7 +156,45 @@ class ModelGenerationMethodProvider { | |||
95 | invalidWF, | 156 | invalidWF, |
96 | mustUnitPropagationPreconditions, | 157 | mustUnitPropagationPreconditions, |
97 | currentUnitPropagationPreconditions, | 158 | currentUnitPropagationPreconditions, |
159 | modalRelationQueries, | ||
98 | queries.allQueries | 160 | queries.allQueries |
99 | ) | 161 | ) |
100 | } | 162 | } |
163 | |||
164 | private def createScopePropagator(ScopePropagatorStrategy scopePropagatorStrategy, | ||
165 | PartialInterpretation emptySolution, Collection<LinearTypeConstraintHint> hints, GeneratedPatterns queries, | ||
166 | ModelGenerationStatistics statistics) { | ||
167 | if (!hints.empty && !(scopePropagatorStrategy instanceof ScopePropagatorStrategy.Polyhedral)) { | ||
168 | throw new IllegalArgumentException("Only the Polyhedral scope propagator strategy can use hints.") | ||
169 | } | ||
170 | switch (scopePropagatorStrategy) { | ||
171 | case ScopePropagatorStrategy.None, | ||
172 | case ScopePropagatorStrategy.Basic: | ||
173 | new ScopePropagator(emptySolution, statistics) | ||
174 | case ScopePropagatorStrategy.BasicTypeHierarchy: | ||
175 | new TypeHierarchyScopePropagator(emptySolution, statistics) | ||
176 | ScopePropagatorStrategy.Polyhedral: { | ||
177 | val types = queries.refineObjectQueries.keySet.map[newType].toSet | ||
178 | val allPatternsByName = queries.allQueries.toMap[fullyQualifiedName] | ||
179 | val solver = switch (scopePropagatorStrategy.solver) { | ||
180 | case Z3Integer: | ||
181 | new Z3PolyhedronSolver(false, scopePropagatorStrategy.timeoutSeconds) | ||
182 | case Z3Real: | ||
183 | new Z3PolyhedronSolver(true, scopePropagatorStrategy.timeoutSeconds) | ||
184 | case Cbc: | ||
185 | new CbcPolyhedronSolver(false, scopePropagatorStrategy.timeoutSeconds, true) | ||
186 | case Clp: | ||
187 | new CbcPolyhedronSolver(true, scopePropagatorStrategy.timeoutSeconds, true) | ||
188 | default: | ||
189 | throw new IllegalArgumentException("Unknown polyhedron solver: " + | ||
190 | scopePropagatorStrategy.solver) | ||
191 | } | ||
192 | new PolyhedronScopePropagator(emptySolution, statistics, types, queries.multiplicityConstraintQueries, | ||
193 | queries.hasElementInContainmentQuery, allPatternsByName, hints, solver, | ||
194 | scopePropagatorStrategy.requiresUpperBoundIndexing, scopePropagatorStrategy.updateHeuristic) | ||
195 | } | ||
196 | default: | ||
197 | throw new IllegalArgumentException("Unknown scope propagator strategy: " + scopePropagatorStrategy) | ||
198 | } | ||
199 | } | ||
101 | } | 200 | } |