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, 3 insertions, 2 deletions

diff --git a/src/util/rational_cln_imp.h b/src/util/rational_cln_imp.h
index 182e813cd..575f09ef5 100644
--- a/src/util/rational_cln_imp.h
+++ b/src/util/rational_cln_imp.h
@@ -25,6 +25,7 @@
 #include <gmp.h>
 #include <string>
 #include <sstream>
+#include <cassert>
 #include <cln/rational.h>
 #include <cln/input.h>
 #include <cln/io.h>
@@ -32,7 +33,7 @@
 #include <cln/rational_io.h>
 #include <cln/number_io.h>
 
-#include "util/Assert.h"
+#include "util/exception.h"
 #include "util/integer.h"
 
 namespace CVC4 {
@@ -213,7 +214,7 @@ public:
     }else if(cln::minusp(d_value)){
        return -1;
     }else{
-      Assert(cln::plusp(d_value));
+      assert(cln::plusp(d_value));
       return 1;
     }
   }