Public interface review items:

* Internal uses of CheckArgument changed to AssertArgument/AlwaysAssertArgument()
* Make util/Assert.h cvc4_private instead of public, so AssertionException and friends are now internal-only
* CheckArgument() throws non-AssertionException
* things outside the core library (parsers, driver) use regular C-style assert,
  or a public exception type.
* auto-generated documentation for Smt options and internal options

Also, a small fix to SMT-LIBv1 QF_ABV and QF_AUFBV definitions, which were nonstandard.

4 files changed, 13 insertions, 7 deletions

diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index a3086d96c..3eba7ff6a 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -33,7 +33,6 @@
 #include "parser/parser_exception.h"
 #include "expr/expr_manager.h"
 #include "expr/command.h"
-#include "util/Assert.h"
 #include "util/configuration.h"
 #include "options/options.h"
 #include "main/command_executor.h"
diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index 719c8f61d..4f75779af 100644
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -37,6 +37,7 @@
 #include "util/language.h"
 
 #include <string.h>
+#include <cassert>
 
 #if HAVE_LIBREADLINE
 #  include <readline/readline.h>
@@ -121,7 +122,9 @@ InteractiveShell::InteractiveShell(ExprManager& exprManager,
       commandsEnd = tptp_commands + sizeof(tptp_commands) / sizeof(*tptp_commands);
       break;
     default:
-      Unhandled(lang);
+      std::stringstream ss;
+      ss << "internal error: unhandled language " << lang;
+      throw Exception(ss.str());
     }
     d_usingReadline = true;
     int err = ::read_history(d_historyFilename.c_str());
@@ -195,12 +198,12 @@ Command* InteractiveShell::readCommand() {
   while(true) {
     Debug("interactive") << "Input now '" << input << line << "'" << endl << flush;
 
-    Assert( !(d_in.fail() && !d_in.eof()) || line.empty() );
+    assert( !(d_in.fail() && !d_in.eof()) || line.empty() );
 
     /* Check for failure. */
     if(d_in.fail() && !d_in.eof()) {
       /* This should only happen if the input line was empty. */
-      Assert( line.empty() );
+      assert( line.empty() );
       d_in.clear();
     }
 
@@ -229,7 +232,7 @@ Command* InteractiveShell::readCommand() {
     if(!d_usingReadline) {
       /* Extract the newline delimiter from the stream too */
       int c CVC4_UNUSED = d_in.get();
-      Assert( c == '\n' );
+      assert( c == '\n' );
       Debug("interactive") << "Next char is '" << (char)c << "'" << endl << flush;
     }
 
diff --git a/src/main/main.cpp b/src/main/main.cpp
index 73936526f..e3196bb4e 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -33,7 +33,6 @@
 #include "expr/expr_manager.h"
 #include "smt/smt_engine.h"
 #include "expr/command.h"
-#include "util/Assert.h"
 #include "util/configuration.h"
 #include "main/options.h"
 #include "theory/uf/options.h"
diff --git a/src/main/util.cpp b/src/main/util.cpp
index 523486f80..90e960673 100644
--- a/src/main/util.cpp
+++ b/src/main/util.cpp
@@ -25,10 +25,10 @@
 #include <sys/resource.h>
 #include <unistd.h>
 
-#include "util/Assert.h"
 #include "util/exception.h"
 #include "options/options.h"
 #include "util/statistics.h"
+#include "util/tls.h"
 #include "smt/smt_engine.h"
 
 #include "cvc4autoconfig.h"
@@ -39,6 +39,11 @@ using CVC4::Exception;
 using namespace std;
 
 namespace CVC4 {
+
+#ifdef CVC4_DEBUG
+  extern CVC4_THREADLOCAL(const char*) s_debugLastException;
+#endif /* CVC4_DEBUG */
+
 namespace main {
 
 size_t cvc4StackSize;