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, 9 deletions

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 {
 /**