diff options
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver')
14 files changed, 830 insertions, 139 deletions
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ModelGenerationMethodBasedGlobalConstraint.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ModelGenerationMethodBasedGlobalConstraint.xtend index 9ef5e091..691e0645 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ModelGenerationMethodBasedGlobalConstraint.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ModelGenerationMethodBasedGlobalConstraint.xtend | |||
@@ -1,7 +1,6 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner | 1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner |
2 | 2 | ||
3 | import org.eclipse.viatra.dse.objectives.IGlobalConstraint | 3 | import org.eclipse.viatra.dse.objectives.IGlobalConstraint |
4 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod | ||
5 | 4 | ||
6 | abstract class ModelGenerationMethodBasedGlobalConstraint implements IGlobalConstraint { | 5 | abstract class ModelGenerationMethodBasedGlobalConstraint implements IGlobalConstraint { |
7 | val protected ModelGenerationMethod method | 6 | val protected ModelGenerationMethod method |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ModelGenerationMethodProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ModelGenerationMethodProvider.xtend new file mode 100644 index 00000000..25137eba --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ModelGenerationMethodProvider.xtend | |||
@@ -0,0 +1,201 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner | ||
2 | |||
3 | import com.google.common.collect.ImmutableMap | ||
4 | import com.google.common.collect.ImmutableSet | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | ||
7 | import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransfomedViatraQuery | ||
8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationStatistics | ||
9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.CachingSimplePolyhedronScopePropagatorStrategy | ||
10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.CbcPolyhedronSolver | ||
11 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearTypeConstraintHint | ||
12 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.MultiplicityGoalConstraintCalculator | ||
13 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronExtensionOperator | ||
14 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronScopePropagator | ||
15 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.RelationConstraintCalculator | ||
16 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagator | ||
17 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy | ||
18 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.TypeHierarchyScopePropagator | ||
19 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Z3PolyhedronSolver | ||
20 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.GeneratedPatterns | ||
21 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.ModalPatternQueries | ||
22 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.PatternProvider | ||
23 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules.GoalConstraintProvider | ||
24 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.rules.RefinementRuleProvider | ||
25 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | ||
26 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.DiversityChecker | ||
27 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ViatraReasonerSolutionSaver | ||
28 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ThreeValuedCostObjectiveProvider | ||
29 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace | ||
30 | import java.util.Collection | ||
31 | import java.util.List | ||
32 | import java.util.Map | ||
33 | import java.util.Set | ||
34 | import org.eclipse.viatra.dse.objectives.IObjective | ||
35 | import org.eclipse.viatra.query.runtime.api.GenericQueryGroup | ||
36 | import org.eclipse.viatra.query.runtime.api.IPatternMatch | ||
37 | import org.eclipse.viatra.query.runtime.api.IQuerySpecification | ||
38 | import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine | ||
39 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher | ||
40 | import org.eclipse.viatra.query.runtime.emf.EMFScope | ||
41 | import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint | ||
42 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery | ||
43 | import org.eclipse.viatra.transformation.runtime.emf.rules.batch.BatchTransformationRule | ||
44 | import org.eclipse.xtend.lib.annotations.Data | ||
45 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ExtendedPolyhedronScopePropagatorStrategy | ||
46 | |||
47 | @Data class ModelGenerationMethod { | ||
48 | ModelGenerationStatistics statistics | ||
49 | |||
50 | Collection<? extends BatchTransformationRule<?, ?>> objectRefinementRules | ||
51 | Collection<? extends BatchTransformationRule<?, ?>> relationRefinementRules | ||
52 | |||
53 | List<MultiplicityGoalConstraintCalculator> unfinishedMultiplicities | ||
54 | |||
55 | Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWF | ||
56 | |||
57 | Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> invalidWF | ||
58 | |||
59 | Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> mustUnitPropagationPreconditions | ||
60 | Map<PConstraint, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> currentUnitPropagationPreconditions | ||
61 | |||
62 | Map<String, ModalPatternQueries> modalRelationQueries | ||
63 | |||
64 | Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> allPatterns | ||
65 | |||
66 | Collection<IObjective> costObjectives | ||
67 | boolean optimizationProblem | ||
68 | ViatraReasonerSolutionSaver solutionSaver | ||
69 | } | ||
70 | |||
71 | class ModelGenerationMethodProvider { | ||
72 | val PatternProvider patternProvider = new PatternProvider | ||
73 | val RefinementRuleProvider refinementRuleProvider = new RefinementRuleProvider | ||
74 | val GoalConstraintProvider goalConstraintProvider = new GoalConstraintProvider | ||
75 | val relationConstraintCalculator = new RelationConstraintCalculator | ||
76 | |||
77 | def ModelGenerationMethod createModelGenerationMethod( | ||
78 | LogicProblem logicProblem, | ||
79 | PartialInterpretation emptySolution, | ||
80 | ReasonerWorkspace workspace, | ||
81 | ViatraReasonerConfiguration config | ||
82 | ) { | ||
83 | val statistics = new ModelGenerationStatistics | ||
84 | val debugLevel = config.documentationLevel | ||
85 | val writeFiles = (debugLevel === DocumentationLevel.NORMAL || debugLevel === DocumentationLevel.FULL) | ||
86 | |||
87 | val Set<PQuery> existingQueries = logicProblem.relations.map[annotations].flatten.filter(TransfomedViatraQuery). | ||
88 | map[it.patternPQuery as PQuery].toSet | ||
89 | |||
90 | val relationConstraints = relationConstraintCalculator.calculateRelationConstraints(logicProblem) | ||
91 | val queries = patternProvider.generateQueries(logicProblem, emptySolution, statistics, existingQueries, | ||
92 | workspace, config.typeInferenceMethod, config.scopePropagatorStrategy, relationConstraints, config.hints, | ||
93 | config.unitPropagationPatternGenerators, writeFiles) | ||
94 | |||
95 | val unfinishedMultiplicities = goalConstraintProvider.getUnfinishedMultiplicityQueries(logicProblem, queries, | ||
96 | config.calculateObjectCreationCosts) | ||
97 | val unfinishedWF = queries.getUnfinishedWFQueries.values | ||
98 | val modalRelationQueriesBuilder = ImmutableMap.builder | ||
99 | for (entry : queries.modalRelationQueries.entrySet) { | ||
100 | val annotation = entry.key.annotations.filter(TransfomedViatraQuery).head | ||
101 | if (annotation !== null) { | ||
102 | modalRelationQueriesBuilder.put(annotation.patternFullyQualifiedName, entry.value) | ||
103 | } | ||
104 | } | ||
105 | val modalRelationQueries = modalRelationQueriesBuilder.build | ||
106 | val invalidWF = queries.getInvalidWFQueries.values | ||
107 | val mustUnitPropagationPreconditions = queries.getMustUnitPropagationPreconditionPatterns | ||
108 | val currentUnitPropagationPreconditions = queries.getCurrentUnitPropagationPreconditionPatterns | ||
109 | val queriesToPrepare = ImmutableSet.builder.addAll(queries.refineObjectQueries.values).addAll( | ||
110 | queries.refineTypeQueries.values).addAll(queries.refineRelationQueries.values).addAll( | ||
111 | queries.mustRelationPropagationQueries.values).addAll(queries.multiplicityConstraintQueries.values.flatMap [ | ||
112 | allQueries | ||
113 | ]).addAll(queries.unfinishedWFQueries.values).addAll(queries.invalidWFQueries.values).addAll( | ||
114 | queries.mustUnitPropagationPreconditionPatterns.values).addAll( | ||
115 | queries.currentUnitPropagationPreconditionPatterns.values).add(queries.hasElementInContainmentQuery).build | ||
116 | val queryEngine = ViatraQueryEngine.on(new EMFScope(emptySolution)) | ||
117 | GenericQueryGroup.of(queriesToPrepare).prepare(queryEngine) | ||
118 | |||
119 | val objectiveProvider = new ThreeValuedCostObjectiveProvider(queryEngine, emptySolution, modalRelationQueries) | ||
120 | val transformedObjectives = objectiveProvider.getCostObjectives(config.costObjectives) | ||
121 | |||
122 | val solutionSaver = new ViatraReasonerSolutionSaver(transformedObjectives.leveledExtremalObjectives, | ||
123 | config.solutionScope.numberOfRequiredSolutions, DiversityChecker.of(config.diversityRequirement)) | ||
124 | |||
125 | val allHints = ImmutableSet.builder | ||
126 | allHints.addAll(config.hints) | ||
127 | for (hint : transformedObjectives.hints) { | ||
128 | hint.boundsProvider = solutionSaver | ||
129 | allHints.add(hint) | ||
130 | } | ||
131 | |||
132 | val scopePropagator = createScopePropagator(config.scopePropagatorStrategy, emptySolution, allHints.build, | ||
133 | transformedObjectives.extensionOperators, queries, statistics) | ||
134 | scopePropagator.propagateAllScopeConstraints | ||
135 | val unitRulePropagator = refinementRuleProvider.createUnitPrulePropagator(logicProblem, emptySolution, queries, | ||
136 | scopePropagator, statistics) | ||
137 | val objectRefinementRules = refinementRuleProvider.createObjectRefinementRules(logicProblem, emptySolution, | ||
138 | queries, unitRulePropagator, config.nameNewElements, statistics) | ||
139 | val relationRefinementRules = refinementRuleProvider.createRelationRefinementRules(queries, unitRulePropagator, | ||
140 | statistics) | ||
141 | |||
142 | return new ModelGenerationMethod( | ||
143 | statistics, | ||
144 | objectRefinementRules.values, | ||
145 | relationRefinementRules.values, | ||
146 | unfinishedMultiplicities, | ||
147 | unfinishedWF, | ||
148 | invalidWF, | ||
149 | mustUnitPropagationPreconditions, | ||
150 | currentUnitPropagationPreconditions, | ||
151 | modalRelationQueries, | ||
152 | queries.allQueries, | ||
153 | transformedObjectives.objectives, | ||
154 | transformedObjectives.optimizationProblem, | ||
155 | solutionSaver | ||
156 | ) | ||
157 | } | ||
158 | |||
159 | private def createScopePropagator(ScopePropagatorStrategy scopePropagatorStrategy, | ||
160 | PartialInterpretation emptySolution, Collection<LinearTypeConstraintHint> hints, | ||
161 | Collection<PolyhedronExtensionOperator> extensionOperators, GeneratedPatterns queries, | ||
162 | ModelGenerationStatistics statistics) { | ||
163 | if (!hints.empty && !(scopePropagatorStrategy instanceof ScopePropagatorStrategy.Polyhedral)) { | ||
164 | throw new IllegalArgumentException("Only the Polyhedral scope propagator strategy can use hints.") | ||
165 | } | ||
166 | switch (scopePropagatorStrategy) { | ||
167 | case ScopePropagatorStrategy.None, | ||
168 | case ScopePropagatorStrategy.Basic: | ||
169 | new ScopePropagator(emptySolution, statistics) | ||
170 | case ScopePropagatorStrategy.BasicTypeHierarchy: | ||
171 | new TypeHierarchyScopePropagator(emptySolution, statistics) | ||
172 | ScopePropagatorStrategy.Polyhedral: { | ||
173 | val types = queries.refineObjectQueries.keySet.map[newType].toSet | ||
174 | val allPatternsByName = queries.allQueries.toMap[fullyQualifiedName] | ||
175 | val solver = switch (scopePropagatorStrategy.solver) { | ||
176 | case Z3Integer: | ||
177 | new Z3PolyhedronSolver(false, scopePropagatorStrategy.timeoutSeconds) | ||
178 | case Z3Real: | ||
179 | new Z3PolyhedronSolver(true, scopePropagatorStrategy.timeoutSeconds) | ||
180 | case Cbc: | ||
181 | new CbcPolyhedronSolver(false, scopePropagatorStrategy.timeoutSeconds, true) | ||
182 | case Clp: | ||
183 | new CbcPolyhedronSolver(true, scopePropagatorStrategy.timeoutSeconds, true) | ||
184 | default: | ||
185 | throw new IllegalArgumentException("Unknown polyhedron solver: " + | ||
186 | scopePropagatorStrategy.solver) | ||
187 | } | ||
188 | val strategy = if (extensionOperators.empty) { | ||
189 | new CachingSimplePolyhedronScopePropagatorStrategy(solver, statistics) | ||
190 | } else { | ||
191 | new ExtendedPolyhedronScopePropagatorStrategy(solver, extensionOperators, statistics) | ||
192 | } | ||
193 | new PolyhedronScopePropagator(emptySolution, statistics, types, queries.multiplicityConstraintQueries, | ||
194 | queries.hasElementInContainmentQuery, allPatternsByName, hints, strategy, | ||
195 | scopePropagatorStrategy.requiresUpperBoundIndexing, scopePropagatorStrategy.updateHeuristic) | ||
196 | } | ||
197 | default: | ||
198 | throw new IllegalArgumentException("Unknown scope propagator strategy: " + scopePropagatorStrategy) | ||
199 | } | ||
200 | } | ||
201 | } | ||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend index c333feca..8e992741 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend | |||
@@ -1,7 +1,5 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner | 1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner |
2 | 2 | ||
3 | import com.google.common.collect.ImmutableList | ||
4 | import com.google.common.collect.Lists | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel | 3 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel |
6 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner | 4 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner |
7 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException | 5 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException |
@@ -11,7 +9,6 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | |||
11 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage | 9 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage |
12 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory | 10 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory |
13 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult | 11 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult |
14 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethodProvider | ||
15 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy | 12 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy |
16 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.PartialInterpretationInitialiser | 13 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.PartialInterpretationInitialiser |
17 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | 14 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation |
@@ -22,7 +19,6 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.sta | |||
22 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.statecoder.PairwiseNeighbourhoodBasedStateCoderFactory | 19 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.statecoder.PairwiseNeighbourhoodBasedStateCoderFactory |
23 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.BasicScopeGlobalConstraint | 20 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.BasicScopeGlobalConstraint |
24 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.BestFirstStrategyForModelGeneration | 21 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.BestFirstStrategyForModelGeneration |
25 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.DiversityChecker | ||
26 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.InconsistentScopeGlobalConstraint | 22 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.InconsistentScopeGlobalConstraint |
27 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.LoggerSolutionFoundHandler | 23 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.LoggerSolutionFoundHandler |
28 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ModelGenerationCompositeObjective | 24 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ModelGenerationCompositeObjective |
@@ -32,11 +28,8 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.PunishSizeObjective | |||
32 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ScopeObjective | 28 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ScopeObjective |
33 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.SurelyViolatedObjectiveGlobalConstraint | 29 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.SurelyViolatedObjectiveGlobalConstraint |
34 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.UnfinishedMultiplicityObjective | 30 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.UnfinishedMultiplicityObjective |
35 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ViatraReasonerSolutionSaver | ||
36 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.WF2ObjectiveConverter | 31 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.WF2ObjectiveConverter |
37 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveKind | 32 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveKind |
38 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ThreeValuedCostElement | ||
39 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ThreeValuedCostObjective | ||
40 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace | 33 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace |
41 | import java.util.List | 34 | import java.util.List |
42 | import java.util.Map | 35 | import java.util.Map |
@@ -86,12 +79,7 @@ class ViatraReasoner extends LogicReasoner { | |||
86 | problem, | 79 | problem, |
87 | emptySolution, | 80 | emptySolution, |
88 | workspace, | 81 | workspace, |
89 | viatraConfig.nameNewElements, | 82 | viatraConfig |
90 | viatraConfig.typeInferenceMethod, | ||
91 | viatraConfig.calculateObjectCreationCosts, | ||
92 | viatraConfig.scopePropagatorStrategy, | ||
93 | viatraConfig.hints, | ||
94 | viatraConfig.documentationLevel | ||
95 | ) | 83 | ) |
96 | 84 | ||
97 | val compositeObjective = new ModelGenerationCompositeObjective( | 85 | val compositeObjective = new ModelGenerationCompositeObjective( |
@@ -111,45 +99,21 @@ class ViatraReasoner extends LogicReasoner { | |||
111 | dse.addObjective(punishObjective) | 99 | dse.addObjective(punishObjective) |
112 | } | 100 | } |
113 | 101 | ||
114 | val extremalObjectives = Lists.newArrayListWithExpectedSize(viatraConfig.costObjectives.size) | 102 | for (costObjective : method.costObjectives) { |
115 | for (entry : viatraConfig.costObjectives.indexed) { | ||
116 | val objectiveName = '''costObjective«entry.key»''' | ||
117 | val objectiveConfig = entry.value | ||
118 | val elementsBuilder = ImmutableList.builder | ||
119 | for (elementConfig : objectiveConfig.elements) { | ||
120 | val relationName = elementConfig.patternQualifiedName | ||
121 | val modalQueries = method.modalRelationQueries.get(relationName) | ||
122 | if (modalQueries === null) { | ||
123 | throw new IllegalArgumentException("Unknown relation: " + relationName) | ||
124 | } | ||
125 | elementsBuilder.add(new ThreeValuedCostElement( | ||
126 | modalQueries.currentQuery, | ||
127 | modalQueries.mayQuery, | ||
128 | modalQueries.mustQuery, | ||
129 | elementConfig.weight | ||
130 | )) | ||
131 | } | ||
132 | val costElements = elementsBuilder.build | ||
133 | val costObjective = new ThreeValuedCostObjective(objectiveName, costElements, objectiveConfig.kind, | ||
134 | objectiveConfig.threshold, 3) | ||
135 | dse.addObjective(costObjective) | 103 | dse.addObjective(costObjective) |
136 | if (objectiveConfig.findExtremum) { | ||
137 | extremalObjectives += costObjective | ||
138 | } | ||
139 | } | 104 | } |
140 | |||
141 | val numberOfRequiredSolutions = configuration.solutionScope.numberOfRequiredSolutions | 105 | val numberOfRequiredSolutions = configuration.solutionScope.numberOfRequiredSolutions |
142 | val solutionStore = if (extremalObjectives.empty) { | 106 | val solutionStore = if (method.optimizationProblem) { |
143 | new SolutionStore(numberOfRequiredSolutions) | ||
144 | } else { | ||
145 | new SolutionStore() | 107 | new SolutionStore() |
108 | } else { | ||
109 | new SolutionStore(numberOfRequiredSolutions) | ||
146 | } | 110 | } |
147 | solutionStore.registerSolutionFoundHandler(new LoggerSolutionFoundHandler(viatraConfig)) | 111 | solutionStore.registerSolutionFoundHandler(new LoggerSolutionFoundHandler(viatraConfig)) |
148 | val diversityChecker = DiversityChecker.of(viatraConfig.diversityRequirement) | ||
149 | val numericSolver = new NumericSolver(method, viatraConfig.runIntermediateNumericalConsistencyChecks, false) | 112 | val numericSolver = new NumericSolver(method, viatraConfig.runIntermediateNumericalConsistencyChecks, false) |
150 | val solutionSaver = new ViatraReasonerSolutionSaver(newArrayList(extremalObjectives), numberOfRequiredSolutions, | 113 | val solutionSaver = method.solutionSaver |
151 | diversityChecker, numericSolver) | 114 | solutionSaver.numericSolver = numericSolver |
152 | val solutionCopier = solutionSaver.solutionCopier | 115 | val solutionCopier = solutionSaver.solutionCopier |
116 | val diversityChecker = solutionSaver.diversityChecker | ||
153 | solutionStore.withSolutionSaver(solutionSaver) | 117 | solutionStore.withSolutionSaver(solutionSaver) |
154 | dse.solutionStore = solutionStore | 118 | dse.solutionStore = solutionStore |
155 | 119 | ||
@@ -184,7 +148,8 @@ class ViatraReasoner extends LogicReasoner { | |||
184 | dse.addTransformationRule(rule) | 148 | dse.addTransformationRule(rule) |
185 | } | 149 | } |
186 | 150 | ||
187 | val strategy = new BestFirstStrategyForModelGeneration(workspace, viatraConfig, method, solutionSaver, numericSolver) | 151 | val strategy = new BestFirstStrategyForModelGeneration(workspace, viatraConfig, method, solutionSaver, |
152 | numericSolver) | ||
188 | viatraConfig.progressMonitor.workedForwardTransformation | 153 | viatraConfig.progressMonitor.workedForwardTransformation |
189 | val transformationFinished = System.nanoTime | 154 | val transformationFinished = System.nanoTime |
190 | val transformationTime = transformationFinished - transformationStartTime | 155 | val transformationTime = transformationFinished - transformationStartTime |
@@ -210,14 +175,15 @@ class ViatraReasoner extends LogicReasoner { | |||
210 | it.value = (pair.value / 1000000) as int | 175 | it.value = (pair.value / 1000000) as int |
211 | ] | 176 | ] |
212 | } | 177 | } |
213 | for(x: 0..<strategy.times.size) { | 178 | for (x : 0 ..< strategy.times.size) { |
214 | it.entries += createStringStatisticEntry => [ | 179 | it.entries += createStringStatisticEntry => [ |
215 | it.name = '''Solution«x+1»DetailedStatistics''' | 180 | it.name = '''Solution«x+1»DetailedStatistics''' |
216 | it.value = strategy.times.get(x) | 181 | it.value = strategy.times.get(x) |
217 | ] | 182 | ] |
218 | } | 183 | } |
219 | it.entries += createIntStatisticEntry => [ | 184 | it.entries += createIntStatisticEntry => [ |
220 | it.name = "ExplorationInitializationTime" it.value = ((strategy.explorationStarted-transformationFinished)/1000000) as int | 185 | it.name = "ExplorationInitializationTime" |
186 | it.value = ((strategy.explorationStarted - transformationFinished) / 1000000) as int | ||
221 | ] | 187 | ] |
222 | it.entries += createIntStatisticEntry => [ | 188 | it.entries += createIntStatisticEntry => [ |
223 | it.name = "TransformationExecutionTime" | 189 | it.name = "TransformationExecutionTime" |
@@ -228,6 +194,10 @@ class ViatraReasoner extends LogicReasoner { | |||
228 | it.value = (method.statistics.scopePropagationTime / 1000000) as int | 194 | it.value = (method.statistics.scopePropagationTime / 1000000) as int |
229 | ] | 195 | ] |
230 | it.entries += createIntStatisticEntry => [ | 196 | it.entries += createIntStatisticEntry => [ |
197 | it.name = "MustRelationPropagationTime" | ||
198 | it.value = (method.statistics.mustRelationPropagationTime / 1000000) as int | ||
199 | ] | ||
200 | it.entries += createIntStatisticEntry => [ | ||
231 | it.name = "TypeAnalysisTime" | 201 | it.name = "TypeAnalysisTime" |
232 | it.value = (method.statistics.preliminaryTypeAnalisisTime / 1000000) as int | 202 | it.value = (method.statistics.preliminaryTypeAnalisisTime / 1000000) as int |
233 | ] | 203 | ] |
@@ -248,22 +218,28 @@ class ViatraReasoner extends LogicReasoner { | |||
248 | it.value = dse.numberOfStates as int | 218 | it.value = dse.numberOfStates as int |
249 | ] | 219 | ] |
250 | it.entries += createIntStatisticEntry => [ | 220 | it.entries += createIntStatisticEntry => [ |
251 | it.name = "ForwardTime" it.value = (strategy.forwardTime/1000000) as int | 221 | it.name = "ForwardTime" |
222 | it.value = (strategy.forwardTime / 1000000) as int | ||
252 | ] | 223 | ] |
253 | it.entries += createIntStatisticEntry => [ | 224 | it.entries += createIntStatisticEntry => [ |
254 | it.name = "BacktrackingTime" it.value = (strategy.backtrackingTime/1000000) as int | 225 | it.name = "BacktrackingTime" |
226 | it.value = (strategy.backtrackingTime / 1000000) as int | ||
255 | ] | 227 | ] |
256 | it.entries += createIntStatisticEntry => [ | 228 | it.entries += createIntStatisticEntry => [ |
257 | it.name = "GlobalConstraintEvaluationTime" it.value = (strategy.globalConstraintEvaluationTime/1000000) as int | 229 | it.name = "GlobalConstraintEvaluationTime" |
230 | it.value = (strategy.globalConstraintEvaluationTime / 1000000) as int | ||
258 | ] | 231 | ] |
259 | it.entries += createIntStatisticEntry => [ | 232 | it.entries += createIntStatisticEntry => [ |
260 | it.name = "FitnessCalculationTime" it.value = (strategy.fitnessCalculationTime/1000000) as int | 233 | it.name = "FitnessCalculationTime" |
234 | it.value = (strategy.fitnessCalculationTime / 1000000) as int | ||
261 | ] | 235 | ] |
262 | it.entries += createIntStatisticEntry => [ | 236 | it.entries += createIntStatisticEntry => [ |
263 | it.name = "SolutionCopyTime" it.value = (solutionSaver.totalCopierRuntime/1000000) as int | 237 | it.name = "SolutionCopyTime" |
238 | it.value = (solutionSaver.totalCopierRuntime / 1000000) as int | ||
264 | ] | 239 | ] |
265 | it.entries += createIntStatisticEntry => [ | 240 | it.entries += createIntStatisticEntry => [ |
266 | it.name = "ActivationSelectionTime" it.value = (strategy.activationSelector.runtime/1000000) as int | 241 | it.name = "ActivationSelectionTime" |
242 | it.value = (strategy.activationSelector.runtime / 1000000) as int | ||
267 | ] | 243 | ] |
268 | it.entries += createIntStatisticEntry => [ | 244 | it.entries += createIntStatisticEntry => [ |
269 | it.name = "Decisions" | 245 | it.name = "Decisions" |
@@ -282,27 +258,34 @@ class ViatraReasoner extends LogicReasoner { | |||
282 | it.value = method.statistics.scopePropagatorSolverInvocations | 258 | it.value = method.statistics.scopePropagatorSolverInvocations |
283 | ] | 259 | ] |
284 | it.entries += createIntStatisticEntry => [ | 260 | it.entries += createIntStatisticEntry => [ |
285 | it.name = "NumericalSolverSumTime" it.value = (strategy.numericSolver.runtime/1000000) as int | 261 | it.name = "NumericalSolverSumTime" |
262 | it.value = (strategy.numericSolver.runtime / 1000000) as int | ||
286 | ] | 263 | ] |
287 | it.entries += createIntStatisticEntry => [ | 264 | it.entries += createIntStatisticEntry => [ |
288 | it.name = "NumericalSolverProblemFormingTime" it.value = (strategy.numericSolver.solverFormingProblem/1000000) as int | 265 | it.name = "NumericalSolverProblemFormingTime" |
266 | it.value = (strategy.numericSolver.solverFormingProblem / 1000000) as int | ||
289 | ] | 267 | ] |
290 | it.entries += createIntStatisticEntry => [ | 268 | it.entries += createIntStatisticEntry => [ |
291 | it.name = "NumericalSolverSolvingTime" it.value = (strategy.numericSolver.solverSolvingProblem/1000000) as int | 269 | it.name = "NumericalSolverSolvingTime" |
270 | it.value = (strategy.numericSolver.solverSolvingProblem / 1000000) as int | ||
292 | ] | 271 | ] |
293 | it.entries += createIntStatisticEntry => [ | 272 | it.entries += createIntStatisticEntry => [ |
294 | it.name = "NumericalSolverInterpretingSolution" it.value = (strategy.numericSolver.solverSolution/1000000) as int | 273 | it.name = "NumericalSolverInterpretingSolution" |
274 | it.value = (strategy.numericSolver.solverSolution / 1000000) as int | ||
295 | ] | 275 | ] |
296 | it.entries += createIntStatisticEntry => [ | 276 | it.entries += createIntStatisticEntry => [ |
297 | it.name = "NumericalSolverCachingTime" it.value = (strategy.numericSolver.cachingTime/1000000) as int | 277 | it.name = "NumericalSolverCachingTime" |
278 | it.value = (strategy.numericSolver.cachingTime / 1000000) as int | ||
298 | ] | 279 | ] |
299 | it.entries += createIntStatisticEntry => [ | 280 | it.entries += createIntStatisticEntry => [ |
300 | it.name = "NumericalSolverCallNumber" it.value = strategy.numericSolver.numberOfSolverCalls | 281 | it.name = "NumericalSolverCallNumber" |
282 | it.value = strategy.numericSolver.numberOfSolverCalls | ||
301 | ] | 283 | ] |
302 | it.entries += createIntStatisticEntry => [ | 284 | it.entries += createIntStatisticEntry => [ |
303 | it.name = "NumericalSolverCachedAnswerNumber" it.value = strategy.numericSolver.numberOfCachedSolverCalls | 285 | it.name = "NumericalSolverCachedAnswerNumber" |
286 | it.value = strategy.numericSolver.numberOfCachedSolverCalls | ||
304 | ] | 287 | ] |
305 | if(diversityChecker.active) { | 288 | if (diversityChecker.active) { |
306 | it.entries += createIntStatisticEntry => [ | 289 | it.entries += createIntStatisticEntry => [ |
307 | it.name = "SolutionDiversityCheckTime" | 290 | it.name = "SolutionDiversityCheckTime" |
308 | it.value = (diversityChecker.totalRuntime / 1000000) as int | 291 | it.value = (diversityChecker.totalRuntime / 1000000) as int |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend index 0173124c..fbe6da9d 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend | |||
@@ -4,19 +4,20 @@ import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner | |||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration | 4 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration |
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration | 5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration |
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration | 6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration |
7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod | ||
8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeInferenceMethod | 7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeInferenceMethod |
8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearTypeConstraintHint | ||
9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedralScopePropagatorConstraints | 9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedralScopePropagatorConstraints |
10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedralScopePropagatorSolver | 10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedralScopePropagatorSolver |
11 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy | 11 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy |
12 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.UnitPropagationPatternGenerator | ||
12 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretationVisualiser | 13 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretationVisualiser |
14 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.CostObjectiveHint | ||
13 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveKind | 15 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveKind |
14 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveThreshold | 16 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveThreshold |
15 | import java.util.LinkedList | 17 | import java.util.LinkedList |
16 | import java.util.List | 18 | import java.util.List |
17 | import java.util.Set | 19 | import java.util.Set |
18 | import org.eclipse.xtext.xbase.lib.Functions.Function1 | 20 | import org.eclipse.xtext.xbase.lib.Functions.Function1 |
19 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearTypeConstraintHint | ||
20 | 21 | ||
21 | enum StateCoderStrategy { | 22 | enum StateCoderStrategy { |
22 | Neighbourhood, | 23 | Neighbourhood, |
@@ -77,6 +78,8 @@ class ViatraReasonerConfiguration extends LogicSolverConfiguration { | |||
77 | public var List<LinearTypeConstraintHint> hints = newArrayList | 78 | public var List<LinearTypeConstraintHint> hints = newArrayList |
78 | 79 | ||
79 | public var List<CostObjectiveConfiguration> costObjectives = newArrayList | 80 | public var List<CostObjectiveConfiguration> costObjectives = newArrayList |
81 | |||
82 | public var List<UnitPropagationPatternGenerator> unitPropagationPatternGenerators = newArrayList | ||
80 | } | 83 | } |
81 | 84 | ||
82 | class DiversityDescriptor { | 85 | class DiversityDescriptor { |
@@ -111,9 +114,11 @@ class CostObjectiveConfiguration { | |||
111 | public var ObjectiveKind kind | 114 | public var ObjectiveKind kind |
112 | public var ObjectiveThreshold threshold | 115 | public var ObjectiveThreshold threshold |
113 | public var boolean findExtremum | 116 | public var boolean findExtremum |
117 | public var CostObjectiveHint hint | ||
114 | } | 118 | } |
115 | 119 | ||
116 | class CostObjectiveElementConfiguration { | 120 | class CostObjectiveElementConfiguration { |
117 | public var String patternQualifiedName | 121 | public var String patternQualifiedName |
118 | public var int weight | 122 | public var int weight |
119 | } | 123 | } |
124 | |||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java index a2de1abc..4b7cead1 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java | |||
@@ -28,8 +28,6 @@ import org.eclipse.viatra.dse.objectives.Fitness; | |||
28 | import org.eclipse.viatra.dse.objectives.ObjectiveComparatorHelper; | 28 | import org.eclipse.viatra.dse.objectives.ObjectiveComparatorHelper; |
29 | import org.eclipse.viatra.dse.solutionstore.ISolutionFoundHandler; | 29 | import org.eclipse.viatra.dse.solutionstore.ISolutionFoundHandler; |
30 | import org.eclipse.viatra.dse.solutionstore.SolutionStore; | 30 | import org.eclipse.viatra.dse.solutionstore.SolutionStore; |
31 | import org.eclipse.viatra.query.runtime.api.IPatternMatch; | ||
32 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher; | ||
33 | 31 | ||
34 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel; | 32 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel; |
35 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner; | 33 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner; |
@@ -37,12 +35,11 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem; | |||
37 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.InconsistencyResult; | 35 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.InconsistencyResult; |
38 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult; | 36 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult; |
39 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult; | 37 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult; |
40 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod; | ||
41 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.PartialInterpretation2Logic; | 38 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.PartialInterpretation2Logic; |
42 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation; | 39 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation; |
43 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.statecoder.NeighbourhoodBasedPartialInterpretationStateCoder; | ||
44 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretationVisualisation; | 40 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretationVisualisation; |
45 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretationVisualiser; | 41 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretationVisualiser; |
42 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ModelGenerationMethod; | ||
46 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration; | 43 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration; |
47 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace; | 44 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace; |
48 | 45 | ||
@@ -301,13 +298,12 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { | |||
301 | return activationIds; | 298 | return activationIds; |
302 | } | 299 | } |
303 | 300 | ||
304 | private void checkForSolution(final Fitness fittness) { | 301 | private void checkForSolution(final Fitness fitness) { |
305 | solutionStore.newSolution(context); | 302 | solutionStore.newSolution(context); |
306 | } | 303 | } |
307 | 304 | ||
308 | public List<String> times = new LinkedList<String>(); | 305 | public List<String> times = new LinkedList<String>(); |
309 | private void saveTimes() { | 306 | private void saveTimes() { |
310 | long statecoderTime = ((NeighbourhoodBasedPartialInterpretationStateCoder<?, ?>)this.context.getStateCoder()).getStatecoderRuntime()/1000000; | ||
311 | long forwardTime = context.getDesignSpaceManager().getForwardTime()/1000000; | 307 | long forwardTime = context.getDesignSpaceManager().getForwardTime()/1000000; |
312 | long backtrackingTime = context.getDesignSpaceManager().getBacktrackingTime()/1000000; | 308 | long backtrackingTime = context.getDesignSpaceManager().getBacktrackingTime()/1000000; |
313 | long activationSelection = this.activationSelector.getRuntime()/1000000; | 309 | long activationSelection = this.activationSelector.getRuntime()/1000000; |
@@ -317,8 +313,7 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { | |||
317 | long numericalSolverSolving = this.numericSolver.getSolverSolvingProblem()/1000000; | 313 | long numericalSolverSolving = this.numericSolver.getSolverSolvingProblem()/1000000; |
318 | long numericalSolverInterpreting = this.numericSolver.getSolverSolution()/1000000; | 314 | long numericalSolverInterpreting = this.numericSolver.getSolverSolution()/1000000; |
319 | this.times.add( | 315 | this.times.add( |
320 | "(TransformationExecutionTime"+method.getStatistics().transformationExecutionTime/1000000+ | 316 | "(TransformationExecutionTime"+method.getStatistics().transformationExecutionTime/1000000+ |
321 | "|StateCoderTime:"+statecoderTime+ | ||
322 | "|ForwardTime:"+forwardTime+ | 317 | "|ForwardTime:"+forwardTime+ |
323 | "|Backtrackingtime:"+backtrackingTime+ | 318 | "|Backtrackingtime:"+backtrackingTime+ |
324 | "|GlobalConstraintEvaluationTime:"+(globalConstraintEvaluationTime/1000000)+ | 319 | "|GlobalConstraintEvaluationTime:"+(globalConstraintEvaluationTime/1000000)+ |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend index 066040a0..70e8e9c2 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend | |||
@@ -1,13 +1,13 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse | 1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse |
2 | 2 | ||
3 | import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericTranslator | 3 | import hu.bme.mit.inf.dslreasoner.viatra2logic.NumericTranslator |
4 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod | ||
5 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BooleanElement | 4 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.BooleanElement |
6 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement | 5 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement |
7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | 6 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation |
8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement | 7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement |
9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement | 8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement |
10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.StringElement | 9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.StringElement |
10 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ModelGenerationMethod | ||
11 | import java.math.BigDecimal | 11 | import java.math.BigDecimal |
12 | import java.util.HashMap | 12 | import java.util.HashMap |
13 | import java.util.LinkedHashMap | 13 | import java.util.LinkedHashMap |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/PartialModelAsLogicInterpretation.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/PartialModelAsLogicInterpretation.xtend index cfd11816..b48d0831 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/PartialModelAsLogicInterpretation.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/PartialModelAsLogicInterpretation.xtend | |||
@@ -22,12 +22,13 @@ import java.util.List | |||
22 | import java.util.Map | 22 | import java.util.Map |
23 | import java.util.TreeSet | 23 | import java.util.TreeSet |
24 | import org.eclipse.emf.ecore.EObject | 24 | import org.eclipse.emf.ecore.EObject |
25 | import org.eclipse.xtend.lib.annotations.Accessors | ||
25 | import org.eclipse.xtext.xbase.lib.Functions.Function1 | 26 | import org.eclipse.xtext.xbase.lib.Functions.Function1 |
26 | 27 | ||
27 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | 28 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* |
28 | 29 | ||
29 | class PartialModelAsLogicInterpretation implements LogicModelInterpretation{ | 30 | class PartialModelAsLogicInterpretation implements LogicModelInterpretation{ |
30 | val PartialInterpretation partialInterpretation | 31 | @Accessors val PartialInterpretation partialInterpretation |
31 | val Map<EObject, EObject> trace; | 32 | val Map<EObject, EObject> trace; |
32 | val Map<TypeDeclaration,PartialComplexTypeInterpretation> type2Interpretation | 33 | val Map<TypeDeclaration,PartialComplexTypeInterpretation> type2Interpretation |
33 | val Map<RelationDeclaration,PartialRelationInterpretation> relation2Interpretation | 34 | val Map<RelationDeclaration,PartialRelationInterpretation> relation2Interpretation |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionCopier.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionCopier.xtend index 38c8f5a1..33b69436 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionCopier.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/SolutionCopier.xtend | |||
@@ -26,16 +26,12 @@ class CopiedSolution { | |||
26 | * using the supplied {@link NumericSolver}. | 26 | * using the supplied {@link NumericSolver}. |
27 | */ | 27 | */ |
28 | class SolutionCopier { | 28 | class SolutionCopier { |
29 | val NumericSolver numericSolver | ||
30 | val copiedSolutions = new LinkedHashMap<Object, CopiedSolution> | 29 | val copiedSolutions = new LinkedHashMap<Object, CopiedSolution> |
31 | 30 | ||
31 | @Accessors NumericSolver numericSolver | ||
32 | long startTime = System.nanoTime | 32 | long startTime = System.nanoTime |
33 | @Accessors(PUBLIC_GETTER) long totalCopierRuntime = 0 | 33 | @Accessors(PUBLIC_GETTER) long totalCopierRuntime = 0 |
34 | 34 | ||
35 | new(NumericSolver numericSolver) { | ||
36 | this.numericSolver = numericSolver | ||
37 | } | ||
38 | |||
39 | def void copySolution(ThreadContext context, Object solutionId) { | 35 | def void copySolution(ThreadContext context, Object solutionId) { |
40 | val existingCopy = copiedSolutions.get(solutionId) | 36 | val existingCopy = copiedSolutions.get(solutionId) |
41 | if (existingCopy === null) { | 37 | if (existingCopy === null) { |
@@ -47,7 +43,7 @@ class SolutionCopier { | |||
47 | totalCopierRuntime += System.nanoTime - copyStart | 43 | totalCopierRuntime += System.nanoTime - copyStart |
48 | val copierRuntime = System.nanoTime - startTime | 44 | val copierRuntime = System.nanoTime - startTime |
49 | val copiedSolution = new CopiedSolution(copiedPartialInterpretation, copier, copierRuntime) | 45 | val copiedSolution = new CopiedSolution(copiedPartialInterpretation, copier, copierRuntime) |
50 | numericSolver.fillSolutionCopy(copiedSolution.trace) | 46 | numericSolver?.fillSolutionCopy(copiedSolution.trace) |
51 | copiedSolutions.put(solutionId, copiedSolution) | 47 | copiedSolutions.put(solutionId, copiedSolution) |
52 | } else { | 48 | } else { |
53 | existingCopy.current = true | 49 | existingCopy.current = true |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ViatraReasonerSolutionSaver.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ViatraReasonerSolutionSaver.xtend index c0b5008c..e00f76ff 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ViatraReasonerSolutionSaver.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ViatraReasonerSolutionSaver.xtend | |||
@@ -1,5 +1,9 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse | 1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse |
2 | 2 | ||
3 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Bounds | ||
4 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.DirectionalThresholdObjective | ||
5 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.IObjectiveBoundsProvider | ||
6 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveThreshold | ||
3 | import java.util.HashMap | 7 | import java.util.HashMap |
4 | import java.util.Map | 8 | import java.util.Map |
5 | import org.eclipse.viatra.dse.api.DSEException | 9 | import org.eclipse.viatra.dse.api.DSEException |
@@ -18,24 +22,32 @@ import org.eclipse.xtend.lib.annotations.Accessors | |||
18 | * Will also automatically fill any missing numerical values in the saved solutions | 22 | * Will also automatically fill any missing numerical values in the saved solutions |
19 | * using the supplied {@link NumericSolver}. | 23 | * using the supplied {@link NumericSolver}. |
20 | */ | 24 | */ |
21 | class ViatraReasonerSolutionSaver implements ISolutionSaver { | 25 | class ViatraReasonerSolutionSaver implements ISolutionSaver, IObjectiveBoundsProvider { |
26 | static val TOLERANCE = 1e-10 | ||
27 | |||
22 | @Accessors val SolutionCopier solutionCopier | 28 | @Accessors val SolutionCopier solutionCopier |
23 | val NumericSolver numericSolver | ||
24 | @Accessors val DiversityChecker diversityChecker | 29 | @Accessors val DiversityChecker diversityChecker |
30 | val IObjective[][] leveledExtremalObjectives | ||
25 | val boolean hasExtremalObjectives | 31 | val boolean hasExtremalObjectives |
26 | val int numberOfRequiredSolutions | 32 | val int numberOfRequiredSolutions |
27 | val ObjectiveComparatorHelper comparatorHelper | 33 | val ObjectiveComparatorHelper comparatorHelper |
28 | val Map<SolutionTrajectory, Fitness> trajectories = new HashMap | 34 | val Map<SolutionTrajectory, Fitness> trajectories = new HashMap |
29 | 35 | ||
30 | @Accessors(PUBLIC_SETTER) var Map<Object, Solution> solutionsCollection | 36 | @Accessors var NumericSolver numericSolver |
37 | @Accessors var Map<Object, Solution> solutionsCollection | ||
31 | 38 | ||
32 | new(IObjective[][] leveledExtremalObjectives, int numberOfRequiredSolutions, DiversityChecker diversityChecker, NumericSolver numericSolver) { | 39 | new(IObjective[][] leveledExtremalObjectives, int numberOfRequiredSolutions, DiversityChecker diversityChecker) { |
33 | this.diversityChecker = diversityChecker | 40 | this.diversityChecker = diversityChecker |
34 | comparatorHelper = new ObjectiveComparatorHelper(leveledExtremalObjectives) | 41 | comparatorHelper = new ObjectiveComparatorHelper(leveledExtremalObjectives) |
42 | this.leveledExtremalObjectives = leveledExtremalObjectives | ||
35 | hasExtremalObjectives = leveledExtremalObjectives.exists[!empty] | 43 | hasExtremalObjectives = leveledExtremalObjectives.exists[!empty] |
36 | this.numberOfRequiredSolutions = numberOfRequiredSolutions | 44 | this.numberOfRequiredSolutions = numberOfRequiredSolutions |
37 | this.solutionCopier = new SolutionCopier(numericSolver) | 45 | this.solutionCopier = new SolutionCopier |
46 | } | ||
47 | |||
48 | def setNumericSolver(NumericSolver numericSolver) { | ||
38 | this.numericSolver = numericSolver | 49 | this.numericSolver = numericSolver |
50 | solutionCopier.numericSolver = numericSolver | ||
39 | } | 51 | } |
40 | 52 | ||
41 | override saveSolution(ThreadContext context, Object id, SolutionTrajectory solutionTrajectory) { | 53 | override saveSolution(ThreadContext context, Object id, SolutionTrajectory solutionTrajectory) { |
@@ -51,6 +63,7 @@ class ViatraReasonerSolutionSaver implements ISolutionSaver { | |||
51 | if (!shouldSaveSolution(fitness, context)) { | 63 | if (!shouldSaveSolution(fitness, context)) { |
52 | return false | 64 | return false |
53 | } | 65 | } |
66 | println("Found: " + fitness) | ||
54 | val dominatedTrajectories = newArrayList | 67 | val dominatedTrajectories = newArrayList |
55 | for (entry : trajectories.entrySet) { | 68 | for (entry : trajectories.entrySet) { |
56 | val isLastFitnessBetter = comparatorHelper.compare(fitness, entry.value) | 69 | val isLastFitnessBetter = comparatorHelper.compare(fitness, entry.value) |
@@ -99,7 +112,7 @@ class ViatraReasonerSolutionSaver implements ISolutionSaver { | |||
99 | } | 112 | } |
100 | 113 | ||
101 | private def shouldSaveSolution(Fitness fitness, ThreadContext context) { | 114 | private def shouldSaveSolution(Fitness fitness, ThreadContext context) { |
102 | return fitness.satisifiesHardObjectives && numericSolver.currentSatisfiable | 115 | fitness.satisifiesHardObjectives && (numericSolver === null || numericSolver.currentSatisfiable) |
103 | } | 116 | } |
104 | 117 | ||
105 | private def basicSaveSolution(ThreadContext context, Object id, SolutionTrajectory solutionTrajectory, | 118 | private def basicSaveSolution(ThreadContext context, Object id, SolutionTrajectory solutionTrajectory, |
@@ -145,8 +158,93 @@ class ViatraReasonerSolutionSaver implements ISolutionSaver { | |||
145 | } | 158 | } |
146 | solutionsCollection.size < numberOfRequiredSolutions | 159 | solutionsCollection.size < numberOfRequiredSolutions |
147 | } | 160 | } |
148 | 161 | ||
149 | def getTotalCopierRuntime() { | 162 | def getTotalCopierRuntime() { |
150 | solutionCopier.totalCopierRuntime | 163 | solutionCopier.totalCopierRuntime |
151 | } | 164 | } |
165 | |||
166 | override computeRequiredBounds(IObjective objective, Bounds bounds) { | ||
167 | if (!hasExtremalObjectives) { | ||
168 | return | ||
169 | } | ||
170 | if (objective instanceof DirectionalThresholdObjective) { | ||
171 | switch (threshold : objective.threshold) { | ||
172 | case ObjectiveThreshold.NO_THRESHOLD: { | ||
173 | // No threshold to set. | ||
174 | } | ||
175 | ObjectiveThreshold.Exclusive: { | ||
176 | switch (kind : objective.kind) { | ||
177 | case HIGHER_IS_BETTER: | ||
178 | bounds.tightenLowerBound(Math.floor(threshold.threshold + 1) as int) | ||
179 | case LOWER_IS_BETTER: | ||
180 | bounds.tightenUpperBound(Math.ceil(threshold.threshold - 1) as int) | ||
181 | default: | ||
182 | throw new IllegalArgumentException("Unknown objective kind" + kind) | ||
183 | } | ||
184 | if (threshold.clampToThreshold) { | ||
185 | return | ||
186 | } | ||
187 | } | ||
188 | ObjectiveThreshold.Inclusive: { | ||
189 | switch (kind : objective.kind) { | ||
190 | case HIGHER_IS_BETTER: | ||
191 | bounds.tightenLowerBound(Math.ceil(threshold.threshold) as int) | ||
192 | case LOWER_IS_BETTER: | ||
193 | bounds.tightenUpperBound(Math.floor(threshold.threshold) as int) | ||
194 | default: | ||
195 | throw new IllegalArgumentException("Unknown objective kind" + kind) | ||
196 | } | ||
197 | if (threshold.clampToThreshold) { | ||
198 | return | ||
199 | } | ||
200 | } | ||
201 | default: | ||
202 | throw new IllegalArgumentException("Unknown threshold: " + threshold) | ||
203 | } | ||
204 | for (level : leveledExtremalObjectives) { | ||
205 | switch (level.size) { | ||
206 | case 0: { | ||
207 | // Nothing to do, wait for the next level. | ||
208 | } | ||
209 | case 1: { | ||
210 | val primaryObjective = level.get(0) | ||
211 | if (primaryObjective != objective) { | ||
212 | // There are no worst-case bounds for secondary objectives. | ||
213 | return | ||
214 | } | ||
215 | } | ||
216 | default: | ||
217 | // There are no worst-case bounds for Pareto front calculation. | ||
218 | return | ||
219 | } | ||
220 | } | ||
221 | val fitnessIterator = trajectories.values.iterator | ||
222 | if (!fitnessIterator.hasNext) { | ||
223 | return | ||
224 | } | ||
225 | val fitness = fitnessIterator.next.get(objective.name) | ||
226 | while (fitnessIterator.hasNext) { | ||
227 | val otherFitness = fitnessIterator.next.get(objective.name) | ||
228 | if (Math.abs(fitness - otherFitness) > TOLERANCE) { | ||
229 | throw new IllegalStateException("Inconsistent fitness: " + objective.name) | ||
230 | } | ||
231 | } | ||
232 | switch (kind : objective.kind) { | ||
233 | case HIGHER_IS_BETTER: | ||
234 | if (needsMoreSolutionsWithSameFitness) { | ||
235 | bounds.tightenLowerBound(Math.floor(fitness) as int) | ||
236 | } else { | ||
237 | bounds.tightenLowerBound(Math.floor(fitness + 1) as int) | ||
238 | } | ||
239 | case LOWER_IS_BETTER: | ||
240 | if (needsMoreSolutionsWithSameFitness) { | ||
241 | bounds.tightenUpperBound(Math.ceil(fitness) as int) | ||
242 | } else { | ||
243 | bounds.tightenUpperBound(Math.ceil(fitness - 1) as int) | ||
244 | } | ||
245 | default: | ||
246 | throw new IllegalArgumentException("Unknown objective kind" + kind) | ||
247 | } | ||
248 | } | ||
249 | } | ||
152 | } | 250 | } |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/CostElementMatchers.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/CostElementMatchers.xtend new file mode 100644 index 00000000..885b14e8 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/CostElementMatchers.xtend | |||
@@ -0,0 +1,137 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization | ||
2 | |||
3 | import com.google.common.collect.ImmutableList | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage | ||
5 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialinterpretationPackage | ||
6 | import java.util.List | ||
7 | import org.eclipse.emf.ecore.EObject | ||
8 | import org.eclipse.viatra.query.runtime.api.IPatternMatch | ||
9 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher | ||
10 | import org.eclipse.xtend.lib.annotations.Data | ||
11 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | ||
12 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | ||
13 | |||
14 | @FunctionalInterface | ||
15 | interface ParameterScopeBound { | ||
16 | def double getUpperBound() | ||
17 | } | ||
18 | |||
19 | @Data | ||
20 | class CostElementMatch { | ||
21 | val IPatternMatch match | ||
22 | val boolean must | ||
23 | |||
24 | def isMulti() { | ||
25 | CostElementMatchers.isMultiMatch(match) | ||
26 | } | ||
27 | } | ||
28 | |||
29 | @Data | ||
30 | class CostElementMatchers { | ||
31 | val ViatraQueryMatcher<? extends IPatternMatch> currentMatcher | ||
32 | val ViatraQueryMatcher<? extends IPatternMatch> mayMatcher | ||
33 | val ViatraQueryMatcher<? extends IPatternMatch> mustMatcher | ||
34 | val List<ParameterScopeBound> parameterScopeBounds | ||
35 | val int weight | ||
36 | |||
37 | def getCurrentNumberOfMatches() { | ||
38 | currentMatcher.countMatches | ||
39 | } | ||
40 | |||
41 | def getMinimumNumberOfMatches() { | ||
42 | mustMatcher.countMatches | ||
43 | } | ||
44 | |||
45 | def getMaximumNumberOfMatches() { | ||
46 | var double sum = 0 | ||
47 | val iterator = mayMatcher.streamAllMatches.iterator | ||
48 | while (iterator.hasNext) { | ||
49 | val match = iterator.next | ||
50 | var double product = 1 | ||
51 | val numberOfParameters = parameterScopeBounds.size | ||
52 | for (var int i = 0; i < numberOfParameters; i++) { | ||
53 | if (isMulti(match.get(i + 2))) { | ||
54 | val scopeBound = parameterScopeBounds.get(i) | ||
55 | product *= scopeBound.upperBound | ||
56 | } | ||
57 | |||
58 | } | ||
59 | sum += product | ||
60 | } | ||
61 | sum | ||
62 | } | ||
63 | |||
64 | def getMatches() { | ||
65 | ImmutableList.copyOf(mayMatcher.streamAllMatches.iterator.map [ match | | ||
66 | new CostElementMatch(match, mustMatcher.isMatch(match)) | ||
67 | ]) | ||
68 | } | ||
69 | |||
70 | def projectMayMatch(IPatternMatch match, int... indices) { | ||
71 | mayMatcher.projectMatch(match, indices) | ||
72 | } | ||
73 | |||
74 | private static def <T extends IPatternMatch> projectMatch(ViatraQueryMatcher<T> matcher, IPatternMatch match, int... indices) { | ||
75 | checkMatch(match) | ||
76 | val n = matcher.specification.parameters.length - 2 | ||
77 | if (indices.length != n) { | ||
78 | throw new IllegalArgumentException("Invalid number of projection indices") | ||
79 | } | ||
80 | val newMatch = matcher.newEmptyMatch | ||
81 | newMatch.set(0, match.get(0)) | ||
82 | newMatch.set(1, match.get(1)) | ||
83 | for (var int i = 0; i < n; i++) { | ||
84 | newMatch.set(i + 2, match.get(indices.get(i))) | ||
85 | } | ||
86 | if (!matcher.hasMatch(newMatch)) { | ||
87 | throw new IllegalArgumentException("Projected match does not exist") | ||
88 | } | ||
89 | return newMatch | ||
90 | } | ||
91 | |||
92 | private static def <T extends IPatternMatch> isMatch(ViatraQueryMatcher<T> matcher, IPatternMatch match) { | ||
93 | val n = matcher.specification.parameters.length | ||
94 | if (n != match.specification.parameters.length) { | ||
95 | throw new IllegalArgumentException("Invalid number of match arguments") | ||
96 | } | ||
97 | val newMatch = matcher.newEmptyMatch | ||
98 | for (var int i = 0; i < n; i++) { | ||
99 | newMatch.set(i, match.get(i)) | ||
100 | } | ||
101 | return matcher.hasMatch(newMatch) | ||
102 | } | ||
103 | |||
104 | static def isMulti(Object o) { | ||
105 | if (o instanceof EObject) { | ||
106 | switch (feature : o.eContainmentFeature) { | ||
107 | case LogicproblemPackage.eINSTANCE.logicProblem_Elements, | ||
108 | case PartialinterpretationPackage.eINSTANCE.partialInterpretation_NewElements: | ||
109 | false | ||
110 | case PartialinterpretationPackage.eINSTANCE.partialInterpretation_OpenWorldElements: | ||
111 | true | ||
112 | default: | ||
113 | throw new IllegalStateException("Unknown containment feature for element: " + feature) | ||
114 | } | ||
115 | } else { | ||
116 | false | ||
117 | } | ||
118 | } | ||
119 | |||
120 | static def isMultiMatch(IPatternMatch match) { | ||
121 | checkMatch(match) | ||
122 | val n = match.specification.parameters.length | ||
123 | for (var int i = 2; i < n; i++) { | ||
124 | if (isMulti(match.get(i))) { | ||
125 | return true | ||
126 | } | ||
127 | } | ||
128 | false | ||
129 | } | ||
130 | |||
131 | private static def checkMatch(IPatternMatch match) { | ||
132 | val n = match.specification.parameters.length | ||
133 | if (n < 2 || !(match.get(0) instanceof LogicProblem) || !(match.get(1) instanceof PartialInterpretation)) { | ||
134 | throw new IllegalArgumentException("Match is not from the partial interpretation") | ||
135 | } | ||
136 | } | ||
137 | } | ||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/CostObjectiveHint.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/CostObjectiveHint.xtend new file mode 100644 index 00000000..2434073d --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/CostObjectiveHint.xtend | |||
@@ -0,0 +1,68 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.BoundSaturationListener | ||
4 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ExtendedLinearExpressionBuilder | ||
5 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearTypeConstraintHint | ||
6 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearTypeExpressionBuilderFactory | ||
7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronExtensionOperator | ||
8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.PatternGenerator | ||
9 | import java.util.Map | ||
10 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery | ||
11 | import org.eclipse.xtend.lib.annotations.Accessors | ||
12 | |||
13 | abstract class CostObjectiveHint implements LinearTypeConstraintHint, BoundSaturationListener { | ||
14 | @Accessors ThreeValuedCostObjective objective | ||
15 | @Accessors IObjectiveBoundsProvider boundsProvider | ||
16 | |||
17 | Integer bestUpper = null | ||
18 | |||
19 | override getAdditionalPatterns(PatternGenerator patternGenerator, Map<String, PQuery> fqnToPQuery) { | ||
20 | '''''' | ||
21 | } | ||
22 | |||
23 | override createConstraintUpdater(LinearTypeExpressionBuilderFactory builderFactory) { | ||
24 | null | ||
25 | } | ||
26 | |||
27 | def isExact() { | ||
28 | false | ||
29 | } | ||
30 | |||
31 | def PolyhedronExtensionOperator createPolyhedronExtensionOperator( | ||
32 | Map<String, CostElementMatchers> costElementMatchers) { | ||
33 | null | ||
34 | } | ||
35 | |||
36 | def setObjective(ThreeValuedCostObjective objective) { | ||
37 | if (this.objective !== null) { | ||
38 | throw new IllegalStateException("Objective was already set") | ||
39 | } | ||
40 | this.objective = objective | ||
41 | } | ||
42 | |||
43 | def setBoundsProvider(IObjectiveBoundsProvider boundsProvider) { | ||
44 | if (this.boundsProvider !== null) { | ||
45 | throw new IllegalStateException("Objective bounds provider was already set") | ||
46 | } | ||
47 | this.boundsProvider = boundsProvider | ||
48 | } | ||
49 | |||
50 | protected def buildWithBounds(ExtendedLinearExpressionBuilder builder) { | ||
51 | val bounds = builder.build(this) | ||
52 | if (objective !== null && boundsProvider !== null) { | ||
53 | boundsProvider.computeRequiredBounds(objective, bounds) | ||
54 | } | ||
55 | if (exact && bestUpper !== null) { | ||
56 | bounds.tightenLowerBound(bestUpper) | ||
57 | } | ||
58 | bounds | ||
59 | } | ||
60 | |||
61 | override boundsSaturated(Integer lower, Integer upper) { | ||
62 | if (upper !== null && (bestUpper === null || bestUpper < upper)) { | ||
63 | bestUpper = upper | ||
64 | } | ||
65 | objective?.boundsSaturated(lower, upper) | ||
66 | } | ||
67 | |||
68 | } | ||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/IObjectiveBoundsProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/IObjectiveBoundsProvider.xtend new file mode 100644 index 00000000..3c4d36a5 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/IObjectiveBoundsProvider.xtend | |||
@@ -0,0 +1,8 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Bounds | ||
4 | import org.eclipse.viatra.dse.objectives.IObjective | ||
5 | |||
6 | interface IObjectiveBoundsProvider { | ||
7 | def void computeRequiredBounds(IObjective objective, Bounds bounds) | ||
8 | } | ||
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/ThreeValuedCostObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/ThreeValuedCostObjective.xtend index 0a6fd55b..9b1a7e9f 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/ThreeValuedCostObjective.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/ThreeValuedCostObjective.xtend | |||
@@ -1,85 +1,80 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization | 1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization |
2 | 2 | ||
3 | import com.google.common.collect.ImmutableList | 3 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.BoundSaturationListener |
4 | import java.util.Collection | 4 | import java.util.Map |
5 | import org.eclipse.viatra.dse.base.ThreadContext | 5 | import org.eclipse.viatra.dse.base.ThreadContext |
6 | import org.eclipse.viatra.query.runtime.api.IPatternMatch | 6 | import org.eclipse.xtend.lib.annotations.Accessors |
7 | import org.eclipse.viatra.query.runtime.api.IQuerySpecification | ||
8 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher | ||
9 | import org.eclipse.xtend.lib.annotations.Data | ||
10 | 7 | ||
11 | @Data | 8 | class ThreeValuedCostObjective extends AbstractThreeValuedObjective implements BoundSaturationListener { |
12 | class ThreeValuedCostElement { | 9 | @Accessors val Map<String, CostElementMatchers> matchers |
13 | val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> currentMatchQuery | 10 | double lowerBoundHint = Double.NEGATIVE_INFINITY |
14 | val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> mayMatchQuery | 11 | double upperBoundHint = Double.POSITIVE_INFINITY |
15 | val IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> mustMatchQuery | ||
16 | val int weight | ||
17 | } | ||
18 | |||
19 | class ThreeValuedCostObjective extends AbstractThreeValuedObjective { | ||
20 | val Collection<ThreeValuedCostElement> costElements | ||
21 | Collection<CostElementMatchers> matchers | ||
22 | 12 | ||
23 | new(String name, Collection<ThreeValuedCostElement> costElements, ObjectiveKind kind, ObjectiveThreshold threshold, | 13 | new(String name, Map<String, CostElementMatchers> matchers, ObjectiveKind kind, ObjectiveThreshold threshold, |
24 | int level) { | 14 | int level) { |
25 | super(name, kind, threshold, level) | 15 | super(name, kind, threshold, level) |
26 | this.costElements = costElements | 16 | this.matchers = matchers |
27 | } | 17 | } |
28 | 18 | ||
29 | override createNew() { | 19 | override createNew() { |
30 | new ThreeValuedCostObjective(name, costElements, kind, threshold, level) | 20 | // new ThreeValuedCostObjective(name, matchers, kind, threshold, level) |
21 | throw new UnsupportedOperationException("ThreeValuedCostObjective can only be used from a single thread") | ||
31 | } | 22 | } |
32 | 23 | ||
33 | override init(ThreadContext context) { | 24 | override init(ThreadContext context) { |
34 | val queryEngine = context.queryEngine | ||
35 | matchers = ImmutableList.copyOf(costElements.map [ element | | ||
36 | new CostElementMatchers( | ||
37 | queryEngine.getMatcher(element.currentMatchQuery), | ||
38 | queryEngine.getMatcher(element.mayMatchQuery), | ||
39 | queryEngine.getMatcher(element.mustMatchQuery), | ||
40 | element.weight | ||
41 | ) | ||
42 | ]) | ||
43 | } | 25 | } |
44 | 26 | ||
45 | override getRawFitness(ThreadContext context) { | 27 | override getRawFitness(ThreadContext context) { |
46 | var int cost = 0 | 28 | var double cost = 0 |
47 | for (matcher : matchers) { | 29 | for (matcher : matchers.values) { |
48 | cost += matcher.weight * matcher.currentMatcher.countMatches | 30 | cost += matcher.weight * matcher.currentNumberOfMatches |
49 | } | 31 | } |
50 | cost as double | 32 | cost |
51 | } | 33 | } |
52 | 34 | ||
53 | override getLowestPossibleFitness(ThreadContext threadContext) { | 35 | override getLowestPossibleFitness(ThreadContext threadContext) { |
54 | var int cost = 0 | 36 | var double cost = 0 |
55 | for (matcher : matchers) { | 37 | for (matcher : matchers.values) { |
56 | if (matcher.weight >= 0) { | 38 | if (matcher.weight >= 0) { |
57 | cost += matcher.weight * matcher.mustMatcher.countMatches | 39 | cost += matcher.weight * matcher.minimumNumberOfMatches |
58 | } else if (matcher.mayMatcher.countMatches > 0) { | 40 | } else { |
59 | // TODO Count may matches. | 41 | cost += matcher.weight * matcher.maximumNumberOfMatches |
60 | return Double.NEGATIVE_INFINITY | ||
61 | } | 42 | } |
62 | } | 43 | } |
63 | cost as double | 44 | val boundWithHint = Math.max(lowerBoundHint, cost) |
45 | if (boundWithHint > upperBoundHint) { | ||
46 | throw new IllegalStateException("Inconsistent cost bounds") | ||
47 | } | ||
48 | boundWithHint | ||
64 | } | 49 | } |
65 | 50 | ||
66 | override getHighestPossibleFitness(ThreadContext threadContext) { | 51 | override getHighestPossibleFitness(ThreadContext threadContext) { |
67 | var int cost = 0 | 52 | var double cost = 0 |
68 | for (matcher : matchers) { | 53 | for (matcher : matchers.values) { |
69 | if (matcher.weight <= 0) { | 54 | if (matcher.weight <= 0) { |
70 | cost += matcher.weight * matcher.mustMatcher.countMatches | 55 | cost += matcher.weight * matcher.minimumNumberOfMatches |
71 | } else if (matcher.mayMatcher.countMatches > 0) { | 56 | } else { |
72 | return Double.POSITIVE_INFINITY | 57 | cost += matcher.weight * matcher.maximumNumberOfMatches |
73 | } | 58 | } |
74 | } | 59 | } |
75 | cost as double | 60 | val boundWithHint = Math.min(upperBoundHint, cost) |
61 | if (boundWithHint < lowerBoundHint) { | ||
62 | throw new IllegalStateException("Inconsistent cost bounds") | ||
63 | } | ||
64 | boundWithHint | ||
76 | } | 65 | } |
77 | 66 | ||
78 | @Data | 67 | override boundsSaturated(Integer lower, Integer upper) { |
79 | private static class CostElementMatchers { | 68 | lowerBoundHint = if (lower === null) { |
80 | val ViatraQueryMatcher<? extends IPatternMatch> currentMatcher | 69 | Double.NEGATIVE_INFINITY |
81 | val ViatraQueryMatcher<? extends IPatternMatch> mayMatcher | 70 | } else { |
82 | val ViatraQueryMatcher<? extends IPatternMatch> mustMatcher | 71 | lower |
83 | val int weight | 72 | } |
73 | upperBoundHint = if (upper === null) { | ||
74 | Double.POSITIVE_INFINITY | ||
75 | } else { | ||
76 | upper | ||
77 | } | ||
78 | println('''Bounds saturated: «lower»..«upper»''') | ||
84 | } | 79 | } |
85 | } | 80 | } |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/ThreeValuedCostObjectiveProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/ThreeValuedCostObjectiveProvider.xtend new file mode 100644 index 00000000..c2750acd --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/ThreeValuedCostObjectiveProvider.xtend | |||
@@ -0,0 +1,205 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization | ||
2 | |||
3 | import com.google.common.collect.ImmutableList | ||
4 | import com.google.common.collect.ImmutableMap | ||
5 | import com.google.common.collect.Lists | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference | ||
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntTypeReference | ||
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference | ||
10 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation | ||
11 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.StringTypeReference | ||
12 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration | ||
13 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference | ||
14 | import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransfomedViatraQuery | ||
15 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedronExtensionOperator | ||
16 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.ModalPatternQueries | ||
17 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialBooleanInterpretation | ||
18 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialComplexTypeInterpretation | ||
19 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialIntegerInterpretation | ||
20 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | ||
21 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialRealInterpretation | ||
22 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialStringInterpretation | ||
23 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.Scope | ||
24 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.CostObjectiveConfiguration | ||
25 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.CostObjectiveElementConfiguration | ||
26 | import java.util.Collection | ||
27 | import java.util.Map | ||
28 | import org.eclipse.viatra.dse.objectives.IObjective | ||
29 | import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine | ||
30 | import org.eclipse.xtend.lib.annotations.Data | ||
31 | |||
32 | @Data | ||
33 | class ThreeValuedCostObjectiveProviderResult { | ||
34 | val Collection<IObjective> objectives | ||
35 | val Collection<CostObjectiveHint> hints | ||
36 | val Collection<PolyhedronExtensionOperator> extensionOperators | ||
37 | val IObjective[][] leveledExtremalObjectives | ||
38 | val boolean optimizationProblem | ||
39 | } | ||
40 | |||
41 | class ThreeValuedCostObjectiveProvider { | ||
42 | static val COST_OBJECTIVE_LEVEL = 3 | ||
43 | |||
44 | val ViatraQueryEngine queryEngine | ||
45 | val Map<String, ModalPatternQueries> modalRelationQueries | ||
46 | val Map<String, Relation> qualifiedNameToRelationMap | ||
47 | val ParameterScopeBound defaultBounds | ||
48 | val ParameterScopeBound booleanBounds | ||
49 | val ParameterScopeBound integerBounds | ||
50 | val ParameterScopeBound realBounds | ||
51 | val ParameterScopeBound stringBounds | ||
52 | val Map<TypeDeclaration, ParameterScopeBound> typeDeclarationToBoundsMap | ||
53 | |||
54 | new(ViatraQueryEngine queryEngine, PartialInterpretation interpretation, | ||
55 | Map<String, ModalPatternQueries> modalRelationQueries) { | ||
56 | this.queryEngine = queryEngine | ||
57 | this.modalRelationQueries = modalRelationQueries | ||
58 | qualifiedNameToRelationMap = ImmutableMap.copyOf( | ||
59 | interpretation.problem.annotations.filter(TransfomedViatraQuery). | ||
60 | toMap([patternFullyQualifiedName], [target])) | ||
61 | defaultBounds = new PartialInterpretationBasedParameterScopeBound(interpretation) | ||
62 | var ParameterScopeBound booleanBounds = null | ||
63 | var ParameterScopeBound integerBounds = null | ||
64 | var ParameterScopeBound realBounds = null | ||
65 | var ParameterScopeBound stringBounds = null | ||
66 | val typeDeclarationToBoundsMapBuilder = ImmutableMap.builder | ||
67 | for (scope : interpretation.scopes) { | ||
68 | val bounds = new ScopeBasedParameterScopeBound(scope) | ||
69 | switch (typeInterpretation : scope.targetTypeInterpretation) { | ||
70 | PartialBooleanInterpretation: | ||
71 | if (booleanBounds === null) { | ||
72 | booleanBounds = bounds | ||
73 | } else { | ||
74 | throw new IllegalStateException("Duplicate partial boolean interpretation") | ||
75 | } | ||
76 | PartialIntegerInterpretation: | ||
77 | if (integerBounds === null) { | ||
78 | integerBounds = bounds | ||
79 | } else { | ||
80 | throw new IllegalStateException("Duplicate partial integer interpretation") | ||
81 | } | ||
82 | PartialRealInterpretation: | ||
83 | if (realBounds === null) { | ||
84 | realBounds = bounds | ||
85 | } else { | ||
86 | throw new IllegalStateException("Duplicate partial real interpretation") | ||
87 | } | ||
88 | PartialStringInterpretation: | ||
89 | if (stringBounds === null) { | ||
90 | stringBounds = bounds | ||
91 | } else { | ||
92 | throw new IllegalStateException("Duplicate partial string interpretation") | ||
93 | } | ||
94 | PartialComplexTypeInterpretation: | ||
95 | typeDeclarationToBoundsMapBuilder.put(typeInterpretation.interpretationOf, bounds) | ||
96 | } | ||
97 | } | ||
98 | this.booleanBounds = booleanBounds ?: defaultBounds | ||
99 | this.integerBounds = integerBounds ?: defaultBounds | ||
100 | this.realBounds = realBounds ?: defaultBounds | ||
101 | this.stringBounds = stringBounds ?: defaultBounds | ||
102 | typeDeclarationToBoundsMap = typeDeclarationToBoundsMapBuilder.build | ||
103 | } | ||
104 | |||
105 | def getCostObjectives(Collection<CostObjectiveConfiguration> costObjectives) { | ||
106 | val objectives = ImmutableList.<IObjective>builder | ||
107 | val hints = ImmutableList.<CostObjectiveHint>builder | ||
108 | val extensionOperators = ImmutableList.<PolyhedronExtensionOperator>builder | ||
109 | val extremalObjectives = Lists.newArrayListWithExpectedSize(costObjectives.size) | ||
110 | for (entry : costObjectives.indexed) { | ||
111 | val objectiveName = '''costObjective«entry.key»''' | ||
112 | val objectiveConfig = entry.value | ||
113 | val costObjective = transformCostObjective(objectiveConfig, objectiveName) | ||
114 | objectives.add(costObjective) | ||
115 | if (objectiveConfig.findExtremum) { | ||
116 | extremalObjectives += costObjective | ||
117 | } | ||
118 | val hint = objectiveConfig.hint | ||
119 | if (hint !== null) { | ||
120 | hints.add(hint) | ||
121 | hint.objective = costObjective | ||
122 | val extensionOperator = hint.createPolyhedronExtensionOperator(costObjective.matchers) | ||
123 | if (extensionOperator !== null) { | ||
124 | extensionOperators.add(extensionOperator) | ||
125 | } | ||
126 | } | ||
127 | } | ||
128 | new ThreeValuedCostObjectiveProviderResult( | ||
129 | objectives.build, | ||
130 | hints.build, | ||
131 | extensionOperators.build, | ||
132 | newArrayList(extremalObjectives), | ||
133 | !extremalObjectives.empty | ||
134 | ) | ||
135 | } | ||
136 | |||
137 | private def transformCostObjective(CostObjectiveConfiguration configuration, String name) { | ||
138 | val costElements = ImmutableMap.copyOf(configuration.elements.toMap([patternQualifiedName], [ | ||
139 | transformCostElement | ||
140 | ])) | ||
141 | new ThreeValuedCostObjective(name, costElements, configuration.kind, configuration.threshold, | ||
142 | COST_OBJECTIVE_LEVEL) | ||
143 | } | ||
144 | |||
145 | private def transformCostElement(CostObjectiveElementConfiguration elementConfig) { | ||
146 | val relationName = elementConfig.patternQualifiedName | ||
147 | val modalQueries = modalRelationQueries.get(relationName) | ||
148 | if (modalQueries === null) { | ||
149 | throw new IllegalArgumentException("Unknown relation queries: " + relationName) | ||
150 | } | ||
151 | val relation = qualifiedNameToRelationMap.get(relationName) | ||
152 | if (relation === null) { | ||
153 | throw new IllegalArgumentException("Unknown transformed relation: " + relationName) | ||
154 | } | ||
155 | val parameterBounds = ImmutableList.copyOf(relation.parameters.map[parameterBound]) | ||
156 | new CostElementMatchers( | ||
157 | queryEngine.getMatcher(modalQueries.currentQuery), | ||
158 | queryEngine.getMatcher(modalQueries.mayQuery), | ||
159 | queryEngine.getMatcher(modalQueries.mustQuery), | ||
160 | parameterBounds, | ||
161 | elementConfig.weight | ||
162 | ) | ||
163 | } | ||
164 | |||
165 | private def getParameterBound(TypeReference typeReference) { | ||
166 | switch (typeReference) { | ||
167 | BoolTypeReference: booleanBounds | ||
168 | IntTypeReference: integerBounds | ||
169 | RealTypeReference: realBounds | ||
170 | StringTypeReference: stringBounds | ||
171 | ComplexTypeReference: typeDeclarationToBoundsMap.getOrDefault(typeReference.referred, defaultBounds) | ||
172 | } | ||
173 | } | ||
174 | |||
175 | private static abstract class AbstractParameterScopeBound implements ParameterScopeBound { | ||
176 | override getUpperBound() { | ||
177 | val rawValue = rawUpperBound | ||
178 | if (rawValue < 0) { | ||
179 | Double.POSITIVE_INFINITY | ||
180 | } else { | ||
181 | rawValue | ||
182 | } | ||
183 | } | ||
184 | |||
185 | protected def int getRawUpperBound() | ||
186 | } | ||
187 | |||
188 | @Data | ||
189 | private static class ScopeBasedParameterScopeBound extends AbstractParameterScopeBound { | ||
190 | val Scope scope | ||
191 | |||
192 | override protected getRawUpperBound() { | ||
193 | scope.maxNewElements | ||
194 | } | ||
195 | } | ||
196 | |||
197 | @Data | ||
198 | private static class PartialInterpretationBasedParameterScopeBound extends AbstractParameterScopeBound { | ||
199 | val PartialInterpretation interpretation | ||
200 | |||
201 | override protected getRawUpperBound() { | ||
202 | interpretation.maxNewElements | ||
203 | } | ||
204 | } | ||
205 | } | ||