diff options
author | Kristóf Marussy <kris7topher@gmail.com> | 2019-08-14 18:26:33 +0200 |
---|---|---|
committer | Kristóf Marussy <kris7topher@gmail.com> | 2019-08-14 18:26:33 +0200 |
commit | fc84d3fe670331bc89fb1e4c44104bc1fc811438 (patch) | |
tree | 466da8333151c51d2e17075600f9452ed35835da /Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend | |
parent | Be more lenient with rounding IP solver results (diff) | |
download | VIATRA-Generator-fc84d3fe670331bc89fb1e4c44104bc1fc811438.tar.gz VIATRA-Generator-fc84d3fe670331bc89fb1e4c44104bc1fc811438.tar.zst VIATRA-Generator-fc84d3fe670331bc89fb1e4c44104bc1fc811438.zip |
Measurements WIP
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 | 35 |
1 files changed, 28 insertions, 7 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 23632d4d..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 | |||
@@ -5,6 +5,7 @@ import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel | |||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | 5 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem |
6 | 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 | 7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.CbcPolyhedronSolver |
8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearTypeConstraintHint | ||
8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.MultiplicityGoalConstraintCalculator | 9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.MultiplicityGoalConstraintCalculator |
9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronScopePropagator | 10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronScopePropagator |
10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.RelationConstraintCalculator | 11 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.RelationConstraintCalculator |
@@ -46,16 +47,28 @@ class ModelGenerationStatistics { | |||
46 | public var long preliminaryTypeAnalisisTime = 0 | 47 | public var long preliminaryTypeAnalisisTime = 0 |
47 | 48 | ||
48 | public var int decisionsTried = 0 | 49 | public var int decisionsTried = 0 |
49 | 50 | ||
50 | synchronized def incrementDecisionCount() { | 51 | synchronized def incrementDecisionCount() { |
51 | decisionsTried++ | 52 | decisionsTried++ |
52 | } | 53 | } |
54 | |||
55 | public var int transformationInvocations | ||
53 | 56 | ||
57 | synchronized def incrementTransformationCount() { | ||
58 | transformationInvocations++ | ||
59 | } | ||
60 | |||
54 | public var int scopePropagatorInvocations | 61 | public var int scopePropagatorInvocations |
55 | 62 | ||
56 | synchronized def incrementScopePropagationCount() { | 63 | synchronized def incrementScopePropagationCount() { |
57 | scopePropagatorInvocations++ | 64 | scopePropagatorInvocations++ |
58 | } | 65 | } |
66 | |||
67 | public var int scopePropagatorSolverInvocations | ||
68 | |||
69 | synchronized def incrementScopePropagationSolverCount() { | ||
70 | scopePropagatorSolverInvocations++ | ||
71 | } | ||
59 | } | 72 | } |
60 | 73 | ||
61 | @Data class ModelGenerationMethod { | 74 | @Data class ModelGenerationMethod { |
@@ -93,6 +106,7 @@ class ModelGenerationMethodProvider { | |||
93 | boolean nameNewElements, | 106 | boolean nameNewElements, |
94 | TypeInferenceMethod typeInferenceMethod, | 107 | TypeInferenceMethod typeInferenceMethod, |
95 | ScopePropagatorStrategy scopePropagatorStrategy, | 108 | ScopePropagatorStrategy scopePropagatorStrategy, |
109 | Collection<LinearTypeConstraintHint> hints, | ||
96 | DocumentationLevel debugLevel | 110 | DocumentationLevel debugLevel |
97 | ) { | 111 | ) { |
98 | val statistics = new ModelGenerationStatistics | 112 | val statistics = new ModelGenerationStatistics |
@@ -103,8 +117,8 @@ class ModelGenerationMethodProvider { | |||
103 | 117 | ||
104 | val relationConstraints = relationConstraintCalculator.calculateRelationConstraints(logicProblem) | 118 | val relationConstraints = relationConstraintCalculator.calculateRelationConstraints(logicProblem) |
105 | val queries = patternProvider.generateQueries(logicProblem, emptySolution, statistics, existingQueries, | 119 | val queries = patternProvider.generateQueries(logicProblem, emptySolution, statistics, existingQueries, |
106 | workspace, typeInferenceMethod, scopePropagatorStrategy, relationConstraints, writeFiles) | 120 | workspace, typeInferenceMethod, scopePropagatorStrategy, relationConstraints, hints, writeFiles) |
107 | val scopePropagator = createScopePropagator(scopePropagatorStrategy, emptySolution, queries, statistics) | 121 | val scopePropagator = createScopePropagator(scopePropagatorStrategy, emptySolution, hints, queries, statistics) |
108 | scopePropagator.propagateAllScopeConstraints | 122 | scopePropagator.propagateAllScopeConstraints |
109 | val objectRefinementRules = refinementRuleProvider.createObjectRefinementRules(queries, scopePropagator, | 123 | val objectRefinementRules = refinementRuleProvider.createObjectRefinementRules(queries, scopePropagator, |
110 | nameNewElements, statistics) | 124 | nameNewElements, statistics) |
@@ -138,14 +152,20 @@ class ModelGenerationMethodProvider { | |||
138 | } | 152 | } |
139 | 153 | ||
140 | private def createScopePropagator(ScopePropagatorStrategy scopePropagatorStrategy, | 154 | private def createScopePropagator(ScopePropagatorStrategy scopePropagatorStrategy, |
141 | PartialInterpretation emptySolution, GeneratedPatterns queries, ModelGenerationStatistics statistics) { | 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 | } | ||
142 | switch (scopePropagatorStrategy) { | 160 | switch (scopePropagatorStrategy) { |
143 | case ScopePropagatorStrategy.Count: | 161 | case ScopePropagatorStrategy.None, |
162 | case ScopePropagatorStrategy.Basic: | ||
144 | new ScopePropagator(emptySolution, statistics) | 163 | new ScopePropagator(emptySolution, statistics) |
145 | case ScopePropagatorStrategy.BasicTypeHierarchy: | 164 | case ScopePropagatorStrategy.BasicTypeHierarchy: |
146 | new TypeHierarchyScopePropagator(emptySolution, statistics) | 165 | new TypeHierarchyScopePropagator(emptySolution, statistics) |
147 | ScopePropagatorStrategy.Polyhedral: { | 166 | ScopePropagatorStrategy.Polyhedral: { |
148 | val types = queries.refineObjectQueries.keySet.map[newType].toSet | 167 | val types = queries.refineObjectQueries.keySet.map[newType].toSet |
168 | val allPatternsByName = queries.allQueries.toMap[fullyQualifiedName] | ||
149 | val solver = switch (scopePropagatorStrategy.solver) { | 169 | val solver = switch (scopePropagatorStrategy.solver) { |
150 | case Z3Integer: | 170 | case Z3Integer: |
151 | new Z3PolyhedronSolver(false, scopePropagatorStrategy.timeoutSeconds) | 171 | new Z3PolyhedronSolver(false, scopePropagatorStrategy.timeoutSeconds) |
@@ -160,7 +180,8 @@ class ModelGenerationMethodProvider { | |||
160 | scopePropagatorStrategy.solver) | 180 | scopePropagatorStrategy.solver) |
161 | } | 181 | } |
162 | new PolyhedronScopePropagator(emptySolution, statistics, types, queries.multiplicityConstraintQueries, | 182 | new PolyhedronScopePropagator(emptySolution, statistics, types, queries.multiplicityConstraintQueries, |
163 | queries.hasElementInContainmentQuery, solver, scopePropagatorStrategy.requiresUpperBoundIndexing) | 183 | queries.hasElementInContainmentQuery, allPatternsByName, hints, solver, |
184 | scopePropagatorStrategy.requiresUpperBoundIndexing, scopePropagatorStrategy.updateHeuristic) | ||
164 | } | 185 | } |
165 | default: | 186 | default: |
166 | throw new IllegalArgumentException("Unknown scope propagator strategy: " + scopePropagatorStrategy) | 187 | throw new IllegalArgumentException("Unknown scope propagator strategy: " + scopePropagatorStrategy) |