[Optimization] Use Result in OptimizationResult (#6740)

OptimizationResult now contains: 
- cvc5::Result
- optimal value for objective
- whether the objective is unbounded

This gets benefit from cvc5::Result (e.g., we could get explanation for UNKNOWN) and it's slightly easier to integrate to the current API. 

Also refactors BV optimizer so that it uses switch statement (instead of if-then-else) to judge the checkSat results (I was planning to do this a long while ago)... 

1 files changed, 63 insertions, 58 deletions

diff --git a/src/smt/optimization_solver.h b/src/smt/optimization_solver.h
index 6d138deb2..d13168780 100644
--- a/src/smt/optimization_solver.h
+++ b/src/smt/optimization_solver.h
@@ -33,63 +33,75 @@ namespace smt {
 /**
  * The optimization result of an optimization objective
  * containing:
- * - whether it's optimal or not
- * - if so, the optimal value, otherwise the value might be empty node or
- *   something suboptimal
+ * - the optimization result: SAT/UNSAT/UNKNOWN
+ * - the optimal value if SAT and bounded
+ *     (optimal value reached and it's not infinity),
+ *   or an empty node if SAT and unbounded
+ *     (optimal value is +inf for maximum or -inf for minimum),
+ *   otherwise the value might be empty node
+ *   or something suboptimal
+ * - whether the objective is unbounded
  */
 class OptimizationResult
 {
  public:
   /**
-   * Enum indicating whether the checkOpt result
-   * is optimal or not.
-   **/
-  enum ResultType
-  {
-    // whether the value is optimal is UNKNOWN
-    UNKNOWN,
-    // the original set of assertions has result UNSAT
-    UNSAT,
-    // the value is optimal
-    OPTIMAL,
-    // the goal is unbounded,
-    // if objective is maximize, it's +infinity
-    // if objective is minimize, it's -infinity
-    UNBOUNDED,
-  };
-
-  /**
    * Constructor
    * @param type the optimization outcome
    * @param value the optimized value
+   * @param unbounded whether the objective is unbounded
    **/
-  OptimizationResult(ResultType type, TNode value)
-      : d_type(type), d_value(value)
+  OptimizationResult(Result result, TNode value, bool unbounded = false)
+      : d_result(result), d_value(value), d_unbounded(unbounded)
+  {
+  }
+  OptimizationResult()
+      : d_result(Result::Sat::SAT_UNKNOWN,
+                 Result::UnknownExplanation::NO_STATUS),
+        d_value(),
+        d_unbounded(false)
   {
   }
-  OptimizationResult() : d_type(UNKNOWN), d_value() {}
   ~OptimizationResult() = default;
 
   /**
    * Returns an enum indicating whether
-   * the result is optimal or not.
-   * @return an enum showing whether the result is optimal, unbounded,
-   *   unsat or unknown.
+   * the result is SAT or not.
+   * @return whether the result is SAT, UNSAT or SAT_UNKNOWN
    **/
-  ResultType getType() const { return d_type; }
+  Result getResult() const { return d_result; }
+
   /**
    * Returns the optimal value.
    * @return Node containing the optimal value,
-   *   if getType() is not OPTIMAL, it might return an empty node or a node
-   *   containing non-optimal value
+   *   if result is unbounded, this will be an empty node,
+   *   if getResult() is UNSAT, it will return an empty node,
+   *   if getResult() is SAT_UNKNOWN, it will return something suboptimal
+   *   or an empty node, depending on how the solver runs.
    **/
   Node getValue() const { return d_value; }
 
+  /**
+   * Checks whether the objective is unbouned
+   * @return whether the objective is unbounded
+   *   if the objective is unbounded (this function returns true), 
+   *   then the optimal value is:
+   *   +inf, if it's maximize;
+   *   -inf, if it's minimize
+   **/
+  bool isUnbounded() const { return d_unbounded; }
+
  private:
-  /** the indicating whether the result is optimal or something else **/
-  ResultType d_type;
-  /** if the result is optimal, this is storing the optimal value **/
+  /** indicating whether the result is SAT, UNSAT or UNKNOWN **/
+  Result d_result;
+  /** if the result is bounded, this is storing the value **/
   Node d_value;
+  /** whether the objective is unbounded
+   * If this is true, then:
+   * if objective is maximize, it's +infinity;
+   * if objective is minimize, it's -infinity
+   **/
+  bool d_unbounded;
 };
 
 /**
@@ -199,10 +211,10 @@ class OptimizationSolver
   /**
    * Run the optimization loop for the added objective
    * For multiple objective combination, it defaults to lexicographic,
-   * and combination could be set by calling
-   *   setObjectiveCombination(BOX/LEXICOGRAPHIC/PARETO)
+   * possible combinations: BOX, LEXICOGRAPHIC, PARETO
+   * @param combination BOX / LEXICOGRAPHIC / PARETO
    */
-  OptimizationResult::ResultType checkOpt();
+  Result checkOpt(ObjectiveCombination combination = LEXICOGRAPHIC);
 
   /**
    * Add an optimization objective.
@@ -223,11 +235,6 @@ class OptimizationSolver
    **/
   std::vector<OptimizationResult> getValues();
 
-  /**
-   * Sets the objective combination
-   **/
-  void setObjectiveCombination(ObjectiveCombination combination);
-
  private:
   /**
    * Initialize an SMT subsolver for offline optimization purpose
@@ -244,26 +251,26 @@ class OptimizationSolver
 
   /**
    * Optimize multiple goals in Box order
-   * @return OPTIMAL if all of the objectives are either OPTIMAL or UNBOUNDED;
-   *   UNSAT if at least one objective is UNSAT and no objective is UNKNOWN;
-   *   UNKNOWN if any of the objective is UNKNOWN.
+   * @return SAT if all of the objectives are optimal or unbounded;
+   *   UNSAT if at least one objective is UNSAT and no objective is SAT_UNKNOWN;
+   *   SAT_UNKNOWN if any of the objective is SAT_UNKNOWN.
    **/
-  OptimizationResult::ResultType optimizeBox();
+  Result optimizeBox();
 
   /**
    * Optimize multiple goals in Lexicographic order,
    * using iterative implementation
-   * @return OPTIMAL if all objectives are OPTIMAL and bounded;
-   *   UNBOUNDED if one of the objectives is UNBOUNDED
+   * @return SAT if the objectives are optimal,
+   *     if one of the objectives is unbounded,
+   *     the optimization will stop at that objective;
+   *   UNSAT if any of the objectives is UNSAT
    *     and optimization will stop at that objective;
-   *   UNSAT if one of the objectives is UNSAT
-   *     and optimization will stop at that objective;
-   *   UNKNOWN if one of the objectives is UNKNOWN
+   *   SAT_UNKNOWN if any of the objectives is UNKNOWN
    *     and optimization will stop at that objective;
    *   If the optimization is stopped at an objective,
-   *     all objectives following that objective will be UNKNOWN.
+   *     all objectives following that objective will be SAT_UNKNOWN.
    **/
-  OptimizationResult::ResultType optimizeLexicographicIterative();
+  Result optimizeLexicographicIterative();
 
   /**
    * Optimize multiple goals in Pareto order
@@ -277,11 +284,12 @@ class OptimizationSolver
    * D. Rayside, H.-C. Estler, and D. Jackson. The Guided Improvement Algorithm.
    *  Technical Report MIT-CSAIL-TR-2009-033, MIT, 2009.
    *
-   * @return if it finds a new Pareto optimal result it will return OPTIMAL;
+   * @return if it finds a new Pareto optimal result it will return SAT;
    *   if it exhausts the results in the Pareto front it will return UNSAT;
-   *   if the underlying SMT solver returns UNKNOWN, it will return UNKNOWN.
+   *   if the underlying SMT solver returns SAT_UNKNOWN,
+   *   it will return SAT_UNKNOWN.
    **/
-  OptimizationResult::ResultType optimizeParetoNaiveGIA();
+  Result optimizeParetoNaiveGIA();
 
   /** A pointer to the parent SMT engine **/
   SmtEngine* d_parent;
@@ -294,9 +302,6 @@ class OptimizationSolver
 
   /** The results of the optimizations from the last checkOpt call **/
   std::vector<OptimizationResult> d_results;
-
-  /** The current objective combination method **/
-  ObjectiveCombination d_objectiveCombination;
 };
 
 }  // namespace smt