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

diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h
index 5b6468a9e..66428ec41 100644
--- a/src/util/integer_gmp_imp.h
+++ b/src/util/integer_gmp_imp.h
@@ -25,8 +25,8 @@
 #include <string>
 #include <iostream>
 
-#include "util/Assert.h"
 #include "util/gmp_util.h"
+#include "util/exception.h"
 
 namespace CVC4 {
 
@@ -178,7 +178,7 @@ public:
    */
   Integer oneExtend(uint32_t size, uint32_t amount) const {
     // check that the size is accurate
-    Assert ((*this) < Integer(1).multiplyByPow2(size));
+    DebugCheckArgument((*this) < Integer(1).multiplyByPow2(size), size);
     mpz_class res = d_value;
 
     for (unsigned i = size; i < size + amount; ++i) {
@@ -251,7 +251,7 @@ public:
    * If y divides *this, then exactQuotient returns (this/y)
    */
   Integer exactQuotient(const Integer& y) const {
-    Assert(y.divides(*this));
+    DebugCheckArgument(y.divides(*this), y);
     mpz_class q;
     mpz_divexact(q.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
     return Integer( q );
@@ -346,15 +346,15 @@ public:
   long getLong() const {
     long si = d_value.get_si();
     // ensure there wasn't overflow
-    AlwaysAssert(mpz_cmp_si(d_value.get_mpz_t(), si) == 0,
+    CheckArgument(mpz_cmp_si(d_value.get_mpz_t(), si) == 0, this,
                  "Overflow detected in Integer::getLong()");
     return si;
   }
   unsigned long getUnsignedLong() const {
     unsigned long ui = d_value.get_ui();
     // ensure there wasn't overflow
-    AlwaysAssert(mpz_cmp_ui(d_value.get_mpz_t(), ui) == 0,
-                 "Overflow detected in Integer::getUnsignedLong()");
+    CheckArgument(mpz_cmp_ui(d_value.get_mpz_t(), ui) == 0, this,
+                  "Overflow detected in Integer::getUnsignedLong()");
     return ui;
   }