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

util/options.h,cpp

1 files changed, 67 insertions, 24 deletions

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);
     }