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

diff --git a/src/util/result.h b/src/util/result.h
index f0cf3f20e..0894007bc 100644
--- a/src/util/result.h
+++ b/src/util/result.h
@@ -24,16 +24,10 @@
 #include <iostream>
 #include <string>
 
-#include "util/Assert.h"
+#include "util/exception.h"
 
 namespace CVC4 {
 
-// TODO: either templatize Result on its Kind (Sat/Validity) or subclass.
-// TODO: INVALID/SAT provide models, etc?---perhaps just by linking back
-// into the SmtEngine that produced the Result?
-// TODO: make unconstructible except by SmtEngine?  That would ensure that
-// any Result in the system is bona fide.
-
 class Result;
 
 std::ostream& operator<<(std::ostream& out, const Result& r) CVC4_PUBLIC;
@@ -137,9 +131,9 @@ public:
     return d_which == TYPE_NONE;
   }
   enum UnknownExplanation whyUnknown() const {
-    AlwaysAssert( isUnknown(),
-                  "This result is not unknown, so the reason for "
-                  "being unknown cannot be inquired of it" );
+    CheckArgument( isUnknown(), this,
+                   "This result is not unknown, so the reason for "
+                   "being unknown cannot be inquired of it" );
     return d_unknownExplanation;
   }