Add support for Box optimization (#6599)

Add support for box optimization -- independently optimize each goal as if the other goals do not exist.
Single minimize() / maximize() now maintains the pushed / popped context.
Of course unit tests are here as well.

9 files changed, 244 insertions, 51 deletions

diff --git a/src/omt/bitvector_optimizer.cpp b/src/omt/bitvector_optimizer.cpp
index cd233295e..bce6c9b6d 100644
--- a/src/omt/bitvector_optimizer.cpp
+++ b/src/omt/bitvector_optimizer.cpp
@@ -1,6 +1,6 @@
 /******************************************************************************
  * Top contributors (to current version):
- *   Yancheng Ou, Michael Chang
+ *   Yancheng Ou
  *
  * This file is part of the cvc5 project.
  *
@@ -106,6 +106,7 @@ OptimizationResult OMTOptimizerBitVector::minimize(SmtEngine* optChecker,
     intermediateSatResult = optChecker->checkSat();
     if (intermediateSatResult.isUnknown() || intermediateSatResult.isNull())
     {
+      optChecker->pop();
       return OptimizationResult(OptimizationResult::UNKNOWN, value);
     }
     if (intermediateSatResult.isSat() == Result::SAT)
@@ -120,6 +121,7 @@ OptimizationResult OMTOptimizerBitVector::minimize(SmtEngine* optChecker,
         // lowerBound == pivot ==> upperbound = lowerbound + 1
         // and lowerbound <= target < upperbound is UNSAT
         // return the upperbound
+        optChecker->pop();
         return OptimizationResult(OptimizationResult::OPTIMAL, value);
       }
       else
@@ -129,6 +131,7 @@ OptimizationResult OMTOptimizerBitVector::minimize(SmtEngine* optChecker,
     }
     else
     {
+      optChecker->pop();
       return OptimizationResult(OptimizationResult::UNKNOWN, value);
     }
     optChecker->pop();
@@ -195,6 +198,7 @@ OptimizationResult OMTOptimizerBitVector::maximize(SmtEngine* optChecker,
     intermediateSatResult = optChecker->checkSat();
     if (intermediateSatResult.isUnknown() || intermediateSatResult.isNull())
     {
+      optChecker->pop();
       return OptimizationResult(OptimizationResult::UNKNOWN, value);
     }
     if (intermediateSatResult.isSat() == Result::SAT)
@@ -209,6 +213,7 @@ OptimizationResult OMTOptimizerBitVector::maximize(SmtEngine* optChecker,
         // upperbound = lowerbound + 1
         // and lowerbound < target <= upperbound is UNSAT
         // return the lowerbound
+        optChecker->pop();
         return OptimizationResult(OptimizationResult::OPTIMAL, value);
       }
       else
@@ -218,6 +223,7 @@ OptimizationResult OMTOptimizerBitVector::maximize(SmtEngine* optChecker,
     }
     else
     {
+      optChecker->pop();
       return OptimizationResult(OptimizationResult::UNKNOWN, value);
     }
     optChecker->pop();
diff --git a/src/omt/integer_optimizer.cpp b/src/omt/integer_optimizer.cpp
index 5e3dc15ff..045268337 100644
--- a/src/omt/integer_optimizer.cpp
+++ b/src/omt/integer_optimizer.cpp
@@ -1,6 +1,6 @@
 /******************************************************************************
  * Top contributors (to current version):
- *   Yancheng Ou, Michael Chang
+ *   Michael Chang, Yancheng Ou
  *
  * This file is part of the cvc5 project.
  *
@@ -29,7 +29,7 @@ OptimizationResult OMTOptimizerInteger::optimize(SmtEngine* optChecker,
   // the smt engine to which we send intermediate queries
   // for the linear search.
   NodeManager* nm = optChecker->getNodeManager();
-
+  optChecker->push();
   Result intermediateSatResult = optChecker->checkSat();
   // Model-value of objective (used in optimization loop)
   Node value;
@@ -41,7 +41,7 @@ OptimizationResult OMTOptimizerInteger::optimize(SmtEngine* optChecker,
   {
     return OptimizationResult(OptimizationResult::UNSAT, value);
   }
-  // asserts objective > old_value (used in optimization loop)
+  // node storing target > old_value (used in optimization loop)
   Node increment;
   Kind incrementalOperator = kind::NULL_EXPR;
   if (isMinimize)
@@ -68,6 +68,7 @@ OptimizationResult OMTOptimizerInteger::optimize(SmtEngine* optChecker,
     optChecker->assertFormula(increment);
     intermediateSatResult = optChecker->checkSat();
   }
+  optChecker->pop();
   return OptimizationResult(OptimizationResult::OPTIMAL, value);
 }
 
diff --git a/src/omt/omt_optimizer.cpp b/src/omt/omt_optimizer.cpp
index bcf84cb53..08f1809ec 100644
--- a/src/omt/omt_optimizer.cpp
+++ b/src/omt/omt_optimizer.cpp
@@ -1,6 +1,6 @@
 /******************************************************************************
  * Top contributors (to current version):
- *   Yancheng Ou, Michael Chang, Aina Niemetz
+ *   Yancheng Ou, Aina Niemetz
  *
  * This file is part of the cvc5 project.
  *
@@ -47,7 +47,8 @@ std::unique_ptr<OMTOptimizer> OMTOptimizer::getOptimizerForObjective(
   }
   else
   {
-    return nullptr;
+    Unimplemented() << "Target type " << objectiveType
+                    << " does not support optimization";
   }
 }
 
@@ -81,7 +82,8 @@ Node OMTOptimizer::mkStrongIncrementalExpression(
       }
       else
       {
-        Unimplemented() << "Target type does not support optimization";
+        Unimplemented() << "Target type " << targetType
+                        << " does not support optimization";
       }
     }
     case OptimizationObjective::MAXIMIZE:
@@ -102,7 +104,8 @@ Node OMTOptimizer::mkStrongIncrementalExpression(
       }
       else
       {
-        Unimplemented() << "Target type does not support optimization";
+        Unimplemented() << "Target type " << targetType
+                        << " does not support optimization";
       }
     }
     default:
@@ -143,7 +146,8 @@ Node OMTOptimizer::mkWeakIncrementalExpression(NodeManager* nm,
       }
       else
       {
-        Unimplemented() << "Target type does not support optimization";
+        Unimplemented() << "Target type " << targetType
+                        << " does not support optimization";
       }
     }
     case OptimizationObjective::MAXIMIZE:
@@ -164,7 +168,8 @@ Node OMTOptimizer::mkWeakIncrementalExpression(NodeManager* nm,
       }
       else
       {
-        Unimplemented() << "Target type does not support optimization";
+        Unimplemented() << "Target type " << targetType
+                        << " does not support optimization";
       }
     }
     default:
diff --git a/src/smt/optimization_solver.cpp b/src/smt/optimization_solver.cpp
index e66e4e2ca..f73bc90b7 100644
--- a/src/smt/optimization_solver.cpp
+++ b/src/smt/optimization_solver.cpp
@@ -1,6 +1,6 @@
 /******************************************************************************
  * Top contributors (to current version):
- *   Michael Chang, Yancheng Ou, Aina Niemetz
+ *   Yancheng Ou, Michael Chang, Aina Niemetz
  *
  * This file is part of the cvc5 project.
  *
@@ -26,41 +26,43 @@ using namespace cvc5::omt;
 namespace cvc5 {
 namespace smt {
 
-OptimizationResult::ResultType OptimizationSolver::checkOpt()
+OptimizationSolver::OptimizationSolver(SmtEngine* parent)
+    : d_parent(parent),
+      d_optChecker(),
+      d_objectives(),
+      d_results(),
+      d_objectiveCombination(BOX)
 {
-  Assert(d_objectives.size() == 1);
-  // NOTE: currently we are only dealing with single obj
-  std::unique_ptr<OMTOptimizer> optimizer =
-      OMTOptimizer::getOptimizerForObjective(d_objectives[0]);
-
-  if (!optimizer) return OptimizationResult::UNSUPPORTED;
+}
 
-  OptimizationResult optResult;
-  std::unique_ptr<SmtEngine> optChecker = createOptCheckerWithTimeout(d_parent);
-  if (d_objectives[0].getType() == OptimizationObjective::MAXIMIZE)
-  {
-    optResult =
-        optimizer->maximize(optChecker.get(), d_objectives[0].getTarget());
-  }
-  else if (d_objectives[0].getType() == OptimizationObjective::MINIMIZE)
+OptimizationResult::ResultType OptimizationSolver::checkOpt()
+{
+  switch (d_objectiveCombination)
   {
-    optResult =
-        optimizer->minimize(optChecker.get(), d_objectives[0].getTarget());
+    case BOX: return optimizeBox(); break;
+    default:
+      Unimplemented()
+          << "Only BOX objective combination is supported in current version";
   }
-
-  d_results[0] = optResult;
-  return optResult.getType();
+  Unreachable();
 }
 
 void OptimizationSolver::pushObjective(
     TNode target, OptimizationObjective::ObjectiveType type, bool bvSigned)
 {
+  if (!OMTOptimizer::nodeSupportsOptimization(target))
+  {
+    CVC5_FATAL()
+        << "Objective not pushed: Target node does not support optimization";
+  }
+  d_optChecker.reset();
   d_objectives.emplace_back(target, type, bvSigned);
-  d_results.emplace_back(OptimizationResult::UNSUPPORTED, Node());
+  d_results.emplace_back(OptimizationResult::UNKNOWN, Node());
 }
 
 void OptimizationSolver::popObjective()
 {
+  d_optChecker.reset();
   d_objectives.pop_back();
   d_results.pop_back();
 }
@@ -71,6 +73,12 @@ std::vector<OptimizationResult> OptimizationSolver::getValues()
   return d_results;
 }
 
+void OptimizationSolver::setObjectiveCombination(
+    ObjectiveCombination combination)
+{
+  d_objectiveCombination = combination;
+}
+
 std::unique_ptr<SmtEngine> OptimizationSolver::createOptCheckerWithTimeout(
     SmtEngine* parentSMTSolver, bool needsTimeout, unsigned long timeout)
 {
@@ -91,5 +99,56 @@ std::unique_ptr<SmtEngine> OptimizationSolver::createOptCheckerWithTimeout(
   return optChecker;
 }
 
+OptimizationResult::ResultType OptimizationSolver::optimizeBox()
+{
+  // resets the optChecker
+  d_optChecker = createOptCheckerWithTimeout(d_parent);
+  OptimizationResult partialResult;
+  OptimizationResult::ResultType aggregatedResultType =
+      OptimizationResult::OPTIMAL;
+  std::unique_ptr<OMTOptimizer> optimizer;
+  for (size_t i = 0, numObj = d_objectives.size(); i < numObj; ++i)
+  {
+    optimizer = OMTOptimizer::getOptimizerForObjective(d_objectives[i]);
+    // checks whether the objective type is maximize or minimize
+    switch (d_objectives[i].getType())
+    {
+      case OptimizationObjective::MAXIMIZE:
+        partialResult = optimizer->maximize(d_optChecker.get(),
+                                            d_objectives[i].getTarget());
+        break;
+      case OptimizationObjective::MINIMIZE:
+        partialResult = optimizer->minimize(d_optChecker.get(),
+                                            d_objectives[i].getTarget());
+        break;
+      default:
+        CVC5_FATAL()
+            << "Optimization objective is neither MAXIMIZE nor MINIMIZE";
+    }
+    // match the optimization result type, and aggregate the results of
+    // subproblems
+    switch (partialResult.getType())
+    {
+      case OptimizationResult::OPTIMAL: break;
+      case OptimizationResult::UNBOUNDED: break;
+      case OptimizationResult::UNSAT:
+        if (aggregatedResultType == OptimizationResult::OPTIMAL)
+        {
+          aggregatedResultType = OptimizationResult::UNSAT;
+        }
+        break;
+      case OptimizationResult::UNKNOWN:
+        aggregatedResultType = OptimizationResult::UNKNOWN;
+        break;
+      default: Unreachable();
+    }
+
+    d_results[i] = partialResult;
+  }
+  // kill optChecker after optimization ends
+  d_optChecker.reset();
+  return aggregatedResultType;
+}
+
 }  // namespace smt
 }  // namespace cvc5
diff --git a/src/smt/optimization_solver.h b/src/smt/optimization_solver.h
index 3037c2924..0a1883737 100644
--- a/src/smt/optimization_solver.h
+++ b/src/smt/optimization_solver.h
@@ -1,6 +1,6 @@
 /******************************************************************************
  * Top contributors (to current version):
- *   Michael Chang, Yancheng Ou, Aina Niemetz
+ *   Yancheng Ou, Michael Chang, Aina Niemetz
  *
  * This file is part of the cvc5 project.
  *
@@ -44,8 +44,6 @@ class OptimizationResult
    **/
   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
@@ -67,14 +65,14 @@ class OptimizationResult
       : d_type(type), d_value(value)
   {
   }
-  OptimizationResult() : d_type(UNSUPPORTED), d_value() {}
+  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, unknown or unsupported.
+   *   unsat or unknown.
    **/
   ResultType getType() { return d_type; }
   /**
@@ -165,20 +163,38 @@ class OptimizationSolver
 {
  public:
   /**
+   * An enum specifying how multiple objectives are dealt with.
+   * Definition:
+   *   phi(x, y): set of assertions with variables x and y
+   *
+   * Box: treat the objectives as independent objectives
+   *   v_x = max(x) s.t. phi(x, y) = sat
+   *   v_y = max(y) s.t. phi(x, y) = sat
+   *
+   * Lexicographic: optimize the objectives one-by-one, in the order they push
+   *   v_x = max(x) s.t. phi(x, y) = sat
+   *   v_y = max(y) s.t. phi(v_x, y) = sat
+   *
+   * Pareto: optimize multiple goals to a state such that
+   *   further optimization of one goal will worsen the other goal(s)
+   *   (v_x, v_y) s.t. phi(v_x, v_y) = sat, and
+   *     forall (x, y), (phi(x, y) = sat) -> (x <= v_x or y <= v_y)
+   **/
+  enum ObjectiveCombination
+  {
+    BOX,
+    LEXICOGRAPHIC,
+    PARETO,
+  };
+  /**
    * Constructor
    * @param parent the smt_solver that the user added their assertions to
    **/
-  OptimizationSolver(SmtEngine* parent)
-      : d_parent(parent), d_objectives(), d_results()
-  {
-  }
+  OptimizationSolver(SmtEngine* parent);
   ~OptimizationSolver() = default;
 
   /**
    * 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();
 
@@ -196,7 +212,7 @@ class OptimizationSolver
                      bool bvSigned = false);
 
   /**
-   * Pop the most recent objective.
+   * Pop the most recently successfully-pushed objective.
    **/
   void popObjective();
 
@@ -207,6 +223,11 @@ class OptimizationSolver
    **/
   std::vector<OptimizationResult> getValues();
 
+  /**
+   * Sets the objective combination
+   **/
+  void setObjectiveCombination(ObjectiveCombination combination);
+
  private:
   /**
    * Initialize an SMT subsolver for offline optimization purpose
@@ -221,14 +242,28 @@ class OptimizationSolver
       bool needsTimeout = false,
       unsigned long timeout = 0);
 
-  /** The parent SMT engine **/
+  /**
+   * 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.
+   **/
+  OptimizationResult::ResultType optimizeBox();
+
+  /** A pointer to the parent SMT engine **/
   SmtEngine* d_parent;
 
+  /** A subsolver for offline optimization **/
+  std::unique_ptr<SmtEngine> d_optChecker;
+
   /** The objectives to optimize for **/
   std::vector<OptimizationObjective> d_objectives;
 
   /** 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
diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt
index 9fb0e21f1..5d5f4c680 100644
--- a/test/unit/theory/CMakeLists.txt
+++ b/test/unit/theory/CMakeLists.txt
@@ -30,6 +30,7 @@ cvc5_add_unit_test_white(theory_bv_opt_white theory)
 cvc5_add_unit_test_white(theory_bv_int_blaster_white theory)
 cvc5_add_unit_test_white(theory_engine_white theory)
 cvc5_add_unit_test_white(theory_int_opt_white theory)
+cvc5_add_unit_test_white(theory_opt_multigoal_white theory)
 cvc5_add_unit_test_white(theory_quantifiers_bv_instantiator_white theory)
 cvc5_add_unit_test_white(theory_quantifiers_bv_inverter_white theory)
 cvc5_add_unit_test_white(theory_sets_type_enumerator_white theory)
diff --git a/test/unit/theory/theory_bv_opt_white.cpp b/test/unit/theory/theory_bv_opt_white.cpp
index 3422b2784..42dcb9fee 100644
--- a/test/unit/theory/theory_bv_opt_white.cpp
+++ b/test/unit/theory/theory_bv_opt_white.cpp
@@ -1,6 +1,6 @@
 /******************************************************************************
  * Top contributors (to current version):
- *   Yancheng Ou, Michael Chang
+ *   Yancheng Ou
  *
  * This file is part of the cvc5 project.
  *
@@ -164,5 +164,6 @@ TEST_F(TestTheoryWhiteBVOpt, min_boundary)
   d_optslv->popObjective();
 }
 
+
 }  // namespace test
 }  // namespace cvc5
diff --git a/test/unit/theory/theory_int_opt_white.cpp b/test/unit/theory/theory_int_opt_white.cpp
index 770927544..efb963f16 100644
--- a/test/unit/theory/theory_int_opt_white.cpp
+++ b/test/unit/theory/theory_int_opt_white.cpp
@@ -59,7 +59,6 @@ TEST_F(TestTheoryWhiteIntOpt, max)
   d_smtEngine->assertFormula(upb);
   d_smtEngine->assertFormula(lowb);
 
-
   // We activate our objective so the subsolver knows to optimize it
   d_optslv->pushObjective(max_cost, OptimizationObjective::MAXIMIZE);
 
@@ -91,7 +90,6 @@ TEST_F(TestTheoryWhiteIntOpt, min)
   d_smtEngine->assertFormula(upb);
   d_smtEngine->assertFormula(lowb);
 
-
   // We activate our objective so the subsolver knows to optimize it
   d_optslv->pushObjective(max_cost, OptimizationObjective::MINIMIZE);
 
@@ -123,13 +121,12 @@ TEST_F(TestTheoryWhiteIntOpt, result)
   d_smtEngine->assertFormula(upb);
   d_smtEngine->assertFormula(lowb);
 
-
   // We activate our objective so the subsolver knows to optimize it
   d_optslv->pushObjective(max_cost, OptimizationObjective::MAXIMIZE);
 
   // This should return OPT_UNSAT since 0 > x > 100 is impossible.
   OptimizationResult::ResultType r = d_optslv->checkOpt();
-  
+
   // We expect our check to have returned UNSAT
   ASSERT_EQ(r, OptimizationResult::UNSAT);
   d_optslv->popObjective();
diff --git a/test/unit/theory/theory_opt_multigoal_white.cpp b/test/unit/theory/theory_opt_multigoal_white.cpp
new file mode 100644
index 000000000..3bffc9af1
--- /dev/null
+++ b/test/unit/theory/theory_opt_multigoal_white.cpp
@@ -0,0 +1,88 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Yancheng Ou
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * White-box testing for multigoal optimization.
+ */
+#include <iostream>
+
+#include "smt/optimization_solver.h"
+#include "test_smt.h"
+#include "util/bitvector.h"
+
+namespace cvc5 {
+
+using namespace theory;
+using namespace smt;
+
+namespace test {
+
+class TestTheoryWhiteOptMultigoal : public TestSmtNoFinishInit
+{
+ protected:
+  void SetUp() override
+  {
+    TestSmtNoFinishInit::SetUp();
+    d_smtEngine->setOption("produce-assertions", "true");
+    d_smtEngine->finishInit();
+
+    d_BV32Type.reset(new TypeNode(d_nodeManager->mkBitVectorType(32u)));
+  }
+
+  std::unique_ptr<TypeNode> d_BV32Type;
+};
+
+TEST_F(TestTheoryWhiteOptMultigoal, box)
+{
+  d_smtEngine->resetAssertions();
+  Node x = d_nodeManager->mkVar(*d_BV32Type);
+  Node y = d_nodeManager->mkVar(*d_BV32Type);
+  Node z = d_nodeManager->mkVar(*d_BV32Type);
+
+  // 18 <= x
+  d_smtEngine->assertFormula(d_nodeManager->mkNode(
+      kind::BITVECTOR_ULE, d_nodeManager->mkConst(BitVector(32u, 18u)), x));
+
+  // y <= x
+  d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, y, x));
+
+  // Box optimization
+  OptimizationSolver optSolver(d_smtEngine.get());
+
+  optSolver.setObjectiveCombination(OptimizationSolver::BOX);
+
+  // minimize x
+  optSolver.pushObjective(x, OptimizationObjective::MINIMIZE, false);
+  // maximize y with `signed` comparison over bit-vectors.
+  optSolver.pushObjective(y, OptimizationObjective::MAXIMIZE, true);
+  // maximize z
+  optSolver.pushObjective(z, OptimizationObjective::MAXIMIZE, false);
+
+  OptimizationResult::ResultType r = optSolver.checkOpt();
+
+  ASSERT_EQ(r, OptimizationResult::OPTIMAL);
+
+  std::vector<OptimizationResult> results = optSolver.getValues();
+
+  // x == 18
+  ASSERT_EQ(results[0].getValue().getConst<BitVector>(), BitVector(32u, 18u));
+
+  // y == 0x7FFFFFFF
+  ASSERT_EQ(results[1].getValue().getConst<BitVector>(),
+            BitVector(32u, (unsigned)0x7FFFFFFF));
+
+  // z == 0xFFFFFFFF
+  ASSERT_EQ(results[2].getValue().getConst<BitVector>(),
+            BitVector(32u, (unsigned)0xFFFFFFFF));
+}
+
+}  // namespace test
+}  // namespace cvc5