Add SmtGlobals Class

- The options replayStream, lemmaInputChannel, lemmaOutputChannel have been removed due to their datatypes. These datatypes were previously pointers to types that were not usable from the options/ library.
- The option replayLog has been removed due to inconsistent memory management.
- SmtGlobals is a class that wraps a pointer to each of these removed options. These can each be set independently.
- There is a single SmtGlobals per SmtEngine with the lifetime of the SmtEngine.
- A pointer to this is freely given to the user of an SmtEngine to parameterize the solver after construction.
- Selected classes have been given a copy of this pointer in their constructors.
- Removed the dependence on Node from Result. Moving Result back into util/.

8 files changed, 157 insertions, 140 deletions

diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h
index b93d0561e..7b071b9e9 100644
--- a/src/theory/bv/bitblaster_template.h
+++ b/src/theory/bv/bitblaster_template.h
@@ -19,17 +19,17 @@
 #ifndef __CVC4__BITBLASTER_TEMPLATE_H
 #define __CVC4__BITBLASTER_TEMPLATE_H
 
-
-#include "expr/node.h"
-#include <vector>
 #include <ext/hash_map>
+#include <vector>
 
-#include "context/cdhashmap.h"
 #include "bitblast_strategies_template.h"
+#include "context/cdhashmap.h"
+#include "expr/node.h"
 #include "expr/resource_manager.h"
 #include "prop/sat_solver.h"
-#include "theory/valuation.h"
+#include "smt/smt_globals.h"
 #include "theory/theory_registrar.h"
+#include "theory/valuation.h"
 
 class Abc_Obj_t_;
 typedef Abc_Obj_t_ Abc_Obj_t;
@@ -84,25 +84,25 @@ protected:
   // caches and mappings
   TermDefMap d_termCache;
   ModelCache d_modelCache;
-  
+
   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; 
+  AtomBBStrategy d_atomBBStrategies[kind::LAST_KIND];
+  virtual Node getModelFromSatSolver(TNode node, bool fullModel) = 0;
 public:
-  TBitblaster(); 
+  TBitblaster();
   virtual ~TBitblaster() {}
-  virtual void bbAtom(TNode node) = 0; 
+  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;
   void storeBBTerm(TNode term, const Bits& bits);
@@ -114,10 +114,10 @@ public:
    */
   Node getTermModel(TNode node, bool fullModel);
   void invalidateModelCache();
-}; 
+};
 
 
-class TheoryBV; 
+class TheoryBV;
 
 class TLazyBitblaster :  public TBitblaster<Node> {
   typedef std::vector<Node> Bits;
@@ -127,19 +127,20 @@ class TLazyBitblaster :  public TBitblaster<Node> {
   class MinisatNotify : public prop::BVSatSolverInterface::Notify {
     prop::CnfStream* d_cnf;
     TheoryBV *d_bv;
-    TLazyBitblaster* d_lazyBB; 
+    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);
     void notify(prop::SatClause& clause);
     void spendResource(unsigned ammount);
     void safePoint(unsigned ammount);
   };
-  
+
   TheoryBV *d_bv;
   context::Context* d_ctx;
 
@@ -155,24 +156,25 @@ class TLazyBitblaster :  public TBitblaster<Node> {
   ExplanationMap* d_explanations; /**< context dependent list of explanations for the propagated literals.
                                     Only used when bvEagerPropagate option enabled. */
   TNodeSet d_variables;
-  TNodeSet d_bbAtoms; 
+  TNodeSet d_bbAtoms;
   AbstractionModule* d_abstraction;
   bool d_emptyNotify;
 
   context::CDO<bool> d_satSolverFullModel;
-  
+
   void addAtom(TNode atom);
   bool hasValue(TNode a);
-  Node getModelFromSatSolver(TNode a, bool fullModel);  
+  Node getModelFromSatSolver(TNode a, bool fullModel);
+
 public:
   void bbTerm(TNode node, Bits&  bits);
   void bbAtom(TNode node);
   Node getBBAtom(TNode atom) const;
   void storeBBAtom(TNode atom, Node atom_bb);
-  bool hasBBAtom(TNode atom) const; 
+  bool hasBBAtom(TNode atom) const;
   TLazyBitblaster(context::Context* c, bv::TheoryBV* bv, const std::string name="", bool emptyNotify = false);
   ~TLazyBitblaster() throw();
-  /** 
+  /**
    * Pushes the assumption literal associated with node to the SAT
    * solver assumption queue. 
    * 
@@ -261,26 +263,27 @@ class EagerBitblaster : public TBitblaster<Node> {
   TNodeSet d_variables;
 
   Node getModelFromSatSolver(TNode a, bool fullModel);
-  bool isSharedTerm(TNode node); 
+  bool isSharedTerm(TNode node);
 
 public:
+  EagerBitblaster(theory::bv::TheoryBV* theory_bv);
+  ~EagerBitblaster();
+
   void addAtom(TNode atom);
   void makeVariable(TNode node, Bits& bits);
   void bbTerm(TNode node, Bits&  bits);
   void bbAtom(TNode node);
   Node getBBAtom(TNode node) const;
-  bool hasBBAtom(TNode atom) const; 
+  bool hasBBAtom(TNode atom) const;
   void bbFormula(TNode formula);
   void storeBBAtom(TNode atom, Node atom_bb);
-  EagerBitblaster(theory::bv::TheoryBV* theory_bv); 
-  ~EagerBitblaster();
   bool assertToSat(TNode node, bool propagate = true);
   bool solve();
   void collectModelInfo(TheoryModel* m, bool fullModel);
 };
 
 class BitblastingRegistrar: public prop::Registrar {
-  EagerBitblaster* d_bitblaster; 
+  EagerBitblaster* d_bitblaster;
 public:
   BitblastingRegistrar(EagerBitblaster* bb)
     : d_bitblaster(bb)
diff --git a/src/theory/bv/bv_eager_solver.h b/src/theory/bv/bv_eager_solver.h
index 37e1bd9ba..ff13867cc 100644
--- a/src/theory/bv/bv_eager_solver.h
+++ b/src/theory/bv/bv_eager_solver.h
@@ -33,15 +33,16 @@ class AigBitblaster;
  * BitblastSolver
  */
 class EagerBitblastSolver {
-  typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> AssertionSet; 
+  typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> AssertionSet;
   AssertionSet d_assertionSet;
   /** Bitblasters */
   EagerBitblaster* d_bitblaster;
   AigBitblaster* d_aigBitblaster;
   bool d_useAig;
-  TheoryBV* d_bv; 
+  TheoryBV* d_bv;
+
 public:
-  EagerBitblastSolver(theory::bv::TheoryBV* bv); 
+  EagerBitblastSolver(theory::bv::TheoryBV* bv);
   ~EagerBitblastSolver();
   bool checkSat();
   void assertFormula(TNode formula);
diff --git a/src/theory/bv/bv_quick_check.h b/src/theory/bv/bv_quick_check.h
index 261a0b1c4..8ef49f786 100644
--- a/src/theory/bv/bv_quick_check.h
+++ b/src/theory/bv/bv_quick_check.h
@@ -35,7 +35,7 @@ class TheoryModel;
 
 namespace bv {
 
-class TLazyBitblaster; 
+class TLazyBitblaster;
 class TheoryBV;
 
 class BVQuickCheck {
diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h
index 77461163c..0e066eefb 100644
--- a/src/theory/bv/bv_subtheory_bitblast.h
+++ b/src/theory/bv/bv_subtheory_bitblast.h
@@ -18,8 +18,8 @@
 
 #pragma once
 
-#include "theory/bv/bv_subtheory.h"
 #include "theory/bv/bitblaster_template.h"
+#include "theory/bv/bv_subtheory.h"
 
 namespace CVC4 {
 namespace theory {
@@ -58,7 +58,7 @@ class BitblastSolver : public SubtheorySolver {
   BVQuickCheck* d_quickCheck;
   QuickXPlain* d_quickXplain;
   //  Node getModelValueRec(TNode node);
-  void setConflict(TNode conflict); 
+  void setConflict(TNode conflict);
 public:
   BitblastSolver(context::Context* c, TheoryBV* bv);
   ~BitblastSolver();
diff --git a/src/theory/bv/eager_bitblaster.cpp b/src/theory/bv/eager_bitblaster.cpp
index ec2bfd9c0..39606ca7c 100644
--- a/src/theory/bv/eager_bitblaster.cpp
+++ b/src/theory/bv/eager_bitblaster.cpp
@@ -46,7 +46,8 @@ EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv)
   d_nullContext = new context::Context();
 
   d_satSolver = prop::SatSolverFactory::createMinisat(d_nullContext, "EagerBitblaster");
-  d_cnfStream = new prop::TseitinCnfStream(d_satSolver, d_bitblastingRegistrar, d_nullContext);
+  d_cnfStream = new prop::TseitinCnfStream(d_satSolver, d_bitblastingRegistrar,
+                                           d_nullContext, d_bv->globals());
 
   MinisatEmptyNotify* notify = new MinisatEmptyNotify();
   d_satSolver->setNotify(notify);
diff --git a/src/theory/bv/lazy_bitblaster.cpp b/src/theory/bv/lazy_bitblaster.cpp
index 3c2b4ed78..b8173cb8b 100644
--- a/src/theory/bv/lazy_bitblaster.cpp
+++ b/src/theory/bv/lazy_bitblaster.cpp
@@ -26,12 +26,13 @@
 #include "theory/theory_model.h"
 #include "theory_bv_utils.h"
 
-using namespace CVC4;
-using namespace CVC4::theory;
-using namespace CVC4::theory::bv; 
+namespace CVC4 {
+namespace theory {
+namespace bv {
 
 
-TLazyBitblaster::TLazyBitblaster(context::Context* c, bv::TheoryBV* bv, const std::string name, bool emptyNotify)
+TLazyBitblaster::TLazyBitblaster(context::Context* c, bv::TheoryBV* bv,
+                                 const std::string name, bool emptyNotify)
   : TBitblaster<Node>()
   , d_bv(bv)
   , d_ctx(c)
@@ -44,13 +45,13 @@ TLazyBitblaster::TLazyBitblaster(context::Context* c, bv::TheoryBV* bv, const st
   , d_satSolverFullModel(c, false)
   , d_name(name)
   , d_statistics(name) {
+
   d_satSolver = prop::SatSolverFactory::createMinisat(c, name);
   d_nullRegistrar = new prop::NullRegistrar();
   d_nullContext = new context::Context();
-  d_cnfStream = new prop::TseitinCnfStream(d_satSolver,
-                                           d_nullRegistrar,
-                                           d_nullContext);
-  
+  d_cnfStream = new prop::TseitinCnfStream(d_satSolver, d_nullRegistrar,
+                                           d_nullContext, d_bv->globals());
+
   d_satSolverNotify = d_emptyNotify ?
     (prop::BVSatSolverInterface::Notify*) new MinisatEmptyNotify() :
     (prop::BVSatSolverInterface::Notify*) new MinisatNotify(d_cnfStream, bv, this);
@@ -59,7 +60,7 @@ TLazyBitblaster::TLazyBitblaster(context::Context* c, bv::TheoryBV* bv, const st
 }
 
 void TLazyBitblaster::setAbstraction(AbstractionModule* abs) {
-  d_abstraction = abs; 
+  d_abstraction = abs;
 }
 
 TLazyBitblaster::~TLazyBitblaster() throw() {
@@ -103,8 +104,8 @@ void TLazyBitblaster::bbAtom(TNode node) {
     if (expansion.getKind() == kind::CONST_BOOLEAN) {
       atom_bb = expansion;
     } else {
-      Assert (expansion.getKind() == kind::AND); 
-      std::vector<Node> atoms; 
+      Assert (expansion.getKind() == kind::AND);
+      std::vector<Node> atoms;
       for (unsigned i = 0; i < expansion.getNumChildren(); ++i) {
         Node normalized_i = Rewriter::rewrite(expansion[i]);
         Node atom_i = normalized_i.getKind() != kind::CONST_BOOLEAN ?
@@ -481,7 +482,7 @@ void TLazyBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) {
 }
 
 void TLazyBitblaster::clearSolver() {
-  Assert (d_ctx->getLevel() == 0); 
+  Assert (d_ctx->getLevel() == 0);
   delete d_satSolver;
   delete d_satSolverNotify;
   delete d_cnfStream;
@@ -492,16 +493,19 @@ void TLazyBitblaster::clearSolver() {
   d_bbAtoms.clear();
   d_variables.clear();
   d_termCache.clear();
-  
-  invalidateModelCache();  
+
+  invalidateModelCache();
   // recreate sat solver
   d_satSolver = prop::SatSolverFactory::createMinisat(d_ctx);
-  d_cnfStream = new prop::TseitinCnfStream(d_satSolver,
-                                           d_nullRegistrar,
-                                           d_nullContext);
+  d_cnfStream = new prop::TseitinCnfStream(d_satSolver, d_nullRegistrar,
+                                           d_nullContext, d_bv->globals());
 
   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 */
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 4039fceec..0505035c7 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -31,38 +31,40 @@
 #include "theory/theory_model.h"
 #include "theory/valuation.h"
 
-using namespace CVC4;
-using namespace CVC4::theory;
-using namespace CVC4::theory::bv;
 using namespace CVC4::context;
-
-using namespace std;
 using namespace CVC4::theory::bv::utils;
+using namespace std;
 
-TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo)
-  : Theory(THEORY_BV, c, u, out, valuation, logicInfo),
-    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(NULL),
-    d_abstractionModule(new AbstractionModule()),
-    d_isCoreTheory(false),
-    d_calledPreregister(false)
+namespace CVC4 {
+namespace theory {
+namespace bv {
+
+TheoryBV::TheoryBV(context::Context* c, context::UserContext* u,
+                   OutputChannel& out, Valuation valuation,
+                   const LogicInfo& logicInfo, SmtGlobals* globals)
+    : Theory(THEORY_BV, c, u, out, valuation, logicInfo, globals),
+      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(NULL),
+      d_abstractionModule(new AbstractionModule()),
+      d_isCoreTheory(false),
+      d_calledPreregister(false)
 {
 
   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
     d_eagerSolver = new EagerBitblastSolver(this);
-    return; 
+    return;
   }
 
   if (options::bitvectorEqualitySolver()) {
@@ -70,7 +72,7 @@ TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel&
     d_subtheories.push_back(core_solver);
     d_subtheoryMap[SUB_CORE] = core_solver;
   }
-  
+
   if (options::bitvectorInequalitySolver()) {
     SubtheorySolver* ineq_solver = new InequalitySolver(c, this);
     d_subtheories.push_back(ineq_solver);
@@ -101,7 +103,7 @@ TheoryBV::~TheoryBV() {
 
 void TheoryBV::setMasterEqualityEngine(eq::EqualityEngine* eq) {
   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
-    return; 
+    return;
   }
   if (options::bitvectorEqualitySolver()) {
     dynamic_cast<CoreSolver*>(d_subtheoryMap[SUB_CORE])->setMasterEqualityEngine(eq);
@@ -179,31 +181,31 @@ void TheoryBV::collectNumerators(TNode term, TNodeSet& seen) {
       d_BVDivByZeroAckerman[size] = TNodeSet();
     }
     d_BVDivByZeroAckerman[size].insert(term[0]);
-    seen.insert(term); 
+    seen.insert(term);
   } else if (term.getKind() == kind::BITVECTOR_ACKERMANIZE_UREM) {
     unsigned size = utils::getSize(term[0]);
     if (d_BVRemByZeroAckerman.find(size) == d_BVRemByZeroAckerman.end()) {
       d_BVRemByZeroAckerman[size] = TNodeSet();
     }
     d_BVRemByZeroAckerman[size].insert(term[0]);
-    seen.insert(term); 
+    seen.insert(term);
   }
   for (unsigned i = 0; i < term.getNumChildren(); ++i) {
-    collectNumerators(term[i], seen); 
+    collectNumerators(term[i], seen);
   }
-  seen.insert(term); 
+  seen.insert(term);
 }
 
 void TheoryBV::mkAckermanizationAsssertions(std::vector<Node>& assertions) {
   Debug("bv-ackermanize") << "TheoryBV::mkAckermanizationAsssertions\n";
-  
+
   Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER);
   AlwaysAssert(!options::incrementalSolving());
-  TNodeSet seen; 
+  TNodeSet seen;
   for (unsigned i = 0; i < assertions.size(); ++i) {
-    collectNumerators(assertions[i], seen); 
+    collectNumerators(assertions[i], seen);
   }
-  
+
   // process division UF
   Debug("bv-ackermanize") << "Process division UF...\n";
   for (WidthToNumerators::const_iterator it = d_BVDivByZeroAckerman.begin(); it != d_BVDivByZeroAckerman.end(); ++it) {
@@ -215,13 +217,13 @@ void TheoryBV::mkAckermanizationAsssertions(std::vector<Node>& assertions) {
         TNode arg1 = *i;
         TNode arg2 = *j;
         TNode acker1 = utils::mkNode(kind::BITVECTOR_ACKERMANIZE_UDIV, arg1);
-        TNode acker2 = utils::mkNode(kind::BITVECTOR_ACKERMANIZE_UDIV, arg2); 
+        TNode acker2 = utils::mkNode(kind::BITVECTOR_ACKERMANIZE_UDIV, arg2);
 
         Node arg_eq = utils::mkNode(kind::EQUAL, arg1, arg2);
         Node acker_eq = utils::mkNode(kind::EQUAL, acker1, acker2);
         Node lemma = utils::mkNode(kind::IMPLIES, arg_eq, acker_eq);
         Debug("bv-ackermanize") << "  " << lemma << "\n";
-        assertions.push_back(lemma); 
+        assertions.push_back(lemma);
       }
     }
   }
@@ -236,13 +238,13 @@ void TheoryBV::mkAckermanizationAsssertions(std::vector<Node>& assertions) {
         TNode arg1 = *i;
         TNode arg2 = *j;
         TNode acker1 = utils::mkNode(kind::BITVECTOR_ACKERMANIZE_UREM, arg1);
-        TNode acker2 = utils::mkNode(kind::BITVECTOR_ACKERMANIZE_UREM, arg2); 
+        TNode acker2 = utils::mkNode(kind::BITVECTOR_ACKERMANIZE_UREM, arg2);
 
         Node arg_eq = utils::mkNode(kind::EQUAL, arg1, arg2);
         Node acker_eq = utils::mkNode(kind::EQUAL, acker1, acker2);
         Node lemma = utils::mkNode(kind::IMPLIES, arg_eq, acker_eq);
         Debug("bv-ackermanize") << "  " << lemma << "\n";
-        assertions.push_back(lemma); 
+        assertions.push_back(lemma);
       }
     }
   }
@@ -265,7 +267,7 @@ Node TheoryBV::expandDefinition(LogicRequest &logicRequest, Node node) {
 
     if (options::bitvectorDivByZeroConst()) {
       Kind kind = node.getKind() == kind::BITVECTOR_UDIV ? kind::BITVECTOR_UDIV_TOTAL : kind::BITVECTOR_UREM_TOTAL;
-      return nm->mkNode(kind, node[0], node[1]); 
+      return nm->mkNode(kind, node[0], node[1]);
     }
 
     TNode num = node[0], den = node[1];
@@ -275,9 +277,9 @@ Node TheoryBV::expandDefinition(LogicRequest &logicRequest, Node node) {
 
     if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
       // Ackermanize UF if using eager bit-blasting
-      Node ackerman_var = nm->mkNode(node.getKind() == kind::BITVECTOR_UDIV ? kind::BITVECTOR_ACKERMANIZE_UDIV : kind::BITVECTOR_ACKERMANIZE_UREM, num); 
+      Node ackerman_var = nm->mkNode(node.getKind() == kind::BITVECTOR_UDIV ? kind::BITVECTOR_ACKERMANIZE_UDIV : kind::BITVECTOR_ACKERMANIZE_UREM, num);
       node = nm->mkNode(kind::ITE, den_eq_0, ackerman_var, divTotalNumDen);
-      return node; 
+      return node;
     } else {
       Node divByZero = getBVDivByZero(node.getKind(), width);
       Node divByZeroNum = nm->mkNode(kind::APPLY_UF, divByZero, num);
@@ -300,7 +302,7 @@ Node TheoryBV::expandDefinition(LogicRequest &logicRequest, Node node) {
 void TheoryBV::preRegisterTerm(TNode node) {
   d_calledPreregister = true;
   Debug("bitvector-preregister") << "TheoryBV::preRegister(" << node << ")" << std::endl;
- 
+
   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
     // the aig bit-blaster option is set heuristically
     // if bv abstraction is not used
@@ -309,13 +311,13 @@ void TheoryBV::preRegisterTerm(TNode node) {
     }
 
     if (node.getKind() == kind::BITVECTOR_EAGER_ATOM) {
-      Node formula = node[0]; 
+      Node formula = node[0];
       d_eagerSolver->assertFormula(formula);
     }
     // nothing to do for the other terms
-    return; 
+    return;
   }
-  
+
   for (unsigned i = 0; i < d_subtheories.size(); ++i) {
     d_subtheories[i]->preRegister(node);
   }
@@ -370,7 +372,7 @@ void TheoryBV::check(Effort e)
   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); 
+  d_invalidateModelCache.set(true);
   // if we are using the eager solver
   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
     // this can only happen on an empty benchmark
@@ -380,28 +382,28 @@ void TheoryBV::check(Effort e)
     if (!Theory::fullEffort(e))
       return;
 
-    std::vector<TNode> assertions; 
+    std::vector<TNode> assertions;
     while (!done()) {
       TNode fact = get().assertion;
       Assert (fact.getKind() == kind::BITVECTOR_EAGER_ATOM);
-      assertions.push_back(fact); 
+      assertions.push_back(fact);
     }
-    Assert (d_eagerSolver->hasAssertions(assertions)); 
-    
+    Assert (d_eagerSolver->hasAssertions(assertions));
+
     bool ok = d_eagerSolver->checkSat();
     if (!ok) {
       if (assertions.size() == 1) {
         d_out->conflict(assertions[0]);
-        return; 
+        return;
       }
       Node conflict = NodeManager::currentNM()->mkNode(kind::AND, assertions);
       d_out->conflict(conflict);
-      return; 
+      return;
     }
     return;
   }
-  
-  
+
+
   if (Theory::fullEffort(e)) {
     ++(d_statistics.d_numCallsToCheckFullEffort);
   } else {
@@ -446,7 +448,7 @@ void TheoryBV::check(Effort e)
 void TheoryBV::collectModelInfo( TheoryModel* m, bool fullModel ){
   Assert(!inConflict());
   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
-    d_eagerSolver->collectModelInfo(m, fullModel); 
+    d_eagerSolver->collectModelInfo(m, fullModel);
   }
   for (unsigned i = 0; i < d_subtheories.size(); ++i) {
     if (d_subtheories[i]->isComplete()) {
@@ -469,7 +471,7 @@ Node TheoryBV::getModelValue(TNode var) {
 void TheoryBV::propagate(Effort e) {
   Debug("bitvector") << indent() << "TheoryBV::propagate()" << std::endl;
   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
-    return; 
+    return;
   }
 
   if (inConflict()) {
@@ -508,29 +510,29 @@ Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitu
         outSubstitutions.addSubstitution(in[1], in[0]);
         return PP_ASSERT_STATUS_SOLVED;
       }
-      Node node = Rewriter::rewrite(in); 
+      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].getKind() == kind::VARIABLE) {
           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(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); 
+            children.push_back(skolem);
           } else {
             unsigned skolem1_size = low;
             unsigned skolem2_size = var_bitwidth - high - 1;
@@ -541,7 +543,7 @@ Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitu
             children.push_back(skolem1);
           }
           Node concat = utils::mkNode(kind::BITVECTOR_CONCAT, children);
-          Assert (utils::getSize(concat) == utils::getSize(extract[0])); 
+          Assert (utils::getSize(concat) == utils::getSize(extract[0]));
           outSubstitutions.addSubstitution(extract[0], concat);
           return PP_ASSERT_STATUS_SOLVED;
         }
@@ -552,7 +554,7 @@ Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitu
   case kind::BITVECTOR_SLT:
   case kind::BITVECTOR_ULE:
   case kind::BITVECTOR_SLE:
-    
+
   default:
     // TODO other predicates
     break;
@@ -562,7 +564,7 @@ Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitu
 
 Node TheoryBV::ppRewrite(TNode t)
 {
-  Debug("bv-pp-rewrite") << "TheoryBV::ppRewrite " << t << "\n"; 
+  Debug("bv-pp-rewrite") << "TheoryBV::ppRewrite " << t << "\n";
   Node res = t;
   if (RewriteRule<BitwiseEq>::applies(t)) {
     Node result = RewriteRule<BitwiseEq>::run<false>(t);
@@ -591,8 +593,8 @@ Node TheoryBV::ppRewrite(TNode t)
     } else {
       res = t;
     }
-  } 
-  
+  }
+
 
   // if(t.getKind() == kind::EQUAL &&
   //    ((t[0].getKind() == kind::BITVECTOR_MULT && t[1].getKind() == kind::BITVECTOR_PLUS) ||
@@ -618,18 +620,18 @@ Node TheoryBV::ppRewrite(TNode t)
   //         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); 
+    d_abstractionModule->addInputAtom(res);
   }
-  Debug("bv-pp-rewrite") << "to   " << res << "\n"; 
+  Debug("bv-pp-rewrite") << "to   " << res << "\n";
   return res;
 }
 
@@ -637,13 +639,13 @@ void TheoryBV::presolve() {
   Debug("bitvector") << "TheoryBV::presolve" << endl;
 }
 
-static int prop_count = 0; 
+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++; 
-  
+  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;
@@ -720,7 +722,7 @@ void TheoryBV::addSharedTerm(TNode t) {
 
 EqualityStatus TheoryBV::getEqualityStatus(TNode a, TNode b)
 {
-  Assert (options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY); 
+  Assert (options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY);
   for (unsigned i = 0; i < d_subtheories.size(); ++i) {
     EqualityStatus status = d_subtheories[i]->getEqualityStatus(a, b);
     if (status != EQUALITY_UNKNOWN) {
@@ -736,7 +738,7 @@ void TheoryBV::enableCoreTheorySlicer() {
   d_isCoreTheory = true;
   if (d_subtheoryMap.find(SUB_CORE) != d_subtheoryMap.end()) {
     CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE];
-    core->enableSlicer(); 
+    core->enableSlicer();
   }
 }
 
@@ -746,7 +748,7 @@ void TheoryBV::ppStaticLearn(TNode in, NodeBuilder<>& learned) {
     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)) {
@@ -754,7 +756,7 @@ void TheoryBV::ppStaticLearn(TNode in, NodeBuilder<>& learned) {
       TNode s = in[0].getKind() == kind::BITVECTOR_PLUS ? in[1] : in[0];
 
       if(p.getNumChildren() == 2
-         && p[0].getKind()  == kind::BITVECTOR_SHL 
+         && p[0].getKind()  == kind::BITVECTOR_SHL
          && p[1].getKind()  == kind::BITVECTOR_SHL ){
         unsigned size = utils::getSize(s);
         Node one = utils::mkConst(size, 1u);
@@ -796,14 +798,18 @@ bool TheoryBV::applyAbstraction(const std::vector<Node>& assertions, std::vector
 void TheoryBV::setConflict(Node conflict) {
   if (options::bvAbstraction()) {
     Node new_conflict = d_abstractionModule->simplifyConflict(conflict);
-      
+
     std::vector<Node> lemmas;
-    lemmas.push_back(new_conflict); 
+    lemmas.push_back(new_conflict);
     d_abstractionModule->generalizeConflict(new_conflict, lemmas);
     for (unsigned i = 0; i < lemmas.size(); ++i) {
-      lemma(utils::mkNode(kind::NOT, lemmas[i])); 
+      lemma(utils::mkNode(kind::NOT, lemmas[i]));
     }
   }
   d_conflict = true;
   d_conflictNode = conflict;
 }
+
+} /* namespace CVC4::theory::bv */
+} /* namespace CVC4::theory */
+} /* namespace CVC4 */
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 4b3649a86..8ded63c28 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -23,6 +23,7 @@
 #include "context/cdlist.h"
 #include "context/context.h"
 #include "expr/statistics_registry.h"
+#include "smt/smt_globals.h"
 #include "theory/bv/bv_subtheory.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/theory.h"
@@ -35,10 +36,10 @@ namespace bv {
 class CoreSolver;
 class InequalitySolver;
 class AlgebraicSolver;
-class BitblastSolver; 
+class BitblastSolver;
 
 class EagerBitblastSolver;
-  
+
 class AbstractionModule;
 
 class TheoryBV : public Theory {
@@ -49,14 +50,14 @@ class TheoryBV : public Theory {
   /** Context dependent set of atoms we already propagated */
   context::CDHashSet<Node, NodeHashFunction> d_alreadyPropagatedSet;
   context::CDHashSet<Node, NodeHashFunction> d_sharedTermsSet;
-  
-  std::vector<SubtheorySolver*> d_subtheories;
-  __gnu_cxx::hash_map<SubTheory, SubtheorySolver*, std::hash<int> > d_subtheoryMap; 
 
+  std::vector<SubtheorySolver*> d_subtheories;
+  __gnu_cxx::hash_map<SubTheory, SubtheorySolver*, std::hash<int> > d_subtheoryMap;
 
 public:
 
-  TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo);
+  TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, SmtGlobals* globals);
+
   ~TheoryBV();
 
   void setMasterEqualityEngine(eq::EqualityEngine* eq);
@@ -80,13 +81,14 @@ public:
   PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
 
   void enableCoreTheorySlicer();
-  
+
   Node ppRewrite(TNode t);
 
   void ppStaticLearn(TNode in, NodeBuilder<>& learned);
-  
+
   void presolve();
-  bool applyAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions); 
+  bool applyAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions);
+
 private:
 
   class Statistics {