Optimizing generator with linear objective functions

1 files changed, 105 insertions, 7 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
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 @@
 package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
 
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.Bounds
+import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.DirectionalThresholdObjective
+import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.IObjectiveBoundsProvider
+import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveThreshold
 import java.util.HashMap
 import java.util.Map
 import org.eclipse.viatra.dse.api.DSEException
@@ -18,24 +22,32 @@ import org.eclipse.xtend.lib.annotations.Accessors
  * Will also automatically fill any missing numerical values in the saved solutions
  * using the supplied {@link NumericSolver}.
  */
-class ViatraReasonerSolutionSaver implements ISolutionSaver {
+class ViatraReasonerSolutionSaver implements ISolutionSaver, IObjectiveBoundsProvider {
+        static val TOLERANCE = 1e-10
+
         @Accessors val SolutionCopier solutionCopier
-        val NumericSolver numericSolver
         @Accessors val DiversityChecker diversityChecker
+        val IObjective[][] leveledExtremalObjectives
         val boolean hasExtremalObjectives
         val int numberOfRequiredSolutions
         val ObjectiveComparatorHelper comparatorHelper
         val Map<SolutionTrajectory, Fitness> trajectories = new HashMap
 
-        @Accessors(PUBLIC_SETTER) var Map<Object, Solution> solutionsCollection
+        @Accessors var NumericSolver numericSolver
+        @Accessors var Map<Object, Solution> solutionsCollection
 
-        new(IObjective[][] leveledExtremalObjectives, int numberOfRequiredSolutions, DiversityChecker diversityChecker, NumericSolver numericSolver) {
+        new(IObjective[][] leveledExtremalObjectives, int numberOfRequiredSolutions, DiversityChecker diversityChecker) {
                 this.diversityChecker = diversityChecker
                 comparatorHelper = new ObjectiveComparatorHelper(leveledExtremalObjectives)
+                this.leveledExtremalObjectives = leveledExtremalObjectives
                 hasExtremalObjectives = leveledExtremalObjectives.exists[!empty]
                 this.numberOfRequiredSolutions = numberOfRequiredSolutions
-                this.solutionCopier = new SolutionCopier(numericSolver)
+                this.solutionCopier = new SolutionCopier
+        }
+        
+        def setNumericSolver(NumericSolver numericSolver) {
                 this.numericSolver = numericSolver
+                solutionCopier.numericSolver = numericSolver
         }
 
         override saveSolution(ThreadContext context, Object id, SolutionTrajectory solutionTrajectory) {
@@ -51,6 +63,7 @@ class ViatraReasonerSolutionSaver implements ISolutionSaver {
                 if (!shouldSaveSolution(fitness, context)) {
                         return false
                 }
+                println("Found: " + fitness)
                 val dominatedTrajectories = newArrayList
                 for (entry : trajectories.entrySet) {
                         val isLastFitnessBetter = comparatorHelper.compare(fitness, entry.value)
@@ -99,7 +112,7 @@ class ViatraReasonerSolutionSaver implements ISolutionSaver {
         }
 
         private def shouldSaveSolution(Fitness fitness, ThreadContext context) {
-                return fitness.satisifiesHardObjectives && numericSolver.currentSatisfiable
+                fitness.satisifiesHardObjectives && (numericSolver === null || numericSolver.currentSatisfiable)
         }
 
         private def basicSaveSolution(ThreadContext context, Object id, SolutionTrajectory solutionTrajectory,
@@ -145,8 +158,93 @@ class ViatraReasonerSolutionSaver implements ISolutionSaver {
                 }
                 solutionsCollection.size < numberOfRequiredSolutions
         }
-        
+
         def getTotalCopierRuntime() {
                 solutionCopier.totalCopierRuntime
         }
+
+        override computeRequiredBounds(IObjective objective, Bounds bounds) {
+                if (!hasExtremalObjectives) {
+                        return
+                }
+                if (objective instanceof DirectionalThresholdObjective) {
+                        switch (threshold : objective.threshold) {
+                                case ObjectiveThreshold.NO_THRESHOLD: {
+                                        // No threshold to set.
+                                }
+                                ObjectiveThreshold.Exclusive: {
+                                        switch (kind : objective.kind) {
+                                                case HIGHER_IS_BETTER:
+                                                        bounds.tightenLowerBound(Math.floor(threshold.threshold + 1) as int)
+                                                case LOWER_IS_BETTER:
+                                                        bounds.tightenUpperBound(Math.ceil(threshold.threshold - 1) as int)
+                                                default:
+                                                        throw new IllegalArgumentException("Unknown objective kind" + kind)
+                                        }
+                                        if (threshold.clampToThreshold) {
+                                                return
+                                        }
+                                }
+                                ObjectiveThreshold.Inclusive: {
+                                        switch (kind : objective.kind) {
+                                                case HIGHER_IS_BETTER:
+                                                        bounds.tightenLowerBound(Math.ceil(threshold.threshold) as int)
+                                                case LOWER_IS_BETTER:
+                                                        bounds.tightenUpperBound(Math.floor(threshold.threshold) as int)
+                                                default:
+                                                        throw new IllegalArgumentException("Unknown objective kind" + kind)
+                                        }
+                                        if (threshold.clampToThreshold) {
+                                                return
+                                        }
+                                }
+                                default:
+                                        throw new IllegalArgumentException("Unknown threshold: " + threshold)
+                        }
+                        for (level : leveledExtremalObjectives) {
+                                switch (level.size) {
+                                        case 0: {
+                                                // Nothing to do, wait for the next level.
+                                        }
+                                        case 1: {
+                                                val primaryObjective = level.get(0)
+                                                if (primaryObjective != objective) {
+                                                        // There are no worst-case bounds for secondary objectives.
+                                                        return
+                                                }
+                                        }
+                                        default:
+                                                // There are no worst-case bounds for Pareto front calculation.
+                                                return
+                                }
+                        }
+                        val fitnessIterator = trajectories.values.iterator
+                        if (!fitnessIterator.hasNext) {
+                                return
+                        }
+                        val fitness = fitnessIterator.next.get(objective.name)
+                        while (fitnessIterator.hasNext) {
+                                val otherFitness = fitnessIterator.next.get(objective.name)
+                                if (Math.abs(fitness - otherFitness) > TOLERANCE) {
+                                        throw new IllegalStateException("Inconsistent fitness: " + objective.name)
+                                }
+                        }
+                        switch (kind : objective.kind) {
+                                case HIGHER_IS_BETTER:
+                                        if (needsMoreSolutionsWithSameFitness) {
+                                                bounds.tightenLowerBound(Math.floor(fitness) as int)
+                                        } else {
+                                                bounds.tightenLowerBound(Math.floor(fitness + 1) as int)
+                                        }
+                                case LOWER_IS_BETTER:
+                                        if (needsMoreSolutionsWithSameFitness) {
+                                                bounds.tightenUpperBound(Math.ceil(fitness) as int)
+                                        } else {
+                                                bounds.tightenUpperBound(Math.ceil(fitness - 1) as int)
+                                        }
+                                default:
+                                        throw new IllegalArgumentException("Unknown objective kind" + kind)
+                        }
+                }
+        }
 }