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.

12 files changed, 887 insertions, 120 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 490d335a2..6c2af8226 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -47,6 +47,12 @@ libcvc4_add_sources(
   lib/replacements.h
   lib/strtok_r.c
   lib/strtok_r.h
+  omt/bitvector_optimizer.cpp
+  omt/bitvector_optimizer.h
+  omt/integer_optimizer.cpp
+  omt/integer_optimizer.h
+  omt/omt_optimizer.cpp
+  omt/omt_optimizer.h
   preprocessing/assertion_pipeline.cpp
   preprocessing/assertion_pipeline.h
   preprocessing/passes/ackermann.cpp
diff --git a/src/omt/bitvector_optimizer.cpp b/src/omt/bitvector_optimizer.cpp
new file mode 100644
index 000000000..c8c2a39d7
--- /dev/null
+++ b/src/omt/bitvector_optimizer.cpp
@@ -0,0 +1,239 @@
+/*********************                                                        */
+/*! \file bitvector_optimizer.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 Optimizer for BitVector type
+ **/
+
+#include "omt/bitvector_optimizer.h"
+
+#include "options/smt_options.h"
+#include "smt/smt_engine.h"
+
+using namespace cvc5::smt;
+namespace cvc5::omt {
+
+OMTOptimizerBitVector::OMTOptimizerBitVector(bool isSigned)
+    : d_isSigned(isSigned)
+{
+}
+
+BitVector OMTOptimizerBitVector::computeAverage(const BitVector& a,
+                                                const BitVector& b,
+                                                bool isSigned)
+{
+  // computes (a + b) / 2 without overflow
+  // rounding towards -infinity: -1.5 --> -2,  1.5 --> 1
+  // average = (a / 2) + (b / 2) + (((a % 2) + (b % 2)) / 2)
+  uint32_t aMod2 = static_cast<uint32_t>(a.isBitSet(0));
+  uint32_t bMod2 = static_cast<uint32_t>(b.isBitSet(0));
+  BitVector aMod2PlusbMod2(a.getSize(), (aMod2 + bMod2) / 2);
+  BitVector bv1 = BitVector::mkOne(a.getSize());
+  if (isSigned)
+  {
+    return (a.arithRightShift(bv1) + b.arithRightShift(bv1)
+            + aMod2PlusbMod2.arithRightShift(bv1));
+  }
+  else
+  {
+    return (a.logicalRightShift(bv1) + b.logicalRightShift(bv1)
+            + aMod2PlusbMod2.logicalRightShift(bv1));
+  }
+}
+
+std::pair<OptResult, Node> OMTOptimizerBitVector::minimize(
+    SmtEngine* parentSMTSolver, Node target)
+{
+  // the smt engine to which we send intermediate queries
+  // for the binary search.
+  std::unique_ptr<SmtEngine> optChecker =
+      OMTOptimizer::createOptCheckerWithTimeout(parentSMTSolver, false);
+  NodeManager* nm = optChecker->getNodeManager();
+  Result intermediateSatResult = optChecker->checkSat();
+  // Model-value of objective (used in optimization loop)
+  Node value;
+  if (intermediateSatResult.isUnknown())
+  {
+    return std::make_pair(OptResult::OPT_UNKNOWN, value);
+  }
+  if (intermediateSatResult.isSat() == Result::UNSAT)
+  {
+    return std::make_pair(OptResult::OPT_UNSAT, value);
+  }
+
+  // value equals to upperBound
+  value = optChecker->getValue(target);
+
+  // this gets the bitvector!
+  BitVector bvValue = value.getConst<BitVector>();
+  unsigned int bvSize = bvValue.getSize();
+
+  // lowerbound
+  BitVector lowerBound = ((this->d_isSigned) ? (BitVector::mkMinSigned(bvSize))
+                                             : (BitVector::mkZero(bvSize)));
+  // upperbound must be a satisfying value
+  // and value == upperbound
+  BitVector upperBound = bvValue;
+
+  Kind LTOperator =
+      ((d_isSigned) ? (kind::BITVECTOR_SLT) : (kind::BITVECTOR_ULT));
+  Kind GEOperator =
+      ((d_isSigned) ? (kind::BITVECTOR_SGE) : (kind::BITVECTOR_UGE));
+
+  // the pivot value for binary search,
+  // pivot = (lowerBound + upperBound) / 2
+  // rounded towards -infinity
+  BitVector pivot;
+  while (true)
+  {
+    if (d_isSigned)
+    {
+      if (!lowerBound.signedLessThan(upperBound)) break;
+    }
+    else
+    {
+      if (!lowerBound.unsignedLessThan(upperBound)) break;
+    }
+    pivot = computeAverage(lowerBound, upperBound, d_isSigned);
+    optChecker->push();
+    // lowerBound <= target < pivot
+    optChecker->assertFormula(
+        nm->mkNode(kind::AND,
+                   nm->mkNode(GEOperator, target, nm->mkConst(lowerBound)),
+                   nm->mkNode(LTOperator, target, nm->mkConst(pivot))));
+    intermediateSatResult = optChecker->checkSat();
+    if (intermediateSatResult.isUnknown() || intermediateSatResult.isNull())
+    {
+      return std::make_pair(OptResult::OPT_UNKNOWN, value);
+    }
+    if (intermediateSatResult.isSat() == Result::SAT)
+    {
+      value = optChecker->getValue(target);
+      upperBound = value.getConst<BitVector>();
+    }
+    else if (intermediateSatResult.isSat() == Result::UNSAT)
+    {
+      if (lowerBound == pivot)
+      {
+        // lowerBound == pivot ==> upperbound = lowerbound + 1
+        // and lowerbound <= target < upperbound is UNSAT
+        // return the upperbound
+        return std::make_pair(OptResult::OPT_OPTIMAL, value);
+      }
+      else
+      {
+        lowerBound = pivot;
+      }
+    }
+    else
+    {
+      return std::make_pair(OptResult::OPT_UNKNOWN, value);
+    }
+    optChecker->pop();
+  }
+  return std::make_pair(OptResult::OPT_OPTIMAL, value);
+}
+
+std::pair<OptResult, Node> OMTOptimizerBitVector::maximize(
+    SmtEngine* parentSMTSolver, Node target)
+{
+  // the smt engine to which we send intermediate queries
+  // for the binary search.
+  std::unique_ptr<SmtEngine> optChecker =
+      OMTOptimizer::createOptCheckerWithTimeout(parentSMTSolver, false);
+  NodeManager* nm = optChecker->getNodeManager();
+  Result intermediateSatResult = optChecker->checkSat();
+  // Model-value of objective (used in optimization loop)
+  Node value;
+  if (intermediateSatResult.isUnknown())
+  {
+    return std::make_pair(OptResult::OPT_UNKNOWN, value);
+  }
+  if (intermediateSatResult.isSat() == Result::UNSAT)
+  {
+    return std::make_pair(OptResult::OPT_UNSAT, value);
+  }
+
+  // value equals to upperBound
+  value = optChecker->getValue(target);
+
+  // this gets the bitvector!
+  BitVector bvValue = value.getConst<BitVector>();
+  unsigned int bvSize = bvValue.getSize();
+
+  // lowerbound must be a satisfying value
+  // and value == lowerbound
+  BitVector lowerBound = bvValue;
+
+  // upperbound
+  BitVector upperBound = ((this->d_isSigned) ? (BitVector::mkMaxSigned(bvSize))
+                                             : (BitVector::mkOnes(bvSize)));
+
+  Kind LEOperator =
+      ((d_isSigned) ? (kind::BITVECTOR_SLE) : (kind::BITVECTOR_ULE));
+  Kind GTOperator =
+      ((d_isSigned) ? (kind::BITVECTOR_SGT) : (kind::BITVECTOR_UGT));
+
+  // the pivot value for binary search,
+  // pivot = (lowerBound + upperBound) / 2
+  // rounded towards -infinity
+  BitVector pivot;
+  while (true)
+  {
+    if (d_isSigned)
+    {
+      if (!lowerBound.signedLessThan(upperBound)) break;
+    }
+    else
+    {
+      if (!lowerBound.unsignedLessThan(upperBound)) break;
+    }
+    pivot = computeAverage(lowerBound, upperBound, d_isSigned);
+
+    optChecker->push();
+    // pivot < target <= upperBound
+    optChecker->assertFormula(
+        nm->mkNode(kind::AND,
+                   nm->mkNode(GTOperator, target, nm->mkConst(pivot)),
+                   nm->mkNode(LEOperator, target, nm->mkConst(upperBound))));
+    intermediateSatResult = optChecker->checkSat();
+    if (intermediateSatResult.isUnknown() || intermediateSatResult.isNull())
+    {
+      return std::make_pair(OptResult::OPT_UNKNOWN, value);
+    }
+    if (intermediateSatResult.isSat() == Result::SAT)
+    {
+      value = optChecker->getValue(target);
+      lowerBound = value.getConst<BitVector>();
+    }
+    else if (intermediateSatResult.isSat() == Result::UNSAT)
+    {
+      if (lowerBound == pivot)
+      {
+        // upperbound = lowerbound + 1
+        // and lowerbound < target <= upperbound is UNSAT
+        // return the lowerbound
+        return std::make_pair(OptResult::OPT_OPTIMAL, value);
+      }
+      else
+      {
+        upperBound = pivot;
+      }
+    }
+    else
+    {
+      return std::make_pair(OptResult::OPT_UNKNOWN, value);
+    }
+    optChecker->pop();
+  }
+  return std::make_pair(OptResult::OPT_OPTIMAL, value);
+}
+
+}  // namespace cvc5::omt
diff --git a/src/omt/bitvector_optimizer.h b/src/omt/bitvector_optimizer.h
new file mode 100644
index 000000000..9cafea38b
--- /dev/null
+++ b/src/omt/bitvector_optimizer.h
@@ -0,0 +1,50 @@
+/*********************                                                        */
+/*! \file bitvector_optimizer.h
+ ** \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 Optimizer for BitVector type
+ **/
+
+#ifndef CVC4__OMT__BITVECTOR_OPTIMIZER_H
+#define CVC4__OMT__BITVECTOR_OPTIMIZER_H
+
+#include "omt/omt_optimizer.h"
+
+namespace cvc5::omt {
+
+/**
+ * Optimizer for BitVector type
+ */
+class OMTOptimizerBitVector : public OMTOptimizer
+{
+ public:
+  OMTOptimizerBitVector(bool isSigned);
+  virtual ~OMTOptimizerBitVector() = default;
+  std::pair<smt::OptResult, Node> minimize(SmtEngine* parentSMTSolver,
+                                           Node target) override;
+  std::pair<smt::OptResult, Node> maximize(SmtEngine* parentSMTSolver,
+                                           Node target) override;
+
+ private:
+  /**
+   * Computes the BitVector version of (a + b) / 2 without overflow,
+   * rounding towards -infinity: -1.5 --> -2 and 1.5 --> 1
+   * same as the rounding scheme for int32_t
+   **/
+  BitVector computeAverage(const BitVector& a,
+                           const BitVector& b,
+                           bool isSigned);
+  /** Is the BitVector doing signed comparison? **/
+  bool d_isSigned;
+};
+
+}  // namespace cvc5::omt
+
+#endif /* CVC4__OMT__BITVECTOR_OPTIMIZER_H */
diff --git a/src/omt/integer_optimizer.cpp b/src/omt/integer_optimizer.cpp
new file mode 100644
index 000000000..f9509b47d
--- /dev/null
+++ b/src/omt/integer_optimizer.cpp
@@ -0,0 +1,87 @@
+/*********************                                                        */
+/*! \file integer_optimizer.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 Optimizer for Integer type
+ **/
+
+#include "omt/integer_optimizer.h"
+
+#include "options/smt_options.h"
+#include "smt/smt_engine.h"
+
+using namespace cvc5::smt;
+namespace cvc5::omt {
+
+std::pair<OptResult, Node> OMTOptimizerInteger::optimize(
+    SmtEngine* parentSMTSolver, Node target, ObjectiveType objType)
+{
+  // linear search for integer goal
+  // the smt engine to which we send intermediate queries
+  // for the linear search.
+  std::unique_ptr<SmtEngine> optChecker =
+      OMTOptimizer::createOptCheckerWithTimeout(parentSMTSolver, false);
+  NodeManager* nm = optChecker->getNodeManager();
+
+  Result intermediateSatResult = optChecker->checkSat();
+  // Model-value of objective (used in optimization loop)
+  Node value;
+  if (intermediateSatResult.isUnknown())
+  {
+    return std::make_pair(OptResult::OPT_UNKNOWN, value);
+  }
+  if (intermediateSatResult.isSat() == Result::UNSAT)
+  {
+    return std::make_pair(OptResult::OPT_UNSAT, value);
+  }
+  // asserts objective > old_value (used in optimization loop)
+  Node increment;
+  Kind incrementalOperator = kind::NULL_EXPR;
+  if (objType == ObjectiveType::OBJECTIVE_MINIMIZE)
+  {
+    // if objective is MIN, then assert optimization_target <
+    // current_model_value
+    incrementalOperator = kind::LT;
+  }
+  else if (objType == ObjectiveType::OBJECTIVE_MAXIMIZE)
+  {
+    // if objective is MAX, then assert optimization_target >
+    // current_model_value
+    incrementalOperator = kind::GT;
+  }
+  // Workhorse of linear search:
+  // This loop will keep incrmenting/decrementing the objective until unsat
+  // When unsat is hit,
+  // the optimized value is the model value just before the unsat call
+  while (intermediateSatResult.isSat() == Result::SAT)
+  {
+    value = optChecker->getValue(target);
+    Assert(!value.isNull());
+    increment = nm->mkNode(incrementalOperator, target, value);
+    optChecker->assertFormula(increment);
+    intermediateSatResult = optChecker->checkSat();
+  }
+  return std::make_pair(OptResult::OPT_OPTIMAL, value);
+}
+
+std::pair<OptResult, Node> OMTOptimizerInteger::minimize(
+    SmtEngine* parentSMTSolver, Node target)
+{
+  return this->optimize(
+      parentSMTSolver, target, ObjectiveType::OBJECTIVE_MINIMIZE);
+}
+std::pair<OptResult, Node> OMTOptimizerInteger::maximize(
+    SmtEngine* parentSMTSolver, Node target)
+{
+  return this->optimize(
+      parentSMTSolver, target, ObjectiveType::OBJECTIVE_MAXIMIZE);
+}
+
+}  // namespace cvc5::omt
diff --git a/src/omt/integer_optimizer.h b/src/omt/integer_optimizer.h
new file mode 100644
index 000000000..398aed616
--- /dev/null
+++ b/src/omt/integer_optimizer.h
@@ -0,0 +1,47 @@
+/*********************                                                        */
+/*! \file integer_optimizer.h
+ ** \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 Optimizer for Integer type
+ **/
+
+#ifndef CVC4__OMT__INTEGER_OPTIMIZER_H
+#define CVC4__OMT__INTEGER_OPTIMIZER_H
+
+#include "omt/omt_optimizer.h"
+
+namespace cvc5::omt {
+
+/**
+ * Optimizer for Integer type
+ */
+class OMTOptimizerInteger : public OMTOptimizer
+{
+ public:
+  OMTOptimizerInteger() = default;
+  virtual ~OMTOptimizerInteger() = default;
+  std::pair<smt::OptResult, Node> minimize(SmtEngine* parentSMTSolver,
+                                           Node target) override;
+  std::pair<smt::OptResult, Node> maximize(SmtEngine* parentSMTSolver,
+                                           Node target) override;
+
+ private:
+  /**
+   * Handles the optimization query specified by objType
+   * (objType = OBJECTIVE_MINIMIZE / OBJECTIVE_MAXIMIZE)
+   **/
+  std::pair<smt::OptResult, Node> optimize(SmtEngine* parentSMTSolver,
+                                           Node target,
+                                           smt::ObjectiveType objType);
+};
+
+}  // namespace cvc5::omt
+
+#endif /* CVC4__OMT__INTEGER_OPTIMIZER_H */
diff --git a/src/omt/omt_optimizer.cpp b/src/omt/omt_optimizer.cpp
new file mode 100644
index 000000000..4f64026e2
--- /dev/null
+++ b/src/omt/omt_optimizer.cpp
@@ -0,0 +1,69 @@
+/*********************                                                        */
+/*! \file omt_optimizer.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 The base class for optimizers of individual CVC4 type
+ **/
+
+#include "omt/omt_optimizer.h"
+
+#include "omt/bitvector_optimizer.h"
+#include "omt/integer_optimizer.h"
+#include "options/smt_options.h"
+#include "smt/smt_engine.h"
+#include "theory/quantifiers/quantifiers_attributes.h"
+#include "theory/smt_engine_subsolver.h"
+
+using namespace cvc5::theory;
+using namespace cvc5::smt;
+namespace cvc5::omt {
+
+std::unique_ptr<OMTOptimizer> OMTOptimizer::getOptimizerForNode(Node targetNode,
+                                                                bool isSigned)
+{
+  // the datatype of the target node
+  TypeNode objectiveType = targetNode.getType(true);
+  if (objectiveType.isInteger())
+  {
+    // integer type: use OMTOptimizerInteger
+    return std::unique_ptr<OMTOptimizer>(new OMTOptimizerInteger());
+  }
+  else if (objectiveType.isBitVector())
+  {
+    // bitvector type: use OMTOptimizerBitVector
+    return std::unique_ptr<OMTOptimizer>(new OMTOptimizerBitVector(isSigned));
+  }
+  else
+  {
+    return nullptr;
+  }
+}
+
+std::unique_ptr<SmtEngine> OMTOptimizer::createOptCheckerWithTimeout(
+    SmtEngine* parentSMTSolver, bool needsTimeout, unsigned long timeout)
+{
+  std::unique_ptr<SmtEngine> optChecker;
+  // initializeSubSolver will copy the options and theories enabled
+  // from the current solver to optChecker and adds timeout
+  theory::initializeSubsolver(optChecker, needsTimeout, timeout);
+  // we need to be in incremental mode for multiple objectives since we need to
+  // push pop we need to produce models to inrement on our objective
+  optChecker->setOption("incremental", "true");
+  optChecker->setOption("produce-models", "true");
+  // Move assertions from the parent solver to the subsolver
+  std::vector<Node> p_assertions = parentSMTSolver->getExpandedAssertions();
+  for (const Node& e : p_assertions)
+  {
+    optChecker->assertFormula(e);
+  }
+  return optChecker;
+}
+
+}  // namespace cvc5::omt
diff --git a/src/omt/omt_optimizer.h b/src/omt/omt_optimizer.h
new file mode 100644
index 000000000..da84556da
--- /dev/null
+++ b/src/omt/omt_optimizer.h
@@ -0,0 +1,84 @@
+/*********************                                                        */
+/*! \file omt_optimizer.h
+ ** \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 The base class for optimizers of individual CVC4 type
+ **/
+
+#ifndef CVC4__OMT__OMT_OPTIMIZER_H
+#define CVC4__OMT__OMT_OPTIMIZER_H
+
+#include "smt/optimization_solver.h"
+
+namespace cvc5::omt {
+
+/**
+ * The base class for optimizers of individual CVC type
+ */
+class OMTOptimizer
+{
+ public:
+  virtual ~OMTOptimizer() = default;
+  /**
+   * Given a target node, retrieve an optimizer specific for the node's type
+   * the second field isSigned specifies whether we should use signed comparison
+   * for BitVectors and it's only valid when the type is BitVector
+   *
+   * @param targetNode the target node for the expression to be optimized
+   * @param isSigned speficies whether to use signed comparison for BitVectors
+   *   and it's only valid when the type of targetNode is BitVector
+   * @return a unique_pointer pointing to a derived class of OMTOptimizer
+   *   and this is the optimizer for targetNode
+   **/
+  static std::unique_ptr<OMTOptimizer> getOptimizerForNode(
+      Node targetNode, bool isSigned = false);
+
+  /**
+   * Initialize an SMT subsolver for offline optimization purpose
+   * @param parentSMTSolver the parental solver containing the assertions
+   * @param needsTimeout specifies whether it needs timeout for each single
+   *    query
+   * @param timeout the timeout value, given in milliseconds (ms)
+   * @return a unique_pointer of SMT subsolver
+   **/
+  static std::unique_ptr<SmtEngine> createOptCheckerWithTimeout(
+      SmtEngine* parentSMTSolver,
+      bool needsTimeout = false,
+      unsigned long timeout = 0);
+
+  /**
+   * Minimize the target node with constraints encoded in parentSMTSolver
+   *
+   * @param parentSMTSolver an SMT solver encoding the assertions as the
+   *   constraints
+   * @param target the target expression to optimize
+   * @return pair<OptResult, Node>: the result of optimization and the optimized
+   *   value, if OptResult is OPT_UNKNOWN, value returned could be empty node or
+   *   something suboptimal.
+   **/
+  virtual std::pair<smt::OptResult, Node> minimize(SmtEngine* parentSMTSolver,
+                                                   Node target) = 0;
+  /**
+   * Maximize the target node with constraints encoded in parentSMTSolver
+   *
+   * @param parentSMTSolver an SMT solver encoding the assertions as the
+   *   constraints
+   * @param target the target expression to optimize
+   * @return pair<OptResult, Node>: the result of optimization and the optimized
+   *   value, if OptResult is OPT_UNKNOWN, value returned could be empty node or
+   *   something suboptimal.
+   **/
+  virtual std::pair<smt::OptResult, Node> maximize(SmtEngine* parentSMTSolver,
+                                                   Node target) = 0;
+};
+
+}  // namespace cvc5::omt
+
+#endif /* CVC4__OMT__OMT_OPTIMIZER_H */
diff --git a/src/smt/optimization_solver.cpp b/src/smt/optimization_solver.cpp
index ae1ce7057..70fa0f28c 100644
--- a/src/smt/optimization_solver.cpp
+++ b/src/smt/optimization_solver.cpp
@@ -2,7 +2,7 @@
 /*! \file optimization_solver.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.
@@ -14,13 +14,10 @@
 
 #include "smt/optimization_solver.h"
 
-#include "options/smt_options.h"
-#include "smt/smt_engine.h"
-#include "theory/quantifiers/quantifiers_attributes.h"
-#include "theory/smt_engine_subsolver.h"
+#include "omt/omt_optimizer.h"
 
 using namespace cvc5::theory;
-
+using namespace cvc5::omt;
 namespace cvc5 {
 namespace smt {
 
@@ -33,7 +30,7 @@ namespace smt {
 
 OptimizationSolver::OptimizationSolver(SmtEngine* parent)
     : d_parent(parent),
-      d_activatedObjective(Node(), OBJECTIVE_UNDEFINED),
+      d_activatedObjective(Node(), ObjectiveType::OBJECTIVE_UNDEFINED),
       d_savedValue()
 {
 }
@@ -43,80 +40,35 @@ OptimizationSolver::~OptimizationSolver() {}
 OptResult OptimizationSolver::checkOpt()
 {
   // Make sure that the objective is not the default one
-  Assert(d_activatedObjective.getType() != OBJECTIVE_UNDEFINED);
+  Assert(d_activatedObjective.getType() != ObjectiveType::OBJECTIVE_UNDEFINED);
   Assert(!d_activatedObjective.getNode().isNull());
 
-  // the smt engine to which we send intermediate queries
-  // for the linear search.
-  std::unique_ptr<SmtEngine> optChecker;
-  initializeSubsolver(optChecker);
-  NodeManager* nm = optChecker->getNodeManager();
-
-  // we need to be in incremental mode for multiple objectives since we need to
-  // push pop we need to produce models to inrement on our objective
-  optChecker->setOption("incremental", "true");
-  optChecker->setOption("produce-models", "true");
-
-  // Move assertions from the parent solver to the subsolver
-  std::vector<Node> p_assertions = d_parent->getExpandedAssertions();
-  for (const Node& e : p_assertions)
-  {
-    optChecker->assertFormula(e);
-  }
+  std::unique_ptr<OMTOptimizer> optimizer = OMTOptimizer::getOptimizerForNode(
+      d_activatedObjective.getNode(), d_activatedObjective.getSigned());
 
-  // We need to checksat once before the optimization loop so we have a
-  // baseline value to increment
-  Result loop_r = optChecker->checkSat();
+  Assert(optimizer != nullptr);
 
-  if (loop_r.isUnknown())
+  std::pair<OptResult, Node> optResult;
+  if (d_activatedObjective.getType() == ObjectiveType::OBJECTIVE_MAXIMIZE)
   {
-    return OPT_UNKNOWN;
+    optResult = optimizer->maximize(this->d_parent,
+                                    this->d_activatedObjective.getNode());
   }
-  if (!loop_r.isSat())
+  else if (d_activatedObjective.getType() == ObjectiveType::OBJECTIVE_MINIMIZE)
   {
-    return OPT_UNSAT;
+    optResult = optimizer->minimize(this->d_parent,
+                                    this->d_activatedObjective.getNode());
   }
 
-  // Model-value of objective (used in optimization loop)
-  Node value;
-  // asserts objective > old_value (used in optimization loop)
-  Node increment;
-
-  // Workhorse of linear optimization:
-  // This loop will keep incrmenting the objective until unsat
-  // When unsat is hit, the optimized value is the model value just before the
-  // unsat call
-  while (loop_r.isSat())
-  {
-    // get the model-value of objective in last sat call
-    value = optChecker->getValue(d_activatedObjective.getNode());
-
-    // We need to save the value since we need the model value just before the
-    // unsat call
-    Assert(!value.isNull());
-    d_savedValue = value;
-
-    // increment on the model-value of objective:
-    // if we're maximizing increment = objective > old_objective value
-    // if we're minimizing increment = objective < old_objective value
-    if (d_activatedObjective.getType() == OBJECTIVE_MAXIMIZE)
-    {
-      increment = nm->mkNode(kind::GT, d_activatedObjective.getNode(), value);
-    }
-    else
-    {
-      increment = nm->mkNode(kind::LT, d_activatedObjective.getNode(), value);
-    }
-    optChecker->assertFormula(increment);
-    loop_r = optChecker->checkSat();
-  }
-
-  return OPT_OPTIMAL;
+  this->d_savedValue = optResult.second;
+  return optResult.first;
 }
 
-void OptimizationSolver::activateObj(const Node& obj, const int& type)
+void OptimizationSolver::activateObj(const Node& obj,
+                                     const ObjectiveType type,
+                                     bool bvSigned)
 {
-  d_activatedObjective = Objective(obj, (ObjectiveType)type);
+  d_activatedObjective = Objective(obj, type, bvSigned);
 }
 
 Node OptimizationSolver::objectiveGetValue()
@@ -125,7 +77,8 @@ Node OptimizationSolver::objectiveGetValue()
   return d_savedValue;
 }
 
-Objective::Objective(Node obj, ObjectiveType type) : d_type(type), d_node(obj)
+Objective::Objective(Node obj, ObjectiveType type, bool bvSigned)
+    : d_type(type), d_node(obj), d_bvSigned(bvSigned)
 {
 }
 
@@ -133,5 +86,7 @@ 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 b79a4a823..b7f264ef1 100644
--- a/src/smt/optimization_solver.h
+++ b/src/smt/optimization_solver.h
@@ -2,7 +2,7 @@
 /*! \file optimization_solver.h
  ** \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.
@@ -33,7 +33,7 @@ namespace smt {
  *
  * Represents whether an objective should be minimized or maximized
  */
-enum ObjectiveType
+enum class ObjectiveType
 {
   OBJECTIVE_MINIMIZE,
   OBJECTIVE_MAXIMIZE,
@@ -46,7 +46,7 @@ enum ObjectiveType
  * Represents the result of a checkopt query
  * (unimplemented) OPT_OPTIMAL: if value was found
  */
-enum OptResult
+enum class OptResult
 {
   // the original set of assertions has result UNKNOWN
   OPT_UNKNOWN,
@@ -55,6 +55,9 @@ enum OptResult
   // the optimization loop finished and optimal
   OPT_OPTIMAL,
 
+  // the goal is unbounded, so it would be -inf or +inf
+  OPT_UNBOUNDED,
+
   // The last value is here as a preparation for future work
   // in which pproximate optimizations will be supported.
 
@@ -62,16 +65,32 @@ enum OptResult
   OPT_SAT_APPROX
 };
 
+/**
+ * The optimization objective, which contains:
+ * - the optimization target node,
+ * - whether it's maximize/minimize
+ * - and whether it's signed for BitVectors
+ **/
 class Objective
 {
  public:
-  Objective(Node n, ObjectiveType type);
+  /**
+   * Constructor
+   * @param n 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(){};
 
   /** A getter for d_type **/
   ObjectiveType getType();
   /** A getter for d_node **/
   Node getNode();
+  /** A getter for d_bvSigned **/
+  bool getSigned();
 
  private:
   /** The type of objective this is, either OBJECTIVE_MAXIMIZE OR
@@ -80,38 +99,55 @@ class Objective
   /** The node associated to the term that was used to construct the objective.
    * **/
   Node d_node;
-  };
 
+  /** Specify whether to use signed or unsigned comparison
+   * for BitVectors (only for BitVectors), this variable is defaulted to false
+   * **/
+  bool d_bvSigned;
+};
+
+/**
+ * A solver for optimization queries.
+ *
+ * This class is responsible for responding to optmization queries. It
+ * spawns a subsolver SmtEngine that captures the parent assertions and
+ * implements a linear optimization loop. Supports activateObjective,
+ * checkOpt, and objectiveGetValue in that order.
+ */
+class OptimizationSolver
+{
+ public:
   /**
-   * A solver for optimization queries.
-   * 
-   * This class is responsible for responding to optmization queries. It
-   * spawns a subsolver SmtEngine that captures the parent assertions and 
-   * implements a linear optimization loop. Supports activateObjective, 
-   * checkOpt, and objectiveGetValue in that order.
-   */
-  class OptimizationSolver
-  {
-   public:
-    /** parent is the smt_solver that the user added their assertions to **/
-    OptimizationSolver(SmtEngine* parent);
-    ~OptimizationSolver();
-
-    /** Runs the optimization loop for the activated objective **/
-    OptResult checkOpt();
-    /** Activates an objective: will be optimized for **/
-    void activateObj(const Node& obj, const int& type);
-    /** Gets the value of the optimized objective after checkopt is called **/
-    Node objectiveGetValue();
-
-   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;
-  };
+   * Constructor
+   * @param parent the smt_solver that the user added their assertions to
+   **/
+  OptimizationSolver(SmtEngine* parent);
+  ~OptimizationSolver();
+
+  /** 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
+   * @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();
+
+ 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;
+};
 
 }  // namespace smt
 }  // namespace cvc5
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