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