src/expr/kind.h is now automatically generated.

Build src/expr before src/util.

Moved CVC4::Command to the expr package.

Re-quieted the "result is sat/invalid" etc. from PropEngine (this is
now done at the main driver level).

Added file-level documentation to Antlr sources

When built for debug, spin on SEGV instead of aborting.  Really useful
for debugging problems that crop up only on long runs.  Added
'--segv-nospin' to override this spinning so that "make check,"
nightly regressions, etc. don't hang when built with debug.

Updated src/main/about.h for 2010.

6 files changed, 84 insertions, 24 deletions

diff --git a/src/main/about.h b/src/main/about.h
index d00b1eaec..a30cffd39 100644
--- a/src/main/about.h
+++ b/src/main/about.h
@@ -21,9 +21,11 @@ namespace main {
 
 const char about[] = "\
 This is a pre-release of CVC4.\n\
-Copyright (C) 2009 The ACSys Group\n\
-                   Courant Institute of Mathematical Sciences,\n\
-                   New York University\n\
+Copyright (C) 2009, 2010\n\
+  The ACSys Group\n\
+  Courant Institute of Mathematical Sciences,\n\
+  New York University\n\
+  New York, NY  10012  USA\n\
 ";
 
 }/* CVC4::main namespace */
diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp
index 6eb70a3e1..f4d32cd68 100644
--- a/src/main/getopt.cpp
+++ b/src/main/getopt.cpp
@@ -56,25 +56,35 @@ CNF conversions currently supported as arguments to the --cnf option:\n\
 enum OptionValue {
   CNF = 256, /* no clash with char options */
   SMTCOMP,
-  STATS
+  STATS,
+  SEGV_NOSPIN
 };/* enum OptionValue */
 
 // FIXME add a comment here describing the option array
 static struct option cmdlineOptions[] = {
   // name, has_arg, *flag, val
-  { "help"   , no_argument      , NULL, 'h'     },
-  { "version", no_argument      , NULL, 'V'     },
-  { "verbose", no_argument      , NULL, 'v'     },
-  { "quiet"  , no_argument      , NULL, 'q'     },
-  { "lang"   , required_argument, NULL, 'L'     },
-  { "debug"  , required_argument, NULL, 'd'     },
-  { "cnf"    , required_argument, NULL, CNF     },
-  { "smtcomp", no_argument      , NULL, SMTCOMP },
-  { "stats"  , no_argument      , NULL, STATS   }
+  { "help"       , no_argument      , NULL, 'h'         },
+  { "version"    , no_argument      , NULL, 'V'         },
+  { "verbose"    , no_argument      , NULL, 'v'         },
+  { "quiet"      , no_argument      , NULL, 'q'         },
+  { "lang"       , required_argument, NULL, 'L'         },
+  { "debug"      , required_argument, NULL, 'd'         },
+  { "cnf"        , required_argument, NULL, CNF         },
+  { "smtcomp"    , no_argument      , NULL, SMTCOMP     },
+  { "stats"      , no_argument      , NULL, STATS       },
+  { "segv-nospin", no_argument      , NULL, SEGV_NOSPIN }
 };/* if you add things to the above, please remember to update usage.h! */
 
-int parseOptions(int argc, char** argv, CVC4::Options* opts) throw(OptionException) {
-  const char *progName = argv[0];
+/** 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
@@ -85,17 +95,18 @@ int parseOptions(int argc, char** argv, CVC4::Options* opts) throw(OptionExcepti
   opts->binary_name = string(progName);
 
   // FIXME add a comment here describing the option string
-  while((c = getopt_long(argc, argv, "+:hVvqL:d:", cmdlineOptions, NULL)) != -1) {
+  while((c = getopt_long(argc, argv,
+                         "+:hVvqL:d:",
+                         cmdlineOptions, NULL)) != -1) {
     switch(c) {
 
     case 'h':
       printf(usage, opts->binary_name.c_str());
       exit(1);
-      break;
 
     case 'V':
       fputs(about, stdout);
-      break;
+      exit(0);
 
     case 'v':
       ++opts->verbosity;
@@ -148,6 +159,10 @@ int parseOptions(int argc, char** argv, CVC4::Options* opts) throw(OptionExcepti
       opts->statistics = true;
       break;
 
+    case SEGV_NOSPIN:
+      segvNoSpin = true;
+      break;
+
     case SMTCOMP:
       // silences CVC4 (except "sat" or "unsat" or "unknown", forces smtlib input)
       opts->smtcomp_mode = true;
diff --git a/src/main/main.cpp b/src/main/main.cpp
index 02ebe8deb..de179edb8 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -25,7 +25,7 @@
 #include "parser/parser.h"
 #include "expr/expr_manager.h"
 #include "smt/smt_engine.h"
-#include "util/command.h"
+#include "expr/command.h"
 #include "util/result.h"
 #include "util/Assert.h"
 #include "util/output.h"
diff --git a/src/main/main.h b/src/main/main.h
index 9b2f4fcbe..0c78912ae 100644
--- a/src/main/main.h
+++ b/src/main/main.h
@@ -28,12 +28,31 @@ 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) {}
+  OptionException(const std::string& s) throw() :
+    CVC4::Exception("Error in option parsing: " + s) {
+  }
 };/* class OptionException */
 
+/** Full argv[0] */
+extern const char *progPath;
+
+/** Just the basename component of argv[0] */
+extern const char *progName;
+
+/**
+ * If true, will not spin on segfault even when CVC4_DEBUG is on.
+ * Useful for nightly regressions, noninteractive performance runs
+ * etc.  See util.cpp.
+ */
+extern bool segvNoSpin;
+
+/** Parse argc/argv and put the result into a CVC4::Options struct. */
 int parseOptions(int argc, char** argv, CVC4::Options*) throw(OptionException);
+
+/** Initialize the driver.  Sets signal handlers for SIGINT and SIGSEGV. */
 void cvc4_init() throw();
 
 }/* CVC4::main namespace */
diff --git a/src/main/usage.h b/src/main/usage.h
index f6c089f1d..6927f0f2f 100644
--- a/src/main/usage.h
+++ b/src/main/usage.h
@@ -27,8 +27,7 @@ usage: %s [options] [input-file]\n\
 Without an input file, or with `-', CVC4 reads from standard input.\n\
 \n\
 CVC4 options:\n\
-   --lang | -L     set input language (--lang help gives a list;\n\
-                                       `auto' is default)\n\
+   --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\
    --verbose | -v  increase verbosity (repeatable)\n\
@@ -36,6 +35,7 @@ CVC4 options:\n\
    --debug | -d    debugging for something (e.g. --debug arith)\n\
    --smtcomp       competition mode (very quiet)\n\
    --stats         give statistics on exit\n\
+   --segv-nospin   (debug builds only) don't spin on segfault waiting for gdb\n\
 ";
 
 }/* CVC4::main namespace */
diff --git a/src/main/util.cpp b/src/main/util.cpp
index df4ab803d..03ae26092 100644
--- a/src/main/util.cpp
+++ b/src/main/util.cpp
@@ -10,7 +10,7 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **
- ** [[ Add file-specific comments here ]]
+ ** Utilities for the main driver.
  **/
 
 #include <cstdio>
@@ -22,24 +22,48 @@
 #include "util/exception.h"
 #include "config.h"
 
+#include "main.h"
+
 using CVC4::Exception;
 using namespace std;
 
 namespace CVC4 {
 namespace main {
 
-// FIXME add comments to functions
+/**
+ * If true, will not spin on segfault even when CVC4_DEBUG is on.
+ * Useful for nightly regressions, noninteractive performance runs
+ * etc.
+ */
+bool segvNoSpin = false;
 
+/** Handler for SIGINT, i.e., when the user hits control C. */
 void sigint_handler(int sig, siginfo_t* info, void*) {
   fprintf(stderr, "CVC4 interrupted by user.\n");
   abort();
 }
 
+/** Handler for SIGSEGV (segfault). */
 void segv_handler(int sig, siginfo_t* info, void*) {
+#ifdef CVC4_DEBUG
+  fprintf(stderr, "CVC4 suffered a segfault in DEBUG mode.\n");
+  if(segvNoSpin) {
+    fprintf(stderr, "No-spin requested, aborting...\n");
+    abort();
+  } else {
+    fprintf(stderr, "Spinning so that a debugger can be connected.\n");
+    fprintf(stderr, "Try:  gdb %s %u\n", progName, getpid());
+    for(;;) {
+      sleep(60);
+    }
+  }
+#else /* CVC4_DEBUG */
   fprintf(stderr, "CVC4 suffered a segfault.\n");
   abort();
+#endif /* CVC4_DEBUG */
 }
 
+/** Initialize the driver.  Sets signal handlers for SIGINT and SIGSEGV. */
 void cvc4_init() throw() {
   struct sigaction act1;
   act1.sa_sigaction = sigint_handler;