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.

16 files changed, 122 insertions, 298 deletions

diff --git a/src/main/Makefile.am b/src/main/Makefile.am
index 3ac0db7cb..478d3f3ee 100644
--- a/src/main/Makefile.am
+++ b/src/main/Makefile.am
@@ -30,7 +30,6 @@ pcvc4_LDADD = \
 	libmain.a \
 	@builddir@/../parser/libcvc4parser.la \
 	@builddir@/../libcvc4.la \
-	@builddir@/../util/libstatistics.la \
 	$(READLINE_LIBS)
 if CVC4_NEEDS_REPLACEMENT_FUNCTIONS
 pcvc4_LDADD += \
@@ -55,7 +54,6 @@ cvc4_LDADD = \
 	libmain.a \
 	@builddir@/../parser/libcvc4parser.la \
 	@builddir@/../libcvc4.la \
-	@builddir@/../util/libstatistics.la \
 	$(READLINE_LIBS)
 if CVC4_NEEDS_REPLACEMENT_FUNCTIONS
 cvc4_LDADD += \
@@ -80,8 +78,6 @@ smt2_tokens.h: @srcdir@/../parser/smt2/Smt2.g
 tptp_tokens.h: @srcdir@/../parser/tptp/Tptp.g
 	$(AM_V_GEN)grep "'[a-zA-Z][a-zA-Z0-9_-][a-zA-Z0-9_-]*'" $^ | sed 's/.*'\''\([a-zA-Z0-9_-]*\)'\''.*/"\1",/' | sort -u >$@
 
-EXTRA_DIST = \
-	options_handlers.h
 
 clean-local:
 	rm -f $(BUILT_SOURCES)
diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index 460274515..0b53c3cbe 100644
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -12,22 +12,22 @@
  ** \brief An additional layer between commands and invoking them.
  **/
 
-#include <iostream>
-#include <string>
-
 #include "main/command_executor.h"
-#include "expr/command.h"
-
-#include "main/main.h"
-
-#include "main/options.h"
-#include "smt/options.h"
-#include "printer/options.h"
 
 #ifndef __WIN32__
 #  include <sys/resource.h>
 #endif /* ! __WIN32__ */
 
+#include <iostream>
+#include <string>
+
+#include "main/main.h"
+#include "options/main_options.h"
+#include "options/printer_options.h"
+#include "options/smt_options.h"
+#include "smt_util/command.h"
+
+
 namespace CVC4 {
 namespace main {
 
diff --git a/src/main/command_executor.h b/src/main/command_executor.h
index 9fe6347be..49d18a153 100644
--- a/src/main/command_executor.h
+++ b/src/main/command_executor.h
@@ -15,14 +15,14 @@
 #ifndef __CVC4__MAIN__COMMAND_EXECUTOR_H
 #define __CVC4__MAIN__COMMAND_EXECUTOR_H
 
+#include <iostream>
+#include <string>
+
 #include "expr/expr_manager.h"
-#include "smt/smt_engine.h"
-#include "util/statistics_registry.h"
+#include "expr/statistics_registry.h"
 #include "options/options.h"
-#include "expr/command.h"
-
-#include <string>
-#include <iostream>
+#include "smt/smt_engine.h"
+#include "smt_util/command.h"
 
 namespace CVC4 {
 namespace main {
diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp
index f0d87cdf2..bb6487bf0 100644
--- a/src/main/command_executor_portfolio.cpp
+++ b/src/main/command_executor_portfolio.cpp
@@ -15,27 +15,28 @@
  ** threads.
  **/
 
-#include <boost/thread.hpp>
-#include <boost/thread/condition.hpp>
+#include "main/command_executor_portfolio.h"
+
+#if HAVE_UNISTD_H
+#  include <unistd.h>
+#endif /* HAVE_UNISTD_H */
+
 #include <boost/exception_ptr.hpp>
 #include <boost/lexical_cast.hpp>
+#include <boost/thread.hpp>
+#include <boost/thread/condition.hpp>
 #include <string>
 
-#include "expr/command.h"
+#include "cvc4autoconfig.h"
 #include "expr/pickler.h"
-#include "main/command_executor_portfolio.h"
 #include "main/main.h"
-#include "main/options.h"
 #include "main/portfolio.h"
+#include "options/main_options.h"
 #include "options/options.h"
-#include "smt/options.h"
-#include "printer/options.h"
-
-#include "cvc4autoconfig.h"
+#include "options/printer_options.h"
+#include "options/smt_options.h"
+#include "smt_util/command.h"
 
-#if HAVE_UNISTD_H
-#  include <unistd.h>
-#endif /* HAVE_UNISTD_H */
 
 using namespace std;
 
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index c29ba55a4..df78df0f3 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -13,39 +13,38 @@
  ** sequential and portfolio versions
  **/
 
+#include <stdio.h>
+#include <unistd.h>
+
 #include <cstdlib>
 #include <cstring>
 #include <fstream>
 #include <iostream>
 #include <new>
-#include <unistd.h>
-
-#include <stdio.h>
-#include <unistd.h>
 
+#include "base/output.h"
 #include "cvc4autoconfig.h"
-#include "main/main.h"
-#include "main/interactive_shell.h"
-#include "main/options.h"
-#include "parser/parser.h"
-#include "parser/parser_builder.h"
-#include "parser/parser_exception.h"
 #include "expr/expr_manager.h"
-#include "expr/command.h"
-#include "util/configuration.h"
-#include "options/options.h"
-#include "theory/quantifiers/options.h"
+#include "expr/result.h"
+#include "expr/statistics_registry.h"
 #include "main/command_executor.h"
 
 #ifdef PORTFOLIO_BUILD
 #  include "main/command_executor_portfolio.h"
 #endif
 
-#include "main/options.h"
-#include "smt/options.h"
-#include "util/output.h"
-#include "util/result.h"
-#include "util/statistics_registry.h"
+#include "main/interactive_shell.h"
+#include "main/main.h"
+#include "options/main_options.h"
+#include "options/options.h"
+#include "options/quantifiers_options.h"
+#include "options/smt_options.h"
+#include "parser/parser.h"
+#include "parser/parser_builder.h"
+#include "parser/parser_exception.h"
+#include "smt/smt_options_handler.h"
+#include "smt_util/command.h"
+#include "util/configuration.h"
 
 using namespace std;
 using namespace CVC4;
@@ -130,8 +129,11 @@ int runCvc4(int argc, char* argv[], Options& opts) {
 
   progPath = argv[0];
 
+#warning "TODO: Check that the SmtEngine pointer should be NULL with Kshitij."
+  smt::SmtOptionsHandler optionsHandler(NULL);
+
   // Parse the options
-  vector<string> filenames = opts.parseOptions(argc, argv);
+  vector<string> filenames = opts.parseOptions(argc, argv, &optionsHandler);
 
 # ifndef PORTFOLIO_BUILD
   if( opts.wasSetByUser(options::threads) ||
@@ -302,7 +304,7 @@ int runCvc4(int argc, char* argv[], Options& opts) {
       }
 #ifndef PORTFOLIO_BUILD
       if(!opts.wasSetByUser(options::incrementalSolving)) {
-        cmd = new SetOptionCommand("incremental", true);
+        cmd = new SetOptionCommand("incremental", SExpr(true));
         cmd->setMuted(true);
         pExecutor->doCommand(cmd);
         delete cmd;
@@ -349,7 +351,7 @@ int runCvc4(int argc, char* argv[], Options& opts) {
           throw OptionException("--tear-down-incremental incompatible with --incremental");
         }
 
-        cmd = new SetOptionCommand("incremental", false);
+        cmd = new SetOptionCommand("incremental", SExpr(false));
         cmd->setMuted(true);
         pExecutor->doCommand(cmd);
         delete cmd;
@@ -488,7 +490,7 @@ int runCvc4(int argc, char* argv[], Options& opts) {
       delete parser;
     } else {
       if(!opts.wasSetByUser(options::incrementalSolving)) {
-        cmd = new SetOptionCommand("incremental", false);
+        cmd = new SetOptionCommand("incremental", SExpr(false));
         cmd->setMuted(true);
         pExecutor->doCommand(cmd);
         delete cmd;
diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index 3b237f6a4..da2813e24 100644
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -14,31 +14,17 @@
  ** This file is the implementation for the CVC4 interactive shell.
  ** The shell supports the readline library.
  **/
+#include "main/interactive_shell.h"
 
-#include <iostream>
+#include <algorithm>
+#include <cassert>
 #include <cstdlib>
-#include <vector>
-#include <string>
+#include <iostream>
 #include <set>
-#include <algorithm>
-#include <utility>
-
-#include "cvc4autoconfig.h"
-
-#include "main/interactive_shell.h"
-
-#include "expr/command.h"
-#include "parser/input.h"
-#include "parser/parser.h"
-#include "parser/parser_builder.h"
-#include "options/options.h"
-#include "smt/options.h"
-#include "main/options.h"
-#include "util/language.h"
-#include "util/output.h"
-
 #include <string.h>
-#include <cassert>
+#include <string>
+#include <utility>
+#include <vector>
 
 #if HAVE_LIBREADLINE
 #  include <readline/readline.h>
@@ -48,6 +34,19 @@
 #  endif /* HAVE_EXT_STDIO_FILEBUF_H */
 #endif /* HAVE_LIBREADLINE */
 
+
+#include "base/output.h"
+#include "cvc4autoconfig.h"
+#include "options/language.h"
+#include "options/main_options.h"
+#include "options/options.h"
+#include "options/smt_options.h"
+#include "parser/input.h"
+#include "parser/parser.h"
+#include "parser/parser_builder.h"
+#include "theory/logic_info.h"
+#include "smt_util/command.h"
+
 using namespace std;
 
 namespace CVC4 {
@@ -99,7 +98,7 @@ InteractiveShell::InteractiveShell(ExprManager& exprManager,
   /* Create parser with bogus input. */
   d_parser = parserBuilder.withStringInput("").build();
   if(d_options.wasSetByUser(options::forceLogic)) {
-    d_parser->forceLogic(d_options[options::forceLogic].getLogicString());
+    d_parser->forceLogic(d_options[options::forceLogic]->getLogicString());
   }
 
 #if HAVE_LIBREADLINE
@@ -401,4 +400,3 @@ char* commandGenerator(const char* text, int state) {
 #endif /* HAVE_LIBREADLINE */
 
 }/* CVC4 namespace */
-
diff --git a/src/main/interactive_shell.h b/src/main/interactive_shell.h
index ef55919a1..1b1031776 100644
--- a/src/main/interactive_shell.h
+++ b/src/main/interactive_shell.h
@@ -18,9 +18,9 @@
 #include <iostream>
 #include <string>
 
-#include "util/language.h"
-#include "util/unsafe_interrupt_exception.h"
+#include "options/language.h"
 #include "options/options.h"
+#include "util/unsafe_interrupt_exception.h"
 
 namespace CVC4 {
 
diff --git a/src/main/main.cpp b/src/main/main.cpp
index 1c825bc35..36a339d94 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -13,30 +13,29 @@
  **
  ** Main driver for CVC4 executable.
  **/
+#include "main/main.h"
 
 #include <cstdlib>
 #include <cstring>
 #include <fstream>
 #include <iostream>
-
 #include <stdio.h>
 #include <unistd.h>
 
-#include "main/main.h"
-#include "main/interactive_shell.h"
+#include "base/output.h"
+#include "expr/expr_manager.h"
+#include "expr/result.h"
+#include "expr/statistics.h"
 #include "main/command_executor.h"
+#include "main/interactive_shell.h"
+#include "options/language.h"
+#include "options/main_options.h"
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
 #include "parser/parser_exception.h"
-#include "expr/expr_manager.h"
 #include "smt/smt_engine.h"
-#include "expr/command.h"
+#include "smt_util/command.h"
 #include "util/configuration.h"
-#include "main/options.h"
-#include "util/output.h"
-#include "util/result.h"
-#include "util/statistics.h"
-#include "util/language.h"
 
 using namespace std;
 using namespace CVC4;
diff --git a/src/main/main.h b/src/main/main.h
index a2e813c6c..7dda429af 100644
--- a/src/main/main.h
+++ b/src/main/main.h
@@ -17,14 +17,14 @@
 #include <exception>
 #include <string>
 
-#include "options/options.h"
+#include "base/exception.h"
+#include "base/tls.h"
+#include "cvc4autoconfig.h"
 #include "expr/expr_manager.h"
+#include "expr/statistics.h"
+#include "expr/statistics_registry.h"
+#include "options/options.h"
 #include "smt/smt_engine.h"
-#include "util/exception.h"
-#include "util/statistics.h"
-#include "util/tls.h"
-#include "util/statistics_registry.h"
-#include "cvc4autoconfig.h"
 
 #ifndef __CVC4__MAIN__MAIN_H
 #define __CVC4__MAIN__MAIN_H
diff --git a/src/main/options b/src/main/options
deleted file mode 100644
index f523ea499..000000000
--- a/src/main/options
+++ /dev/null
@@ -1,63 +0,0 @@
-#
-# Option specification file for CVC4
-# See src/options/base_options for a description of this file format
-#
-
-module DRIVER "main/options.h" Driver
-
-common-option version -V --version/ bool
- identify this CVC4 binary
-undocumented-alias --license = --version
-
-common-option help -h --help/ bool
- full command line reference
-
-common-option - --show-config void :handler CVC4::main::showConfiguration :handler-include "main/options_handlers.h"
- show CVC4 static configuration
-
-option - --show-debug-tags void :handler CVC4::main::showDebugTags :handler-include "main/options_handlers.h"
- show all available tags for debugging
-option - --show-trace-tags void :handler CVC4::main::showTraceTags :handler-include "main/options_handlers.h"
- show all available tags for tracing
-
-expert-option earlyExit --early-exit bool :default true
- do not run destructors at exit; default on except in debug builds
-
-# portfolio options
-option threads --threads=N unsigned :default 2 :predicate options::greater(0)
- Total number of threads for portfolio
-option - --threadN=string void :handler CVC4::main::threadN :handler-include "main/options_handlers.h"
- configures portfolio thread N (0..#threads-1)
-option threadStackSize --thread-stack=N unsigned :default 0
- stack size for worker threads in MB (0 means use Boost/thread lib default)
-option threadArgv std::vector<std::string> :include <vector> <string>
- Thread configuration (a string to be passed to parseOptions)
-option thread_id int :default -1
- Thread ID, for internal use in case of multi-threaded run
-option sharingFilterByLength --filter-lemma-length=N int :default -1 :read-write
- don't share (among portfolio threads) lemmas strictly longer than N
-option fallbackSequential  --fallback-sequential bool :default false
- Switch to sequential mode (instead of printing an error) if it can't be solved in portfolio mode
-option incrementalParallel --incremental-parallel bool :default false :link --incremental
- Use parallel solver even in incremental mode (may print 'unknown's at times)
-
-option interactive : --interactive bool :read-write
- force interactive/non-interactive mode
-undocumented-option interactivePrompt /--no-interactive-prompt bool :default true
- turn off interactive prompting while in interactive mode
-
-# error behaviors (--immediate-exit is default in cases we support, thus no options)
-option continuedExecution --continued-execution/ bool :default false :link "--interactive --no-interactive-prompt"/
- continue executing commands, even on error
-
-option segvSpin --segv-spin bool :default false
- spin on segfault/other crash waiting for gdb
-undocumented-alias --segv-nospin = --no-segv-spin
-
-expert-option tearDownIncremental : --tear-down-incremental bool :default false
- implement PUSH/POP/multi-query by destroying and recreating SmtEngine
-
-expert-option waitToJoin --wait-to-join bool :default true
- wait for other threads to join before quitting
-
-endmodule
diff --git a/src/main/options_handlers.h b/src/main/options_handlers.h
deleted file mode 100644
index 00f192d2f..000000000
--- a/src/main/options_handlers.h
+++ /dev/null
@@ -1,115 +0,0 @@
-/*********************                                                        */
-/*! \file options_handlers.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 Custom handlers and predicates for main driver options
- **
- ** Custom handlers and predicates for main driver options.
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__MAIN__OPTIONS_HANDLERS_H
-#define __CVC4__MAIN__OPTIONS_HANDLERS_H
-
-namespace CVC4 {
-namespace main {
-
-inline void showConfiguration(std::string option, SmtEngine* smt) {
-  fputs(Configuration::about().c_str(), stdout);
-  printf("\n");
-  printf("version    : %s\n", Configuration::getVersionString().c_str());
-  if(Configuration::isGitBuild()) {
-    const char* branchName = Configuration::getGitBranchName();
-    if(*branchName == '\0') {
-      branchName = "-";
-    }
-    printf("scm        : git [%s %s%s]\n",
-           branchName,
-           std::string(Configuration::getGitCommit()).substr(0, 8).c_str(),
-           Configuration::hasGitModifications() ?
-             " (with modifications)" : "");
-  } else if(Configuration::isSubversionBuild()) {
-    printf("scm        : svn [%s r%u%s]\n",
-           Configuration::getSubversionBranchName(),
-           Configuration::getSubversionRevision(),
-           Configuration::hasSubversionModifications() ?
-             " (with modifications)" : "");
-  } else {
-    printf("scm        : no\n");
-  }
-  printf("\n");
-  printf("library    : %u.%u.%u\n",
-         Configuration::getVersionMajor(),
-         Configuration::getVersionMinor(),
-         Configuration::getVersionRelease());
-  printf("\n");
-  printf("debug code : %s\n", Configuration::isDebugBuild() ? "yes" : "no");
-  printf("statistics : %s\n", Configuration::isStatisticsBuild() ? "yes" : "no");
-  printf("replay     : %s\n", Configuration::isReplayBuild() ? "yes" : "no");
-  printf("tracing    : %s\n", Configuration::isTracingBuild() ? "yes" : "no");
-  printf("dumping    : %s\n", Configuration::isDumpingBuild() ? "yes" : "no");
-  printf("muzzled    : %s\n", Configuration::isMuzzledBuild() ? "yes" : "no");
-  printf("assertions : %s\n", Configuration::isAssertionBuild() ? "yes" : "no");
-  printf("proof      : %s\n", Configuration::isProofBuild() ? "yes" : "no");
-  printf("coverage   : %s\n", Configuration::isCoverageBuild() ? "yes" : "no");
-  printf("profiling  : %s\n", Configuration::isProfilingBuild() ? "yes" : "no");
-  printf("competition: %s\n", Configuration::isCompetitionBuild() ? "yes" : "no");
-  printf("\n");
-  printf("cudd       : %s\n", Configuration::isBuiltWithCudd() ? "yes" : "no");
-  printf("cln        : %s\n", Configuration::isBuiltWithCln() ? "yes" : "no");
-  printf("gmp        : %s\n", Configuration::isBuiltWithGmp() ? "yes" : "no");
-  printf("glpk       : %s\n", Configuration::isBuiltWithGlpk() ? "yes" : "no");
-  printf("abc        : %s\n", Configuration::isBuiltWithAbc() ? "yes" : "no");
-  printf("readline   : %s\n", Configuration::isBuiltWithReadline() ? "yes" : "no");
-  printf("tls        : %s\n", Configuration::isBuiltWithTlsSupport() ? "yes" : "no");
-  exit(0);
-}
-
-inline void showDebugTags(std::string option, SmtEngine* smt) {
-  if(Configuration::isDebugBuild() && Configuration::isTracingBuild()) {
-    printf("available tags:");
-    unsigned ntags = Configuration::getNumDebugTags();
-    char const* const* tags = Configuration::getDebugTags();
-    for(unsigned i = 0; i < ntags; ++ i) {
-      printf(" %s", tags[i]);
-    }
-    printf("\n");
-  } else if(! Configuration::isDebugBuild()) {
-    throw OptionException("debug tags not available in non-debug builds");
-  } else {
-    throw OptionException("debug tags not available in non-tracing builds");
-  }
-  exit(0);
-}
-
-inline void showTraceTags(std::string option, SmtEngine* smt) {
-  if(Configuration::isTracingBuild()) {
-    printf("available tags:");
-    unsigned ntags = Configuration::getNumTraceTags();
-    char const* const* tags = Configuration::getTraceTags();
-    for (unsigned i = 0; i < ntags; ++ i) {
-      printf(" %s", tags[i]);
-    }
-    printf("\n");
-  } else {
-    throw OptionException("trace tags not available in non-tracing build");
-  }
-  exit(0);
-}
-
-inline void threadN(std::string option, SmtEngine* smt) {
-  throw OptionException(option + " is not a real option by itself.  Use e.g. --thread0=\"--random-seed=10 --random-freq=0.02\" --thread1=\"--random-seed=20 --random-freq=0.05\"");
-}
-
-}/* CVC4::main namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__MAIN__OPTIONS_HANDLERS_H */
diff --git a/src/main/portfolio.cpp b/src/main/portfolio.cpp
index 51b4779cc..884c3eda7 100644
--- a/src/main/portfolio.cpp
+++ b/src/main/portfolio.cpp
@@ -19,11 +19,12 @@
 #include <boost/thread/condition.hpp>
 #include <boost/exception_ptr.hpp>
 
-#include "smt/smt_engine.h"
-#include "util/output.h"
-#include "util/result.h"
-#include "util/statistics_registry.h"
+#include "base/output.h"
+#include "expr/result.h"
+#include "expr/statistics_registry.h"
 #include "options/options.h"
+#include "smt/smt_engine.h"
+
 
 
 namespace CVC4 {
diff --git a/src/main/portfolio.h b/src/main/portfolio.h
index f89c8f548..5a730c005 100644
--- a/src/main/portfolio.h
+++ b/src/main/portfolio.h
@@ -19,10 +19,10 @@
 #include <boost/function.hpp>
 #include <utility>
 
-#include "smt/smt_engine.h"
-#include "expr/command.h"
+#include "expr/statistics_registry.h"
 #include "options/options.h"
-#include "util/statistics_registry.h"
+#include "smt/smt_engine.h"
+#include "smt_util/command.h"
 
 namespace CVC4 {
 
diff --git a/src/main/portfolio_util.cpp b/src/main/portfolio_util.cpp
index 7a4beb0d0..6b5fe4723 100644
--- a/src/main/portfolio_util.cpp
+++ b/src/main/portfolio_util.cpp
@@ -12,13 +12,16 @@
  ** \brief Code relevant only for portfolio builds
  **/
 
+#include <unistd.h>
+
 #include <cassert>
 #include <vector>
-#include <unistd.h>
+
+#include "options/main_options.h"
 #include "options/options.h"
-#include "main/options.h"
-#include "prop/options.h"
-#include "smt/options.h"
+#include "options/prop_options.h"
+#include "options/smt_options.h"
+#include "smt/smt_options_handler.h"
 
 using namespace std;
 
@@ -28,6 +31,9 @@ vector<Options> parseThreadSpecificOptions(Options opts)
 {
   vector<Options> threadOptions;
 
+#warning "TODO: Check that the SmtEngine pointer should be NULL with Kshitij."
+  smt::SmtOptionsHandler optionsHandler(NULL);
+
   unsigned numThreads = opts[options::threads];
 
   for(unsigned i = 0; i < numThreads; ++i) {
@@ -37,7 +43,7 @@ vector<Options> parseThreadSpecificOptions(Options opts)
     // Set thread identifier
     tOpts.set(options::thread_id, i);
 
-    if(i < opts[options::threadArgv].size() && 
+    if(i < opts[options::threadArgv].size() &&
        !opts[options::threadArgv][i].empty()) {
 
       // separate out the thread's individual configuration string
@@ -60,7 +66,7 @@ vector<Options> parseThreadSpecificOptions(Options opts)
       *vp++ = NULL;
       if(targc > 1) { // this is necessary in case you do e.g. --thread0="  "
         try {
-          tOpts.parseOptions(targc, targv);
+          tOpts.parseOptions(targc, targv, &optionsHandler);
         } catch(OptionException& e) {
           stringstream ss;
           ss << optid << ": " << e.getMessage();
diff --git a/src/main/portfolio_util.h b/src/main/portfolio_util.h
index 8ae730506..d6d6a2d02 100644
--- a/src/main/portfolio_util.h
+++ b/src/main/portfolio_util.h
@@ -17,12 +17,12 @@
 
 #include <queue>
 
+#include "base/output.h"
 #include "expr/pickler.h"
+#include "options/main_options.h"
+#include "smt_util/lemma_input_channel.h"
+#include "smt_util/lemma_output_channel.h"
 #include "util/channel.h"
-#include "util/lemma_input_channel.h"
-#include "util/lemma_output_channel.h"
-#include "util/output.h"
-#include "main/options.h"
 
 namespace CVC4 {
 
diff --git a/src/main/util.cpp b/src/main/util.cpp
index f0cab25fa..86272ee53 100644
--- a/src/main/util.cpp
+++ b/src/main/util.cpp
@@ -28,15 +28,14 @@
 
 #endif /* __WIN32__ */
 
-#include "util/exception.h"
-#include "options/options.h"
-#include "util/statistics.h"
-#include "util/tls.h"
-#include "smt/smt_engine.h"
-
+#include "base/exception.h"
+#include "base/tls.h"
 #include "cvc4autoconfig.h"
-#include "main/main.h"
+#include "expr/statistics.h"
 #include "main/command_executor.h"
+#include "main/main.h"
+#include "options/options.h"
+#include "smt/smt_engine.h"
 
 using CVC4::Exception;
 using namespace std;