diff options
author | Kristóf Marussy <kris7topher@gmail.com> | 2019-08-01 01:00:12 +0200 |
---|---|---|
committer | Kristóf Marussy <kris7topher@gmail.com> | 2019-08-01 01:00:12 +0200 |
commit | 7021a4d1f2805ebf3145cbc3893761d12f23361f (patch) | |
tree | b75c51136d3b593f94bf517a8552a1dbf8abdd2b /Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/ModelGenerationMethodProvider.xtend | |
parent | Build Cbc wrapper under Ubuntu 18.04 (diff) | |
download | VIATRA-Generator-7021a4d1f2805ebf3145cbc3893761d12f23361f.tar.gz VIATRA-Generator-7021a4d1f2805ebf3145cbc3893761d12f23361f.tar.zst VIATRA-Generator-7021a4d1f2805ebf3145cbc3893761d12f23361f.zip |
Configurability and better statistics for measurements
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 | 54 |
1 files changed, 42 insertions, 12 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 4b278188..8e061b63 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 | |||
@@ -27,6 +27,7 @@ import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher | |||
27 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery | 27 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery |
28 | import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRule | 28 | import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRule |
29 | import org.eclipse.xtend.lib.annotations.Data | 29 | import org.eclipse.xtend.lib.annotations.Data |
30 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Z3PolyhedronSolver | ||
30 | 31 | ||
31 | class ModelGenerationStatistics { | 32 | class ModelGenerationStatistics { |
32 | public var long transformationExecutionTime = 0 | 33 | public var long transformationExecutionTime = 0 |
@@ -35,7 +36,25 @@ class ModelGenerationStatistics { | |||
35 | transformationExecutionTime += amount | 36 | transformationExecutionTime += amount |
36 | } | 37 | } |
37 | 38 | ||
38 | public var long PreliminaryTypeAnalisisTime = 0 | 39 | public var long scopePropagationTime = 0 |
40 | |||
41 | synchronized def addScopePropagationTime(long amount) { | ||
42 | scopePropagationTime += amount | ||
43 | } | ||
44 | |||
45 | public var long preliminaryTypeAnalisisTime = 0 | ||
46 | |||
47 | public var int decisionsTried = 0 | ||
48 | |||
49 | synchronized def incrementDecisionCount() { | ||
50 | decisionsTried++ | ||
51 | } | ||
52 | |||
53 | public var int scopePropagatorInvocations | ||
54 | |||
55 | synchronized def incrementScopePropagationCount() { | ||
56 | scopePropagatorInvocations++ | ||
57 | } | ||
39 | } | 58 | } |
40 | 59 | ||
41 | @Data class ModelGenerationMethod { | 60 | @Data class ModelGenerationMethod { |
@@ -84,12 +103,12 @@ class ModelGenerationMethodProvider { | |||
84 | val relationConstraints = relationConstraintCalculator.calculateRelationConstraints(logicProblem) | 103 | val relationConstraints = relationConstraintCalculator.calculateRelationConstraints(logicProblem) |
85 | val queries = patternProvider.generateQueries(logicProblem, emptySolution, statistics, existingQueries, | 104 | val queries = patternProvider.generateQueries(logicProblem, emptySolution, statistics, existingQueries, |
86 | workspace, typeInferenceMethod, scopePropagatorStrategy, relationConstraints, writeFiles) | 105 | workspace, typeInferenceMethod, scopePropagatorStrategy, relationConstraints, writeFiles) |
87 | val scopePropagator = createScopePropagator(scopePropagatorStrategy, emptySolution, queries) | 106 | val scopePropagator = createScopePropagator(scopePropagatorStrategy, emptySolution, queries, statistics) |
88 | scopePropagator.propagateAllScopeConstraints | 107 | scopePropagator.propagateAllScopeConstraints |
89 | val // LinkedHashMap<Pair<Relation, ? extends Type>, BatchTransformationRule<GenericPatternMatch, ViatraQueryMatcher<GenericPatternMatch>>> | 108 | val objectRefinementRules = refinementRuleProvider.createObjectRefinementRules(queries, scopePropagator, |
90 | objectRefinementRules = refinementRuleProvider.createObjectRefinementRules(queries, scopePropagator, | ||
91 | nameNewElements, statistics) | 109 | nameNewElements, statistics) |
92 | val relationRefinementRules = refinementRuleProvider.createRelationRefinementRules(queries, statistics) | 110 | val relationRefinementRules = refinementRuleProvider.createRelationRefinementRules(queries, scopePropagator, |
111 | statistics) | ||
93 | 112 | ||
94 | val unfinishedMultiplicities = goalConstraintProvider.getUnfinishedMultiplicityQueries(queries) | 113 | val unfinishedMultiplicities = goalConstraintProvider.getUnfinishedMultiplicityQueries(queries) |
95 | val unfinishedWF = queries.getUnfinishedWFQueries.values | 114 | val unfinishedWF = queries.getUnfinishedWFQueries.values |
@@ -118,15 +137,26 @@ class ModelGenerationMethodProvider { | |||
118 | } | 137 | } |
119 | 138 | ||
120 | private def createScopePropagator(ScopePropagatorStrategy scopePropagatorStrategy, | 139 | private def createScopePropagator(ScopePropagatorStrategy scopePropagatorStrategy, |
121 | PartialInterpretation emptySolution, GeneratedPatterns queries) { | 140 | PartialInterpretation emptySolution, GeneratedPatterns queries, ModelGenerationStatistics statistics) { |
122 | switch (scopePropagatorStrategy) { | 141 | switch (scopePropagatorStrategy) { |
123 | case BasicTypeHierarchy: | 142 | case ScopePropagatorStrategy.BasicTypeHierarchy: |
124 | new ScopePropagator(emptySolution) | 143 | new ScopePropagator(emptySolution, statistics) |
125 | case PolyhedralTypeHierarchy, | 144 | ScopePropagatorStrategy.Polyhedral: { |
126 | case PolyhedralRelations: { | ||
127 | val types = queries.refineObjectQueries.keySet.map[newType].toSet | 145 | val types = queries.refineObjectQueries.keySet.map[newType].toSet |
128 | val solver = new CbcPolyhedronSolver | 146 | val solver = switch (scopePropagatorStrategy.solver) { |
129 | new PolyhedronScopePropagator(emptySolution, types, queries.multiplicityConstraintQueries, | 147 | case Z3Integer: |
148 | new Z3PolyhedronSolver(false, scopePropagatorStrategy.timeoutSeconds) | ||
149 | case Z3Real: | ||
150 | new Z3PolyhedronSolver(true, scopePropagatorStrategy.timeoutSeconds) | ||
151 | case Cbc: | ||
152 | new CbcPolyhedronSolver(false, scopePropagatorStrategy.timeoutSeconds, true) | ||
153 | case Clp: | ||
154 | new CbcPolyhedronSolver(true, scopePropagatorStrategy.timeoutSeconds, true) | ||
155 | default: | ||
156 | throw new IllegalArgumentException("Unknown polyhedron solver: " + | ||
157 | scopePropagatorStrategy.solver) | ||
158 | } | ||
159 | new PolyhedronScopePropagator(emptySolution, statistics, types, queries.multiplicityConstraintQueries, | ||
130 | queries.hasElementInContainmentQuery, solver, scopePropagatorStrategy.requiresUpperBoundIndexing) | 160 | queries.hasElementInContainmentQuery, solver, scopePropagatorStrategy.requiresUpperBoundIndexing) |
131 | } | 161 | } |
132 | default: | 162 | default: |