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, 16 insertions, 16 deletions

diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp
index 134498eea..7df2b0210 100644
--- a/src/parser/tptp/tptp.cpp
+++ b/src/parser/tptp/tptp.cpp
@@ -83,7 +83,9 @@ void Tptp::addTheory(Theory theory) {
     break;
 
   default:
-    Unhandled(theory);
+    std::stringstream ss;
+    ss << "internal error: Tptp::addTheory(): unhandled theory " << theory;
+    throw ParserException(ss.str());
   }
 }
 
diff --git a/src/parser/tptp/tptp.h b/src/parser/tptp/tptp.h
index 9d75a1d37..6d35cac61 100644
--- a/src/parser/tptp/tptp.h
+++ b/src/parser/tptp/tptp.h
@@ -24,6 +24,7 @@
 #include "parser/parser.h"
 #include "expr/command.h"
 #include <ext/hash_set>
+#include <cassert>
 
 namespace CVC4 {
 
@@ -52,9 +53,9 @@ class Tptp : public Parser {
 public:
   bool cnf; //in a cnf formula
 
-  void addFreeVar(Expr var){Assert(cnf); d_freeVar.push_back(var); };
+  void addFreeVar(Expr var){assert(cnf); d_freeVar.push_back(var); };
   std::vector< Expr > getFreeVar(){
-    Assert(cnf);
+    assert(cnf);
     std::vector< Expr > r;
     r.swap(d_freeVar);
     return r;
@@ -212,22 +213,19 @@ inline Command* Tptp::makeCommand(FormulaRole fr, Expr & expr){
   case FR_PLAIN:
     // it's a usual assert
     return new AssertCommand(expr);
-    break;
   case FR_CONJECTURE:
     // something to prove
     return new AssertCommand(getExprManager()->mkExpr(kind::NOT,expr));
-    break;
   case FR_UNKNOWN:
   case FR_FI_DOMAIN:
   case FR_FI_FUNCTORS:
   case FR_FI_PREDICATES:
   case FR_TYPE:
     return new EmptyCommand("Untreated role");
-    break;
-  default:
-    Unreachable("fr",fr);
-  };
-};
+  }
+  assert(false);// unreachable
+  return NULL;
+}
 
 namespace tptp {
 /**
diff --git a/src/parser/tptp/tptp_input.cpp b/src/parser/tptp/tptp_input.cpp
index 689f13a8b..8d41a5b68 100644
--- a/src/parser/tptp/tptp_input.cpp
+++ b/src/parser/tptp/tptp_input.cpp
@@ -34,7 +34,7 @@ namespace parser {
 TptpInput::TptpInput(AntlrInputStream& inputStream) :
   AntlrInput(inputStream, 1) {
   pANTLR3_INPUT_STREAM input = inputStream.getAntlr3InputStream();
-  AlwaysAssert( input != NULL );
+  assert( input != NULL );
 
   d_pTptpLexer = TptpLexerNew(input);
   if( d_pTptpLexer == NULL ) {
@@ -44,7 +44,7 @@ TptpInput::TptpInput(AntlrInputStream& inputStream) :
   setAntlr3Lexer( d_pTptpLexer->pLexer );
 
   pANTLR3_COMMON_TOKEN_STREAM tokenStream = getTokenStream();
-  AlwaysAssert( tokenStream != NULL );
+  assert( tokenStream != NULL );
 
   d_pTptpParser = TptpParserNew(tokenStream);
   if( d_pTptpParser == NULL ) {
@@ -61,12 +61,12 @@ TptpInput::~TptpInput() {
 }
 
 Command* TptpInput::parseCommand()
-  throw (ParserException, TypeCheckingException, AssertionException) {
+  throw (ParserException, TypeCheckingException) {
   return d_pTptpParser->parseCommand(d_pTptpParser);
 }
 
 Expr TptpInput::parseExpr()
-  throw (ParserException, TypeCheckingException, AssertionException) {
+  throw (ParserException, TypeCheckingException) {
   return d_pTptpParser->parseExpr(d_pTptpParser);
 }
 
diff --git a/src/parser/tptp/tptp_input.h b/src/parser/tptp/tptp_input.h
index 7977117d0..32d3efad1 100644
--- a/src/parser/tptp/tptp_input.h
+++ b/src/parser/tptp/tptp_input.h
@@ -78,7 +78,7 @@ protected:
    * @throws ParserException if an error is encountered during parsing.
    */
   Command* parseCommand()
-    throw(ParserException, TypeCheckingException, AssertionException);
+    throw(ParserException, TypeCheckingException);
 
   /**
    * Parse an expression from the input. Returns a null
@@ -87,7 +87,7 @@ protected:
    * @throws ParserException if an error is encountered during parsing.
    */
   Expr parseExpr()
-    throw(ParserException, TypeCheckingException, AssertionException);
+    throw(ParserException, TypeCheckingException);
 
 };/* class TptpInput */