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.

1 files changed, 7 insertions, 4 deletions

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