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

util/options.h,cpp

5 files changed, 71 insertions, 406 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/getopt.cpp b/src/main/getopt.cpp
deleted file mode 100644
index 25badb7e5..000000000
--- a/src/main/getopt.cpp
+++ /dev/null
@@ -1,360 +0,0 @@
-/*********************                                                        */
-/*! \file getopt.cpp
- ** \verbatim
- ** Original author: mdeters
- ** Major contributors: cconway
- ** Minor contributors (to current version): dejan, barrett
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Contains code for handling command-line options.
- **
- ** Contains code for handling command-line options
- **/
-
-#include <cstdio>
-#include <cstdlib>
-#include <new>
-#include <unistd.h>
-#include <string.h>
-#include <stdint.h>
-#include <time.h>
-
-#include <getopt.h>
-
-#include "util/exception.h"
-#include "util/configuration.h"
-#include "util/output.h"
-#include "smt/options.h"
-#include "util/language.h"
-#include "expr/expr.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[] = "\
-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\
-  smt | smtlib   SMT-LIB format 1.2\n\
-  smt2 | smtlib2 SMT-LIB format 2.0\n\
-";
-
-/**
- * For the main getopt() routine, we need ways to switch on long
- * options without clashing with short option characters.  This is an
- * enum of those long options.  For long options (e.g. "--verbose")
- * with a short option equivalent ("-v"), we use the single-letter
- * short option; therefore, this enumeration starts at 256 to avoid
- * any collision.
- */
-enum OptionValue {
-  SMTCOMP = 256, /* no clash with char options */
-  STATS,
-  SEGV_NOSPIN,
-  PARSE_ONLY,
-  NO_CHECKING,
-  USE_MMAP,
-  SHOW_CONFIG,
-  STRICT_PARSING,
-  DEFAULT_EXPR_DEPTH,
-  PRINT_EXPR_TYPES,
-  UF_THEORY,
-  LAZY_DEFINITION_EXPANSION,
-  INTERACTIVE,
-  NO_INTERACTIVE,
-  PRODUCE_MODELS,
-  PRODUCE_ASSIGNMENTS,
-  NO_TYPE_CHECKING,
-  LAZY_TYPE_CHECKING,
-  EAGER_TYPE_CHECKING,
-};/* enum OptionValue */
-
-/**
- * This is a table of long options.  By policy, each short option
- * should have an equivalent long option (but the reverse isn't the
- * case), so this table should thus contain all command-line options.
- *
- * Each option in this array has four elements:
- *
- * 1. the long option string
- * 2. argument behavior for the option:
- *    no_argument - no argument permitted
- *    required_argument - an argument is expected
- *    optional_argument - an argument is permitted but not required
- * 3. this is a pointer to an int which is set to the 4th entry of the
- *    array if the option is present; or NULL, in which case
- *    getopt_long() returns the 4th entry
- * 4. the return value for getopt_long() when this long option (or the
- *    value to set the 3rd entry to; see #3)
- *
- * If you add something here, you should add it in src/main/usage.h
- * also, to document it.
- *
- * If you add something that has a short option equivalent, you should
- * add it to the getopt_long() call in parseOptions().
- */
-static struct option cmdlineOptions[] = {
-  // name, has_arg, *flag, val
-  { "verbose"    , no_argument      , NULL, 'v'         },
-  { "quiet"      , no_argument      , NULL, 'q'         },
-  { "debug"      , required_argument, NULL, 'd'         },
-  { "trace"      , required_argument, NULL, 't'         },
-  { "stats"      , no_argument      , NULL, STATS       },
-  { "no-checking", no_argument      , NULL, NO_CHECKING },
-  { "show-config", no_argument      , NULL, SHOW_CONFIG },
-  { "segv-nospin", no_argument      , NULL, SEGV_NOSPIN },
-  { "help"       , no_argument      , NULL, 'h'         },
-  { "version"    , no_argument      , NULL, 'V'         },
-  { "about"      , no_argument      , NULL, 'V'         },
-  { "lang"       , required_argument, NULL, 'L'         },
-  { "parse-only" , no_argument      , NULL, PARSE_ONLY  },
-  { "mmap"       , no_argument      , NULL, USE_MMAP    },
-  { "strict-parsing", no_argument   , NULL, STRICT_PARSING },
-  { "default-expr-depth", required_argument, NULL, DEFAULT_EXPR_DEPTH },
-  { "print-expr-types", no_argument , NULL, PRINT_EXPR_TYPES },
-  { "uf"         , required_argument, NULL, UF_THEORY },
-  { "lazy-definition-expansion", no_argument, NULL, LAZY_DEFINITION_EXPANSION },
-  { "interactive", no_argument      , NULL, INTERACTIVE },
-  { "no-interactive", no_argument   , NULL, NO_INTERACTIVE },
-  { "produce-models", no_argument   , NULL, PRODUCE_MODELS},
-  { "produce-assignments", no_argument, NULL, PRODUCE_ASSIGNMENTS},
-  { "no-type-checking", no_argument, NULL, NO_TYPE_CHECKING},
-  { "lazy-type-checking", no_argument, NULL, LAZY_TYPE_CHECKING},
-  { "eager-type-checking", no_argument, NULL, EAGER_TYPE_CHECKING},
-  { 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)
-throw(OptionException) {
-  progPath = progName = argv[0];
-  int c;
-
-  // find the base name of the program
-  const char *x = strrchr(progName, '/');
-  if(x != NULL) {
-    progName = x + 1;
-  }
-  opts->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
-  // non-option argument is encountered.  The initial ':' indicates
-  // that getopt_long() should return ':' instead of '?' for a missing
-  // option argument.  Then, each letter is a valid short option for
-  // getopt_long(), and if it's encountered, getopt_long() returns
-  // that character.  A ':' after an option character means an
-  // argument is required; two colons indicates an argument is
-  // optional; no colons indicate an argument is not permitted.
-  // cmdlineOptions specifies all the long-options and the return
-  // value for getopt_long() should they be encountered.
-  while((c = getopt_long(argc, argv,
-                         "+:hVvqL:d:t:",
-                         cmdlineOptions, NULL)) != -1) {
-    switch(c) {
-
-    case 'h':
-      printf(usage, opts->binary_name.c_str());
-      exit(1);
-
-    case 'V':
-      fputs(Configuration::about().c_str(), stdout);
-      exit(0);
-
-    case 'v':
-      ++opts->verbosity;
-      break;
-
-    case 'q':
-      --opts->verbosity;
-      break;
-
-    case 'L':
-      if(!strcmp(optarg, "cvc4") || !strcmp(optarg, "pl")) {
-        opts->inputLanguage = language::input::LANG_CVC4;
-        break;
-      } else if(!strcmp(optarg, "smtlib") || !strcmp(optarg, "smt")) {
-        opts->inputLanguage = language::input::LANG_SMTLIB;
-        break;
-      } else if(!strcmp(optarg, "smtlib2") || !strcmp(optarg, "smt2")) {
-        opts->inputLanguage = language::input::LANG_SMTLIB_V2;
-        break;
-      } else if(!strcmp(optarg, "auto")) {
-        opts->inputLanguage = language::input::LANG_AUTO;
-        break;
-      }
-
-      if(strcmp(optarg, "help")) {
-        throw OptionException(string("unknown language for --lang: `") +
-                              optarg + "'.  Try --lang help.");
-      }
-
-      fputs(lang_help, stdout);
-      exit(1);
-
-    case 't':
-      Trace.on(optarg);
-      break;
-
-    case 'd':
-      Debug.on(optarg);
-      Trace.on(optarg);
-      break;
-
-    case STATS:
-      opts->statistics = true;
-      break;
-
-    case SEGV_NOSPIN:
-      segvNoSpin = true;
-      break;
-
-    case PARSE_ONLY:
-      opts->parseOnly = true;
-      break;
-
-    case NO_CHECKING:
-      opts->semanticChecks = false;
-      opts->typeChecking = false;
-      opts->earlyTypeChecking = false;
-      break;
-
-    case USE_MMAP:
-      opts->memoryMap = true;
-      break;
-
-    case STRICT_PARSING:
-      opts->strictParsing = true;
-      break;
-
-    case DEFAULT_EXPR_DEPTH:
-      {
-        int depth = atoi(optarg);
-        Debug.getStream() << Expr::setdepth(depth);
-        Trace.getStream() << Expr::setdepth(depth);
-        Notice.getStream() << Expr::setdepth(depth);
-        Chat.getStream() << Expr::setdepth(depth);
-        Message.getStream() << Expr::setdepth(depth);
-        Warning.getStream() << Expr::setdepth(depth);
-      }
-      break;
-
-    case PRINT_EXPR_TYPES:
-      {
-        Debug.getStream() << Expr::printtypes(true);
-        Trace.getStream() << Expr::printtypes(true);
-        Notice.getStream() << Expr::printtypes(true);
-        Chat.getStream() << Expr::printtypes(true);
-        Message.getStream() << Expr::printtypes(true);
-        Warning.getStream() << Expr::printtypes(true);
-      }
-      break;
-
-    case UF_THEORY:
-      {
-        if(!strcmp(optarg, "tim")) {
-          opts->uf_implementation = Options::TIM;
-        } else if(!strcmp(optarg, "morgan")) {
-          opts->uf_implementation = Options::MORGAN;
-        } else if(!strcmp(optarg, "help")) {
-          printf("UF implementations available:\n");
-          printf("tim\n");
-          printf("morgan\n");
-          exit(1);
-        } else {
-          throw OptionException(string("unknown option for --uf: `") +
-                                optarg + "'.  Try --uf help.");
-        }
-      }
-      break;
-
-    case LAZY_DEFINITION_EXPANSION:
-      opts->lazyDefinitionExpansion = true;
-      break;
-
-    case INTERACTIVE:
-      opts->interactive = true;
-      opts->interactiveSetByUser = true;
-      break;
-
-    case NO_INTERACTIVE:
-      opts->interactive = false;
-      opts->interactiveSetByUser = true;
-      break;
-
-    case PRODUCE_MODELS:
-      opts->produceModels = true;
-      break;
-
-    case PRODUCE_ASSIGNMENTS:
-      opts->produceAssignments = true;
-      break;
-
-    case NO_TYPE_CHECKING:
-      opts->typeChecking = false;
-      opts->earlyTypeChecking = false;
-      break;
-
-    case LAZY_TYPE_CHECKING:
-      opts->earlyTypeChecking = false;
-      break;
-
-    case EAGER_TYPE_CHECKING:
-      opts->typeChecking = true;
-      opts->earlyTypeChecking = true;
-      break;
-
-    case SHOW_CONFIG:
-      fputs(Configuration::about().c_str(), stdout);
-      printf("\n");
-      printf("version    : %s\n", Configuration::getVersionString().c_str());
-      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("tracing    : %s\n", Configuration::isTracingBuild() ? "yes" : "no");
-      printf("muzzled    : %s\n", Configuration::isMuzzledBuild() ? "yes" : "no");
-      printf("assertions : %s\n", Configuration::isAssertionBuild() ? "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");
-      exit(0);
-
-    case '?':
-      throw OptionException(string("can't understand option `") + argv[optind - 1] + "'");
-
-    case ':':
-      throw OptionException(string("option `") + argv[optind - 1] + "' missing its required argument");
-
-    default:
-      throw OptionException(string("can't understand option:") + argv[optind - 1] + "'");
-    }
-
-  }
-
-  return optind;
-}
-
-}/* CVC4::main namespace */
-}/* CVC4 namespace */
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"