Merging main/getopt.cpp, main/usage.h, and smt/options.h in

util/options.h,cpp

17 files changed, 243 insertions, 140 deletions

diff --git a/src/main/Makefile.am b/src/main/Makefile.am
index b6cdbb1f4..05a451d52 100644
--- a/src/main/Makefile.am
+++ b/src/main/Makefile.am
@@ -6,7 +6,6 @@ AM_CXXFLAGS = -Wall -Wno-unknown-pragmas
 bin_PROGRAMS = cvc4
 
 cvc4_SOURCES = \
-	getopt.cpp \
 	interactive_shell.h \
 	interactive_shell.cpp \
 	main.h \
diff --git a/src/main/main.cpp b/src/main/main.cpp
index 8ed938351..544c6fd29 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -28,7 +28,6 @@
 #include "cvc4autoconfig.h"
 #include "main.h"
 #include "interactive_shell.h"
-#include "usage.h"
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
 #include "parser/parser_exception.h"
@@ -37,8 +36,8 @@
 #include "expr/command.h"
 #include "util/Assert.h"
 #include "util/configuration.h"
+#include "util/options.h"
 #include "util/output.h"
-#include "smt/options.h"
 #include "util/result.h"
 #include "util/stats.h"
 
@@ -47,14 +46,41 @@ using namespace CVC4;
 using namespace CVC4::parser;
 using namespace CVC4::main;
 
-namespace CVC4 {
-  namespace main {
-    struct Options options;
-  }/* CVC4::main namespace */
-}/* CVC4 namespace */
-
 int runCvc4(int argc, char* argv[]);
 void doCommand(SmtEngine&, Command*);
+void printUsage();
+
+namespace CVC4 {
+  namespace main {/* Global options variable */
+    Options options;
+
+    /** Full argv[0] */
+    const char *progPath;
+
+    /** Just the basename component of argv[0] */
+    const char *progName;
+  }
+}
+
+
+// no more % chars in here without being escaped; it's used as a
+// printf() format string
+const string usageMessage = "\
+usage: %s [options] [input-file]\n\
+\n\
+Without an input file, or with `-', CVC4 reads from standard input.\n\
+\n\
+CVC4 options:\n";
+
+void printUsage() {
+  stringstream ss;
+  ss << "usage: " << options.binary_name << " [options] [input-file]" << endl
+      << endl
+      << "Without an input file, or with `-', CVC4 reads from standard input." << endl
+      << endl
+      << "CVC4 options:" << endl;
+  Options::printUsage( ss.str(), options.out );
+}
 
 /**
  * CVC4's main() routine is just an exception-safe wrapper around CVC4.
@@ -68,34 +94,34 @@ int main(int argc, char* argv[]) {
     return runCvc4(argc, argv);
   } catch(OptionException& e) {
 #ifdef CVC4_COMPETITION_MODE
-    cout << "unknown" << endl;
+    options.out << "unknown" << endl;
 #endif
     cerr << "CVC4 Error:" << endl << e << endl;
-    printf(usage, options.binary_name.c_str());
+    printUsage();
     exit(1);
   } catch(Exception& e) {
 #ifdef CVC4_COMPETITION_MODE
-    cout << "unknown" << endl;
+    options.out << "unknown" << endl;
 #endif
-    cerr << "CVC4 Error:" << endl << e << endl;
+    options.err << "CVC4 Error:" << endl << e << endl;
     if(options.statistics) {
-      StatisticsRegistry::flushStatistics(cerr);
+      StatisticsRegistry::flushStatistics(options.err);
     }
     exit(1);
   } catch(bad_alloc) {
 #ifdef CVC4_COMPETITION_MODE
-    cout << "unknown" << endl;
+    options.out << "unknown" << endl;
 #endif
-    cerr << "CVC4 ran out of memory." << endl;
+    options.err << "CVC4 ran out of memory." << endl;
     if(options.statistics) {
-      StatisticsRegistry::flushStatistics(cerr);
+      StatisticsRegistry::flushStatistics(options.err);
     }
     exit(1);
   } catch(...) {
 #ifdef CVC4_COMPETITION_MODE
-    cout << "unknown" << endl;
+    options.out << "unknown" << endl;
 #endif
-    cerr << "CVC4 threw an exception of unknown type." << endl;
+    options.err << "CVC4 threw an exception of unknown type." << endl;
     exit(1);
   }
 }
@@ -106,12 +132,29 @@ int runCvc4(int argc, char* argv[]) {
   // Initialize the signal handlers
   cvc4_init();
 
+  progPath = argv[0];
+  
   // Parse the options
-  int firstArgIndex = parseOptions(argc, argv, &options);
+  int firstArgIndex = options.parseOptions(argc, argv);
+
+  progName = options.binary_name.c_str();
+
+  if( options.help ) {
+    printUsage();
+    exit(1);
+  } else if( options.languageHelp ) {
+    Options::printLanguageHelp(options.out);
+    exit(1);
+  } else if( options.version ) {
+    options.out << Configuration::about().c_str() << flush;
+    exit(0);
+  } 
+
+  segvNoSpin = options.segvNoSpin;
 
   // If in competition mode, set output stream option to flush immediately
 #ifdef CVC4_COMPETITION_MODE
-  cout << unitbuf;
+  options.out << unitbuf;
 #endif
 
   // We only accept one input file
@@ -201,7 +244,7 @@ int runCvc4(int argc, char* argv[]) {
   // Parse and execute commands until we are done
   Command* cmd;
   if( options.interactive ) {
-    InteractiveShell shell(cin,cout,parserBuilder);
+    InteractiveShell shell(options.in,options.out,parserBuilder);
     while((cmd = shell.readCommand())) {
       doCommand(smt,cmd);
       delete cmd;
@@ -237,7 +280,7 @@ int runCvc4(int argc, char* argv[]) {
   StatisticsRegistry::registerStat(&s_statSatResult);
 
   if(options.statistics) {
-    StatisticsRegistry::flushStatistics(cerr);
+    StatisticsRegistry::flushStatistics(options.err);
   }
 
   StatisticsRegistry::unregisterStat(&s_statSatResult);
@@ -261,11 +304,11 @@ void doCommand(SmtEngine& smt, Command* cmd) {
     }
   } else {
     if(options.verbosity > 0) {
-      cout << "Invoking: " << *cmd << endl;
+      options.out << "Invoking: " << *cmd << endl;
     }
 
     if(options.verbosity >= 0) {
-      cmd->invoke(&smt, cout);
+      cmd->invoke(&smt, options.out);
     } else {
       cmd->invoke(&smt);
     }
diff --git a/src/main/main.h b/src/main/main.h
index 350578ffa..b6a8bcfb1 100644
--- a/src/main/main.h
+++ b/src/main/main.h
@@ -19,26 +19,16 @@
 #include <exception>
 #include <string>
 
+#include "util/options.h"
 #include "cvc4autoconfig.h"
-#include "util/exception.h"
 
 #ifndef __CVC4__MAIN__MAIN_H
 #define __CVC4__MAIN__MAIN_H
 
 namespace CVC4 {
 
-struct Options;
-
 namespace main {
 
-/** Class representing an option-parsing exception. */
-class OptionException : public CVC4::Exception {
-public:
-  OptionException(const std::string& s) throw() :
-    CVC4::Exception("Error in option parsing: " + s) {
-  }
-};/* class OptionException */
-
 /** Full argv[0] */
 extern const char *progPath;
 
@@ -52,14 +42,7 @@ extern const char *progName;
  */
 extern bool segvNoSpin;
 
-/**
- * Keep a copy of the options around globally, so that signal handlers can
- * access it.
- */
-extern struct Options options;
-
-/** Parse argc/argv and put the result into a CVC4::Options struct. */
-int parseOptions(int argc, char** argv, CVC4::Options*) throw(OptionException);
+extern Options options;
 
 /** Initialize the driver.  Sets signal handlers for SIGINT and SIGSEGV. */
 void cvc4_init() throw();
diff --git a/src/main/util.cpp b/src/main/util.cpp
index 70cb85c93..4ec1c1bee 100644
--- a/src/main/util.cpp
+++ b/src/main/util.cpp
@@ -23,9 +23,9 @@
 #include <string.h>
 #include <signal.h>
 
-#include "util/exception.h"
-#include "smt/options.h"
 #include "util/Assert.h"
+#include "util/exception.h"
+#include "util/options.h"
 #include "util/stats.h"
 
 #include "cvc4autoconfig.h"
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index f503efae2..5851f3990 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -21,10 +21,10 @@
 #include "sat.h"
 
 #include "theory/theory_engine.h"
-#include "util/decision_engine.h"
 #include "util/Assert.h"
+#include "util/decision_engine.h"
+#include "util/options.h"
 #include "util/output.h"
-#include "smt/options.h"
 #include "util/result.h"
 
 #include <utility>
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index 1c7c506ee..ecef29ac2 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -24,9 +24,9 @@
 #define __CVC4__PROP_ENGINE_H
 
 #include "expr/node.h"
-#include "util/result.h"
 #include "util/decision_engine.h"
-#include "smt/options.h"
+#include "util/options.h"
+#include "util/result.h"
 
 namespace CVC4 {
 
diff --git a/src/prop/sat.h b/src/prop/sat.h
index 17bf447f8..550de5527 100644
--- a/src/prop/sat.h
+++ b/src/prop/sat.h
@@ -25,9 +25,9 @@
 // Optional blocks below will be unconditionally included
 #define __CVC4_USE_MINISAT
 
-#include "util/stats.h"
 #include "theory/theory.h"
-#include "smt/options.h"
+#include "util/options.h"
+#include "util/stats.h"
 
 #ifdef __CVC4_USE_MINISAT
 
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 149c3620d..81930a5ea 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -20,22 +20,22 @@
 #include <string>
 #include <sstream>
 
-#include "smt/smt_engine.h"
-#include "smt/modal_exception.h"
-#include "smt/bad_option_exception.h"
-#include "smt/no_such_function_exception.h"
-#include "context/context.h"
 #include "context/cdlist.h"
 #include "context/cdset.h"
-#include "expr/expr.h"
+#include "context/context.h"
 #include "expr/command.h"
+#include "expr/expr.h"
 #include "expr/node_builder.h"
-#include "util/output.h"
-#include "util/exception.h"
-#include "smt/options.h"
-#include "util/configuration.h"
 #include "prop/prop_engine.h"
+#include "smt/bad_option_exception.h"
+#include "smt/modal_exception.h"
+#include "smt/no_such_function_exception.h"
+#include "smt/smt_engine.h"
 #include "theory/theory_engine.h"
+#include "util/configuration.h"
+#include "util/exception.h"
+#include "util/options.h"
+#include "util/output.h"
 
 using namespace std;
 using namespace CVC4;
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 0831a0447..35bfb0bcc 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -23,19 +23,19 @@
 
 #include <vector>
 
-#include "expr/expr.h"
-#include "expr/expr_manager.h"
+#include "context/cdlist_forward.h"
 #include "context/cdmap_forward.h"
 #include "context/cdset_forward.h"
-#include "context/cdlist_forward.h"
-#include "util/result.h"
-#include "util/model.h"
-#include "util/sexpr.h"
-#include "util/hash.h"
+#include "expr/expr.h"
+#include "expr/expr_manager.h"
+#include "smt/bad_option_exception.h"
 #include "smt/modal_exception.h"
 #include "smt/no_such_function_exception.h"
-#include "smt/options.h"
-#include "smt/bad_option_exception.h"
+#include "util/hash.h"
+#include "util/model.h"
+#include "util/options.h"
+#include "util/result.h"
+#include "util/sexpr.h"
 
 // In terms of abstraction, this is below (and provides services to)
 // ValidityChecker and above (and requires the services of)
@@ -47,7 +47,7 @@ template <bool ref_count> class NodeTemplate;
 typedef NodeTemplate<true> Node;
 typedef NodeTemplate<false> TNode;
 class NodeHashFunction;
-class Command;
+
 class TheoryEngine;
 class DecisionEngine;
 
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 2fcfc9626..40debc7c7 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -19,13 +19,13 @@
 #include <vector>
 #include <list>
 
-#include "theory/theory_engine.h"
-#include "expr/node.h"
 #include "expr/attribute.h"
-#include "theory/theory.h"
+#include "expr/node.h"
 #include "expr/node_builder.h"
-#include "smt/options.h"
+#include "util/options.h"
 
+#include "theory/theory.h"
+#include "theory/theory_engine.h"
 #include "theory/builtin/theory_builtin.h"
 #include "theory/booleans/theory_bool.h"
 #include "theory/uf/theory_uf.h"
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 0bca372ca..7e08a29d5 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -23,10 +23,10 @@
 
 #include "expr/node.h"
 #include "prop/prop_engine.h"
-#include "smt/options.h"
 #include "theory/shared_term_manager.h"
 #include "theory/theory.h"
 #include "theory/theoryof_table.h"
+#include "util/options.h"
 #include "util/stats.h"
 
 namespace CVC4 {
diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index 61c0bf885..e75735f82 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -18,6 +18,8 @@ libutil_la_SOURCES = \
 	hash.h \
 	bool.h \
 	model.h \
+	options.h \
+	options.cpp \
 	output.cpp \
 	output.h \
 	result.h \
diff --git a/src/main/getopt.cpp b/src/util/options.cpp
index 25badb7e5..f6d3c3092 100644
--- a/src/main/getopt.cpp
+++ b/src/util/options.cpp
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file getopt.cpp
+/*! \file options.cpp
  ** \verbatim
  ** Original author: mdeters
  ** Major contributors: cconway
@@ -26,24 +26,48 @@
 
 #include <getopt.h>
 
-#include "util/exception.h"
+#include "expr/expr.h"
 #include "util/configuration.h"
-#include "util/output.h"
-#include "smt/options.h"
+#include "util/exception.h"
 #include "util/language.h"
-#include "expr/expr.h"
+#include "util/options.h"
+#include "util/output.h"
 
 #include "cvc4autoconfig.h"
-#include "main.h"
-#include "usage.h"
 
 using namespace std;
 using namespace CVC4;
 
 namespace CVC4 {
-namespace main {
 
-static const char lang_help[] = "\
+static const string optionsDescription = "\
+   --lang | -L            force input language (default is `auto'; see --lang help)\n\
+   --version | -V         identify this CVC4 binary\n\
+   --help | -h            this command line reference\n\
+   --parse-only           exit after parsing input\n\
+   --mmap                 memory map file input\n\
+   --show-config          show CVC4 static configuration\n\
+   --segv-nospin          don't spin on segfault waiting for gdb\n\
+   --lazy-type-checking   type check expressions only when necessary (default)\n\
+   --eager-type-checking  type check expressions immediately on creation\n\
+   --no-type-checking     never type check expressions\n\
+   --no-checking          disable ALL semantic checks, including type checks \n\
+   --strict-parsing       fail on non-conformant inputs (SMT2 only)\n\
+   --verbose | -v         increase verbosity (repeatable)\n\
+   --quiet | -q           decrease verbosity (repeatable)\n\
+   --trace | -t           tracing for something (e.g. --trace pushpop)\n\
+   --debug | -d           debugging for something (e.g. --debug arith), implies -t\n\
+   --stats                give statistics on exit\n\
+   --default-expr-depth=N print exprs to depth N (0 == default, -1 == no limit)\n\
+   --print-expr-types     print types with variables when printing exprs\n\
+   --uf=morgan|tim        select uninterpreted function theory implementation\n\
+   --interactive          run interactively\n\
+   --no-interactive       do not run interactively\n\
+   --produce-models       support the get-value command\n\
+   --produce-assignments  support the get-assignment command\n\
+   --lazy-definition-expansion expand define-fun lazily\n";
+
+static const string languageDescription = "\
 Languages currently supported as arguments to the -L / --lang option:\n\
   auto           attempt to automatically determine the input language\n\
   pl | cvc4      CVC4 presentation language\n\
@@ -51,6 +75,20 @@ Languages currently supported as arguments to the -L / --lang option:\n\
   smt2 | smtlib2 SMT-LIB format 2.0\n\
 ";
 
+string Options::getDescription() const {
+  return optionsDescription;
+}
+
+void Options::printUsage(const string msg, std::ostream& out) {
+  out << msg << optionsDescription << endl << flush;
+  // printf(usage + options.getDescription(), options.binary_name.c_str());
+  //     printf(usage, binary_name.c_str());
+}
+
+void Options::printLanguageHelp(std::ostream& out) {
+  out << languageDescription << flush;
+}
+
 /**
  * For the main getopt() routine, we need ways to switch on long
  * options without clashing with short option characters.  This is an
@@ -136,16 +174,11 @@ static struct option cmdlineOptions[] = {
   { NULL         , no_argument      , NULL, '\0'        }
 };/* if you add things to the above, please remember to update usage.h! */
 
-/** Full argv[0] */
-const char *progPath;
-
-/** Just the basename component of argv[0] */
-const char *progName;
 
 /** Parse argc/argv and put the result into a CVC4::Options struct. */
-int parseOptions(int argc, char* argv[], CVC4::Options* opts)
+int Options::parseOptions(int argc, char* argv[])
 throw(OptionException) {
-  progPath = progName = argv[0];
+  const char *progName = argv[0];
   int c;
 
   // find the base name of the program
@@ -153,7 +186,7 @@ throw(OptionException) {
   if(x != NULL) {
     progName = x + 1;
   }
-  opts->binary_name = string(progName);
+  binary_name = string(progName);
 
   // The strange string in this call is the short option string.  The
   // initial '+' means that option processing stops as soon as a
@@ -172,33 +205,37 @@ throw(OptionException) {
     switch(c) {
 
     case 'h':
-      printf(usage, opts->binary_name.c_str());
-      exit(1);
+      help = true;
+      break;
+      // options.printUsage(usage);
+      // exit(1);
 
     case 'V':
-      fputs(Configuration::about().c_str(), stdout);
-      exit(0);
+      version = true;
+      break;
+      // fputs(Configuration::about().c_str(), stdout);
+      // exit(0);
 
     case 'v':
-      ++opts->verbosity;
+      ++verbosity;
       break;
 
     case 'q':
-      --opts->verbosity;
+      --verbosity;
       break;
 
     case 'L':
       if(!strcmp(optarg, "cvc4") || !strcmp(optarg, "pl")) {
-        opts->inputLanguage = language::input::LANG_CVC4;
+        inputLanguage = language::input::LANG_CVC4;
         break;
       } else if(!strcmp(optarg, "smtlib") || !strcmp(optarg, "smt")) {
-        opts->inputLanguage = language::input::LANG_SMTLIB;
+        inputLanguage = language::input::LANG_SMTLIB;
         break;
       } else if(!strcmp(optarg, "smtlib2") || !strcmp(optarg, "smt2")) {
-        opts->inputLanguage = language::input::LANG_SMTLIB_V2;
+        inputLanguage = language::input::LANG_SMTLIB_V2;
         break;
       } else if(!strcmp(optarg, "auto")) {
-        opts->inputLanguage = language::input::LANG_AUTO;
+        inputLanguage = language::input::LANG_AUTO;
         break;
       }
 
@@ -207,8 +244,8 @@ throw(OptionException) {
                               optarg + "'.  Try --lang help.");
       }
 
-      fputs(lang_help, stdout);
-      exit(1);
+      languageHelp = true;
+      break;
 
     case 't':
       Trace.on(optarg);
@@ -220,7 +257,7 @@ throw(OptionException) {
       break;
 
     case STATS:
-      opts->statistics = true;
+      statistics = true;
       break;
 
     case SEGV_NOSPIN:
@@ -228,21 +265,21 @@ throw(OptionException) {
       break;
 
     case PARSE_ONLY:
-      opts->parseOnly = true;
+      parseOnly = true;
       break;
 
     case NO_CHECKING:
-      opts->semanticChecks = false;
-      opts->typeChecking = false;
-      opts->earlyTypeChecking = false;
+      semanticChecks = false;
+      typeChecking = false;
+      earlyTypeChecking = false;
       break;
 
     case USE_MMAP:
-      opts->memoryMap = true;
+      memoryMap = true;
       break;
 
     case STRICT_PARSING:
-      opts->strictParsing = true;
+      strictParsing = true;
       break;
 
     case DEFAULT_EXPR_DEPTH:
@@ -271,9 +308,9 @@ throw(OptionException) {
     case UF_THEORY:
       {
         if(!strcmp(optarg, "tim")) {
-          opts->uf_implementation = Options::TIM;
+          uf_implementation = Options::TIM;
         } else if(!strcmp(optarg, "morgan")) {
-          opts->uf_implementation = Options::MORGAN;
+          uf_implementation = Options::MORGAN;
         } else if(!strcmp(optarg, "help")) {
           printf("UF implementations available:\n");
           printf("tim\n");
@@ -287,39 +324,39 @@ throw(OptionException) {
       break;
 
     case LAZY_DEFINITION_EXPANSION:
-      opts->lazyDefinitionExpansion = true;
+      lazyDefinitionExpansion = true;
       break;
 
     case INTERACTIVE:
-      opts->interactive = true;
-      opts->interactiveSetByUser = true;
+      interactive = true;
+      interactiveSetByUser = true;
       break;
 
     case NO_INTERACTIVE:
-      opts->interactive = false;
-      opts->interactiveSetByUser = true;
+      interactive = false;
+      interactiveSetByUser = true;
       break;
 
     case PRODUCE_MODELS:
-      opts->produceModels = true;
+      produceModels = true;
       break;
 
     case PRODUCE_ASSIGNMENTS:
-      opts->produceAssignments = true;
+      produceAssignments = true;
       break;
 
     case NO_TYPE_CHECKING:
-      opts->typeChecking = false;
-      opts->earlyTypeChecking = false;
+      typeChecking = false;
+      earlyTypeChecking = false;
       break;
 
     case LAZY_TYPE_CHECKING:
-      opts->earlyTypeChecking = false;
+      earlyTypeChecking = false;
       break;
 
     case EAGER_TYPE_CHECKING:
-      opts->typeChecking = true;
-      opts->earlyTypeChecking = true;
+      typeChecking = true;
+      earlyTypeChecking = true;
       break;
 
     case SHOW_CONFIG:
@@ -356,5 +393,4 @@ throw(OptionException) {
   return optind;
 }
 
-}/* CVC4::main namespace */
 }/* CVC4 namespace */
diff --git a/src/smt/options.h b/src/util/options.h
index 73c38545f..b56741fba 100644
--- a/src/smt/options.h
+++ b/src/util/options.h
@@ -30,18 +30,28 @@
 #include <iostream>
 #include <string>
 
-#include "util/language.h"
+#include "exception.h"
+#include "language.h"
 
 namespace CVC4 {
 
+/** Class representing an option-parsing exception. */
+class OptionException : public CVC4::Exception {
+public:
+    OptionException(const std::string& s) throw() :
+      CVC4::Exception("Error in option parsing: " + s) {
+    }
+};/* class OptionException */
+
 struct CVC4_PUBLIC Options {
 
   std::string binary_name;
 
   bool statistics;
 
-  std::ostream *out;
-  std::ostream *err;
+  std::istream& in;
+  std::ostream& out;
+  std::ostream& err;
 
   /* -1 means no output */
   /* 0 is normal (and default) -- warnings only */
@@ -59,6 +69,15 @@ struct CVC4_PUBLIC Options {
   /** Which implementation of uninterpreted function theory to use */
   UfImplementation uf_implementation;
 
+  /** Should we print the help message? */
+  bool help;
+
+  /** Should we print the release information? */
+  bool version;
+
+  /** Should we print the language help information? */
+  bool languageHelp;
+
   /** Should we exit after parsing? */
   bool parseOnly;
 
@@ -83,6 +102,9 @@ struct CVC4_PUBLIC Options {
    */
   bool interactiveSetByUser;
 
+  /** Whether we should "spin" on a SIG_SEGV. */
+  bool segvNoSpin;
+
   /** Whether we support SmtEngine::getValue() for this run. */
   bool produceModels;
 
@@ -98,8 +120,9 @@ struct CVC4_PUBLIC Options {
   Options() :
     binary_name(),
     statistics(false),
-    out(0),
-    err(0),
+    in(std::cin),
+    out(std::cout),
+    err(std::cerr),
     verbosity(0),
     inputLanguage(language::input::LANG_AUTO),
     uf_implementation(MORGAN),
@@ -110,11 +133,27 @@ struct CVC4_PUBLIC Options {
     lazyDefinitionExpansion(false),
     interactive(false),
     interactiveSetByUser(false),
+    segvNoSpin(false),
     produceModels(false),
     produceAssignments(false),
     typeChecking(true),
     earlyTypeChecking(USE_EARLY_TYPE_CHECKING_BY_DEFAULT) {
   }
+
+  /** 
+   * Get a description of the command-line flags accepted by
+   * parseOptions.  The returned string will be escaped so that it is
+   * suitable as an argument to printf. */
+  std::string getDescription() const;
+
+  static void printUsage(const std::string msg, std::ostream& out);
+  static void printLanguageHelp(std::ostream& out);
+
+  /**
+   * Initialize the options based on the given command-line arguments.
+   */
+  int parseOptions(int argc, char* argv[])
+    throw(OptionException);
 };/* struct Options */
 
 inline std::ostream& operator<<(std::ostream& out,
@@ -133,6 +172,8 @@ inline std::ostream& operator<<(std::ostream& out,
   return out;
 }
 
+ 
+
 }/* CVC4 namespace */
 
 #undef USE_EARLY_TYPE_CHECKING_BY_DEFAULT
diff --git a/test/unit/prop/cnf_stream_black.h b/test/unit/prop/cnf_stream_black.h
index b340beb50..cee8a6a64 100644
--- a/test/unit/prop/cnf_stream_black.h
+++ b/test/unit/prop/cnf_stream_black.h
@@ -30,7 +30,6 @@
 #include "prop/prop_engine.h"
 #include "prop/sat.h"
 #include "smt/smt_engine.h"
-#include "smt/options.h"
 #include "util/decision_engine.h"
 
 using namespace CVC4;
diff --git a/test/unit/theory/shared_term_manager_black.h b/test/unit/theory/shared_term_manager_black.h
index 5007f43ed..7340f6ae7 100644
--- a/test/unit/theory/shared_term_manager_black.h
+++ b/test/unit/theory/shared_term_manager_black.h
@@ -31,7 +31,7 @@
 #include "context/context.h"
 #include "util/rational.h"
 #include "util/integer.h"
-#include "smt/options.h"
+#include "util/options.h"
 #include "util/Assert.h"
 
 using namespace CVC4;
@@ -51,7 +51,6 @@ class SharedTermManagerBlack : public CxxTest::TestSuite {
   NodeManager* d_nm;
   NodeManagerScope* d_scope;
   TheoryEngine* d_theoryEngine;
-  Options d_options;
 
 public:
 
@@ -61,7 +60,8 @@ public:
     d_nm = new NodeManager(d_ctxt);
     d_scope = new NodeManagerScope(d_nm);
 
-    d_theoryEngine = new TheoryEngine(d_ctxt, d_options);
+    Options options;
+    d_theoryEngine = new TheoryEngine(d_ctxt, options);
   }
 
   void tearDown() {
diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h
index 00766ec90..bd6ec515b 100644
--- a/test/unit/theory/theory_engine_white.h
+++ b/test/unit/theory/theory_engine_white.h
@@ -35,7 +35,7 @@
 #include "context/context.h"
 #include "util/rational.h"
 #include "util/integer.h"
-#include "smt/options.h"
+#include "util/options.h"
 #include "util/Assert.h"
 
 using namespace CVC4;
@@ -227,7 +227,6 @@ class TheoryEngineWhite : public CxxTest::TestSuite {
   FakeOutputChannel *d_nullChannel;
   FakeTheory *d_builtin, *d_bool, *d_uf, *d_arith, *d_arrays, *d_bv;
   TheoryEngine* d_theoryEngine;
-  Options d_options;
 
 public:
 
@@ -248,7 +247,8 @@ public:
     d_bv = new FakeTheory(d_ctxt, *d_nullChannel, "BV");
 
     // create the TheoryEngine
-    d_theoryEngine = new TheoryEngine(d_ctxt, d_options);
+    Options options;
+    d_theoryEngine = new TheoryEngine(d_ctxt, options);
 
     // insert our fake versions into the TheoryEngine's theoryOf table
     d_theoryEngine->d_theoryOfTable.