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