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

diff --git a/src/parser/input.h b/src/parser/input.h
index d47ca4d12..6f30724d1 100644
--- a/src/parser/input.h
+++ b/src/parser/input.h
@@ -29,7 +29,6 @@
 #include "expr/expr.h"
 #include "expr/expr_manager.h"
 #include "parser/parser_exception.h"
-#include "util/Assert.h"
 #include "util/language.h"
 
 namespace CVC4 {
@@ -111,7 +110,7 @@ public:
   static Input* newFileInput(InputLanguage lang,
                              const std::string& filename,
                              bool useMmap = false)
-    throw (InputStreamException, AssertionException);
+    throw (InputStreamException);
 
   /** Create an input for the given stream.
    *
@@ -126,7 +125,7 @@ public:
                                std::istream& input,
                                const std::string& name,
                                bool lineBuffered = false)
-    throw (InputStreamException, AssertionException);
+    throw (InputStreamException);
 
   /** Create an input for the given string
    *
@@ -137,7 +136,7 @@ public:
   static Input* newStringInput(InputLanguage lang,
                                const std::string& input,
                                const std::string& name)
-    throw (InputStreamException, AssertionException);
+    throw (InputStreamException);
 
 
   /** Destructor. Frees the input stream and closes the input. */
@@ -172,7 +171,7 @@ protected:
    * @throws ParserException if an error is encountered during parsing.
    */
   virtual Command* parseCommand()
-    throw (ParserException, TypeCheckingException, AssertionException) = 0;
+    throw (ParserException, TypeCheckingException) = 0;
 
   /**
    * Issue a warning to the user, with source file, line, and column info.
@@ -183,7 +182,7 @@ protected:
    * Throws a <code>ParserException</code> with the given message.
    */
   virtual void parseError(const std::string& msg)
-    throw (ParserException, AssertionException) = 0;
+    throw (ParserException) = 0;
 
   /** Parse an expression from the input by invoking the
    * implementation-specific parsing method. Returns a null
@@ -192,7 +191,7 @@ protected:
    * @throws ParserException if an error is encountered during parsing.
    */
   virtual Expr parseExpr()
-    throw (ParserException, TypeCheckingException, AssertionException) = 0;
+    throw (ParserException, TypeCheckingException) = 0;
 
   /** Set the Parser object for this input. */
   virtual void setParser(Parser& parser) = 0;