Reorganize bitblaster code. (#1695)

This splits bitblaster_template.h into the separate header files {aig,eager,lazy}_bitblaster.h and
bitblaster.h (the template class TBitblaster). All the bitblaster related code is moved into the
sub-directory bitblast/.

14 files changed, 792 insertions, 675 deletions

diff --git a/src/theory/bv/aig_bitblaster.cpp b/src/theory/bv/bitblast/aig_bitblaster.cpp
index 010eaf4e5..7e666bcbf 100644
--- a/src/theory/bv/aig_bitblaster.cpp
+++ b/src/theory/bv/bitblast/aig_bitblaster.cpp
@@ -9,29 +9,35 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief 
+ ** \brief AIG bitblaster.
  **
- ** Bitblaster for the lazy bv solver. 
+ ** AIG bitblaster.
  **/
 
-#include "bitblaster_template.h"
-
 #include "cvc4_private.h"
 
+#include "theory/bv/bitblast/aig_bitblaster.h"
+
 #include "base/cvc4_check.h"
 #include "options/bv_options.h"
-#include "prop/cnf_stream.h"
 #include "prop/sat_solver_factory.h"
 #include "smt/smt_statistics_registry.h"
 
 #ifdef CVC4_USE_ABC
-// Function is defined as static in ABC. Not sure how else to do this. 
-static inline int Cnf_Lit2Var( int Lit ) { return (Lit & 1)? -(Lit >> 1)-1 : (Lit >> 1)+1;  }
 
 extern "C" {
-extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
+#include "base/abc/abc.h"
+#include "base/main/main.h"
+#include "sat/cnf/cnf.h"
+
+extern Aig_Man_t* Abc_NtkToDar(Abc_Ntk_t* pNtk, int fExors, int fRegisters);
 }
 
+// Function is defined as static in ABC. Not sure how else to do this.
+static inline int Cnf_Lit2Var(int Lit)
+{
+  return (Lit & 1) ? -(Lit >> 1) - 1 : (Lit >> 1) + 1;
+}
 
 namespace CVC4 {
 namespace theory {
@@ -110,26 +116,17 @@ Abc_Obj_t* mkIte<Abc_Obj_t*>(Abc_Obj_t* cond, Abc_Obj_t* a, Abc_Obj_t* b) {
   return Abc_AigMux(AigBitblaster::currentAigM(), cond, a, b); 
 }
 
-} /* CVC4::theory::bv */
-} /* CVC4::theory */
-} /* CVC4 */
-
-using namespace CVC4;
-using namespace CVC4::theory;
-using namespace CVC4::theory::bv;
-
-
-Abc_Ntk_t* AigBitblaster::abcAigNetwork = NULL;
+CVC4_THREAD_LOCAL Abc_Ntk_t* AigBitblaster::s_abcAigNetwork = nullptr;
 
 Abc_Ntk_t* AigBitblaster::currentAigNtk() {
-  if (!AigBitblaster::abcAigNetwork) {
+  if (!AigBitblaster::s_abcAigNetwork) {
     Abc_Start();
-    abcAigNetwork = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1); 
+    s_abcAigNetwork = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1);
     char pName[] = "CVC4::theory::bv::AigNetwork";
-    abcAigNetwork->pName = Extra_UtilStrsav(pName);
+    s_abcAigNetwork->pName = Extra_UtilStrsav(pName);
   }
   
-  return abcAigNetwork;
+  return s_abcAigNetwork;
 }
 
 
@@ -138,34 +135,39 @@ Abc_Aig_t* AigBitblaster::currentAigM() {
 }
 
 AigBitblaster::AigBitblaster()
-  : TBitblaster<Abc_Obj_t*>()
-  , d_aigCache()
-  , d_bbAtoms()
-  , d_aigOutputNode(NULL)
+    : TBitblaster<Abc_Obj_t*>(),
+      d_nullContext(new context::Context()),
+      d_aigCache(),
+      d_bbAtoms(),
+      d_aigOutputNode(NULL)
 {
-  d_nullContext = new context::Context();
-  switch(options::bvSatSolver()) {
-  case SAT_SOLVER_MINISAT: {
-    prop::BVSatSolverInterface* minisat = prop::SatSolverFactory::createMinisat(d_nullContext,
-                                                                                smtStatisticsRegistry(),
-                                                                                "AigBitblaster");
-    MinisatEmptyNotify* notify = new MinisatEmptyNotify();
-    minisat->setNotify(notify);
-    d_satSolver = minisat;
-    break;
-  }
-  case SAT_SOLVER_CRYPTOMINISAT:
-    d_satSolver = prop::SatSolverFactory::createCryptoMinisat(smtStatisticsRegistry(),
-                                                              "AigBitblaster");
-    break;
-  default: CVC4_FATAL() << "Unknown SAT solver type";
+  prop::SatSolver* solver = nullptr;
+  switch (options::bvSatSolver())
+  {
+    case SAT_SOLVER_MINISAT:
+    {
+      prop::BVSatSolverInterface* minisat =
+          prop::SatSolverFactory::createMinisat(
+              d_nullContext.get(), smtStatisticsRegistry(), "AigBitblaster");
+      MinisatEmptyNotify notify;
+      minisat->setNotify(&notify);
+      solver = minisat;
+      break;
+    }
+    case SAT_SOLVER_CADICAL:
+      solver = prop::SatSolverFactory::createCadical(smtStatisticsRegistry(),
+                                                     "AigBitblaster");
+      break;
+    case SAT_SOLVER_CRYPTOMINISAT:
+      solver = prop::SatSolverFactory::createCryptoMinisat(
+          smtStatisticsRegistry(), "AigBitblaster");
+      break;
+    default: CVC4_FATAL() << "Unknown SAT solver type";
   }
+  d_satSolver.reset(solver);
 }
 
-AigBitblaster::~AigBitblaster() {
-  Assert (abcAigNetwork == NULL);
-  delete d_nullContext;
-}
+AigBitblaster::~AigBitblaster() {}
 
 Abc_Obj_t* AigBitblaster::bbFormula(TNode node) {
   Assert (node.getType().isBoolean());
@@ -363,7 +365,7 @@ void AigBitblaster::simplifyAig() {
     fprintf( stdout, "Cannot execute command \"%s\".\n", command );
     exit(-1); 
   }
-  abcAigNetwork = Abc_FrameReadNtk(pAbc); 
+  s_abcAigNetwork = Abc_FrameReadNtk(pAbc);
 }
 
 
@@ -380,7 +382,7 @@ void AigBitblaster::convertToCnfAndAssert() {
 
   // // free old network
   // Abc_NtkDelete(currentAigNtk());
-  // abcAigNetwork = NULL;
+  // s_abcAigNetwork = NULL;
   
   Assert (pMan != NULL);
   Assert (Aig_ManCheck(pMan));
@@ -485,4 +487,8 @@ AigBitblaster::Statistics::~Statistics() {
   smtStatisticsRegistry()->unregisterStat(&d_cnfConversionTime);
   smtStatisticsRegistry()->unregisterStat(&d_solveTime); 
 }
+
+}  // namespace bv
+}  // namespace theory
+}  // namespace CVC4
 #endif // CVC4_USE_ABC
diff --git a/src/theory/bv/bitblast/aig_bitblaster.h b/src/theory/bv/bitblast/aig_bitblaster.h
new file mode 100644
index 000000000..30f1dd00b
--- /dev/null
+++ b/src/theory/bv/bitblast/aig_bitblaster.h
@@ -0,0 +1,105 @@
+/*********************                                                        */
+/*! \file aig_bitblaster.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Liana Hadarean, Tim King, Aina Niemetz
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 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 AIG bitblaster.
+ **
+ ** AIG Bitblaster based on ABC.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__BV__BITBLAST__AIG_BITBLASTER_H
+#define __CVC4__THEORY__BV__BITBLAST__AIG_BITBLASTER_H
+
+#include "theory/bv/bitblast/bitblaster.h"
+
+#include "base/tls.h"
+
+class Abc_Obj_t_;
+typedef Abc_Obj_t_ Abc_Obj_t;
+
+class Abc_Ntk_t_;
+typedef Abc_Ntk_t_ Abc_Ntk_t;
+
+class Abc_Aig_t_;
+typedef Abc_Aig_t_ Abc_Aig_t;
+
+class Cnf_Dat_t_;
+typedef Cnf_Dat_t_ Cnf_Dat_t;
+
+namespace CVC4 {
+namespace theory {
+namespace bv {
+
+class AigBitblaster : public TBitblaster<Abc_Obj_t*>
+{
+ public:
+  AigBitblaster();
+  ~AigBitblaster();
+
+  void makeVariable(TNode node, Bits& bits) override;
+  void bbTerm(TNode node, Bits& bits) override;
+  void bbAtom(TNode node) override;
+  Abc_Obj_t* bbFormula(TNode formula);
+  bool solve(TNode query);
+  static Abc_Aig_t* currentAigM();
+  static Abc_Ntk_t* currentAigNtk();
+
+ private:
+  typedef std::unordered_map<TNode, Abc_Obj_t*, TNodeHashFunction> TNodeAigMap;
+  typedef std::unordered_map<Node, Abc_Obj_t*, NodeHashFunction> NodeAigMap;
+
+  static CVC4_THREAD_LOCAL Abc_Ntk_t* s_abcAigNetwork;
+  std::unique_ptr<context::Context> d_nullContext;
+  std::unique_ptr<prop::SatSolver> d_satSolver;
+  TNodeAigMap d_aigCache;
+  NodeAigMap d_bbAtoms;
+
+  NodeAigMap d_nodeToAigInput;
+  // the thing we are checking for sat
+  Abc_Obj_t* d_aigOutputNode;
+
+  void addAtom(TNode atom);
+  void simplifyAig();
+  void storeBBAtom(TNode atom, Abc_Obj_t* atom_bb) override;
+  Abc_Obj_t* getBBAtom(TNode atom) const override;
+  bool hasBBAtom(TNode atom) const override;
+  void cacheAig(TNode node, Abc_Obj_t* aig);
+  bool hasAig(TNode node);
+  Abc_Obj_t* getAig(TNode node);
+  Abc_Obj_t* mkInput(TNode input);
+  bool hasInput(TNode input);
+  void convertToCnfAndAssert();
+  void assertToSatSolver(Cnf_Dat_t* pCnf);
+  Node getModelFromSatSolver(TNode a, bool fullModel) override
+  {
+    Unreachable();
+  }
+
+  class Statistics
+  {
+   public:
+    IntStat d_numClauses;
+    IntStat d_numVariables;
+    TimerStat d_simplificationTime;
+    TimerStat d_cnfConversionTime;
+    TimerStat d_solveTime;
+    Statistics();
+    ~Statistics();
+  };
+
+  Statistics d_statistics;
+};
+
+}  // namespace bv
+}  // namespace theory
+}  // namespace CVC4
+#endif  //  __CVC4__THEORY__BV__BITBLAST__AIG_BITBLASTER_H
diff --git a/src/theory/bv/bitblast_strategies_template.h b/src/theory/bv/bitblast/bitblast_strategies_template.h
index 60e7fc051..3c8b7bddc 100644
--- a/src/theory/bv/bitblast_strategies_template.h
+++ b/src/theory/bv/bitblast/bitblast_strategies_template.h
@@ -14,15 +14,16 @@
  ** Implementation of bitblasting functions for various operators. 
  **/
 
-#ifndef __CVC4__BITBLAST__STRATEGIES_TEMPLATE_H
-#define __CVC4__BITBLAST__STRATEGIES_TEMPLATE_H
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__BV__BITBLAST__BITBLAST_STRATEGIES_TEMPLATE_H
+#define __CVC4__THEORY__BV__BITBLAST__BITBLAST_STRATEGIES_TEMPLATE_H
 
 #include <cmath>
 #include <ostream>
 
-#include "cvc4_private.h"
 #include "expr/node.h"
-#include "theory/bv/bitblast_utils.h"
+#include "theory/bv/bitblast/bitblast_utils.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/rewriter.h"
 
diff --git a/src/theory/bv/bitblast_utils.h b/src/theory/bv/bitblast/bitblast_utils.h
index 1d6920007..a2991c529 100644
--- a/src/theory/bv/bitblast_utils.h
+++ b/src/theory/bv/bitblast/bitblast_utils.h
@@ -16,24 +16,14 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__BITBLAST__UTILS_H
-#define __CVC4__BITBLAST__UTILS_H
+#ifndef __CVC4__THEORY__BV__BITBLAST__BITBLAST_UTILS_H
+#define __CVC4__THEORY__BV__BITBLAST__BITBLAST_UTILS_H
 
 
 #include <ostream>
 #include "expr/node.h"
 
-#ifdef CVC4_USE_ABC
-#include "base/main/main.h"
-#include "base/abc/abc.h"
-
-extern "C" {
-#include "sat/cnf/cnf.h"
-}
-#endif
-
 namespace CVC4 {
-
 namespace theory {
 namespace bv {
 
@@ -275,9 +265,8 @@ T inline sLessThanBB(const std::vector<T>&a, const std::vector<T>& b, bool orEqu
   return res;
 }
 
+}  // namespace bv
+}  // namespace theory
+}  // namespace CVC4
 
-}
-}
-}
-
-#endif
+#endif  // __CVC4__THEORY__BV__BITBLAST__BITBLAST_UTILS_H
diff --git a/src/theory/bv/bitblast/bitblaster.h b/src/theory/bv/bitblast/bitblaster.h
new file mode 100644
index 000000000..f9c444b45
--- /dev/null
+++ b/src/theory/bv/bitblast/bitblaster.h
@@ -0,0 +1,261 @@
+/*********************                                                        */
+/*! \file bitblaster.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Liana Hadarean, Tim King, Clark Barrett
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 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 Wrapper around the SAT solver used for bitblasting
+ **
+ ** Wrapper around the SAT solver used for bitblasting.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__BV__BITBLAST__BITBLASTER_H
+#define __CVC4__THEORY__BV__BITBLAST__BITBLASTER_H
+
+#include <unordered_map>
+#include <unordered_set>
+#include <vector>
+
+#include "expr/node.h"
+#include "prop/sat_solver.h"
+#include "theory/bv/bitblast/bitblast_strategies_template.h"
+#include "theory/theory_registrar.h"
+#include "theory/valuation.h"
+#include "util/resource_manager.h"
+
+namespace CVC4 {
+namespace theory {
+namespace bv {
+
+typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
+typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
+
+/**
+ * The Bitblaster that manages the mapping between Nodes
+ * and their bitwise definition
+ *
+ */
+
+template <class T>
+class TBitblaster
+{
+ protected:
+  typedef std::vector<T> Bits;
+  typedef std::unordered_map<Node, Bits, NodeHashFunction> TermDefMap;
+  typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
+  typedef std::unordered_map<Node, Node, NodeHashFunction> ModelCache;
+
+  typedef void (*TermBBStrategy)(TNode, Bits&, TBitblaster<T>*);
+  typedef T (*AtomBBStrategy)(TNode, TBitblaster<T>*);
+
+  // caches and mappings
+  TermDefMap d_termCache;
+  ModelCache d_modelCache;
+
+  BitVectorProof* d_bvp;
+
+  void initAtomBBStrategies();
+  void initTermBBStrategies();
+
+ protected:
+  /// function tables for the various bitblasting strategies indexed by node
+  /// kind
+  TermBBStrategy d_termBBStrategies[kind::LAST_KIND];
+  AtomBBStrategy d_atomBBStrategies[kind::LAST_KIND];
+  virtual Node getModelFromSatSolver(TNode node, bool fullModel) = 0;
+
+ public:
+  TBitblaster();
+  virtual ~TBitblaster() {}
+  virtual void bbAtom(TNode node) = 0;
+  virtual void bbTerm(TNode node, Bits& bits) = 0;
+  virtual void makeVariable(TNode node, Bits& bits) = 0;
+  virtual T getBBAtom(TNode atom) const = 0;
+  virtual bool hasBBAtom(TNode atom) const = 0;
+  virtual void storeBBAtom(TNode atom, T atom_bb) = 0;
+
+  bool hasBBTerm(TNode node) const;
+  void getBBTerm(TNode node, Bits& bits) const;
+  virtual void storeBBTerm(TNode term, const Bits& bits);
+  /**
+   * Return a constant representing the value of a in the  model.
+   * If fullModel is true set unconstrained bits to 0. If not return
+   * NullNode() for a fully or partially unconstrained.
+   *
+   */
+  Node getTermModel(TNode node, bool fullModel);
+  void invalidateModelCache();
+};
+
+class MinisatEmptyNotify : public prop::BVSatSolverInterface::Notify
+{
+ public:
+  MinisatEmptyNotify() {}
+  bool notify(prop::SatLiteral lit) override { return true; }
+  void notify(prop::SatClause& clause) override {}
+  void spendResource(unsigned amount) override
+  {
+    NodeManager::currentResourceManager()->spendResource(amount);
+  }
+  void safePoint(unsigned amount) override {}
+};
+
+// Bitblaster implementation
+
+template <class T>
+void TBitblaster<T>::initAtomBBStrategies()
+{
+  for (int i = 0; i < kind::LAST_KIND; ++i)
+  {
+    d_atomBBStrategies[i] = UndefinedAtomBBStrategy<T>;
+  }
+  /// setting default bb strategies for atoms
+  d_atomBBStrategies[kind::EQUAL] = DefaultEqBB<T>;
+  d_atomBBStrategies[kind::BITVECTOR_ULT] = DefaultUltBB<T>;
+  d_atomBBStrategies[kind::BITVECTOR_ULE] = DefaultUleBB<T>;
+  d_atomBBStrategies[kind::BITVECTOR_UGT] = DefaultUgtBB<T>;
+  d_atomBBStrategies[kind::BITVECTOR_UGE] = DefaultUgeBB<T>;
+  d_atomBBStrategies[kind::BITVECTOR_SLT] = DefaultSltBB<T>;
+  d_atomBBStrategies[kind::BITVECTOR_SLE] = DefaultSleBB<T>;
+  d_atomBBStrategies[kind::BITVECTOR_SGT] = DefaultSgtBB<T>;
+  d_atomBBStrategies[kind::BITVECTOR_SGE] = DefaultSgeBB<T>;
+}
+
+template <class T>
+void TBitblaster<T>::initTermBBStrategies()
+{
+  for (int i = 0; i < kind::LAST_KIND; ++i)
+  {
+    d_termBBStrategies[i] = DefaultVarBB<T>;
+  }
+  /// setting default bb strategies for terms:
+  d_termBBStrategies[kind::CONST_BITVECTOR] = DefaultConstBB<T>;
+  d_termBBStrategies[kind::BITVECTOR_NOT] = DefaultNotBB<T>;
+  d_termBBStrategies[kind::BITVECTOR_CONCAT] = DefaultConcatBB<T>;
+  d_termBBStrategies[kind::BITVECTOR_AND] = DefaultAndBB<T>;
+  d_termBBStrategies[kind::BITVECTOR_OR] = DefaultOrBB<T>;
+  d_termBBStrategies[kind::BITVECTOR_XOR] = DefaultXorBB<T>;
+  d_termBBStrategies[kind::BITVECTOR_XNOR] = DefaultXnorBB<T>;
+  d_termBBStrategies[kind::BITVECTOR_NAND] = DefaultNandBB<T>;
+  d_termBBStrategies[kind::BITVECTOR_NOR] = DefaultNorBB<T>;
+  d_termBBStrategies[kind::BITVECTOR_COMP] = DefaultCompBB<T>;
+  d_termBBStrategies[kind::BITVECTOR_MULT] = DefaultMultBB<T>;
+  d_termBBStrategies[kind::BITVECTOR_PLUS] = DefaultPlusBB<T>;
+  d_termBBStrategies[kind::BITVECTOR_SUB] = DefaultSubBB<T>;
+  d_termBBStrategies[kind::BITVECTOR_NEG] = DefaultNegBB<T>;
+  d_termBBStrategies[kind::BITVECTOR_UDIV] = UndefinedTermBBStrategy<T>;
+  d_termBBStrategies[kind::BITVECTOR_UREM] = UndefinedTermBBStrategy<T>;
+  d_termBBStrategies[kind::BITVECTOR_UDIV_TOTAL] = DefaultUdivBB<T>;
+  d_termBBStrategies[kind::BITVECTOR_UREM_TOTAL] = DefaultUremBB<T>;
+  d_termBBStrategies[kind::BITVECTOR_SDIV] = UndefinedTermBBStrategy<T>;
+  d_termBBStrategies[kind::BITVECTOR_SREM] = UndefinedTermBBStrategy<T>;
+  d_termBBStrategies[kind::BITVECTOR_SMOD] = UndefinedTermBBStrategy<T>;
+  d_termBBStrategies[kind::BITVECTOR_SHL] = DefaultShlBB<T>;
+  d_termBBStrategies[kind::BITVECTOR_LSHR] = DefaultLshrBB<T>;
+  d_termBBStrategies[kind::BITVECTOR_ASHR] = DefaultAshrBB<T>;
+  d_termBBStrategies[kind::BITVECTOR_ULTBV] = DefaultUltbvBB<T>;
+  d_termBBStrategies[kind::BITVECTOR_SLTBV] = DefaultSltbvBB<T>;
+  d_termBBStrategies[kind::BITVECTOR_ITE] = DefaultIteBB<T>;
+  d_termBBStrategies[kind::BITVECTOR_EXTRACT] = DefaultExtractBB<T>;
+  d_termBBStrategies[kind::BITVECTOR_REPEAT] = DefaultRepeatBB<T>;
+  d_termBBStrategies[kind::BITVECTOR_ZERO_EXTEND] = DefaultZeroExtendBB<T>;
+  d_termBBStrategies[kind::BITVECTOR_SIGN_EXTEND] = DefaultSignExtendBB<T>;
+  d_termBBStrategies[kind::BITVECTOR_ROTATE_RIGHT] = DefaultRotateRightBB<T>;
+  d_termBBStrategies[kind::BITVECTOR_ROTATE_LEFT] = DefaultRotateLeftBB<T>;
+}
+
+template <class T>
+TBitblaster<T>::TBitblaster() : d_termCache(), d_modelCache(), d_bvp(NULL)
+{
+  initAtomBBStrategies();
+  initTermBBStrategies();
+}
+
+template <class T>
+bool TBitblaster<T>::hasBBTerm(TNode node) const
+{
+  return d_termCache.find(node) != d_termCache.end();
+}
+template <class T>
+void TBitblaster<T>::getBBTerm(TNode node, Bits& bits) const
+{
+  Assert(hasBBTerm(node));
+  bits = d_termCache.find(node)->second;
+}
+
+template <class T>
+void TBitblaster<T>::storeBBTerm(TNode node, const Bits& bits)
+{
+  d_termCache.insert(std::make_pair(node, bits));
+}
+
+template <class T>
+void TBitblaster<T>::invalidateModelCache()
+{
+  d_modelCache.clear();
+}
+
+template <class T>
+Node TBitblaster<T>::getTermModel(TNode node, bool fullModel)
+{
+  if (d_modelCache.find(node) != d_modelCache.end()) return d_modelCache[node];
+
+  if (node.isConst()) return node;
+
+  Node value = getModelFromSatSolver(node, false);
+  if (!value.isNull())
+  {
+    Debug("bv-equality-status")
+        << "TLazyBitblaster::getTermModel from SatSolver" << node << " => "
+        << value << "\n";
+    d_modelCache[node] = value;
+    Assert(value.isConst());
+    return value;
+  }
+
+  if (Theory::isLeafOf(node, theory::THEORY_BV))
+  {
+    // if it is a leaf may ask for fullModel
+    value = getModelFromSatSolver(node, true);
+    Debug("bv-equality-status") << "TLazyBitblaster::getTermModel from VarValue"
+                                << node << " => " << value << "\n";
+    Assert((fullModel && !value.isNull() && value.isConst()) || !fullModel);
+    if (!value.isNull())
+    {
+      d_modelCache[node] = value;
+    }
+    return value;
+  }
+  Assert(node.getType().isBitVector());
+
+  NodeBuilder<> nb(node.getKind());
+  if (node.getMetaKind() == kind::metakind::PARAMETERIZED)
+  {
+    nb << node.getOperator();
+  }
+
+  for (unsigned i = 0; i < node.getNumChildren(); ++i)
+  {
+    nb << getTermModel(node[i], fullModel);
+  }
+  value = nb;
+  value = Rewriter::rewrite(value);
+  Assert(value.isConst());
+  d_modelCache[node] = value;
+  Debug("bv-term-model") << "TLazyBitblaster::getTermModel Building Value"
+                         << node << " => " << value << "\n";
+  return value;
+}
+
+}  // namespace bv
+}  // namespace theory
+}  // namespace CVC4
+
+#endif /* __CVC4__THEORY__BV__BITBLAST__BITBLASTER_H */
diff --git a/src/theory/bv/eager_bitblaster.cpp b/src/theory/bv/bitblast/eager_bitblaster.cpp
index 25610af2b..d49c1f432 100644
--- a/src/theory/bv/eager_bitblaster.cpp
+++ b/src/theory/bv/bitblast/eager_bitblaster.cpp
@@ -16,12 +16,13 @@
 
 #include "cvc4_private.h"
 
+#include "theory/bv/bitblast/eager_bitblaster.h"
+
 #include "options/bv_options.h"
 #include "proof/bitvector_proof.h"
 #include "prop/cnf_stream.h"
 #include "prop/sat_solver_factory.h"
 #include "smt/smt_statistics_registry.h"
-#include "theory/bv/bitblaster_template.h"
 #include "theory/bv/theory_bv.h"
 #include "theory/theory_model.h"
 
@@ -29,58 +30,50 @@ namespace CVC4 {
 namespace theory {
 namespace bv {
 
-void BitblastingRegistrar::preRegister(Node n) { d_bitblaster->bbAtom(n); }
-
 EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv)
     : TBitblaster<Node>(),
-      d_satSolver(NULL),
-      d_bitblastingRegistrar(NULL),
-      d_nullContext(NULL),
-      d_cnfStream(NULL),
+      d_satSolver(),
+      d_bitblastingRegistrar(new BitblastingRegistrar(this)),
+      d_nullContext(new context::Context()),
+      d_cnfStream(),
       d_bv(theory_bv),
       d_bbAtoms(),
       d_variables(),
-      d_notify(NULL) {
-  d_bitblastingRegistrar = new BitblastingRegistrar(this);
-  d_nullContext = new context::Context();
-
+      d_notify()
+{
+  prop::SatSolver *solver = nullptr;
   switch (options::bvSatSolver())
   {
     case SAT_SOLVER_MINISAT:
     {
       prop::BVSatSolverInterface* minisat =
           prop::SatSolverFactory::createMinisat(
-              d_nullContext, smtStatisticsRegistry(), "EagerBitblaster");
-      d_notify = new MinisatEmptyNotify();
-      minisat->setNotify(d_notify);
-      d_satSolver = minisat;
+              d_nullContext.get(), smtStatisticsRegistry(), "EagerBitblaster");
+      d_notify.reset(new MinisatEmptyNotify());
+      minisat->setNotify(d_notify.get());
+      solver = minisat;
       break;
     }
     case SAT_SOLVER_CADICAL:
-      d_satSolver = prop::SatSolverFactory::createCadical(
-          smtStatisticsRegistry(), "EagerBitblaster");
+      solver = prop::SatSolverFactory::createCadical(smtStatisticsRegistry(),
+                                                     "EagerBitblaster");
       break;
     case SAT_SOLVER_CRYPTOMINISAT:
-      d_satSolver = prop::SatSolverFactory::createCryptoMinisat(
+      solver = prop::SatSolverFactory::createCryptoMinisat(
           smtStatisticsRegistry(), "EagerBitblaster");
       break;
     default: Unreachable("Unknown SAT solver type");
   }
-
-  d_cnfStream = new prop::TseitinCnfStream(d_satSolver, d_bitblastingRegistrar,
-                                           d_nullContext, options::proof(),
-                                           "EagerBitblaster");
-
-  d_bvp = NULL;
+  d_satSolver.reset(solver);
+  d_cnfStream.reset(
+      new prop::TseitinCnfStream(d_satSolver.get(),
+                                 d_bitblastingRegistrar.get(),
+                                 d_nullContext.get(),
+                                 options::proof(),
+                                 "EagerBitblaster"));
 }
 
-EagerBitblaster::~EagerBitblaster() {
-  delete d_cnfStream;
-  delete d_satSolver;
-  delete d_notify;
-  delete d_nullContext;
-  delete d_bitblastingRegistrar;
-}
+EagerBitblaster::~EagerBitblaster() {}
 
 void EagerBitblaster::bbFormula(TNode node) {
   d_cnfStream->convertAndAssert(node, false, false, RULE_INVALID,
@@ -257,13 +250,14 @@ bool EagerBitblaster::collectModelInfo(TheoryModel* m, bool fullModel)
 void EagerBitblaster::setProofLog(BitVectorProof* bvp) {
   d_bvp = bvp;
   d_satSolver->setProofLog(bvp);
-  bvp->initCnfProof(d_cnfStream, d_nullContext);
+  bvp->initCnfProof(d_cnfStream.get(), d_nullContext.get());
 }
 
 bool EagerBitblaster::isSharedTerm(TNode node) {
   return d_bv->d_sharedTermsSet.find(node) != d_bv->d_sharedTermsSet.end();
 }
 
-} /* namespace CVC4::theory::bv; */
-} /* namespace CVC4::theory; */
-} /* namespace CVC4; */
+
+}  // namespace bv
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/bv/bitblast/eager_bitblaster.h b/src/theory/bv/bitblast/eager_bitblaster.h
new file mode 100644
index 000000000..8610d0181
--- /dev/null
+++ b/src/theory/bv/bitblast/eager_bitblaster.h
@@ -0,0 +1,89 @@
+/*********************                                                        */
+/*! \file eager_bitblaster.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Liana Hadarean, Tim King, Aina Niemetz
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 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 Bitblaster for eager BV solver.
+ **
+ ** Bitblaster for the eager BV solver.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__BV__BITBLAST__EAGER_BITBLASTER_H
+#define __CVC4__THEORY__BV__BITBLAST__EAGER_BITBLASTER_H
+
+#include <unordered_set>
+
+#include "theory/bv/bitblast/bitblaster.h"
+
+#include "prop/cnf_stream.h"
+#include "prop/sat_solver.h"
+
+namespace CVC4 {
+namespace theory {
+namespace bv {
+
+class BitblastingRegistrar;
+class TheoryBV;
+
+class EagerBitblaster : public TBitblaster<Node>
+{
+ public:
+  EagerBitblaster(TheoryBV* theory_bv);
+  ~EagerBitblaster();
+
+  void addAtom(TNode atom);
+  void makeVariable(TNode node, Bits& bits) override;
+  void bbTerm(TNode node, Bits& bits) override;
+  void bbAtom(TNode node) override;
+  Node getBBAtom(TNode node) const override;
+  bool hasBBAtom(TNode atom) const override;
+  void bbFormula(TNode formula);
+  void storeBBAtom(TNode atom, Node atom_bb) override;
+  void storeBBTerm(TNode node, const Bits& bits) override;
+
+  bool assertToSat(TNode node, bool propagate = true);
+  bool solve();
+  bool collectModelInfo(TheoryModel* m, bool fullModel);
+  void setProofLog(BitVectorProof* bvp);
+
+ private:
+  typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
+  // sat solver used for bitblasting and associated CnfStream
+  std::unique_ptr<prop::SatSolver> d_satSolver;
+  std::unique_ptr<BitblastingRegistrar> d_bitblastingRegistrar;
+  std::unique_ptr<context::Context> d_nullContext;
+  std::unique_ptr<prop::CnfStream> d_cnfStream;
+
+  TheoryBV* d_bv;
+  TNodeSet d_bbAtoms;
+  TNodeSet d_variables;
+
+  // This is either an MinisatEmptyNotify or NULL.
+  std::unique_ptr<MinisatEmptyNotify> d_notify;
+
+  Node getModelFromSatSolver(TNode a, bool fullModel) override;
+  bool isSharedTerm(TNode node);
+};
+
+class BitblastingRegistrar : public prop::Registrar
+{
+ public:
+  BitblastingRegistrar(EagerBitblaster* bb) : d_bitblaster(bb) {}
+  void preRegister(Node n) override { d_bitblaster->bbAtom(n); }
+
+ private:
+  EagerBitblaster* d_bitblaster;
+};
+
+}  // namespace bv
+}  // namespace theory
+}  // namespace CVC4
+#endif  //  __CVC4__THEORY__BV__BITBLAST__EAGER_BITBLASTER_H
diff --git a/src/theory/bv/lazy_bitblaster.cpp b/src/theory/bv/bitblast/lazy_bitblaster.cpp
index 189898c0c..539d40384 100644
--- a/src/theory/bv/lazy_bitblaster.cpp
+++ b/src/theory/bv/bitblast/lazy_bitblaster.cpp
@@ -14,8 +14,10 @@
  ** Bitblaster for the lazy bv solver.
  **/
 
-#include "bitblaster_template.h"
 #include "cvc4_private.h"
+
+#include "theory/bv/bitblast/lazy_bitblaster.h"
+
 #include "options/bv_options.h"
 #include "prop/cnf_stream.h"
 #include "prop/sat_solver.h"
@@ -57,38 +59,42 @@ uint64_t numNodes(TNode node, utils::NodeSet& seen)
 }
 }
 
+TLazyBitblaster::TLazyBitblaster(context::Context* c,
+                                 bv::TheoryBV* bv,
+                                 const std::string name,
+                                 bool emptyNotify)
+    : TBitblaster<Node>(),
+      d_bv(bv),
+      d_ctx(c),
+      d_nullRegistrar(new prop::NullRegistrar()),
+      d_nullContext(new context::Context()),
+      d_assertedAtoms(new (true) context::CDList<prop::SatLiteral>(c)),
+      d_explanations(new (true) ExplanationMap(c)),
+      d_variables(),
+      d_bbAtoms(),
+      d_abstraction(NULL),
+      d_emptyNotify(emptyNotify),
+      d_fullModelAssertionLevel(c, 0),
+      d_name(name),
+      d_statistics(name)
+{
+  d_satSolver.reset(
+      prop::SatSolverFactory::createMinisat(c, smtStatisticsRegistry(), name));
 
-TLazyBitblaster::TLazyBitblaster(context::Context* c, bv::TheoryBV* bv,
-                                 const std::string name, bool emptyNotify)
-  : TBitblaster<Node>()
-  , d_bv(bv)
-  , d_ctx(c)
-  , d_assertedAtoms(new(true) context::CDList<prop::SatLiteral>(c))
-  , d_explanations(new(true) ExplanationMap(c))
-  , d_variables()
-  , d_bbAtoms()
-  , d_abstraction(NULL)
-  , d_emptyNotify(emptyNotify)
-  , d_fullModelAssertionLevel(c, 0)
-  , d_name(name)
-  , d_statistics(name) {
-
-  d_satSolver = prop::SatSolverFactory::createMinisat(
-      c, smtStatisticsRegistry(), name);
-  d_nullRegistrar = new prop::NullRegistrar();
-  d_nullContext = new context::Context();
-  d_cnfStream = new prop::TseitinCnfStream(d_satSolver,
-                                           d_nullRegistrar,
-                                           d_nullContext,
-                                           options::proof(),
-                                           "LazyBitblaster");
+  d_cnfStream.reset(
+      new prop::TseitinCnfStream(d_satSolver.get(),
+                                 d_nullRegistrar.get(),
+                                 d_nullContext.get(),
+                                 options::proof(),
+                                 "LazyBitblaster"));
 
-  d_satSolverNotify = d_emptyNotify ?
-    (prop::BVSatSolverInterface::Notify*) new MinisatEmptyNotify() :
-    (prop::BVSatSolverInterface::Notify*) new MinisatNotify(d_cnfStream, bv,
-                                                            this);
+  d_satSolverNotify.reset(
+      d_emptyNotify
+          ? (prop::BVSatSolverInterface::Notify*)new MinisatEmptyNotify()
+          : (prop::BVSatSolverInterface::Notify*)new MinisatNotify(
+                d_cnfStream.get(), bv, this));
 
-  d_satSolver->setNotify(d_satSolverNotify);
+  d_satSolver->setNotify(d_satSolverNotify.get());
 }
 
 void TLazyBitblaster::setAbstraction(AbstractionModule* abs) {
@@ -97,11 +103,6 @@ void TLazyBitblaster::setAbstraction(AbstractionModule* abs) {
 
 TLazyBitblaster::~TLazyBitblaster()
 {
-  delete d_cnfStream;
-  delete d_nullRegistrar;
-  delete d_nullContext;
-  delete d_satSolver;
-  delete d_satSolverNotify;
   d_assertedAtoms->deleteSelf();
   d_explanations->deleteSelf();
 }
@@ -568,14 +569,11 @@ bool TLazyBitblaster::collectModelInfo(TheoryModel* m, bool fullModel)
 void TLazyBitblaster::setProofLog( BitVectorProof * bvp ){
   d_bvp = bvp;
   d_satSolver->setProofLog( bvp );
-  bvp->initCnfProof(d_cnfStream, d_nullContext);
+  bvp->initCnfProof(d_cnfStream.get(), d_nullContext.get());
 }
 
 void TLazyBitblaster::clearSolver() {
   Assert (d_ctx->getLevel() == 0);
-  delete d_satSolver;
-  delete d_satSolverNotify;
-  delete d_cnfStream;
   d_assertedAtoms->deleteSelf();
   d_assertedAtoms = new(true) context::CDList<prop::SatLiteral>(d_ctx);
   d_explanations->deleteSelf();
@@ -586,18 +584,18 @@ void TLazyBitblaster::clearSolver() {
 
   invalidateModelCache();
   // recreate sat solver
-  d_satSolver = prop::SatSolverFactory::createMinisat(
-      d_ctx, smtStatisticsRegistry());
-  d_cnfStream = new prop::TseitinCnfStream(d_satSolver, d_nullRegistrar,
-                                           d_nullContext);
-
-  d_satSolverNotify = d_emptyNotify ?
-    (prop::BVSatSolverInterface::Notify*) new MinisatEmptyNotify() :
-    (prop::BVSatSolverInterface::Notify*) new MinisatNotify(d_cnfStream, d_bv,
-                                                            this);
-  d_satSolver->setNotify(d_satSolverNotify);
-}
-
-} /* namespace CVC4::theory::bv */
-} /* namespace CVC4::theory */
-} /* namespace CVC4 */
+  d_satSolver.reset(
+      prop::SatSolverFactory::createMinisat(d_ctx, smtStatisticsRegistry()));
+  d_cnfStream.reset(new prop::TseitinCnfStream(
+      d_satSolver.get(), d_nullRegistrar.get(), d_nullContext.get()));
+  d_satSolverNotify.reset(
+      d_emptyNotify
+          ? (prop::BVSatSolverInterface::Notify*)new MinisatEmptyNotify()
+          : (prop::BVSatSolverInterface::Notify*)new MinisatNotify(
+                d_cnfStream.get(), d_bv, this));
+  d_satSolver->setNotify(d_satSolverNotify.get());
+}
+
+}  // namespace bv
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/bv/bitblast/lazy_bitblaster.h b/src/theory/bv/bitblast/lazy_bitblaster.h
new file mode 100644
index 000000000..97fef1e50
--- /dev/null
+++ b/src/theory/bv/bitblast/lazy_bitblaster.h
@@ -0,0 +1,181 @@
+/*********************                                                        */
+/*! \file lazy_bitblaster.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Liana Hadarean, Tim King, Aina Niemetz
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 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 Bitblaster for the lazy bv solver.
+ **
+ ** Bitblaster for the lazy bv solver.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__BV__BITBLAST__LAZY_BITBLASTER_H
+#define __CVC4__THEORY__BV__BITBLAST__LAZY_BITBLASTER_H
+
+#include "theory/bv/bitblast/bitblaster.h"
+
+#include "context/cdhashmap.h"
+#include "context/cdlist.h"
+#include "prop/cnf_stream.h"
+#include "prop/registrar.h"
+#include "prop/sat_solver.h"
+#include "theory/bv/abstraction.h"
+
+namespace CVC4 {
+namespace theory {
+namespace bv {
+
+class TheoryBV;
+
+class TLazyBitblaster : public TBitblaster<Node>
+{
+ public:
+  void bbTerm(TNode node, Bits& bits) override;
+  void bbAtom(TNode node) override;
+  Node getBBAtom(TNode atom) const override;
+  void storeBBAtom(TNode atom, Node atom_bb) override;
+  void storeBBTerm(TNode node, const Bits& bits) override;
+  bool hasBBAtom(TNode atom) const override;
+
+  TLazyBitblaster(context::Context* c,
+                  TheoryBV* bv,
+                  const std::string name = "",
+                  bool emptyNotify = false);
+  ~TLazyBitblaster();
+  /**
+   * Pushes the assumption literal associated with node to the SAT
+   * solver assumption queue.
+   *
+   * @param node assumption
+   * @param propagate run bcp or not
+   *
+   * @return false if a conflict detected
+   */
+  bool assertToSat(TNode node, bool propagate = true);
+  bool propagate();
+  bool solve();
+  prop::SatValue solveWithBudget(unsigned long conflict_budget);
+  void getConflict(std::vector<TNode>& conflict);
+  void explain(TNode atom, std::vector<TNode>& explanation);
+  void setAbstraction(AbstractionModule* abs);
+
+  theory::EqualityStatus getEqualityStatus(TNode a, TNode b);
+
+  /**
+   * Adds a constant value for each bit-blasted variable in the model.
+   *
+   * @param m the model
+   * @param fullModel whether to create a "full model," i.e., add
+   * constants to equivalence classes that don't already have them
+   */
+  bool collectModelInfo(TheoryModel* m, bool fullModel);
+  void setProofLog(BitVectorProof* bvp);
+
+  typedef TNodeSet::const_iterator vars_iterator;
+  vars_iterator beginVars() { return d_variables.begin(); }
+  vars_iterator endVars() { return d_variables.end(); }
+
+  /**
+   * Creates the bits corresponding to the variable (or non-bv term).
+   *
+   * @param var
+   */
+  void makeVariable(TNode var, Bits& bits) override;
+
+  bool isSharedTerm(TNode node);
+  uint64_t computeAtomWeight(TNode node, NodeSet& seen);
+  /**
+   * Deletes SatSolver and CnfCache, but maintains bit-blasting
+   * terms cache.
+   *
+   */
+  void clearSolver();
+
+ private:
+  typedef std::vector<Node> Bits;
+  typedef context::CDList<prop::SatLiteral> AssertionList;
+  typedef context::CDHashMap<prop::SatLiteral,
+                             std::vector<prop::SatLiteral>,
+                             prop::SatLiteralHashFunction>
+      ExplanationMap;
+  /** This class gets callbacks from minisat on propagations */
+  class MinisatNotify : public prop::BVSatSolverInterface::Notify
+  {
+    prop::CnfStream* d_cnf;
+    TheoryBV* d_bv;
+    TLazyBitblaster* d_lazyBB;
+
+   public:
+    MinisatNotify(prop::CnfStream* cnf, TheoryBV* bv, TLazyBitblaster* lbv)
+        : d_cnf(cnf), d_bv(bv), d_lazyBB(lbv)
+    {
+    }
+
+    bool notify(prop::SatLiteral lit) override;
+    void notify(prop::SatClause& clause) override;
+    void spendResource(unsigned amount) override;
+    void safePoint(unsigned amount) override;
+  };
+
+  TheoryBV* d_bv;
+  context::Context* d_ctx;
+
+  std::unique_ptr<prop::NullRegistrar> d_nullRegistrar;
+  std::unique_ptr<context::Context> d_nullContext;
+  // sat solver used for bitblasting and associated CnfStream
+  std::unique_ptr<prop::BVSatSolverInterface> d_satSolver;
+  std::unique_ptr<prop::BVSatSolverInterface::Notify> d_satSolverNotify;
+  std::unique_ptr<prop::CnfStream> d_cnfStream;
+
+  AssertionList*
+      d_assertedAtoms;            /**< context dependent list storing the atoms
+                                     currently asserted by the DPLL SAT solver. */
+  ExplanationMap* d_explanations; /**< context dependent list of explanations
+                                    for the propagated literals. Only used when
+                                    bvEagerPropagate option enabled. */
+  TNodeSet d_variables;
+  TNodeSet d_bbAtoms;
+  AbstractionModule* d_abstraction;
+  bool d_emptyNotify;
+
+  // The size of the fact queue when we most recently called solve() in the
+  // bit-vector SAT solver. This is the level at which we should have
+  // a full model in the bv SAT solver.
+  context::CDO<int> d_fullModelAssertionLevel;
+
+  void addAtom(TNode atom);
+  bool hasValue(TNode a);
+  Node getModelFromSatSolver(TNode a, bool fullModel) override;
+
+  class Statistics
+  {
+   public:
+    IntStat d_numTermClauses, d_numAtomClauses;
+    IntStat d_numTerms, d_numAtoms;
+    IntStat d_numExplainedPropagations;
+    IntStat d_numBitblastingPropagations;
+    TimerStat d_bitblastTimer;
+    Statistics(const std::string& name);
+    ~Statistics();
+  };
+  std::string d_name;
+
+ // NOTE: d_statistics is public since d_bitblastTimer needs to be initalized
+ //       prior to calling bbAtom. As it is now, the timer can't be initialized
+ //       in bbAtom since the method is called recursively and the timer would
+ //       be initialized multiple times, which is not allowed.
+ public:
+  Statistics d_statistics;
+};
+
+}  // namespace bv
+}  // namespace theory
+}  // namespace CVC4
+#endif  //  __CVC4__THEORY__BV__BITBLAST__LAZY_BITBLASTER_H
diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h
deleted file mode 100644
index 3bb701fdf..000000000
--- a/src/theory/bv/bitblaster_template.h
+++ /dev/null
@@ -1,508 +0,0 @@
-/*********************                                                        */
-/*! \file bitblaster_template.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Liana Hadarean, Tim King, Clark Barrett
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 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 Wrapper around the SAT solver used for bitblasting
- **
- ** Wrapper around the SAT solver used for bitblasting.
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__BITBLASTER_TEMPLATE_H
-#define __CVC4__BITBLASTER_TEMPLATE_H
-
-#include <unordered_map>
-#include <unordered_set>
-#include <vector>
-
-#include "bitblast_strategies_template.h"
-#include "context/cdhashmap.h"
-#include "expr/node.h"
-#include "prop/sat_solver.h"
-#include "theory/theory_registrar.h"
-#include "theory/valuation.h"
-#include "util/resource_manager.h"
-
-class Abc_Obj_t_;
-typedef Abc_Obj_t_ Abc_Obj_t;
-
-class Abc_Ntk_t_;
-typedef Abc_Ntk_t_ Abc_Ntk_t;
-
-class Abc_Aig_t_;
-typedef Abc_Aig_t_ Abc_Aig_t;
-
-class Cnf_Dat_t_;
-typedef Cnf_Dat_t_ Cnf_Dat_t;
-
-
-namespace CVC4 {
-namespace prop {
-class CnfStream;
-class BVSatSolverInterface;
-class NullRegistrar;
-}
-
-namespace theory {
-class OutputChannel;
-class TheoryModel;
-
-namespace bv {
-
-class BitblastingRegistrar;
-
-typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
-typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
-
-class AbstractionModule;
-
-/**
- * The Bitblaster that manages the mapping between Nodes
- * and their bitwise definition
- *
- */
-
-template <class T>
-class TBitblaster {
-protected:
-  typedef std::vector<T> Bits;
-  typedef std::unordered_map <Node, Bits, NodeHashFunction>  TermDefMap;
-  typedef std::unordered_set<TNode, TNodeHashFunction>       TNodeSet;
-  typedef std::unordered_map<Node, Node, NodeHashFunction>   ModelCache;
-
-  typedef void  (*TermBBStrategy) (TNode, Bits&, TBitblaster<T>*);
-  typedef T     (*AtomBBStrategy) (TNode, TBitblaster<T>*);
-
-  // caches and mappings
-  TermDefMap d_termCache;
-  ModelCache d_modelCache;
-
-  BitVectorProof * d_bvp;
-
-  void initAtomBBStrategies();
-  void initTermBBStrategies();
-protected:
-  /// function tables for the various bitblasting strategies indexed by node kind
-  TermBBStrategy d_termBBStrategies[kind::LAST_KIND];
-  AtomBBStrategy d_atomBBStrategies[kind::LAST_KIND];
-  virtual Node getModelFromSatSolver(TNode node, bool fullModel) = 0;
-public:
-  TBitblaster();
-  virtual ~TBitblaster() {}
-  virtual void bbAtom(TNode node) = 0;
-  virtual void bbTerm(TNode node, Bits&  bits) = 0;
-  virtual void makeVariable(TNode node, Bits& bits) = 0;
-  virtual T getBBAtom(TNode atom) const = 0;
-  virtual bool hasBBAtom(TNode atom) const = 0;
-  virtual void storeBBAtom(TNode atom, T atom_bb) = 0;
-
-
-  bool hasBBTerm(TNode node) const;
-  void getBBTerm(TNode node, Bits& bits) const;
-  virtual void storeBBTerm(TNode term, const Bits& bits);
-  /**
-   * Return a constant representing the value of a in the  model.
-   * If fullModel is true set unconstrained bits to 0. If not return
-   * NullNode() for a fully or partially unconstrained.
-   *
-   */
-  Node getTermModel(TNode node, bool fullModel);
-  void invalidateModelCache();
-};
-
-
-class TheoryBV;
-
-class TLazyBitblaster :  public TBitblaster<Node> {
-  typedef std::vector<Node> Bits;
-  typedef context::CDList<prop::SatLiteral> AssertionList;
-  typedef context::CDHashMap<prop::SatLiteral, std::vector<prop::SatLiteral> , prop::SatLiteralHashFunction> ExplanationMap;
-  /** This class gets callbacks from minisat on propagations */
-  class MinisatNotify : public prop::BVSatSolverInterface::Notify {
-    prop::CnfStream* d_cnf;
-    TheoryBV *d_bv;
-    TLazyBitblaster* d_lazyBB;
-  public:
-    MinisatNotify(prop::CnfStream* cnf, TheoryBV *bv, TLazyBitblaster* lbv)
-    : d_cnf(cnf)
-    , d_bv(bv)
-    , d_lazyBB(lbv)
-    {}
-
-    bool notify(prop::SatLiteral lit) override;
-    void notify(prop::SatClause& clause) override;
-    void spendResource(unsigned amount) override;
-    void safePoint(unsigned amount) override;
-  };
-
-  TheoryBV *d_bv;
-  context::Context* d_ctx;
-
-  prop::NullRegistrar* d_nullRegistrar;
-  context::Context* d_nullContext;
-  // sat solver used for bitblasting and associated CnfStream
-  prop::BVSatSolverInterface*         d_satSolver;
-  prop::BVSatSolverInterface::Notify* d_satSolverNotify;
-  prop::CnfStream*                    d_cnfStream;
-
-  AssertionList* d_assertedAtoms; /**< context dependent list storing the atoms
-                                     currently asserted by the DPLL SAT solver. */
-  ExplanationMap* d_explanations; /**< context dependent list of explanations for the propagated literals.
-                                    Only used when bvEagerPropagate option enabled. */
-  TNodeSet d_variables;
-  TNodeSet d_bbAtoms;
-  AbstractionModule* d_abstraction;
-  bool d_emptyNotify;
-
-  // The size of the fact queue when we most recently called solve() in the
-  // bit-vector SAT solver. This is the level at which we should have
-  // a full model in the bv SAT solver.
-  context::CDO<int> d_fullModelAssertionLevel;
-
-  void addAtom(TNode atom);
-  bool hasValue(TNode a);
-  Node getModelFromSatSolver(TNode a, bool fullModel) override;
-
- public:
-  void bbTerm(TNode node, Bits& bits) override;
-  void bbAtom(TNode node) override;
-  Node getBBAtom(TNode atom) const override;
-  void storeBBAtom(TNode atom, Node atom_bb) override;
-  void storeBBTerm(TNode node, const Bits& bits) override;
-  bool hasBBAtom(TNode atom) const override;
-
-  TLazyBitblaster(context::Context* c, bv::TheoryBV* bv, const std::string name="", bool emptyNotify = false);
-  ~TLazyBitblaster();
-  /**
-   * Pushes the assumption literal associated with node to the SAT
-   * solver assumption queue. 
-   * 
-   * @param node assumption
-   * @param propagate run bcp or not
-   * 
-   * @return false if a conflict detected
-   */
-  bool assertToSat(TNode node, bool propagate = true);
-  bool propagate();
-  bool solve();
-  prop::SatValue solveWithBudget(unsigned long conflict_budget);
-  void getConflict(std::vector<TNode>& conflict);
-  void explain(TNode atom, std::vector<TNode>& explanation);
-  void setAbstraction(AbstractionModule* abs);
-  
-  theory::EqualityStatus getEqualityStatus(TNode a, TNode b);
-
-  /**
-   * Adds a constant value for each bit-blasted variable in the model.
-   *
-   * @param m the model
-   * @param fullModel whether to create a "full model," i.e., add
-   * constants to equivalence classes that don't already have them
-   */
-  bool collectModelInfo(TheoryModel* m, bool fullModel);
-  void setProofLog( BitVectorProof * bvp );
-
-  typedef TNodeSet::const_iterator vars_iterator;
-  vars_iterator beginVars() { return d_variables.begin(); }
-  vars_iterator endVars() { return d_variables.end(); }
-
-  /**
-   * Creates the bits corresponding to the variable (or non-bv term). 
-   *
-   * @param var
-   */
-  void makeVariable(TNode var, Bits& bits) override;
-
-  bool isSharedTerm(TNode node);
-  uint64_t computeAtomWeight(TNode node, NodeSet& seen);
-  /** 
-   * Deletes SatSolver and CnfCache, but maintains bit-blasting
-   * terms cache. 
-   * 
-   */
-  void clearSolver(); 
-private:
-
-  class Statistics {
-  public:
-    IntStat d_numTermClauses, d_numAtomClauses;
-    IntStat d_numTerms, d_numAtoms;
-    IntStat d_numExplainedPropagations;
-    IntStat d_numBitblastingPropagations;
-    TimerStat d_bitblastTimer;
-    Statistics(const std::string& name);
-    ~Statistics();
-  };
-  std::string d_name;
-public:
-  Statistics d_statistics;
-};
-
-class MinisatEmptyNotify : public prop::BVSatSolverInterface::Notify {
-public:
-  MinisatEmptyNotify() {}
-  bool notify(prop::SatLiteral lit) override { return true; }
-  void notify(prop::SatClause& clause) override {}
-  void spendResource(unsigned amount) override
-  {
-    NodeManager::currentResourceManager()->spendResource(amount);
-  }
-  void safePoint(unsigned amount) override {}
-};
-
-
-class EagerBitblaster : public TBitblaster<Node> {
-  typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
-  // sat solver used for bitblasting and associated CnfStream
-  prop::SatSolver*                   d_satSolver;
-  BitblastingRegistrar*              d_bitblastingRegistrar;
-  context::Context*                  d_nullContext;
-  prop::CnfStream*                   d_cnfStream;
-
-  theory::bv::TheoryBV* d_bv;
-  TNodeSet d_bbAtoms;
-  TNodeSet d_variables;
-
-  // This is either an MinisatEmptyNotify or NULL.
-  MinisatEmptyNotify* d_notify;
-
-  Node getModelFromSatSolver(TNode a, bool fullModel) override;
-  bool isSharedTerm(TNode node);
-
-public:
-  EagerBitblaster(theory::bv::TheoryBV* theory_bv);
-  ~EagerBitblaster();
-
-  void addAtom(TNode atom);
-  void makeVariable(TNode node, Bits& bits) override;
-  void bbTerm(TNode node, Bits& bits) override;
-  void bbAtom(TNode node) override;
-  Node getBBAtom(TNode node) const override;
-  bool hasBBAtom(TNode atom) const override;
-  void bbFormula(TNode formula);
-  void storeBBAtom(TNode atom, Node atom_bb) override;
-  void storeBBTerm(TNode node, const Bits& bits) override;
-
-  bool assertToSat(TNode node, bool propagate = true);
-  bool solve();
-  bool collectModelInfo(TheoryModel* m, bool fullModel);
-  void setProofLog( BitVectorProof * bvp );
-};
-
-class BitblastingRegistrar: public prop::Registrar {
-  EagerBitblaster* d_bitblaster;
-public:
-  BitblastingRegistrar(EagerBitblaster* bb)
-    : d_bitblaster(bb)
-  {}
-  void preRegister(Node n) override;
-}; /* class Registrar */
-
-class AigBitblaster : public TBitblaster<Abc_Obj_t*> {
-  typedef std::unordered_map<TNode, Abc_Obj_t*, TNodeHashFunction > TNodeAigMap;
-  typedef std::unordered_map<Node, Abc_Obj_t*, NodeHashFunction > NodeAigMap;
-  
-  static Abc_Ntk_t* abcAigNetwork;
-  context::Context* d_nullContext;
-  prop::SatSolver* d_satSolver;
-  TNodeAigMap d_aigCache;
-  NodeAigMap d_bbAtoms;
-  
-  NodeAigMap d_nodeToAigInput;
-  // the thing we are checking for sat
-  Abc_Obj_t* d_aigOutputNode;
-
-  void addAtom(TNode atom);
-  void simplifyAig();
-  void storeBBAtom(TNode atom, Abc_Obj_t* atom_bb) override;
-  Abc_Obj_t* getBBAtom(TNode atom) const override;
-  bool hasBBAtom(TNode atom) const override;
-  void cacheAig(TNode node, Abc_Obj_t* aig);
-  bool hasAig(TNode node);
-  Abc_Obj_t* getAig(TNode node);
-  Abc_Obj_t* mkInput(TNode input);
-  bool hasInput(TNode input);
-  void convertToCnfAndAssert();
-  void assertToSatSolver(Cnf_Dat_t* pCnf);
-  Node getModelFromSatSolver(TNode a, bool fullModel) override
-  {
-    Unreachable();
-  }
-
- public:
-  AigBitblaster();
-  ~AigBitblaster();
-
-  void makeVariable(TNode node, Bits& bits) override;
-  void bbTerm(TNode node, Bits& bits) override;
-  void bbAtom(TNode node) override;
-  Abc_Obj_t* bbFormula(TNode formula);
-  bool solve(TNode query); 
-  static Abc_Aig_t* currentAigM();
-  static Abc_Ntk_t* currentAigNtk();
-  
-private:
-  class Statistics {
-  public:
-    IntStat     d_numClauses;
-    IntStat     d_numVariables; 
-    TimerStat   d_simplificationTime;
-    TimerStat   d_cnfConversionTime;
-    TimerStat   d_solveTime; 
-    Statistics();
-    ~Statistics();
-  };
-
-  Statistics d_statistics;
-
-};
-
-
-// Bitblaster implementation
-
-template <class T> void TBitblaster<T>::initAtomBBStrategies() {
-  for (int i = 0 ; i < kind::LAST_KIND; ++i ) {
-    d_atomBBStrategies[i] = UndefinedAtomBBStrategy<T>;
-  }
-  /// setting default bb strategies for atoms
-  d_atomBBStrategies [ kind::EQUAL ]           = DefaultEqBB<T>;
-  d_atomBBStrategies [ kind::BITVECTOR_ULT ]   = DefaultUltBB<T>;
-  d_atomBBStrategies [ kind::BITVECTOR_ULE ]   = DefaultUleBB<T>;
-  d_atomBBStrategies [ kind::BITVECTOR_UGT ]   = DefaultUgtBB<T>;
-  d_atomBBStrategies [ kind::BITVECTOR_UGE ]   = DefaultUgeBB<T>;
-  d_atomBBStrategies [ kind::BITVECTOR_SLT ]   = DefaultSltBB<T>;
-  d_atomBBStrategies [ kind::BITVECTOR_SLE ]   = DefaultSleBB<T>;
-  d_atomBBStrategies [ kind::BITVECTOR_SGT ]   = DefaultSgtBB<T>;
-  d_atomBBStrategies [ kind::BITVECTOR_SGE ]   = DefaultSgeBB<T>;
-}
-
-template <class T> void TBitblaster<T>::initTermBBStrategies() {
-  for (int i = 0 ; i < kind::LAST_KIND; ++i ) {
-    d_termBBStrategies[i] = DefaultVarBB<T>;
-  }
-  /// setting default bb strategies for terms:
-  d_termBBStrategies [ kind::CONST_BITVECTOR ]        = DefaultConstBB<T>;
-  d_termBBStrategies [ kind::BITVECTOR_NOT ]          = DefaultNotBB<T>;
-  d_termBBStrategies [ kind::BITVECTOR_CONCAT ]       = DefaultConcatBB<T>;
-  d_termBBStrategies [ kind::BITVECTOR_AND ]          = DefaultAndBB<T>;
-  d_termBBStrategies [ kind::BITVECTOR_OR ]           = DefaultOrBB<T>;
-  d_termBBStrategies [ kind::BITVECTOR_XOR ]          = DefaultXorBB<T>;
-  d_termBBStrategies [ kind::BITVECTOR_XNOR ]         = DefaultXnorBB<T>;
-  d_termBBStrategies [ kind::BITVECTOR_NAND ]         = DefaultNandBB<T>;
-  d_termBBStrategies [ kind::BITVECTOR_NOR ]          = DefaultNorBB<T>;
-  d_termBBStrategies [ kind::BITVECTOR_COMP ]         = DefaultCompBB<T>;
-  d_termBBStrategies [ kind::BITVECTOR_MULT ]         = DefaultMultBB<T>;
-  d_termBBStrategies [ kind::BITVECTOR_PLUS ]         = DefaultPlusBB<T>;
-  d_termBBStrategies [ kind::BITVECTOR_SUB ]          = DefaultSubBB<T>;
-  d_termBBStrategies [ kind::BITVECTOR_NEG ]          = DefaultNegBB<T>;
-  d_termBBStrategies [ kind::BITVECTOR_UDIV ]         = UndefinedTermBBStrategy<T>;
-  d_termBBStrategies [ kind::BITVECTOR_UREM ]         = UndefinedTermBBStrategy<T>;
-  d_termBBStrategies [ kind::BITVECTOR_UDIV_TOTAL ]   = DefaultUdivBB<T>;
-  d_termBBStrategies [ kind::BITVECTOR_UREM_TOTAL ]   = DefaultUremBB<T>;
-  d_termBBStrategies [ kind::BITVECTOR_SDIV ]         = UndefinedTermBBStrategy<T>;
-  d_termBBStrategies [ kind::BITVECTOR_SREM ]         = UndefinedTermBBStrategy<T>;
-  d_termBBStrategies [ kind::BITVECTOR_SMOD ]         = UndefinedTermBBStrategy<T>;
-  d_termBBStrategies [ kind::BITVECTOR_SHL ]          = DefaultShlBB<T>;
-  d_termBBStrategies [ kind::BITVECTOR_LSHR ]         = DefaultLshrBB<T>;
-  d_termBBStrategies [ kind::BITVECTOR_ASHR ]         = DefaultAshrBB<T>;
-  d_termBBStrategies [ kind::BITVECTOR_ULTBV ]        = DefaultUltbvBB<T>;
-  d_termBBStrategies [ kind::BITVECTOR_SLTBV ]        = DefaultSltbvBB<T>;
-  d_termBBStrategies [ kind::BITVECTOR_ITE ]          = DefaultIteBB<T>;
-  d_termBBStrategies [ kind::BITVECTOR_EXTRACT ]      = DefaultExtractBB<T>;
-  d_termBBStrategies [ kind::BITVECTOR_REPEAT ]       = DefaultRepeatBB<T>;
-  d_termBBStrategies [ kind::BITVECTOR_ZERO_EXTEND ]  = DefaultZeroExtendBB<T>;
-  d_termBBStrategies [ kind::BITVECTOR_SIGN_EXTEND ]  = DefaultSignExtendBB<T>;
-  d_termBBStrategies [ kind::BITVECTOR_ROTATE_RIGHT ] = DefaultRotateRightBB<T>;
-  d_termBBStrategies [ kind::BITVECTOR_ROTATE_LEFT ]  = DefaultRotateLeftBB<T>;
-}
-
-template <class T>
-TBitblaster<T>::TBitblaster()
-  : d_termCache()
-  , d_modelCache()
-  , d_bvp( NULL )
-{
-  initAtomBBStrategies();
-  initTermBBStrategies(); 
-}
-
-template <class T>
-bool TBitblaster<T>::hasBBTerm(TNode node) const {
-  return d_termCache.find(node) != d_termCache.end();
-}
-template <class T>
-void TBitblaster<T>::getBBTerm(TNode node, Bits& bits) const {
-  Assert (hasBBTerm(node));
-  bits = d_termCache.find(node)->second;
-}
-
-template <class T>
-void TBitblaster<T>::storeBBTerm(TNode node, const Bits& bits) {
-  d_termCache.insert(std::make_pair(node, bits));
-}
-
-template <class T>
-void TBitblaster<T>::invalidateModelCache() {
-  d_modelCache.clear();
-}
-
-template <class T>
-Node TBitblaster<T>::getTermModel(TNode node, bool fullModel) {
-  if (d_modelCache.find(node) != d_modelCache.end())
-    return d_modelCache[node]; 
-
-  if (node.isConst())
-    return node; 
-
-  Node value = getModelFromSatSolver(node, false);
-  if (!value.isNull()) {
-    Debug("bv-equality-status")<< "TLazyBitblaster::getTermModel from SatSolver" << node <<" => " << value <<"\n";
-    d_modelCache[node] = value;
-    Assert (value.isConst()); 
-    return value;
-  }
-
-  if (Theory::isLeafOf(node, theory::THEORY_BV)) {
-    // if it is a leaf may ask for fullModel
-    value = getModelFromSatSolver(node, true); 
-    Debug("bv-equality-status")<< "TLazyBitblaster::getTermModel from VarValue" << node <<" => " << value <<"\n";
-    Assert ((fullModel && !value.isNull() && value.isConst()) || !fullModel); 
-    if (!value.isNull()) {
-      d_modelCache[node] = value;
-    }
-    return value;
-  }
-  Assert (node.getType().isBitVector());
-  
-  NodeBuilder<> nb(node.getKind());
-  if (node.getMetaKind() == kind::metakind::PARAMETERIZED) {
-    nb << node.getOperator(); 
-  }
-
-  for (unsigned i = 0; i < node.getNumChildren(); ++i) {
-    nb << getTermModel(node[i], fullModel); 
-  }
-  value = nb; 
-  value = Rewriter::rewrite(value);
-  Assert (value.isConst()); 
-  d_modelCache[node] = value;
-  Debug("bv-term-model")<< "TLazyBitblaster::getTermModel Building Value" << node <<" => " << value <<"\n";
-  return value; 
-}
-
-
-} /* bv namespace */
-
-} /* theory namespace */
-
-} /* CVC4 namespace */
-
-#endif /* __CVC4__BITBLASTER_H */
diff --git a/src/theory/bv/bv_eager_solver.cpp b/src/theory/bv/bv_eager_solver.cpp
index 01282880c..f1af28d04 100644
--- a/src/theory/bv/bv_eager_solver.cpp
+++ b/src/theory/bv/bv_eager_solver.cpp
@@ -15,9 +15,11 @@
  **/
 
 #include "theory/bv/bv_eager_solver.h"
+
 #include "options/bv_options.h"
 #include "proof/bitvector_proof.h"
-#include "theory/bv/bitblaster_template.h"
+#include "theory/bv/bitblast/aig_bitblaster.h"
+#include "theory/bv/bitblast/eager_bitblaster.h"
 
 using namespace std;
 
diff --git a/src/theory/bv/bv_quick_check.cpp b/src/theory/bv/bv_quick_check.cpp
index 101b64173..44e87e368 100644
--- a/src/theory/bv/bv_quick_check.cpp
+++ b/src/theory/bv/bv_quick_check.cpp
@@ -17,7 +17,7 @@
 #include "theory/bv/bv_quick_check.h"
 
 #include "smt/smt_statistics_registry.h"
-#include "theory/bv/bitblaster_template.h"
+#include "theory/bv/bitblast/lazy_bitblaster.h"
 #include "theory/bv/theory_bv_utils.h"
 
 using namespace CVC4::prop;
diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp
index 902a4dbe0..cdbf2f955 100644
--- a/src/theory/bv/bv_subtheory_bitblast.cpp
+++ b/src/theory/bv/bv_subtheory_bitblast.cpp
@@ -14,18 +14,18 @@
  ** Algebraic solver.
  **/
 
+#include "theory/bv/bv_subtheory_bitblast.h"
 #include "decision/decision_attributes.h"
-#include "options/decision_options.h"
 #include "options/bv_options.h"
+#include "options/decision_options.h"
+#include "proof/bitvector_proof.h"
+#include "proof/proof_manager.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/bv/abstraction.h"
-#include "theory/bv/bitblaster_template.h"
+#include "theory/bv/bitblast/lazy_bitblaster.h"
 #include "theory/bv/bv_quick_check.h"
-#include "theory/bv/bv_subtheory_bitblast.h"
 #include "theory/bv/theory_bv.h"
 #include "theory/bv/theory_bv_utils.h"
-#include "proof/proof_manager.h"
-#include "proof/bitvector_proof.h"
 
 using namespace std;
 using namespace CVC4::context;
diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h
index 509e59b19..ca9f472c2 100644
--- a/src/theory/bv/bv_subtheory_bitblast.h
+++ b/src/theory/bv/bv_subtheory_bitblast.h
@@ -20,14 +20,13 @@
 
 #include <unordered_map>
 
-#include "theory/bv/bitblaster_template.h"
 #include "theory/bv/bv_subtheory.h"
 
 namespace CVC4 {
 namespace theory {
 namespace bv {
 
-class LazyBitblaster;
+class TLazyBitblaster;
 class AbstractionModule;
 class BVQuickCheck;
 class QuickXPlain;