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.

4 files changed, 92 insertions, 5 deletions

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