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, 1 insertions, 4 deletions

diff --git a/src/util/cardinality.h b/src/util/cardinality.h
index 81a291006..17368c157 100644
--- a/src/util/cardinality.h
+++ b/src/util/cardinality.h
@@ -26,7 +26,7 @@
 #include <utility>
 
 #include "util/integer.h"
-#include "util/Assert.h"
+#include "util/exception.h"
 
 namespace CVC4 {
 
@@ -118,7 +118,6 @@ public:
     CheckArgument(card >= 0, card,
                   "Cardinality must be a nonnegative integer, not %ld.", card);
     d_card += 1;
-    Assert(isFinite());
   }
 
   /**
@@ -130,14 +129,12 @@ public:
                   "Cardinality must be a nonnegative integer, not %s.",
                   card.toString().c_str());
     d_card += 1;
-    Assert(isFinite());
   }
 
   /**
    * Construct an infinite cardinality equal to the given Beth number.
    */
   Cardinality(CardinalityBeth beth) : d_card(-beth.getNumber() - 1) {
-    Assert(!isFinite());
   }
 
   /**