* public/private code untangled (smt/smt_engine.h no longer #includes

  expr/node.h).  This removes the warnings we had during compilation,
  and heads off a number of potential linking errors due to improper
  inlining of private (library-only) stuff in client (out-of-library)
  code.

* "configure" now takes some options as part of a "bare-option" build
  type (e.g., "./configure debug-coverage" or "./configure production-muzzle").

* split cdo.h, cdlist.h, cdmap.h, and cdset.h from context.h

* split cdlist_black unit test from context_black

* implement CDMap<>.

* give ExprManagers ownership of the context (and have SmtEngine share
  that one)

* fix main driver to properly report file-not-found

* fix MemoryMappedInputBuffer class to report reasons for
  "errno"-returned system errors

* src/expr/attribute.h: context-dependent attribute kinds now
  supported

* test/unit/expr/node_white.h: context-dependent attribute tests

* src/prop/cnf_conversion.h and associated parts of src/util/options.h
  and src/main/getopt.cpp: obsolete command-line option, removed.

* src/util/Assert.h: assertions are now somewhat more useful (in debug
  builds, anyway) during stack unwinding.

* test/unit/theory/theory_black.h: test context-dependent behavior of
  registerTerm() attribute for theories

* src/expr/node_builder.h: formatting, fixes for arithmetic
  convenience node builders, check memory allocations

* test/unit/expr/node_builder_black.h: add tessts for addition,
  subtraction, unary minus, and multiplication convenience node
  builders

* src/expr/attribute.h: more comments

* (various) code formatting, comment cleanup, added throws specifier
  to some destructors

* contrib/code-checker: prototype perl script to test (some) code policy

* contrib/indent-settings: command line for GNU indent to indent using
  CVC4 style (sort of; this is a work in progress)

* COPYING: legal stuff

* DESIGN_QUESTIONS: obsolete, removed

3 files changed, 45 insertions, 25 deletions

diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp
index baad6fe31..b319b7293 100644
--- a/src/main/getopt.cpp
+++ b/src/main/getopt.cpp
@@ -46,12 +46,6 @@ Languages currently supported as arguments to the -L / --lang option:\n\
   smt | smtlib  SMT-LIB format\n\
 ";
 
-static const char cnf_help[] = "\
-CNF conversions currently supported as arguments to the --cnf option:\n\
-  direct  put in equiv. CNF directly (exp. blow up in # clauses, no new vars)\n\
-  var     variable-introduction method (new vars, no exp. blow up in # clauses)\n\
-";
-
 /**
  * For the main getopt() routine, we need ways to switch on long
  * options without clashing with short option characters.  This is an
@@ -61,8 +55,7 @@ CNF conversions currently supported as arguments to the --cnf option:\n\
  * any collision.
  */
 enum OptionValue {
-  CNF = 256, /* no clash with char options */
-  SMTCOMP,
+  SMTCOMP = 256, /* no clash with char options */
   STATS,
   SEGV_NOSPIN,
   PARSE_ONLY,
@@ -98,7 +91,6 @@ static struct option cmdlineOptions[] = {
   { "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 },
@@ -179,21 +171,6 @@ throw(OptionException) {
       fputs(lang_help, stdout);
       exit(1);
 
-    case CNF:
-      if(!strcmp(optarg, "direct")) {
-        opts->d_cnfConversion = CNF_DIRECT_EXPONENTIAL;
-        break;
-      } else if(!strcmp(optarg, "var")) {
-        opts->d_cnfConversion = CNF_VAR_INTRODUCTION;
-        break;
-      } else if(strcmp(optarg, "help")) {
-        throw OptionException(string("unknown CNF conversion for --cnf: `") +
-                              optarg + "'.  Try --cnf help.");
-      }
-
-      fputs(cnf_help, stdout);
-      exit(1);
-
     case 'd':
       Debug.on(optarg);
       /* fall-through */
diff --git a/src/main/main.cpp b/src/main/main.cpp
index 2eea56947..1da56b9f9 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -151,7 +151,7 @@ int runCvc4(int argc, char *argv[]) {
   } else {
     string filename = argv[firstArgIndex];
     input = new ifstream(filename.c_str());
-    if(input == NULL) {
+    if(!*input) {
       throw Exception("file does not exist or is unreadable: " + filename);
     }
     parser = Parser::getNewParser(&exprMgr, options.lang, *input, filename);
diff --git a/src/main/util.cpp b/src/main/util.cpp
index adb117b9d..a2b46513d 100644
--- a/src/main/util.cpp
+++ b/src/main/util.cpp
@@ -16,6 +16,7 @@
 #include <cstdio>
 #include <cstdlib>
 #include <cerrno>
+#include <exception>
 #include <string.h>
 #include <signal.h>
 
@@ -63,6 +64,45 @@ void segv_handler(int sig, siginfo_t* info, void*) {
 #endif /* CVC4_DEBUG */
 }
 
+static terminate_handler default_terminator;
+
+void cvc4unexpected() {
+#ifdef CVC4_DEBUG
+  fprintf(stderr,
+          "\n"
+          "CVC4 threw an \"unexpected\" exception (one that wasn't properly specified\n"
+          "in the throws() specifier for the throwing function).\n\n");
+  if(segvNoSpin) {
+    fprintf(stderr, "No-spin requested.\n");
+    set_terminate(default_terminator);
+  } 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 threw an \"unexpected\" exception.\n");
+  set_terminate(default_terminator);
+#endif /* CVC4_DEBUG */
+}
+
+void cvc4terminate() {
+#ifdef CVC4_DEBUG
+  fprintf(stderr,
+          "\n"
+          "CVC4 was terminated by the C++ runtime.\n"
+          "Perhaps an exception was thrown during stack unwinding.  (Don't do that.)\n");
+  default_terminator();
+#else /* CVC4_DEBUG */
+  fprintf(stderr,
+          "CVC4 was terminated by the C++ runtime.\n"
+          "Perhaps an exception was thrown during stack unwinding.\n");
+  default_terminator();
+#endif /* CVC4_DEBUG */
+}
+
 /** Initialize the driver.  Sets signal handlers for SIGINT and SIGSEGV. */
 void cvc4_init() throw() {
   struct sigaction act1;
@@ -78,6 +118,9 @@ void cvc4_init() throw() {
   sigemptyset(&act2.sa_mask);
   if(sigaction(SIGSEGV, &act2, NULL))
     throw Exception(string("sigaction(SIGSEGV) failure: ") + strerror(errno));
+
+  set_unexpected(cvc4unexpected);
+  default_terminator = set_terminate(cvc4terminate);
 }
 
 }/* CVC4::main namespace */