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.

53 files changed, 256 insertions, 823 deletions

diff --git a/src/theory/arith/approx_simplex.cpp b/src/theory/arith/approx_simplex.cpp
index 5b3c87b3d..71ac18e84 100644
--- a/src/theory/arith/approx_simplex.cpp
+++ b/src/theory/arith/approx_simplex.cpp
@@ -15,17 +15,18 @@
  ** \todo document this file
  **/
 
-#include "cvc4autoconfig.h"
+#include <cfloat>
+#include <cmath>
+#include <map>
+#include <math.h>
 
+#include "base/output.h"
+#include "cvc4autoconfig.h"
 #include "theory/arith/approx_simplex.h"
-#include "theory/arith/normal_form.h"
 #include "theory/arith/constraint.h"
 #include "theory/arith/cut_log.h"
 #include "theory/arith/matrix.h"
-#include <math.h>
-#include <cmath>
-#include <cfloat>
-#include <map>
+#include "theory/arith/normal_form.h"
 
 using namespace std;
 
diff --git a/src/theory/arith/approx_simplex.h b/src/theory/arith/approx_simplex.h
index 808b64703..064887787 100644
--- a/src/theory/arith/approx_simplex.h
+++ b/src/theory/arith/approx_simplex.h
@@ -19,14 +19,13 @@
 #include "cvc4_private.h"
 
 #pragma once
+#include <vector>
 
-#include "util/statistics_registry.h"
+#include "expr/statistics_registry.h"
 #include "theory/arith/arithvar.h"
-#include "util/rational.h"
 #include "theory/arith/delta_rational.h"
-//#include "theory/arith/linear_equality.h"
 #include "util/dense_map.h"
-#include <vector>
+#include "util/rational.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/arith/arith_heuristic_pivot_rule.cpp b/src/theory/arith/arith_heuristic_pivot_rule.cpp
deleted file mode 100644
index 8ef2385c7..000000000
--- a/src/theory/arith/arith_heuristic_pivot_rule.cpp
+++ /dev/null
@@ -1,41 +0,0 @@
-/*********************                                                        */
-/*! \file arith_heuristic_pivot_rule.cpp
- ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: Tim King
- ** 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 [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#include "theory/arith/arith_heuristic_pivot_rule.h"
-
-namespace CVC4 {
-
-std::ostream& operator<<(std::ostream& out, ErrorSelectionRule rule) {
-  switch(rule) {
-  case MINIMUM_AMOUNT:
-    out << "MINIMUM_AMOUNT";
-    break;
-  case VAR_ORDER:
-    out << "VAR_ORDER";
-    break;
-  case MAXIMUM_AMOUNT:
-    out << "MAXIMUM_AMOUNT";
-    break;
-  default:
-    out << "ArithHeuristicPivotRule!UNKNOWN";
-  }
-
-  return out;
-}
-
-}/* CVC4 namespace */
-
diff --git a/src/theory/arith/arith_heuristic_pivot_rule.h b/src/theory/arith/arith_heuristic_pivot_rule.h
deleted file mode 100644
index a64a7c846..000000000
--- a/src/theory/arith/arith_heuristic_pivot_rule.h
+++ /dev/null
@@ -1,38 +0,0 @@
-/*********************                                                        */
-/*! \file arith_heuristic_pivot_rule.h
- ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: Tim King
- ** 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 [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#include "cvc4_public.h"
-
-#ifndef __CVC4__THEORY__ARITH__ARITH_HEURISTIC_PIVOT_RULE_H
-#define __CVC4__THEORY__ARITH__ARITH_HEURISTIC_PIVOT_RULE_H
-
-#include <iostream>
-
-namespace CVC4 {
-
-typedef enum {
-  VAR_ORDER,
-  MINIMUM_AMOUNT,
-  MAXIMUM_AMOUNT,
-  SUM_METRIC
-} ErrorSelectionRule;
-
-std::ostream& operator<<(std::ostream& out, ErrorSelectionRule rule) CVC4_PUBLIC;
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4__THEORY__ARITH__ARITH_HEURISTIC_PIVOT_RULE_H */
diff --git a/src/theory/arith/arith_ite_utils.cpp b/src/theory/arith/arith_ite_utils.cpp
index 2b31831e2..cd180e59e 100644
--- a/src/theory/arith/arith_ite_utils.cpp
+++ b/src/theory/arith/arith_ite_utils.cpp
@@ -15,15 +15,18 @@
  ** \todo document this file
  **/
 
-#include "smt/options.h"
 #include "theory/arith/arith_ite_utils.h"
-#include "theory/arith/normal_form.h"
+
+#include <ostream>
+
+#include "base/output.h"
+#include "options/smt_options.h"
 #include "theory/arith/arith_utilities.h"
+#include "theory/arith/normal_form.h"
 #include "theory/ite_utilities.h"
-#include "theory/theory_model.h"
 #include "theory/rewriter.h"
 #include "theory/substitutions.h"
-#include <ostream>
+#include "theory/theory_model.h"
 
 using namespace std;
 
diff --git a/src/theory/arith/arith_propagation_mode.cpp b/src/theory/arith/arith_propagation_mode.cpp
deleted file mode 100644
index 119761906..000000000
--- a/src/theory/arith/arith_propagation_mode.cpp
+++ /dev/null
@@ -1,44 +0,0 @@
-/*********************                                                        */
-/*! \file arith_propagation_mode.cpp
- ** \verbatim
- ** Original author: Morgan Deters
- ** 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 [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#include "theory/arith/arith_propagation_mode.h"
-
-namespace CVC4 {
-
-std::ostream& operator<<(std::ostream& out, ArithPropagationMode mode) {
-  switch(mode) {
-  case NO_PROP:
-    out << "NO_PROP";
-    break;
-  case UNATE_PROP:
-    out << "UNATE_PROP";
-    break;
-  case BOUND_INFERENCE_PROP:
-    out << "BOUND_INFERENCE_PROP";
-    break;
-  case BOTH_PROP:
-    out << "BOTH_PROP";
-    break;
-  default:
-    out << "ArithPropagationMode!UNKNOWN";
-  }
-
-  return out;
-}
-
-}/* CVC4 namespace */
-
diff --git a/src/theory/arith/arith_propagation_mode.h b/src/theory/arith/arith_propagation_mode.h
deleted file mode 100644
index fe8f8c9cc..000000000
--- a/src/theory/arith/arith_propagation_mode.h
+++ /dev/null
@@ -1,38 +0,0 @@
-/*********************                                                        */
-/*! \file arith_propagation_mode.h
- ** \verbatim
- ** Original author: Morgan Deters
- ** 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 [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#include "cvc4_public.h"
-
-#ifndef __CVC4__THEORY__ARITH__ARITH_PROPAGATION_MODE_H
-#define __CVC4__THEORY__ARITH__ARITH_PROPAGATION_MODE_H
-
-#include <iostream>
-
-namespace CVC4 {
-
-typedef enum {
-  NO_PROP,
-  UNATE_PROP,
-  BOUND_INFERENCE_PROP,
-  BOTH_PROP
-} ArithPropagationMode;
-
-std::ostream& operator<<(std::ostream& out, ArithPropagationMode rule) CVC4_PUBLIC;
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4__THEORY__ARITH__ARITH_PROPAGATION_MODE_H */
diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index a85fd024f..ca286d53a 100644
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -15,14 +15,15 @@
  ** \todo document this file
  **/
 
-#include "theory/theory.h"
-#include "theory/arith/normal_form.h"
-#include "theory/arith/arith_rewriter.h"
-#include "theory/arith/arith_utilities.h"
-
-#include <vector>
 #include <set>
 #include <stack>
+#include <vector>
+
+#include "base/output.h"
+#include "theory/arith/arith_rewriter.h"
+#include "theory/arith/arith_utilities.h"
+#include "theory/arith/normal_form.h"
+#include "theory/theory.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp
index a7767e38b..383c6b418 100644
--- a/src/theory/arith/arith_static_learner.cpp
+++ b/src/theory/arith/arith_static_learner.cpp
@@ -15,18 +15,16 @@
  ** \todo document this file
  **/
 
-#include "theory/rewriter.h"
+#include <vector>
 
-#include "theory/arith/arith_utilities.h"
+#include "base/output.h"
+#include "expr/convenience_node_builders.h"
+#include "expr/expr.h"
+#include "options/arith_options.h"
 #include "theory/arith/arith_static_learner.h"
-#include "theory/arith/options.h"
-
+#include "theory/arith/arith_utilities.h"
 #include "theory/arith/normal_form.h"
-
-#include "expr/expr.h"
-#include "expr/convenience_node_builders.h"
-
-#include <vector>
+#include "theory/rewriter.h"
 
 using namespace std;
 using namespace CVC4::kind;
diff --git a/src/theory/arith/arith_static_learner.h b/src/theory/arith/arith_static_learner.h
index 7a1a1a6db..2b0ee9dad 100644
--- a/src/theory/arith/arith_static_learner.h
+++ b/src/theory/arith/arith_static_learner.h
@@ -20,13 +20,12 @@
 #ifndef __CVC4__THEORY__ARITH__ARITH_STATIC_LEARNER_H
 #define __CVC4__THEORY__ARITH__ARITH_STATIC_LEARNER_H
 
+#include <set>
 
-#include "util/statistics_registry.h"
-#include "theory/arith/arith_utilities.h"
-
-#include "context/context.h"
 #include "context/cdtrail_hashmap.h"
-#include <set>
+#include "context/context.h"
+#include "expr/statistics_registry.h"
+#include "theory/arith/arith_utilities.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/arith/arith_unate_lemma_mode.cpp b/src/theory/arith/arith_unate_lemma_mode.cpp
deleted file mode 100644
index bb6066bb4..000000000
--- a/src/theory/arith/arith_unate_lemma_mode.cpp
+++ /dev/null
@@ -1,44 +0,0 @@
-/*********************                                                        */
-/*! \file arith_unate_lemma_mode.cpp
- ** \verbatim
- ** Original author: Morgan Deters
- ** 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 [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#include "theory/arith/arith_unate_lemma_mode.h"
-
-namespace CVC4 {
-
-std::ostream& operator<<(std::ostream& out, ArithUnateLemmaMode mode) {
-  switch(mode) {
-  case NO_PRESOLVE_LEMMAS:
-    out << "NO_PRESOLVE_LEMMAS";
-    break;
-  case INEQUALITY_PRESOLVE_LEMMAS:
-    out << "INEQUALITY_PRESOLVE_LEMMAS";
-    break;
-  case EQUALITY_PRESOLVE_LEMMAS:
-    out << "EQUALITY_PRESOLVE_LEMMAS";
-    break;
-  case ALL_PRESOLVE_LEMMAS:
-    out << "ALL_PRESOLVE_LEMMAS";
-    break;
-  default:
-    out << "ArithUnateLemmaMode!UNKNOWN";
-  }
-
-  return out;
-}
-
-}/* CVC4 namespace */
-
diff --git a/src/theory/arith/arith_unate_lemma_mode.h b/src/theory/arith/arith_unate_lemma_mode.h
deleted file mode 100644
index 5e1362bcb..000000000
--- a/src/theory/arith/arith_unate_lemma_mode.h
+++ /dev/null
@@ -1,38 +0,0 @@
-/*********************                                                        */
-/*! \file arith_unate_lemma_mode.h
- ** \verbatim
- ** Original author: Morgan Deters
- ** 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 [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#include "cvc4_public.h"
-
-#ifndef __CVC4__THEORY__ARITH__ARITH_UNATE_LEMMA_MODE_H
-#define __CVC4__THEORY__ARITH__ARITH_UNATE_LEMMA_MODE_H
-
-#include <iostream>
-
-namespace CVC4 {
-
-typedef enum {
-  NO_PRESOLVE_LEMMAS,
-  INEQUALITY_PRESOLVE_LEMMAS,
-  EQUALITY_PRESOLVE_LEMMAS,
-  ALL_PRESOLVE_LEMMAS
-} ArithUnateLemmaMode;
-
-std::ostream& operator<<(std::ostream& out, ArithUnateLemmaMode rule) CVC4_PUBLIC;
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4__THEORY__ARITH__ARITH_UNATE_LEMMA_MODE_H */
diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h
index 9d32916cc..ffa896012 100644
--- a/src/theory/arith/arith_utilities.h
+++ b/src/theory/arith/arith_utilities.h
@@ -19,16 +19,17 @@
 #ifndef __CVC4__THEORY__ARITH__ARITH_UTILITIES_H
 #define __CVC4__THEORY__ARITH__ARITH_UTILITIES_H
 
-#include "util/rational.h"
-#include "util/integer.h"
-#include "util/dense_map.h"
-#include "expr/node.h"
-#include "theory/arith/delta_rational.h"
-#include "theory/arith/arithvar.h"
-#include "context/cdhashset.h"
 #include <ext/hash_map>
 #include <vector>
 
+#include "context/cdhashset.h"
+#include "expr/node.h"
+#include "theory/arith/arithvar.h"
+#include "theory/arith/delta_rational.h"
+#include "util/dense_map.h"
+#include "util/integer.h"
+#include "util/rational.h"
+
 namespace CVC4 {
 namespace theory {
 namespace arith {
diff --git a/src/theory/arith/arithvar.h b/src/theory/arith/arithvar.h
index dd049e94f..9e4dab4c3 100644
--- a/src/theory/arith/arithvar.h
+++ b/src/theory/arith/arithvar.h
@@ -22,10 +22,10 @@
 #pragma once
 
 #include <vector>
+
 #include "util/index.h"
 #include "util/rational.h"
 
-
 namespace CVC4 {
 namespace theory {
 namespace arith {
@@ -43,4 +43,3 @@ extern bool debugIsASet(const ArithVarVec& variables);
 }/* CVC4::theory::arith namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
-
diff --git a/src/theory/arith/attempt_solution_simplex.cpp b/src/theory/arith/attempt_solution_simplex.cpp
index 5b92a8809..737cc9e7b 100644
--- a/src/theory/arith/attempt_solution_simplex.cpp
+++ b/src/theory/arith/attempt_solution_simplex.cpp
@@ -15,9 +15,9 @@
  ** \todo document this file
  **/
 
-
+#include "base/output.h"
+#include "options/arith_options.h"
 #include "theory/arith/attempt_solution_simplex.h"
-#include "theory/arith/options.h"
 #include "theory/arith/constraint.h"
 
 using namespace std;
diff --git a/src/theory/arith/attempt_solution_simplex.h b/src/theory/arith/attempt_solution_simplex.h
index 4d94169c9..88d29f6b0 100644
--- a/src/theory/arith/attempt_solution_simplex.h
+++ b/src/theory/arith/attempt_solution_simplex.h
@@ -53,7 +53,7 @@
 
 #pragma once
 
-#include "util/statistics_registry.h"
+#include "expr/statistics_registry.h"
 #include "theory/arith/simplex.h"
 #include "theory/arith/approx_simplex.h"
 
diff --git a/src/theory/arith/bound_counts.h b/src/theory/arith/bound_counts.h
index c1f0ce545..b5e0124c1 100644
--- a/src/theory/arith/bound_counts.h
+++ b/src/theory/arith/bound_counts.h
@@ -19,8 +19,9 @@
 #pragma once
 
 #include <stdint.h>
+
+#include "base/cvc4_assert.h"
 #include "theory/arith/arithvar.h"
-#include "util/cvc4_assert.h"
 #include "util/dense_map.h"
 
 namespace CVC4 {
diff --git a/src/theory/arith/callbacks.h b/src/theory/arith/callbacks.h
index 734c605c6..d180ceab5 100644
--- a/src/theory/arith/callbacks.h
+++ b/src/theory/arith/callbacks.h
@@ -19,12 +19,11 @@
 #pragma once
 
 #include "expr/node.h"
-#include "util/rational.h"
-
-#include "theory/arith/theory_arith_private_forward.h"
 #include "theory/arith/arithvar.h"
 #include "theory/arith/bound_counts.h"
 #include "theory/arith/constraint_forward.h"
+#include "theory/arith/theory_arith_private_forward.h"
+#include "util/rational.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp
index 8a145ffc2..964c92eb5 100644
--- a/src/theory/arith/congruence_manager.cpp
+++ b/src/theory/arith/congruence_manager.cpp
@@ -14,10 +14,10 @@
  ** \todo document this file
  **/
 
+#include "base/output.h"
+#include "theory/arith/arith_utilities.h"
 #include "theory/arith/congruence_manager.h"
-
 #include "theory/arith/constraint.h"
-#include "theory/arith/arith_utilities.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h
index 7ecfd21cf..2fc9c47ed 100644
--- a/src/theory/arith/congruence_manager.h
+++ b/src/theory/arith/congruence_manager.h
@@ -19,19 +19,16 @@
 
 #pragma once
 
+#include "context/cdlist.h"
+#include "context/cdmaybe.h"
+#include "context/cdo.h"
+#include "context/cdtrail_queue.h"
+#include "context/context.h"
+#include "expr/statistics_registry.h"
 #include "theory/arith/arithvar.h"
 #include "theory/arith/constraint_forward.h"
 #include "theory/arith/partial_model.h"
-
 #include "theory/uf/equality_engine.h"
-
-#include "context/cdo.h"
-#include "context/cdlist.h"
-#include "context/context.h"
-#include "context/cdtrail_queue.h"
-#include "context/cdmaybe.h"
-
-#include "util/statistics_registry.h"
 #include "util/dense_map.h"
 
 namespace CVC4 {
diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp
index 4acf86d43..f13565a7f 100644
--- a/src/theory/arith/constraint.cpp
+++ b/src/theory/arith/constraint.cpp
@@ -15,15 +15,15 @@
  ** \todo document this file
  **/
 
-#include "cvc4_private.h"
-#include "theory/arith/constraint.h"
-#include "theory/arith/arith_utilities.h"
-#include "theory/arith/normal_form.h"
+#include <ostream>
+#include <algorithm>
 
+#include "base/output.h"
 #include "proof/proof.h"
+#include "theory/arith/arith_utilities.h"
+#include "theory/arith/constraint.h"
+#include "theory/arith/normal_form.h"
 
-#include <ostream>
-#include <algorithm>
 
 using namespace std;
 using namespace CVC4::kind;
diff --git a/src/theory/arith/cut_log.cpp b/src/theory/arith/cut_log.cpp
index d855caee8..d94e1c760 100644
--- a/src/theory/arith/cut_log.cpp
+++ b/src/theory/arith/cut_log.cpp
@@ -15,17 +15,17 @@
  ** \todo document this file
  **/
 
-#include "cvc4autoconfig.h"
-
+#include <cmath>
+#include <limits.h>
+#include <map>
+#include <math.h>
 
-#include "theory/arith/cut_log.h"
+#include "base/output.h"
+#include "cvc4autoconfig.h"
 #include "theory/arith/approx_simplex.h"
-#include "theory/arith/normal_form.h"
 #include "theory/arith/constraint.h"
-#include <math.h>
-#include <cmath>
-#include <map>
-#include <limits.h>
+#include "theory/arith/cut_log.h"
+#include "theory/arith/normal_form.h"
 
 using namespace std;
 
diff --git a/src/theory/arith/cut_log.h b/src/theory/arith/cut_log.h
index 9ce017488..bbed13418 100644
--- a/src/theory/arith/cut_log.h
+++ b/src/theory/arith/cut_log.h
@@ -20,15 +20,16 @@
 
 #pragma once
 
+#include <ext/hash_map>
+#include <map>
+#include <set>
+#include <vector>
+
 #include "expr/kind.h"
-#include "util/statistics_registry.h"
+#include "expr/statistics_registry.h"
 #include "theory/arith/arithvar.h"
 #include "theory/arith/constraint_forward.h"
 #include "util/dense_map.h"
-#include <vector>
-#include <map>
-#include <set>
-#include <ext/hash_map>
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/arith/delta_rational.h b/src/theory/arith/delta_rational.h
index a9d919c21..5f67847d8 100644
--- a/src/theory/arith/delta_rational.h
+++ b/src/theory/arith/delta_rational.h
@@ -17,14 +17,13 @@
 
 #include "cvc4_private.h"
 
-#include "util/integer.h"
-#include "util/rational.h"
-#include "util/exception.h"
-
+#pragma once
 
 #include <ostream>
-#pragma once
 
+#include "base/exception.h"
+#include "util/integer.h"
+#include "util/rational.h"
 
 namespace CVC4 {
 
diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/dio_solver.cpp
index 7e50dad87..f8b8e0e7b 100644
--- a/src/theory/arith/dio_solver.cpp
+++ b/src/theory/arith/dio_solver.cpp
@@ -14,11 +14,12 @@
  ** A Diophantine equation solver for the theory of arithmetic.
  **/
 
-#include "theory/arith/dio_solver.h"
-#include "theory/arith/options.h"
-
 #include <iostream>
 
+#include "base/output.h"
+#include "options/arith_options.h"
+#include "theory/arith/dio_solver.h"
+
 using namespace std;
 
 namespace CVC4 {
diff --git a/src/theory/arith/dio_solver.h b/src/theory/arith/dio_solver.h
index 9b96acf48..626160b03 100644
--- a/src/theory/arith/dio_solver.h
+++ b/src/theory/arith/dio_solver.h
@@ -16,22 +16,22 @@
 
 #include "cvc4_private.h"
 
+
 #ifndef __CVC4__THEORY__ARITH__DIO_SOLVER_H
 #define __CVC4__THEORY__ARITH__DIO_SOLVER_H
 
-#include "context/context.h"
-#include "context/cdo.h"
+#include <utility>
+#include <vector>
+
+#include "base/output.h"
 #include "context/cdlist.h"
+#include "context/cdo.h"
 #include "context/cdqueue.h"
-
+#include "context/context.h"
+#include "expr/statistics_registry.h"
+#include "theory/arith/normal_form.h"
 #include "theory/arith/partial_model.h"
 #include "util/rational.h"
-#include "theory/arith/normal_form.h"
-
-#include "util/statistics_registry.h"
-
-#include <vector>
-#include <utility>
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/arith/dual_simplex.cpp b/src/theory/arith/dual_simplex.cpp
index 234b33e97..32f81ded8 100644
--- a/src/theory/arith/dual_simplex.cpp
+++ b/src/theory/arith/dual_simplex.cpp
@@ -15,10 +15,10 @@
  ** \todo document this file
  **/
 
-
-#include "theory/arith/dual_simplex.h"
-#include "theory/arith/options.h"
+#include "base/output.h"
+#include "options/arith_options.h"
 #include "theory/arith/constraint.h"
+#include "theory/arith/dual_simplex.h"
 
 using namespace std;
 
diff --git a/src/theory/arith/dual_simplex.h b/src/theory/arith/dual_simplex.h
index 53f627081..d6bf57bb0 100644
--- a/src/theory/arith/dual_simplex.h
+++ b/src/theory/arith/dual_simplex.h
@@ -48,12 +48,11 @@
  **   These are theory valid and are currently turned into lemmas
  **/
 
-
 #include "cvc4_private.h"
 
 #pragma once
 
-#include "util/statistics_registry.h"
+#include "expr/statistics_registry.h"
 #include "theory/arith/simplex.h"
 
 namespace CVC4 {
diff --git a/src/theory/arith/error_set.h b/src/theory/arith/error_set.h
index 5843e0f7b..f12e38c12 100644
--- a/src/theory/arith/error_set.h
+++ b/src/theory/arith/error_set.h
@@ -20,36 +20,18 @@
 
 #pragma once
 
+#include <vector>
+
+#include "expr/statistics_registry.h"
+#include "options/arith_heuristic_pivot_rule.h"
 #include "theory/arith/arithvar.h"
 #include "theory/arith/bound_counts.h"
+#include "theory/arith/callbacks.h"
 #include "theory/arith/delta_rational.h"
 #include "theory/arith/partial_model.h"
-#include "theory/arith/arith_heuristic_pivot_rule.h"
 #include "theory/arith/tableau_sizes.h"
-#include "theory/arith/callbacks.h"
-
-#include "util/statistics_registry.h"
 #include "util/bin_heap.h"
 
-// #if CVC4_GCC_HAS_PB_DS_BUG
-//    // Unfortunate bug in some older GCCs (e.g., v4.2):
-//    //   http://gcc.gnu.org/bugzilla/show_bug.cgi?id=36612
-//    // Requires some header-hacking to work around
-// #  define __throw_container_error inline __throw_container_error
-// #  define __throw_insert_error inline __throw_insert_error
-// #  define __throw_join_error inline __throw_join_error
-// #  define __throw_resize_error inline __throw_resize_error
-// #  include <ext/pb_ds/exception.hpp>
-// #  undef __throw_container_error
-// #  undef __throw_insert_error
-// #  undef __throw_join_error
-// #  undef __throw_resize_error
-// #endif /* CVC4_GCC_HAS_PB_DS_BUG */
-
-// #include <ext/pb_ds/priority_queue.hpp>
-
-#include <vector>
-
 namespace CVC4 {
 namespace theory {
 namespace arith {
diff --git a/src/theory/arith/fc_simplex.cpp b/src/theory/arith/fc_simplex.cpp
index d21bb8f8b..229dc379c 100644
--- a/src/theory/arith/fc_simplex.cpp
+++ b/src/theory/arith/fc_simplex.cpp
@@ -14,13 +14,12 @@
  ** [[ Add lengthier description here ]]
  ** \todo document this file
  **/
-
-
 #include "theory/arith/fc_simplex.h"
-#include "theory/arith/options.h"
-#include "theory/arith/constraint.h"
 
-#include "util/statistics_registry.h"
+#include "base/output.h"
+#include "expr/statistics_registry.h"
+#include "options/arith_options.h"
+#include "theory/arith/constraint.h"
 
 using namespace std;
 
diff --git a/src/theory/arith/fc_simplex.h b/src/theory/arith/fc_simplex.h
index b6c0c4f62..471804003 100644
--- a/src/theory/arith/fc_simplex.h
+++ b/src/theory/arith/fc_simplex.h
@@ -52,10 +52,11 @@
 
 #pragma once
 
+#include <stdint.h>
+
+#include "expr/statistics_registry.h"
 #include "theory/arith/simplex.h"
 #include "util/dense_map.h"
-#include "util/statistics_registry.h"
-#include <stdint.h>
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/arith/infer_bounds.h b/src/theory/arith/infer_bounds.h
index 55486080a..770d9d1b3 100644
--- a/src/theory/arith/infer_bounds.h
+++ b/src/theory/arith/infer_bounds.h
@@ -19,13 +19,15 @@
 
 #pragma once
 
-#include "util/maybe.h"
-#include "util/integer.h"
-#include "util/rational.h"
+#include <ostream>
+
 #include "expr/node.h"
 #include "theory/arith/delta_rational.h"
 #include "theory/theory.h"
-#include <ostream>
+#include "util/integer.h"
+#include "util/maybe.h"
+#include "util/rational.h"
+
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/arith/linear_equality.cpp b/src/theory/arith/linear_equality.cpp
index bd252bf49..d8888bd75 100644
--- a/src/theory/arith/linear_equality.cpp
+++ b/src/theory/arith/linear_equality.cpp
@@ -15,8 +15,9 @@
  **/
 
 
-#include "theory/arith/linear_equality.h"
+#include "base/output.h"
 #include "theory/arith/constraint.h"
+#include "theory/arith/linear_equality.h"
 
 using namespace std;
 
diff --git a/src/theory/arith/linear_equality.h b/src/theory/arith/linear_equality.h
index 99ec6e52c..d7c9c038c 100644
--- a/src/theory/arith/linear_equality.h
+++ b/src/theory/arith/linear_equality.h
@@ -29,16 +29,15 @@
 
 #pragma once
 
-#include "theory/arith/delta_rational.h"
+#include "expr/statistics_registry.h"
+#include "options/arith_options.h"
 #include "theory/arith/arithvar.h"
-#include "theory/arith/partial_model.h"
-#include "theory/arith/tableau.h"
 #include "theory/arith/constraint_forward.h"
+#include "theory/arith/delta_rational.h"
+#include "theory/arith/partial_model.h"
 #include "theory/arith/simplex_update.h"
-#include "theory/arith/options.h"
-
+#include "theory/arith/tableau.h"
 #include "util/maybe.h"
-#include "util/statistics_registry.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/arith/matrix.h b/src/theory/arith/matrix.h
index 6c218eb0b..647df886f 100644
--- a/src/theory/arith/matrix.h
+++ b/src/theory/arith/matrix.h
@@ -19,13 +19,14 @@
 
 #pragma once
 
-#include "util/index.h"
-#include "util/dense_map.h"
-#include "theory/arith/arithvar.h"
-
 #include <queue>
-#include <vector>
 #include <utility>
+#include <vector>
+
+#include "base/output.h"
+#include "theory/arith/arithvar.h"
+#include "util/dense_map.h"
+#include "util/index.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/arith/normal_form.cpp b/src/theory/arith/normal_form.cpp
index fda34960a..e22a5e2e3 100644
--- a/src/theory/arith/normal_form.cpp
+++ b/src/theory/arith/normal_form.cpp
@@ -15,9 +15,11 @@
  ** \todo document this file
  **/
 
+#include <list>
+
+#include "base/output.h"
 #include "theory/arith/normal_form.h"
 #include "theory/arith/arith_utilities.h"
-#include <list>
 #include "theory/theory.h"
 
 using namespace std;
diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h
index 97813338f..eeb56f597 100644
--- a/src/theory/arith/normal_form.h
+++ b/src/theory/arith/normal_form.h
@@ -20,19 +20,20 @@
 #ifndef __CVC4__THEORY__ARITH__NORMAL_FORM_H
 #define __CVC4__THEORY__ARITH__NORMAL_FORM_H
 
-#include "expr/node.h"
-#include "expr/node_self_iterator.h"
-#include "util/rational.h"
-#include "theory/arith/delta_rational.h"
-//#include "theory/arith/arith_utilities.h"
-
-#include <list>
 #include <algorithm>
+#include <list>
 
 #if IS_SORTED_IN_GNUCXX_NAMESPACE
 #  include <ext/algorithm>
 #endif /* IS_SORTED_IN_GNUCXX_NAMESPACE */
 
+#include "base/output.h"
+#include "expr/node.h"
+#include "expr/node_self_iterator.h"
+#include "theory/arith/delta_rational.h"
+#include "util/rational.h"
+
+
 namespace CVC4 {
 namespace theory {
 namespace arith {
diff --git a/src/theory/arith/options b/src/theory/arith/options
deleted file mode 100644
index ea9658eb3..000000000
--- a/src/theory/arith/options
+++ /dev/null
@@ -1,164 +0,0 @@
-#
-# Option specification file for CVC4
-# See src/options/base_options for a description of this file format
-#
-
-module ARITH "theory/arith/options.h" Arithmetic theory
-
-option arithUnateLemmaMode --unate-lemmas=MODE ArithUnateLemmaMode :handler CVC4::theory::arith::stringToArithUnateLemmaMode :default ALL_PRESOLVE_LEMMAS :handler-include "theory/arith/options_handlers.h" :include "theory/arith/arith_unate_lemma_mode.h"
- determines which lemmas to add before solving (default is 'all', see --unate-lemmas=help)
-
-option arithPropagationMode --arith-prop=MODE ArithPropagationMode :handler CVC4::theory::arith::stringToArithPropagationMode :default BOTH_PROP :handler-include "theory/arith/options_handlers.h" :include "theory/arith/arith_propagation_mode.h"
- turns on arithmetic propagation (default is 'old', see --arith-prop=help)
-
-# The maximum number of difference pivots to do per invocation of simplex.
-# If this is negative, the number of pivots done is the number of variables.
-# If this is not set by the user, different logics are free to chose different
-# defaults.
-option arithHeuristicPivots --heuristic-pivots=N int16_t :default 0 :read-write
- the number of times to apply the heuristic pivot rule; if N < 0, this defaults to the number of variables; if this is unset, this is tuned by the logic selection
-
-# The maximum number of variable order pivots to do per invocation of simplex.
-# If this is negative, the number of pivots done is unlimited.
-# If this is not set by the user, different logics are free to chose different
-# defaults.
-expert-option arithStandardCheckVarOrderPivots --standard-effort-variable-order-pivots=N int16_t :default -1 :read-write
- limits the number of pivots in a single invocation of check() at a non-full effort level using Bland's pivot rule
-
-option arithErrorSelectionRule --error-selection-rule=RULE ErrorSelectionRule :handler CVC4::theory::arith::stringToErrorSelectionRule :default MINIMUM_AMOUNT :handler-include "theory/arith/options_handlers.h" :include "theory/arith/arith_heuristic_pivot_rule.h"
- change the pivot rule for the basic variable (default is 'min', see --pivot-rule help)
-
-# The number of pivots before simplex rechecks every basic variable for a conflict
-option arithSimplexCheckPeriod --simplex-check-period=N uint16_t :default 200
- the number of pivots to do in simplex before rechecking for a conflict on all variables
-
-# This is the pivots per basic variable that can be done using heuristic choices
-# before variable order must be used.
-# If this is not set by the user, different logics are free to chose different
-# defaults.
-option arithPivotThreshold --pivot-threshold=N uint16_t :default 2 :read-write
- sets the number of pivots using --pivot-rule per basic variable per simplex instance before using variable order
-
-option arithPropagateMaxLength --prop-row-length=N uint16_t :default 16
- sets the maximum row length to be used in propagation
-
-option arithDioSolver /--disable-dio-solver bool :default true
- turns off Linear Diophantine Equation solver (Griggio, JSAT 2012)
-
-# Whether to split (= x y) into (and (<= x y) (>= x y)) in
-# arithmetic preprocessing.
-option arithRewriteEq --enable-arith-rewrite-equalities/--disable-arith-rewrite-equalities bool :default false :read-write
- turns on the preprocessing rewrite turning equalities into a conjunction of inequalities
-/turns off the preprocessing rewrite turning equalities into a conjunction of inequalities
-
-
-option arithMLTrick miplib-trick --enable-miplib-trick/--disable-miplib-trick bool :default false
- turns on the preprocessing step of attempting to infer bounds on miplib problems
-/turns off the preprocessing step of attempting to infer bounds on miplib problems
-
-option arithMLTrickSubstitutions miplib-trick-subs --miplib-trick-subs=N unsigned :default 1
- do substitution for miplib 'tmp' vars if defined in <= N eliminated vars
-
-option doCutAllBounded --cut-all-bounded bool :default false :read-write
- turns on the integer solving step of periodically cutting all integer variables that have both upper and lower bounds
-/turns off the integer solving step of periodically cutting all integer variables that have both upper and lower bounds
-
-option maxCutsInContext --maxCutsInContext unsigned :default 65535
- maximum cuts in a given context before signalling a restart
-
-option revertArithModels --revert-arith-models-on-unsat bool :default false
- revert the arithmetic model to a known safe model on unsat if one is cached
-
-option havePenalties --fc-penalties bool :default false :read-write
- turns on degenerate pivot penalties
-/turns off degenerate pivot penalties
-
-option useFC --use-fcsimplex bool :default false :read-write
- use focusing and converging simplex (FMCAD 2013 submission)
-
-option useSOI --use-soi bool :default false :read-write
- use sum of infeasibility simplex (FMCAD 2013 submission)
-
-option restrictedPivots --restrict-pivots bool :default true :read-write
- have a pivot cap for simplex at effort levels below fullEffort
-
-option collectPivots --collect-pivot-stats bool :default false :read-write
- collect the pivot history
-
-option useApprox --use-approx bool :default false :read-write
- attempt to use an approximate solver
-
-option maxApproxDepth --approx-branch-depth int16_t :default 200 :read-write
- maximum branch depth the approximate solver is allowed to take
-
-option exportDioDecompositions --dio-decomps bool :default false :read-write
- let skolem variables for integer divisibility constraints leak from the dio solver
-
-option newProp --new-prop bool :default false :read-write
- use the new row propagation system
-
-option arithPropAsLemmaLength --arith-prop-clauses uint16_t :default 8 :read-write
- rows shorter than this are propagated as clauses
-
-option soiQuickExplain --soi-qe bool :default false :read-write
- use quick explain to minimize the sum of infeasibility conflicts
-
-option rewriteDivk rewrite-divk --rewrite-divk bool :default false :read-write
- rewrite division and mod when by a constant into linear terms
-
-option trySolveIntStandardEffort --se-solve-int bool :default false
- attempt to use the approximate solve integer method on standard effort
-
-option replayFailureLemma --lemmas-on-replay-failure bool :default false
- attempt to use external lemmas if approximate solve integer failed
-
-option dioSolverTurns --dio-turns int :default 10
- turns in a row dio solver cutting gets
-
-option rrTurns --rr-turns int :default 3
- round robin turn
-
-option dioRepeat --dio-repeat bool :default false
- handle dio solver constraints in mass or one at a time
-
-option replayEarlyCloseDepths --replay-early-close-depth int :default 1
- multiples of the depths to try to close the approx log eagerly
-
-option replayFailurePenalty --replay-failure-penalty int :default 100
- number of solve integer attempts to skips after a numeric failure
-
-option replayNumericFailurePenalty --replay-num-err-penalty int :default 4194304
- number of solve integer attempts to skips after a numeric failure
-
-option replayRejectCutSize --replay-reject-cut unsigned :default 25500
- maximum complexity of any coefficient while replaying cuts
-
-option lemmaRejectCutSize --replay-lemma-reject-cut unsigned :default 25500
- maximum complexity of any coefficient while outputing replaying cut lemmas
-
-option soiApproxMajorFailure --replay-soi-major-threshold double :default .01
- threshold for a major tolerance failure by the approximate solver
-
-option soiApproxMajorFailurePen --replay-soi-major-threshold-pen int :default 50
- threshold for a major tolerance failure by the approximate solver
-
-option soiApproxMinorFailure --replay-soi-minor-threshold double :default .0001
- threshold for a minor tolerance failure by the approximate solver
-
-option soiApproxMinorFailurePen --replay-soi-minor-threshold-pen int :default 10
- threshold for a minor tolerance failure by the approximate solver
-
-option ppAssertMaxSubSize --pp-assert-max-sub-size unsigned :default 2
- threshold for substituting an equality in ppAssert
-
-option maxReplayTree --max-replay-tree int :default 512
- threshold for attempting to replay a tree
-
-
-option pbRewrites --pb-rewrites bool :default false
- apply pseudo boolean rewrites
-
-option pbRewriteThreshold --pb-rewrite-threshold int :default 256
- threshold of number of pseudoboolean variables to have before doing rewrites
-
-endmodule
diff --git a/src/theory/arith/options_handlers.h b/src/theory/arith/options_handlers.h
deleted file mode 100644
index 57b9661ba..000000000
--- a/src/theory/arith/options_handlers.h
+++ /dev/null
@@ -1,122 +0,0 @@
-/*********************                                                        */
-/*! \file options_handlers.h
- ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): Kshitij Bansal, Tim King
- ** 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 arithmetic options
- **
- ** Custom handlers and predicates for arithmetic options.
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY__ARITH__OPTIONS_HANDLERS_H
-#define __CVC4__THEORY__ARITH__OPTIONS_HANDLERS_H
-
-#include <string>
-
-namespace CVC4 {
-namespace theory {
-namespace arith {
-
-static const std::string arithUnateLemmasHelp = "\
-Unate lemmas are generated before SAT search begins using the relationship\n\
-of constant terms and polynomials.\n\
-Modes currently supported by the --unate-lemmas option:\n\
-+ none \n\
-+ ineqs \n\
-  Outputs lemmas of the general form (<= p c) implies (<= p d) for c < d.\n\
-+ eqs \n\
-  Outputs lemmas of the general forms\n\
-  (= p c) implies (<= p d) for c < d, or\n\
-  (= p c) implies (not (= p d)) for c != d.\n\
-+ all \n\
-  A combination of inequalities and equalities.\n\
-";
-
-static const std::string propagationModeHelp = "\
-This decides on kind of propagation arithmetic attempts to do during the search.\n\
-+ none\n\
-+ unate\n\
- use constraints to do unate propagation\n\
-+ bi (Bounds Inference)\n\
-  infers bounds on basic variables using the upper and lower bounds of the\n\
-  non-basic variables in the tableau.\n\
-+both\n\
-";
-
-static const std::string errorSelectionRulesHelp = "\
-This decides on the rule used by simplex during heuristic rounds\n\
-for deciding the next basic variable to select.\n\
-Heuristic pivot rules available:\n\
-+min\n\
-  The minimum abs() value of the variable's violation of its bound. (default)\n\
-+max\n\
-  The maximum violation the bound\n\
-+varord\n\
-  The variable order\n\
-";
-
-inline ArithUnateLemmaMode stringToArithUnateLemmaMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
-  if(optarg == "all") {
-    return ALL_PRESOLVE_LEMMAS;
-  } else if(optarg == "none") {
-    return NO_PRESOLVE_LEMMAS;
-  } else if(optarg == "ineqs") {
-    return INEQUALITY_PRESOLVE_LEMMAS;
-  } else if(optarg == "eqs") {
-    return EQUALITY_PRESOLVE_LEMMAS;
-  } else if(optarg == "help") {
-    puts(arithUnateLemmasHelp.c_str());
-    exit(1);
-  } else {
-    throw OptionException(std::string("unknown option for --unate-lemmas: `") +
-                          optarg + "'.  Try --unate-lemmas help.");
-  }
-}
-
-inline ArithPropagationMode stringToArithPropagationMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
-  if(optarg == "none") {
-    return NO_PROP;
-  } else if(optarg == "unate") {
-    return UNATE_PROP;
-  } else if(optarg == "bi") {
-    return BOUND_INFERENCE_PROP;
-  } else if(optarg == "both") {
-    return BOTH_PROP;
-  } else if(optarg == "help") {
-    puts(propagationModeHelp.c_str());
-    exit(1);
-  } else {
-    throw OptionException(std::string("unknown option for --arith-prop: `") +
-                          optarg + "'.  Try --arith-prop help.");
-  }
-}
-
-inline ErrorSelectionRule stringToErrorSelectionRule(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
-  if(optarg == "min") {
-    return MINIMUM_AMOUNT;
-  } else if(optarg == "varord") {
-    return VAR_ORDER;
-  } else if(optarg == "max") {
-    return MAXIMUM_AMOUNT;
-  } else if(optarg == "help") {
-    puts(errorSelectionRulesHelp.c_str());
-    exit(1);
-  } else {
-    throw OptionException(std::string("unknown option for --heuristic-pivot-rule: `") +
-                          optarg + "'.  Try --heuristic-pivot-rule help.");
-  }
-}
-
-}/* CVC4::theory::arith namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__THEORY__ARITH__OPTIONS_HANDLERS_H */
diff --git a/src/theory/arith/partial_model.cpp b/src/theory/arith/partial_model.cpp
index cb853953f..0124ee0f9 100644
--- a/src/theory/arith/partial_model.cpp
+++ b/src/theory/arith/partial_model.cpp
@@ -15,11 +15,10 @@
  ** \todo document this file
  **/
 
-
-#include "theory/arith/partial_model.h"
-#include "util/output.h"
+#include "base/output.h"
 #include "theory/arith/constraint.h"
 #include "theory/arith/normal_form.h"
+#include "theory/arith/partial_model.h"
 
 using namespace std;
 
diff --git a/src/theory/arith/pseudoboolean_proc.cpp b/src/theory/arith/pseudoboolean_proc.cpp
index 829952c5e..c09b0180a 100644
--- a/src/theory/arith/pseudoboolean_proc.cpp
+++ b/src/theory/arith/pseudoboolean_proc.cpp
@@ -15,9 +15,10 @@
  ** \todo document this file
  **/
 
-#include "theory/arith/pseudoboolean_proc.h"
-#include "theory/arith/normal_form.h"
+#include "base/output.h"
 #include "theory/arith/arith_utilities.h"
+#include "theory/arith/normal_form.h"
+#include "theory/arith/pseudoboolean_proc.h"
 #include "theory/rewriter.h"
 
 namespace CVC4 {
diff --git a/src/theory/arith/pseudoboolean_proc.h b/src/theory/arith/pseudoboolean_proc.h
index 665f1aa06..d1e10f695 100644
--- a/src/theory/arith/pseudoboolean_proc.h
+++ b/src/theory/arith/pseudoboolean_proc.h
@@ -19,17 +19,16 @@
 
 #pragma once
 
+#include <ext/hash_set>
 #include <vector>
-#include "util/rational.h"
-#include "util/maybe.h"
-#include "expr/node.h"
 
-#include "context/context.h"
-#include "context/cdo.h"
 #include "context/cdhashmap.h"
-
+#include "context/cdo.h"
+#include "context/context.h"
+#include "expr/node.h"
 #include "theory/substitutions.h"
-#include <ext/hash_set>
+#include "util/maybe.h"
+#include "util/rational.h"
 
 namespace CVC4 {
 namespace theory {
@@ -107,4 +106,3 @@ private:
 }/* CVC4::theory::arith namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
-
diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp
index 49664e0ea..24c6ce432 100644
--- a/src/theory/arith/simplex.cpp
+++ b/src/theory/arith/simplex.cpp
@@ -16,9 +16,10 @@
  **/
 
 
-#include "theory/arith/simplex.h"
-#include "theory/arith/options.h"
+#include "base/output.h"
+#include "options/arith_options.h"
 #include "theory/arith/constraint.h"
+#include "theory/arith/simplex.h"
 
 
 using namespace std;
diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h
index 2d7fc597a..f39006788 100644
--- a/src/theory/arith/simplex.h
+++ b/src/theory/arith/simplex.h
@@ -53,15 +53,14 @@
 
 #pragma once
 
+#include "expr/result.h"
 #include "theory/arith/arithvar.h"
-#include "theory/arith/error_set.h"
 #include "theory/arith/delta_rational.h"
-#include "theory/arith/tableau.h"
-#include "theory/arith/partial_model.h"
+#include "theory/arith/error_set.h"
 #include "theory/arith/linear_equality.h"
-
+#include "theory/arith/partial_model.h"
+#include "theory/arith/tableau.h"
 #include "util/dense_map.h"
-#include "util/result.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/arith/soi_simplex.cpp b/src/theory/arith/soi_simplex.cpp
index 0d07c5ffc..765e6a00d 100644
--- a/src/theory/arith/soi_simplex.cpp
+++ b/src/theory/arith/soi_simplex.cpp
@@ -14,15 +14,15 @@
  ** [[ Add lengthier description here ]]
  ** \todo document this file
  **/
+#include "theory/arith/soi_simplex.h"
 
+#include <algorithm>
 
-#include "theory/arith/soi_simplex.h"
-#include "theory/arith/options.h"
+#include "base/output.h"
+#include "expr/statistics_registry.h"
+#include "options/arith_options.h"
 #include "theory/arith/constraint.h"
 
-#include "util/statistics_registry.h"
-
-#include <algorithm>
 
 using namespace std;
 
diff --git a/src/theory/arith/soi_simplex.h b/src/theory/arith/soi_simplex.h
index 6dd6373d4..b08d7794b 100644
--- a/src/theory/arith/soi_simplex.h
+++ b/src/theory/arith/soi_simplex.h
@@ -52,10 +52,11 @@
 
 #pragma once
 
+#include <stdint.h>
+
+#include "expr/statistics_registry.h"
 #include "theory/arith/simplex.h"
 #include "util/dense_map.h"
-#include "util/statistics_registry.h"
-#include <stdint.h>
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/arith/tableau.cpp b/src/theory/arith/tableau.cpp
index 231eb1562..744dda6b7 100644
--- a/src/theory/arith/tableau.cpp
+++ b/src/theory/arith/tableau.cpp
@@ -15,6 +15,7 @@
  ** \todo document this file
  **/
 
+#include "base/output.h"
 #include "theory/arith/tableau.h"
 
 using namespace std;
diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h
index c6750f61b..77187c798 100644
--- a/src/theory/arith/tableau.h
+++ b/src/theory/arith/tableau.h
@@ -19,11 +19,12 @@
 
 #pragma once
 
-#include "util/dense_map.h"
-#include "util/rational.h"
+#include <vector>
+
 #include "theory/arith/arithvar.h"
 #include "theory/arith/matrix.h"
-#include <vector>
+#include "util/dense_map.h"
+#include "util/rational.h"
 
 namespace CVC4 {
 namespace theory {
@@ -161,4 +162,3 @@ private:
 }/* CVC4::theory::arith namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
-
diff --git a/src/theory/arith/tableau_sizes.cpp b/src/theory/arith/tableau_sizes.cpp
index fdd9ff16a..64bae22fe 100644
--- a/src/theory/arith/tableau_sizes.cpp
+++ b/src/theory/arith/tableau_sizes.cpp
@@ -15,6 +15,7 @@
  ** \todo document this file
  **/
 
+#include "base/output.h"
 #include "theory/arith/tableau_sizes.h"
 #include "theory/arith/tableau.h"
 
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 565c69514..1e3b21b17 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -16,9 +16,10 @@
  **/
 
 #include "theory/arith/theory_arith.h"
-#include "theory/arith/theory_arith_private.h"
+
+#include "options/smt_options.h"
 #include "theory/arith/infer_bounds.h"
-#include "smt/options.h"
+#include "theory/arith/theory_arith_private.h"
 
 using namespace std;
 using namespace CVC4::kind;
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index c9c45af2f..ab800f10d 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -17,71 +17,59 @@
 
 #include "theory/arith/theory_arith_private.h"
 
-#include "expr/node.h"
-#include "expr/kind.h"
-#include "expr/metakind.h"
-#include "expr/node_builder.h"
+#include <stdint.h>
 
-#include "context/context.h"
-#include "context/cdlist.h"
+#include <map>
+#include <queue>
+#include <vector>
+
+#include "base/output.h"
 #include "context/cdhashset.h"
 #include "context/cdinsert_hashmap.h"
+#include "context/cdlist.h"
 #include "context/cdqueue.h"
-
-#include "theory/valuation.h"
-#include "theory/rewriter.h"
-
-#include "util/rational.h"
-#include "util/integer.h"
-#include "util/boolean_simplification.h"
-#include "util/dense_map.h"
-#include "util/statistics_registry.h"
-#include "util/result.h"
-
-#include "smt/logic_request.h"
+#include "context/context.h"
+#include "expr/kind.h"
+#include "expr/metakind.h"
+#include "expr/node.h"
+#include "expr/node_builder.h"
+#include "expr/result.h"
+#include "expr/statistics_registry.h"
+#include "options/arith_options.h"
+#include "options/smt_options.h"  // for incrementalSolving()
 #include "smt/logic_exception.h"
-#include "smt/options.h"  // for incrementalSolving()
-
-#include "theory/arith/arithvar.h"
-#include "theory/arith/cut_log.h"
-#include "theory/arith/delta_rational.h"
-#include "theory/arith/matrix.h"
+#include "smt/logic_request.h"
+#include "smt_util/boolean_simplification.h"
+#include "theory/arith/approx_simplex.h"
+#include "theory/arith/arith_ite_utils.h"
+#include "theory/arith/arith_rewriter.h"
 #include "theory/arith/arith_rewriter.h"
-#include "theory/arith/partial_model.h"
-#include "theory/arith/linear_equality.h"
-#include "theory/arith/simplex.h"
 #include "theory/arith/arith_static_learner.h"
-#include "theory/arith/dio_solver.h"
+#include "theory/arith/arith_utilities.h"
+#include "theory/arith/arithvar.h"
 #include "theory/arith/congruence_manager.h"
-
-#include "theory/arith/approx_simplex.h"
 #include "theory/arith/constraint.h"
-
-#include "theory/ite_utilities.h"
-#include "theory/arith/arith_ite_utils.h"
-
-#include "theory/arith/arith_utilities.h"
+#include "theory/arith/constraint.h"
+#include "theory/arith/cut_log.h"
 #include "theory/arith/delta_rational.h"
-#include "theory/arith/partial_model.h"
+#include "theory/arith/delta_rational.h"
+#include "theory/arith/dio_solver.h"
+#include "theory/arith/linear_equality.h"
+#include "theory/arith/matrix.h"
 #include "theory/arith/matrix.h"
-
-#include "theory/arith/arith_rewriter.h"
-#include "theory/arith/constraint.h"
-#include "theory/arith/theory_arith.h"
 #include "theory/arith/normal_form.h"
-#include "theory/theory_model.h"
-
-#include "theory/arith/options.h"
-#include "theory/quantifiers/options.h"
-
-
+#include "theory/arith/partial_model.h"
+#include "theory/arith/partial_model.h"
+#include "theory/arith/simplex.h"
+#include "theory/arith/theory_arith.h"
+#include "theory/ite_utilities.h"
 #include "theory/quantifiers/bounded_integers.h"
-
-#include <stdint.h>
-
-#include <vector>
-#include <map>
-#include <queue>
+#include "theory/rewriter.h"
+#include "theory/theory_model.h"
+#include "theory/valuation.h"
+#include "util/dense_map.h"
+#include "util/integer.h"
+#include "util/rational.h"
 
 using namespace std;
 using namespace CVC4::kind;
diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index 4c539c60d..0c2a704e8 100644
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -17,70 +17,56 @@
 
 #pragma once
 
-#include "theory/arith/theory_arith_private_forward.h"
-
-#include "expr/node.h"
-#include "expr/kind.h"
-#include "expr/metakind.h"
-#include "expr/node_builder.h"
+#include <map>
+#include <queue>
+#include <stdint.h>
+#include <vector>
 
-#include "context/context.h"
-#include "context/cdlist.h"
 #include "context/cdhashset.h"
 #include "context/cdinsert_hashmap.h"
+#include "context/cdlist.h"
 #include "context/cdqueue.h"
-
-#include "theory/valuation.h"
-#include "theory/rewriter.h"
-
-#include "util/rational.h"
-#include "util/integer.h"
-#include "util/boolean_simplification.h"
-#include "util/dense_map.h"
-#include "util/statistics_registry.h"
-#include "util/result.h"
-
+#include "context/context.h"
+#include "expr/kind.h"
+#include "expr/metakind.h"
+#include "expr/node.h"
+#include "expr/node_builder.h"
+#include "expr/result.h"
+#include "expr/statistics_registry.h"
+#include "options/arith_options.h"
 #include "smt/logic_exception.h"
-
-
-
-#include "theory/arith/arithvar.h"
-#include "theory/arith/delta_rational.h"
-#include "theory/arith/matrix.h"
+#include "smt_util/boolean_simplification.h"
+#include "theory/arith/arith_rewriter.h"
 #include "theory/arith/arith_rewriter.h"
-#include "theory/arith/partial_model.h"
-#include "theory/arith/linear_equality.h"
 #include "theory/arith/arith_static_learner.h"
-#include "theory/arith/dio_solver.h"
-#include "theory/arith/congruence_manager.h"
-
-#include "theory/arith/simplex.h"
-#include "theory/arith/dual_simplex.h"
-#include "theory/arith/fc_simplex.h"
-#include "theory/arith/soi_simplex.h"
+#include "theory/arith/arith_utilities.h"
+#include "theory/arith/arithvar.h"
 #include "theory/arith/attempt_solution_simplex.h"
-
+#include "theory/arith/congruence_manager.h"
+#include "theory/arith/constraint.h"
 #include "theory/arith/constraint.h"
-
-#include "theory/arith/arith_utilities.h"
 #include "theory/arith/delta_rational.h"
+#include "theory/arith/delta_rational.h"
+#include "theory/arith/dio_solver.h"
+#include "theory/arith/dual_simplex.h"
+#include "theory/arith/fc_simplex.h"
 #include "theory/arith/infer_bounds.h"
-#include "theory/arith/partial_model.h"
+#include "theory/arith/linear_equality.h"
+#include "theory/arith/matrix.h"
 #include "theory/arith/matrix.h"
-
-#include "theory/arith/arith_rewriter.h"
-#include "theory/arith/constraint.h"
-#include "theory/arith/theory_arith.h"
 #include "theory/arith/normal_form.h"
+#include "theory/arith/partial_model.h"
+#include "theory/arith/partial_model.h"
+#include "theory/arith/simplex.h"
+#include "theory/arith/soi_simplex.h"
+#include "theory/arith/theory_arith.h"
+#include "theory/arith/theory_arith_private_forward.h"
+#include "theory/rewriter.h"
 #include "theory/theory_model.h"
-
-#include "theory/arith/options.h"
-
-#include <stdint.h>
-
-#include <vector>
-#include <map>
-#include <queue>
+#include "theory/valuation.h"
+#include "util/dense_map.h"
+#include "util/integer.h"
+#include "util/rational.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/arith/type_enumerator.h b/src/theory/arith/type_enumerator.h
index f661e18d3..c4501fc43 100644
--- a/src/theory/arith/type_enumerator.h
+++ b/src/theory/arith/type_enumerator.h
@@ -19,11 +19,11 @@
 #ifndef __CVC4__THEORY__ARITH__TYPE_ENUMERATOR_H
 #define __CVC4__THEORY__ARITH__TYPE_ENUMERATOR_H
 
+#include "expr/kind.h"
+#include "expr/type_node.h"
+#include "theory/type_enumerator.h"
 #include "util/integer.h"
 #include "util/rational.h"
-#include "theory/type_enumerator.h"
-#include "expr/type_node.h"
-#include "expr/kind.h"
 
 namespace CVC4 {
 namespace theory {