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.

8 files changed, 43 insertions, 50 deletions

diff --git a/test/unit/expr/expr_manager_public.h b/test/unit/expr/expr_manager_public.h
index e709648c9..e0ebe9640 100644
--- a/test/unit/expr/expr_manager_public.h
+++ b/test/unit/expr/expr_manager_public.h
@@ -23,7 +23,6 @@
 
 #include "expr/expr_manager.h"
 #include "expr/expr.h"
-#include "util/Assert.h"
 #include "util/exception.h"
 
 using namespace CVC4;
@@ -120,12 +119,12 @@ public:
 
   void testMkAssociativeTooFew() {
     std::vector<Expr> vars = mkVars(d_exprManager->booleanType(), 1);
-    TS_ASSERT_THROWS( d_exprManager->mkAssociative(AND,vars), AssertionException);
+    TS_ASSERT_THROWS( d_exprManager->mkAssociative(AND,vars), IllegalArgumentException);
   }
 
   void testMkAssociativeBadKind() {
     std::vector<Expr> vars = mkVars(d_exprManager->integerType(), 10);
-    TS_ASSERT_THROWS( d_exprManager->mkAssociative(TUPLE,vars), AssertionException);
+    TS_ASSERT_THROWS( d_exprManager->mkAssociative(TUPLE,vars), IllegalArgumentException);
   }
 
 };
diff --git a/test/unit/expr/expr_public.h b/test/unit/expr/expr_public.h
index 279d4bebe..0d7608cac 100644
--- a/test/unit/expr/expr_public.h
+++ b/test/unit/expr/expr_public.h
@@ -23,7 +23,6 @@
 
 #include "expr/expr_manager.h"
 #include "expr/expr.h"
-#include "util/Assert.h"
 #include "util/exception.h"
 
 using namespace CVC4;
diff --git a/test/unit/expr/kind_map_black.h b/test/unit/expr/kind_map_black.h
index e5bcdd298..b994bd3af 100644
--- a/test/unit/expr/kind_map_black.h
+++ b/test/unit/expr/kind_map_black.h
@@ -102,7 +102,7 @@ public:
     TS_ASSERT(!(AND ^ AND ^ AND).isEmpty());
 
 #ifdef CVC4_ASSERTIONS
-    TS_ASSERT_THROWS(~LAST_KIND, IllegalArgumentException);
+    TS_ASSERT_THROWS(~LAST_KIND, AssertArgumentException);
 #endif /* CVC4_ASSERTIONS */
   }
 
diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h
index 1518efadf..1a5f5ecfa 100644
--- a/test/unit/expr/node_black.h
+++ b/test/unit/expr/node_black.h
@@ -427,8 +427,8 @@ public:
 
     TS_ASSERT( f == fa.getOperator() );
 #ifdef CVC4_ASSERTIONS
-    TS_ASSERT_THROWS( f.getOperator(), AssertionException );
-    TS_ASSERT_THROWS( a.getOperator(), AssertionException );
+    TS_ASSERT_THROWS( f.getOperator(), IllegalArgumentException );
+    TS_ASSERT_THROWS( a.getOperator(), IllegalArgumentException );
 #endif /* CVC4_ASSERTIONS */
   }
 
diff --git a/test/unit/expr/type_cardinality_public.h b/test/unit/expr/type_cardinality_public.h
index 7ba212dd5..78a872aea 100644
--- a/test/unit/expr/type_cardinality_public.h
+++ b/test/unit/expr/type_cardinality_public.h
@@ -26,7 +26,6 @@
 #include "expr/type.h"
 #include "expr/expr_manager.h"
 #include "util/cardinality.h"
-#include "util/Assert.h"
 
 using namespace CVC4;
 using namespace CVC4::kind;
diff --git a/test/unit/theory/logic_info_white.h b/test/unit/theory/logic_info_white.h
index a2f61f5d2..c091eab71 100644
--- a/test/unit/theory/logic_info_white.h
+++ b/test/unit/theory/logic_info_white.h
@@ -450,31 +450,29 @@ public:
     LogicInfo info;
     TS_ASSERT( !info.isLocked() );
 
-#ifdef CVC4_ASSERTIONS
-    TS_ASSERT_THROWS( info.getLogicString(), CVC4::AssertionException );
-    TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_BUILTIN ), CVC4::AssertionException );
-    TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_BOOL ), CVC4::AssertionException );
-    TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_UF ), CVC4::AssertionException );
-    TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_ARITH ), CVC4::AssertionException );
-    TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_ARRAY ), CVC4::AssertionException );
-    TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_BV ), CVC4::AssertionException );
-    TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_DATATYPES ), CVC4::AssertionException );
-    TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_QUANTIFIERS ), CVC4::AssertionException );
-    TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_REWRITERULES ), CVC4::AssertionException );
-    TS_ASSERT_THROWS( ! info.isPure( THEORY_BUILTIN ), CVC4::AssertionException );
-    TS_ASSERT_THROWS( ! info.isPure( THEORY_BOOL ), CVC4::AssertionException );
-    TS_ASSERT_THROWS( ! info.isPure( THEORY_UF ), CVC4::AssertionException );
-    TS_ASSERT_THROWS( ! info.isPure( THEORY_ARITH ), CVC4::AssertionException );
-    TS_ASSERT_THROWS( ! info.isPure( THEORY_ARRAY ), CVC4::AssertionException );
-    TS_ASSERT_THROWS( ! info.isPure( THEORY_BV ), CVC4::AssertionException );
-    TS_ASSERT_THROWS( ! info.isPure( THEORY_DATATYPES ), CVC4::AssertionException );
-    TS_ASSERT_THROWS( ! info.isPure( THEORY_QUANTIFIERS ), CVC4::AssertionException );
-    TS_ASSERT_THROWS( ! info.isPure( THEORY_REWRITERULES ), CVC4::AssertionException );
-    TS_ASSERT_THROWS( info.isQuantified(), CVC4::AssertionException );
-    TS_ASSERT_THROWS( info.areIntegersUsed(), CVC4::AssertionException );
-    TS_ASSERT_THROWS( info.areRealsUsed(), CVC4::AssertionException );
-    TS_ASSERT_THROWS( ! info.isLinear(), CVC4::AssertionException );
-#endif /* CVC4_ASSERTIONS */
+    TS_ASSERT_THROWS( info.getLogicString(), CVC4::IllegalArgumentException );
+    TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_BUILTIN ), CVC4::IllegalArgumentException );
+    TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_BOOL ), CVC4::IllegalArgumentException );
+    TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_UF ), CVC4::IllegalArgumentException );
+    TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_ARITH ), CVC4::IllegalArgumentException );
+    TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_ARRAY ), CVC4::IllegalArgumentException );
+    TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_BV ), CVC4::IllegalArgumentException );
+    TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_DATATYPES ), CVC4::IllegalArgumentException );
+    TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_QUANTIFIERS ), CVC4::IllegalArgumentException );
+    TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_REWRITERULES ), CVC4::IllegalArgumentException );
+    TS_ASSERT_THROWS( ! info.isPure( THEORY_BUILTIN ), CVC4::IllegalArgumentException );
+    TS_ASSERT_THROWS( ! info.isPure( THEORY_BOOL ), CVC4::IllegalArgumentException );
+    TS_ASSERT_THROWS( ! info.isPure( THEORY_UF ), CVC4::IllegalArgumentException );
+    TS_ASSERT_THROWS( ! info.isPure( THEORY_ARITH ), CVC4::IllegalArgumentException );
+    TS_ASSERT_THROWS( ! info.isPure( THEORY_ARRAY ), CVC4::IllegalArgumentException );
+    TS_ASSERT_THROWS( ! info.isPure( THEORY_BV ), CVC4::IllegalArgumentException );
+    TS_ASSERT_THROWS( ! info.isPure( THEORY_DATATYPES ), CVC4::IllegalArgumentException );
+    TS_ASSERT_THROWS( ! info.isPure( THEORY_QUANTIFIERS ), CVC4::IllegalArgumentException );
+    TS_ASSERT_THROWS( ! info.isPure( THEORY_REWRITERULES ), CVC4::IllegalArgumentException );
+    TS_ASSERT_THROWS( info.isQuantified(), CVC4::IllegalArgumentException );
+    TS_ASSERT_THROWS( info.areIntegersUsed(), CVC4::IllegalArgumentException );
+    TS_ASSERT_THROWS( info.areRealsUsed(), CVC4::IllegalArgumentException );
+    TS_ASSERT_THROWS( ! info.isLinear(), CVC4::IllegalArgumentException );
 
     info.lock();
     TS_ASSERT( info.isLocked() );
@@ -503,17 +501,15 @@ public:
     TS_ASSERT( info.areRealsUsed() );
     TS_ASSERT( ! info.isLinear() );
 
-#ifdef CVC4_ASSERTIONS
-    TS_ASSERT_THROWS( info.arithOnlyLinear(), CVC4::AssertionException );
-    TS_ASSERT_THROWS( info.disableIntegers(), CVC4::AssertionException );
-    TS_ASSERT_THROWS( info.disableQuantifiers(), CVC4::AssertionException );
-    TS_ASSERT_THROWS( info.disableTheory(THEORY_BV), CVC4::AssertionException );
-    TS_ASSERT_THROWS( info.disableTheory(THEORY_DATATYPES), CVC4::AssertionException );
-    TS_ASSERT_THROWS( info.enableIntegers(), CVC4::AssertionException );
-    TS_ASSERT_THROWS( info.disableReals(), CVC4::AssertionException );
-    TS_ASSERT_THROWS( info.disableTheory(THEORY_ARITH), CVC4::AssertionException );
-    TS_ASSERT_THROWS( info.disableTheory(THEORY_UF), CVC4::AssertionException );
-#endif /* CVC4_ASSERTIONS */
+    TS_ASSERT_THROWS( info.arithOnlyLinear(), CVC4::IllegalArgumentException );
+    TS_ASSERT_THROWS( info.disableIntegers(), CVC4::IllegalArgumentException );
+    TS_ASSERT_THROWS( info.disableQuantifiers(), CVC4::IllegalArgumentException );
+    TS_ASSERT_THROWS( info.disableTheory(THEORY_BV), CVC4::IllegalArgumentException );
+    TS_ASSERT_THROWS( info.disableTheory(THEORY_DATATYPES), CVC4::IllegalArgumentException );
+    TS_ASSERT_THROWS( info.enableIntegers(), CVC4::IllegalArgumentException );
+    TS_ASSERT_THROWS( info.disableReals(), CVC4::IllegalArgumentException );
+    TS_ASSERT_THROWS( info.disableTheory(THEORY_ARITH), CVC4::IllegalArgumentException );
+    TS_ASSERT_THROWS( info.disableTheory(THEORY_UF), CVC4::IllegalArgumentException );
 
     info = info.getUnlockedCopy();
     TS_ASSERT( !info.isLocked() );
diff --git a/test/unit/util/assert_white.h b/test/unit/util/assert_white.h
index 6d88f89bd..54c77b165 100644
--- a/test/unit/util/assert_white.h
+++ b/test/unit/util/assert_white.h
@@ -32,7 +32,7 @@ public:
   void testAssert() {
 #ifdef CVC4_ASSERTIONS
     TS_ASSERT_THROWS( Assert(false), AssertionException );
-    TS_ASSERT_THROWS( AssertArgument(false, "x"), IllegalArgumentException );
+    TS_ASSERT_THROWS( AssertArgument(false, "x"), AssertArgumentException );
 #else /* CVC4_ASSERTIONS */
     TS_ASSERT_THROWS_NOTHING( Assert(false) );
     TS_ASSERT_THROWS_NOTHING( AssertArgument(false, "x") );
@@ -46,7 +46,7 @@ public:
     TS_ASSERT_THROWS( IllegalArgument("x"), IllegalArgumentException );
     TS_ASSERT_THROWS( CheckArgument(false, "x"), IllegalArgumentException );
     TS_ASSERT_THROWS( AlwaysAssertArgument(false, "x"),
-                      IllegalArgumentException );
+                      AssertArgumentException );
     TS_ASSERT_THROWS_NOTHING( AssertArgument(true, "x") );
     TS_ASSERT_THROWS_NOTHING( AssertArgument(true, "x") );
   }
diff --git a/test/unit/util/boolean_simplification_black.h b/test/unit/util/boolean_simplification_black.h
index 8f2d0d97f..e333e7205 100644
--- a/test/unit/util/boolean_simplification_black.h
+++ b/test/unit/util/boolean_simplification_black.h
@@ -135,7 +135,7 @@ public:
 
 #ifdef CVC4_ASSERTIONS
     in = Node();
-    TS_ASSERT_THROWS( BooleanSimplification::negate(in), IllegalArgumentException );
+    TS_ASSERT_THROWS( BooleanSimplification::negate(in), AssertArgumentException );
 #endif /* CVC4_ASSERTIONS */
   }
 
@@ -170,7 +170,7 @@ public:
 
 #ifdef CVC4_ASSERTIONS
     in = d_nm->mkNode(kind::AND, a, b);
-    TS_ASSERT_THROWS( BooleanSimplification::simplifyClause(in), IllegalArgumentException );
+    TS_ASSERT_THROWS( BooleanSimplification::simplifyClause(in), AssertArgumentException );
 #endif /* CVC4_ASSERTIONS */
   }
 
@@ -195,7 +195,7 @@ public:
 
 #ifdef CVC4_ASSERTIONS
     in = d_nm->mkNode(kind::OR, a, b);
-    TS_ASSERT_THROWS( BooleanSimplification::simplifyHornClause(in), IllegalArgumentException );
+    TS_ASSERT_THROWS( BooleanSimplification::simplifyHornClause(in), AssertArgumentException );
 #endif /* CVC4_ASSERTIONS */
   }
 
@@ -216,7 +216,7 @@ public:
 
 #ifdef CVC4_ASSERTIONS
     in = d_nm->mkNode(kind::OR, a, b);
-    TS_ASSERT_THROWS( BooleanSimplification::simplifyConflict(in), IllegalArgumentException );
+    TS_ASSERT_THROWS( BooleanSimplification::simplifyConflict(in), AssertArgumentException );
 #endif /* CVC4_ASSERTIONS */
   }