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.

36 files changed, 126 insertions, 118 deletions

diff --git a/test/system/ouroborous.cpp b/test/system/ouroborous.cpp
index 4fbabf5f1..fd06517a9 100644
--- a/test/system/ouroborous.cpp
+++ b/test/system/ouroborous.cpp
@@ -29,9 +29,9 @@
 #include <string>
 
 #include "expr/expr.h"
-#include "expr/command.h"
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
+#include "smt_util/command.h"
 
 using namespace CVC4;
 using namespace CVC4::parser;
diff --git a/test/system/smt2_compliance.cpp b/test/system/smt2_compliance.cpp
index f754adc0e..108e30b5c 100644
--- a/test/system/smt2_compliance.cpp
+++ b/test/system/smt2_compliance.cpp
@@ -14,16 +14,16 @@
  ** A test of SMT-LIBv2 commands, checks for compliant output.
  **/
 
+#include <cassert>
 #include <iostream>
 #include <sstream>
-#include <cassert>
 
-#include "smt/options.h"
-#include "parser/parser.h"
 #include "expr/expr_manager.h"
-#include "expr/command.h"
-#include "smt/smt_engine.h"
+#include "options/smt_options.h"
+#include "parser/parser.h"
 #include "parser/parser_builder.h"
+#include "smt/smt_engine.h"
+#include "smt_util/command.h"
 
 using namespace CVC4;
 using namespace CVC4::parser;
diff --git a/test/system/statistics.cpp b/test/system/statistics.cpp
index f955bd150..baa901540 100644
--- a/test/system/statistics.cpp
+++ b/test/system/statistics.cpp
@@ -19,8 +19,9 @@
 #include <sstream>
 
 #include "expr/expr.h"
+#include "expr/sexpr.h"
+#include "expr/statistics.h"
 #include "smt/smt_engine.h"
-#include "util/statistics.h"
 
 using namespace CVC4;
 using namespace std;
@@ -53,7 +54,8 @@ int main() {
     cout << "stat1 " << (*i).first << " is " << stats.getStatistic((*i).first) << endl;
     cout << "stat2 " << (*i).first << " is " << (*i).second << endl;
     if(smt.getStatistic((*i).first) != (*i).second) {
-      cout << "SMT engine reports different value for statistic " << (*i).first << ": " << smt.getStatistic((*i).first) << endl;
+      cout << "SMT engine reports different value for statistic "
+           << (*i).first << ": " << smt.getStatistic((*i).first) << endl;
       exit(1);
     }
     different = different || stats.getStatistic((*i).first) != (*i).second;
@@ -68,5 +70,3 @@ int main() {
 
   return r == Result::VALID ? 0 : 1;
 }
-
-
diff --git a/test/unit/context/cdlist_black.h b/test/unit/context/cdlist_black.h
index 5f473478c..5980972be 100644
--- a/test/unit/context/cdlist_black.h
+++ b/test/unit/context/cdlist_black.h
@@ -16,16 +16,14 @@
 
 #include <cxxtest/TestSuite.h>
 
-#include <vector>
 #include <iostream>
-
 #include <limits.h>
+#include <vector>
 
-#include "memory.h"
-
-#include "util/exception.h"
+#include "base/exception.h"
 #include "context/context.h"
 #include "context/cdlist.h"
+#include "memory.h"
 
 using namespace std;
 using namespace CVC4::context;
diff --git a/test/unit/context/cdmap_white.h b/test/unit/context/cdmap_white.h
index 84b8242b4..11642c3e9 100644
--- a/test/unit/context/cdmap_white.h
+++ b/test/unit/context/cdmap_white.h
@@ -16,8 +16,8 @@
 
 #include <cxxtest/TestSuite.h>
 
+#include "base/cvc4_assert.h"
 #include "context/cdhashmap.h"
-#include "util/cvc4_assert.h"
 
 using namespace std;
 using namespace CVC4;
diff --git a/test/unit/context/cdo_black.h b/test/unit/context/cdo_black.h
index fe04421b4..4ca01df85 100644
--- a/test/unit/context/cdo_black.h
+++ b/test/unit/context/cdo_black.h
@@ -16,12 +16,13 @@
 
 #include <cxxtest/TestSuite.h>
 
-#include <vector>
 #include <iostream>
-#include "context/context.h"
+#include <vector>
+
+#include "base/cvc4_assert.h"
 #include "context/cdlist.h"
 #include "context/cdo.h"
-#include "util/cvc4_assert.h"
+#include "context/context.h"
 
 using namespace std;
 using namespace CVC4;
diff --git a/test/unit/context/context_black.h b/test/unit/context/context_black.h
index f72cc05f4..d7148c990 100644
--- a/test/unit/context/context_black.h
+++ b/test/unit/context/context_black.h
@@ -16,12 +16,14 @@
 
 #include <cxxtest/TestSuite.h>
 
-#include <vector>
 #include <iostream>
-#include "context/context.h"
+#include <vector>
+
+#include "base/cvc4_assert.h"
 #include "context/cdlist.h"
 #include "context/cdo.h"
-#include "util/cvc4_assert.h"
+#include "context/context.h"
+
 
 using namespace std;
 using namespace CVC4;
diff --git a/test/unit/context/context_white.h b/test/unit/context/context_white.h
index 7ad70f061..10f603abd 100644
--- a/test/unit/context/context_white.h
+++ b/test/unit/context/context_white.h
@@ -16,9 +16,9 @@
 
 #include <cxxtest/TestSuite.h>
 
+#include "base/cvc4_assert.h"
 #include "context/context.h"
 #include "context/cdo.h"
-#include "util/cvc4_assert.h"
 
 using namespace std;
 using namespace CVC4;
diff --git a/test/unit/expr/attribute_white.h b/test/unit/expr/attribute_white.h
index 00ebc8b8d..df7e263d2 100644
--- a/test/unit/expr/attribute_white.h
+++ b/test/unit/expr/attribute_white.h
@@ -18,18 +18,18 @@
 
 #include <string>
 
-#include "expr/node_value.h"
+#include "base/cvc4_assert.h"
+#include "expr/attribute.h"
+#include "expr/node.h"
 #include "expr/node_builder.h"
 #include "expr/node_manager.h"
-#include "expr/attribute.h"
 #include "expr/node_manager_attributes.h"
-#include "expr/node.h"
+#include "expr/node_value.h"
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
 #include "theory/theory.h"
 #include "theory/theory_engine.h"
 #include "theory/uf/theory_uf.h"
-#include "util/cvc4_assert.h"
-#include "smt/smt_engine.h"
-#include "smt/smt_engine_scope.h"
 
 using namespace CVC4;
 using namespace CVC4::kind;
diff --git a/test/unit/expr/expr_manager_public.h b/test/unit/expr/expr_manager_public.h
index 727abe984..040bd7161 100644
--- a/test/unit/expr/expr_manager_public.h
+++ b/test/unit/expr/expr_manager_public.h
@@ -21,7 +21,7 @@
 
 #include "expr/expr_manager.h"
 #include "expr/expr.h"
-#include "util/exception.h"
+#include "base/exception.h"
 
 using namespace CVC4;
 using namespace CVC4::kind;
diff --git a/test/unit/expr/expr_public.h b/test/unit/expr/expr_public.h
index b70c51276..a83e53780 100644
--- a/test/unit/expr/expr_public.h
+++ b/test/unit/expr/expr_public.h
@@ -19,9 +19,10 @@
 #include <sstream>
 #include <string>
 
+#include "base/exception.h"
 #include "expr/expr_manager.h"
 #include "expr/expr.h"
-#include "util/exception.h"
+#include "smt/smt_options_handler.h"
 
 using namespace CVC4;
 using namespace CVC4::kind;
@@ -31,6 +32,7 @@ class ExprPublic : public CxxTest::TestSuite {
 private:
 
   Options opts;
+  smt::SmtOptionsHandler* d_handler;
 
   ExprManager* d_em;
 
@@ -53,10 +55,12 @@ public:
 
   void setUp() {
     try {
+      d_handler = new smt::SmtOptionsHandler(NULL);
+
       char *argv[2];
       argv[0] = strdup("");
       argv[1] = strdup("--output-language=ast");
-      opts.parseOptions(2, argv);
+      opts.parseOptions(2, argv, d_handler);
       free(argv[0]);
       free(argv[1]);
 
@@ -98,6 +102,7 @@ public:
       delete c_bool_and;
       delete b_bool;
       delete a_bool;
+      delete d_handler;
 
       delete d_em;
     } catch(Exception e) {
diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h
index 7d6ee523a..3a24057b2 100644
--- a/test/unit/expr/node_black.h
+++ b/test/unit/expr/node_black.h
@@ -25,6 +25,7 @@
 #include "expr/node_builder.h"
 #include "expr/node_manager.h"
 #include "expr/node.h"
+#include "smt/smt_options_handler.h"
 
 using namespace CVC4;
 using namespace CVC4::kind;
@@ -34,6 +35,7 @@ class NodeBlack : public CxxTest::TestSuite {
 private:
 
   Options opts;
+  smt::SmtOptionsHandler* d_handler;
   NodeManager* d_nodeManager;
   NodeManagerScope* d_scope;
   TypeNode* d_booleanType;
@@ -42,10 +44,13 @@ private:
 public:
 
   void setUp() {
+#warning "TODO: Discuss the effects of this change with Clark."
+    d_handler = new smt::SmtOptionsHandler(NULL);
+
     char *argv[2];
     argv[0] = strdup("");
     argv[1] = strdup("--output-language=ast");
-    opts.parseOptions(2, argv);
+    opts.parseOptions(2, argv, d_handler);
     free(argv[0]);
     free(argv[1]);
 
@@ -59,6 +64,7 @@ public:
     delete d_booleanType;
     delete d_scope;
     delete d_nodeManager;
+    delete d_handler;
   }
 
   bool imp(bool a, bool b) const {
diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h
index 9bac0d818..a7ebea2fe 100644
--- a/test/unit/expr/node_builder_black.h
+++ b/test/unit/expr/node_builder_black.h
@@ -20,12 +20,12 @@
 #include <limits.h>
 #include <sstream>
 
-#include "expr/node_builder.h"
+#include "base/cvc4_assert.h"
 #include "expr/convenience_node_builders.h"
-#include "expr/node_manager.h"
-#include "expr/node.h"
 #include "expr/kind.h"
-#include "util/cvc4_assert.h"
+#include "expr/node.h"
+#include "expr/node_builder.h"
+#include "expr/node_manager.h"
 #include "util/rational.h"
 
 using namespace CVC4;
diff --git a/test/unit/expr/node_manager_black.h b/test/unit/expr/node_manager_black.h
index b94e6a691..781829e36 100644
--- a/test/unit/expr/node_manager_black.h
+++ b/test/unit/expr/node_manager_black.h
@@ -21,9 +21,8 @@
 
 #include "expr/node_manager.h"
 #include "expr/node_manager_attributes.h"
-
-#include "util/rational.h"
 #include "util/integer.h"
+#include "util/rational.h"
 
 using namespace CVC4;
 using namespace CVC4::expr;
diff --git a/test/unit/expr/node_manager_white.h b/test/unit/expr/node_manager_white.h
index aaa3256dd..fa44b837a 100644
--- a/test/unit/expr/node_manager_white.h
+++ b/test/unit/expr/node_manager_white.h
@@ -19,9 +19,8 @@
 #include <string>
 
 #include "expr/node_manager.h"
-
-#include "util/rational.h"
 #include "util/integer.h"
+#include "util/rational.h"
 
 using namespace CVC4;
 using namespace CVC4::expr;
diff --git a/test/unit/expr/node_white.h b/test/unit/expr/node_white.h
index 8a68db269..594a981c8 100644
--- a/test/unit/expr/node_white.h
+++ b/test/unit/expr/node_white.h
@@ -18,11 +18,11 @@
 
 #include <string>
 
-#include "expr/node_value.h"
+#include "base/cvc4_assert.h"
+#include "expr/node.h"
 #include "expr/node_builder.h"
 #include "expr/node_manager.h"
-#include "expr/node.h"
-#include "util/cvc4_assert.h"
+#include "expr/node_value.h"
 
 using namespace CVC4;
 using namespace CVC4::kind;
diff --git a/test/unit/expr/symbol_table_black.h b/test/unit/expr/symbol_table_black.h
index 2acd1ebae..2b26ad745 100644
--- a/test/unit/expr/symbol_table_black.h
+++ b/test/unit/expr/symbol_table_black.h
@@ -19,13 +19,13 @@
 #include <sstream>
 #include <string>
 
+#include "base/cvc4_assert.h"
+#include "base/exception.h"
 #include "context/context.h"
-#include "expr/symbol_table.h"
-#include "expr/expr_manager.h"
 #include "expr/expr.h"
+#include "expr/expr_manager.h"
+#include "expr/symbol_table.h"
 #include "expr/type.h"
-#include "util/cvc4_assert.h"
-#include "util/exception.h"
 
 using namespace CVC4;
 using namespace CVC4::kind;
diff --git a/test/unit/main/interactive_shell_black.h b/test/unit/main/interactive_shell_black.h
index b09246d95..6c3e73d2c 100644
--- a/test/unit/main/interactive_shell_black.h
+++ b/test/unit/main/interactive_shell_black.h
@@ -22,9 +22,9 @@
 
 #include "expr/expr_manager.h"
 #include "main/interactive_shell.h"
-#include "parser/parser_builder.h"
-#include "util/language.h"
+#include "options/language.h"
 #include "options/options.h"
+#include "parser/parser_builder.h"
 
 using namespace CVC4;
 using namespace std;
diff --git a/test/unit/memory.h b/test/unit/memory.h
index 2809edee7..06c4a4a44 100644
--- a/test/unit/memory.h
+++ b/test/unit/memory.h
@@ -29,7 +29,7 @@
 #include <sys/time.h>
 #include <sys/resource.h>
 
-#include "util/cvc4_assert.h"
+#include "base/cvc4_assert.h"
 
 namespace CVC4 {
 namespace test {
diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h
index 61da34460..9b700eda6 100644
--- a/test/unit/parser/parser_black.h
+++ b/test/unit/parser/parser_black.h
@@ -19,15 +19,16 @@
 #include <cxxtest/TestSuite.h>
 #include <sstream>
 
+#include "base/output.h"
 #include "expr/expr.h"
 #include "expr/expr_manager.h"
+#include "options/language.h"
+#include "options/options.h"
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
 #include "parser/smt2/smt2.h"
-#include "expr/command.h"
-#include "options/options.h"
-#include "util/output.h"
-#include "util/language.h"
+#include "smt_util/command.h"
+
 
 using namespace CVC4;
 using namespace CVC4::parser;
diff --git a/test/unit/parser/parser_builder_black.h b/test/unit/parser/parser_builder_black.h
index c2c7cc18d..029c95ec9 100644
--- a/test/unit/parser/parser_builder_black.h
+++ b/test/unit/parser/parser_builder_black.h
@@ -15,18 +15,21 @@
  **/
 
 #include <cxxtest/TestSuite.h>
+
 #include <ext/stdio_filebuf.h>
-#include <fstream>
-#include <iostream>
 #include <stdio.h>
 #include <string.h>
 #include <sys/stat.h>
 #include <unistd.h>
 
-#include "expr/command.h"
+#include <fstream>
+#include <iostream>
+
+#include "options/language.h"
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
-#include "util/language.h"
+#include "smt_util/command.h"
+
 
 typedef __gnu_cxx::stdio_filebuf<char> filebuf_gnu;
 
diff --git a/test/unit/prop/cnf_stream_white.h b/test/unit/prop/cnf_stream_white.h
index db49e2521..e705da409 100644
--- a/test/unit/prop/cnf_stream_white.h
+++ b/test/unit/prop/cnf_stream_white.h
@@ -18,25 +18,22 @@
 /* #include <gmock/gmock.h> */
 /* #include <gtest/gtest.h> */
 
-#include "util/cvc4_assert.h"
-
+#include "base/cvc4_assert.h"
+#include "context/context.h"
 #include "expr/expr_manager.h"
 #include "expr/node_manager.h"
-#include "context/context.h"
 #include "prop/cnf_stream.h"
 #include "prop/prop_engine.h"
 #include "prop/theory_proxy.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
-
+#include "theory/arith/theory_arith.h"
+#include "theory/booleans/theory_bool.h"
+#include "theory/builtin/theory_builtin.h"
 #include "theory/theory.h"
 #include "theory/theory_engine.h"
 #include "theory/theory_registrar.h"
 
-#include "theory/builtin/theory_builtin.h"
-#include "theory/booleans/theory_bool.h"
-#include "theory/arith/theory_arith.h"
-
 using namespace CVC4;
 using namespace CVC4::context;
 using namespace CVC4::prop;
diff --git a/test/unit/theory/logic_info_white.h b/test/unit/theory/logic_info_white.h
index efc7c5582..1d363ec9c 100644
--- a/test/unit/theory/logic_info_white.h
+++ b/test/unit/theory/logic_info_white.h
@@ -28,6 +28,8 @@ class LogicInfoWhite : public CxxTest::TestSuite {
 
 public:
 
+#warning "This test is of questionable compatiblity with contrib/new-theory. Is the new theory id handled correctly by the Logic info."
+
   void testSmtlibLogics() {
     LogicInfo info("QF_SAT");
     TS_ASSERT( info.isLocked() );
@@ -1300,4 +1302,3 @@ public:
   }
 
 };/* class LogicInfoWhite */
-
diff --git a/test/unit/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h
index 58bbe7a2b..d8615eda7 100644
--- a/test/unit/theory/theory_arith_white.h
+++ b/test/unit/theory/theory_arith_white.h
@@ -15,23 +15,21 @@
  ** \todo document this file
  **/
 
-
 #include <cxxtest/TestSuite.h>
 
-#include "theory/theory.h"
-#include "theory/theory_engine.h"
-#include "theory/arith/theory_arith.h"
-#include "theory/quantifiers_engine.h"
+#include <vector>
+
+#include "context/context.h"
 #include "expr/node.h"
 #include "expr/node_manager.h"
-#include "context/context.h"
-#include "util/rational.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
-
+#include "theory/arith/theory_arith.h"
+#include "theory/quantifiers_engine.h"
+#include "theory/theory.h"
+#include "theory/theory_engine.h"
 #include "theory/theory_test_utils.h"
-
-#include <vector>
+#include "util/rational.h"
 
 using namespace CVC4;
 using namespace CVC4::theory;
@@ -103,7 +101,7 @@ public:
     d_em = new ExprManager();
     d_nm = NodeManager::fromExprManager(d_em);
     d_smt = new SmtEngine(d_em);
-    d_smt->setOption("incremental", false);
+    d_smt->setOption("incremental", CVC4::SExpr(false));
     d_ctxt = d_smt->d_context;
     d_uctxt = d_smt->d_userContext;
     d_scope = new SmtScope(d_smt);
diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h
index 7440de350..d1883da9f 100644
--- a/test/unit/theory/theory_engine_white.h
+++ b/test/unit/theory/theory_engine_white.h
@@ -20,24 +20,24 @@
 
 #include <cxxtest/TestSuite.h>
 
+#include <deque>
 #include <iostream>
 #include <string>
-#include <deque>
 
-#include "theory/theory.h"
-#include "theory/theory_engine.h"
-#include "theory/valuation.h"
-#include "theory/rewriter.h"
+#include "base/cvc4_assert.h"
+#include "context/context.h"
+#include "expr/kind.h"
 #include "expr/node.h"
 #include "expr/node_manager.h"
-#include "expr/kind.h"
-#include "context/context.h"
+#include "options/options.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
-#include "util/rational.h"
+#include "theory/rewriter.h"
+#include "theory/theory.h"
+#include "theory/theory_engine.h"
+#include "theory/valuation.h"
 #include "util/integer.h"
-#include "options/options.h"
-#include "util/cvc4_assert.h"
+#include "util/rational.h"
 
 using namespace CVC4;
 using namespace CVC4::theory;
diff --git a/test/unit/theory/type_enumerator_white.h b/test/unit/theory/type_enumerator_white.h
index d9963f78c..993021c5a 100644
--- a/test/unit/theory/type_enumerator_white.h
+++ b/test/unit/theory/type_enumerator_white.h
@@ -17,13 +17,13 @@
 
 #include <cxxtest/TestSuite.h>
 
-#include "expr/node_manager.h"
+#include "expr/array_store_all.h"
 #include "expr/expr_manager.h"
-#include "expr/type_node.h"
 #include "expr/kind.h"
+#include "expr/node_manager.h"
+#include "expr/type_node.h"
+#include "options/language.h"
 #include "theory/type_enumerator.h"
-#include "util/language.h"
-#include "util/array_store_all.h"
 
 using namespace CVC4;
 using namespace CVC4::theory;
diff --git a/test/unit/util/array_store_all_black.h b/test/unit/util/array_store_all_black.h
index 433dd7601..6a75bc7fa 100644
--- a/test/unit/util/array_store_all_black.h
+++ b/test/unit/util/array_store_all_black.h
@@ -16,7 +16,7 @@
 
 #include <cxxtest/TestSuite.h>
 
-#include "util/array_store_all.h"
+#include "expr/array_store_all.h"
 #include "expr/expr_manager.h"
 #include "expr/expr_manager_scope.h"
 #include "expr/type.h"
diff --git a/test/unit/util/assert_white.h b/test/unit/util/assert_white.h
index 38dfe87e6..bbc4d02b3 100644
--- a/test/unit/util/assert_white.h
+++ b/test/unit/util/assert_white.h
@@ -19,7 +19,7 @@
 #include <string>
 #include <cstring>
 
-#include "util/cvc4_assert.h"
+#include "base/cvc4_assert.h"
 
 using namespace CVC4;
 using namespace std;
diff --git a/test/unit/util/boolean_simplification_black.h b/test/unit/util/boolean_simplification_black.h
index db02ce207..ac343ede8 100644
--- a/test/unit/util/boolean_simplification_black.h
+++ b/test/unit/util/boolean_simplification_black.h
@@ -14,15 +14,15 @@
  ** Black box testing of CVC4::BooleanSimplification.
  **/
 
-#include "util/language.h"
-#include "expr/node.h"
-#include "expr/kind.h"
-#include "expr/node_manager.h"
-#include "util/boolean_simplification.h"
-
 #include <algorithm>
-#include <vector>
 #include <set>
+#include <vector>
+
+#include "expr/kind.h"
+#include "expr/node.h"
+#include "expr/node_manager.h"
+#include "options/language.h"
+#include "smt_util/boolean_simplification.h"
 
 using namespace CVC4;
 using namespace std;
@@ -214,4 +214,3 @@ public:
   }
 
 };/* class BooleanSimplificationBlack */
-
diff --git a/test/unit/util/cardinality_public.h b/test/unit/util/cardinality_public.h
index 732bb0dbb..2fcee66b6 100644
--- a/test/unit/util/cardinality_public.h
+++ b/test/unit/util/cardinality_public.h
@@ -14,11 +14,11 @@
  ** Public-box testing of CVC4::Cardinality.
  **/
 
-#include "util/cardinality.h"
-#include "util/integer.h"
-
-#include <string>
 #include <sstream>
+#include <string>
+
+#include "util/integer.h"
+#include "util/cardinality.h"
 
 using namespace CVC4;
 using namespace std;
diff --git a/test/unit/util/datatype_black.h b/test/unit/util/datatype_black.h
index ff36336ca..91a53ddc3 100644
--- a/test/unit/util/datatype_black.h
+++ b/test/unit/util/datatype_black.h
@@ -17,8 +17,7 @@
 #include <cxxtest/TestSuite.h>
 #include <sstream>
 
-#include "util/datatype.h"
-
+#include "expr/datatype.h"
 #include "expr/expr.h"
 #include "expr/expr_manager.h"
 #include "expr/expr_manager_scope.h"
diff --git a/test/unit/util/exception_black.h b/test/unit/util/exception_black.h
index d2ae7d3e5..c2c7f83c0 100644
--- a/test/unit/util/exception_black.h
+++ b/test/unit/util/exception_black.h
@@ -19,7 +19,7 @@
 #include <iostream>
 #include <sstream>
 
-#include "util/exception.h"
+#include "base/exception.h"
 
 using namespace CVC4;
 using namespace std;
diff --git a/test/unit/util/integer_black.h b/test/unit/util/integer_black.h
index 36de17cba..510afe7b7 100644
--- a/test/unit/util/integer_black.h
+++ b/test/unit/util/integer_black.h
@@ -15,8 +15,9 @@
  **/
 
 #include <cxxtest/TestSuite.h>
-#include <sstream>
+
 #include <limits>
+#include <sstream>
 
 #include "util/integer.h"
 
diff --git a/test/unit/util/output_black.h b/test/unit/util/output_black.h
index 0b151ef3f..87423f026 100644
--- a/test/unit/util/output_black.h
+++ b/test/unit/util/output_black.h
@@ -19,7 +19,7 @@
 #include <iostream>
 #include <sstream>
 
-#include "util/output.h"
+#include "base/output.h"
 
 using namespace CVC4;
 using namespace std;
diff --git a/test/unit/util/stats_black.h b/test/unit/util/stats_black.h
index 249f9a5b1..c0e1ea7fd 100644
--- a/test/unit/util/stats_black.h
+++ b/test/unit/util/stats_black.h
@@ -19,7 +19,7 @@
 #include <string>
 #include <ctime>
 
-#include "util/statistics_registry.h"
+#include "expr/statistics_registry.h"
 
 using namespace CVC4;
 using namespace std;
diff --git a/test/unit/util/subrange_bound_white.h b/test/unit/util/subrange_bound_white.h
index 71947b297..3b785ae0d 100644
--- a/test/unit/util/subrange_bound_white.h
+++ b/test/unit/util/subrange_bound_white.h
@@ -14,11 +14,11 @@
  ** White-box testing of CVC4::SubrangeBound.
  **/
 
-#include "util/subrange_bound.h"
-#include "util/integer.h"
-
-#include <string>
 #include <sstream>
+#include <string>
+
+#include "util/integer.h"
+#include "util/subrange_bound.h"
 
 using namespace CVC4;
 using namespace std;
@@ -72,4 +72,3 @@ public:
   }
 
 };/* class SubrangeBoundWhite */
-