Refactor optimization result and objective classes + add preliminary support for multiple objectives (#6459)

This PR is one part of multiple.
Preliminary support means currently only supports single objective.
It supports queue-ing up objectives and it always optimizes the first.
Multiple-obj optimization algorithm will be up next.

*  Refactor optimization result and objective classes
*  Add preliminary support for multiple objectives
* The unit tests are now comparing node values instead of node addresses

2 files changed, 150 insertions, 106 deletions

diff --git a/src/smt/optimization_solver.cpp b/src/smt/optimization_solver.cpp
index f854ec402..1c8fe6514 100644
--- a/src/smt/optimization_solver.cpp
+++ b/src/smt/optimization_solver.cpp
@@ -16,78 +16,54 @@
 #include "smt/optimization_solver.h"
 
 #include "omt/omt_optimizer.h"
+#include "smt/assertions.h"
 
 using namespace cvc5::theory;
 using namespace cvc5::omt;
 namespace cvc5 {
 namespace smt {
 
-/**
- * d_activatedObjective is initialized to a default objective:
- * default objective constructed with Null Node and OBJECTIVE_UNDEFINED
- *
- * d_savedValue is initialized to a default node (Null Node)
- */
-
-OptimizationSolver::OptimizationSolver(SmtEngine* parent)
-    : d_parent(parent),
-      d_activatedObjective(Node(), ObjectiveType::OBJECTIVE_UNDEFINED),
-      d_savedValue()
+OptimizationResult::ResultType OptimizationSolver::checkOpt()
 {
-}
-
-OptimizationSolver::~OptimizationSolver() {}
-
-OptResult OptimizationSolver::checkOpt()
-{
-  // Make sure that the objective is not the default one
-  Assert(d_activatedObjective.getType() != ObjectiveType::OBJECTIVE_UNDEFINED);
-  Assert(!d_activatedObjective.getNode().isNull());
-
+  Assert(d_objectives.size() == 1);
+  // NOTE: currently we are only dealing with single obj
   std::unique_ptr<OMTOptimizer> optimizer = OMTOptimizer::getOptimizerForNode(
-      d_activatedObjective.getNode(), d_activatedObjective.getSigned());
+      d_objectives[0].getTarget(), d_objectives[0].bvIsSigned());
 
-  Assert(optimizer != nullptr);
+  if (!optimizer) return OptimizationResult::UNSUPPORTED;
 
-  std::pair<OptResult, Node> optResult;
-  if (d_activatedObjective.getType() == ObjectiveType::OBJECTIVE_MAXIMIZE)
+  OptimizationResult optResult;
+  if (d_objectives[0].getType() == OptimizationObjective::MAXIMIZE)
   {
-    optResult = optimizer->maximize(this->d_parent,
-                                    this->d_activatedObjective.getNode());
+    optResult = optimizer->maximize(d_parent, d_objectives[0].getTarget());
   }
-  else if (d_activatedObjective.getType() == ObjectiveType::OBJECTIVE_MINIMIZE)
+  else if (d_objectives[0].getType() == OptimizationObjective::MINIMIZE)
   {
-    optResult = optimizer->minimize(this->d_parent,
-                                    this->d_activatedObjective.getNode());
+    optResult = optimizer->minimize(d_parent, d_objectives[0].getTarget());
   }
 
-  this->d_savedValue = optResult.second;
-  return optResult.first;
+  d_results[0] = optResult;
+  return optResult.getType();
 }
 
-void OptimizationSolver::activateObj(const Node& obj,
-                                     const ObjectiveType type,
-                                     bool bvSigned)
+void OptimizationSolver::pushObjective(
+    TNode target, OptimizationObjective::ObjectiveType type, bool bvSigned)
 {
-  d_activatedObjective = Objective(obj, type, bvSigned);
+  d_objectives.emplace_back(target, type, bvSigned);
+  d_results.emplace_back(OptimizationResult::UNSUPPORTED, Node());
 }
 
-Node OptimizationSolver::objectiveGetValue()
+void OptimizationSolver::popObjective()
 {
-  Assert(!d_savedValue.isNull());
-  return d_savedValue;
+  d_objectives.pop_back();
+  d_results.pop_back();
 }
 
-Objective::Objective(Node obj, ObjectiveType type, bool bvSigned)
-    : d_type(type), d_node(obj), d_bvSigned(bvSigned)
+std::vector<OptimizationResult> OptimizationSolver::getValues()
 {
+  Assert(d_objectives.size() == d_results.size());
+  return d_results;
 }
 
-ObjectiveType Objective::getType() { return d_type; }
-
-Node Objective::getNode() { return d_node; }
-
-bool Objective::getSigned() { return d_bvSigned; }
-
 }  // namespace smt
 }  // namespace cvc5
diff --git a/src/smt/optimization_solver.h b/src/smt/optimization_solver.h
index 59c228e27..0babd7a4a 100644
--- a/src/smt/optimization_solver.h
+++ b/src/smt/optimization_solver.h
@@ -20,7 +20,6 @@
 
 #include "expr/node.h"
 #include "expr/type_node.h"
-#include "smt/assertions.h"
 #include "util/result.h"
 
 namespace cvc5 {
@@ -30,40 +29,67 @@ class SmtEngine;
 namespace smt {
 
 /**
- * An enum for optimization queries.
- *
- * Represents whether an objective should be minimized or maximized
- */
-enum class ObjectiveType
-{
-  OBJECTIVE_MINIMIZE,
-  OBJECTIVE_MAXIMIZE,
-  OBJECTIVE_UNDEFINED
-};
-
-/**
- * An enum for optimization queries.
- *
- * Represents the result of a checkopt query
- * (unimplemented) OPT_OPTIMAL: if value was found
+ * 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
  */
-enum class OptResult
+class OptimizationResult
 {
-  // the original set of assertions has result UNKNOWN
-  OPT_UNKNOWN,
-  // the original set of assertions has result UNSAT
-  OPT_UNSAT,
-  // the optimization loop finished and optimal
-  OPT_OPTIMAL,
+ public:
+  /**
+   * Enum indicating whether the checkOpt result
+   * is optimal or not.
+   **/
+  enum ResultType
+  {
+    // the type of the target is not supported
+    UNSUPPORTED,
+    // 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,
+  };
 
-  // the goal is unbounded, so it would be -inf or +inf
-  OPT_UNBOUNDED,
+  /**
+   * Constructor
+   * @param type the optimization outcome
+   * @param value the optimized value
+   **/
+  OptimizationResult(ResultType type, TNode value)
+      : d_type(type), d_value(value)
+  {
+  }
+  OptimizationResult() : d_type(UNSUPPORTED), d_value() {}
+  ~OptimizationResult() = default;
 
-  // The last value is here as a preparation for future work
-  // in which pproximate optimizations will be supported.
+  /**
+   * Returns an enum indicating whether
+   * the result is optimal or not.
+   * @return an enum showing whether the result is optimal, unbounded,
+   *   unsat, unknown or unsupported.
+   **/
+  ResultType getType() { return d_type; }
+  /**
+   * 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
+   **/
+  Node getValue() { return d_value; }
 
-  // if the solver halted early and value is only approximate
-  OPT_SAT_APPROX
+ 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 **/
+  Node d_value;
 };
 
 /**
@@ -72,38 +98,58 @@ enum class OptResult
  * - whether it's maximize/minimize
  * - and whether it's signed for BitVectors
  */
-class Objective
+class OptimizationObjective
 {
  public:
   /**
+   * An enum for optimization queries.
+   * Represents whether an objective should be minimized or maximized
+   */
+  enum ObjectiveType
+  {
+    MINIMIZE,
+    MAXIMIZE,
+  };
+
+  /**
    * Constructor
-   * @param n the optimization target node
+   * @param target the optimization target node
    * @param type speficies whether it's maximize/minimize
    * @param bvSigned specifies whether it's using signed or unsigned comparison
    *    for BitVectors this parameter is only valid when the type of target node
    *    is BitVector
    **/
-  Objective(Node n, ObjectiveType type, bool bvSigned = false);
-  ~Objective(){};
+  OptimizationObjective(TNode target, ObjectiveType type, bool bvSigned = false)
+      : d_type(type), d_target(target), d_bvSigned(bvSigned)
+  {
+  }
+  ~OptimizationObjective() = default;
 
   /** A getter for d_type **/
-  ObjectiveType getType();
-  /** A getter for d_node **/
-  Node getNode();
+  ObjectiveType getType() { return d_type; }
+
+  /** A getter for d_target **/
+  Node getTarget() { return d_target; }
+
   /** A getter for d_bvSigned **/
-  bool getSigned();
+  bool bvIsSigned() { return d_bvSigned; }
 
  private:
-  /** The type of objective this is, either OBJECTIVE_MAXIMIZE OR
-   * OBJECTIVE_MINIMIZE  **/
+  /**
+   * The type of objective,
+   * it's either MAXIMIZE OR MINIMIZE
+   **/
   ObjectiveType d_type;
-  /** The node associated to the term that was used to construct the objective.
-   * **/
-  Node d_node;
 
-  /** Specify whether to use signed or unsigned comparison
+  /**
+   * The node associated to the term that was used to construct the objective.
+   **/
+  Node d_target;
+
+  /**
+   * Specify whether to use signed or unsigned comparison
    * for BitVectors (only for BitVectors), this variable is defaulted to false
-   * **/
+   **/
   bool d_bvSigned;
 };
 
@@ -122,32 +168,54 @@ class OptimizationSolver
    * Constructor
    * @param parent the smt_solver that the user added their assertions to
    **/
-  OptimizationSolver(SmtEngine* parent);
-  ~OptimizationSolver();
+  OptimizationSolver(SmtEngine* parent)
+      : d_parent(parent), d_objectives(), d_results()
+  {
+  }
+  ~OptimizationSolver() = default;
 
-  /** Runs the optimization loop for the activated objective **/
-  OptResult checkOpt();
   /**
-   * Activates an objective: will be optimized for
-   * @param obj the Node representing the expression that will be optimized for
+   * Run the optimization loop for the pushed objective
+   * NOTE: this function currently supports only single objective
+   * for multiple pushed objectives it always optimizes the first one.
+   * Add support for multi-obj later
+   */
+  OptimizationResult::ResultType checkOpt();
+
+  /**
+   * Push an objective.
+   * @param target the Node representing the expression that will be optimized
+   *for
    * @param type specifies whether it's maximize or minimize
    * @param bvSigned specifies whether we should use signed/unsigned
    *   comparison for BitVectors (only effective for BitVectors)
    *   and its default is false
    **/
-  void activateObj(const Node& obj,
-                   const ObjectiveType type,
-                   bool bvSigned = false);
-  /** Gets the value of the optimized objective after checkopt is called **/
-  Node objectiveGetValue();
+  void pushObjective(TNode target,
+                     OptimizationObjective::ObjectiveType type,
+                     bool bvSigned = false);
+
+  /**
+   * Pop the most recent objective.
+   **/
+  void popObjective();
+
+  /**
+   * Returns the values of the optimized objective after checkOpt is called
+   * @return a vector of Optimization Result,
+   *   each containing the outcome and the value.
+   **/
+  std::vector<OptimizationResult> getValues();
 
  private:
   /** The parent SMT engine **/
   SmtEngine* d_parent;
+
   /** The objectives to optimize for **/
-  Objective d_activatedObjective;
-  /** A saved value of the objective from the last sat call. **/
-  Node d_savedValue;
+  std::vector<OptimizationObjective> d_objectives;
+
+  /** The results of the optimizations from the last checkOpt call **/
+  std::vector<OptimizationResult> d_results;
 };
 
 }  // namespace smt