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.

37 files changed, 150 insertions, 1186 deletions

diff --git a/src/theory/quantifiers/ambqi_builder.cpp b/src/theory/quantifiers/ambqi_builder.cpp
index f047276b0..b18676cbc 100644
--- a/src/theory/quantifiers/ambqi_builder.cpp
+++ b/src/theory/quantifiers/ambqi_builder.cpp
@@ -13,9 +13,9 @@
  **/
 
 
+#include "options/quantifiers_options.h"
 #include "theory/quantifiers/ambqi_builder.h"
 #include "theory/quantifiers/term_database.h"
-#include "theory/quantifiers/options.h"
 
 using namespace std;
 using namespace CVC4;
diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp
index 2fd595a9f..ceab8394f 100644
--- a/src/theory/quantifiers/bounded_integers.cpp
+++ b/src/theory/quantifiers/bounded_integers.cpp
@@ -14,12 +14,12 @@
  ** This class manages integer bounds for quantifiers
  **/
 
+#include "options/quantifiers_options.h"
 #include "theory/quantifiers/bounded_integers.h"
-#include "theory/quantifiers/quant_util.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/model_engine.h"
+#include "theory/quantifiers/quant_util.h"
 #include "theory/quantifiers/term_database.h"
-#include "theory/quantifiers/options.h"
 
 using namespace CVC4;
 using namespace std;
@@ -425,4 +425,3 @@ void BoundedIntegers::getBoundValues( Node f, Node v, RepSetIterator * rsi, Node
 bool BoundedIntegers::isGroundRange(Node f, Node v) {
   return isBoundVar(f,v) && !getLowerBound(f,v).hasBoundVar() && !getUpperBound(f,v).hasBoundVar();
 }
-
diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp
index b67c4bd56..0cdb22be4 100644
--- a/src/theory/quantifiers/candidate_generator.cpp
+++ b/src/theory/quantifiers/candidate_generator.cpp
@@ -12,13 +12,13 @@
  ** \brief Implementation of theory uf candidate generator class
  **/
 
+#include "options/quantifiers_options.h"
 #include "theory/quantifiers/candidate_generator.h"
-#include "theory/theory_engine.h"
-#include "theory/uf/theory_uf.h"
-#include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/inst_match.h"
+#include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers_engine.h"
-#include "theory/quantifiers/options.h"
+#include "theory/theory_engine.h"
+#include "theory/uf/theory_uf.h"
 
 using namespace std;
 using namespace CVC4;
diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index 398ae1ffe..81fe00674 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -12,14 +12,14 @@
  ** \brief counterexample guided instantiation class
  **
  **/
-
 #include "theory/quantifiers/ce_guided_instantiation.h"
-#include "theory/theory_engine.h"
-#include "theory/quantifiers/options.h"
-#include "theory/quantifiers/term_database.h"
-#include "theory/quantifiers/first_order_model.h"
+
+#include "expr/datatype.h"
+#include "options/quantifiers_options.h"
 #include "theory/datatypes/datatypes_rewriter.h"
-#include "util/datatype.h"
+#include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/term_database.h"
+#include "theory/theory_engine.h"
 
 using namespace CVC4;
 using namespace CVC4::kind;
diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h
index 6fcfdbc58..8274561ca 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.h
+++ b/src/theory/quantifiers/ce_guided_instantiation.h
@@ -17,11 +17,11 @@
 #ifndef __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_INSTANTIATION_H
 #define __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_INSTANTIATION_H
 
-#include "context/cdhashmap.h"
 #include "context/cdchunk_list.h"
-#include "theory/quantifiers_engine.h"
+#include "context/cdhashmap.h"
+#include "options/quantifiers_modes.h"
 #include "theory/quantifiers/ce_guided_single_inv.h"
-#include "theory/quantifiers/modes.h"
+#include "theory/quantifiers_engine.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp
index f533a2bbb..7ef23077f 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv.cpp
@@ -12,18 +12,18 @@
  ** \brief utility for processing single invocation synthesis conjectures
  **
  **/
-
 #include "theory/quantifiers/ce_guided_single_inv.h"
+
+#include "expr/datatype.h"
+#include "options/quantifiers_options.h"
+#include "theory/datatypes/datatypes_rewriter.h"
 #include "theory/quantifiers/ce_guided_instantiation.h"
 #include "theory/quantifiers/ce_guided_single_inv_ei.h"
-#include "theory/theory_engine.h"
-#include "theory/quantifiers/options.h"
-#include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/first_order_model.h"
-#include "theory/datatypes/datatypes_rewriter.h"
-#include "util/datatype.h"
 #include "theory/quantifiers/quant_util.h"
+#include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/trigger.h"
+#include "theory/theory_engine.h"
 
 using namespace CVC4;
 using namespace CVC4::kind;
@@ -1186,4 +1186,4 @@ void SingleInvocationPartition::debugPrint( const char * c ) {
   Trace(c) << std::endl;
 }
 
-}
\ No newline at end of file
+}
diff --git a/src/theory/quantifiers/ce_guided_single_inv_ei.cpp b/src/theory/quantifiers/ce_guided_single_inv_ei.cpp
index 18252e190..f45285851 100644
--- a/src/theory/quantifiers/ce_guided_single_inv_ei.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv_ei.cpp
@@ -13,12 +13,12 @@
  **
  **/
 
-#include "theory/quantifiers/ce_guided_single_inv_ei.h"
+#include "options/quantifiers_options.h"
 #include "theory/quantifiers/ce_guided_instantiation.h"
-#include "theory/theory_engine.h"
-#include "theory/quantifiers/options.h"
-#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/ce_guided_single_inv_ei.h"
 #include "theory/quantifiers/quant_util.h"
+#include "theory/quantifiers/term_database.h"
+#include "theory/theory_engine.h"
 
 using namespace CVC4;
 using namespace CVC4::kind;
@@ -44,4 +44,4 @@ bool CegEntailmentInfer::getEntailedConjecture( Node& conj, Node& exp ) {
   return false;
 }
 
-}
\ No newline at end of file
+}
diff --git a/src/theory/quantifiers/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/ce_guided_single_inv_sol.cpp
index 8fd935368..6ba5bed02 100644
--- a/src/theory/quantifiers/ce_guided_single_inv_sol.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv_sol.cpp
@@ -12,18 +12,18 @@
  ** \brief utility for processing single invocation synthesis conjectures
  **
  **/
-
 #include "theory/quantifiers/ce_guided_single_inv_sol.h"
-#include "theory/quantifiers/ce_guided_single_inv.h"
+
+#include "expr/datatype.h"
+#include "options/quantifiers_options.h"
+#include "theory/datatypes/datatypes_rewriter.h"
 #include "theory/quantifiers/ce_guided_instantiation.h"
-#include "theory/theory_engine.h"
-#include "theory/quantifiers/options.h"
-#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/ce_guided_single_inv.h"
 #include "theory/quantifiers/first_order_model.h"
-#include "theory/datatypes/datatypes_rewriter.h"
-#include "util/datatype.h"
 #include "theory/quantifiers/quant_util.h"
+#include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/trigger.h"
+#include "theory/theory_engine.h"
 
 using namespace CVC4;
 using namespace CVC4::kind;
diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp
index 7c10da90c..cea90621d 100644
--- a/src/theory/quantifiers/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/ceg_instantiator.cpp
@@ -11,16 +11,16 @@
  **
  ** \brief Implementation of counterexample-guided quantifier instantiation
  **/
-
 #include "theory/quantifiers/ceg_instantiator.h"
-#include "theory/arith/theory_arith.h"
+
+#include "options/quantifiers_options.h"
+#include "smt_util/ite_removal.h"
 #include "theory/arith/partial_model.h"
+#include "theory/arith/theory_arith.h"
 #include "theory/arith/theory_arith_private.h"
-#include "theory/theory_engine.h"
-#include "theory/quantifiers/options.h"
-#include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/first_order_model.h"
-#include "util/ite_removal.h"
+#include "theory/quantifiers/term_database.h"
+#include "theory/theory_engine.h"
 
 //#define MBP_STRICT_ASSERTIONS
 
diff --git a/src/theory/quantifiers/ceg_instantiator.h b/src/theory/quantifiers/ceg_instantiator.h
index 9504bd407..5b3c5263f 100644
--- a/src/theory/quantifiers/ceg_instantiator.h
+++ b/src/theory/quantifiers/ceg_instantiator.h
@@ -18,8 +18,8 @@
 #ifndef __CVC4__CEG_INSTANTIATOR_H
 #define __CVC4__CEG_INSTANTIATOR_H
 
+#include "expr/statistics_registry.h"
 #include "theory/quantifiers_engine.h"
-#include "util/statistics_registry.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index 1cdad589b..8e083ae1e 100644
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -13,12 +13,12 @@
  **
  **/
 
+#include "options/quantifiers_options.h"
 #include "theory/quantifiers/conjecture_generator.h"
-#include "theory/theory_engine.h"
-#include "theory/quantifiers/options.h"
+#include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/trigger.h"
-#include "theory/quantifiers/first_order_model.h"
+#include "theory/theory_engine.h"
 
 using namespace CVC4;
 using namespace CVC4::kind;
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index 36d055b69..095e7868e 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -12,13 +12,13 @@
  ** \brief Implementation of model engine model class
  **/
 
+#include "options/quantifiers_options.h"
+#include "theory/quantifiers/ambqi_builder.h"
 #include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/full_model_check.h"
 #include "theory/quantifiers/model_engine.h"
-#include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
-#include "theory/quantifiers/full_model_check.h"
-#include "theory/quantifiers/ambqi_builder.h"
-#include "theory/quantifiers/options.h"
+#include "theory/quantifiers/term_database.h"
 
 #define USE_INDEX_ORDERING
 
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index c3a723fce..02c6bbba8 100644
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -12,9 +12,9 @@
  ** \brief Implementation of full model check class
  **/
 
-#include "theory/quantifiers/full_model_check.h"
+#include "options/quantifiers_options.h"
 #include "theory/quantifiers/first_order_model.h"
-#include "theory/quantifiers/options.h"
+#include "theory/quantifiers/full_model_check.h"
 #include "theory/quantifiers/term_database.h"
 
 using namespace std;
diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp
index f4e8861dc..89c2d4868 100644
--- a/src/theory/quantifiers/inst_match_generator.cpp
+++ b/src/theory/quantifiers/inst_match_generator.cpp
@@ -11,15 +11,15 @@
  **
  ** [[ Add lengthier description here ]]
  ** \todo document this file
-**/
-
+ **/
 #include "theory/quantifiers/inst_match_generator.h"
-#include "theory/quantifiers/trigger.h"
-#include "theory/quantifiers/term_database.h"
+
+#include "expr/datatype.h"
+#include "options/quantifiers_options.h"
 #include "theory/quantifiers/candidate_generator.h"
+#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/trigger.h"
 #include "theory/quantifiers_engine.h"
-#include "theory/quantifiers/options.h"
-#include "util/datatype.h"
 
 using namespace std;
 using namespace CVC4;
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index eff1c0d9b..a4632398d 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -11,17 +11,17 @@
  **
  ** \brief Implementation of counterexample-guided quantifier instantiation strategies
  **/
-
 #include "theory/quantifiers/inst_strategy_cbqi.h"
-#include "theory/arith/theory_arith.h"
+
+#include "options/quantifiers_options.h"
+#include "smt_util/ite_removal.h"
 #include "theory/arith/partial_model.h"
+#include "theory/arith/theory_arith.h"
 #include "theory/arith/theory_arith_private.h"
-#include "theory/theory_engine.h"
-#include "theory/quantifiers/options.h"
-#include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/trigger.h"
-#include "util/ite_removal.h"
+#include "theory/theory_engine.h"
 
 using namespace std;
 using namespace CVC4;
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h
index d14b85111..b8bc25c6a 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.h
+++ b/src/theory/quantifiers/inst_strategy_cbqi.h
@@ -18,11 +18,10 @@
 #ifndef __CVC4__INST_STRATEGY_CBQI_H
 #define __CVC4__INST_STRATEGY_CBQI_H
 
-#include "theory/quantifiers/instantiation_engine.h"
+#include "expr/statistics_registry.h"
 #include "theory/arith/arithvar.h"
 #include "theory/quantifiers/ceg_instantiator.h"
-
-#include "util/statistics_registry.h"
+#include "theory/quantifiers/instantiation_engine.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp
index 9237d95c2..299eb51fd 100644
--- a/src/theory/quantifiers/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp
@@ -14,11 +14,11 @@
 
 #include "theory/quantifiers/inst_strategy_e_matching.h"
 
-#include "theory/theory_engine.h"
-#include "theory/quantifiers/options.h"
-#include "theory/quantifiers/term_database.h"
+#include "options/quantifiers_options.h"
 #include "theory/quantifiers/inst_match_generator.h"
 #include "theory/quantifiers/relevant_domain.h"
+#include "theory/quantifiers/term_database.h"
+#include "theory/theory_engine.h"
 
 using namespace std;
 using namespace CVC4;
@@ -652,4 +652,3 @@ bool FullSaturation::process( Node f, bool fullEffort ){
 void FullSaturation::registerQuantifier( Node q ) {
 
 }
-
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.h b/src/theory/quantifiers/inst_strategy_e_matching.h
index 2f7e7dcf1..a19bcca76 100644
--- a/src/theory/quantifiers/inst_strategy_e_matching.h
+++ b/src/theory/quantifiers/inst_strategy_e_matching.h
@@ -17,14 +17,12 @@
 #ifndef __CVC4__INST_STRATEGY_E_MATCHING_H
 #define __CVC4__INST_STRATEGY_E_MATCHING_H
 
-#include "theory/quantifiers_engine.h"
-#include "theory/quantifiers/trigger.h"
-
 #include "context/context.h"
 #include "context/context_mm.h"
-
-#include "util/statistics_registry.h"
+#include "expr/statistics_registry.h"
 #include "theory/quantifiers/instantiation_engine.h"
+#include "theory/quantifiers/trigger.h"
+#include "theory/quantifiers_engine.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index 16cecb657..88a67e3c8 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -14,12 +14,12 @@
 
 #include "theory/quantifiers/instantiation_engine.h"
 
-#include "theory/theory_engine.h"
-#include "theory/quantifiers/options.h"
-#include "theory/quantifiers/term_database.h"
+#include "options/quantifiers_options.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/inst_strategy_e_matching.h"
+#include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/trigger.h"
+#include "theory/theory_engine.h"
 
 using namespace std;
 using namespace CVC4;
diff --git a/src/theory/quantifiers/macros.cpp b/src/theory/quantifiers/macros.cpp
index 163005806..a5e3dada8 100644
--- a/src/theory/quantifiers/macros.cpp
+++ b/src/theory/quantifiers/macros.cpp
@@ -14,16 +14,17 @@
  ** This class implements quantifiers macro definitions.
  **/
 
+#include "theory/quantifiers/macros.h"
+
 #include <vector>
 
-#include "theory/quantifiers/macros.h"
-#include "theory/rewriter.h"
+#include "options/quantifiers_modes.h"
+#include "options/quantifiers_options.h"
 #include "proof/proof_manager.h"
 #include "smt/smt_engine_scope.h"
-#include "theory/quantifiers/modes.h"
-#include "theory/quantifiers/options.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/trigger.h"
+#include "theory/rewriter.h"
 
 using namespace CVC4;
 using namespace std;
@@ -485,4 +486,4 @@ void QuantifierMacros::addMacro( Node op, Node n, std::vector< Node >& opc ) {
       }
     }
   }
-}
\ No newline at end of file
+}
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index 79b995ef0..dc18548a5 100644
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -12,18 +12,19 @@
  ** \brief Implementation of model builder class
  **/
 
+#include "theory/quantifiers/model_builder.h"
+
+#include "options/quantifiers_options.h"
+#include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/model_engine.h"
+#include "theory/quantifiers/quantifiers_attributes.h"
+#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/trigger.h"
 #include "theory/theory_engine.h"
 #include "theory/uf/equality_engine.h"
 #include "theory/uf/theory_uf.h"
 #include "theory/uf/theory_uf_model.h"
 #include "theory/uf/theory_uf_strong_solver.h"
-#include "theory/quantifiers/first_order_model.h"
-#include "theory/quantifiers/term_database.h"
-#include "theory/quantifiers/model_builder.h"
-#include "theory/quantifiers/quantifiers_attributes.h"
-#include "theory/quantifiers/trigger.h"
-#include "theory/quantifiers/options.h"
 
 using namespace std;
 using namespace CVC4;
@@ -745,5 +746,3 @@ void QModelBuilderDefault::constructModelUf( FirstOrderModel* fm, Node op ){
     Debug("fmf-model-cons") << "  Finished constructing model for " << op << "." << std::endl;
   }
 }
-
-
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index f5a063eb8..6a21a50e5 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -13,16 +13,17 @@
  **/
 
 #include "theory/quantifiers/model_engine.h"
+
+#include "options/quantifiers_options.h"
+#include "theory/quantifiers/ambqi_builder.h"
+#include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/full_model_check.h"
+#include "theory/quantifiers/quantifiers_attributes.h"
+#include "theory/quantifiers/term_database.h"
 #include "theory/theory_engine.h"
 #include "theory/uf/equality_engine.h"
 #include "theory/uf/theory_uf.h"
 #include "theory/uf/theory_uf_strong_solver.h"
-#include "theory/quantifiers/options.h"
-#include "theory/quantifiers/first_order_model.h"
-#include "theory/quantifiers/term_database.h"
-#include "theory/quantifiers/quantifiers_attributes.h"
-#include "theory/quantifiers/full_model_check.h"
-#include "theory/quantifiers/ambqi_builder.h"
 
 using namespace std;
 using namespace CVC4;
@@ -335,5 +336,3 @@ ModelEngine::Statistics::~Statistics(){
   StatisticsRegistry::unregisterStat(&d_exh_inst_lemmas);
   StatisticsRegistry::unregisterStat(&d_mbqi_inst_lemmas);
 }
-
-
diff --git a/src/theory/quantifiers/modes.cpp b/src/theory/quantifiers/modes.cpp
deleted file mode 100644
index 253f23561..000000000
--- a/src/theory/quantifiers/modes.cpp
+++ /dev/null
@@ -1,86 +0,0 @@
-/*********************                                                        */
-/*! \file modes.cpp
- ** \verbatim
- ** Original author: Andrew Reynolds
- ** Major contributors: Morgan Deters
- ** 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 <iostream>
-#include "theory/quantifiers/modes.h"
-
-namespace CVC4 {
-
-std::ostream& operator<<(std::ostream& out, theory::quantifiers::InstWhenMode mode) {
-  switch(mode) {
-  case theory::quantifiers::INST_WHEN_PRE_FULL:
-    out << "INST_WHEN_PRE_FULL";
-    break;
-  case theory::quantifiers::INST_WHEN_FULL:
-    out << "INST_WHEN_FULL";
-    break;
-  case theory::quantifiers::INST_WHEN_FULL_LAST_CALL:
-    out << "INST_WHEN_FULL_LAST_CALL";
-    break;
-  case theory::quantifiers::INST_WHEN_LAST_CALL:
-    out << "INST_WHEN_LAST_CALL";
-    break;
-  default:
-    out << "InstWhenMode!UNKNOWN";
-  }
-
-  return out;
-}
-
-std::ostream& operator<<(std::ostream& out, theory::quantifiers::LiteralMatchMode mode) {
-  switch(mode) {
-  case theory::quantifiers::LITERAL_MATCH_NONE:
-    out << "LITERAL_MATCH_NONE";
-    break;
-  case theory::quantifiers::LITERAL_MATCH_PREDICATE:
-    out << "LITERAL_MATCH_PREDICATE";
-    break;
-  case theory::quantifiers::LITERAL_MATCH_EQUALITY:
-    out << "LITERAL_MATCH_EQUALITY";
-    break;
-  default:
-    out << "LiteralMatchMode!UNKNOWN";
-  }
-
-  return out;
-}
-
-std::ostream& operator<<(std::ostream& out, theory::quantifiers::MbqiMode mode) {
-  switch(mode) {
-  case theory::quantifiers::MBQI_GEN_EVAL:
-    out << "MBQI_GEN_EVAL";
-    break;
-  case theory::quantifiers::MBQI_NONE:
-    out << "MBQI_NONE";
-    break;
-  case theory::quantifiers::MBQI_FMC:
-    out << "MBQI_FMC";
-    break;
-  case theory::quantifiers::MBQI_ABS:
-    out << "MBQI_ABS";
-    break;
-  case theory::quantifiers::MBQI_TRUST:
-    out << "MBQI_TRUST";
-    break;
-  default:
-    out << "MbqiMode!UNKNOWN";
-  }
-  return out;
-}
-
-}/* CVC4 namespace */
-
diff --git a/src/theory/quantifiers/modes.h b/src/theory/quantifiers/modes.h
deleted file mode 100644
index 01d3f0c22..000000000
--- a/src/theory/quantifiers/modes.h
+++ /dev/null
@@ -1,173 +0,0 @@
-/*********************                                                        */
-/*! \file modes.h
- ** \verbatim
- ** Original author: Andrew Reynolds
- ** Major contributors: Morgan Deters
- ** 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__QUANTIFIERS__MODES_H
-#define __CVC4__THEORY__QUANTIFIERS__MODES_H
-
-#include <iostream>
-
-namespace CVC4 {
-namespace theory {
-namespace quantifiers {
-
-typedef enum {
-  /** Apply instantiation round before full effort (possibly at standard effort) */
-  INST_WHEN_PRE_FULL,
-  /** Apply instantiation round at full effort or above  */
-  INST_WHEN_FULL,
-  /** Apply instantiation round at full effort, after all other theories finish, or above  */
-  INST_WHEN_FULL_DELAY,
-  /** Apply instantiation round at full effort half the time, and last call always */
-  INST_WHEN_FULL_LAST_CALL,
-  /** Apply instantiation round at full effort after all other theories finish half the time, and last call always */
-  INST_WHEN_FULL_DELAY_LAST_CALL,
-  /** Apply instantiation round at last call only */
-  INST_WHEN_LAST_CALL,
-} InstWhenMode;
-
-typedef enum {
-  /** Do not consider polarity of patterns */
-  LITERAL_MATCH_NONE,
-  /** Consider polarity of boolean predicates only */
-  LITERAL_MATCH_PREDICATE,
-  /** Consider polarity of boolean predicates, as well as equalities */
-  LITERAL_MATCH_EQUALITY,
-} LiteralMatchMode;
-
-typedef enum {
-  /** mbqi from CADE 24 paper */
-  MBQI_GEN_EVAL,
-  /** no mbqi */
-  MBQI_NONE,
-  /** default, mbqi from Section 5.4.2 of AJR thesis */
-  MBQI_FMC,
-  /** mbqi with integer intervals */
-  MBQI_FMC_INTERVAL,
-  /** abstract mbqi algorithm */
-  MBQI_ABS,
-  /** mbqi trust (produce no instantiations) */
-  MBQI_TRUST,
-} MbqiMode;
-
-typedef enum {
-  /** default, apply at full effort */
-  QCF_WHEN_MODE_DEFAULT,
-  /** apply at last call */
-  QCF_WHEN_MODE_LAST_CALL,
-  /** apply at standard effort */
-  QCF_WHEN_MODE_STD,
-  /** apply based on heuristics */
-  QCF_WHEN_MODE_STD_H,
-} QcfWhenMode;
-
-typedef enum {
-  /** default, use qcf for conflicts only */
-  QCF_CONFLICT_ONLY,
-  /** use qcf for conflicts and propagations */
-  QCF_PROP_EQ,
-  /** use qcf for conflicts, propagations and heuristic instantiations */
-  QCF_PARTIAL,
-  /** use qcf for model checking */
-  QCF_MC,
-} QcfMode;
-
-typedef enum {
-  /** use but do not trust */
-  USER_PAT_MODE_USE,
-  /** default, if patterns are supplied for a quantifier, use only those */
-  USER_PAT_MODE_TRUST,
-  /** resort to user patterns only when necessary */
-  USER_PAT_MODE_RESORT,
-  /** ignore user patterns */
-  USER_PAT_MODE_IGNORE,
-  /** interleave use/resort for user patterns */
-  USER_PAT_MODE_INTERLEAVE,
-} UserPatMode;
-
-typedef enum {
-  /** default for trigger selection */
-  TRIGGER_SEL_DEFAULT,
-  /** only consider minimal terms for triggers */
-  TRIGGER_SEL_MIN,
-  /** only consider maximal terms for triggers */
-  TRIGGER_SEL_MAX,
-} TriggerSelMode;
-
-typedef enum CVC4_PUBLIC {
-  /** default : prenex quantifiers without user patterns */
-  PRENEX_NO_USER_PAT,
-  /** prenex all */
-  PRENEX_ALL,
-  /** prenex none */
-  PRENEX_NONE,
-} PrenexQuantMode;
-
-typedef enum {
-  /** enforce fairness by UF corresponding to datatypes size */
-  CEGQI_FAIR_UF_DT_SIZE,
-  /** enforce fairness by datatypes size */
-  CEGQI_FAIR_DT_SIZE,
-  /** enforce fairness by datatypes height bound */
-  CEGQI_FAIR_DT_HEIGHT_PRED,
-  /** do not use fair strategy for CEGQI */
-  CEGQI_FAIR_NONE,
-} CegqiFairMode;
-
-typedef enum {
-  /** consider all terms in master equality engine */
-  TERM_DB_ALL,
-  /** consider only relevant terms */
-  TERM_DB_RELEVANT,
-} TermDbMode;
-
-typedef enum {
-  /** do not lift ITEs in quantified formulas */
-  ITE_LIFT_QUANT_MODE_NONE,
-  /** only lift ITEs in quantified formulas if reduces the term size */
-  ITE_LIFT_QUANT_MODE_SIMPLE,
-  /** lift ITEs  */
-  ITE_LIFT_QUANT_MODE_ALL,
-} IteLiftQuantMode;
-
-typedef enum {
-  /** synthesize I( x ) */
-  SYGUS_INV_TEMPL_MODE_NONE,
-  /** synthesize ( pre( x ) V I( x ) ) */
-  SYGUS_INV_TEMPL_MODE_PRE,
-  /** synthesize ( post( x ) ^ I( x ) ) */
-  SYGUS_INV_TEMPL_MODE_POST,
-} SygusInvTemplMode;
-
-typedef enum {
-  /** infer all definitions */
-  MACROS_QUANT_MODE_ALL,
-  /** infer ground definitions */
-  MACROS_QUANT_MODE_GROUND,
-  /** infer ground uf definitions */
-  MACROS_QUANT_MODE_GROUND_UF,
-} MacrosQuantMode;
-
-}/* CVC4::theory::quantifiers namespace */
-}/* CVC4::theory namespace */
-
-std::ostream& operator<<(std::ostream& out, theory::quantifiers::InstWhenMode mode) CVC4_PUBLIC;
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4__THEORY__QUANTIFIERS__MODES_H */
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
deleted file mode 100644
index 065da0d5a..000000000
--- a/src/theory/quantifiers/options
+++ /dev/null
@@ -1,297 +0,0 @@
-#
-# Option specification file for CVC4
-# See src/options/base_options for a description of this file format
-#
-
-module QUANTIFIERS "theory/quantifiers/options.h" Quantifiers
-
-#### rewriter options
-
-# Whether to mini-scope quantifiers.
-# For example, forall x. ( P( x ) ^ Q( x ) ) will be rewritten to
-# ( forall x. P( x ) ) ^ ( forall x. Q( x ) )
-option miniscopeQuant --miniscope-quant bool :default true :read-write
- miniscope quantifiers
-# Whether to mini-scope quantifiers based on formulas with no free variables.
-# For example, forall x. ( P( x ) V Q ) will be rewritten to
-# ( forall x. P( x ) ) V Q
-option miniscopeQuantFreeVar --miniscope-quant-fv bool :default true :read-write
- miniscope quantifiers for ground subformulas
-option quantSplit --quant-split bool :default true
- apply splitting to quantified formulas based on variable disjoint disjuncts
-option prenexQuant --prenex-quant=MODE CVC4::theory::quantifiers::PrenexQuantMode :default CVC4::theory::quantifiers::PRENEX_NO_USER_PAT :include "theory/quantifiers/modes.h" :read-write :handler CVC4::theory::quantifiers::stringToPrenexQuantMode :handler-include "theory/quantifiers/options_handlers.h"
- prenex mode for quantified formulas
-# Whether to variable-eliminate quantifiers.
-# For example, forall x y. ( P( x, y ) V x != c ) will be rewritten to
-#   forall y. P( c, y )
-option varElimQuant --var-elim-quant bool :default true
- enable simple variable elimination for quantified formulas
-option dtVarExpandQuant --dt-var-exp-quant bool :default true
- expand datatype variables bound to one constructor in quantifiers
-#ite lift mode for quantified formulas
-option iteLiftQuant --ite-lift-quant=MODE CVC4::theory::quantifiers::IteLiftQuantMode :default CVC4::theory::quantifiers::ITE_LIFT_QUANT_MODE_SIMPLE :include "theory/quantifiers/modes.h" :read-write :handler CVC4::theory::quantifiers::stringToIteLiftQuantMode :handler-include "theory/quantifiers/options_handlers.h"
- ite lifting mode for quantified formulas
-option condVarSplitQuant --cond-var-split-quant bool :default true
- split quantified formulas that lead to variable eliminations
-option condVarSplitQuantAgg --cond-var-split-agg-quant bool :default false
- aggressive split quantified formulas that lead to variable eliminations
-option iteDtTesterSplitQuant --ite-dtt-split-quant bool :read-write :default false
- split ites with dt testers as conditions
-# Whether to CNF quantifier bodies
-# option cnfQuant --cnf-quant bool :default false
-#  apply CNF conversion to quantified formulas
-option nnfQuant --nnf-quant bool :default true
- apply NNF conversion to quantified formulas
-# Whether to pre-skolemize quantifier bodies.
-# For example, forall x. ( P( x ) => (exists y. f( y ) = x) ) will be rewritten to
-#   forall x. P( x ) => f( S( x ) ) = x
-option preSkolemQuant --pre-skolem-quant bool :read-write :default false
- apply skolemization eagerly to bodies of quantified formulas
-option preSkolemQuantNested --pre-skolem-quant-nested bool :read-write :default true
- apply skolemization to nested quantified formulass
-option preSkolemQuantAgg --pre-skolem-quant-agg bool :read-write :default true
- apply skolemization to quantified formulas aggressively
-option aggressiveMiniscopeQuant --ag-miniscope-quant bool :default false
- perform aggressive miniscoping for quantifiers
-option elimTautQuant --elim-taut-quant bool :default true
- eliminate tautological disjuncts of quantified formulas
-option purifyQuant --purify-quant bool :default false
- purify quantified formulas
- 
-#### E-matching options
- 
-option eMatching --e-matching bool :read-write :default true
- whether to do heuristic E-matching
-
-option termDbMode --term-db-mode CVC4::theory::quantifiers::TermDbMode :default CVC4::theory::quantifiers::TERM_DB_ALL :read-write :include "theory/quantifiers/modes.h" :handler  CVC4::theory::quantifiers::stringToTermDbMode :handler-include "theory/quantifiers/options_handlers.h"
- which ground terms to consider for instantiation
-option registerQuantBodyTerms --register-quant-body-terms bool :default false
- consider ground terms within bodies of quantified formulas for matching
- 
-option smartTriggers --smart-triggers bool :default true
- enable smart triggers
-option relevantTriggers --relevant-triggers bool :default false
- prefer triggers that are more relevant based on SInE style analysis
-option relationalTriggers --relational-triggers bool :default false
- choose relational triggers such as x = f(y), x >= f(y)
-option purifyTriggers --purify-triggers bool :default false :read-write
- purify triggers, e.g. f( x+1 ) becomes f( y ), x mapsto y-1
-option purifyDtTriggers --purify-dt-triggers bool :default false :read-write
- purify dt triggers, match all constructors of correct form instead of selectors
-option pureThTriggers --pure-th-triggers bool :default false :read-write
- use pure theory terms as single triggers
-option partialTriggers --partial-triggers bool :default false :read-write
- use triggers that do not contain all free variables
-option multiTriggerWhenSingle --multi-trigger-when-single bool :default false
- select multi triggers when single triggers exist
-option multiTriggerPriority --multi-trigger-priority bool :default false
- only try multi triggers if single triggers give no instantiations
-option triggerSelMode --trigger-sel CVC4::theory::quantifiers::TriggerSelMode :default CVC4::theory::quantifiers::TRIGGER_SEL_DEFAULT :read-write :include "theory/quantifiers/modes.h" :handler  CVC4::theory::quantifiers::stringToTriggerSelMode :handler-include "theory/quantifiers/options_handlers.h"
- selection mode for triggers
-option userPatternsQuant --user-pat=MODE CVC4::theory::quantifiers::UserPatMode :default CVC4::theory::quantifiers::USER_PAT_MODE_TRUST :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToUserPatMode :handler-include "theory/quantifiers/options_handlers.h"
- policy for handling user-provided patterns for quantifier instantiation
-option incrementTriggers --increment-triggers bool :default true
- generate additional triggers as needed during search
- 
-option instWhenMode --inst-when=MODE CVC4::theory::quantifiers::InstWhenMode :default CVC4::theory::quantifiers::INST_WHEN_FULL_LAST_CALL :read-write :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToInstWhenMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkInstWhenMode :predicate-include "theory/quantifiers/options_handlers.h"
- when to apply instantiation
- 
-option instMaxLevel --inst-max-level=N int :read-write :default -1
- maximum inst level of terms used to instantiate quantified formulas with (-1 == no limit, default)
-option instLevelInputOnly --inst-level-input-only bool :default true
- only input terms are assigned instantiation level zero
-option internalReps --quant-internal-reps bool :default true
- instantiate with representatives chosen by quantifiers engine
- 
-option eagerInstQuant --eager-inst-quant bool :default false
- apply quantifier instantiation eagerly
-
-option fullSaturateQuant --full-saturate-quant bool :default false :read-write
- when all other quantifier instantiation strategies fail, instantiate with ground terms from relevant domain, then arbitrary ground terms before answering unknown
-option fullSaturateQuantRd --full-saturate-quant-rd bool :default true
- whether to use relevant domain first for full saturation instantiation strategy
-option fullSaturateInst --fs-inst bool :default false
- interleave full saturate instantiation with other techniques
-
-option literalMatchMode --literal-matching=MODE CVC4::theory::quantifiers::LiteralMatchMode :default CVC4::theory::quantifiers::LITERAL_MATCH_NONE :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToLiteralMatchMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkLiteralMatchMode :predicate-include "theory/quantifiers/options_handlers.h"
- choose literal matching mode
-
-### finite model finding options
- 
-option finiteModelFind finite-model-find --finite-model-find bool :default false :read-write
- use finite model finding heuristic for quantifier instantiation
-
-option quantFunWellDefined --quant-fun-wd bool :default false
- assume that function defined by quantifiers are well defined
-option fmfFunWellDefined --fmf-fun bool :default false :read-write
- find models for recursively defined functions, assumes functions are admissible
-option fmfFunWellDefinedRelevant --fmf-fun-rlv bool :default false
- find models for recursively defined functions, assumes functions are admissible, allows empty type when function is irrelevant
-option fmfEmptySorts --fmf-empty-sorts bool :default false
- allow finite model finding to assume sorts that do not occur in ground assertions are empty
- 
-option mbqiMode --mbqi=MODE CVC4::theory::quantifiers::MbqiMode :read-write :default CVC4::theory::quantifiers::MBQI_FMC :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToMbqiMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkMbqiMode :predicate-include "theory/quantifiers/options_handlers.h"
- choose mode for model-based quantifier instantiation
-option fmfOneInstPerRound --mbqi-one-inst-per-round bool :read-write :default false
- only add one instantiation per quantifier per round for mbqi
-option fmfOneQuantPerRound --mbqi-one-quant-per-round bool :default false
- only add instantiations for one quantifier per round for mbqi
-
-option fmfInstEngine --fmf-inst-engine bool :default false
- use instantiation engine in conjunction with finite model finding
-option fmfInstGen --fmf-inst-gen bool :default true
- enable Inst-Gen instantiation techniques for finite model finding 
-option fmfInstGenOneQuantPerRound --fmf-inst-gen-one-quant-per-round bool :default false
- only perform Inst-Gen instantiation techniques on one quantifier per round
-option fmfFreshDistConst --fmf-fresh-dc bool :default false
- use fresh distinguished representative when applying Inst-Gen techniques
-option fmfFmcSimple --fmf-fmc-simple bool :default true
- simple models in full model check for finite model finding
-option fmfBoundInt fmf-bound-int --fmf-bound-int bool :default false :read-write
- finite model finding on bounded integer quantification
-option fmfBoundIntLazy --fmf-bound-int-lazy bool :default false :read-write
- enforce bounds for bounded integer quantification lazily via use of proxy variables
- 
-### conflict-based instantiation options 
- 
-option quantConflictFind --quant-cf bool :read-write :default true
- enable conflict find mechanism for quantifiers
-option qcfMode --quant-cf-mode=MODE CVC4::theory::quantifiers::QcfMode :default CVC4::theory::quantifiers::QCF_PROP_EQ :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToQcfMode :handler-include "theory/quantifiers/options_handlers.h"
- what effort to apply conflict find mechanism
-option qcfWhenMode --quant-cf-when=MODE CVC4::theory::quantifiers::QcfWhenMode :default CVC4::theory::quantifiers::QCF_WHEN_MODE_DEFAULT :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToQcfWhenMode :handler-include "theory/quantifiers/options_handlers.h"
- when to invoke conflict find mechanism for quantifiers
-option qcfTConstraint --qcf-tconstraint bool :read-write :default false
- enable entailment checks for t-constraints in qcf algorithm
-option qcfAllConflict --qcf-all-conflict bool :read-write :default false
- add all available conflicting instances during conflict-based instantiation
-
-option instNoEntail --inst-no-entail bool :read-write :default true
- do not consider instances of quantified formulas that are currently entailed
- 
-### rewrite rules options 
- 
-option quantRewriteRules --rewrite-rules bool :default false
- use rewrite rules module
-option rrOneInstPerRound --rr-one-inst-per-round bool :default false
- add one instance of rewrite rule per round
- 
-### induction options 
- 
-option quantInduction --quant-ind bool :default false
- use all available techniques for inductive reasoning
-option dtStcInduction --dt-stc-ind bool :read-write :default false
- apply strengthening for existential quantification over datatypes based on structural induction
-option intWfInduction --int-wf-ind bool :read-write :default false
- apply strengthening for integers based on well-founded induction
-option conjectureGen --conjecture-gen bool :read-write :default false
- generate candidate conjectures for inductive proofs
- 
-option conjectureGenPerRound --conjecture-gen-per-round=N int :default 1
- number of conjectures to generate per instantiation round 
-option conjectureNoFilter --conjecture-no-filter bool :default false
- do not filter conjectures
-option conjectureFilterActiveTerms --conjecture-filter-active-terms bool :read-write :default true
- filter based on active terms
-option conjectureFilterCanonical --conjecture-filter-canonical bool :read-write :default true
- filter based on canonicity
-option conjectureFilterModel --conjecture-filter-model bool :read-write :default true
- filter based on model
-option conjectureGenGtEnum --conjecture-gen-gt-enum=N int :default 50
- number of ground terms to generate for model filtering
-option conjectureUeeIntro --conjecture-gen-uee-intro bool :default false
- more aggressive merging for universal equality engine, introduces terms
-  
-### synthesis options 
-
-option ceGuidedInst --cegqi bool :default false :read-write
-  counterexample-guided quantifier instantiation
-option ceGuidedInstFair --cegqi-fair=MODE CVC4::theory::quantifiers::CegqiFairMode :default CVC4::theory::quantifiers::CEGQI_FAIR_DT_SIZE :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToCegqiFairMode :handler-include "theory/quantifiers/options_handlers.h"
-  if and how to apply fairness for cegqi
-option cegqiSingleInv --cegqi-si bool :default false :read-write
-  process single invocation synthesis conjectures
-option cegqiSingleInvPartial --cegqi-si-partial bool :default false
-  combined techniques for synthesis conjectures that are partially single invocation 
-option cegqiSingleInvReconstruct --cegqi-si-reconstruct bool :default true
-  reconstruct solutions for single invocation conjectures in original grammar
-option cegqiSingleInvReconstructConst --cegqi-si-reconstruct-const bool :default true
-  include constants when reconstruct solutions for single invocation conjectures in original grammar
-option cegqiSingleInvAbort --cegqi-si-abort bool :default false
-  abort if synthesis conjecture is not single invocation
-option cegqiSingleInvMultiInstAbort --cegqi-si-multi-inst-abort bool :default false
-  abort if synthesis conjecture is single invocation with no ITE in grammar and multiple instantiations are tried
-  
-option sygusNormalForm --sygus-nf bool :default true
-  only search for sygus builtin terms that are in normal form
-option sygusNormalFormArg --sygus-nf-arg bool :default true
-  account for relationship between arguments of operations in sygus normal form
-option sygusNormalFormGlobal --sygus-nf-sym bool :default true
-  narrow sygus search space based on global state of current candidate program
-option sygusNormalFormGlobalGen --sygus-nf-sym-gen bool :default true
-  generalize lemmas for global search space narrowing
-option sygusNormalFormGlobalArg --sygus-nf-sym-arg bool :default true
-  generalize based on arguments in global search space narrowing
-option sygusNormalFormGlobalContent --sygus-nf-sym-content bool :default true
-  generalize based on content in global search space narrowing
-  
-option sygusInvTemplMode --sygus-inv-templ=MODE CVC4::theory::quantifiers::SygusInvTemplMode :default CVC4::theory::quantifiers::SYGUS_INV_TEMPL_MODE_NONE :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToSygusInvTemplMode :handler-include "theory/quantifiers/options_handlers.h"
-  template mode for sygus invariant synthesis
-
-# approach applied to general quantified formulas
-option cbqiSplx --cbqi-splx bool :read-write :default false
- turns on old implementation of counterexample-based quantifier instantiation
-option cbqi --cbqi bool :read-write :default false
- turns on counterexample-based quantifier instantiation
-option recurseCbqi --cbqi-recurse bool :default true
- turns on recursive counterexample-based quantifier instantiation
-option cbqiSat --cbqi-sat bool :read-write :default true
- answer sat when quantifiers are asserted with counterexample-based quantifier instantiation
-option cbqiModel --cbqi-model bool :read-write :default true
- guide instantiations by model values for counterexample-based quantifier instantiation
-option cbqiAll --cbqi-all bool :read-write :default false
- apply counterexample-based instantiation to all quantified formulas
-option cbqiUseInfInt --cbqi-use-inf-int bool :read-write :default false
- use integer infinity for vts in counterexample-based quantifier instantiation
-option cbqiUseInfReal --cbqi-use-inf-real bool :read-write :default false
- use real infinity for vts in counterexample-based quantifier instantiation
-option cbqiPreRegInst --cbqi-prereg-inst bool :read-write :default false
-  preregister ground instantiations in counterexample-based quantifier instantiation
-option cbqiMinBounds --cbqi-min-bounds bool :default false
-  use minimally constrained lower/upper bound for counterexample-based quantifier instantiation
-option cbqiSymLia --cbqi-sym-lia bool :default false
-  use symbolic integer division in substitutions for counterexample-based quantifier instantiation
-option cbqiRoundUpLowerLia --cbqi-round-up-lia bool :default false
-  round up integer lower bounds in substitutions for counterexample-based quantifier instantiation
-option cbqiMidpoint --cbqi-midpoint bool :default false
-  choose substitutions based on midpoints of lower and upper bounds for counterexample-based quantifier instantiation
-option cbqiNopt --cbqi-nopt bool :default true
-  non-optimal bounds for counterexample-based quantifier instantiation
- 
-### local theory extensions options 
-
-option localTheoryExt --local-t-ext bool :default false
-  do instantiation based on local theory extensions
-option ltePartialInst --lte-partial-inst bool :default false
-  partially instantiate local theory quantifiers
-option lteRestrictInstClosure --lte-restrict-inst-closure bool :default false
-  treat arguments of inst closure as restricted terms for instantiation
- 
-### reduction options
-
-option quantAlphaEquiv --quant-alpha-equiv bool :default true
-  infer alpha equivalence between quantified formulas
-option macrosQuant --macros-quant bool :read-write :default false
- perform quantifiers macro expansion
-option macrosQuantMode --macros-quant-mode=MODE CVC4::theory::quantifiers::MacrosQuantMode :default CVC4::theory::quantifiers::MACROS_QUANT_MODE_GROUND_UF :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToMacrosQuantMode :handler-include "theory/quantifiers/options_handlers.h"
- mode for quantifiers macro expansion
-
-### recursive function options
-
-#option funDefs --fun-defs bool :default false
-#  enable specialized techniques for recursive function definitions
- 
-### e-unification options
-
-option quantEqualityEngine --quant-ee bool :default false
-  maintain congrunce closure over universal equalities
- 
-endmodule
diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h
deleted file mode 100644
index 02a1a6cf2..000000000
--- a/src/theory/quantifiers/options_handlers.h
+++ /dev/null
@@ -1,480 +0,0 @@
-/*********************                                                        */
-/*! \file options_handlers.h
- ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: Andrew Reynolds
- ** 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_private.h"
-
-#ifndef __CVC4__THEORY__QUANTIFIERS__OPTIONS_HANDLERS_H
-#define __CVC4__THEORY__QUANTIFIERS__OPTIONS_HANDLERS_H
-
-#include <string>
-
-namespace CVC4 {
-namespace theory {
-namespace quantifiers {
-
-static const std::string instWhenHelp = "\
-Modes currently supported by the --inst-when option:\n\
-\n\
-full-last-call (default)\n\
-+ Alternate running instantiation rounds at full effort and last\n\
-  call.  In other words, interleave instantiation and theory combination.\n\
-\n\
-full\n\
-+ Run instantiation round at full effort, before theory combination.\n\
-\n\
-full-delay \n\
-+ Run instantiation round at full effort, before theory combination, after\n\
-  all other theories have finished.\n\
-\n\
-full-delay-last-call \n\
-+ Alternate running instantiation rounds at full effort after all other\n\
-  theories have finished, and last call.  \n\
-\n\
-last-call\n\
-+ Run instantiation at last call effort, after theory combination and\n\
-  and theories report sat.\n\
-\n\
-";
-
-static const std::string literalMatchHelp = "\
-Literal match modes currently supported by the --literal-match option:\n\
-\n\
-none (default)\n\
-+ Do not use literal matching.\n\
-\n\
-predicate\n\
-+ Consider the phase requirements of predicate literals when applying heuristic\n\
-  quantifier instantiation.  For example, the trigger P( x ) in the quantified \n\
-  formula forall( x ). ( P( x ) V ~Q( x ) ) will only be matched with ground\n\
-  terms P( t ) where P( t ) is in the equivalence class of false, and likewise\n\
-  Q( x ) with Q( s ) where Q( s ) is in the equivalence class of true.\n\
-\n\
-";
-static const std::string mbqiModeHelp = "\
-Model-based quantifier instantiation modes currently supported by the --mbqi option:\n\
-\n\
-default \n\
-+ Use algorithm from Section 5.4.2 of thesis Finite Model Finding in Satisfiability \n\
-  Modulo Theories.\n\
-\n\
-none \n\
-+ Disable model-based quantifier instantiation.\n\
-\n\
-gen-ev \n\
-+ Use model-based quantifier instantiation algorithm from CADE 24 finite\n\
-  model finding paper based on generalizing evaluations.\n\
-\n\
-fmc-interval \n\
-+ Same as default, but with intervals for models of integer functions.\n\
-\n\
-abs \n\
-+ Use abstract MBQI algorithm (uses disjoint sets). \n\
-\n\
-";
-static const std::string qcfWhenModeHelp = "\
-Quantifier conflict find modes currently supported by the --quant-cf-when option:\n\
-\n\
-default \n\
-+ Default, apply conflict finding at full effort.\n\
-\n\
-last-call \n\
-+ Apply conflict finding at last call, after theory combination and \n\
-  and all theories report sat. \n\
-\n\
-std \n\
-+ Apply conflict finding at standard effort.\n\
-\n\
-std-h \n\
-+ Apply conflict finding at standard effort when heuristic says to. \n\
-\n\
-";
-static const std::string qcfModeHelp = "\
-Quantifier conflict find modes currently supported by the --quant-cf option:\n\
-\n\
-prop-eq \n\
-+ Default, apply QCF algorithm to propagate equalities as well as conflicts. \n\
-\n\
-conflict \n\
-+ Apply QCF algorithm to find conflicts only.\n\
-\n\
-partial \n\
-+ Apply QCF algorithm to instantiate heuristically as well. \n\
-\n\
-mc \n\
-+ Apply QCF algorithm in a complete way, so that a model is ensured when it fails. \n\
-\n\
-";
-static const std::string userPatModeHelp = "\
-User pattern modes currently supported by the --user-pat option:\n\
-\n\
-trust \n\
-+ When provided, use only user-provided patterns for a quantified formula.\n\
-\n\
-use \n\
-+ Use both user-provided and auto-generated patterns when patterns\n\
-  are provided for a quantified formula.\n\
-\n\
-resort \n\
-+ Use user-provided patterns only after auto-generated patterns saturate.\n\
-\n\
-ignore \n\
-+ Ignore user-provided patterns. \n\
-\n\
-interleave \n\
-+ Alternate between use/resort. \n\
-\n\
-";
-static const std::string triggerSelModeHelp = "\
-Trigger selection modes currently supported by the --trigger-sel option:\n\
-\n\
-default \n\
-+ Default, consider all subterms of quantified formulas for trigger selection.\n\
-\n\
-min \n\
-+ Consider only minimal subterms that meet criteria for triggers.\n\
-\n\
-max \n\
-+ Consider only maximal subterms that meet criteria for triggers. \n\
-\n\
-";
-static const std::string prenexQuantModeHelp = "\
-Prenex quantifiers modes currently supported by the --prenex-quant option:\n\
-\n\
-default \n\
-+ Default, prenex all nested quantifiers except those with user patterns.\n\
-\n\
-all \n\
-+ Prenex all nested quantifiers.\n\
-\n\
-none \n\
-+ Do no prenex nested quantifiers. \n\
-\n\
-";
-static const std::string cegqiFairModeHelp = "\
-Modes for enforcing fairness for counterexample guided quantifier instantion, supported by --cegqi-fair:\n\
-\n\
-uf-dt-size \n\
-+ Enforce fairness using an uninterpreted function for datatypes size.\n\
-\n\
-default | dt-size \n\
-+ Default, enforce fairness using size theory operator.\n\
-\n\
-dt-height-bound \n\
-+ Enforce fairness by height bound predicate.\n\
-\n\
-none \n\
-+ Do not enforce fairness. \n\
-\n\
-";
-static const std::string termDbModeHelp = "\
-Modes for term database, supported by --term-db-mode:\n\
-\n\
-all  \n\
-+ Quantifiers module considers all ground terms.\n\
-\n\
-relevant \n\
-+ Quantifiers module considers only ground terms connected to current assertions. \n\
-\n\
-";
-static const std::string iteLiftQuantHelp = "\
-Modes for term database, supported by --ite-lift-quant:\n\
-\n\
-none  \n\
-+ Do not lift if-then-else in quantified formulas.\n\
-\n\
-simple  \n\
-+ Lift if-then-else in quantified formulas if results in smaller term size.\n\
-\n\
-all \n\
-+ Lift if-then-else in quantified formulas. \n\
-\n\
-";
-static const std::string sygusInvTemplHelp = "\
-Template modes for sygus invariant synthesis, supported by --sygus-inv-templ:\n\
-\n\
-none  \n\
-+ Synthesize invariant directly.\n\
-\n\
-pre  \n\
-+ Synthesize invariant based on weakening of precondition .\n\
-\n\
-post \n\
-+ Synthesize invariant based on strengthening of postcondition. \n\
-\n\
-";
-static const std::string macrosQuantHelp = "\
-Template modes for quantifiers macro expansion, supported by --macros-quant-mode:\n\
-\n\
-all \n\
-+ Infer definitions for functions, including those containing quantified formulas.\n\
-\n\
-ground (default) \n\
-+ Only infer ground definitions for functions.\n\
-\n\
-ground-uf \n\
-+ Only infer ground definitions for functions that result in triggers for all free variables.\n\
-\n\
-";
-
-inline InstWhenMode stringToInstWhenMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
-  if(optarg == "pre-full") {
-    return INST_WHEN_PRE_FULL;
-  } else if(optarg == "full") {
-    return INST_WHEN_FULL;
-  } else if(optarg == "full-delay") {
-    return INST_WHEN_FULL_DELAY;
-  } else if(optarg == "full-last-call") {
-    return INST_WHEN_FULL_LAST_CALL;
-  } else if(optarg == "full-delay-last-call") {
-    return INST_WHEN_FULL_DELAY_LAST_CALL;
-  } else if(optarg == "last-call") {
-    return INST_WHEN_LAST_CALL;
-  } else if(optarg == "help") {
-    puts(instWhenHelp.c_str());
-    exit(1);
-  } else {
-    throw OptionException(std::string("unknown option for --inst-when: `") +
-                          optarg + "'.  Try --inst-when help.");
-  }
-}
-
-inline void checkInstWhenMode(std::string option, InstWhenMode mode, SmtEngine* smt) throw(OptionException) {
-  if(mode == INST_WHEN_PRE_FULL) {
-    throw OptionException(std::string("Mode pre-full for ") + option + " is not supported in this release.");
-  }
-}
-
-inline LiteralMatchMode stringToLiteralMatchMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
-  if(optarg ==  "none") {
-    return LITERAL_MATCH_NONE;
-  } else if(optarg ==  "predicate") {
-    return LITERAL_MATCH_PREDICATE;
-  } else if(optarg ==  "equality") {
-    return LITERAL_MATCH_EQUALITY;
-  } else if(optarg ==  "help") {
-    puts(literalMatchHelp.c_str());
-    exit(1);
-  } else {
-    throw OptionException(std::string("unknown option for --literal-matching: `") +
-                          optarg + "'.  Try --literal-matching help.");
-  }
-}
-
-inline void checkLiteralMatchMode(std::string option, LiteralMatchMode mode, SmtEngine* smt) throw(OptionException) {
-  if(mode == LITERAL_MATCH_EQUALITY) {
-    throw OptionException(std::string("Mode equality for ") + option + " is not supported in this release.");
-  }
-}
-
-inline MbqiMode stringToMbqiMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
-  if(optarg == "gen-ev") {
-    return MBQI_GEN_EVAL;
-  } else if(optarg == "none") {
-    return MBQI_NONE;
-  } else if(optarg == "default" || optarg ==  "fmc") {
-    return MBQI_FMC;
-  } else if(optarg == "fmc-interval") {
-    return MBQI_FMC_INTERVAL;
-  } else if(optarg == "abs") {
-    return MBQI_ABS;
-  } else if(optarg == "trust") {
-    return MBQI_TRUST;
-  } else if(optarg == "help") {
-    puts(mbqiModeHelp.c_str());
-    exit(1);
-  } else {
-    throw OptionException(std::string("unknown option for --mbqi: `") +
-                          optarg + "'.  Try --mbqi help.");
-  }
-}
-
-inline void checkMbqiMode(std::string option, MbqiMode mode, SmtEngine* smt) throw(OptionException) {
-
-}
-
-inline QcfWhenMode stringToQcfWhenMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
-  if(optarg ==  "default") {
-    return QCF_WHEN_MODE_DEFAULT;
-  } else if(optarg ==  "last-call") {
-    return QCF_WHEN_MODE_LAST_CALL;
-  } else if(optarg ==  "std") {
-    return QCF_WHEN_MODE_STD;
-  } else if(optarg ==  "std-h") {
-    return QCF_WHEN_MODE_STD_H;
-  } else if(optarg ==  "help") {
-    puts(qcfWhenModeHelp.c_str());
-    exit(1);
-  } else {
-    throw OptionException(std::string("unknown option for --quant-cf-when: `") +
-                          optarg + "'.  Try --quant-cf-when help.");
-  }
-}
-inline QcfMode stringToQcfMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
-  if(optarg ==  "conflict") {
-    return QCF_CONFLICT_ONLY;
-  } else if(optarg ==  "default" || optarg == "prop-eq") {
-    return QCF_PROP_EQ;
-  } else if(optarg == "partial") {
-    return QCF_PARTIAL;
-  } else if(optarg == "mc" ) {
-    return QCF_MC;
-  } else if(optarg ==  "help") {
-    puts(qcfModeHelp.c_str());
-    exit(1);
-  } else {
-    throw OptionException(std::string("unknown option for --quant-cf-mode: `") +
-                          optarg + "'.  Try --quant-cf-mode help.");
-  }
-}
-
-inline UserPatMode stringToUserPatMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
-  if(optarg == "use") {
-    return USER_PAT_MODE_USE;
-  } else if(optarg ==  "default" || optarg == "trust") {
-    return USER_PAT_MODE_TRUST;
-  } else if(optarg == "resort") {
-    return USER_PAT_MODE_RESORT;
-  } else if(optarg == "ignore") {
-    return USER_PAT_MODE_IGNORE;
-  } else if(optarg == "interleave") {
-    return USER_PAT_MODE_INTERLEAVE;
-  } else if(optarg ==  "help") {
-    puts(userPatModeHelp.c_str());
-    exit(1);
-  } else {
-    throw OptionException(std::string("unknown option for --user-pat: `") +
-                          optarg + "'.  Try --user-pat help.");
-  }
-}
-
-inline TriggerSelMode stringToTriggerSelMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
-  if(optarg ==  "default" || optarg == "all" ) {
-    return TRIGGER_SEL_DEFAULT;
-  } else if(optarg == "min") {
-    return TRIGGER_SEL_MIN;
-  } else if(optarg == "max") {
-    return TRIGGER_SEL_MAX;
-  } else if(optarg ==  "help") {
-    puts(triggerSelModeHelp.c_str());
-    exit(1);
-  } else {
-    throw OptionException(std::string("unknown option for --trigger-sel: `") +
-                          optarg + "'.  Try --trigger-sel help.");
-  }
-}
-
-inline PrenexQuantMode stringToPrenexQuantMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
-  if(optarg ==  "default" ) {
-    return PRENEX_NO_USER_PAT;
-  } else if(optarg == "all") {
-    return PRENEX_ALL;
-  } else if(optarg == "none") {
-    return PRENEX_NONE;
-  } else if(optarg ==  "help") {
-    puts(prenexQuantModeHelp.c_str());
-    exit(1);
-  } else {
-    throw OptionException(std::string("unknown option for --prenex-quant: `") +
-                          optarg + "'.  Try --prenex-quant help.");
-  }
-}
-
-inline CegqiFairMode stringToCegqiFairMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
-  if(optarg == "uf-dt-size" ) {
-    return CEGQI_FAIR_UF_DT_SIZE;
-  } else if(optarg == "default" || optarg == "dt-size") {
-    return CEGQI_FAIR_DT_SIZE;
-  } else if(optarg == "dt-height-bound" ){
-    return CEGQI_FAIR_DT_HEIGHT_PRED;
-  } else if(optarg == "none") {
-    return CEGQI_FAIR_NONE;
-  } else if(optarg ==  "help") {
-    puts(cegqiFairModeHelp.c_str());
-    exit(1);
-  } else {
-    throw OptionException(std::string("unknown option for --cegqi-fair: `") +
-                          optarg + "'.  Try --cegqi-fair help.");
-  }
-}
-
-inline TermDbMode stringToTermDbMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
-  if(optarg == "all" ) {
-    return TERM_DB_ALL;
-  } else if(optarg == "relevant") {
-    return TERM_DB_RELEVANT;
-  } else if(optarg ==  "help") {
-    puts(termDbModeHelp.c_str());
-    exit(1);
-  } else {
-    throw OptionException(std::string("unknown option for --term-db-mode: `") +
-                          optarg + "'.  Try --term-db-mode help.");
-  }
-}
-
-inline IteLiftQuantMode stringToIteLiftQuantMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
-  if(optarg == "all" ) {
-    return ITE_LIFT_QUANT_MODE_ALL;
-  } else if(optarg == "simple") {
-    return ITE_LIFT_QUANT_MODE_SIMPLE;
-  } else if(optarg == "none") {
-    return ITE_LIFT_QUANT_MODE_NONE;
-  } else if(optarg ==  "help") {
-    puts(iteLiftQuantHelp.c_str());
-    exit(1);
-  } else {
-    throw OptionException(std::string("unknown option for --ite-lift-quant: `") +
-                          optarg + "'.  Try --ite-lift-quant help.");
-  }
-}
-
-inline SygusInvTemplMode stringToSygusInvTemplMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
-  if(optarg == "none" ) {
-    return SYGUS_INV_TEMPL_MODE_NONE;
-  } else if(optarg == "pre") {
-    return SYGUS_INV_TEMPL_MODE_PRE;
-  } else if(optarg == "post") {
-    return SYGUS_INV_TEMPL_MODE_POST;
-  } else if(optarg ==  "help") {
-    puts(sygusInvTemplHelp.c_str());
-    exit(1);
-  } else {
-    throw OptionException(std::string("unknown option for --sygus-inv-templ: `") +
-                          optarg + "'.  Try --sygus-inv-templ help.");
-  }
-}
-
-inline MacrosQuantMode stringToMacrosQuantMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
-  if(optarg == "all" ) {
-    return MACROS_QUANT_MODE_ALL;
-  } else if(optarg == "ground") {
-    return MACROS_QUANT_MODE_GROUND;
-  } else if(optarg == "ground-uf") {
-    return MACROS_QUANT_MODE_GROUND_UF;
-  } else if(optarg ==  "help") {
-    puts(macrosQuantHelp.c_str());
-    exit(1);
-  } else {
-    throw OptionException(std::string("unknown option for --macros-quant-mode: `") +
-                          optarg + "'.  Try --macros-quant-mode help.");
-  }
-}
-
-}/* CVC4::theory::quantifiers namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__THEORY__QUANTIFIERS__OPTIONS_HANDLERS_H */
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index ca5d23cd1..b6256980a 100644
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -13,14 +13,15 @@
  **
  **/
 
+#include "theory/quantifiers/quant_conflict_find.h"
+
 #include <vector>
 
-#include "theory/quantifiers/quant_conflict_find.h"
+#include "options/quantifiers_options.h"
 #include "theory/quantifiers/quant_util.h"
-#include "theory/theory_engine.h"
-#include "theory/quantifiers/options.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/trigger.h"
+#include "theory/theory_engine.h"
 
 using namespace CVC4;
 using namespace CVC4::kind;
diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp
index ef5b71f9d..8c6b30124 100644
--- a/src/theory/quantifiers/quantifiers_attributes.cpp
+++ b/src/theory/quantifiers/quantifiers_attributes.cpp
@@ -13,7 +13,8 @@
  **/
 
 #include "theory/quantifiers/quantifiers_attributes.h"
-#include "theory/quantifiers/options.h"
+
+#include "options/quantifiers_options.h"
 #include "theory/quantifiers/term_database.h"
 
 using namespace std;
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 1e2ac21a0..0afc8b1bb 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -13,9 +13,10 @@
  **/
 
 #include "theory/quantifiers/quantifiers_rewriter.h"
-#include "theory/quantifiers/options.h"
-#include "theory/quantifiers/term_database.h"
+
+#include "options/quantifiers_options.h"
 #include "theory/datatypes/datatypes_rewriter.h"
+#include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/trigger.h"
 
 using namespace std;
diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp
index a70d36ac0..4c8050239 100644
--- a/src/theory/quantifiers/rewrite_engine.cpp
+++ b/src/theory/quantifiers/rewrite_engine.cpp
@@ -15,13 +15,14 @@
  **/
 
 #include "theory/quantifiers/rewrite_engine.h"
-#include "theory/quantifiers/quant_util.h"
+
+#include "options/quantifiers_options.h"
 #include "theory/quantifiers/first_order_model.h"
-#include "theory/quantifiers/model_engine.h"
-#include "theory/quantifiers/options.h"
 #include "theory/quantifiers/inst_match_generator.h"
-#include "theory/theory_engine.h"
+#include "theory/quantifiers/model_engine.h"
+#include "theory/quantifiers/quant_util.h"
 #include "theory/quantifiers/term_database.h"
+#include "theory/theory_engine.h"
 
 using namespace CVC4;
 using namespace std;
diff --git a/src/theory/quantifiers/symmetry_breaking.cpp b/src/theory/quantifiers/symmetry_breaking.cpp
index 12b16ef06..4c8e24d08 100644
--- a/src/theory/quantifiers/symmetry_breaking.cpp
+++ b/src/theory/quantifiers/symmetry_breaking.cpp
@@ -13,15 +13,16 @@
  **
  **/
 
+#include "theory/quantifiers/symmetry_breaking.h"
+
 #include <vector>
 
-#include "theory/quantifiers/symmetry_breaking.h"
-#include "theory/rewriter.h"
 #include "theory/quantifiers_engine.h"
+#include "theory/rewriter.h"
+#include "theory/sort_inference.h"
 #include "theory/theory_engine.h"
-#include "util/sort_inference.h"
-#include "theory/uf/theory_uf_strong_solver.h"
 #include "theory/uf/theory_uf.h"
+#include "theory/uf/theory_uf_strong_solver.h"
 
 using namespace CVC4;
 using namespace CVC4::kind;
diff --git a/src/theory/quantifiers/symmetry_breaking.h b/src/theory/quantifiers/symmetry_breaking.h
index c3ba92214..43e5ec765 100644
--- a/src/theory/quantifiers/symmetry_breaking.h
+++ b/src/theory/quantifiers/symmetry_breaking.h
@@ -17,20 +17,19 @@
 #ifndef __CVC4__QUANT_SYMMETRY_BREAKING_H
 #define __CVC4__QUANT_SYMMETRY_BREAKING_H
 
-#include "theory/theory.h"
-
 #include <iostream>
+#include <map>
 #include <string>
 #include <vector>
-#include <map>
-#include "expr/node.h"
-#include "expr/type_node.h"
 
-#include "util/sort_inference.h"
+#include "context/cdchunk_list.h"
+#include "context/cdhashmap.h"
 #include "context/context.h"
 #include "context/context_mm.h"
-#include "context/cdhashmap.h"
-#include "context/cdchunk_list.h"
+#include "expr/node.h"
+#include "expr/type_node.h"
+#include "theory/sort_inference.h"
+#include "theory/theory.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 724f16947..f3bbc65cc 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -13,22 +13,23 @@
  **/
 
 #include "theory/quantifiers/term_database.h"
-#include "theory/quantifiers_engine.h"
-#include "theory/quantifiers/trigger.h"
-#include "theory/theory_engine.h"
-#include "theory/quantifiers/first_order_model.h"
-#include "theory/quantifiers/options.h"
-#include "theory/quantifiers/theory_quantifiers.h"
-#include "util/datatype.h"
+
+#include "expr/datatype.h"
+#include "options/quantifiers_options.h"
 #include "theory/datatypes/datatypes_rewriter.h"
 #include "theory/quantifiers/ce_guided_instantiation.h"
-#include "theory/quantifiers/rewrite_engine.h"
+#include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/fun_def_engine.h"
+#include "theory/quantifiers/rewrite_engine.h"
+#include "theory/quantifiers/theory_quantifiers.h"
+#include "theory/quantifiers/trigger.h"
+#include "theory/quantifiers_engine.h"
+#include "theory/theory_engine.h"
 
 //for sygus
+#include "smt/smt_engine_scope.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "util/bitvector.h"
-#include "smt/smt_engine_scope.h"
 
 using namespace std;
 using namespace CVC4;
@@ -2807,4 +2808,3 @@ void TermDbSygus::printSygusTerm( std::ostream& out, Node n, std::vector< Node >
     out << n;
   }
 }
-
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index 48891732b..e9ff60137 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -14,17 +14,18 @@
  ** Implementation of the theory of quantifiers.
  **/
 
-
 #include "theory/quantifiers/theory_quantifiers.h"
-#include "theory/valuation.h"
-#include "theory/quantifiers_engine.h"
+
+
+#include "base/cvc4_assert.h"
+#include "expr/kind.h"
+#include "options/quantifiers_options.h"
 #include "theory/quantifiers/instantiation_engine.h"
 #include "theory/quantifiers/model_engine.h"
-#include "expr/kind.h"
-#include "util/cvc4_assert.h"
-#include "theory/quantifiers/options.h"
-#include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
+#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers_engine.h"
+#include "theory/valuation.h"
 
 using namespace std;
 using namespace CVC4;
diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h
index 0f16f0e80..98f486145 100644
--- a/src/theory/quantifiers/theory_quantifiers.h
+++ b/src/theory/quantifiers/theory_quantifiers.h
@@ -19,15 +19,15 @@
 #ifndef __CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H
 #define __CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H
 
-#include "context/cdhashmap.h"
-#include "theory/theory.h"
-#include "util/hash.h"
-#include "util/statistics_registry.h"
-
 #include <ext/hash_set>
 #include <iostream>
 #include <map>
 
+#include "context/cdhashmap.h"
+#include "expr/statistics_registry.h"
+#include "theory/theory.h"
+#include "util/hash.h"
+
 namespace CVC4 {
 class TheoryEngine;
 
diff --git a/src/theory/quantifiers/theory_quantifiers_type_rules.h b/src/theory/quantifiers/theory_quantifiers_type_rules.h
index 3ce0250fe..1fb8ddaf9 100644
--- a/src/theory/quantifiers/theory_quantifiers_type_rules.h
+++ b/src/theory/quantifiers/theory_quantifiers_type_rules.h
@@ -19,7 +19,7 @@
 #ifndef __CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_TYPE_RULES_H
 #define __CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_TYPE_RULES_H
 
-#include "util/matcher.h"
+#include "expr/matcher.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index fdfa77b02..9aee18317 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -13,13 +13,14 @@
  **/
 
 #include "theory/quantifiers/trigger.h"
-#include "theory/theory_engine.h"
-#include "theory/quantifiers_engine.h"
+
+#include "options/quantifiers_options.h"
 #include "theory/quantifiers/candidate_generator.h"
-#include "theory/uf/equality_engine.h"
-#include "theory/quantifiers/options.h"
-#include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/inst_match_generator.h"
+#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers_engine.h"
+#include "theory/theory_engine.h"
+#include "theory/uf/equality_engine.h"
 
 using namespace std;
 using namespace CVC4;