Split lazy bit-vector solver from TheoryBV (#5009)

This commit separates the lazy bit-vector solver from TheoryBV, which is now a thin wrapper around a bit-vector solver d_internal . This will allow us to easily swap out the bit-vector solver in the future.

28 files changed, 1606 insertions, 1113 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index a0fd277f8..6cd2c24d1 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -406,6 +406,9 @@ libcvc4_add_sources(
   theory/bv/bv_inequality_graph.h
   theory/bv/bv_quick_check.cpp
   theory/bv/bv_quick_check.h
+  theory/bv/bv_solver.h
+  theory/bv/bv_solver_lazy.cpp
+  theory/bv/bv_solver_lazy.h
   theory/bv/bv_subtheory.h
   theory/bv/bv_subtheory_algebraic.cpp
   theory/bv/bv_subtheory_algebraic.h
diff --git a/src/theory/bv/bitblast/eager_bitblaster.cpp b/src/theory/bv/bitblast/eager_bitblaster.cpp
index 627a17bc5..6417740fd 100644
--- a/src/theory/bv/bitblast/eager_bitblaster.cpp
+++ b/src/theory/bv/bitblast/eager_bitblaster.cpp
@@ -14,14 +14,14 @@
  ** Bitblaster for the eager bv solver.
  **/
 
-#include "cvc4_private.h"
-
 #include "theory/bv/bitblast/eager_bitblaster.h"
 
+#include "cvc4_private.h"
 #include "options/bv_options.h"
 #include "prop/cnf_stream.h"
 #include "prop/sat_solver_factory.h"
 #include "smt/smt_statistics_registry.h"
+#include "theory/bv/bv_solver_lazy.h"
 #include "theory/bv/theory_bv.h"
 #include "theory/theory_model.h"
 
@@ -29,7 +29,7 @@ namespace CVC4 {
 namespace theory {
 namespace bv {
 
-EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv, context::Context* c)
+EagerBitblaster::EagerBitblaster(BVSolverLazy* theory_bv, context::Context* c)
     : TBitblaster<Node>(),
       d_context(c),
       d_satSolver(),
diff --git a/src/theory/bv/bitblast/eager_bitblaster.h b/src/theory/bv/bitblast/eager_bitblaster.h
index da9488d43..b57f1ee0b 100644
--- a/src/theory/bv/bitblast/eager_bitblaster.h
+++ b/src/theory/bv/bitblast/eager_bitblaster.h
@@ -31,12 +31,12 @@ namespace theory {
 namespace bv {
 
 class BitblastingRegistrar;
-class TheoryBV;
+class BVSolverLazy;
 
 class EagerBitblaster : public TBitblaster<Node>
 {
  public:
-  EagerBitblaster(TheoryBV* theory_bv, context::Context* context);
+  EagerBitblaster(BVSolverLazy* theory_bv, context::Context* context);
   ~EagerBitblaster();
 
   void addAtom(TNode atom);
@@ -61,7 +61,7 @@ class EagerBitblaster : public TBitblaster<Node>
   std::unique_ptr<prop::SatSolver> d_satSolver;
   std::unique_ptr<BitblastingRegistrar> d_bitblastingRegistrar;
 
-  TheoryBV* d_bv;
+  BVSolverLazy* d_bv;
   TNodeSet d_bbAtoms;
   TNodeSet d_variables;
 
diff --git a/src/theory/bv/bitblast/lazy_bitblaster.cpp b/src/theory/bv/bitblast/lazy_bitblaster.cpp
index 3109d6ed7..3e32b4cc3 100644
--- a/src/theory/bv/bitblast/lazy_bitblaster.cpp
+++ b/src/theory/bv/bitblast/lazy_bitblaster.cpp
@@ -14,16 +14,16 @@
  ** Bitblaster for the lazy bv solver.
  **/
 
-#include "cvc4_private.h"
-
 #include "theory/bv/bitblast/lazy_bitblaster.h"
 
+#include "cvc4_private.h"
 #include "options/bv_options.h"
 #include "prop/cnf_stream.h"
 #include "prop/sat_solver.h"
 #include "prop/sat_solver_factory.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/bv/abstraction.h"
+#include "theory/bv/bv_solver_lazy.h"
 #include "theory/bv/theory_bv.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/rewriter.h"
@@ -58,7 +58,7 @@ uint64_t numNodes(TNode node, utils::NodeSet& seen)
 }
 
 TLazyBitblaster::TLazyBitblaster(context::Context* c,
-                                 bv::TheoryBV* bv,
+                                 bv::BVSolverLazy* bv,
                                  const std::string name,
                                  bool emptyNotify)
     : TBitblaster<Node>(),
@@ -292,8 +292,12 @@ bool TLazyBitblaster::assertToSat(TNode lit, bool propagate) {
     markerLit = ~markerLit;
   }
 
-  Debug("bitvector-bb") << "TheoryBV::TLazyBitblaster::assertToSat asserting node: " << atom <<"\n";
-  Debug("bitvector-bb") << "TheoryBV::TLazyBitblaster::assertToSat with literal:   " << markerLit << "\n";
+  Debug("bitvector-bb")
+      << "BVSolverLazy::TLazyBitblaster::assertToSat asserting node: " << atom
+      << "\n";
+  Debug("bitvector-bb")
+      << "BVSolverLazy::TLazyBitblaster::assertToSat with literal:   "
+      << markerLit << "\n";
 
   prop::SatValue ret = d_satSolver->assertAssumption(markerLit, propagate);
 
@@ -410,9 +414,9 @@ void TLazyBitblaster::MinisatNotify::notify(prop::SatClause& clause) {
       lemmab << d_cnf->getNode(clause[i]);
     }
     Node lemma = lemmab;
-    d_bv->d_out->lemma(lemma);
+    d_bv->d_inferManager.lemma(lemma);
   } else {
-    d_bv->d_out->lemma(d_cnf->getNode(clause[0]));
+    d_bv->d_inferManager.lemma(d_cnf->getNode(clause[0]));
   }
 }
 
@@ -423,7 +427,7 @@ void TLazyBitblaster::MinisatNotify::spendResource(ResourceManager::Resource r)
 
 void TLazyBitblaster::MinisatNotify::safePoint(ResourceManager::Resource r)
 {
-  d_bv->d_out->safePoint(r);
+  d_bv->d_inferManager.safePoint(r);
 }
 
 EqualityStatus TLazyBitblaster::getEqualityStatus(TNode a, TNode b)
diff --git a/src/theory/bv/bitblast/lazy_bitblaster.h b/src/theory/bv/bitblast/lazy_bitblaster.h
index bc930aec4..e53f1697d 100644
--- a/src/theory/bv/bitblast/lazy_bitblaster.h
+++ b/src/theory/bv/bitblast/lazy_bitblaster.h
@@ -32,7 +32,7 @@ namespace CVC4 {
 namespace theory {
 namespace bv {
 
-class TheoryBV;
+class BVSolverLazy;
 
 class TLazyBitblaster : public TBitblaster<Node>
 {
@@ -45,7 +45,7 @@ class TLazyBitblaster : public TBitblaster<Node>
   bool hasBBAtom(TNode atom) const override;
 
   TLazyBitblaster(context::Context* c,
-                  TheoryBV* bv,
+                  BVSolverLazy* bv,
                   const std::string name = "",
                   bool emptyNotify = false);
   ~TLazyBitblaster();
@@ -108,11 +108,11 @@ class TLazyBitblaster : public TBitblaster<Node>
   class MinisatNotify : public prop::BVSatSolverNotify
   {
     prop::CnfStream* d_cnf;
-    TheoryBV* d_bv;
+    BVSolverLazy* d_bv;
     TLazyBitblaster* d_lazyBB;
 
    public:
-    MinisatNotify(prop::CnfStream* cnf, TheoryBV* bv, TLazyBitblaster* lbv)
+    MinisatNotify(prop::CnfStream* cnf, BVSolverLazy* bv, TLazyBitblaster* lbv)
         : d_cnf(cnf), d_bv(bv), d_lazyBB(lbv)
     {
     }
@@ -123,7 +123,7 @@ class TLazyBitblaster : public TBitblaster<Node>
     void safePoint(ResourceManager::Resource r) override;
   };
 
-  TheoryBV* d_bv;
+  BVSolverLazy* d_bv;
   context::Context* d_ctx;
 
   std::unique_ptr<prop::NullRegistrar> d_nullRegistrar;
diff --git a/src/theory/bv/bv_eager_solver.cpp b/src/theory/bv/bv_eager_solver.cpp
index d1490374d..fcb678987 100644
--- a/src/theory/bv/bv_eager_solver.cpp
+++ b/src/theory/bv/bv_eager_solver.cpp
@@ -26,7 +26,7 @@ namespace CVC4 {
 namespace theory {
 namespace bv {
 
-EagerBitblastSolver::EagerBitblastSolver(context::Context* c, TheoryBV* bv)
+EagerBitblastSolver::EagerBitblastSolver(context::Context* c, BVSolverLazy* bv)
     : d_assertionSet(c),
       d_assumptionSet(c),
       d_context(c),
diff --git a/src/theory/bv/bv_eager_solver.h b/src/theory/bv/bv_eager_solver.h
index e0b55c23b..eef824af4 100644
--- a/src/theory/bv/bv_eager_solver.h
+++ b/src/theory/bv/bv_eager_solver.h
@@ -23,7 +23,7 @@
 #include <vector>
 
 #include "expr/node.h"
-#include "theory/bv/theory_bv.h"
+#include "theory/bv/bv_solver_lazy.h"
 #include "theory/theory_model.h"
 
 namespace CVC4 {
@@ -38,7 +38,7 @@ class AigBitblaster;
  */
 class EagerBitblastSolver {
  public:
-  EagerBitblastSolver(context::Context* c, theory::bv::TheoryBV* bv);
+  EagerBitblastSolver(context::Context* c, theory::bv::BVSolverLazy* bv);
   ~EagerBitblastSolver();
   bool checkSat();
   void assertFormula(TNode formula);
@@ -58,7 +58,7 @@ class EagerBitblastSolver {
   std::unique_ptr<AigBitblaster> d_aigBitblaster;
   bool d_useAig;
 
-  TheoryBV* d_bv;
+  BVSolverLazy* d_bv;
 };  // class EagerBitblastSolver
 
 }  // namespace bv
diff --git a/src/theory/bv/bv_quick_check.cpp b/src/theory/bv/bv_quick_check.cpp
index ed445eb33..f8e30247f 100644
--- a/src/theory/bv/bv_quick_check.cpp
+++ b/src/theory/bv/bv_quick_check.cpp
@@ -18,6 +18,7 @@
 
 #include "smt/smt_statistics_registry.h"
 #include "theory/bv/bitblast/lazy_bitblaster.h"
+#include "theory/bv/bv_solver_lazy.h"
 #include "theory/bv/theory_bv_utils.h"
 
 using namespace CVC4::prop;
@@ -26,11 +27,12 @@ namespace CVC4 {
 namespace theory {
 namespace bv {
 
-BVQuickCheck::BVQuickCheck(const std::string& name, theory::bv::TheoryBV* bv)
-  : d_ctx()
-  , d_bitblaster(new TLazyBitblaster(&d_ctx, bv, name, true))
-  , d_conflict()
-  , d_inConflict(&d_ctx, false)
+BVQuickCheck::BVQuickCheck(const std::string& name,
+                           theory::bv::BVSolverLazy* bv)
+    : d_ctx(),
+      d_bitblaster(new TLazyBitblaster(&d_ctx, bv, name, true)),
+      d_conflict(),
+      d_inConflict(&d_ctx, false)
 {}
 
 
diff --git a/src/theory/bv/bv_quick_check.h b/src/theory/bv/bv_quick_check.h
index 03a62e41b..c1d9e333e 100644
--- a/src/theory/bv/bv_quick_check.h
+++ b/src/theory/bv/bv_quick_check.h
@@ -19,8 +19,8 @@
 #ifndef CVC4__BV_QUICK_CHECK_H
 #define CVC4__BV_QUICK_CHECK_H
 
-#include <vector>
 #include <unordered_set>
+#include <vector>
 
 #include "context/cdo.h"
 #include "expr/node.h"
@@ -36,43 +36,44 @@ class TheoryModel;
 namespace bv {
 
 class TLazyBitblaster;
-class TheoryBV;
+class BVSolverLazy;
 
-class BVQuickCheck {
+class BVQuickCheck
+{
   context::Context d_ctx;
   std::unique_ptr<TLazyBitblaster> d_bitblaster;
   Node d_conflict;
   context::CDO<bool> d_inConflict;
   void setConflict();
 
-public:
-  BVQuickCheck(const std::string& name, theory::bv::TheoryBV* bv);
+ public:
+  BVQuickCheck(const std::string& name, theory::bv::BVSolverLazy* bv);
   ~BVQuickCheck();
   bool inConflict();
   Node getConflict() { return d_conflict; }
-  /** 
+  /**
    * Checks the satisfiability for a given set of assumptions.
-   * 
+   *
    * @param assumptions literals assumed true
    * @param budget max number of conflicts
-   * 
-   * @return 
+   *
+   * @return
    */
   prop::SatValue checkSat(std::vector<Node>& assumptions, unsigned long budget);
-  /** 
+  /**
    * Checks the satisfiability of given assertions.
-   * 
+   *
    * @param budget max number of conflicts
-   * 
-   * @return 
+   *
+   * @return
    */
   prop::SatValue checkSat(unsigned long budget);
-  
-  /** 
+
+  /**
    * Convert to CNF and assert the given literal.
-   * 
+   *
    * @param assumption bv literal
-   * 
+   *
    * @return false if a conflict has been found via bcp.
    */
   bool addAssertion(TNode assumption);
@@ -80,36 +81,37 @@ public:
   void push();
   void pop();
   void popToZero();
-  /** 
+  /**
    * Deletes the SAT solver and CNF stream, but maintains the
-   * bit-blasting term cache. 
-   * 
+   * bit-blasting term cache.
+   *
    */
-  void clearSolver(); 
+  void clearSolver();
 
-  /** 
+  /**
    * Computes the size of the circuit required to bit-blast
-   * atom, by not recounting the nodes in seen. 
-   * 
-   * @param node 
-   * @param seen 
-   * 
-   * @return 
+   * atom, by not recounting the nodes in seen.
+   *
+   * @param node
+   * @param seen
+   *
+   * @return
    */
   uint64_t computeAtomWeight(TNode atom, NodeSet& seen);
   bool collectModelInfo(theory::TheoryModel* model, bool fullModel);
 
-  typedef std::unordered_set<TNode, TNodeHashFunction>::const_iterator vars_iterator;
-  vars_iterator beginVars(); 
-  vars_iterator endVars(); 
-
-  Node getVarValue(TNode var, bool fullModel); 
+  typedef std::unordered_set<TNode, TNodeHashFunction>::const_iterator
+      vars_iterator;
+  vars_iterator beginVars();
+  vars_iterator endVars();
 
+  Node getVarValue(TNode var, bool fullModel);
 };
 
-
-class QuickXPlain {
-  struct Statistics {
+class QuickXPlain
+{
+  struct Statistics
+  {
     TimerStat d_xplainTime;
     IntStat d_numSolved;
     IntStat d_numUnknown;
@@ -124,52 +126,59 @@ class QuickXPlain {
   unsigned long d_budget;
 
   // crazy heuristic variables
-  unsigned d_numCalled; // number of times called
-  double d_minRatioSum; // sum of minimization ratio for computing average min ratio  
-  unsigned d_numConflicts; // number of conflicts (including when minimization not applied)
+  unsigned d_numCalled;  // number of times called
+  double d_minRatioSum;  // sum of minimization ratio for computing average min
+                         // ratio
+  unsigned d_numConflicts;  // number of conflicts (including when minimization
+                            // not applied)
   // unsigned d_period; // after how many conflicts to try minimizing again
 
   // double d_thresh; // if minimization ratio is less, increase period
-  // double d_hardThresh; // decrease period if minimization ratio is greater than this
-  
-  
+  // double d_hardThresh; // decrease period if minimization ratio is greater
+  // than this
+
   Statistics d_statistics;
-  /** 
+  /**
    * Uses solve with assumptions unsat core feature to
    * further minimize a conflict. The minimized conflict
    * will be between low and the returned value in conflict.
-   * 
-   * @param low 
-   * @param high 
-   * @param conflict 
-   * 
-   * @return 
+   *
+   * @param low
+   * @param high
+   * @param conflict
+   *
+   * @return
    */
-  unsigned selectUnsatCore(unsigned low, unsigned high,
+  unsigned selectUnsatCore(unsigned low,
+                           unsigned high,
                            std::vector<TNode>& conflict);
-  /** 
+  /**
    * Internal conflict  minimization, attempts to minimize
    * literals in conflict between low and high and adds the
-   * result in new_conflict. 
-   * 
-   * @param low 
-   * @param high 
-   * @param conflict 
-   * @param new_conflict 
+   * result in new_conflict.
+   *
+   * @param low
+   * @param high
+   * @param conflict
+   * @param new_conflict
    */
-  void minimizeConflictInternal(unsigned low, unsigned high,
+  void minimizeConflictInternal(unsigned low,
+                                unsigned high,
                                 std::vector<TNode>& conflict,
                                 std::vector<TNode>& new_conflict);
 
   bool useHeuristic();
-public:
-  QuickXPlain(const std::string& name, BVQuickCheck* solver, unsigned long budged = 10000);
+
+ public:
+  QuickXPlain(const std::string& name,
+              BVQuickCheck* solver,
+              unsigned long budged = 10000);
   ~QuickXPlain();
-  Node minimizeConflict(TNode conflict); 
+  Node minimizeConflict(TNode conflict);
 };
 
-} /* bv namespace */
-} /* theory namespace */
-} /* CVC4 namespace */
+}  // namespace bv
+}  // namespace theory
+}  // namespace CVC4
 
 #endif /* CVC4__BV_QUICK_CHECK_H */
diff --git a/src/theory/bv/bv_solver.h b/src/theory/bv/bv_solver.h
new file mode 100644
index 000000000..fef95ceef
--- /dev/null
+++ b/src/theory/bv/bv_solver.h
@@ -0,0 +1,119 @@
+/*********************                                                        */
+/*! \file bv_solver.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Mathias Preiner
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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 Bit-vector solver interface.
+ **
+ ** Describes the interface for the internal bit-vector solver of TheoryBV.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__BV__BV_SOLVER_H
+#define CVC4__THEORY__BV__BV_SOLVER_H
+
+#include "theory/theory.h"
+
+namespace CVC4 {
+namespace theory {
+namespace bv {
+
+class BVSolver
+{
+ public:
+  BVSolver(TheoryState& state, TheoryInferenceManager& inferMgr)
+      : d_state(state), d_inferManager(inferMgr){};
+
+  virtual ~BVSolver(){};
+
+  /**
+   * Returns true if we need an equality engine. If so, we initialize the
+   * information regarding how it should be setup. For details, see the
+   * documentation in Theory::needsEqualityEngine.
+   */
+  virtual bool needsEqualityEngine(EeSetupInfo& esi) { return false; }
+
+  virtual void finishInit(){};
+
+  virtual void preRegisterTerm(TNode n) = 0;
+
+  /**
+   * Forwarded from TheoryBV::preCheck().
+   */
+  virtual bool preCheck(Theory::Effort level = Theory::Effort::EFFORT_FULL)
+  {
+    return false;
+  }
+  /**
+   * Forwarded from TheoryBV::postCheck().
+   */
+  virtual void postCheck(Theory::Effort level = Theory::Effort::EFFORT_FULL){};
+  /**
+   * Forwarded from TheoryBV:preNotifyFact().
+   */
+  virtual bool preNotifyFact(
+      TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal)
+  {
+    return false;
+  }
+  /**
+   * Forwarded from TheoryBV::notifyFact().
+   */
+  virtual void notifyFact(TNode atom, bool pol, TNode fact, bool isInternal) {}
+
+  virtual bool needsCheckLastEffort() = 0;
+
+  virtual void propagate(Theory::Effort e){};
+
+  virtual TrustNode explain(TNode n)
+  {
+    Unimplemented() << "BVSolver propagated a node but doesn't implement the "
+                       "BVSolver::explain() interface!";
+    return TrustNode::null();
+  };
+
+  /**
+   * This is temporary only and will be deprecated soon in favor of
+   * Theory::collectModelValues.
+   */
+  virtual bool collectModelInfo(TheoryModel* m) = 0;
+
+  virtual std::string identify() const = 0;
+
+  virtual Theory::PPAssertStatus ppAssert(
+      TNode in, SubstitutionMap& outSubstitutions) = 0;
+
+  virtual TrustNode ppRewrite(TNode t) { return TrustNode::null(); };
+
+  virtual void ppStaticLearn(TNode in, NodeBuilder<>& learned){};
+
+  virtual void presolve(){};
+
+  virtual void notifySharedTerm(TNode t) = 0;
+
+  virtual EqualityStatus getEqualityStatus(TNode a, TNode b)
+  {
+    return EqualityStatus::EQUALITY_UNKNOWN;
+  }
+
+  /** Called by abstraction preprocessing pass. */
+  virtual bool applyAbstraction(const std::vector<Node>& assertions,
+                                std::vector<Node>& new_assertions) = 0;
+
+ protected:
+  TheoryState& d_state;
+  TheoryInferenceManager& d_inferManager;
+};
+
+}  // namespace bv
+}  // namespace theory
+}  // namespace CVC4
+
+#endif /* CVC4__THEORY__BV__BV_SOLVER_H */
diff --git a/src/theory/bv/bv_solver_lazy.cpp b/src/theory/bv/bv_solver_lazy.cpp
new file mode 100644
index 000000000..ad673b402
--- /dev/null
+++ b/src/theory/bv/bv_solver_lazy.cpp
@@ -0,0 +1,835 @@
+/*********************                                                        */
+/*! \file theory_bv_lazy.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Liana Hadarean, Andrew Reynolds, Aina Niemetz
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "theory/bv/bv_solver_lazy.h"
+
+#include "expr/node_algorithm.h"
+#include "options/bv_options.h"
+#include "options/smt_options.h"
+#include "smt/smt_statistics_registry.h"
+#include "theory/bv/abstraction.h"
+#include "theory/bv/bv_eager_solver.h"
+#include "theory/bv/bv_subtheory_algebraic.h"
+#include "theory/bv/bv_subtheory_bitblast.h"
+#include "theory/bv/bv_subtheory_core.h"
+#include "theory/bv/bv_subtheory_inequality.h"
+#include "theory/bv/theory_bv_rewrite_rules_normalization.h"
+#include "theory/bv/theory_bv_rewrite_rules_simplification.h"
+#include "theory/bv/theory_bv_rewriter.h"
+#include "theory/bv/theory_bv_utils.h"
+#include "theory/theory_model.h"
+
+using namespace CVC4::theory::bv::utils;
+
+namespace CVC4 {
+namespace theory {
+namespace bv {
+
+BVSolverLazy::BVSolverLazy(TheoryBV& bv,
+                           context::Context* c,
+                           context::UserContext* u,
+                           ProofNodeManager* pnm,
+                           std::string name)
+    : BVSolver(bv.d_state, bv.d_inferMgr),
+      d_bv(bv),
+      d_context(c),
+      d_alreadyPropagatedSet(c),
+      d_sharedTermsSet(c),
+      d_subtheories(),
+      d_subtheoryMap(),
+      d_statistics(),
+      d_staticLearnCache(),
+      d_lemmasAdded(c, false),
+      d_conflict(c, false),
+      d_invalidateModelCache(c, true),
+      d_literalsToPropagate(c),
+      d_literalsToPropagateIndex(c, 0),
+      d_propagatedBy(c),
+      d_eagerSolver(),
+      d_abstractionModule(new AbstractionModule(getStatsPrefix(THEORY_BV))),
+      d_calledPreregister(false)
+{
+  if (options::bitblastMode() == options::BitblastMode::EAGER)
+  {
+    d_eagerSolver.reset(new EagerBitblastSolver(c, this));
+    return;
+  }
+
+  if (options::bitvectorEqualitySolver())
+  {
+    d_subtheories.emplace_back(new CoreSolver(c, this));
+    d_subtheoryMap[SUB_CORE] = d_subtheories.back().get();
+  }
+
+  if (options::bitvectorInequalitySolver())
+  {
+    d_subtheories.emplace_back(new InequalitySolver(c, u, this));
+    d_subtheoryMap[SUB_INEQUALITY] = d_subtheories.back().get();
+  }
+
+  if (options::bitvectorAlgebraicSolver())
+  {
+    d_subtheories.emplace_back(new AlgebraicSolver(c, this));
+    d_subtheoryMap[SUB_ALGEBRAIC] = d_subtheories.back().get();
+  }
+
+  BitblastSolver* bb_solver = new BitblastSolver(c, this);
+  if (options::bvAbstraction())
+  {
+    bb_solver->setAbstraction(d_abstractionModule.get());
+  }
+  d_subtheories.emplace_back(bb_solver);
+  d_subtheoryMap[SUB_BITBLAST] = bb_solver;
+}
+
+BVSolverLazy::~BVSolverLazy() {}
+
+bool BVSolverLazy::needsEqualityEngine(EeSetupInfo& esi)
+{
+  CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE];
+  if (core)
+  {
+    return core->needsEqualityEngine(esi);
+  }
+  // otherwise we don't use an equality engine
+  return false;
+}
+
+void BVSolverLazy::finishInit()
+{
+  CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE];
+  if (core)
+  {
+    // must finish initialization in the core solver
+    core->finishInit();
+  }
+}
+
+void BVSolverLazy::spendResource(ResourceManager::Resource r)
+{
+  d_inferManager.spendResource(r);
+}
+
+BVSolverLazy::Statistics::Statistics()
+    : d_avgConflictSize("theory::bv::lazy::AvgBVConflictSize"),
+      d_solveSubstitutions("theory::bv::lazy::NumSolveSubstitutions", 0),
+      d_solveTimer("theory::bv::lazy::solveTimer"),
+      d_numCallsToCheckFullEffort("theory::bv::lazy::NumFullCheckCalls", 0),
+      d_numCallsToCheckStandardEffort("theory::bv::lazy::NumStandardCheckCalls",
+                                      0),
+      d_weightComputationTimer("theory::bv::lazy::weightComputationTimer"),
+      d_numMultSlice("theory::bv::lazy::NumMultSliceApplied", 0)
+{
+  smtStatisticsRegistry()->registerStat(&d_avgConflictSize);
+  smtStatisticsRegistry()->registerStat(&d_solveSubstitutions);
+  smtStatisticsRegistry()->registerStat(&d_solveTimer);
+  smtStatisticsRegistry()->registerStat(&d_numCallsToCheckFullEffort);
+  smtStatisticsRegistry()->registerStat(&d_numCallsToCheckStandardEffort);
+  smtStatisticsRegistry()->registerStat(&d_weightComputationTimer);
+  smtStatisticsRegistry()->registerStat(&d_numMultSlice);
+}
+
+BVSolverLazy::Statistics::~Statistics()
+{
+  smtStatisticsRegistry()->unregisterStat(&d_avgConflictSize);
+  smtStatisticsRegistry()->unregisterStat(&d_solveSubstitutions);
+  smtStatisticsRegistry()->unregisterStat(&d_solveTimer);
+  smtStatisticsRegistry()->unregisterStat(&d_numCallsToCheckFullEffort);
+  smtStatisticsRegistry()->unregisterStat(&d_numCallsToCheckStandardEffort);
+  smtStatisticsRegistry()->unregisterStat(&d_weightComputationTimer);
+  smtStatisticsRegistry()->unregisterStat(&d_numMultSlice);
+}
+
+void BVSolverLazy::preRegisterTerm(TNode node)
+{
+  d_calledPreregister = true;
+  Debug("bitvector-preregister")
+      << "BVSolverLazy::preRegister(" << node << ")" << std::endl;
+
+  if (options::bitblastMode() == options::BitblastMode::EAGER)
+  {
+    // the aig bit-blaster option is set heuristically
+    // if bv abstraction is used
+    if (!d_eagerSolver->isInitialized())
+    {
+      d_eagerSolver->initialize();
+    }
+
+    if (node.getKind() == kind::BITVECTOR_EAGER_ATOM)
+    {
+      Node formula = node[0];
+      d_eagerSolver->assertFormula(formula);
+    }
+    return;
+  }
+
+  for (unsigned i = 0; i < d_subtheories.size(); ++i)
+  {
+    d_subtheories[i]->preRegister(node);
+  }
+
+  // AJR : equality solver currently registers all terms to ExtTheory, if we
+  // want a lazy reduction without the bv equality solver, need to call this
+  // d_bv.d_extTheory->registerTermRec( node );
+}
+
+void BVSolverLazy::sendConflict()
+{
+  Assert(d_conflict);
+  if (d_conflictNode.isNull())
+  {
+    return;
+  }
+  else
+  {
+    Debug("bitvector") << indent() << "BVSolverLazy::check(): conflict "
+                       << d_conflictNode << std::endl;
+    d_inferManager.conflict(d_conflictNode);
+    d_statistics.d_avgConflictSize.addEntry(d_conflictNode.getNumChildren());
+    d_conflictNode = Node::null();
+  }
+}
+
+void BVSolverLazy::checkForLemma(TNode fact)
+{
+  if (fact.getKind() == kind::EQUAL)
+  {
+    NodeManager* nm = NodeManager::currentNM();
+    if (fact[0].getKind() == kind::BITVECTOR_UREM_TOTAL)
+    {
+      TNode urem = fact[0];
+      TNode result = fact[1];
+      TNode divisor = urem[1];
+      Node result_ult_div = nm->mkNode(kind::BITVECTOR_ULT, result, divisor);
+      Node divisor_eq_0 =
+          nm->mkNode(kind::EQUAL, divisor, mkZero(getSize(divisor)));
+      Node split = nm->mkNode(
+          kind::OR, divisor_eq_0, nm->mkNode(kind::NOT, fact), result_ult_div);
+      lemma(split);
+    }
+    if (fact[1].getKind() == kind::BITVECTOR_UREM_TOTAL)
+    {
+      TNode urem = fact[1];
+      TNode result = fact[0];
+      TNode divisor = urem[1];
+      Node result_ult_div = nm->mkNode(kind::BITVECTOR_ULT, result, divisor);
+      Node divisor_eq_0 =
+          nm->mkNode(kind::EQUAL, divisor, mkZero(getSize(divisor)));
+      Node split = nm->mkNode(
+          kind::OR, divisor_eq_0, nm->mkNode(kind::NOT, fact), result_ult_div);
+      lemma(split);
+    }
+  }
+}
+
+bool BVSolverLazy::preCheck(Theory::Effort e)
+{
+  check(e);
+  return true;
+}
+
+void BVSolverLazy::check(Theory::Effort e)
+{
+  if (done() && e < Theory::EFFORT_FULL)
+  {
+    return;
+  }
+
+  // last call : do reductions on extended bitvector functions
+  if (e == Theory::EFFORT_LAST_CALL)
+  {
+    CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE];
+    if (core)
+    {
+      // check extended functions at last call effort
+      core->checkExtf(e);
+    }
+    return;
+  }
+
+  Debug("bitvector") << "BVSolverLazy::check(" << e << ")" << std::endl;
+  TimerStat::CodeTimer codeTimer(d_statistics.d_solveTimer);
+  // we may be getting new assertions so the model cache may not be sound
+  d_invalidateModelCache.set(true);
+  // if we are using the eager solver
+  if (options::bitblastMode() == options::BitblastMode::EAGER)
+  {
+    // this can only happen on an empty benchmark
+    if (!d_eagerSolver->isInitialized())
+    {
+      d_eagerSolver->initialize();
+    }
+    if (!Theory::fullEffort(e)) return;
+
+    std::vector<TNode> assertions;
+    while (!done())
+    {
+      TNode fact = get().d_assertion;
+      Assert(fact.getKind() == kind::BITVECTOR_EAGER_ATOM);
+      assertions.push_back(fact);
+      d_eagerSolver->assertFormula(fact[0]);
+    }
+
+    bool ok = d_eagerSolver->checkSat();
+    if (!ok)
+    {
+      if (assertions.size() == 1)
+      {
+        d_inferManager.conflict(assertions[0]);
+        return;
+      }
+      Node conflict = utils::mkAnd(assertions);
+      d_inferManager.conflict(conflict);
+      return;
+    }
+    return;
+  }
+
+  if (Theory::fullEffort(e))
+  {
+    ++(d_statistics.d_numCallsToCheckFullEffort);
+  }
+  else
+  {
+    ++(d_statistics.d_numCallsToCheckStandardEffort);
+  }
+  // if we are already in conflict just return the conflict
+  if (inConflict())
+  {
+    sendConflict();
+    return;
+  }
+
+  while (!done())
+  {
+    TNode fact = get().d_assertion;
+
+    checkForLemma(fact);
+
+    for (unsigned i = 0; i < d_subtheories.size(); ++i)
+    {
+      d_subtheories[i]->assertFact(fact);
+    }
+  }
+
+  bool ok = true;
+  bool complete = false;
+  for (unsigned i = 0; i < d_subtheories.size(); ++i)
+  {
+    Assert(!inConflict());
+    ok = d_subtheories[i]->check(e);
+    complete = d_subtheories[i]->isComplete();
+
+    if (!ok)
+    {
+      // if we are in a conflict no need to check with other theories
+      Assert(inConflict());
+      sendConflict();
+      return;
+    }
+    if (complete)
+    {
+      // if the last subtheory was complete we stop
+      break;
+    }
+  }
+
+  // check extended functions
+  if (Theory::fullEffort(e))
+  {
+    CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE];
+    if (core)
+    {
+      // check extended functions at full effort
+      core->checkExtf(e);
+    }
+  }
+}
+
+bool BVSolverLazy::needsCheckLastEffort()
+{
+  CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE];
+  if (core)
+  {
+    return core->needsCheckLastEffort();
+  }
+  return false;
+}
+
+bool BVSolverLazy::collectModelInfo(TheoryModel* m)
+{
+  Assert(!inConflict());
+  if (options::bitblastMode() == options::BitblastMode::EAGER)
+  {
+    if (!d_eagerSolver->collectModelInfo(m, true))
+    {
+      return false;
+    }
+  }
+  for (unsigned i = 0; i < d_subtheories.size(); ++i)
+  {
+    if (d_subtheories[i]->isComplete())
+    {
+      return d_subtheories[i]->collectModelInfo(m, true);
+    }
+  }
+  return true;
+}
+
+Node BVSolverLazy::getModelValue(TNode var)
+{
+  Assert(!inConflict());
+  for (unsigned i = 0; i < d_subtheories.size(); ++i)
+  {
+    if (d_subtheories[i]->isComplete())
+    {
+      return d_subtheories[i]->getModelValue(var);
+    }
+  }
+  Unreachable();
+}
+
+void BVSolverLazy::propagate(Theory::Effort e)
+{
+  Debug("bitvector") << indent() << "BVSolverLazy::propagate()" << std::endl;
+  if (options::bitblastMode() == options::BitblastMode::EAGER)
+  {
+    return;
+  }
+
+  if (inConflict())
+  {
+    return;
+  }
+
+  // go through stored propagations
+  bool ok = true;
+  for (; d_literalsToPropagateIndex < d_literalsToPropagate.size() && ok;
+       d_literalsToPropagateIndex = d_literalsToPropagateIndex + 1)
+  {
+    TNode literal = d_literalsToPropagate[d_literalsToPropagateIndex];
+    // temporary fix for incremental bit-blasting
+    if (d_state.isSatLiteral(literal))
+    {
+      Debug("bitvector::propagate")
+          << "BVSolverLazy:: propagating " << literal << "\n";
+      ok = d_inferManager.propagateLit(literal);
+    }
+  }
+
+  if (!ok)
+  {
+    Debug("bitvector::propagate")
+        << indent() << "BVSolverLazy::propagate(): conflict from theory engine"
+        << std::endl;
+    setConflict();
+  }
+}
+
+Theory::PPAssertStatus BVSolverLazy::ppAssert(TNode in,
+                                              SubstitutionMap& outSubstitutions)
+{
+  switch (in.getKind())
+  {
+    case kind::EQUAL:
+    {
+      if (in[0].isVar() && d_bv.isLegalElimination(in[0], in[1]))
+      {
+        ++(d_statistics.d_solveSubstitutions);
+        outSubstitutions.addSubstitution(in[0], in[1]);
+        return Theory::PP_ASSERT_STATUS_SOLVED;
+      }
+      if (in[1].isVar() && d_bv.isLegalElimination(in[1], in[0]))
+      {
+        ++(d_statistics.d_solveSubstitutions);
+        outSubstitutions.addSubstitution(in[1], in[0]);
+        return Theory::PP_ASSERT_STATUS_SOLVED;
+      }
+      Node node = Rewriter::rewrite(in);
+      if ((node[0].getKind() == kind::BITVECTOR_EXTRACT && node[1].isConst())
+          || (node[1].getKind() == kind::BITVECTOR_EXTRACT
+              && node[0].isConst()))
+      {
+        Node extract = node[0].isConst() ? node[1] : node[0];
+        if (extract[0].isVar())
+        {
+          Node c = node[0].isConst() ? node[0] : node[1];
+
+          unsigned high = utils::getExtractHigh(extract);
+          unsigned low = utils::getExtractLow(extract);
+          unsigned var_bitwidth = utils::getSize(extract[0]);
+          std::vector<Node> children;
+
+          if (low == 0)
+          {
+            Assert(high != var_bitwidth - 1);
+            unsigned skolem_size = var_bitwidth - high - 1;
+            Node skolem = utils::mkVar(skolem_size);
+            children.push_back(skolem);
+            children.push_back(c);
+          }
+          else if (high == var_bitwidth - 1)
+          {
+            unsigned skolem_size = low;
+            Node skolem = utils::mkVar(skolem_size);
+            children.push_back(c);
+            children.push_back(skolem);
+          }
+          else
+          {
+            unsigned skolem1_size = low;
+            unsigned skolem2_size = var_bitwidth - high - 1;
+            Node skolem1 = utils::mkVar(skolem1_size);
+            Node skolem2 = utils::mkVar(skolem2_size);
+            children.push_back(skolem2);
+            children.push_back(c);
+            children.push_back(skolem1);
+          }
+          Node concat = utils::mkConcat(children);
+          Assert(utils::getSize(concat) == utils::getSize(extract[0]));
+          if (d_bv.isLegalElimination(extract[0], concat))
+          {
+            outSubstitutions.addSubstitution(extract[0], concat);
+            return Theory::PP_ASSERT_STATUS_SOLVED;
+          }
+        }
+      }
+    }
+    break;
+    case kind::BITVECTOR_ULT:
+    case kind::BITVECTOR_SLT:
+    case kind::BITVECTOR_ULE:
+    case kind::BITVECTOR_SLE:
+
+    default:
+      // TODO other predicates
+      break;
+  }
+  return Theory::PP_ASSERT_STATUS_UNSOLVED;
+}
+
+TrustNode BVSolverLazy::ppRewrite(TNode t)
+{
+  Debug("bv-pp-rewrite") << "BVSolverLazy::ppRewrite " << t << "\n";
+  Node res = t;
+  if (options::bitwiseEq() && RewriteRule<BitwiseEq>::applies(t))
+  {
+    Node result = RewriteRule<BitwiseEq>::run<false>(t);
+    res = Rewriter::rewrite(result);
+  }
+  else if (RewriteRule<UltPlusOne>::applies(t))
+  {
+    Node result = RewriteRule<UltPlusOne>::run<false>(t);
+    res = Rewriter::rewrite(result);
+  }
+  else if (res.getKind() == kind::EQUAL
+           && ((res[0].getKind() == kind::BITVECTOR_PLUS
+                && RewriteRule<ConcatToMult>::applies(res[1]))
+               || (res[1].getKind() == kind::BITVECTOR_PLUS
+                   && RewriteRule<ConcatToMult>::applies(res[0]))))
+  {
+    Node mult = RewriteRule<ConcatToMult>::applies(res[0])
+                    ? RewriteRule<ConcatToMult>::run<false>(res[0])
+                    : RewriteRule<ConcatToMult>::run<true>(res[1]);
+    Node factor = mult[0];
+    Node sum = RewriteRule<ConcatToMult>::applies(res[0]) ? res[1] : res[0];
+    Node new_eq = NodeManager::currentNM()->mkNode(kind::EQUAL, sum, mult);
+    Node rewr_eq = RewriteRule<SolveEq>::run<true>(new_eq);
+    if (rewr_eq[0].isVar() || rewr_eq[1].isVar())
+    {
+      res = Rewriter::rewrite(rewr_eq);
+    }
+    else
+    {
+      res = t;
+    }
+  }
+  else if (RewriteRule<SignExtendEqConst>::applies(t))
+  {
+    res = RewriteRule<SignExtendEqConst>::run<false>(t);
+  }
+  else if (RewriteRule<ZeroExtendEqConst>::applies(t))
+  {
+    res = RewriteRule<ZeroExtendEqConst>::run<false>(t);
+  }
+  else if (RewriteRule<NormalizeEqPlusNeg>::applies(t))
+  {
+    res = RewriteRule<NormalizeEqPlusNeg>::run<false>(t);
+  }
+
+  // if(t.getKind() == kind::EQUAL &&
+  //    ((t[0].getKind() == kind::BITVECTOR_MULT && t[1].getKind() ==
+  //    kind::BITVECTOR_PLUS) ||
+  //     (t[1].getKind() == kind::BITVECTOR_MULT && t[0].getKind() ==
+  //     kind::BITVECTOR_PLUS))) {
+  //   // if we have an equality between a multiplication and addition
+  //   // try to express multiplication in terms of addition
+  //   Node mult = t[0].getKind() == kind::BITVECTOR_MULT? t[0] : t[1];
+  //   Node add = t[0].getKind() == kind::BITVECTOR_PLUS? t[0] : t[1];
+  //   if (RewriteRule<MultSlice>::applies(mult)) {
+  //     Node new_mult = RewriteRule<MultSlice>::run<false>(mult);
+  //     Node new_eq =
+  //     Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::EQUAL,
+  //     new_mult, add));
+
+  //     // the simplification can cause the formula to blow up
+  //     // only apply if formula reduced
+  //     if (d_subtheoryMap.find(SUB_BITBLAST) != d_subtheoryMap.end()) {
+  //       BitblastSolver* bv = (BitblastSolver*)d_subtheoryMap[SUB_BITBLAST];
+  //       uint64_t old_size = bv->computeAtomWeight(t);
+  //       Assert (old_size);
+  //       uint64_t new_size = bv->computeAtomWeight(new_eq);
+  //       double ratio = ((double)new_size)/old_size;
+  //       if (ratio <= 0.4) {
+  //         ++(d_statistics.d_numMultSlice);
+  //         return new_eq;
+  //       }
+  //     }
+
+  //     if (new_eq.getKind() == kind::CONST_BOOLEAN) {
+  //       ++(d_statistics.d_numMultSlice);
+  //       return new_eq;
+  //     }
+  //   }
+  // }
+
+  if (options::bvAbstraction() && t.getType().isBoolean())
+  {
+    d_abstractionModule->addInputAtom(res);
+  }
+  Debug("bv-pp-rewrite") << "to   " << res << "\n";
+  if (res != t)
+  {
+    return TrustNode::mkTrustRewrite(t, res, nullptr);
+  }
+  return TrustNode::null();
+}
+
+void BVSolverLazy::presolve()
+{
+  Debug("bitvector") << "BVSolverLazy::presolve" << std::endl;
+}
+
+static int prop_count = 0;
+
+bool BVSolverLazy::storePropagation(TNode literal, SubTheory subtheory)
+{
+  Debug("bitvector::propagate") << indent() << d_context->getLevel() << " "
+                                << "BVSolverLazy::storePropagation(" << literal
+                                << ", " << subtheory << ")" << std::endl;
+  prop_count++;
+
+  // If already in conflict, no more propagation
+  if (d_conflict)
+  {
+    Debug("bitvector::propagate")
+        << indent() << "BVSolverLazy::storePropagation(" << literal << ", "
+        << subtheory << "): already in conflict" << std::endl;
+    return false;
+  }
+
+  // If propagated already, just skip
+  PropagatedMap::const_iterator find = d_propagatedBy.find(literal);
+  if (find != d_propagatedBy.end())
+  {
+    return true;
+  }
+  else
+  {
+    bool polarity = literal.getKind() != kind::NOT;
+    Node negatedLiteral = polarity ? literal.notNode() : (Node)literal[0];
+    find = d_propagatedBy.find(negatedLiteral);
+    if (find != d_propagatedBy.end() && (*find).second != subtheory)
+    {
+      // Safe to ignore this one, subtheory should produce a conflict
+      return true;
+    }
+
+    d_propagatedBy[literal] = subtheory;
+  }
+
+  // Propagate differs depending on the subtheory
+  // * bitblaster needs to be left alone until it's done, otherwise it doesn't
+  //   know how to explain
+  // * equality engine can propagate eagerly
+  // TODO(2348): Determine if ok should be set by propagate. If not, remove ok.
+  constexpr bool ok = true;
+  if (subtheory == SUB_CORE)
+  {
+    d_inferManager.propagateLit(literal);
+    if (!ok)
+    {
+      setConflict();
+    }
+  }
+  else
+  {
+    d_literalsToPropagate.push_back(literal);
+  }
+  return ok;
+
+} /* BVSolverLazy::propagate(TNode) */
+
+void BVSolverLazy::explain(TNode literal, std::vector<TNode>& assumptions)
+{
+  Assert(wasPropagatedBySubtheory(literal));
+  SubTheory sub = getPropagatingSubtheory(literal);
+  d_subtheoryMap[sub]->explain(literal, assumptions);
+}
+
+TrustNode BVSolverLazy::explain(TNode node)
+{
+  Debug("bitvector::explain")
+      << "BVSolverLazy::explain(" << node << ")" << std::endl;
+  std::vector<TNode> assumptions;
+
+  // Ask for the explanation
+  explain(node, assumptions);
+  // this means that it is something true at level 0
+  Node explanation;
+  if (assumptions.size() == 0)
+  {
+    explanation = utils::mkTrue();
+  }
+  else
+  {
+    // return the explanation
+    explanation = utils::mkAnd(assumptions);
+  }
+  Debug("bitvector::explain") << "BVSolverLazy::explain(" << node << ") => "
+                              << explanation << std::endl;
+  Debug("bitvector::explain") << "BVSolverLazy::explain done. \n";
+  return TrustNode::mkTrustPropExp(node, explanation, nullptr);
+}
+
+void BVSolverLazy::notifySharedTerm(TNode t)
+{
+  Debug("bitvector::sharing")
+      << indent() << "BVSolverLazy::notifySharedTerm(" << t << ")" << std::endl;
+  d_sharedTermsSet.insert(t);
+  if (options::bitvectorEqualitySolver())
+  {
+    for (unsigned i = 0; i < d_subtheories.size(); ++i)
+    {
+      d_subtheories[i]->addSharedTerm(t);
+    }
+  }
+}
+
+EqualityStatus BVSolverLazy::getEqualityStatus(TNode a, TNode b)
+{
+  if (options::bitblastMode() == options::BitblastMode::EAGER)
+    return EQUALITY_UNKNOWN;
+  Assert(options::bitblastMode() == options::BitblastMode::LAZY);
+  for (unsigned i = 0; i < d_subtheories.size(); ++i)
+  {
+    EqualityStatus status = d_subtheories[i]->getEqualityStatus(a, b);
+    if (status != EQUALITY_UNKNOWN)
+    {
+      return status;
+    }
+  }
+  return EQUALITY_UNKNOWN;
+  ;
+}
+
+void BVSolverLazy::ppStaticLearn(TNode in, NodeBuilder<>& learned)
+{
+  if (d_staticLearnCache.find(in) != d_staticLearnCache.end())
+  {
+    return;
+  }
+  d_staticLearnCache.insert(in);
+
+  if (in.getKind() == kind::EQUAL)
+  {
+    if ((in[0].getKind() == kind::BITVECTOR_PLUS
+         && in[1].getKind() == kind::BITVECTOR_SHL)
+        || (in[1].getKind() == kind::BITVECTOR_PLUS
+            && in[0].getKind() == kind::BITVECTOR_SHL))
+    {
+      TNode p = in[0].getKind() == kind::BITVECTOR_PLUS ? in[0] : in[1];
+      TNode s = in[0].getKind() == kind::BITVECTOR_PLUS ? in[1] : in[0];
+
+      if (p.getNumChildren() == 2 && p[0].getKind() == kind::BITVECTOR_SHL
+          && p[1].getKind() == kind::BITVECTOR_SHL)
+      {
+        unsigned size = utils::getSize(s);
+        Node one = utils::mkConst(size, 1u);
+        if (s[0] == one && p[0][0] == one && p[1][0] == one)
+        {
+          Node zero = utils::mkConst(size, 0u);
+          TNode b = p[0];
+          TNode c = p[1];
+          // (s : 1 << S) = (b : 1 << B) + (c : 1 << C)
+          Node b_eq_0 = b.eqNode(zero);
+          Node c_eq_0 = c.eqNode(zero);
+          Node b_eq_c = b.eqNode(c);
+
+          Node dis = NodeManager::currentNM()->mkNode(
+              kind::OR, b_eq_0, c_eq_0, b_eq_c);
+          Node imp = in.impNode(dis);
+          learned << imp;
+        }
+      }
+    }
+  }
+  else if (in.getKind() == kind::AND)
+  {
+    for (size_t i = 0, N = in.getNumChildren(); i < N; ++i)
+    {
+      ppStaticLearn(in[i], learned);
+    }
+  }
+}
+
+bool BVSolverLazy::applyAbstraction(const std::vector<Node>& assertions,
+                                    std::vector<Node>& new_assertions)
+{
+  bool changed =
+      d_abstractionModule->applyAbstraction(assertions, new_assertions);
+  if (changed && options::bitblastMode() == options::BitblastMode::EAGER
+      && options::bitvectorAig())
+  {
+    // disable AIG mode
+    AlwaysAssert(!d_eagerSolver->isInitialized());
+    d_eagerSolver->turnOffAig();
+    d_eagerSolver->initialize();
+  }
+  return changed;
+}
+
+void BVSolverLazy::setConflict(Node conflict)
+{
+  if (options::bvAbstraction())
+  {
+    NodeManager* const nm = NodeManager::currentNM();
+    Node new_conflict = d_abstractionModule->simplifyConflict(conflict);
+
+    std::vector<Node> lemmas;
+    lemmas.push_back(new_conflict);
+    d_abstractionModule->generalizeConflict(new_conflict, lemmas);
+    for (unsigned i = 0; i < lemmas.size(); ++i)
+    {
+      lemma(nm->mkNode(kind::NOT, lemmas[i]));
+    }
+  }
+  d_conflict = true;
+  d_conflictNode = conflict;
+}
+
+}  // namespace bv
+}  // namespace theory
+} /* namespace CVC4 */
diff --git a/src/theory/bv/bv_solver_lazy.h b/src/theory/bv/bv_solver_lazy.h
new file mode 100644
index 000000000..81f40340e
--- /dev/null
+++ b/src/theory/bv/bv_solver_lazy.h
@@ -0,0 +1,240 @@
+/*********************                                                        */
+/*! \file bv_solver_lazy.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Liana Hadarean, Andrew Reynolds, Tim King
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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 Lazy bit-vector solver.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__BV__BV_SOLVER_LAZY_H
+#define CVC4__THEORY__BV__BV_SOLVER_LAZY_H
+
+#include <unordered_map>
+#include <unordered_set>
+
+#include "context/cdhashset.h"
+#include "context/cdlist.h"
+#include "context/context.h"
+#include "theory/bv/bv_solver.h"
+#include "theory/bv/bv_subtheory.h"
+#include "theory/bv/theory_bv.h"
+#include "util/hash.h"
+
+namespace CVC4 {
+namespace theory {
+namespace bv {
+
+class CoreSolver;
+class InequalitySolver;
+class AlgebraicSolver;
+class BitblastSolver;
+class EagerBitblastSolver;
+class AbstractionModule;
+
+class BVSolverLazy : public BVSolver
+{
+  /** Back reference to TheoryBV */
+  TheoryBV& d_bv;
+
+  /** The context we are using */
+  context::Context* d_context;
+
+  /** Context dependent set of atoms we already propagated */
+  context::CDHashSet<Node, NodeHashFunction> d_alreadyPropagatedSet;
+  context::CDHashSet<Node, NodeHashFunction> d_sharedTermsSet;
+
+  std::vector<std::unique_ptr<SubtheorySolver>> d_subtheories;
+  std::unordered_map<SubTheory, SubtheorySolver*, std::hash<int>>
+      d_subtheoryMap;
+
+ public:
+  BVSolverLazy(TheoryBV& bv,
+               context::Context* c,
+               context::UserContext* u,
+               ProofNodeManager* pnm = nullptr,
+               std::string name = "");
+
+  ~BVSolverLazy();
+
+  //--------------------------------- initialization
+
+  /**
+   * Returns true if we need an equality engine. If so, we initialize the
+   * information regarding how it should be setup. For details, see the
+   * documentation in Theory::needsEqualityEngine.
+   */
+  bool needsEqualityEngine(EeSetupInfo& esi) override;
+
+  /** finish initialization */
+  void finishInit() override;
+  //--------------------------------- end initialization
+
+  void preRegisterTerm(TNode n) override;
+
+  bool preCheck(Theory::Effort e) override;
+
+  bool needsCheckLastEffort() override;
+
+  void propagate(Theory::Effort e) override;
+
+  TrustNode explain(TNode n) override;
+
+  bool collectModelInfo(TheoryModel* m) override;
+
+  std::string identify() const override { return std::string("BVSolverLazy"); }
+
+  Theory::PPAssertStatus ppAssert(TNode in,
+                                  SubstitutionMap& outSubstitutions) override;
+
+  TrustNode ppRewrite(TNode t) override;
+
+  void ppStaticLearn(TNode in, NodeBuilder<>& learned) override;
+
+  void presolve() override;
+
+  bool applyAbstraction(const std::vector<Node>& assertions,
+                        std::vector<Node>& new_assertions) override;
+
+  bool isLeaf(TNode node) { return d_bv.isLeaf(node); }
+
+ private:
+  class Statistics
+  {
+   public:
+    AverageStat d_avgConflictSize;
+    IntStat d_solveSubstitutions;
+    TimerStat d_solveTimer;
+    IntStat d_numCallsToCheckFullEffort;
+    IntStat d_numCallsToCheckStandardEffort;
+    TimerStat d_weightComputationTimer;
+    IntStat d_numMultSlice;
+    Statistics();
+    ~Statistics();
+  };
+
+  Statistics d_statistics;
+
+  void check(Theory::Effort e);
+  void spendResource(ResourceManager::Resource r);
+
+  typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
+  typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
+  NodeSet d_staticLearnCache;
+
+  typedef std::unordered_map<Node, Node, NodeHashFunction> NodeToNode;
+
+  context::CDO<bool> d_lemmasAdded;
+
+  // Are we in conflict?
+  context::CDO<bool> d_conflict;
+
+  // Invalidate the model cache if check was called
+  context::CDO<bool> d_invalidateModelCache;
+
+  /** The conflict node */
+  Node d_conflictNode;
+
+  /** Literals to propagate */
+  context::CDList<Node> d_literalsToPropagate;
+
+  /** Index of the next literal to propagate */
+  context::CDO<unsigned> d_literalsToPropagateIndex;
+
+  /**
+   * Keeps a map from nodes to the subtheory that propagated it so that we can
+   * explain it properly.
+   */
+  typedef context::CDHashMap<Node, SubTheory, NodeHashFunction> PropagatedMap;
+  PropagatedMap d_propagatedBy;
+
+  std::unique_ptr<EagerBitblastSolver> d_eagerSolver;
+  std::unique_ptr<AbstractionModule> d_abstractionModule;
+  bool d_calledPreregister;
+
+  bool wasPropagatedBySubtheory(TNode literal) const
+  {
+    return d_propagatedBy.find(literal) != d_propagatedBy.end();
+  }
+
+  SubTheory getPropagatingSubtheory(TNode literal) const
+  {
+    Assert(wasPropagatedBySubtheory(literal));
+    PropagatedMap::const_iterator find = d_propagatedBy.find(literal);
+    return (*find).second;
+  }
+
+  /** Should be called to propagate the literal.  */
+  bool storePropagation(TNode literal, SubTheory subtheory);
+
+  /**
+   * Explains why this literal (propagated by subtheory) is true by adding
+   * assumptions.
+   */
+  void explain(TNode literal, std::vector<TNode>& assumptions);
+
+  void notifySharedTerm(TNode t) override;
+
+  bool isSharedTerm(TNode t) { return d_sharedTermsSet.contains(t); }
+
+  EqualityStatus getEqualityStatus(TNode a, TNode b) override;
+
+  Node getModelValue(TNode var);
+
+  inline std::string indent()
+  {
+    std::string indentStr(d_context->getLevel(), ' ');
+    return indentStr;
+  }
+
+  void setConflict(Node conflict = Node::null());
+
+  bool inConflict() { return d_conflict; }
+
+  void sendConflict();
+
+  void lemma(TNode node)
+  {
+    d_inferManager.lemma(node);
+    d_lemmasAdded = true;
+  }
+
+  void checkForLemma(TNode node);
+
+  void computeAssertedTerms(std::set<Node>& termSet,
+                            const std::set<Kind>& irrKinds,
+                            bool includeShared) const
+  {
+    return d_bv.computeAssertedTerms(termSet, irrKinds, includeShared);
+  }
+
+  size_t numAssertions() { return d_bv.numAssertions(); }
+
+  theory::Assertion get() { return d_bv.get(); }
+
+  bool done() { return d_bv.done(); }
+
+  friend class LazyBitblaster;
+  friend class TLazyBitblaster;
+  friend class EagerBitblaster;
+  friend class BitblastSolver;
+  friend class EqualitySolver;
+  friend class CoreSolver;
+  friend class InequalitySolver;
+  friend class AlgebraicSolver;
+  friend class EagerBitblastSolver;
+}; /* class BVSolverLazy */
+
+}  // namespace bv
+}  // namespace theory
+
+}  // namespace CVC4
+
+#endif /* CVC4__THEORY__BV__BV_SOLVER_LAZY_H */
diff --git a/src/theory/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h
index f4b88b719..1244ae828 100644
--- a/src/theory/bv/bv_subtheory.h
+++ b/src/theory/bv/bv_subtheory.h
@@ -55,7 +55,7 @@ inline std::ostream& operator<<(std::ostream& out, SubTheory subtheory) {
 }
 
 // forward declaration
-class TheoryBV;
+class BVSolverLazy;
 
 using AssertionQueue = context::CDQueue<Node>;
 
@@ -65,11 +65,10 @@ using AssertionQueue = context::CDQueue<Node>;
  */
 class SubtheorySolver {
  public:
-  SubtheorySolver(context::Context* c, TheoryBV* bv)
-      : d_context(c),
-        d_bv(bv),
-        d_assertionQueue(c),
-        d_assertionIndex(c, 0) {}
+  SubtheorySolver(context::Context* c, BVSolverLazy* bv)
+      : d_context(c), d_bv(bv), d_assertionQueue(c), d_assertionIndex(c, 0)
+  {
+  }
   virtual ~SubtheorySolver() {}
   virtual bool check(Theory::Effort e) = 0;
   virtual void explain(TNode literal, std::vector<TNode>& assumptions) = 0;
@@ -101,7 +100,7 @@ class SubtheorySolver {
   context::Context* d_context;
 
   /** The bit-vector theory */
-  TheoryBV* d_bv;
+  BVSolverLazy* d_bv;
   AssertionQueue d_assertionQueue;
   context::CDO<uint32_t> d_assertionIndex;
 }; /* class SubtheorySolver */
diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp
index 80a6aeb86..49043b445 100644
--- a/src/theory/bv/bv_subtheory_algebraic.cpp
+++ b/src/theory/bv/bv_subtheory_algebraic.cpp
@@ -22,7 +22,7 @@
 #include "smt/smt_statistics_registry.h"
 #include "smt_util/boolean_simplification.h"
 #include "theory/bv/bv_quick_check.h"
-#include "theory/bv/theory_bv.h"
+#include "theory/bv/bv_solver_lazy.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/theory_model.h"
 
@@ -227,7 +227,7 @@ void SubstitutionEx::storeCache(TNode from, TNode to, Node reason) {
   d_cache[from] = SubstitutionElement(to, reason);
 }
 
-AlgebraicSolver::AlgebraicSolver(context::Context* c, TheoryBV* bv)
+AlgebraicSolver::AlgebraicSolver(context::Context* c, BVSolverLazy* bv)
     : SubtheorySolver(c, bv),
       d_modelMap(),
       d_quickSolver(new BVQuickCheck("theory::bv::algebraic", bv)),
@@ -345,7 +345,8 @@ bool AlgebraicSolver::check(Theory::Effort e)
       Debug("bv-subtheory-algebraic") << " UNSAT: assertion simplfies to false with conflict: "<< conflict << "\n";
 
       if (Dump.isOn("bv-algebraic")) {
-        Dump("bv-algebraic") << EchoCommand("TheoryBV::AlgebraicSolver::conflict");
+        Dump("bv-algebraic")
+            << EchoCommand("BVSolverLazy::AlgebraicSolver::conflict");
         Dump("bv-algebraic") << PushCommand();
         Dump("bv-algebraic") << AssertCommand(conflict.toExpr());
         Dump("bv-algebraic") << CheckSatCommand();
diff --git a/src/theory/bv/bv_subtheory_algebraic.h b/src/theory/bv/bv_subtheory_algebraic.h
index d9a9bce6f..a5d7b2db3 100644
--- a/src/theory/bv/bv_subtheory_algebraic.h
+++ b/src/theory/bv/bv_subtheory_algebraic.h
@@ -31,64 +31,60 @@ namespace bv {
 
 class AlgebraicSolver;
 
-
 Node mergeExplanations(TNode expl1, TNode expl2);
 Node mergeExplanations(const std::vector<Node>& expls);
 
-
 /**
  * Non-context dependent substitution with explanations.
- * 
+ *
  */
-class SubstitutionEx {
-  struct SubstitutionElement {
+class SubstitutionEx
+{
+  struct SubstitutionElement
+  {
     Node to;
     Node reason;
-    SubstitutionElement()
-      : to()
-      , reason()
-    {}
-    
-    SubstitutionElement(TNode t, TNode r)
-      : to(t)
-      , reason(r)
-    {}
+    SubstitutionElement() : to(), reason() {}
+
+    SubstitutionElement(TNode t, TNode r) : to(t), reason(r) {}
   };
 
-  struct SubstitutionStackElement {
+  struct SubstitutionStackElement
+  {
     TNode node;
     bool childrenAdded;
     SubstitutionStackElement(TNode n, bool ca = false)
-      : node(n)
-      , childrenAdded(ca)
-    {}
+        : node(n), childrenAdded(ca)
+    {
+    }
   };
 
-  typedef std::unordered_map<Node, SubstitutionElement, NodeHashFunction> Substitutions;
-  typedef std::unordered_map<Node, SubstitutionElement, NodeHashFunction> SubstitutionsCache;
+  typedef std::unordered_map<Node, SubstitutionElement, NodeHashFunction>
+      Substitutions;
+  typedef std::unordered_map<Node, SubstitutionElement, NodeHashFunction>
+      SubstitutionsCache;
 
   Substitutions d_substitutions;
   SubstitutionsCache d_cache;
   bool d_cacheInvalid;
-  theory::SubstitutionMap* d_modelMap; 
+  theory::SubstitutionMap* d_modelMap;
 
-  
   Node getReason(TNode node) const;
   bool hasCache(TNode node) const;
   Node getCache(TNode node) const;
   void storeCache(TNode from, TNode to, Node rason);
   Node internalApply(TNode node);
 
-public:
+ public:
   SubstitutionEx(theory::SubstitutionMap* modelMap);
-  /** 
-   * Returnst true if the substitution map did not contain from. 
-   * 
-   * @param from 
-   * @param to 
-   * @param reason 
-   * 
-   * @return 
+  /**
+   * Returnst true if the substitution map did not contain from.
+   *
+   * @param from
+   * @param to
+   * @param reason
+   *
+   * @return
    */
   bool addSubstitution(TNode from, TNode to, TNode reason);
   Node apply(TNode node);
@@ -97,37 +93,39 @@ public:
 
 /**
  * In-processing worklist element, id keeps track of
- * original assertion. 
- * 
+ * original assertion.
+ *
  */
-struct WorklistElement {
+struct WorklistElement
+{
   Node node;
   unsigned id;
   WorklistElement(Node n, unsigned i) : node(n), id(i) {}
   WorklistElement() : node(), id(-1) {}
-}; 
-
+};
 
 typedef std::unordered_map<Node, Node, NodeHashFunction> NodeNodeMap;
 typedef std::unordered_map<Node, unsigned, NodeHashFunction> NodeIdMap;
 typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
 
-
-class ExtractSkolemizer {
-  struct Extract {
+class ExtractSkolemizer
+{
+  struct Extract
+  {
     unsigned high;
     unsigned low;
     Extract(unsigned h, unsigned l) : high(h), low(l) {}
   };
-    
-  struct ExtractList {
+
+  struct ExtractList
+  {
     Base base;
     std::vector<Extract> extracts;
     ExtractList(unsigned bitwidth) : base(bitwidth), extracts() {}
     ExtractList() : base(1), extracts() {}
-    void addExtract(Extract& e); 
+    void addExtract(Extract& e);
   };
-  typedef   std::unordered_map<Node, ExtractList, NodeHashFunction> VarExtractMap;
+  typedef std::unordered_map<Node, ExtractList, NodeHashFunction> VarExtractMap;
   context::Context d_emptyContext;
   VarExtractMap d_varToExtract;
   theory::SubstitutionMap* d_modelMap;
@@ -141,12 +139,13 @@ class ExtractSkolemizer {
   Node unSkolemize(TNode);
 
   Node mkSkolem(Node node);
-public:
-  ExtractSkolemizer(theory::SubstitutionMap* modelMap); 
+
+ public:
+  ExtractSkolemizer(theory::SubstitutionMap* modelMap);
   void skolemize(std::vector<WorklistElement>&);
   void unSkolemize(std::vector<WorklistElement>&);
   ~ExtractSkolemizer();
-}; 
+};
 
 class BVQuickCheck;
 class QuickXPlain;
@@ -154,9 +153,10 @@ class QuickXPlain;
 /**
  * AlgebraicSolver
  */
-class AlgebraicSolver : public SubtheorySolver {
-  
-  struct Statistics {
+class AlgebraicSolver : public SubtheorySolver
+{
+  struct Statistics
+  {
     IntStat d_numCallstoCheck;
     IntStat d_numSimplifiesToTrue;
     IntStat d_numSimplifiesToFalse;
@@ -171,13 +171,17 @@ class AlgebraicSolver : public SubtheorySolver {
 
   std::unique_ptr<SubstitutionMap> d_modelMap;
   std::unique_ptr<BVQuickCheck> d_quickSolver;
-  context::CDO<bool> d_isComplete; 
-  context::CDO<bool> d_isDifficult; /**< flag to indicate whether the current assertions contain expensive BV operators */
-  
+  context::CDO<bool> d_isComplete;
+  context::CDO<bool>
+      d_isDifficult; /**< flag to indicate whether the current assertions
+                        contain expensive BV operators */
+
   unsigned long d_budget;
-  std::vector<Node> d_explanations; /**< explanations for assertions indexed by assertion id */
-  TNodeSet d_inputAssertions;   /**< assertions in current context (for debugging purposes only) */
-  NodeIdMap d_ids;              /**< map from assertions to ids */
+  std::vector<Node> d_explanations; /**< explanations for assertions indexed by
+                                       assertion id */
+  TNodeSet d_inputAssertions; /**< assertions in current context (for debugging
+                                 purposes only) */
+  NodeIdMap d_ids;            /**< map from assertions to ids */
   uint64_t d_numSolved;
   uint64_t d_numCalls;
 
@@ -191,37 +195,38 @@ class AlgebraicSolver : public SubtheorySolver {
   bool checkExplanation(TNode expl);
   void storeExplanation(TNode expl);
   void storeExplanation(unsigned id, TNode expl);
-  /** 
+  /**
    * Apply substitutions and rewriting to the worklist assertions to a fixpoint.
-   * Subsitutions learned store in subst. 
+   * Subsitutions learned store in subst.
    *
-   * @param worklist 
-   * @param subst 
+   * @param worklist
+   * @param subst
    */
-  void processAssertions(std::vector<WorklistElement>& worklist, SubstitutionEx& subst);
-  /** 
+  void processAssertions(std::vector<WorklistElement>& worklist,
+                         SubstitutionEx& subst);
+  /**
    * Attempt to solve the equation in fact, and if successful
-   * add a substitution to subst. 
-   * 
+   * add a substitution to subst.
+   *
    * @param fact equation we are trying to solve
    * @param reason the reason in terms of original assertions
    * @param subst substitution map
-   * 
+   *
    * @return true if added a substitution to subst
    */
   bool solve(TNode fact, TNode reason, SubstitutionEx& subst);
-  /** 
+  /**
    * Run a SAT solver on the given facts with the given budget.
-   * Sets the isComplete flag and conflict accordingly. 
-   * 
-   * @param facts 
-   * 
-   * @return true if no conflict was detected. 
+   * Sets the isComplete flag and conflict accordingly.
+   *
+   * @param facts
+   *
+   * @return true if no conflict was detected.
    */
   bool quickCheck(std::vector<Node>& facts);
 
-public:
-  AlgebraicSolver(context::Context* c, TheoryBV* bv);
+ public:
+  AlgebraicSolver(context::Context* c, BVSolverLazy* bv);
   ~AlgebraicSolver();
 
   void preRegister(TNode node) override {}
diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp
index 28c70a5b8..93ac87abe 100644
--- a/src/theory/bv/bv_subtheory_bitblast.cpp
+++ b/src/theory/bv/bv_subtheory_bitblast.cpp
@@ -15,6 +15,7 @@
  **/
 
 #include "theory/bv/bv_subtheory_bitblast.h"
+
 #include "decision/decision_attributes.h"
 #include "options/bv_options.h"
 #include "options/decision_options.h"
@@ -22,7 +23,7 @@
 #include "theory/bv/abstraction.h"
 #include "theory/bv/bitblast/lazy_bitblaster.h"
 #include "theory/bv/bv_quick_check.h"
-#include "theory/bv/theory_bv.h"
+#include "theory/bv/bv_solver_lazy.h"
 #include "theory/bv/theory_bv_utils.h"
 
 using namespace std;
@@ -32,7 +33,7 @@ namespace CVC4 {
 namespace theory {
 namespace bv {
 
-BitblastSolver::BitblastSolver(context::Context* c, TheoryBV* bv)
+BitblastSolver::BitblastSolver(context::Context* c, BVSolverLazy* bv)
     : SubtheorySolver(c, bv),
       d_bitblaster(new TLazyBitblaster(c, bv, "theory::bv::lazy")),
       d_bitblastQueue(c),
diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h
index 60ef08d93..0832b6772 100644
--- a/src/theory/bv/bv_subtheory_bitblast.h
+++ b/src/theory/bv/bv_subtheory_bitblast.h
@@ -35,8 +35,10 @@ class QuickXPlain;
 /**
  * BitblastSolver
  */
-class BitblastSolver : public SubtheorySolver {
-  struct Statistics {
+class BitblastSolver : public SubtheorySolver
+{
+  struct Statistics
+  {
     IntStat d_numCallstoCheck;
     IntStat d_numBBLemmas;
     Statistics();
@@ -55,14 +57,15 @@ class BitblastSolver : public SubtheorySolver {
 
   /** Queue for bit-blasting lemma atoms only in full check if we are sat */
   context::CDQueue<TNode> d_lemmaAtomsQueue;
-  bool  d_useSatPropagation;
+  bool d_useSatPropagation;
   AbstractionModule* d_abstractionModule;
   std::unique_ptr<BVQuickCheck> d_quickCheck;
   std::unique_ptr<QuickXPlain> d_quickXplain;
   //  Node getModelValueRec(TNode node);
   void setConflict(TNode conflict);
-public:
-  BitblastSolver(context::Context* c, TheoryBV* bv);
+
+ public:
+  BitblastSolver(context::Context* c, BVSolverLazy* bv);
   ~BitblastSolver();
 
   void preRegister(TNode node) override;
@@ -77,6 +80,6 @@ public:
   uint64_t computeAtomWeight(TNode atom);
 };
 
-} /* namespace CVC4::theory::bv */
-} /* namespace CVC4::theory */
+}  // namespace bv
+}  // namespace theory
 } /* namespace CVC4 */
diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index b341b0671..5bb6a45e4 100644
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -19,7 +19,7 @@
 #include "options/bv_options.h"
 #include "options/smt_options.h"
 #include "smt/smt_statistics_registry.h"
-#include "theory/bv/theory_bv.h"
+#include "theory/bv/bv_solver_lazy.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/ext_theory.h"
 #include "theory/theory_model.h"
@@ -89,7 +89,7 @@ bool CoreSolverExtTheoryCallback::getReduction(int effort,
   return false;
 }
 
-CoreSolver::CoreSolver(context::Context* c, TheoryBV* bv)
+CoreSolver::CoreSolver(context::Context* c, BVSolverLazy* bv)
     : SubtheorySolver(c, bv),
       d_notify(*this),
       d_isComplete(c, true),
@@ -99,13 +99,13 @@ CoreSolver::CoreSolver(context::Context* c, TheoryBV* bv)
       d_bv(bv),
       d_extTheoryCb(),
       d_extTheory(new ExtTheory(d_extTheoryCb,
-                                bv->getSatContext(),
-                                bv->getUserContext(),
-                                bv->getOutputChannel())),
+                                bv->d_bv.getSatContext(),
+                                bv->d_bv.getUserContext(),
+                                bv->d_bv.getOutputChannel())),
       d_reasons(c),
       d_needsLastCallCheck(false),
-      d_extf_range_infer(bv->getUserContext()),
-      d_extf_collapse_infer(bv->getUserContext())
+      d_extf_range_infer(bv->d_bv.getUserContext()),
+      d_extf_collapse_infer(bv->d_bv.getUserContext())
 {
   d_extTheory->addFunctionKind(kind::BITVECTOR_TO_NAT);
   d_extTheory->addFunctionKind(kind::INT_TO_BITVECTOR);
@@ -123,7 +123,7 @@ bool CoreSolver::needsEqualityEngine(EeSetupInfo& esi)
 void CoreSolver::finishInit()
 {
   // use the parent's equality engine, which may be the one we allocated above
-  d_equalityEngine = d_bv->getEqualityEngine();
+  d_equalityEngine = d_bv->d_bv.getEqualityEngine();
 
   // The kinds we are treating as function application in congruence
   d_equalityEngine->addFunctionKind(kind::BITVECTOR_CONCAT, true);
@@ -188,7 +188,8 @@ void CoreSolver::explain(TNode literal, std::vector<TNode>& assumptions) {
 bool CoreSolver::check(Theory::Effort e) {
   Trace("bitvector::core") << "CoreSolver::check \n";
 
-  d_bv->spendResource(ResourceManager::Resource::TheoryCheckStep);
+  d_bv->d_inferManager.spendResource(
+      ResourceManager::Resource::TheoryCheckStep);
 
   d_checkCalled = true;
   Assert(!d_bv->inConflict());
@@ -566,7 +567,7 @@ bool CoreSolver::doExtfInferences(std::vector<Node>& terms)
                               nm->mkNode(kind::LT, n, max));
         Trace("bv-extf-lemma")
             << "BV extf lemma (range) : " << lem << std::endl;
-        d_bv->getOutputChannel().lemma(lem);
+        d_bv->d_inferManager.lemma(lem);
         sentLemma = true;
       }
     }
@@ -615,7 +616,7 @@ bool CoreSolver::doExtfInferences(std::vector<Node>& terms)
           //   (bv2nat ((_ int2bv w) x)) == x + k*2^w for some k
           Trace("bv-extf-lemma")
               << "BV extf lemma (collapse) : " << lem << std::endl;
-          d_bv->getOutputChannel().lemma(lem);
+          d_bv->d_inferManager.lemma(lem);
           sentLemma = true;
         }
       }
diff --git a/src/theory/bv/bv_subtheory_core.h b/src/theory/bv/bv_subtheory_core.h
index 32bc36164..876daeabe 100644
--- a/src/theory/bv/bv_subtheory_core.h
+++ b/src/theory/bv/bv_subtheory_core.h
@@ -97,7 +97,7 @@ class CoreSolver : public SubtheorySolver {
   bool d_checkCalled;
 
   /** Pointer to the parent theory solver that owns this */
-  TheoryBV* d_bv;
+  BVSolverLazy* d_bv;
   /** Pointer to the equality engine of the parent */
   eq::EqualityEngine* d_equalityEngine;
   /** The extended theory callback */
@@ -146,7 +146,7 @@ class CoreSolver : public SubtheorySolver {
   bool doExtfReductions(std::vector<Node>& terms);
 
  public:
-  CoreSolver(context::Context* c, TheoryBV* bv);
+  CoreSolver(context::Context* c, BVSolverLazy* bv);
   ~CoreSolver();
   bool needsEqualityEngine(EeSetupInfo& esi);
   void finishInit();
diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp
index 1ff23c460..ffc354d8d 100644
--- a/src/theory/bv/bv_subtheory_inequality.cpp
+++ b/src/theory/bv/bv_subtheory_inequality.cpp
@@ -18,7 +18,7 @@
 
 #include "options/smt_options.h"
 #include "smt/smt_statistics_registry.h"
-#include "theory/bv/theory_bv.h"
+#include "theory/bv/bv_solver_lazy.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/theory_model.h"
 
diff --git a/src/theory/bv/bv_subtheory_inequality.h b/src/theory/bv/bv_subtheory_inequality.h
index abfb0d3cf..05c9c3d60 100644
--- a/src/theory/bv/bv_subtheory_inequality.h
+++ b/src/theory/bv/bv_subtheory_inequality.h
@@ -31,12 +31,17 @@ namespace theory {
 namespace bv {
 
 /** Cache for InequalitySolver::isInequalityOnly() */
-struct IneqOnlyAttributeId {};
+struct IneqOnlyAttributeId
+{
+};
 typedef expr::Attribute<IneqOnlyAttributeId, bool> IneqOnlyAttribute;
 
 /** Whether the above has been computed yet or not for an expr */
-struct IneqOnlyComputedAttributeId {};
-typedef expr::Attribute<IneqOnlyComputedAttributeId, bool> IneqOnlyComputedAttribute;
+struct IneqOnlyComputedAttributeId
+{
+};
+typedef expr::Attribute<IneqOnlyComputedAttributeId, bool>
+    IneqOnlyComputedAttribute;
 
 class InequalitySolver : public SubtheorySolver
 {
@@ -57,16 +62,18 @@ class InequalitySolver : public SubtheorySolver
   bool isInequalityOnly(TNode node);
   bool addInequality(TNode a, TNode b, bool strict, TNode fact);
   Statistics d_statistics;
-public:
-  InequalitySolver(context::Context* c, context::Context* u, TheoryBV* bv)
-    : SubtheorySolver(c, bv),
-      d_assertionSet(c),
-      d_inequalityGraph(c, u),
-      d_explanations(c),
-      d_isComplete(c, true),
-      d_ineqTerms(),
-      d_statistics()
-  {}
+
+ public:
+  InequalitySolver(context::Context* c, context::Context* u, BVSolverLazy* bv)
+      : SubtheorySolver(c, bv),
+        d_assertionSet(c),
+        d_inequalityGraph(c, u),
+        d_explanations(c),
+        d_isComplete(c, true),
+        d_ineqTerms(),
+        d_statistics()
+  {
+  }
 
   bool check(Theory::Effort e) override;
   void propagate(Theory::Effort e) override;
@@ -79,8 +86,8 @@ public:
   void preRegister(TNode node) override;
 };
 
-}
-}
-}
+}  // namespace bv
+}  // namespace theory
+}  // namespace CVC4
 
 #endif /* CVC4__THEORY__BV__BV_SUBTHEORY__INEQUALITY_H */
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 815656d8f..6f25d0843 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -15,26 +15,9 @@
 
 #include "theory/bv/theory_bv.h"
 
-#include "expr/node_algorithm.h"
 #include "options/bv_options.h"
-#include "options/smt_options.h"
-#include "smt/smt_statistics_registry.h"
-#include "theory/bv/abstraction.h"
-#include "theory/bv/bv_eager_solver.h"
-#include "theory/bv/bv_subtheory_algebraic.h"
-#include "theory/bv/bv_subtheory_bitblast.h"
-#include "theory/bv/bv_subtheory_core.h"
-#include "theory/bv/bv_subtheory_inequality.h"
-#include "theory/bv/theory_bv_rewrite_rules_normalization.h"
-#include "theory/bv/theory_bv_rewrite_rules_simplification.h"
-#include "theory/bv/theory_bv_rewriter.h"
+#include "theory/bv/bv_solver_lazy.h"
 #include "theory/bv/theory_bv_utils.h"
-#include "theory/theory_model.h"
-#include "theory/valuation.h"
-
-using namespace CVC4::context;
-using namespace CVC4::theory::bv::utils;
-using namespace std;
 
 namespace CVC4 {
 namespace theory {
@@ -48,60 +31,16 @@ TheoryBV::TheoryBV(context::Context* c,
                    ProofNodeManager* pnm,
                    std::string name)
     : Theory(THEORY_BV, c, u, out, valuation, logicInfo, pnm, name),
-      d_context(c),
-      d_alreadyPropagatedSet(c),
-      d_sharedTermsSet(c),
-      d_subtheories(),
-      d_subtheoryMap(),
-      d_statistics(),
-      d_staticLearnCache(),
-      d_BVDivByZero(),
-      d_BVRemByZero(),
-      d_lemmasAdded(c, false),
-      d_conflict(c, false),
-      d_invalidateModelCache(c, true),
-      d_literalsToPropagate(c),
-      d_literalsToPropagateIndex(c, 0),
-      d_propagatedBy(c),
-      d_eagerSolver(),
-      d_abstractionModule(new AbstractionModule(getStatsPrefix(THEORY_BV))),
-      d_calledPreregister(false),
-      d_state(c, u, valuation)
-{
-  if (options::bitblastMode() == options::BitblastMode::EAGER)
-  {
-    d_eagerSolver.reset(new EagerBitblastSolver(c, this));
-    return;
-  }
-
-  if (options::bitvectorEqualitySolver())
-  {
-    d_subtheories.emplace_back(new CoreSolver(c, this));
-    d_subtheoryMap[SUB_CORE] = d_subtheories.back().get();
-  }
-
-  if (options::bitvectorInequalitySolver())
-  {
-    d_subtheories.emplace_back(new InequalitySolver(c, u, this));
-    d_subtheoryMap[SUB_INEQUALITY] = d_subtheories.back().get();
-  }
-
-  if (options::bitvectorAlgebraicSolver())
-  {
-    d_subtheories.emplace_back(new AlgebraicSolver(c, this));
-    d_subtheoryMap[SUB_ALGEBRAIC] = d_subtheories.back().get();
-  }
-
-  BitblastSolver* bb_solver = new BitblastSolver(c, this);
-  if (options::bvAbstraction())
-  {
-    bb_solver->setAbstraction(d_abstractionModule.get());
-  }
-  d_subtheories.emplace_back(bb_solver);
-  d_subtheoryMap[SUB_BITBLAST] = bb_solver;
-
-  // indicate we are using the default theory state object
+      d_internal(nullptr),
+      d_ufDivByZero(),
+      d_ufRemByZero(),
+      d_rewriter(),
+      d_state(c, u, valuation),
+      d_inferMgr(*this, d_state, pnm)
+{
+  d_internal.reset(new BVSolverLazy(*this, c, u, pnm, name));
   d_theoryState = &d_state;
+  d_inferManager = &d_inferMgr;
 }
 
 TheoryBV::~TheoryBV() {}
@@ -110,87 +49,53 @@ TheoryRewriter* TheoryBV::getTheoryRewriter() { return &d_rewriter; }
 
 bool TheoryBV::needsEqualityEngine(EeSetupInfo& esi)
 {
-  CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE];
-  if (core)
-  {
-    return core->needsEqualityEngine(esi);
-  }
-  // otherwise we don't use an equality engine
-  return false;
+  return d_internal->needsEqualityEngine(esi);
 }
 
 void TheoryBV::finishInit()
 {
   // these kinds are semi-evaluated in getModelValue (applications of this
   // kind are treated as variables)
-  d_valuation.setSemiEvaluatedKind(kind::BITVECTOR_ACKERMANNIZE_UDIV);
-  d_valuation.setSemiEvaluatedKind(kind::BITVECTOR_ACKERMANNIZE_UREM);
-
-  CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE];
-  if (core)
-  {
-    // must finish initialization in the core solver
-    core->finishInit();
-  }
-}
-
-void TheoryBV::spendResource(ResourceManager::Resource r)
-{
-  getOutputChannel().spendResource(r);
+  getValuation().setSemiEvaluatedKind(kind::BITVECTOR_ACKERMANNIZE_UDIV);
+  getValuation().setSemiEvaluatedKind(kind::BITVECTOR_ACKERMANNIZE_UREM);
+  d_internal->finishInit();
 }
 
-TheoryBV::Statistics::Statistics():
-  d_avgConflictSize("theory::bv::AvgBVConflictSize"),
-  d_solveSubstitutions("theory::bv::NumSolveSubstitutions", 0),
-  d_solveTimer("theory::bv::solveTimer"),
-  d_numCallsToCheckFullEffort("theory::bv::NumFullCheckCalls", 0),
-  d_numCallsToCheckStandardEffort("theory::bv::NumStandardCheckCalls", 0),
-  d_weightComputationTimer("theory::bv::weightComputationTimer"),
-  d_numMultSlice("theory::bv::NumMultSliceApplied", 0)
+Node TheoryBV::getUFDivByZero(Kind k, unsigned width)
 {
-  smtStatisticsRegistry()->registerStat(&d_avgConflictSize);
-  smtStatisticsRegistry()->registerStat(&d_solveSubstitutions);
-  smtStatisticsRegistry()->registerStat(&d_solveTimer);
-  smtStatisticsRegistry()->registerStat(&d_numCallsToCheckFullEffort);
-  smtStatisticsRegistry()->registerStat(&d_numCallsToCheckStandardEffort);
-  smtStatisticsRegistry()->registerStat(&d_weightComputationTimer);
-  smtStatisticsRegistry()->registerStat(&d_numMultSlice);
-}
-
-TheoryBV::Statistics::~Statistics() {
-  smtStatisticsRegistry()->unregisterStat(&d_avgConflictSize);
-  smtStatisticsRegistry()->unregisterStat(&d_solveSubstitutions);
-  smtStatisticsRegistry()->unregisterStat(&d_solveTimer);
-  smtStatisticsRegistry()->unregisterStat(&d_numCallsToCheckFullEffort);
-  smtStatisticsRegistry()->unregisterStat(&d_numCallsToCheckStandardEffort);
-  smtStatisticsRegistry()->unregisterStat(&d_weightComputationTimer);
-  smtStatisticsRegistry()->unregisterStat(&d_numMultSlice);
-}
-
-Node TheoryBV::getBVDivByZero(Kind k, unsigned width) {
   NodeManager* nm = NodeManager::currentNM();
-  if (k == kind::BITVECTOR_UDIV) {
-    if (d_BVDivByZero.find(width) == d_BVDivByZero.end()) {
+  if (k == kind::BITVECTOR_UDIV)
+  {
+    if (d_ufDivByZero.find(width) == d_ufDivByZero.end())
+    {
       // lazily create the function symbols
-      ostringstream os;
+      std::ostringstream os;
       os << "BVUDivByZero_" << width;
-      Node divByZero = nm->mkSkolem(os.str(),
-                                    nm->mkFunctionType(nm->mkBitVectorType(width), nm->mkBitVectorType(width)),
-                                    "partial bvudiv", NodeManager::SKOLEM_EXACT_NAME);
-      d_BVDivByZero[width] = divByZero;
+      Node divByZero =
+          nm->mkSkolem(os.str(),
+                       nm->mkFunctionType(nm->mkBitVectorType(width),
+                                          nm->mkBitVectorType(width)),
+                       "partial bvudiv",
+                       NodeManager::SKOLEM_EXACT_NAME);
+      d_ufDivByZero[width] = divByZero;
     }
-    return d_BVDivByZero[width];
+    return d_ufDivByZero[width];
   }
-  else if (k == kind::BITVECTOR_UREM) {
-    if (d_BVRemByZero.find(width) == d_BVRemByZero.end()) {
-      ostringstream os;
+  else if (k == kind::BITVECTOR_UREM)
+  {
+    if (d_ufRemByZero.find(width) == d_ufRemByZero.end())
+    {
+      std::ostringstream os;
       os << "BVURemByZero_" << width;
-      Node divByZero = nm->mkSkolem(os.str(),
-                                    nm->mkFunctionType(nm->mkBitVectorType(width), nm->mkBitVectorType(width)),
-                                    "partial bvurem", NodeManager::SKOLEM_EXACT_NAME);
-      d_BVRemByZero[width] = divByZero;
+      Node divByZero =
+          nm->mkSkolem(os.str(),
+                       nm->mkFunctionType(nm->mkBitVectorType(width),
+                                          nm->mkBitVectorType(width)),
+                       "partial bvurem",
+                       NodeManager::SKOLEM_EXACT_NAME);
+      d_ufRemByZero[width] = divByZero;
     }
-    return d_BVRemByZero[width];
+    return d_ufRemByZero[width];
   }
 
   Unreachable();
@@ -198,42 +103,47 @@ Node TheoryBV::getBVDivByZero(Kind k, unsigned width) {
 
 TrustNode TheoryBV::expandDefinition(Node node)
 {
-  Debug("bitvector-expandDefinition") << "TheoryBV::expandDefinition(" << node << ")" << std::endl;
+  Debug("bitvector-expandDefinition")
+      << "TheoryBV::expandDefinition(" << node << ")" << std::endl;
 
   Node ret;
-  switch (node.getKind()) {
-  case kind::BITVECTOR_SDIV:
-  case kind::BITVECTOR_SREM:
-  case kind::BITVECTOR_SMOD:
-    ret = TheoryBVRewriter::eliminateBVSDiv(node);
-    break;
+  switch (node.getKind())
+  {
+    case kind::BITVECTOR_SDIV:
+    case kind::BITVECTOR_SREM:
+    case kind::BITVECTOR_SMOD:
+      ret = TheoryBVRewriter::eliminateBVSDiv(node);
+      break;
 
-  case kind::BITVECTOR_UDIV:
-  case kind::BITVECTOR_UREM: {
-    NodeManager* nm = NodeManager::currentNM();
-    unsigned width = node.getType().getBitVectorSize();
+    case kind::BITVECTOR_UDIV:
+    case kind::BITVECTOR_UREM:
+    {
+      NodeManager* nm = NodeManager::currentNM();
+      unsigned width = node.getType().getBitVectorSize();
 
-    if (options::bitvectorDivByZeroConst()) {
-      Kind kind = node.getKind() == kind::BITVECTOR_UDIV ? kind::BITVECTOR_UDIV_TOTAL : kind::BITVECTOR_UREM_TOTAL;
-      ret = nm->mkNode(kind, node[0], node[1]);
-      break;
-    }
+      if (options::bitvectorDivByZeroConst())
+      {
+        Kind kind = node.getKind() == kind::BITVECTOR_UDIV
+                        ? kind::BITVECTOR_UDIV_TOTAL
+                        : kind::BITVECTOR_UREM_TOTAL;
+        ret = nm->mkNode(kind, node[0], node[1]);
+        break;
+      }
 
-    TNode num = node[0], den = node[1];
-    Node den_eq_0 = nm->mkNode(kind::EQUAL, den, utils::mkZero(width));
-    Node divTotalNumDen = nm->mkNode(node.getKind() == kind::BITVECTOR_UDIV
-                                         ? kind::BITVECTOR_UDIV_TOTAL
-                                         : kind::BITVECTOR_UREM_TOTAL,
-                                     num,
-                                     den);
-    Node divByZero = getBVDivByZero(node.getKind(), width);
-    Node divByZeroNum = nm->mkNode(kind::APPLY_UF, divByZero, num);
-    ret = nm->mkNode(kind::ITE, den_eq_0, divByZeroNum, divTotalNumDen);
-  }
+      TNode num = node[0], den = node[1];
+      Node den_eq_0 = nm->mkNode(kind::EQUAL, den, utils::mkZero(width));
+      Node divTotalNumDen = nm->mkNode(node.getKind() == kind::BITVECTOR_UDIV
+                                           ? kind::BITVECTOR_UDIV_TOTAL
+                                           : kind::BITVECTOR_UREM_TOTAL,
+                                       num,
+                                       den);
+      Node divByZero = getUFDivByZero(node.getKind(), width);
+      Node divByZeroNum = nm->mkNode(kind::APPLY_UF, divByZero, num);
+      ret = nm->mkNode(kind::ITE, den_eq_0, divByZeroNum, divTotalNumDen);
+    }
     break;
 
-  default:
-    break;
+    default: break;
   }
   if (!ret.isNull() && node != ret)
   {
@@ -242,600 +152,50 @@ TrustNode TheoryBV::expandDefinition(Node node)
   return TrustNode::null();
 }
 
-void TheoryBV::preRegisterTerm(TNode node) {
-  d_calledPreregister = true;
-  Debug("bitvector-preregister") << "TheoryBV::preRegister(" << node << ")" << std::endl;
-
-  if (options::bitblastMode() == options::BitblastMode::EAGER)
-  {
-    // the aig bit-blaster option is set heuristically
-    // if bv abstraction is used
-    if (!d_eagerSolver->isInitialized())
-    {
-      d_eagerSolver->initialize();
-    }
-
-    if (node.getKind() == kind::BITVECTOR_EAGER_ATOM)
-    {
-      Node formula = node[0];
-      d_eagerSolver->assertFormula(formula);
-    }
-    return;
-  }
-
-  for (unsigned i = 0; i < d_subtheories.size(); ++i) {
-    d_subtheories[i]->preRegister(node);
-  }
-
-  // AJR : equality solver currently registers all terms to ExtTheory, if we
-  // want a lazy reduction without the bv equality solver, need to call this
-  // d_extTheory->registerTermRec( node );
-}
-
-void TheoryBV::sendConflict() {
-  Assert(d_conflict);
-  if (d_conflictNode.isNull()) {
-    return;
-  } else {
-    Debug("bitvector") << indent() << "TheoryBV::check(): conflict " << d_conflictNode << std::endl;
-    d_out->conflict(d_conflictNode);
-    d_statistics.d_avgConflictSize.addEntry(d_conflictNode.getNumChildren());
-    d_conflictNode = Node::null();
-  }
-}
-
-void TheoryBV::checkForLemma(TNode fact)
+void TheoryBV::preRegisterTerm(TNode node)
 {
-  if (fact.getKind() == kind::EQUAL)
-  {
-    NodeManager* nm = NodeManager::currentNM();
-    if (fact[0].getKind() == kind::BITVECTOR_UREM_TOTAL)
-    {
-      TNode urem = fact[0];
-      TNode result = fact[1];
-      TNode divisor = urem[1];
-      Node result_ult_div = nm->mkNode(kind::BITVECTOR_ULT, result, divisor);
-      Node divisor_eq_0 =
-          nm->mkNode(kind::EQUAL, divisor, mkZero(getSize(divisor)));
-      Node split = nm->mkNode(
-          kind::OR, divisor_eq_0, nm->mkNode(kind::NOT, fact), result_ult_div);
-      lemma(split);
-    }
-    if (fact[1].getKind() == kind::BITVECTOR_UREM_TOTAL)
-    {
-      TNode urem = fact[1];
-      TNode result = fact[0];
-      TNode divisor = urem[1];
-      Node result_ult_div = nm->mkNode(kind::BITVECTOR_ULT, result, divisor);
-      Node divisor_eq_0 =
-          nm->mkNode(kind::EQUAL, divisor, mkZero(getSize(divisor)));
-      Node split = nm->mkNode(
-          kind::OR, divisor_eq_0, nm->mkNode(kind::NOT, fact), result_ult_div);
-      lemma(split);
-    }
-  }
+  d_internal->preRegisterTerm(node);
 }
 
-void TheoryBV::check(Effort e)
-{
-  if (done() && e<Theory::EFFORT_FULL) {
-    return;
-  }
-
-  //last call : do reductions on extended bitvector functions
-  if (e == Theory::EFFORT_LAST_CALL) {
-    CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE];
-    if (core)
-    {
-      // check extended functions at last call effort
-      core->checkExtf(e);
-    }
-    return;
-  }
-
-  TimerStat::CodeTimer checkTimer(d_checkTime);
-  Debug("bitvector") << "TheoryBV::check(" << e << ")" << std::endl;
-  TimerStat::CodeTimer codeTimer(d_statistics.d_solveTimer);
-  // we may be getting new assertions so the model cache may not be sound
-  d_invalidateModelCache.set(true);
-  // if we are using the eager solver
-  if (options::bitblastMode() == options::BitblastMode::EAGER)
-  {
-    // this can only happen on an empty benchmark
-    if (!d_eagerSolver->isInitialized()) {
-      d_eagerSolver->initialize();
-    }
-    if (!Theory::fullEffort(e))
-      return;
-
-    std::vector<TNode> assertions;
-    while (!done()) {
-      TNode fact = get().d_assertion;
-      Assert(fact.getKind() == kind::BITVECTOR_EAGER_ATOM);
-      assertions.push_back(fact);
-      d_eagerSolver->assertFormula(fact[0]);
-    }
-
-    bool ok = d_eagerSolver->checkSat();
-    if (!ok) {
-      if (assertions.size() == 1) {
-        d_out->conflict(assertions[0]);
-        return;
-      }
-      Node conflict = utils::mkAnd(assertions);
-      d_out->conflict(conflict);
-      return;
-    }
-    return;
-  }
-
-  if (Theory::fullEffort(e)) {
-    ++(d_statistics.d_numCallsToCheckFullEffort);
-  } else {
-    ++(d_statistics.d_numCallsToCheckStandardEffort);
-  }
-  // if we are already in conflict just return the conflict
-  if (inConflict()) {
-    sendConflict();
-    return;
-  }
-
-  while (!done()) {
-    TNode fact = get().d_assertion;
-
-    checkForLemma(fact);
-
-    for (unsigned i = 0; i < d_subtheories.size(); ++i) {
-      d_subtheories[i]->assertFact(fact);
-    }
-  }
-
-  bool ok = true;
-  bool complete = false;
-  for (unsigned i = 0; i < d_subtheories.size(); ++i) {
-    Assert(!inConflict());
-    ok = d_subtheories[i]->check(e);
-    complete = d_subtheories[i]->isComplete();
-
-    if (!ok) {
-      // if we are in a conflict no need to check with other theories
-      Assert(inConflict());
-      sendConflict();
-      return;
-    }
-    if (complete) {
-      // if the last subtheory was complete we stop
-      break;
-    }
-  }
-
-  //check extended functions
-  if (Theory::fullEffort(e)) {
-    CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE];
-    if (core)
-    {
-      // check extended functions at full effort
-      core->checkExtf(e);
-    }
-  }
-}
+bool TheoryBV::preCheck(Effort e) { return d_internal->preCheck(e); }
 
 bool TheoryBV::needsCheckLastEffort()
 {
-  CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE];
-  if (core)
-  {
-    return core->needsCheckLastEffort();
-  }
-  return false;
+  return d_internal->needsCheckLastEffort();
 }
+
 bool TheoryBV::collectModelInfo(TheoryModel* m)
 {
-  Assert(!inConflict());
-  if (options::bitblastMode() == options::BitblastMode::EAGER)
-  {
-    if (!d_eagerSolver->collectModelInfo(m, true))
-    {
-      return false;
-    }
-  }
-  for (unsigned i = 0; i < d_subtheories.size(); ++i) {
-    if (d_subtheories[i]->isComplete()) {
-      return d_subtheories[i]->collectModelInfo(m, true);
-    }
-  }
-  return true;
+  return d_internal->collectModelInfo(m);
 }
 
-Node TheoryBV::getModelValue(TNode var) {
-  Assert(!inConflict());
-  for (unsigned i = 0; i < d_subtheories.size(); ++i) {
-    if (d_subtheories[i]->isComplete()) {
-      return d_subtheories[i]->getModelValue(var);
-    }
-  }
-  Unreachable();
-}
-
-void TheoryBV::propagate(Effort e) {
-  Debug("bitvector") << indent() << "TheoryBV::propagate()" << std::endl;
-  if (options::bitblastMode() == options::BitblastMode::EAGER)
-  {
-    return;
-  }
-
-  if (inConflict()) {
-    return;
-  }
-
-  // go through stored propagations
-  bool ok = true;
-  for (; d_literalsToPropagateIndex < d_literalsToPropagate.size() && ok; d_literalsToPropagateIndex = d_literalsToPropagateIndex + 1) {
-    TNode literal = d_literalsToPropagate[d_literalsToPropagateIndex];
-    // temporary fix for incremental bit-blasting
-    if (d_valuation.isSatLiteral(literal)) {
-      Debug("bitvector::propagate") << "TheoryBV:: propagating " << literal <<"\n";
-      ok = d_out->propagate(literal);
-    }
-  }
-
-  if (!ok) {
-    Debug("bitvector::propagate") << indent() << "TheoryBV::propagate(): conflict from theory engine" << std::endl;
-    setConflict();
-  }
-}
+void TheoryBV::propagate(Effort e) { return d_internal->propagate(e); }
 
 Theory::PPAssertStatus TheoryBV::ppAssert(TNode in,
                                           SubstitutionMap& outSubstitutions)
 {
-  switch (in.getKind())
-  {
-    case kind::EQUAL:
-    {
-      if (in[0].isVar() && isLegalElimination(in[0], in[1]))
-      {
-        ++(d_statistics.d_solveSubstitutions);
-        outSubstitutions.addSubstitution(in[0], in[1]);
-        return PP_ASSERT_STATUS_SOLVED;
-      }
-      if (in[1].isVar() && isLegalElimination(in[1], in[0]))
-      {
-        ++(d_statistics.d_solveSubstitutions);
-        outSubstitutions.addSubstitution(in[1], in[0]);
-        return PP_ASSERT_STATUS_SOLVED;
-      }
-      Node node = Rewriter::rewrite(in);
-      if ((node[0].getKind() == kind::BITVECTOR_EXTRACT && node[1].isConst())
-          || (node[1].getKind() == kind::BITVECTOR_EXTRACT
-              && node[0].isConst()))
-      {
-        Node extract = node[0].isConst() ? node[1] : node[0];
-        if (extract[0].isVar())
-        {
-          Node c = node[0].isConst() ? node[0] : node[1];
-
-          unsigned high = utils::getExtractHigh(extract);
-          unsigned low = utils::getExtractLow(extract);
-          unsigned var_bitwidth = utils::getSize(extract[0]);
-          std::vector<Node> children;
-
-          if (low == 0)
-          {
-            Assert(high != var_bitwidth - 1);
-            unsigned skolem_size = var_bitwidth - high - 1;
-            Node skolem = utils::mkVar(skolem_size);
-            children.push_back(skolem);
-            children.push_back(c);
-          }
-          else if (high == var_bitwidth - 1)
-          {
-            unsigned skolem_size = low;
-            Node skolem = utils::mkVar(skolem_size);
-            children.push_back(c);
-            children.push_back(skolem);
-          }
-          else
-          {
-            unsigned skolem1_size = low;
-            unsigned skolem2_size = var_bitwidth - high - 1;
-            Node skolem1 = utils::mkVar(skolem1_size);
-            Node skolem2 = utils::mkVar(skolem2_size);
-            children.push_back(skolem2);
-            children.push_back(c);
-            children.push_back(skolem1);
-          }
-          Node concat = utils::mkConcat(children);
-          Assert(utils::getSize(concat) == utils::getSize(extract[0]));
-          if (isLegalElimination(extract[0], concat))
-          {
-            outSubstitutions.addSubstitution(extract[0], concat);
-            return PP_ASSERT_STATUS_SOLVED;
-          }
-        }
-      }
-    }
-    break;
-    case kind::BITVECTOR_ULT:
-    case kind::BITVECTOR_SLT:
-    case kind::BITVECTOR_ULE:
-    case kind::BITVECTOR_SLE:
-
-    default:
-      // TODO other predicates
-      break;
-  }
-  return PP_ASSERT_STATUS_UNSOLVED;
-}
-
-TrustNode TheoryBV::ppRewrite(TNode t)
-{
-  Debug("bv-pp-rewrite") << "TheoryBV::ppRewrite " << t << "\n";
-  Node res = t;
-  if (options::bitwiseEq() && RewriteRule<BitwiseEq>::applies(t)) {
-    Node result = RewriteRule<BitwiseEq>::run<false>(t);
-    res = Rewriter::rewrite(result);
-  } else if (RewriteRule<UltPlusOne>::applies(t)) {
-    Node result = RewriteRule<UltPlusOne>::run<false>(t);
-    res = Rewriter::rewrite(result);
-  }
-  else if (res.getKind() == kind::EQUAL
-           && ((res[0].getKind() == kind::BITVECTOR_PLUS
-                && RewriteRule<ConcatToMult>::applies(res[1]))
-               || (res[1].getKind() == kind::BITVECTOR_PLUS
-                   && RewriteRule<ConcatToMult>::applies(res[0]))))
-  {
-    Node mult = RewriteRule<ConcatToMult>::applies(res[0])?
-      RewriteRule<ConcatToMult>::run<false>(res[0]) :
-      RewriteRule<ConcatToMult>::run<true>(res[1]);
-    Node factor = mult[0];
-    Node sum =  RewriteRule<ConcatToMult>::applies(res[0])? res[1] : res[0];
-    Node new_eq = NodeManager::currentNM()->mkNode(kind::EQUAL, sum, mult);
-    Node rewr_eq = RewriteRule<SolveEq>::run<true>(new_eq);
-    if (rewr_eq[0].isVar() || rewr_eq[1].isVar()){
-      res = Rewriter::rewrite(rewr_eq);
-    } else {
-      res = t;
-    }
-  }
-  else if (RewriteRule<SignExtendEqConst>::applies(t))
-  {
-    res = RewriteRule<SignExtendEqConst>::run<false>(t);
-  }
-  else if (RewriteRule<ZeroExtendEqConst>::applies(t))
-  {
-    res = RewriteRule<ZeroExtendEqConst>::run<false>(t);
-  }
-  else if (RewriteRule<NormalizeEqPlusNeg>::applies(t))
-  {
-    res = RewriteRule<NormalizeEqPlusNeg>::run<false>(t);
-  }
-
-  // if(t.getKind() == kind::EQUAL &&
-  //    ((t[0].getKind() == kind::BITVECTOR_MULT && t[1].getKind() ==
-  //    kind::BITVECTOR_PLUS) ||
-  //     (t[1].getKind() == kind::BITVECTOR_MULT && t[0].getKind() ==
-  //     kind::BITVECTOR_PLUS))) {
-  //   // if we have an equality between a multiplication and addition
-  //   // try to express multiplication in terms of addition
-  //   Node mult = t[0].getKind() == kind::BITVECTOR_MULT? t[0] : t[1];
-  //   Node add = t[0].getKind() == kind::BITVECTOR_PLUS? t[0] : t[1];
-  //   if (RewriteRule<MultSlice>::applies(mult)) {
-  //     Node new_mult = RewriteRule<MultSlice>::run<false>(mult);
-  //     Node new_eq =
-  //     Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::EQUAL,
-  //     new_mult, add));
-
-  //     // the simplification can cause the formula to blow up
-  //     // only apply if formula reduced
-  //     if (d_subtheoryMap.find(SUB_BITBLAST) != d_subtheoryMap.end()) {
-  //       BitblastSolver* bv = (BitblastSolver*)d_subtheoryMap[SUB_BITBLAST];
-  //       uint64_t old_size = bv->computeAtomWeight(t);
-  //       Assert (old_size);
-  //       uint64_t new_size = bv->computeAtomWeight(new_eq);
-  //       double ratio = ((double)new_size)/old_size;
-  //       if (ratio <= 0.4) {
-  //         ++(d_statistics.d_numMultSlice);
-  //         return new_eq;
-  //       }
-  //     }
-
-  //     if (new_eq.getKind() == kind::CONST_BOOLEAN) {
-  //       ++(d_statistics.d_numMultSlice);
-  //       return new_eq;
-  //     }
-  //   }
-  // }
-
-  if (options::bvAbstraction() && t.getType().isBoolean()) {
-    d_abstractionModule->addInputAtom(res);
-  }
-  Debug("bv-pp-rewrite") << "to   " << res << "\n";
-  if (res != t)
-  {
-    return TrustNode::mkTrustRewrite(t, res, nullptr);
-  }
-  return TrustNode::null();
-}
-
-void TheoryBV::presolve() {
-  Debug("bitvector") << "TheoryBV::presolve" << endl;
-}
-
-static int prop_count = 0;
-
-bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory)
-{
-  Debug("bitvector::propagate") << indent() << getSatContext()->getLevel() << " " << "TheoryBV::storePropagation(" << literal << ", " << subtheory << ")" << std::endl;
-  prop_count++;
-
-  // If already in conflict, no more propagation
-  if (d_conflict) {
-    Debug("bitvector::propagate") << indent() << "TheoryBV::storePropagation(" << literal << ", " << subtheory << "): already in conflict" << std::endl;
-    return false;
-  }
-
-  // If propagated already, just skip
-  PropagatedMap::const_iterator find = d_propagatedBy.find(literal);
-  if (find != d_propagatedBy.end()) {
-    return true;
-  } else {
-    bool polarity = literal.getKind() != kind::NOT;
-    Node negatedLiteral = polarity ? literal.notNode() : (Node) literal[0];
-    find = d_propagatedBy.find(negatedLiteral);
-    if (find != d_propagatedBy.end() && (*find).second != subtheory) {
-      // Safe to ignore this one, subtheory should produce a conflict
-      return true;
-    }
-
-    d_propagatedBy[literal] = subtheory;
-  }
-
-  // Propagate differs depending on the subtheory
-  // * bitblaster needs to be left alone until it's done, otherwise it doesn't
-  //   know how to explain
-  // * equality engine can propagate eagerly
-  // TODO(2348): Determine if ok should be set by propagate. If not, remove ok.
-  constexpr bool ok = true;
-  if (subtheory == SUB_CORE) {
-    d_out->propagate(literal);
-    if (!ok) {
-      setConflict();
-    }
-  } else {
-    d_literalsToPropagate.push_back(literal);
-  }
-  return ok;
-
-}/* TheoryBV::propagate(TNode) */
-
-
-void TheoryBV::explain(TNode literal, std::vector<TNode>& assumptions) {
-  Assert(wasPropagatedBySubtheory(literal));
-  SubTheory sub = getPropagatingSubtheory(literal);
-  d_subtheoryMap[sub]->explain(literal, assumptions);
+  return d_internal->ppAssert(in, outSubstitutions);
 }
 
-TrustNode TheoryBV::explain(TNode node)
-{
-  Debug("bitvector::explain") << "TheoryBV::explain(" << node << ")" << std::endl;
-  std::vector<TNode> assumptions;
+TrustNode TheoryBV::ppRewrite(TNode t) { return d_internal->ppRewrite(t); }
 
-  // Ask for the explanation
-  explain(node, assumptions);
-  // this means that it is something true at level 0
-  Node explanation;
-  if (assumptions.size() == 0) {
-    explanation = utils::mkTrue();
-  }
-  else
-  {
-    // return the explanation
-    explanation = utils::mkAnd(assumptions);
-  }
-  Debug("bitvector::explain") << "TheoryBV::explain(" << node << ") => " << explanation << std::endl;
-  Debug("bitvector::explain") << "TheoryBV::explain done. \n";
-  return TrustNode::mkTrustPropExp(node, explanation, nullptr);
-}
+void TheoryBV::presolve() { d_internal->presolve(); }
 
-void TheoryBV::notifySharedTerm(TNode t)
-{
-  Debug("bitvector::sharing")
-      << indent() << "TheoryBV::notifySharedTerm(" << t << ")" << std::endl;
-  d_sharedTermsSet.insert(t);
-  if (options::bitvectorEqualitySolver()) {
-    for (unsigned i = 0; i < d_subtheories.size(); ++i) {
-      d_subtheories[i]->addSharedTerm(t);
-    }
-  }
-}
+TrustNode TheoryBV::explain(TNode node) { return d_internal->explain(node); }
 
+void TheoryBV::notifySharedTerm(TNode t) { d_internal->notifySharedTerm(t); };
 
-EqualityStatus TheoryBV::getEqualityStatus(TNode a, TNode b)
+void TheoryBV::ppStaticLearn(TNode in, NodeBuilder<>& learned)
 {
-  if (options::bitblastMode() == options::BitblastMode::EAGER)
-    return EQUALITY_UNKNOWN;
-  Assert(options::bitblastMode() == options::BitblastMode::LAZY);
-  for (unsigned i = 0; i < d_subtheories.size(); ++i) {
-    EqualityStatus status = d_subtheories[i]->getEqualityStatus(a, b);
-    if (status != EQUALITY_UNKNOWN) {
-      return status;
-    }
-  }
-  return EQUALITY_UNKNOWN; ;
-}
-
-void TheoryBV::ppStaticLearn(TNode in, NodeBuilder<>& learned) {
-  if(d_staticLearnCache.find(in) != d_staticLearnCache.end()){
-    return;
-  }
-  d_staticLearnCache.insert(in);
-
-  if (in.getKind() == kind::EQUAL) {
-    if((in[0].getKind() == kind::BITVECTOR_PLUS && in[1].getKind() == kind::BITVECTOR_SHL) ||
-       (in[1].getKind() == kind::BITVECTOR_PLUS && in[0].getKind() == kind::BITVECTOR_SHL)) {
-      TNode p = in[0].getKind() == kind::BITVECTOR_PLUS ? in[0] : in[1];
-      TNode s = in[0].getKind() == kind::BITVECTOR_PLUS ? in[1] : in[0];
-
-      if(p.getNumChildren() == 2
-         && p[0].getKind()  == kind::BITVECTOR_SHL
-         && p[1].getKind()  == kind::BITVECTOR_SHL ){
-        unsigned size = utils::getSize(s);
-        Node one = utils::mkConst(size, 1u);
-        if(s[0] == one && p[0][0] == one && p[1][0] == one){
-          Node zero = utils::mkConst(size, 0u);
-          TNode b = p[0];
-          TNode c = p[1];
-          // (s : 1 << S) = (b : 1 << B) + (c : 1 << C)
-          Node b_eq_0 = b.eqNode(zero);
-          Node c_eq_0 = c.eqNode(zero);
-          Node b_eq_c = b.eqNode(c);
-
-          Node dis = NodeManager::currentNM()->mkNode(
-              kind::OR, b_eq_0, c_eq_0, b_eq_c);
-          Node imp = in.impNode(dis);
-          learned << imp;
-        }
-      }
-    }
-  }else if(in.getKind() == kind::AND){
-    for(size_t i = 0, N = in.getNumChildren(); i < N; ++i){
-      ppStaticLearn(in[i], learned);
-    }
-  }
+  d_internal->ppStaticLearn(in, learned);
 }
 
-bool TheoryBV::applyAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions) {
-  bool changed = d_abstractionModule->applyAbstraction(assertions, new_assertions);
-  if (changed && options::bitblastMode() == options::BitblastMode::EAGER
-      && options::bitvectorAig())
-  {
-    // disable AIG mode
-    AlwaysAssert(!d_eagerSolver->isInitialized());
-    d_eagerSolver->turnOffAig();
-    d_eagerSolver->initialize();
-  }
-  return changed;
-}
-
-void TheoryBV::setConflict(Node conflict)
+bool TheoryBV::applyAbstraction(const std::vector<Node>& assertions,
+                                std::vector<Node>& new_assertions)
 {
-  if (options::bvAbstraction())
-  {
-    NodeManager* const nm = NodeManager::currentNM();
-    Node new_conflict = d_abstractionModule->simplifyConflict(conflict);
-
-    std::vector<Node> lemmas;
-    lemmas.push_back(new_conflict);
-    d_abstractionModule->generalizeConflict(new_conflict, lemmas);
-    for (unsigned i = 0; i < lemmas.size(); ++i)
-    {
-      lemma(nm->mkNode(kind::NOT, lemmas[i]));
-    }
-  }
-  d_conflict = true;
-  d_conflictNode = conflict;
+  return d_internal->applyAbstraction(assertions, new_assertions);
 }
 
-} /* namespace CVC4::theory::bv */
-} /* namespace CVC4::theory */
-} /* namespace CVC4 */
+}  // namespace bv
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 7475feccc..d33ea1337 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -20,42 +20,21 @@
 #define CVC4__THEORY__BV__THEORY_BV_H
 
 #include <unordered_map>
-#include <unordered_set>
 
-#include "context/cdhashset.h"
-#include "context/cdlist.h"
-#include "context/context.h"
-#include "theory/bv/bv_subtheory.h"
 #include "theory/bv/theory_bv_rewriter.h"
-#include "theory/bv/theory_bv_utils.h"
 #include "theory/theory.h"
-#include "util/hash.h"
-#include "util/statistics_registry.h"
 
 namespace CVC4 {
 namespace theory {
 namespace bv {
 
-class CoreSolver;
-class InequalitySolver;
-class AlgebraicSolver;
-class BitblastSolver;
+class BVSolver;
 
-class EagerBitblastSolver;
-
-class AbstractionModule;
-
-class TheoryBV : public Theory {
-
-  /** The context we are using */
-  context::Context* d_context;
-
-  /** Context dependent set of atoms we already propagated */
-  context::CDHashSet<Node, NodeHashFunction> d_alreadyPropagatedSet;
-  context::CDHashSet<Node, NodeHashFunction> d_sharedTermsSet;
-
-  std::vector<std::unique_ptr<SubtheorySolver>> d_subtheories;
-  std::unordered_map<SubTheory, SubtheorySolver*, std::hash<int> > d_subtheoryMap;
+class TheoryBV : public Theory
+{
+  /* BVSolverLazy accesses methods from theory in a way that is deprecated and
+   * will be removed in the future. For now we allow direct access. */
+  friend class BVSolverLazy;
 
  public:
   TheoryBV(context::Context* c,
@@ -68,24 +47,23 @@ class TheoryBV : public Theory {
 
   ~TheoryBV();
 
-  //--------------------------------- initialization
   /** get the official theory rewriter of this theory */
   TheoryRewriter* getTheoryRewriter() override;
+
   /**
    * Returns true if we need an equality engine. If so, we initialize the
    * information regarding how it should be setup. For details, see the
    * documentation in Theory::needsEqualityEngine.
    */
   bool needsEqualityEngine(EeSetupInfo& esi) override;
-  /** finish initialization */
+
   void finishInit() override;
-  //--------------------------------- end initialization
 
   TrustNode expandDefinition(Node node) override;
 
   void preRegisterTerm(TNode n) override;
 
-  void check(Effort e) override;
+  bool preCheck(Effort e) override;
 
   bool needsCheckLastEffort() override;
 
@@ -105,146 +83,44 @@ class TheoryBV : public Theory {
 
   void presolve() override;
 
+  /** Called by abstraction preprocessing pass. */
   bool applyAbstraction(const std::vector<Node>& assertions,
                         std::vector<Node>& new_assertions);
 
  private:
-  class Statistics
-  {
-   public:
-    AverageStat d_avgConflictSize;
-    IntStat     d_solveSubstitutions;
-    TimerStat   d_solveTimer;
-    IntStat     d_numCallsToCheckFullEffort;
-    IntStat     d_numCallsToCheckStandardEffort;
-    TimerStat   d_weightComputationTimer;
-    IntStat     d_numMultSlice;
-    Statistics();
-    ~Statistics();
-  };
-
-  Statistics d_statistics;
-
-  void spendResource(ResourceManager::Resource r);
+  void notifySharedTerm(TNode t) override;
 
   /**
-   * Return the uninterpreted function symbol corresponding to division-by-zero
-   * for this particular bit-width
+   * Return the UF symbol corresponding to division-by-zero for this particular
+   * bit-width.
    * @param k should be UREM or UDIV
-   * @param width
-   *
-   * @return
+   * @param width bit-width
    */
-  Node getBVDivByZero(Kind k, unsigned width);
+  Node getUFDivByZero(Kind k, unsigned width);
 
-  typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
-  typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
-  NodeSet d_staticLearnCache;
+  /** Internal BV solver. */
+  std::unique_ptr<BVSolver> d_internal;
 
   /**
    * Maps from bit-vector width to division-by-zero uninterpreted
    * function symbols.
    */
-  std::unordered_map<unsigned, Node> d_BVDivByZero;
-  std::unordered_map<unsigned, Node> d_BVRemByZero;
-
-  typedef std::unordered_map<Node, Node, NodeHashFunction>  NodeToNode;
-
-  context::CDO<bool> d_lemmasAdded;
-
-  // Are we in conflict?
-  context::CDO<bool> d_conflict;
-
-  // Invalidate the model cache if check was called
-  context::CDO<bool> d_invalidateModelCache;
-
-  /** The conflict node */
-  Node d_conflictNode;
-
-  /** Literals to propagate */
-  context::CDList<Node> d_literalsToPropagate;
-
-  /** Index of the next literal to propagate */
-  context::CDO<unsigned> d_literalsToPropagateIndex;
-
-  /**
-   * Keeps a map from nodes to the subtheory that propagated it so that we can explain it
-   * properly.
-   */
-  typedef context::CDHashMap<Node, SubTheory, NodeHashFunction> PropagatedMap;
-  PropagatedMap d_propagatedBy;
-
-  std::unique_ptr<EagerBitblastSolver> d_eagerSolver;
-  std::unique_ptr<AbstractionModule> d_abstractionModule;
-  bool d_calledPreregister;
-
-  bool wasPropagatedBySubtheory(TNode literal) const {
-    return d_propagatedBy.find(literal) != d_propagatedBy.end();
-  }
-
-  SubTheory getPropagatingSubtheory(TNode literal) const {
-    Assert(wasPropagatedBySubtheory(literal));
-    PropagatedMap::const_iterator find = d_propagatedBy.find(literal);
-    return (*find).second;
-  }
-
-  /** Should be called to propagate the literal.  */
-  bool storePropagation(TNode literal, SubTheory subtheory);
-
-  /**
-   * Explains why this literal (propagated by subtheory) is true by adding assumptions.
-   */
-  void explain(TNode literal, std::vector<TNode>& assumptions);
-
-  void notifySharedTerm(TNode t) override;
-
-  bool isSharedTerm(TNode t) { return d_sharedTermsSet.contains(t); }
-
-  EqualityStatus getEqualityStatus(TNode a, TNode b) override;
-
-  Node getModelValue(TNode var) override;
-
-  inline std::string indent()
-  {
-    std::string indentStr(getSatContext()->getLevel(), ' ');
-    return indentStr;
-  }
-
-  void setConflict(Node conflict = Node::null());
-
-  bool inConflict() {
-    return d_conflict;
-  }
-
-  void sendConflict();
-
-  void lemma(TNode node)
-  {
-    d_out->lemma(node);
-    d_lemmasAdded = true;
-  }
-
-  void checkForLemma(TNode node);
+  std::unordered_map<unsigned, Node> d_ufDivByZero;
+  std::unordered_map<unsigned, Node> d_ufRemByZero;
 
   /** The theory rewriter for this theory. */
   TheoryBVRewriter d_rewriter;
+
   /** A (default) theory state object */
   TheoryState d_state;
 
-  friend class LazyBitblaster;
-  friend class TLazyBitblaster;
-  friend class EagerBitblaster;
-  friend class BitblastSolver;
-  friend class EqualitySolver;
-  friend class CoreSolver;
-  friend class InequalitySolver;
-  friend class AlgebraicSolver;
-  friend class EagerBitblastSolver;
-};/* class TheoryBV */
-
-}/* CVC4::theory::bv namespace */
-}/* CVC4::theory namespace */
-
-}/* CVC4 namespace */
+  /** A (default) theory inference manager. */
+  TheoryInferenceManager d_inferMgr;
+
+}; /* class TheoryBV */
+
+}  // namespace bv
+}  // namespace theory
+}  // namespace CVC4
 
 #endif /* CVC4__THEORY__BV__THEORY_BV_H */
diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp
index 40fa9c5ae..570b878b4 100644
--- a/src/theory/theory_inference_manager.cpp
+++ b/src/theory/theory_inference_manager.cpp
@@ -449,5 +449,15 @@ void TheoryInferenceManager::requirePhase(TNode n, bool pol)
   return d_out.requirePhase(n, pol);
 }
 
+void TheoryInferenceManager::spendResource(ResourceManager::Resource r)
+{
+  d_out.spendResource(r);
+}
+
+void TheoryInferenceManager::safePoint(ResourceManager::Resource r)
+{
+  d_out.safePoint(r);
+}
+
 }  // namespace theory
 }  // namespace CVC4
diff --git a/src/theory/theory_inference_manager.h b/src/theory/theory_inference_manager.h
index 92116648e..7fecacf82 100644
--- a/src/theory/theory_inference_manager.h
+++ b/src/theory/theory_inference_manager.h
@@ -329,6 +329,17 @@ class TheoryInferenceManager
    * decided with polarity pol, for details see OutputChannel::requirePhase.
    */
   void requirePhase(TNode n, bool pol);
+
+  /**
+   * Forward to OutputChannel::spendResource() to spend resources.
+   */
+  void spendResource(ResourceManager::Resource r);
+
+  /**
+   * Forward to OutputChannel::safePoint() to spend resources.
+   */
+  void safePoint(ResourceManager::Resource r);
+
  protected:
   /**
    * Process internal fact. This is a common helper method for the
diff --git a/src/theory/theory_state.cpp b/src/theory/theory_state.cpp
index 8afe3be96..f22a652c0 100644
--- a/src/theory/theory_state.cpp
+++ b/src/theory/theory_state.cpp
@@ -125,5 +125,10 @@ void TheoryState::notifyInConflict() { d_conflict = true; }
 
 bool TheoryState::isInConflict() const { return d_conflict; }
 
+bool TheoryState::isSatLiteral(TNode lit) const
+{
+  return d_valuation.isSatLiteral(lit);
+}
+
 }  // namespace theory
 }  // namespace CVC4
diff --git a/src/theory/theory_state.h b/src/theory/theory_state.h
index de6e6d477..4ae381e78 100644
--- a/src/theory/theory_state.h
+++ b/src/theory/theory_state.h
@@ -72,6 +72,9 @@ class TheoryState
   /** Are we currently in conflict? */
   virtual bool isInConflict() const;
 
+  /** Returns true if lit is a SAT literal. */
+  virtual bool isSatLiteral(TNode lit) const;
+
  protected:
   /** Pointer to the SAT context object used by the theory. */
   context::Context* d_context;
diff --git a/test/unit/theory/theory_bv_white.h b/test/unit/theory/theory_bv_white.h
index 582a031c9..cacd92d41 100644
--- a/test/unit/theory/theory_bv_white.h
+++ b/test/unit/theory/theory_bv_white.h
@@ -15,22 +15,20 @@
  ** \todo document this file
  **/
 
-
 #include <cxxtest/TestSuite.h>
 
-#include "theory/theory.h"
+#include <vector>
+
+#include "context/context.h"
+#include "expr/node.h"
+#include "expr/node_manager.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
-#include "theory/bv/theory_bv.h"
 #include "theory/bv/bitblast/eager_bitblaster.h"
-#include "expr/node.h"
-#include "expr/node_manager.h"
-#include "context/context.h"
-
+#include "theory/bv/bv_solver_lazy.h"
+#include "theory/theory.h"
 #include "theory/theory_test_utils.h"
 
-#include <vector>
-
 using namespace CVC4;
 using namespace CVC4::theory;
 using namespace CVC4::theory::bv;
@@ -76,10 +74,11 @@ public:
     // engine d_smt. We must ensure that d_smt is properly initialized via
     // the following call, which constructs its underlying theory engine.
     d_smt->finishInit();
-    EagerBitblaster* bb = new EagerBitblaster(
-        dynamic_cast<TheoryBV*>(
-            d_smt->getTheoryEngine()->d_theoryTable[THEORY_BV]),
-        d_smt->getContext());
+    TheoryBV* tbv = dynamic_cast<TheoryBV*>(
+        d_smt->getTheoryEngine()->d_theoryTable[THEORY_BV]);
+    BVSolverLazy* bvsl = dynamic_cast<BVSolverLazy*>(tbv->d_internal.get());
+    EagerBitblaster* bb = new EagerBitblaster(bvsl, d_smt->getContext());
+
     Node x = d_nm->mkVar("x", d_nm->mkBitVectorType(16));
     Node y = d_nm->mkVar("y", d_nm->mkBitVectorType(16));
     Node x_plus_y = d_nm->mkNode(kind::BITVECTOR_PLUS, x, y);