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.

3 files changed, 26 insertions, 21 deletions

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 4577b504c..b496aa91c 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -288,7 +288,9 @@ int getOperatorPrecedence(int type) {
   case IN_TOK: return 33;
 
   default:
-    Unhandled(CvcParserTokenNames[type]);
+    std::stringstream ss;
+    ss << "internal error: no entry in precedence table for operator " << CvcParserTokenNames[type];
+    throw ParserException(ss.str());
   }
 }/* getOperatorPrecedence() */
 
@@ -318,16 +320,18 @@ Kind getOperatorKind(int type, bool& negate) {
   case INTDIV_TOK: return kind::INTS_DIVISION;
   case MOD_TOK: return kind::INTS_MODULUS;
   case DIV_TOK: return kind::DIVISION;
-  case EXP_TOK: Unhandled(CvcParserTokenNames[type]);
+  case EXP_TOK: break;
 
     // bvBinop
   case CONCAT_TOK: return kind::BITVECTOR_CONCAT;
   case BAR: return kind::BITVECTOR_OR;
   case BVAND_TOK: return kind::BITVECTOR_AND;
-
-  default:
-    Unhandled(CvcParserTokenNames[type]);
   }
+
+  std::stringstream ss;
+  ss << "internal error: no entry in operator-kind table for operator " << CvcParserTokenNames[type];
+  throw ParserException(ss.str());
+
 }/* getOperatorKind() */
 
 unsigned findPivot(const std::vector<unsigned>& operators,
@@ -355,10 +359,10 @@ Expr createPrecedenceTree(Parser* parser, ExprManager* em,
                           const std::vector<CVC4::Expr>& expressions,
                           const std::vector<unsigned>& operators,
                           unsigned startIndex, unsigned stopIndex) {
-  Assert(expressions.size() == operators.size() + 1);
-  Assert(startIndex < expressions.size());
-  Assert(stopIndex < expressions.size());
-  Assert(startIndex <= stopIndex);
+  assert(expressions.size() == operators.size() + 1);
+  assert(startIndex < expressions.size());
+  assert(stopIndex < expressions.size());
+  assert(startIndex <= stopIndex);
 
   if(stopIndex == startIndex) {
     return expressions[startIndex];
@@ -450,6 +454,7 @@ Expr addNots(ExprManager* em, size_t n, Expr e) {
 @parser::includes {
 
 #include <stdint.h>
+#include <cassert>
 #include "expr/command.h"
 #include "parser/parser.h"
 #include "util/subrange_bound.h"
@@ -1016,7 +1021,7 @@ type[CVC4::Type& t,
     /* a type, possibly a function */
   : restrictedTypePossiblyFunctionLHS[t,check,lhs]
     { if(lhs) {
-        Assert(t.isTuple());
+        assert(t.isTuple());
         args = TupleType(t).getTypes();
       } else {
         args.push_back(t);
@@ -1430,7 +1435,7 @@ arrayStore[CVC4::Expr& f]
 }
   : ( LBRACKET formula[f2] { dims.push_back(f2); } RBRACKET )+
     ASSIGN_TOK uminusTerm[f3]
-    { Assert(dims.size() >= 1);
+    { assert(dims.size() >= 1);
       // these loops are a bit complicated; they're only used for the
       // multidimensional ...WITH [a][b] :=... syntax
       for(unsigned i = 0; i < dims.size() - 1; ++i) {
@@ -1630,7 +1635,7 @@ postfixTerm[CVC4::Expr& f]
         } else if(t.isTester()) {
           f = MK_EXPR(CVC4::kind::APPLY_TESTER, args);
         } else {
-          Unhandled(t);
+          PARSER_STATE->parseError("internal error: unhandled function application kind");
         }
       }
 
@@ -1864,18 +1869,18 @@ simpleTerm[CVC4::Expr& f]
   | INTEGER_LITERAL { f = MK_CONST(AntlrInput::tokenToInteger($INTEGER_LITERAL)); }
     /* bitvector literals */
   | HEX_LITERAL
-    { Assert( AntlrInput::tokenText($HEX_LITERAL).find("0hex") == 0 );
+    { assert( AntlrInput::tokenText($HEX_LITERAL).find("0hex") == 0 );
       std::string hexString = AntlrInput::tokenTextSubstr($HEX_LITERAL, 4);
       f = MK_CONST( BitVector(hexString, 16) ); }
   | BINARY_LITERAL
-    { Assert( AntlrInput::tokenText($BINARY_LITERAL).find("0bin") == 0 );
+    { assert( AntlrInput::tokenText($BINARY_LITERAL).find("0bin") == 0 );
       std::string binString = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 4);
       f = MK_CONST( BitVector(binString, 2) ); }
     /* record literals */
   | PARENHASH recordEntry[name,e] { names.push_back(name); args.push_back(e); }
     ( COMMA recordEntry[name,e] { names.push_back(name); args.push_back(e); } )* HASHPAREN
     { std::vector< std::pair<std::string, Type> > typeIds;
-      Assert(names.size() == args.size());
+      assert(names.size() == args.size());
       for(unsigned i = 0; i < names.size(); ++i) {
         typeIds.push_back(std::make_pair(names[i], args[i].getType()));
       }
diff --git a/src/parser/cvc/cvc_input.cpp b/src/parser/cvc/cvc_input.cpp
index d91a13bee..26ee4a693 100644
--- a/src/parser/cvc/cvc_input.cpp
+++ b/src/parser/cvc/cvc_input.cpp
@@ -32,7 +32,7 @@ namespace parser {
 CvcInput::CvcInput(AntlrInputStream& inputStream) :
   AntlrInput(inputStream,6) {
   pANTLR3_INPUT_STREAM input = inputStream.getAntlr3InputStream();
-  AlwaysAssert( input != NULL );
+  assert( input != NULL );
 
   d_pCvcLexer = CvcLexerNew(input);
   if( d_pCvcLexer == NULL ) {
@@ -42,7 +42,7 @@ CvcInput::CvcInput(AntlrInputStream& inputStream) :
   setAntlr3Lexer( d_pCvcLexer->pLexer );
 
   pANTLR3_COMMON_TOKEN_STREAM tokenStream = getTokenStream();
-  AlwaysAssert( tokenStream != NULL );
+  assert( tokenStream != NULL );
 
   d_pCvcParser = CvcParserNew(tokenStream);
   if( d_pCvcParser == NULL ) {
@@ -59,12 +59,12 @@ CvcInput::~CvcInput() {
 }
 
 Command* CvcInput::parseCommand()
-  throw (ParserException, TypeCheckingException, AssertionException) {
+  throw (ParserException, TypeCheckingException) {
   return d_pCvcParser->parseCommand(d_pCvcParser);
 }
 
 Expr CvcInput::parseExpr()
-  throw (ParserException, TypeCheckingException, AssertionException) {
+  throw (ParserException, TypeCheckingException) {
   return d_pCvcParser->parseExpr(d_pCvcParser);
 }
 
diff --git a/src/parser/cvc/cvc_input.h b/src/parser/cvc/cvc_input.h
index 9a1f24fde..94e1bfc60 100644
--- a/src/parser/cvc/cvc_input.h
+++ b/src/parser/cvc/cvc_input.h
@@ -66,7 +66,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 <code>Expr</code>
    * if there is no expression there to parse.
@@ -74,7 +74,7 @@ protected:
    * @throws ParserException if an error is encountered during parsing.
    */
   Expr parseExpr() 
-    throw(ParserException, TypeCheckingException, AssertionException);
+    throw(ParserException, TypeCheckingException);
 
 private: