Refactoring Options Handler & Library Cycle Breaking

What to Know As a User:
A number of files have moved. Users that include files in the public API in more refined ways than using #include <cvc4.h> should consult which files have moved. Note though that some files may move again after being cleaned up. A number of small tweaks have been made to the swig interfaces that may cause issues. Please file bug reports for any problems.

The Problem:
The build order of CVC4 used to be [roughly] specified as:
  options < expr < util < libcvc4 < parsers < main
Each of these had their own directories and their own Makefile.am files. With the exception of the util/ directory, each of the subdirectories built exactly one convenience library. The util/ directory additionally built a statistics library. While the order above was partially correct, the build order was more complicated as options/Makefile.am executed building the sources for expr/Makefile.am as part of its BUILT_SOURCES phase. This options/Makefile.am also build the options/h and options.cpp files in other directories. There were cyclical library dependencies between the first four above libraries. All of these aspects combined to make options extremely brittle and hard to develop. Maintaining these between clang versus gcc, and bazel versus autotools has become increasing unpredictable.

The Solution:
To address these cyclic build problems, I am simplifying the build process. Here are the main things that have to happen:
1. util/ will be split into 3 separate directories: base, util, and smt_util. Each will have their own library and Makefile.am file.
2. Dependencies for options/ will be moved into options/. If a type appears as an option, this file will be moved into options.
3. All of the old options_handlers.h files have been refactored.
4. Some files have moved from util into expr/ to resolve cycles. Some of these moves are temporary.
5. I am removing the libstatistics library.

The constraints that the CVC4 build system will eventually satisfy are:
- The include order for both the .h and .cpp files for a directory must respect the order libraries are built. For example, a file in options/ cannot include from the expr/ directory. This includes built source files such as those coming from */kinds files and */options files.
- The types definitions must also respect the build order. Forward type declarations will be allowed in exceptional, justified cases.
- The Makefile.am for a directory cannot generate a file outside of the directory it controls. (Or call another Makefile.am except through subdirectory calls.)
- One library per Makefile.am.
- No extra copies of libraries will be built for the purpose of distinguishing between external and internal visibility in libraries for building parser/ or main/ libraries and binaries. Any function used by parser/ and main/ will be labeled with CVC4_PUBLIC and be in a public API. (AFAICT, libstatistics was being built exactly to skirt this.)

The build order of CVC4 can now be [roughly] specified as
  base < options < util < expr < smt_util < libcvc4 < parsers < main
The distinction between "base < options < util < expr" are currently clean. The relationship between expr and the subsequent directories/libraries are not yet clean.

More details about the directories:

base/
The new directory base/ contains the shared utilities that are absolutely crucial to starting cvc4. The list currently includes just: cvc4_assert.{h,cpp}, output.{h,cpp}, exception.{h,cpp}, and tls.{h, h.in, cpp}. These are things that are required everywhere.

options/
The options/ directory is self contained.
- It contains all of the enums that appear as options. This includes things like theory/bv/bitblast_mode.h .
- There are exactly 4 classes that handled currently using forward declarations currently to this: LogicInfo, LemmaInputChannel, LemmaOutputChannel, and CommandSequence. These will all be removed from options.
- Functionality of the options_handlers.h files has been moved into smt/smt_options_handler.h. The options library itself only uses an interface class defined in options/options_handler_interface.h. We are now using virtual dispatch to avoid using inlined functions as was previously done.
- The */options_handlers.h files have been removed.
- The generated smt/smt_options.cpp file has been be replaced by pushing the functionality that was generated into: options/options_handler_{get,set}_option_template.cpp . The non-generated functionality was moved into smt_engine.cpp.
- All of the options files have been moved from their directories into options/. This means includes like theory/arith/options.h have changed to change to options/arith_options.h .

util/
The util/ directory continues to contain core utility classes that may be used [almost] everywhere. The exception is that these are not used by options/ or base/. This includes things like rational and integer. These may not use anything in expr/ or libcvc4. A number of files have been moved out of this directory as they have cyclic dependencies graph with exprs and types. The build process up to this directory is currently clean.

expr/
The expr/ directory continues to be the home of expressions. The major change is files moving from util/ moving into expr/. The reason for this is that these files form a cycle with files in expr/.
- An example is datatype.h. This includes "expr/expr.h", "expr/type.h" while "expr/command.h" includes datatype.h.
- Another example is predicate.h. This uses expr.h and is also declared in a kinds file and thus appears in kinds.h.
- The rule of thumb is if expr/ pulls it in it needs to be independent of expr/, in which case it is in util/, or it is not, in which case it is pulled into expr/.
- Some files do not have a strong justification currently. Result, ResourceManager and SExpr can be moved back into util/ once the iostream manipulation routines are refactored out of the Node and Expr classes.
- Note the kinds files are expected to remain in the theory/ directories. These are only read in order to build sources.
- This directory is not yet clean. It contains forward references into libcvc4 such as the printer. It also makes some classes used by main/ and parser CVC4_PUBLIC.

smt_util/
The smt_util/ directory contains those utility classes which require exprs, but expr/ does not require them. These are mostly utilities for working with expressions and nodes. Examples include ite_removal.h, LemmaInputChannel and LemmaOutputChannel.

What is up next:
- A number of new #warning "TODO: ..." items have been scattered throughout the code as reminders to myself. Help with these issues is welcomed.
- The expr/ directory needs to be cleaned up in a similar to options/. Before this happens statistics needs to be cleaned up.

28 files changed, 148 insertions, 484 deletions

diff --git a/src/theory/bv/abstraction.cpp b/src/theory/bv/abstraction.cpp
index c414ac749..f05520306 100644
--- a/src/theory/bv/abstraction.cpp
+++ b/src/theory/bv/abstraction.cpp
@@ -12,12 +12,13 @@
  ** [[ Add lengthier description here ]]
  ** \todo document this file
  **/
-
 #include "theory/bv/abstraction.h"
+
+#include "options/bv_options.h"
+#include "smt_util/dump.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/rewriter.h"
-#include "theory/bv/options.h"
-#include "util/dump.h"
+
 
 using namespace CVC4;
 using namespace CVC4::theory;
@@ -28,10 +29,10 @@ using namespace std;
 using namespace CVC4::theory::bv::utils;
 
 bool AbstractionModule::applyAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions) {
-  Debug("bv-abstraction") << "AbstractionModule::applyAbstraction\n"; 
+  Debug("bv-abstraction") << "AbstractionModule::applyAbstraction\n";
 
   TimerStat::CodeTimer abstractionTimer(d_statistics.d_abstractionTime);
-    
+
   for (unsigned i = 0; i < assertions.size(); ++i) {
     if (assertions[i].getKind() == kind::OR) {
       for (unsigned j = 0; j < assertions[i].getNumChildren(); ++j) {
diff --git a/src/theory/bv/abstraction.h b/src/theory/bv/abstraction.h
index 2e86c834d..6b4d5a7dc 100644
--- a/src/theory/bv/abstraction.h
+++ b/src/theory/bv/abstraction.h
@@ -14,22 +14,22 @@
  ** Bitvector theory.
  **/
 
+#include "cvc4_private.h"
 
 #ifndef __CVC4__THEORY__BV__ABSTRACTION_H
 #define __CVC4__THEORY__BV__ABSTRACTION_H
 
-#include "cvc4_private.h"
 #include <ext/hash_map>
 #include <ext/hash_set>
+
 #include "expr/node.h"
+#include "expr/statistics_registry.h"
 #include "theory/substitutions.h"
-#include "util/statistics_registry.h"
 
 namespace CVC4 {
 namespace theory {
 namespace bv {
 
-
 typedef std::vector<TNode> ArgsVec;
 
 class AbstractionModule {
diff --git a/src/theory/bv/aig_bitblaster.cpp b/src/theory/bv/aig_bitblaster.cpp
index 6270995ef..f07bd49f7 100644
--- a/src/theory/bv/aig_bitblaster.cpp
+++ b/src/theory/bv/aig_bitblaster.cpp
@@ -14,11 +14,11 @@
  ** Bitblaster for the lazy bv solver. 
  **/
 
-#include "cvc4_private.h"
 #include "bitblaster_template.h"
+#include "cvc4_private.h"
+#include "options/bv_options.h"
 #include "prop/cnf_stream.h"
 #include "prop/sat_solver_factory.h"
-#include "theory/bv/options.h"
 
 
 #ifdef CVC4_USE_ABC
diff --git a/src/theory/bv/bitblast_mode.cpp b/src/theory/bv/bitblast_mode.cpp
deleted file mode 100644
index 51c0290af..000000000
--- a/src/theory/bv/bitblast_mode.cpp
+++ /dev/null
@@ -1,55 +0,0 @@
-/*********************                                                        */
-/*! \file bitblast_mode.cpp
- ** \verbatim
- ** Original author: Liana Hadarean
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Bitblast modes for bit-vector solver.
- **
- ** Bitblast modes for bit-vector solver.
- **/
-
-#include "theory/bv/bitblast_mode.h"
-
-namespace CVC4 {
-
-std::ostream& operator<<(std::ostream& out, theory::bv::BitblastMode mode) {
-  switch(mode) {
-  case theory::bv::BITBLAST_MODE_LAZY:
-    out << "BITBLAST_MODE_LAZY"; 
-    break;
-  case theory::bv::BITBLAST_MODE_EAGER:
-    out << "BITBLAST_MODE_EAGER";
-    break;
-  default:
-    out << "BitblastMode:UNKNOWN![" << unsigned(mode) << "]";
-  }
-
-  return out;
-}
-
-std::ostream& operator<<(std::ostream& out, theory::bv::BvSlicerMode mode) {
-  switch(mode) {
-  case theory::bv::BITVECTOR_SLICER_ON:
-    out << "BITVECTOR_SLICER_ON"; 
-    break;
-  case theory::bv::BITVECTOR_SLICER_OFF:
-    out << "BITVECTOR_SLICER_OFF";
-    break;
-  case theory::bv::BITVECTOR_SLICER_AUTO:
-    out << "BITVECTOR_SLICER_AUTO";
-    break;
-  default:
-    out << "BvSlicerMode:UNKNOWN![" << unsigned(mode) << "]";
-  }
-
-  return out;
-}
-
-
-}/* CVC4 namespace */
diff --git a/src/theory/bv/bitblast_mode.h b/src/theory/bv/bitblast_mode.h
deleted file mode 100644
index 89ecdc381..000000000
--- a/src/theory/bv/bitblast_mode.h
+++ /dev/null
@@ -1,72 +0,0 @@
-/*********************                                                        */
-/*! \file bitblast_mode.h
- ** \verbatim
- ** Original author: Liana Hadarean
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Bitblasting modes for bit-vector solver.
- **
- ** Bitblasting modes for bit-vector solver.
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY__BV__BITBLAST_MODE_H
-#define __CVC4__THEORY__BV__BITBLAST_MODE_H
-
-#include <iostream>
-
-namespace CVC4 {
-namespace theory {
-namespace bv {
-
-/** Enumeration of bit-blasting modes */
-enum BitblastMode {
-
-  /**
-   * Lazy bit-blasting that separates boolean reasoning
-   * from term reasoning.
-   */
-  BITBLAST_MODE_LAZY,
-
-  /**
-   * Bit-blast eagerly to the bit-vector SAT solver.
-   */
-  BITBLAST_MODE_EAGER
-};/* enum BitblastMode */
-
-/** Enumeration of bit-vector equality slicer mode */
-enum BvSlicerMode {
-
-  /**
-   * Force the slicer on. 
-   */
-  BITVECTOR_SLICER_ON, 
-
-  /**
-   * Slicer off. 
-   */
-  BITVECTOR_SLICER_OFF, 
-
-  /**
-   * Auto enable slicer if problem has only equalities.
-   */
-  BITVECTOR_SLICER_AUTO
-
-};/* enum BvSlicerMode */
-
-
-}/* CVC4::theory::bv namespace */
-}/* CVC4::theory namespace */
-
-std::ostream& operator<<(std::ostream& out, theory::bv::BitblastMode mode) CVC4_PUBLIC;
-std::ostream& operator<<(std::ostream& out, theory::bv::BvSlicerMode mode) CVC4_PUBLIC;
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4__THEORY__BV__BITBLAST_MODE_H */
diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h
index d42c4a8c9..b93d0561e 100644
--- a/src/theory/bv/bitblaster_template.h
+++ b/src/theory/bv/bitblaster_template.h
@@ -23,12 +23,13 @@
 #include "expr/node.h"
 #include <vector>
 #include <ext/hash_map>
+
 #include "context/cdhashmap.h"
 #include "bitblast_strategies_template.h"
+#include "expr/resource_manager.h"
 #include "prop/sat_solver.h"
 #include "theory/valuation.h"
 #include "theory/theory_registrar.h"
-#include "util/resource_manager.h"
 
 class Abc_Obj_t_;
 typedef Abc_Obj_t_ Abc_Obj_t;
diff --git a/src/theory/bv/bv_eager_solver.cpp b/src/theory/bv/bv_eager_solver.cpp
index 0c087ddb9..66b1c4182 100644
--- a/src/theory/bv/bv_eager_solver.cpp
+++ b/src/theory/bv/bv_eager_solver.cpp
@@ -14,9 +14,9 @@
  ** Eager bit-blasting solver.
  **/
 
-#include "theory/bv/bv_eager_solver.h"
+#include "options/bv_options.h"
 #include "theory/bv/bitblaster_template.h"
-#include "theory/bv/options.h"
+#include "theory/bv/bv_eager_solver.h"
 
 using namespace std;
 using namespace CVC4;
diff --git a/src/theory/bv/bv_quick_check.h b/src/theory/bv/bv_quick_check.h
index 01d772cb9..261a0b1c4 100644
--- a/src/theory/bv/bv_quick_check.h
+++ b/src/theory/bv/bv_quick_check.h
@@ -22,10 +22,10 @@
 #include <vector>
 #include <ext/hash_map>
 
-#include "expr/node.h"
 #include "context/cdo.h"
+#include "expr/node.h"
+#include "expr/statistics_registry.h"
 #include "prop/sat_solver_types.h"
-#include "util/statistics_registry.h"
 #include "theory/bv/theory_bv_utils.h"
 
 namespace CVC4 {
diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp
index e6e3120f5..4531be040 100644
--- a/src/theory/bv/bv_subtheory_algebraic.cpp
+++ b/src/theory/bv/bv_subtheory_algebraic.cpp
@@ -14,14 +14,13 @@
  ** Algebraic solver.
  **/
 
-#include "util/boolean_simplification.h"
-#include "theory/theory_model.h"
-
-#include "theory/bv/options.h"
-#include "theory/bv/theory_bv.h"
-#include "theory/bv/bv_subtheory_algebraic.h"
+#include "options/bv_options.h"
+#include "smt_util/boolean_simplification.h"
 #include "theory/bv/bv_quick_check.h"
+#include "theory/bv/bv_subtheory_algebraic.h"
+#include "theory/bv/theory_bv.h"
 #include "theory/bv/theory_bv_utils.h"
+#include "theory/theory_model.h"
 
 
 using namespace std;
diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp
index 7e3ed46c8..1d0342c08 100644
--- a/src/theory/bv/bv_subtheory_bitblast.cpp
+++ b/src/theory/bv/bv_subtheory_bitblast.cpp
@@ -14,24 +14,24 @@
  ** Algebraic solver.
  **/
 
+#include "decision/decision_attributes.h"
+#include "options/decision_options.h"
+#include "options/bv_options.h"
+#include "theory/bv/abstraction.h"
+#include "theory/bv/bitblaster_template.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 "theory/bv/bitblaster_template.h"
-#include "theory/bv/bv_quick_check.h"
-#include "theory/bv/options.h"
-#include "theory/bv/abstraction.h"
-#include "theory/decision_attributes.h"
-#include "decision/options.h"
-
 
 using namespace std;
-using namespace CVC4;
 using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::bv;
 using namespace CVC4::theory::bv::utils;
 
+namespace CVC4 {
+namespace theory {
+namespace bv {
+
 BitblastSolver::BitblastSolver(context::Context* c, TheoryBV* bv)
   : SubtheorySolver(c, bv),
     d_bitblaster(new TLazyBitblaster(c, bv, "lazy")),
@@ -78,8 +78,8 @@ void BitblastSolver::preRegister(TNode node) {
     CodeTimer weightComputationTime(d_bv->d_statistics.d_weightComputationTimer);
     d_bitblastQueue.push_back(node);
     if ((options::decisionUseWeight() || options::decisionThreshold() != 0) &&
-        !node.hasAttribute(theory::DecisionWeightAttr())) {
-      node.setAttribute(theory::DecisionWeightAttr(),computeAtomWeight(node));
+        !node.hasAttribute(decision::DecisionWeightAttr())) {
+      node.setAttribute(decision::DecisionWeightAttr(),computeAtomWeight(node));
     }
   }
 }
@@ -277,3 +277,7 @@ void BitblastSolver::setConflict(TNode conflict) {
   }
   d_bv->setConflict(final_conflict);
 }
+
+}/* namespace CVC4::theory::bv */
+}/* namespace CVC4::theory */
+}/* namespace CVC4 */
diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index 6ae0ffb71..ef4d24e82 100644
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -16,12 +16,12 @@
 
 #include "theory/bv/bv_subtheory_core.h"
 
+#include "options/bv_options.h"
+#include "options/smt_options.h"
+#include "theory/bv/slicer.h"
 #include "theory/bv/theory_bv.h"
 #include "theory/bv/theory_bv_utils.h"
-#include "theory/bv/slicer.h"
 #include "theory/theory_model.h"
-#include "theory/bv/options.h"
-#include "smt/options.h"
 
 using namespace std;
 using namespace CVC4;
diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp
index 55dcbb03a..054e43b7c 100644
--- a/src/theory/bv/bv_subtheory_inequality.cpp
+++ b/src/theory/bv/bv_subtheory_inequality.cpp
@@ -15,10 +15,11 @@
  **/
 
 #include "theory/bv/bv_subtheory_inequality.h"
+
+#include "options/smt_options.h"
 #include "theory/bv/theory_bv.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/theory_model.h"
-#include "smt/options.h"
 
 using namespace std;
 using namespace CVC4;
@@ -232,4 +233,3 @@ InequalitySolver::Statistics::Statistics()
 InequalitySolver::Statistics::~Statistics() {
   StatisticsRegistry::unregisterStat(&d_numCallstoCheck);
 }
-
diff --git a/src/theory/bv/bv_to_bool.cpp b/src/theory/bv/bv_to_bool.cpp
index 06a1d4a44..00e6f9ff8 100644
--- a/src/theory/bv/bv_to_bool.cpp
+++ b/src/theory/bv/bv_to_bool.cpp
@@ -13,11 +13,10 @@
  **
  ** Preprocessing pass that lifts bit-vectors of size 1 to booleans. 
  **/
-
-
-#include "util/node_visitor.h"
 #include "theory/bv/bv_to_bool.h"
 
+#include "smt_util/node_visitor.h"
+
 using namespace std;
 using namespace CVC4;
 using namespace CVC4::theory;
diff --git a/src/theory/bv/bv_to_bool.h b/src/theory/bv/bv_to_bool.h
index b266b591b..46b2d5c6e 100644
--- a/src/theory/bv/bv_to_bool.h
+++ b/src/theory/bv/bv_to_bool.h
@@ -15,12 +15,13 @@
  **/
 
 #include "cvc4_private.h"
-#include "theory/bv/theory_bv_utils.h"
-#include "util/statistics_registry.h"
 
 #ifndef __CVC4__THEORY__BV__BV_TO_BOOL_H
 #define __CVC4__THEORY__BV__BV_TO_BOOL_H
 
+#include "expr/statistics_registry.h"
+#include "theory/bv/theory_bv_utils.h"
+
 namespace CVC4 {
 namespace theory {
 namespace bv {
diff --git a/src/theory/bv/eager_bitblaster.cpp b/src/theory/bv/eager_bitblaster.cpp
index 3f076bd4c..ec2bfd9c0 100644
--- a/src/theory/bv/eager_bitblaster.cpp
+++ b/src/theory/bv/eager_bitblaster.cpp
@@ -9,27 +9,31 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
- ** \brief 
+ ** \brief
  **
- ** Bitblaster for the eager bv solver. 
+ ** Bitblaster for the eager bv solver.
  **/
 
 #include "cvc4_private.h"
 
-#include "theory/bv/bitblaster_template.h"
-#include "theory/bv/options.h"
-#include "theory/theory_model.h"
-#include "theory/bv/theory_bv.h"
+#include "options/bv_options.h"
 #include "prop/cnf_stream.h"
 #include "prop/sat_solver_factory.h"
+#include "theory/bv/bitblaster_template.h"
+#include "theory/bv/theory_bv.h"
+#include "theory/theory_model.h"
 
 
 using namespace CVC4;
 using namespace CVC4::theory;
-using namespace CVC4::theory::bv; 
+using namespace CVC4::theory::bv;
+
+namespace CVC4 {
+namespace theory {
+namespace bv {
 
 void BitblastingRegistrar::preRegister(Node n) {
-  d_bitblaster->bbAtom(n); 
+  d_bitblaster->bbAtom(n);
 };
 
 EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv)
@@ -38,12 +42,12 @@ EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv)
   , d_bbAtoms()
   , d_variables()
 {
-  d_bitblastingRegistrar = new BitblastingRegistrar(this); 
+  d_bitblastingRegistrar = new BitblastingRegistrar(this);
   d_nullContext = new context::Context();
 
   d_satSolver = prop::SatSolverFactory::createMinisat(d_nullContext, "EagerBitblaster");
   d_cnfStream = new prop::TseitinCnfStream(d_satSolver, d_bitblastingRegistrar, d_nullContext);
-  
+
   MinisatEmptyNotify* notify = new MinisatEmptyNotify();
   d_satSolver->setNotify(notify);
 }
@@ -68,7 +72,7 @@ void EagerBitblaster::bbFormula(TNode node) {
 void EagerBitblaster::bbAtom(TNode node) {
   node = node.getKind() == kind::NOT?  node[0] : node;
   if (node.getKind() == kind::BITVECTOR_BITOF)
-    return; 
+    return;
   if (hasBBAtom(node)) {
     return;
   }
@@ -83,18 +87,18 @@ void EagerBitblaster::bbAtom(TNode node) {
   // asserting that the atom is true iff the definition holds
   Node atom_definition = utils::mkNode(kind::IFF, node, atom_bb);
 
-  AlwaysAssert (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER); 
+  AlwaysAssert (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER);
   storeBBAtom(node, atom_definition);
   d_cnfStream->convertAndAssert(atom_definition, false, false, RULE_INVALID, TNode::null());
 }
 
 void EagerBitblaster::storeBBAtom(TNode atom, Node atom_bb) {
   // no need to store the definition for the lazy bit-blaster
-  d_bbAtoms.insert(atom); 
+  d_bbAtoms.insert(atom);
 }
 
 bool EagerBitblaster::hasBBAtom(TNode atom) const {
-  return d_bbAtoms.find(atom) != d_bbAtoms.end(); 
+  return d_bbAtoms.find(atom) != d_bbAtoms.end();
 }
 
 void EagerBitblaster::bbTerm(TNode node, Bits& bits) {
@@ -161,7 +165,7 @@ Node EagerBitblaster::getModelFromSatSolver(TNode a, bool fullModel) {
   if (!hasBBTerm(a)) {
     return fullModel? utils::mkConst(utils::getSize(a), 0u) : Node();
   }
-  
+
   Bits bits;
   getBBTerm(a, bits);
   Integer value(0);
@@ -191,9 +195,9 @@ void EagerBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) {
         (var.isVar() && var.getType().isBoolean()))  {
       // only shared terms could not have been bit-blasted
       Assert (hasBBTerm(var) || isSharedTerm(var));
-      
+
       Node const_value = getModelFromSatSolver(var, fullModel);
-      
+
       if(const_value != Node()) {
         Debug("bitvector-model") << "EagerBitblaster::collectModelInfo (assert (= "
                                  << var << " "
@@ -207,3 +211,7 @@ void EagerBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) {
 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; */
diff --git a/src/theory/bv/lazy_bitblaster.cpp b/src/theory/bv/lazy_bitblaster.cpp
index 59ecc7385..3c2b4ed78 100644
--- a/src/theory/bv/lazy_bitblaster.cpp
+++ b/src/theory/bv/lazy_bitblaster.cpp
@@ -14,17 +14,17 @@
  ** Bitblaster for the lazy bv solver. 
  **/
 
-#include "cvc4_private.h"
 #include "bitblaster_template.h"
-#include "theory_bv_utils.h"
-#include "theory/rewriter.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 "theory/bv/abstraction.h"
 #include "theory/bv/theory_bv.h"
-#include "theory/bv/options.h"
+#include "theory/rewriter.h"
 #include "theory/theory_model.h"
-#include "theory/bv/abstraction.h"
+#include "theory_bv_utils.h"
 
 using namespace CVC4;
 using namespace CVC4::theory;
diff --git a/src/theory/bv/options b/src/theory/bv/options
deleted file mode 100644
index eba4608d2..000000000
--- a/src/theory/bv/options
+++ /dev/null
@@ -1,69 +0,0 @@
-#
-# Option specification file for CVC4
-# See src/options/base_options for a description of this file format
-#
-
-module BV "theory/bv/options.h" Bitvector theory
-
-# Option to set the bit-blasting mode (lazy, eager)
-
-option bitblastMode bitblast --bitblast=MODE CVC4::theory::bv::BitblastMode :handler CVC4::theory::bv::stringToBitblastMode :default CVC4::theory::bv::BITBLAST_MODE_LAZY :read-write :include "theory/bv/bitblast_mode.h" :handler-include "theory/bv/options_handlers.h"
- choose bitblasting mode, see --bitblast=help
-
-# Options for eager bit-blasting
- 
-option bitvectorAig --bitblast-aig bool :default false :predicate CVC4::theory::bv::abcEnabledBuild CVC4::theory::bv::setBitblastAig :predicate-include "theory/bv/options_handlers.h" :read-write
- bitblast by first converting to AIG (implies --bitblast=eager)
-expert-option bitvectorAigSimplifications --bv-aig-simp=COMMAND std::string :default "" :predicate CVC4::theory::bv::abcEnabledBuild :read-write :link --bitblast-aig :link-smt bitblast-aig
- abc command to run AIG simplifications (implies --bitblast-aig, default is "balance;drw")
-
-# Options for lazy bit-blasting
-
-option bitvectorPropagate --bv-propagate bool :default true :read-write :link --bitblast=lazy 
- use bit-vector propagation in the bit-blaster
-
-option bitvectorEqualitySolver --bv-eq-solver bool :default true :read-write :link --bitblast=lazy
- use the equality engine for the bit-vector theory (only if --bitblast=lazy)
-
-option bitvectorEqualitySlicer --bv-eq-slicer=MODE CVC4::theory::bv::BvSlicerMode :handler CVC4::theory::bv::stringToBvSlicerMode :default CVC4::theory::bv::BITVECTOR_SLICER_OFF :read-write :include "theory/bv/bitblast_mode.h" :handler-include "theory/bv/options_handlers.h" :read-write :link --bv-eq-solver
- turn on the slicing equality solver for the bit-vector theory (only if --bitblast=lazy)
-
-option bitvectorInequalitySolver --bv-inequality-solver bool :default true :read-write :link --bitblast=lazy
- turn on the inequality solver for the bit-vector theory (only if --bitblast=lazy)
-
-option bitvectorAlgebraicSolver --bv-algebraic-solver bool :default true :read-write :link --bitblast=lazy
- turn on the algebraic solver for the bit-vector theory (only if --bitblast=lazy)
- 
-expert-option bitvectorAlgebraicBudget --bv-algebraic-budget unsigned :default 1500 :read-write :link --bv-algebraic-solver
- the budget allowed for the algebraic solver in number of SAT conflicts
-
-# General options
-
-option bitvectorToBool --bv-to-bool bool :default false :read-write 
- lift bit-vectors of size 1 to booleans when possible
-
-option bitvectorDivByZeroConst --bv-div-zero-const bool :default false :read-write
- always return -1 on division by zero
-
-expert-option bvExtractArithRewrite --bv-extract-arith bool :default false :read-write
- enable rewrite pushing extract [i:0] over arithmetic operations (can blow up)
- 
-expert-option bvAbstraction --bv-abstraction bool :default false :read-write
- mcm benchmark abstraction 
-
-expert-option skolemizeArguments --bv-skolemize bool :default false :read-write 
- skolemize arguments for bv abstraction (only does something if --bv-abstraction is on)
-
-expert-option bvNumFunc --bv-num-func=NUM unsigned :default 1
- number of function symbols in conflicts that are generalized
-
-expert-option bvEagerExplanations --bv-eager-explanations bool :default false :read-write
- compute bit-blasting propagation explanations eagerly
-
-expert-option bitvectorQuickXplain --bv-quick-xplain bool :default false
- minimize bv conflicts using the QuickXplain algorithm
- 
-expert-option bvIntroducePow2 --bv-intro-pow2 bool :default false
- introduce bitvector powers of two as a preprocessing pass
- 
-endmodule
diff --git a/src/theory/bv/options_handlers.h b/src/theory/bv/options_handlers.h
deleted file mode 100644
index a7a7101d2..000000000
--- a/src/theory/bv/options_handlers.h
+++ /dev/null
@@ -1,160 +0,0 @@
-/*********************                                                        */
-/*! \file options_handlers.h
- ** \verbatim
- ** Original author: Liana Hadarean
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Custom handlers and predicates for TheoryBV options
- **
- ** Custom handlers and predicates for TheoryBV options.
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY__BV__OPTIONS_HANDLERS_H
-#define __CVC4__THEORY__BV__OPTIONS_HANDLERS_H
-
-#include "theory/bv/bitblast_mode.h"
-#include "main/options.h"
-
-namespace CVC4 {
-namespace theory {
-namespace bv {
-
-inline void abcEnabledBuild(std::string option, bool value, SmtEngine* smt) throw(OptionException) {
-#ifndef CVC4_USE_ABC
-  if(value) {
-    std::stringstream ss;
-    ss << "option `" << option << "' requires an abc-enabled build of CVC4; this binary was not built with abc support";
-    throw OptionException(ss.str());
-  }
-#endif /* CVC4_USE_ABC */
-}
-
-inline void abcEnabledBuild(std::string option, std::string value, SmtEngine* smt) throw(OptionException) {
-#ifndef CVC4_USE_ABC
-  if(!value.empty()) {
-    std::stringstream ss;
-    ss << "option `" << option << "' requires an abc-enabled build of CVC4; this binary was not built with abc support";
-    throw OptionException(ss.str());
-  }
-#endif /* CVC4_USE_ABC */
-}
-
-static const std::string bitblastingModeHelp = "\
-Bit-blasting modes currently supported by the --bitblast option:\n\
-\n\
-lazy (default)\n\
-+ Separate boolean structure and term reasoning betwen the core\n\
-  SAT solver and the bv SAT solver\n\
-\n\
-eager\n\
-+ Bitblast eagerly to bv SAT solver\n\
-";
-
-inline BitblastMode stringToBitblastMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
-  if(optarg == "lazy") {
-    if (!options::bitvectorPropagate.wasSetByUser()) {
-      options::bitvectorPropagate.set(true);
-    }
-    if (!options::bitvectorEqualitySolver.wasSetByUser()) {
-      options::bitvectorEqualitySolver.set(true);
-    }
-    if (!options::bitvectorEqualitySlicer.wasSetByUser()) {
-      if (options::incrementalSolving() ||
-          options::produceModels()) {
-        options::bitvectorEqualitySlicer.set(BITVECTOR_SLICER_OFF);
-      } else {
-        options::bitvectorEqualitySlicer.set(BITVECTOR_SLICER_AUTO);
-      }
-    }
-    
-    if (!options::bitvectorInequalitySolver.wasSetByUser()) {
-      options::bitvectorInequalitySolver.set(true);
-    }
-    if (!options::bitvectorAlgebraicSolver.wasSetByUser()) {
-      options::bitvectorAlgebraicSolver.set(true);
-    }
-    return BITBLAST_MODE_LAZY;
-  } else if(optarg == "eager") {
-
-    if (options::incrementalSolving() &&
-        options::incrementalSolving.wasSetByUser()) {
-      throw OptionException(std::string("Eager bit-blasting does not currently support incremental mode. \n\
-                                         Try --bitblast=lazy"));
-    }
-    
-    if (!options::bitvectorToBool.wasSetByUser()) {
-      options::bitvectorToBool.set(true);
-    }
-
-    if (!options::bvAbstraction.wasSetByUser() &&
-        !options::skolemizeArguments.wasSetByUser()) {
-      options::bvAbstraction.set(true);
-      options::skolemizeArguments.set(true); 
-    }
-    return BITBLAST_MODE_EAGER;
-  } else if(optarg == "help") {
-    puts(bitblastingModeHelp.c_str());
-    exit(1);
-  } else {
-    throw OptionException(std::string("unknown option for --bitblast: `") +
-                          optarg + "'.  Try --bitblast=help.");
-  }
-}
-
-static const std::string bvSlicerModeHelp = "\
-Bit-vector equality slicer modes supported by the --bv-eq-slicer option:\n\
-\n\
-auto (default)\n\
-+ Turn slicer on if input has only equalities over core symbols\n\
-\n\
-on\n\
-+ Turn slicer on\n\
-\n\
-off\n\
-+ Turn slicer off\n\
-";
-
-inline BvSlicerMode stringToBvSlicerMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
-
-  if(optarg == "auto") {
-    return BITVECTOR_SLICER_AUTO;
-  } else if(optarg == "on") {
-    return BITVECTOR_SLICER_ON;
-  } else if(optarg == "off") {
-    return BITVECTOR_SLICER_OFF; 
-  } else if(optarg == "help") {
-    puts(bitblastingModeHelp.c_str());
-    exit(1);
-  } else {
-    throw OptionException(std::string("unknown option for --bv-eq-slicer: `") +
-                          optarg + "'.  Try --bv-eq-slicer=help.");
-  }
-}
-
-inline void setBitblastAig(std::string option, bool arg, SmtEngine* smt) throw(OptionException) {
-  if(arg) {
-    if(options::bitblastMode.wasSetByUser()) {
-      if(options::bitblastMode() != BITBLAST_MODE_EAGER) {
-        throw OptionException("bitblast-aig must be used with eager bitblaster");
-      }
-    } else {
-      options::bitblastMode.set(stringToBitblastMode("", "eager", smt));
-    }
-    if(!options::bitvectorAigSimplifications.wasSetByUser()) {
-      options::bitvectorAigSimplifications.set("balance;drw");
-    }
-  }
-}
-
-}/* CVC4::theory::bv namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__THEORY__BV__OPTIONS_HANDLERS_H */
diff --git a/src/theory/bv/slicer.cpp b/src/theory/bv/slicer.cpp
index a7587bedf..d31ff50d1 100644
--- a/src/theory/bv/slicer.cpp
+++ b/src/theory/bv/slicer.cpp
@@ -14,10 +14,11 @@
  ** Bitvector theory.
  **/
 
+#include "options/bv_options.h"
 #include "theory/bv/slicer.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/rewriter.h"
-#include "theory/bv/options.h"
+
 using namespace CVC4;
 using namespace CVC4::theory;
 using namespace CVC4::theory::bv;
diff --git a/src/theory/bv/slicer.h b/src/theory/bv/slicer.h
index 7b55054bc..5ecc2a788 100644
--- a/src/theory/bv/slicer.h
+++ b/src/theory/bv/slicer.h
@@ -16,17 +16,19 @@
 
 #include "cvc4_private.h"
 
+#include <math.h>
 
 #include <vector>
 #include <list>
 #include <ext/hash_map>
-#include <math.h>
 
-#include "util/bitvector.h"
-#include "util/statistics_registry.h"
-#include "util/index.h"
 #include "expr/node.h"
+#include "expr/statistics_registry.h"
 #include "theory/bv/theory_bv_utils.h"
+#include "util/bitvector.h"
+#include "util/index.h"
+
+
 #ifndef __CVC4__THEORY__BV__SLICER_BV_H
 #define __CVC4__THEORY__BV__SLICER_BV_H
 
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 95a483d34..4039fceec 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -11,24 +11,25 @@
  **
  ** [[ Add lengthier description here ]]
  ** \todo document this file
-**/
+ **/
 
-#include "smt/options.h"
 #include "theory/bv/theory_bv.h"
-#include "theory/bv/theory_bv_utils.h"
+
+#include "options/bv_options.h"
+#include "options/smt_options.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/slicer.h"
-#include "theory/valuation.h"
-#include "theory/bv/options.h"
 #include "theory/bv/theory_bv_rewrite_rules_normalization.h"
 #include "theory/bv/theory_bv_rewrite_rules_simplification.h"
-#include "theory/bv/bv_subtheory_core.h"
-#include "theory/bv/bv_subtheory_inequality.h"
-#include "theory/bv/bv_subtheory_algebraic.h"
-#include "theory/bv/bv_subtheory_bitblast.h"
-#include "theory/bv/bv_eager_solver.h"
 #include "theory/bv/theory_bv_rewriter.h"
+#include "theory/bv/theory_bv_utils.h"
 #include "theory/theory_model.h"
-#include "theory/bv/abstraction.h"
+#include "theory/valuation.h"
 
 using namespace CVC4;
 using namespace CVC4::theory;
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 193de55db..4b3649a86 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -14,18 +14,19 @@
  ** Bitvector theory.
  **/
 
+#include "cvc4_private.h"
+
 #ifndef __CVC4__THEORY__BV__THEORY_BV_H
 #define __CVC4__THEORY__BV__THEORY_BV_H
 
-#include "cvc4_private.h"
-#include "theory/theory.h"
-#include "context/context.h"
-#include "context/cdlist.h"
 #include "context/cdhashset.h"
+#include "context/cdlist.h"
+#include "context/context.h"
+#include "expr/statistics_registry.h"
+#include "theory/bv/bv_subtheory.h"
 #include "theory/bv/theory_bv_utils.h"
-#include "util/statistics_registry.h"
+#include "theory/theory.h"
 #include "util/hash.h"
-#include "theory/bv/bv_subtheory.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h
index 768923ee6..f5e2a2077 100644
--- a/src/theory/bv/theory_bv_rewrite_rules.h
+++ b/src/theory/bv/theory_bv_rewrite_rules.h
@@ -15,15 +15,17 @@
  ** \todo document this file
  **/
 
-#pragma once 
-
 #include "cvc4_private.h"
-#include "theory/theory.h"
+
+#pragma once
+
+#include <sstream>
+
 #include "context/context.h"
-#include "util/statistics_registry.h"
+#include "expr/statistics_registry.h"
+#include "smt_util/command.h"
 #include "theory/bv/theory_bv_utils.h"
-#include "expr/command.h"
-#include <sstream>
+#include "theory/theory.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
index bc1b92dce..0911b6ccf 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
@@ -19,6 +19,7 @@
 
 #pragma once
 
+#include "theory/rewriter.h"
 #include "theory/bv/theory_bv_rewrite_rules.h"
 #include "theory/bv/theory_bv_utils.h"
 
diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index f2adea411..2c82943ce 100644
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -15,15 +15,15 @@
  ** \todo document this file
  **/
 
-#include "theory/theory.h"
-#include "theory/bv/options.h"
-#include "theory/bv/theory_bv_rewriter.h"
+#include "options/bv_options.h"
 #include "theory/bv/theory_bv_rewrite_rules.h"
+#include "theory/bv/theory_bv_rewrite_rules_constant_evaluation.h"
 #include "theory/bv/theory_bv_rewrite_rules_core.h"
+#include "theory/bv/theory_bv_rewrite_rules_normalization.h"
 #include "theory/bv/theory_bv_rewrite_rules_operator_elimination.h"
-#include "theory/bv/theory_bv_rewrite_rules_constant_evaluation.h"
 #include "theory/bv/theory_bv_rewrite_rules_simplification.h"
-#include "theory/bv/theory_bv_rewrite_rules_normalization.h"
+#include "theory/bv/theory_bv_rewriter.h"
+#include "theory/theory.h"
 
 using namespace CVC4;
 using namespace CVC4::theory;
@@ -682,6 +682,3 @@ Node TheoryBVRewriter::eliminateBVSDiv(TNode node) {
     >::apply(node);
   return result; 
 }
-
-
-
diff --git a/src/theory/bv/theory_bv_rewriter.h b/src/theory/bv/theory_bv_rewriter.h
index 3f0fa8194..7e5d429fd 100644
--- a/src/theory/bv/theory_bv_rewriter.h
+++ b/src/theory/bv/theory_bv_rewriter.h
@@ -20,8 +20,8 @@
 #ifndef __CVC4__THEORY__BV__THEORY_BV_REWRITER_H
 #define __CVC4__THEORY__BV__THEORY_BV_REWRITER_H
 
+#include "expr/statistics_registry.h"
 #include "theory/rewriter.h"
-#include "util/statistics_registry.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/bv/theory_bv_utils.cpp b/src/theory/bv/theory_bv_utils.cpp
index d2025b1b8..f57ccec48 100644
--- a/src/theory/bv/theory_bv_utils.cpp
+++ b/src/theory/bv/theory_bv_utils.cpp
@@ -16,24 +16,23 @@
  **/
 
 #include "theory/bv/theory_bv_utils.h"
-#include "theory/decision_attributes.h"
 #include "theory/theory.h"
 
-using namespace CVC4;
-using namespace CVC4::theory;
-using namespace CVC4::theory::bv;
-using namespace CVC4::theory::bv::utils;
+namespace CVC4 {
+namespace theory {
+namespace bv {
+namespace utils {
 
-bool CVC4::theory::bv::utils::isCoreTerm(TNode term, TNodeBoolMap& cache) {
-  term = term.getKind() == kind::NOT ? term[0] : term; 
-  TNodeBoolMap::const_iterator it = cache.find(term); 
+bool isCoreTerm(TNode term, TNodeBoolMap& cache) {
+  term = term.getKind() == kind::NOT ? term[0] : term;
+  TNodeBoolMap::const_iterator it = cache.find(term);
   if (it != cache.end()) {
     return it->second;
   }
-    
+
   if (term.getNumChildren() == 0)
     return true;
-  
+
   if (theory::Theory::theoryOf(theory::THEORY_OF_TERM_BASED, term) == THEORY_BV) {
     Kind k = term.getKind();
     if (k != kind::CONST_BITVECTOR &&
@@ -52,21 +51,21 @@ bool CVC4::theory::bv::utils::isCoreTerm(TNode term, TNodeBoolMap& cache) {
       return false;
     }
   }
-  
-  cache[term]= true; 
+
+  cache[term]= true;
   return true;
 }
 
-bool CVC4::theory::bv::utils::isEqualityTerm(TNode term, TNodeBoolMap& cache) {
-  term = term.getKind() == kind::NOT ? term[0] : term; 
-  TNodeBoolMap::const_iterator it = cache.find(term); 
+bool isEqualityTerm(TNode term, TNodeBoolMap& cache) {
+  term = term.getKind() == kind::NOT ? term[0] : term;
+  TNodeBoolMap::const_iterator it = cache.find(term);
   if (it != cache.end()) {
     return it->second;
   }
-    
+
   if (term.getNumChildren() == 0)
     return true;
-  
+
   if (theory::Theory::theoryOf(theory::THEORY_OF_TERM_BASED, term) == THEORY_BV) {
     Kind k = term.getKind();
     if (k != kind::CONST_BITVECTOR &&
@@ -83,13 +82,13 @@ bool CVC4::theory::bv::utils::isEqualityTerm(TNode term, TNodeBoolMap& cache) {
       return false;
     }
   }
-  
-  cache[term]= true; 
+
+  cache[term]= true;
   return true;
 }
 
 
-uint64_t CVC4::theory::bv::utils::numNodes(TNode node, NodeSet& seen) {
+uint64_t numNodes(TNode node, NodeSet& seen) {
   if (seen.find(node) != seen.end())
     return 0;
 
@@ -101,9 +100,7 @@ uint64_t CVC4::theory::bv::utils::numNodes(TNode node, NodeSet& seen) {
   return size;
 }
 
-
-
-void CVC4::theory::bv::utils::collectVariables(TNode node, NodeSet& vars) {
+void collectVariables(TNode node, NodeSet& vars) {
   if (vars.find(node) != vars.end())
     return;
 
@@ -115,3 +112,8 @@ void CVC4::theory::bv::utils::collectVariables(TNode node, NodeSet& vars) {
     collectVariables(node[i], vars);
   }
 }
+
+}/* CVC4::theory::bv::utils namespace */
+}/* CVC4::theory::bv namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
diff --git a/src/theory/bv/type_enumerator.h b/src/theory/bv/type_enumerator.h
index 1d835dd23..db98ef66b 100644
--- a/src/theory/bv/type_enumerator.h
+++ b/src/theory/bv/type_enumerator.h
@@ -19,11 +19,11 @@
 #ifndef __CVC4__THEORY__BV__TYPE_ENUMERATOR_H
 #define __CVC4__THEORY__BV__TYPE_ENUMERATOR_H
 
+#include "expr/kind.h"
+#include "expr/type_node.h"
+#include "theory/type_enumerator.h"
 #include "util/bitvector.h"
 #include "util/integer.h"
-#include "theory/type_enumerator.h"
-#include "expr/type_node.h"
-#include "expr/kind.h"
 
 namespace CVC4 {
 namespace theory {