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.

1 files changed, 0 insertions, 517 deletions

diff --git a/src/smt/options_handlers.h b/src/smt/options_handlers.h
deleted file mode 100644
index eeefd7af0..000000000
--- a/src/smt/options_handlers.h
+++ /dev/null
@@ -1,517 +0,0 @@
-/*********************                                                        */
-/*! \file options_handlers.h
- ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): Clark Barrett, Liana Hadarean
- ** 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 SmtEngine options
- **
- ** Custom handlers and predicates for SmtEngine options.
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__SMT__OPTIONS_HANDLERS_H
-#define __CVC4__SMT__OPTIONS_HANDLERS_H
-
-#include "cvc4autoconfig.h"
-#include "util/configuration_private.h"
-#include "util/dump.h"
-#include "util/resource_manager.h"
-#include "smt/modal_exception.h"
-#include "smt/smt_engine.h"
-#include "lib/strtok_r.h"
-
-#include <cerrno>
-#include <cstring>
-#include <sstream>
-
-namespace CVC4 {
-namespace smt {
-
-static inline std::string __cvc4_errno_failreason() {
-#if HAVE_STRERROR_R
-#if STRERROR_R_CHAR_P
-  if(errno != 0) {
-    // GNU version of strerror_r: *might* use the given buffer,
-    // or might not.  It returns a pointer to buf, or not.
-    char buf[80];
-    return std::string(strerror_r(errno, buf, sizeof buf));
-  } else {
-    return "unknown reason";
-  }
-#else /* STRERROR_R_CHAR_P */
-  if(errno != 0) {
-    // XSI version of strerror_r: always uses the given buffer.
-    // Returns an error code.
-    char buf[80];
-    if(strerror_r(errno, buf, sizeof buf) == 0) {
-      return std::string(buf);
-    } else {
-      // some error occurred while getting the error string
-      return "unknown reason";
-    }
-  } else {
-    return "unknown reason";
-  }
-#endif /* STRERROR_R_CHAR_P */
-#else /* HAVE_STRERROR_R */
-  return "unknown reason";
-#endif /* HAVE_STRERROR_R */
-}
-
-static const std::string dumpHelp = "\
-Dump modes currently supported by the --dump option:\n\
-\n\
-benchmark\n\
-+ Dump the benchmark structure (set-logic, push/pop, queries, etc.), but\n\
-  does not include any declarations or assertions.  Implied by all following\n\
-  modes.\n\
-\n\
-declarations\n\
-+ Dump user declarations.  Implied by all following modes.\n\
-\n\
-skolems\n\
-+ Dump internally-created skolem variable declarations.  These can\n\
-  arise from preprocessing simplifications, existential elimination,\n\
-  and a number of other things.  Implied by all following modes.\n\
-\n\
-assertions\n\
-+ Output the assertions after preprocessing and before clausification.\n\
-  Can also specify \"assertions:pre-PASS\" or \"assertions:post-PASS\",\n\
-  where PASS is one of the preprocessing passes: definition-expansion\n\
-  boolean-terms constrain-subtypes substitution strings-pp skolem-quant\n\
-  simplify static-learning ite-removal repeat-simplify\n\
-  rewrite-apply-to-const theory-preprocessing.\n\
-  PASS can also be the special value \"everything\", in which case the\n\
-  assertions are printed before any preprocessing (with\n\
-  \"assertions:pre-everything\") or after all preprocessing completes\n\
-  (with \"assertions:post-everything\").\n\
-\n\
-clauses\n\
-+ Do all the preprocessing outlined above, and dump the CNF-converted\n\
-  output\n\
-\n\
-state\n\
-+ Dump all contextual assertions (e.g., SAT decisions, propagations..).\n\
-  Implied by all \"stateful\" modes below and conflicts with all\n\
-  non-stateful modes below.\n\
-\n\
-t-conflicts [non-stateful]\n\
-+ Output correctness queries for all theory conflicts\n\
-\n\
-missed-t-conflicts [stateful]\n\
-+ Output completeness queries for theory conflicts\n\
-\n\
-t-propagations [stateful]\n\
-+ Output correctness queries for all theory propagations\n\
-\n\
-missed-t-propagations [stateful]\n\
-+ Output completeness queries for theory propagations (LARGE and EXPENSIVE)\n\
-\n\
-t-lemmas [non-stateful]\n\
-+ Output correctness queries for all theory lemmas\n\
-\n\
-t-explanations [non-stateful]\n\
-+ Output correctness queries for all theory explanations\n\
-\n\
-bv-rewrites [non-stateful]\n\
-+ Output correctness queries for all bitvector rewrites\n\
-\n\
-bv-abstraction [non-stateful]\n\
-+ Output correctness queries for all bv abstraction \n\
-\n\
-bv-algebraic [non-stateful]\n\
-+ Output correctness queries for bv algebraic solver. \n\
-\n\
-theory::fullcheck [non-stateful]\n                                      \
-+ Output completeness queries for all full-check effort-level theory checks\n\
-\n\
-Dump modes can be combined with multiple uses of --dump.  Generally you want\n\
-one from the assertions category (either assertions or clauses), and\n\
-perhaps one or more stateful or non-stateful modes for checking correctness\n\
-and completeness of decision procedure implementations.  Stateful modes dump\n\
-the contextual assertions made by the core solver (all decisions and\n\
-propagations as assertions; that affects the validity of the resulting\n\
-correctness and completeness queries, so of course stateful and non-stateful\n\
-modes cannot be mixed in the same run.\n\
-\n\
-The --output-language option controls the language used for dumping, and\n\
-this allows you to connect CVC4 to another solver implementation via a UNIX\n\
-pipe to perform on-line checking.  The --dump-to option can be used to dump\n\
-to a file.\n\
-";
-
-static const std::string simplificationHelp = "\
-Simplification modes currently supported by the --simplification option:\n\
-\n\
-batch (default) \n\
-+ save up all ASSERTions; run nonclausal simplification and clausal\n\
-  (MiniSat) propagation for all of them only after reaching a querying command\n\
-  (CHECKSAT or QUERY or predicate SUBTYPE declaration)\n\
-\n\
-none\n\
-+ do not perform nonclausal simplification\n\
-";
-
-inline void dumpMode(std::string option, std::string optarg, SmtEngine* smt) {
-#ifdef CVC4_DUMPING
-  char* optargPtr = strdup(optarg.c_str());
-  char* tokstr = optargPtr;
-  char* toksave;
-  while((optargPtr = strtok_r(tokstr, ",", &toksave)) != NULL) {
-    tokstr = NULL;
-    if(!strcmp(optargPtr, "benchmark")) {
-    } else if(!strcmp(optargPtr, "declarations")) {
-    } else if(!strcmp(optargPtr, "assertions")) {
-      Dump.on("assertions:post-everything");
-    } else if(!strncmp(optargPtr, "assertions:", 11)) {
-      const char* p = optargPtr + 11;
-      if(!strncmp(p, "pre-", 4)) {
-        p += 4;
-      } else if(!strncmp(p, "post-", 5)) {
-        p += 5;
-      } else {
-        throw OptionException(std::string("don't know how to dump `") +
-                              optargPtr + "'.  Please consult --dump help.");
-      }
-      if(!strcmp(p, "everything")) {
-      } else if(!strcmp(p, "definition-expansion")) {
-      } else if(!strcmp(p, "boolean-terms")) {
-      } else if(!strcmp(p, "constrain-subtypes")) {
-      } else if(!strcmp(p, "substitution")) {
-      } else if(!strcmp(p, "strings-pp")) {
-      } else if(!strcmp(p, "skolem-quant")) {
-      } else if(!strcmp(p, "simplify")) {
-      } else if(!strcmp(p, "static-learning")) {
-      } else if(!strcmp(p, "ite-removal")) {
-      } else if(!strcmp(p, "repeat-simplify")) {
-      } else if(!strcmp(p, "rewrite-apply-to-const")) {
-      } else if(!strcmp(p, "theory-preprocessing")) {
-      } else if(!strcmp(p, "nonclausal")) {
-      } else if(!strcmp(p, "theorypp")) {
-      } else if(!strcmp(p, "itesimp")) {
-      } else if(!strcmp(p, "unconstrained")) {
-      } else if(!strcmp(p, "repeatsimp")) {
-      } else {
-        throw OptionException(std::string("don't know how to dump `") +
-                              optargPtr + "'.  Please consult --dump help.");
-      }
-      Dump.on("assertions");
-    } else if(!strcmp(optargPtr, "skolems")) {
-    } else if(!strcmp(optargPtr, "clauses")) {
-    } else if(!strcmp(optargPtr, "t-conflicts") ||
-              !strcmp(optargPtr, "t-lemmas") ||
-              !strcmp(optargPtr, "t-explanations") ||
-              !strcmp(optargPtr, "bv-rewrites") ||
-              !strcmp(optargPtr, "theory::fullcheck")) {
-      // These are "non-state-dumping" modes.  If state (SAT decisions,
-      // propagations, etc.) is dumped, it will interfere with the validity
-      // of these generated queries.
-      if(Dump.isOn("state")) {
-        throw OptionException(std::string("dump option `") + optargPtr +
-                              "' conflicts with a previous, "
-                              "state-dumping dump option.  You cannot "
-                              "mix stateful and non-stateful dumping modes; "
-                              "see --dump help.");
-      } else {
-        Dump.on("no-permit-state");
-      }
-    } else if(!strcmp(optargPtr, "state") ||
-              !strcmp(optargPtr, "missed-t-conflicts") ||
-              !strcmp(optargPtr, "t-propagations") ||
-              !strcmp(optargPtr, "missed-t-propagations")) {
-      // These are "state-dumping" modes.  If state (SAT decisions,
-      // propagations, etc.) is not dumped, it will interfere with the
-      // validity of these generated queries.
-      if(Dump.isOn("no-permit-state")) {
-        throw OptionException(std::string("dump option `") + optargPtr +
-                              "' conflicts with a previous, "
-                              "non-state-dumping dump option.  You cannot "
-                              "mix stateful and non-stateful dumping modes; "
-                              "see --dump help.");
-      } else {
-        Dump.on("state");
-      }
-    } else if(!strcmp(optargPtr, "help")) {
-      puts(dumpHelp.c_str());
-      exit(1);
-    } else if(!strcmp(optargPtr, "bv-abstraction")) {
-      Dump.on("bv-abstraction");
-    } else if(!strcmp(optargPtr, "bv-algebraic")) {
-      Dump.on("bv-algebraic");
-    } else {
-      throw OptionException(std::string("unknown option for --dump: `") +
-                            optargPtr + "'.  Try --dump help.");
-    }
-
-    Dump.on(optargPtr);
-    Dump.on("benchmark");
-    if(strcmp(optargPtr, "benchmark")) {
-      Dump.on("declarations");
-      if(strcmp(optargPtr, "declarations")) {
-        Dump.on("skolems");
-      }
-    }
-  }
-  free(optargPtr);
-#else /* CVC4_DUMPING */
-  throw OptionException("The dumping feature was disabled in this build of CVC4.");
-#endif /* CVC4_DUMPING */
-}
-
-inline LogicInfo stringToLogicInfo(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
-  try {
-    LogicInfo logic(optarg);
-    if(smt != NULL) {
-      smt->setLogic(logic);
-    }
-    return logic;
-  } catch(IllegalArgumentException& e) {
-    throw OptionException(std::string("invalid logic specification for --force-logic: `") +
-                          optarg + "':\n" + e.what());
-  }
-}
-
-inline SimplificationMode stringToSimplificationMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
-  if(optarg == "batch") {
-    return SIMPLIFICATION_MODE_BATCH;
-  } else if(optarg == "none") {
-    return SIMPLIFICATION_MODE_NONE;
-  } else if(optarg == "help") {
-    puts(simplificationHelp.c_str());
-    exit(1);
-  } else {
-    throw OptionException(std::string("unknown option for --simplification: `") +
-                          optarg + "'.  Try --simplification help.");
-  }
-}
-
-// ensure we haven't started search yet
-inline void beforeSearch(std::string option, bool value, SmtEngine* smt) throw(ModalException) {
-  if(smt != NULL && smt->d_fullyInited) {
-    std::stringstream ss;
-    ss << "cannot change option `" << option << "' after final initialization (i.e., after logic has been set)";
-    throw ModalException(ss.str());
-  }
-}
-
-inline void setProduceAssertions(std::string option, bool value, SmtEngine* smt) throw() {
-  options::produceAssertions.set(value);
-  options::interactiveMode.set(value);
-}
-
-// ensure we are a proof-enabled build of CVC4
-inline void proofEnabledBuild(std::string option, bool value, SmtEngine* smt) throw(OptionException) {
-#if !(IS_PROOFS_BUILD)
-  if(value) {
-    std::stringstream ss;
-    ss << "option `" << option << "' requires a proofs-enabled build of CVC4; this binary was not built with proof support";
-    throw OptionException(ss.str());
-  }
-#endif /* IS_PROOFS_BUILD */
-}
-
-// This macro is used for setting :regular-output-channel and :diagnostic-output-channel
-// to redirect a stream.  It maintains all attributes set on the stream.
-#define __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(__channel_get, __channel_set) \
-  { \
-    int dagSetting = expr::ExprDag::getDag(__channel_get); \
-    size_t exprDepthSetting = expr::ExprSetDepth::getDepth(__channel_get); \
-    bool printtypesSetting = expr::ExprPrintTypes::getPrintTypes(__channel_get); \
-    OutputLanguage languageSetting = expr::ExprSetLanguage::getLanguage(__channel_get); \
-    __channel_set; \
-    __channel_get << Expr::dag(dagSetting); \
-    __channel_get << Expr::setdepth(exprDepthSetting); \
-    __channel_get << Expr::printtypes(printtypesSetting); \
-    __channel_get << Expr::setlanguage(languageSetting); \
-  }
-
-inline void dumpToFile(std::string option, std::string optarg, SmtEngine* smt) {
-#ifdef CVC4_DUMPING
-  std::ostream* outStream = NULL;
-  if(optarg == "") {
-    throw OptionException(std::string("Bad file name for --dump-to"));
-  } else if(optarg == "-") {
-    outStream = &DumpOutC::dump_cout;
-  } else if(!options::filesystemAccess()) {
-    throw OptionException(std::string("Filesystem access not permitted"));
-  } else {
-    errno = 0;
-    outStream = new std::ofstream(optarg.c_str(), std::ofstream::out | std::ofstream::trunc);
-    if(outStream == NULL || !*outStream) {
-      std::stringstream ss;
-      ss << "Cannot open dump-to file: `" << optarg << "': " << __cvc4_errno_failreason();
-      throw OptionException(ss.str());
-    }
-  }
-  __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(Dump.getStream(), Dump.setStream(*outStream));
-#else /* CVC4_DUMPING */
-  throw OptionException("The dumping feature was disabled in this build of CVC4.");
-#endif /* CVC4_DUMPING */
-}
-
-inline void setRegularOutputChannel(std::string option, std::string optarg, SmtEngine* smt) {
-  std::ostream* outStream = NULL;
-  if(optarg == "") {
-    throw OptionException(std::string("Bad file name setting for regular output channel"));
-  } else if(optarg == "stdout") {
-    outStream = &std::cout;
-  } else if(optarg == "stderr") {
-    outStream = &std::cerr;
-  } else if(!options::filesystemAccess()) {
-    throw OptionException(std::string("Filesystem access not permitted"));
-  } else {
-    errno = 0;
-    outStream = new std::ofstream(optarg.c_str(), std::ofstream::out | std::ofstream::trunc);
-    if(outStream == NULL || !*outStream) {
-      std::stringstream ss;
-      ss << "Cannot open regular-output-channel file: `" << optarg << "': " << __cvc4_errno_failreason();
-      throw OptionException(ss.str());
-    }
-  }
-  __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(*options::err(), options::err.set(outStream));
-}
-
-inline void setDiagnosticOutputChannel(std::string option, std::string optarg, SmtEngine* smt) {
-  std::ostream* outStream = NULL;
-  if(optarg == "") {
-    throw OptionException(std::string("Bad file name setting for diagnostic output channel"));
-  } else if(optarg == "stdout") {
-    outStream = &std::cout;
-  } else if(optarg == "stderr") {
-    outStream = &std::cerr;
-  } else if(!options::filesystemAccess()) {
-    throw OptionException(std::string("Filesystem access not permitted"));
-  } else {
-    errno = 0;
-    outStream = new std::ofstream(optarg.c_str(), std::ofstream::out | std::ofstream::trunc);
-    if(outStream == NULL || !*outStream) {
-      std::stringstream ss;
-      ss << "Cannot open diagnostic-output-channel file: `" << optarg << "': " << __cvc4_errno_failreason();
-      throw OptionException(ss.str());
-    }
-  }
-  __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(Debug.getStream(), Debug.setStream(*outStream));
-  __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(Warning.getStream(), Warning.setStream(*outStream));
-  __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(Message.getStream(), Message.setStream(*outStream));
-  __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(Notice.getStream(), Notice.setStream(*outStream));
-  __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(Chat.getStream(), Chat.setStream(*outStream));
-  __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(Trace.getStream(), Trace.setStream(*outStream));
-  __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(*options::err(), options::err.set(outStream));
-}
-
-#undef __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM
-
-inline std::string checkReplayFilename(std::string option, std::string optarg, SmtEngine* smt) {
-#ifdef CVC4_REPLAY
-  if(optarg == "") {
-    throw OptionException(std::string("Bad file name for --replay"));
-  } else {
-    return optarg;
-  }
-#else /* CVC4_REPLAY */
-  throw OptionException("The replay feature was disabled in this build of CVC4.");
-#endif /* CVC4_REPLAY */
-}
-
-inline std::ostream* checkReplayLogFilename(std::string option, std::string optarg, SmtEngine* smt) {
-#ifdef CVC4_REPLAY
-  if(optarg == "") {
-    throw OptionException(std::string("Bad file name for --replay-log"));
-  } else if(optarg == "-") {
-    return &std::cout;
-  } else if(!options::filesystemAccess()) {
-    throw OptionException(std::string("Filesystem access not permitted"));
-  } else {
-    errno = 0;
-    std::ostream* replayLog = new std::ofstream(optarg.c_str(), std::ofstream::out | std::ofstream::trunc);
-    if(replayLog == NULL || !*replayLog) {
-      std::stringstream ss;
-      ss << "Cannot open replay-log file: `" << optarg << "': " << __cvc4_errno_failreason();
-      throw OptionException(ss.str());
-    }
-    return replayLog;
-  }
-#else /* CVC4_REPLAY */
-  throw OptionException("The replay feature was disabled in this build of CVC4.");
-#endif /* CVC4_REPLAY */
-}
-
-// ensure we are a stats-enabled build of CVC4
-inline void statsEnabledBuild(std::string option, bool value, SmtEngine* smt) throw(OptionException) {
-#ifndef CVC4_STATISTICS_ON
-  if(value) {
-    std::stringstream ss;
-    ss << "option `" << option << "' requires a statistics-enabled build of CVC4; this binary was not built with statistics support";
-    throw OptionException(ss.str());
-  }
-#endif /* CVC4_STATISTICS_ON */
-}
-
-inline unsigned long tlimitHandler(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
-  unsigned long ms;
-  std::istringstream convert(optarg);
-  if (!(convert >> ms))
-    throw OptionException("option `"+option+"` requires a number as an argument");
-
-  // make sure the resource is set if the option is updated
-  // if the smt engine is null the resource will be set in the
-  if (smt != NULL) {
-    ResourceManager* rm = NodeManager::fromExprManager(smt->getExprManager())->getResourceManager();
-    rm->setTimeLimit(ms, true);
-  }
-  return ms;
-}
-
-inline unsigned long tlimitPerHandler(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
-  unsigned long ms;
-
-  std::istringstream convert(optarg);
-  if (!(convert >> ms))
-    throw OptionException("option `"+option+"` requires a number as an argument");
-
-  if (smt != NULL) {
-    ResourceManager* rm = NodeManager::fromExprManager(smt->getExprManager())->getResourceManager();
-    rm->setTimeLimit(ms, false);
-  }
-  return ms;
-}
-
-inline unsigned long rlimitHandler(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
-  unsigned long ms;
-
-  std::istringstream convert(optarg);
-  if (!(convert >> ms))
-    throw OptionException("option `"+option+"` requires a number as an argument");
-
-  if (smt != NULL) {
-    ResourceManager* rm = NodeManager::fromExprManager(smt->getExprManager())->getResourceManager();
-    rm->setResourceLimit(ms, true);
-  }
-  return ms;
-}
-
-inline unsigned long rlimitPerHandler(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
-  unsigned long ms;
-
-  std::istringstream convert(optarg);
-  if (!(convert >> ms))
-    throw OptionException("option `"+option+"` requires a number as an argument");
-
-  if (smt != NULL) {
-    ResourceManager* rm = NodeManager::fromExprManager(smt->getExprManager())->getResourceManager();
-    rm->setResourceLimit(ms, false);
-  }
-  return ms;
-}
-
-}/* CVC4::smt namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__SMT__OPTIONS_HANDLERS_H */