diff options
author | Kristóf Marussy <marussy@mit.bme.hu> | 2020-06-25 19:55:10 +0200 |
---|---|---|
committer | Kristóf Marussy <marussy@mit.bme.hu> | 2020-06-25 19:55:10 +0200 |
commit | c3a6d4b9cf3657070d180aa65ddbf0459e880329 (patch) | |
tree | 780c4fc61578dcb309af53fb0c164c7627e51676 /Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ViatraReasonerSolutionSaver.xtend | |
parent | New configuration language parser WIP (diff) | |
parent | Scope unsat benchmarks (diff) | |
download | VIATRA-Generator-c3a6d4b9cf3657070d180aa65ddbf0459e880329.tar.gz VIATRA-Generator-c3a6d4b9cf3657070d180aa65ddbf0459e880329.tar.zst VIATRA-Generator-c3a6d4b9cf3657070d180aa65ddbf0459e880329.zip |
Merge branch 'kris'
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ViatraReasonerSolutionSaver.xtend')
-rw-r--r-- | Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ViatraReasonerSolutionSaver.xtend | 150 |
1 files changed, 150 insertions, 0 deletions
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 new file mode 100644 index 00000000..d879d4cc --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ViatraReasonerSolutionSaver.xtend | |||
@@ -0,0 +1,150 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse | ||
2 | |||
3 | import java.util.HashMap | ||
4 | import java.util.Map | ||
5 | import org.eclipse.viatra.dse.api.DSEException | ||
6 | import org.eclipse.viatra.dse.api.Solution | ||
7 | import org.eclipse.viatra.dse.api.SolutionTrajectory | ||
8 | import org.eclipse.viatra.dse.base.ThreadContext | ||
9 | import org.eclipse.viatra.dse.objectives.Fitness | ||
10 | import org.eclipse.viatra.dse.objectives.IObjective | ||
11 | import org.eclipse.viatra.dse.objectives.ObjectiveComparatorHelper | ||
12 | import org.eclipse.viatra.dse.solutionstore.SolutionStore.ISolutionSaver | ||
13 | import org.eclipse.xtend.lib.annotations.Accessors | ||
14 | |||
15 | /** | ||
16 | * Based on {@link SolutionStore.BestSolutionSaver}. | ||
17 | * | ||
18 | * Will also automatically fill any missing numerical values in the saved solutions | ||
19 | * using the supplied {@link NumericSolver}. | ||
20 | */ | ||
21 | class ViatraReasonerSolutionSaver implements ISolutionSaver { | ||
22 | @Accessors val SolutionCopier solutionCopier | ||
23 | @Accessors val DiversityChecker diversityChecker | ||
24 | val boolean hasExtremalObjectives | ||
25 | val int numberOfRequiredSolutions | ||
26 | val ObjectiveComparatorHelper comparatorHelper | ||
27 | val Map<SolutionTrajectory, Fitness> trajectories = new HashMap | ||
28 | |||
29 | @Accessors(PUBLIC_SETTER) var Map<Object, Solution> solutionsCollection | ||
30 | |||
31 | new(IObjective[][] leveledExtremalObjectives, int numberOfRequiredSolutions, DiversityChecker diversityChecker, NumericSolver numericSolver) { | ||
32 | this.diversityChecker = diversityChecker | ||
33 | comparatorHelper = new ObjectiveComparatorHelper(leveledExtremalObjectives) | ||
34 | hasExtremalObjectives = leveledExtremalObjectives.exists[!empty] | ||
35 | this.numberOfRequiredSolutions = numberOfRequiredSolutions | ||
36 | this.solutionCopier = new SolutionCopier(numericSolver) | ||
37 | } | ||
38 | |||
39 | override saveSolution(ThreadContext context, Object id, SolutionTrajectory solutionTrajectory) { | ||
40 | if (hasExtremalObjectives) { | ||
41 | saveBestSolutionOnly(context, id, solutionTrajectory) | ||
42 | } else { | ||
43 | saveAnyDiverseSolution(context, id, solutionTrajectory) | ||
44 | } | ||
45 | } | ||
46 | |||
47 | private def saveBestSolutionOnly(ThreadContext context, Object id, SolutionTrajectory solutionTrajectory) { | ||
48 | val fitness = context.lastFitness | ||
49 | if (!shouldSaveSolution(fitness, context)) { | ||
50 | return false | ||
51 | } | ||
52 | val dominatedTrajectories = newArrayList | ||
53 | for (entry : trajectories.entrySet) { | ||
54 | val isLastFitnessBetter = comparatorHelper.compare(fitness, entry.value) | ||
55 | if (isLastFitnessBetter < 0) { | ||
56 | // Found a trajectory that dominates the current one, no need to save | ||
57 | return false | ||
58 | } | ||
59 | if (isLastFitnessBetter > 0) { | ||
60 | dominatedTrajectories += entry.key | ||
61 | } | ||
62 | } | ||
63 | if (dominatedTrajectories.size == 0 && !needsMoreSolutionsWithSameFitness) { | ||
64 | return false | ||
65 | } | ||
66 | if (!diversityChecker.newSolution(context, id, dominatedTrajectories.map[solution.stateCode])) { | ||
67 | return false | ||
68 | } | ||
69 | // We must save the new trajectory before removing dominated trajectories | ||
70 | // to avoid removing the current solution when it is reachable only via dominated trajectories. | ||
71 | val solutionSaved = basicSaveSolution(context, id, solutionTrajectory, fitness) | ||
72 | for (dominatedTrajectory : dominatedTrajectories) { | ||
73 | trajectories -= dominatedTrajectory | ||
74 | val dominatedSolution = dominatedTrajectory.solution | ||
75 | if (!dominatedSolution.trajectories.remove(dominatedTrajectory)) { | ||
76 | throw new DSEException( | ||
77 | "Dominated solution is not reachable from dominated trajectory. This should never happen!") | ||
78 | } | ||
79 | if (dominatedSolution.trajectories.empty) { | ||
80 | val dominatedSolutionId = dominatedSolution.stateCode | ||
81 | solutionCopier.markAsObsolete(dominatedSolutionId) | ||
82 | solutionsCollection -= dominatedSolutionId | ||
83 | } | ||
84 | } | ||
85 | solutionSaved | ||
86 | } | ||
87 | |||
88 | private def saveAnyDiverseSolution(ThreadContext context, Object id, SolutionTrajectory solutionTrajectory) { | ||
89 | val fitness = context.lastFitness | ||
90 | if (!shouldSaveSolution(fitness, context)) { | ||
91 | return false | ||
92 | } | ||
93 | if (!diversityChecker.newSolution(context, id, emptyList)) { | ||
94 | return false | ||
95 | } | ||
96 | basicSaveSolution(context, id, solutionTrajectory, fitness) | ||
97 | } | ||
98 | |||
99 | private def shouldSaveSolution(Fitness fitness, ThreadContext context) { | ||
100 | return fitness.satisifiesHardObjectives | ||
101 | } | ||
102 | |||
103 | private def basicSaveSolution(ThreadContext context, Object id, SolutionTrajectory solutionTrajectory, | ||
104 | Fitness fitness) { | ||
105 | var boolean solutionSaved = false | ||
106 | var dseSolution = solutionsCollection.get(id) | ||
107 | if (dseSolution === null) { | ||
108 | solutionCopier.copySolution(context, id) | ||
109 | dseSolution = new Solution(id, solutionTrajectory) | ||
110 | solutionsCollection.put(id, dseSolution) | ||
111 | solutionSaved = true | ||
112 | } else { | ||
113 | solutionSaved = dseSolution.trajectories.add(solutionTrajectory) | ||
114 | } | ||
115 | if (solutionSaved) { | ||
116 | solutionTrajectory.solution = dseSolution | ||
117 | trajectories.put(solutionTrajectory, fitness) | ||
118 | } | ||
119 | solutionSaved | ||
120 | } | ||
121 | |||
122 | def fitnessMayBeSaved(Fitness fitness) { | ||
123 | if (!hasExtremalObjectives) { | ||
124 | return true | ||
125 | } | ||
126 | var boolean mayDominate | ||
127 | for (existingFitness : trajectories.values) { | ||
128 | val isNewFitnessBetter = comparatorHelper.compare(fitness, existingFitness) | ||
129 | if (isNewFitnessBetter < 0) { | ||
130 | return false | ||
131 | } | ||
132 | if (isNewFitnessBetter > 0) { | ||
133 | mayDominate = true | ||
134 | } | ||
135 | } | ||
136 | mayDominate || needsMoreSolutionsWithSameFitness | ||
137 | } | ||
138 | |||
139 | private def boolean needsMoreSolutionsWithSameFitness() { | ||
140 | if (solutionsCollection === null) { | ||
141 | // The solutions collection will only be initialized upon saving the first solution. | ||
142 | return true | ||
143 | } | ||
144 | solutionsCollection.size < numberOfRequiredSolutions | ||
145 | } | ||
146 | |||
147 | def getTotalCopierRuntime() { | ||
148 | solutionCopier.totalCopierRuntime | ||
149 | } | ||
150 | } | ||