Optimizer for BitVectors (#6213)

Adds support for BitVector optimization, which is done via offline binary search. Units tests included.
Also mildly refactors the optimizer architecture.

3 files changed, 210 insertions, 16 deletions

diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt
index 723369200..fef2bdd38 100644
--- a/test/unit/theory/CMakeLists.txt
+++ b/test/unit/theory/CMakeLists.txt
@@ -20,6 +20,7 @@ cvc4_add_unit_test_white(theory_bags_rewriter_white theory)
 cvc4_add_unit_test_white(theory_bags_type_rules_white theory)
 cvc4_add_unit_test_white(theory_bv_rewriter_white theory)
 cvc4_add_unit_test_white(theory_bv_white theory)
+cvc4_add_unit_test_white(theory_bv_opt_white theory)
 cvc4_add_unit_test_white(theory_bv_int_blaster_white theory)
 cvc4_add_unit_test_white(theory_engine_white theory)
 cvc4_add_unit_test_white(theory_int_opt_white theory)
diff --git a/test/unit/theory/theory_bv_opt_white.cpp b/test/unit/theory/theory_bv_opt_white.cpp
new file mode 100644
index 000000000..fde7a5e2e
--- /dev/null
+++ b/test/unit/theory/theory_bv_opt_white.cpp
@@ -0,0 +1,154 @@
+/*********************                                                        */
+/*! \file theory_bv_opt_white.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Yancheng Ou
+ ** This file is part of the CVC4 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.\endverbatim
+ **
+ ** \brief White-box testing for optimization module for BitVectors.
+ **/
+#include <iostream>
+
+#include "smt/optimization_solver.h"
+#include "test_smt.h"
+
+namespace cvc5 {
+
+using namespace theory;
+using namespace smt;
+
+namespace test {
+
+class TestTheoryWhiteBVOpt : public TestSmtNoFinishInit
+{
+ protected:
+  void SetUp() override
+  {
+    TestSmtNoFinishInit::SetUp();
+    d_smtEngine->setOption("produce-assertions", "true");
+    d_smtEngine->finishInit();
+
+    d_optslv.reset(new OptimizationSolver(d_smtEngine.get()));
+    d_BV32Type.reset(new TypeNode(d_nodeManager->mkBitVectorType(32u)));
+    d_BV16Type.reset(new TypeNode(d_nodeManager->mkBitVectorType(16u)));
+  }
+
+  std::unique_ptr<OptimizationSolver> d_optslv;
+  std::unique_ptr<TypeNode> d_BV32Type;
+  std::unique_ptr<TypeNode> d_BV16Type;
+};
+
+TEST_F(TestTheoryWhiteBVOpt, unsigned_min)
+{
+  Node x = d_nodeManager->mkVar(*d_BV32Type);
+
+  Node a = d_nodeManager->mkConst(BitVector(32u, (unsigned)0x3FFFFFA1));
+  Node b = d_nodeManager->mkConst(BitVector(32u, (unsigned)0xFFFFFFF1));
+
+  // (unsigned)0x3FFFFFA1 <= x <= (unsigned)0xFFFFFFF1
+  d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_ULE, a, x));
+  d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_ULE, x, b));
+
+  const ObjectiveType obj_type = ObjectiveType::OBJECTIVE_MINIMIZE;
+  d_optslv->activateObj(x, obj_type, false);
+
+  OptResult r = d_optslv->checkOpt();
+
+  ASSERT_EQ(r, OptResult::OPT_OPTIMAL);
+
+  ASSERT_EQ(d_optslv->objectiveGetValue(),
+            d_nodeManager->mkConst(BitVector(32u, (unsigned)0x3FFFFFA1)));
+
+  std::cout << "Passed!" << std::endl;
+  std::cout << "Optimized value is: " << d_optslv->objectiveGetValue()
+            << std::endl;
+}
+
+TEST_F(TestTheoryWhiteBVOpt, signed_min)
+{
+  Node x = d_nodeManager->mkVar(*d_BV32Type);
+
+  Node a = d_nodeManager->mkConst(BitVector(32u, (unsigned)0x80000000));
+  Node b = d_nodeManager->mkConst(BitVector(32u, 2147483647u));
+  // -2147483648 <= x <= 2147483647
+  d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, a, x));
+  d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, x, b));
+
+  const ObjectiveType obj_type = ObjectiveType::OBJECTIVE_MINIMIZE;
+  d_optslv->activateObj(x, obj_type, true);
+
+  OptResult r = d_optslv->checkOpt();
+
+  ASSERT_EQ(r, OptResult::OPT_OPTIMAL);
+
+  BitVector val = d_optslv->objectiveGetValue().getConst<BitVector>();
+  std::cout << "opt value is: " << val << std::endl;
+
+  // expect the minimum x = -1
+  ASSERT_EQ(d_optslv->objectiveGetValue(),
+            d_nodeManager->mkConst(BitVector(32u, (unsigned)0x80000000)));
+  std::cout << "Passed!" << std::endl;
+  std::cout << "Optimized value is: " << d_optslv->objectiveGetValue()
+            << std::endl;
+}
+
+TEST_F(TestTheoryWhiteBVOpt, unsigned_max)
+{
+  Node x = d_nodeManager->mkVar(*d_BV32Type);
+
+  Node a = d_nodeManager->mkConst(BitVector(32u, (unsigned)1));
+  Node b = d_nodeManager->mkConst(BitVector(32u, (unsigned)2));
+
+  // If the gap is too large, it will have a performance issue!!!
+  // Need binary search!
+  // (unsigned)1 <= x <= (unsigned)2
+  d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_ULE, a, x));
+  d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_ULE, x, b));
+
+  const ObjectiveType obj_type = ObjectiveType::OBJECTIVE_MAXIMIZE;
+  d_optslv->activateObj(x, obj_type, false);
+
+  OptResult r = d_optslv->checkOpt();
+
+  ASSERT_EQ(r, OptResult::OPT_OPTIMAL);
+
+  BitVector val = d_optslv->objectiveGetValue().getConst<BitVector>();
+  std::cout << "opt value is: " << val << std::endl;
+
+  ASSERT_EQ(d_optslv->objectiveGetValue(),
+            d_nodeManager->mkConst(BitVector(32u, (unsigned)2)));
+  std::cout << "Optimized value is: " << d_optslv->objectiveGetValue()
+            << std::endl;
+}
+
+TEST_F(TestTheoryWhiteBVOpt, signed_max)
+{
+  Node x = d_nodeManager->mkVar(*d_BV32Type);
+
+  Node a = d_nodeManager->mkConst(BitVector(32u, (unsigned)0x80000000));
+  Node b = d_nodeManager->mkConst(BitVector(32u, 10u));
+
+  // -2147483648 <= x <= 10
+  d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, a, x));
+  d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, x, b));
+
+  const ObjectiveType obj_type = ObjectiveType::OBJECTIVE_MAXIMIZE;
+  d_optslv->activateObj(x, obj_type, true);
+
+  OptResult r = d_optslv->checkOpt();
+
+  ASSERT_EQ(r, OptResult::OPT_OPTIMAL);
+
+  // expect the maxmum x =
+  ASSERT_EQ(d_optslv->objectiveGetValue(),
+            d_nodeManager->mkConst(BitVector(32u, 10u)));
+  std::cout << "Optimized value is: " << d_optslv->objectiveGetValue()
+            << std::endl;
+}
+
+}  // 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 6111c2640..feab15b2b 100644
--- a/test/unit/theory/theory_int_opt_white.cpp
+++ b/test/unit/theory/theory_int_opt_white.cpp
@@ -2,16 +2,17 @@
 /*! \file theory_int_opt_white.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Michael Chang
+ **   Michael Chang, Yancheng Ou
  ** This file is part of the CVC4 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.\endverbatim
  **
- ** \brief White-box testing for optimization module.
+ ** \brief White-box testing for optimization module for Integers.
  **/
 #include <iostream>
+
 #include "smt/optimization_solver.h"
 #include "test_smt.h"
 
@@ -56,20 +57,21 @@ TEST_F(TestTheoryWhiteIntOpt, max)
   d_smtEngine->assertFormula(upb);
   d_smtEngine->assertFormula(lowb);
 
-  const ObjectiveType max_type = OBJECTIVE_MAXIMIZE;
+  const ObjectiveType max_type = ObjectiveType::OBJECTIVE_MAXIMIZE;
 
   // We activate our objective so the subsolver knows to optimize it
   d_optslv->activateObj(max_cost, max_type);
 
   OptResult r = d_optslv->checkOpt();
 
+  ASSERT_EQ(r, OptResult::OPT_OPTIMAL);
+
   // We expect max_cost == 99
   ASSERT_EQ(d_optslv->objectiveGetValue(),
-                    d_nodeManager->mkConst(Rational("99")));
+            d_nodeManager->mkConst(Rational("99")));
 
-  std::cout << "Result is :" << r << std::endl;
-  std::cout << "Optimized max value is: "
-            << d_optslv->objectiveGetValue() << std::endl;
+  std::cout << "Optimized max value is: " << d_optslv->objectiveGetValue()
+            << std::endl;
 }
 
 TEST_F(TestTheoryWhiteIntOpt, min)
@@ -89,20 +91,21 @@ TEST_F(TestTheoryWhiteIntOpt, min)
   d_smtEngine->assertFormula(upb);
   d_smtEngine->assertFormula(lowb);
 
-  const ObjectiveType min_type = OBJECTIVE_MINIMIZE;
+  const ObjectiveType min_type = ObjectiveType::OBJECTIVE_MINIMIZE;
 
   // We activate our objective so the subsolver knows to optimize it
   d_optslv->activateObj(max_cost, min_type);
 
   OptResult r = d_optslv->checkOpt();
 
+  ASSERT_EQ(r, OptResult::OPT_OPTIMAL);
+
   // We expect max_cost == 99
   ASSERT_EQ(d_optslv->objectiveGetValue(),
-                    d_nodeManager->mkConst(Rational("1")));
+            d_nodeManager->mkConst(Rational("1")));
 
-  std::cout << "Result is :" << r << std::endl;
-  std::cout << "Optimized max value is: "
-            << d_optslv->objectiveGetValue() << std::endl;
+  std::cout << "Optimized max value is: " << d_optslv->objectiveGetValue()
+            << std::endl;
 }
 
 TEST_F(TestTheoryWhiteIntOpt, result)
@@ -122,18 +125,54 @@ TEST_F(TestTheoryWhiteIntOpt, result)
   d_smtEngine->assertFormula(upb);
   d_smtEngine->assertFormula(lowb);
 
-  const ObjectiveType max_type = OBJECTIVE_MAXIMIZE;
+  const ObjectiveType max_type = ObjectiveType::OBJECTIVE_MAXIMIZE;
 
   // We activate our objective so the subsolver knows to optimize it
   d_optslv->activateObj(max_cost, max_type);
 
   // This should return OPT_UNSAT since 0 > x > 100 is impossible.
   OptResult r = d_optslv->checkOpt();
-
+  
   // We expect our check to have returned UNSAT
-  ASSERT_EQ(r, OPT_UNSAT);
+  ASSERT_EQ(r, OptResult::OPT_UNSAT);
+}
+
+TEST_F(TestTheoryWhiteIntOpt, open_interval)
+{
+  Node ub1 = d_nodeManager->mkConst(Rational("100"));
+  Node lb1 = d_nodeManager->mkConst(Rational("0"));
+  Node lb2 = d_nodeManager->mkConst(Rational("110"));
+
+  Node cost1 = d_nodeManager->mkVar(*d_intType);
+  Node cost2 = d_nodeManager->mkVar(*d_intType);
+
+  /* Result of assertion is:
+      0 < cost1 < 100
+      110 < cost2
+  */
+  d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::LT, lb1, cost1));
+  d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::LT, cost1, ub1));
 
-  std::cout << "Result is :" << r << std::endl;
+  d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::LT, lb2, cost2));
+
+  /* Optimization objective:
+      cost1 + cost2
+  */
+  Node cost3 = d_nodeManager->mkNode(kind::PLUS, cost1, cost2);
+
+  const ObjectiveType min_type = ObjectiveType::OBJECTIVE_MINIMIZE;
+  d_optslv->activateObj(cost3, min_type);
+
+  OptResult r = d_optslv->checkOpt();
+
+  ASSERT_EQ(r, OptResult::OPT_OPTIMAL);
+
+  // expect the minimum result of cost3 = cost1 + cost2 to be 1 + 111 = 112
+  ASSERT_EQ(d_optslv->objectiveGetValue(),
+            d_nodeManager->mkConst(Rational("112")));
+  std::cout << "Optimized min value is: " << d_optslv->objectiveGetValue()
+            << std::endl;
 }
+
 }  // namespace test
 }  // namespace cvc5