aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend
diff options
context:
space:
mode:
authorLibravatar Kristóf Marussy <marussy@mit.bme.hu>2020-11-02 02:02:40 +0100
committerLibravatar Kristóf Marussy <marussy@mit.bme.hu>2020-11-02 02:02:40 +0100
commitf06427cd7375551582461f91b3458339a8227f9b (patch)
tree97bc6ec85f4c384e5080a6611b492caf460b6ce9 /Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend
parentMust unit propagation (diff)
downloadVIATRA-Generator-f06427cd7375551582461f91b3458339a8227f9b.tar.gz
VIATRA-Generator-f06427cd7375551582461f91b3458339a8227f9b.tar.zst
VIATRA-Generator-f06427cd7375551582461f91b3458339a8227f9b.zip
Optimizing generator with linear objective functions
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend')
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend102
1 files changed, 40 insertions, 62 deletions
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 8e05665c..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 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner 1package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner
2 2
3import com.google.common.collect.ImmutableList
4import com.google.common.collect.Lists
5import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel 3import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel
6import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner 4import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner
7import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException 5import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException
@@ -11,7 +9,6 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
11import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage 9import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage
12import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory 10import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory
13import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult 11import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult
14import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethodProvider
15import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy 12import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy
16import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.PartialInterpretationInitialiser 13import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.PartialInterpretationInitialiser
17import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation 14import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
@@ -22,7 +19,6 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.sta
22import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.statecoder.PairwiseNeighbourhoodBasedStateCoderFactory 19import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.statecoder.PairwiseNeighbourhoodBasedStateCoderFactory
23import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.BasicScopeGlobalConstraint 20import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.BasicScopeGlobalConstraint
24import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.BestFirstStrategyForModelGeneration 21import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.BestFirstStrategyForModelGeneration
25import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.DiversityChecker
26import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.InconsistentScopeGlobalConstraint 22import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.InconsistentScopeGlobalConstraint
27import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.LoggerSolutionFoundHandler 23import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.LoggerSolutionFoundHandler
28import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ModelGenerationCompositeObjective 24import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ModelGenerationCompositeObjective
@@ -32,11 +28,8 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.PunishSizeObjective
32import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ScopeObjective 28import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ScopeObjective
33import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.SurelyViolatedObjectiveGlobalConstraint 29import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.SurelyViolatedObjectiveGlobalConstraint
34import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.UnfinishedMultiplicityObjective 30import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.UnfinishedMultiplicityObjective
35import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ViatraReasonerSolutionSaver
36import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.WF2ObjectiveConverter 31import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.WF2ObjectiveConverter
37import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveKind 32import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveKind
38import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ThreeValuedCostElement
39import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ThreeValuedCostObjective
40import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace 33import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace
41import java.util.List 34import java.util.List
42import java.util.Map 35import java.util.Map
@@ -86,13 +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.unitPropagationPatternGenerators,
95 viatraConfig.documentationLevel
96 ) 83 )
97 84
98 val compositeObjective = new ModelGenerationCompositeObjective( 85 val compositeObjective = new ModelGenerationCompositeObjective(
@@ -112,45 +99,21 @@ class ViatraReasoner extends LogicReasoner {
112 dse.addObjective(punishObjective) 99 dse.addObjective(punishObjective)
113 } 100 }
114 101
115 val extremalObjectives = Lists.newArrayListWithExpectedSize(viatraConfig.costObjectives.size) 102 for (costObjective : method.costObjectives) {
116 for (entry : viatraConfig.costObjectives.indexed) {
117 val objectiveName = '''costObjective«entry.key»'''
118 val objectiveConfig = entry.value
119 val elementsBuilder = ImmutableList.builder
120 for (elementConfig : objectiveConfig.elements) {
121 val relationName = elementConfig.patternQualifiedName
122 val modalQueries = method.modalRelationQueries.get(relationName)
123 if (modalQueries === null) {
124 throw new IllegalArgumentException("Unknown relation: " + relationName)
125 }
126 elementsBuilder.add(new ThreeValuedCostElement(
127 modalQueries.currentQuery,
128 modalQueries.mayQuery,
129 modalQueries.mustQuery,
130 elementConfig.weight
131 ))
132 }
133 val costElements = elementsBuilder.build
134 val costObjective = new ThreeValuedCostObjective(objectiveName, costElements, objectiveConfig.kind,
135 objectiveConfig.threshold, 3)
136 dse.addObjective(costObjective) 103 dse.addObjective(costObjective)
137 if (objectiveConfig.findExtremum) {
138 extremalObjectives += costObjective
139 }
140 } 104 }
141
142 val numberOfRequiredSolutions = configuration.solutionScope.numberOfRequiredSolutions 105 val numberOfRequiredSolutions = configuration.solutionScope.numberOfRequiredSolutions
143 val solutionStore = if (extremalObjectives.empty) { 106 val solutionStore = if (method.optimizationProblem) {
144 new SolutionStore(numberOfRequiredSolutions)
145 } else {
146 new SolutionStore() 107 new SolutionStore()
108 } else {
109 new SolutionStore(numberOfRequiredSolutions)
147 } 110 }
148 solutionStore.registerSolutionFoundHandler(new LoggerSolutionFoundHandler(viatraConfig)) 111 solutionStore.registerSolutionFoundHandler(new LoggerSolutionFoundHandler(viatraConfig))
149 val diversityChecker = DiversityChecker.of(viatraConfig.diversityRequirement)
150 val numericSolver = new NumericSolver(method, viatraConfig.runIntermediateNumericalConsistencyChecks, false) 112 val numericSolver = new NumericSolver(method, viatraConfig.runIntermediateNumericalConsistencyChecks, false)
151 val solutionSaver = new ViatraReasonerSolutionSaver(newArrayList(extremalObjectives), numberOfRequiredSolutions, 113 val solutionSaver = method.solutionSaver
152 diversityChecker, numericSolver) 114 solutionSaver.numericSolver = numericSolver
153 val solutionCopier = solutionSaver.solutionCopier 115 val solutionCopier = solutionSaver.solutionCopier
116 val diversityChecker = solutionSaver.diversityChecker
154 solutionStore.withSolutionSaver(solutionSaver) 117 solutionStore.withSolutionSaver(solutionSaver)
155 dse.solutionStore = solutionStore 118 dse.solutionStore = solutionStore
156 119
@@ -185,7 +148,8 @@ class ViatraReasoner extends LogicReasoner {
185 dse.addTransformationRule(rule) 148 dse.addTransformationRule(rule)
186 } 149 }
187 150
188 val strategy = new BestFirstStrategyForModelGeneration(workspace, viatraConfig, method, solutionSaver, numericSolver) 151 val strategy = new BestFirstStrategyForModelGeneration(workspace, viatraConfig, method, solutionSaver,
152 numericSolver)
189 viatraConfig.progressMonitor.workedForwardTransformation 153 viatraConfig.progressMonitor.workedForwardTransformation
190 val transformationFinished = System.nanoTime 154 val transformationFinished = System.nanoTime
191 val transformationTime = transformationFinished - transformationStartTime 155 val transformationTime = transformationFinished - transformationStartTime
@@ -211,14 +175,15 @@ class ViatraReasoner extends LogicReasoner {
211 it.value = (pair.value / 1000000) as int 175 it.value = (pair.value / 1000000) as int
212 ] 176 ]
213 } 177 }
214 for(x: 0..<strategy.times.size) { 178 for (x : 0 ..< strategy.times.size) {
215 it.entries += createStringStatisticEntry => [ 179 it.entries += createStringStatisticEntry => [
216 it.name = '''Solution«x+1»DetailedStatistics''' 180 it.name = '''Solution«x+1»DetailedStatistics'''
217 it.value = strategy.times.get(x) 181 it.value = strategy.times.get(x)
218 ] 182 ]
219 } 183 }
220 it.entries += createIntStatisticEntry => [ 184 it.entries += createIntStatisticEntry => [
221 it.name = "ExplorationInitializationTime" it.value = ((strategy.explorationStarted-transformationFinished)/1000000) as int 185 it.name = "ExplorationInitializationTime"
186 it.value = ((strategy.explorationStarted - transformationFinished) / 1000000) as int
222 ] 187 ]
223 it.entries += createIntStatisticEntry => [ 188 it.entries += createIntStatisticEntry => [
224 it.name = "TransformationExecutionTime" 189 it.name = "TransformationExecutionTime"
@@ -253,22 +218,28 @@ class ViatraReasoner extends LogicReasoner {
253 it.value = dse.numberOfStates as int 218 it.value = dse.numberOfStates as int
254 ] 219 ]
255 it.entries += createIntStatisticEntry => [ 220 it.entries += createIntStatisticEntry => [
256 it.name = "ForwardTime" it.value = (strategy.forwardTime/1000000) as int 221 it.name = "ForwardTime"
222 it.value = (strategy.forwardTime / 1000000) as int
257 ] 223 ]
258 it.entries += createIntStatisticEntry => [ 224 it.entries += createIntStatisticEntry => [
259 it.name = "BacktrackingTime" it.value = (strategy.backtrackingTime/1000000) as int 225 it.name = "BacktrackingTime"
226 it.value = (strategy.backtrackingTime / 1000000) as int
260 ] 227 ]
261 it.entries += createIntStatisticEntry => [ 228 it.entries += createIntStatisticEntry => [
262 it.name = "GlobalConstraintEvaluationTime" it.value = (strategy.globalConstraintEvaluationTime/1000000) as int 229 it.name = "GlobalConstraintEvaluationTime"
230 it.value = (strategy.globalConstraintEvaluationTime / 1000000) as int
263 ] 231 ]
264 it.entries += createIntStatisticEntry => [ 232 it.entries += createIntStatisticEntry => [
265 it.name = "FitnessCalculationTime" it.value = (strategy.fitnessCalculationTime/1000000) as int 233 it.name = "FitnessCalculationTime"
234 it.value = (strategy.fitnessCalculationTime / 1000000) as int
266 ] 235 ]
267 it.entries += createIntStatisticEntry => [ 236 it.entries += createIntStatisticEntry => [
268 it.name = "SolutionCopyTime" it.value = (solutionSaver.totalCopierRuntime/1000000) as int 237 it.name = "SolutionCopyTime"
238 it.value = (solutionSaver.totalCopierRuntime / 1000000) as int
269 ] 239 ]
270 it.entries += createIntStatisticEntry => [ 240 it.entries += createIntStatisticEntry => [
271 it.name = "ActivationSelectionTime" it.value = (strategy.activationSelector.runtime/1000000) as int 241 it.name = "ActivationSelectionTime"
242 it.value = (strategy.activationSelector.runtime / 1000000) as int
272 ] 243 ]
273 it.entries += createIntStatisticEntry => [ 244 it.entries += createIntStatisticEntry => [
274 it.name = "Decisions" 245 it.name = "Decisions"
@@ -287,27 +258,34 @@ class ViatraReasoner extends LogicReasoner {
287 it.value = method.statistics.scopePropagatorSolverInvocations 258 it.value = method.statistics.scopePropagatorSolverInvocations
288 ] 259 ]
289 it.entries += createIntStatisticEntry => [ 260 it.entries += createIntStatisticEntry => [
290 it.name = "NumericalSolverSumTime" it.value = (strategy.numericSolver.runtime/1000000) as int 261 it.name = "NumericalSolverSumTime"
262 it.value = (strategy.numericSolver.runtime / 1000000) as int
291 ] 263 ]
292 it.entries += createIntStatisticEntry => [ 264 it.entries += createIntStatisticEntry => [
293 it.name = "NumericalSolverProblemFormingTime" it.value = (strategy.numericSolver.solverFormingProblem/1000000) as int 265 it.name = "NumericalSolverProblemFormingTime"
266 it.value = (strategy.numericSolver.solverFormingProblem / 1000000) as int
294 ] 267 ]
295 it.entries += createIntStatisticEntry => [ 268 it.entries += createIntStatisticEntry => [
296 it.name = "NumericalSolverSolvingTime" it.value = (strategy.numericSolver.solverSolvingProblem/1000000) as int 269 it.name = "NumericalSolverSolvingTime"
270 it.value = (strategy.numericSolver.solverSolvingProblem / 1000000) as int
297 ] 271 ]
298 it.entries += createIntStatisticEntry => [ 272 it.entries += createIntStatisticEntry => [
299 it.name = "NumericalSolverInterpretingSolution" it.value = (strategy.numericSolver.solverSolution/1000000) as int 273 it.name = "NumericalSolverInterpretingSolution"
274 it.value = (strategy.numericSolver.solverSolution / 1000000) as int
300 ] 275 ]
301 it.entries += createIntStatisticEntry => [ 276 it.entries += createIntStatisticEntry => [
302 it.name = "NumericalSolverCachingTime" it.value = (strategy.numericSolver.cachingTime/1000000) as int 277 it.name = "NumericalSolverCachingTime"
278 it.value = (strategy.numericSolver.cachingTime / 1000000) as int
303 ] 279 ]
304 it.entries += createIntStatisticEntry => [ 280 it.entries += createIntStatisticEntry => [
305 it.name = "NumericalSolverCallNumber" it.value = strategy.numericSolver.numberOfSolverCalls 281 it.name = "NumericalSolverCallNumber"
282 it.value = strategy.numericSolver.numberOfSolverCalls
306 ] 283 ]
307 it.entries += createIntStatisticEntry => [ 284 it.entries += createIntStatisticEntry => [
308 it.name = "NumericalSolverCachedAnswerNumber" it.value = strategy.numericSolver.numberOfCachedSolverCalls 285 it.name = "NumericalSolverCachedAnswerNumber"
286 it.value = strategy.numericSolver.numberOfCachedSolverCalls
309 ] 287 ]
310 if(diversityChecker.active) { 288 if (diversityChecker.active) {
311 it.entries += createIntStatisticEntry => [ 289 it.entries += createIntStatisticEntry => [
312 it.name = "SolutionDiversityCheckTime" 290 it.name = "SolutionDiversityCheckTime"
313 it.value = (diversityChecker.totalRuntime / 1000000) as int 291 it.value = (diversityChecker.totalRuntime / 1000000) as int