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

diff --git a/src/util/sexpr.h b/src/util/sexpr.h
index 4feffc18f..345a6c132 100644
--- a/src/util/sexpr.h
+++ b/src/util/sexpr.h
@@ -28,7 +28,7 @@
 
 #include "util/integer.h"
 #include "util/rational.h"
-#include "util/Assert.h"
+#include "util/exception.h"
 
 namespace CVC4 {
 
@@ -182,7 +182,7 @@ inline bool SExpr::isKeyword() const {
 }
 
 inline std::string SExpr::getValue() const {
-  AlwaysAssert( isAtom() );
+  CheckArgument( isAtom(), this );
   switch(d_sexprType) {
   case SEXPR_INTEGER:
     return d_integerValue.toString();
@@ -198,24 +198,24 @@ inline std::string SExpr::getValue() const {
   case SEXPR_STRING:
   case SEXPR_KEYWORD:
     return d_stringValue;
-  default:
-    Unhandled(d_sexprType);
+  case SEXPR_NOT_ATOM:
+    return std::string();
   }
-  return d_stringValue;
+  return std::string();
 }
 
 inline const CVC4::Integer& SExpr::getIntegerValue() const {
-  AlwaysAssert( isInteger() );
+  CheckArgument( isInteger(), this );
   return d_integerValue;
 }
 
 inline const CVC4::Rational& SExpr::getRationalValue() const {
-  AlwaysAssert( isRational() );
+  CheckArgument( isRational(), this );
   return d_rationalValue;
 }
 
 inline const std::vector<SExpr>& SExpr::getChildren() const {
-  AlwaysAssert( !isAtom() );
+  CheckArgument( !isAtom(), this );
   return d_children;
 }