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.

3 files changed, 29 insertions, 26 deletions

diff --git a/src/smt/options b/src/smt/options
index 24c8b5e43..f82867b68 100644
--- a/src/smt/options
+++ b/src/smt/options
@@ -81,4 +81,7 @@ option lemmaInputChannel LemmaInputChannel* :default NULL :include "util/lemma_i
 option lemmaOutputChannel LemmaOutputChannel* :default NULL :include "util/lemma_output_channel.h"
  The output channel to receive notfication events for new lemmas
 
+option optionWithOnlyAlternate /--optionWithOnlyAlternate bool
+ option with only an alternate
+
 endmodule
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 2db746c0a..b968da2e0 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -250,7 +250,7 @@ class SmtEnginePrivate : public NodeManagerListener {
    * to be in that type.
    */
   void constrainSubtypes(TNode n, std::vector<Node>& assertions)
-    throw(AssertionException);
+    throw();
 
   /**
    * Perform non-clausal simplification of a Node.  This involves
@@ -259,7 +259,7 @@ class SmtEnginePrivate : public NodeManagerListener {
    *
    * Returns false if the formula simplifies to "false"
    */
-  bool simplifyAssertions() throw(TypeCheckingException, AssertionException);
+  bool simplifyAssertions() throw(TypeCheckingException);
 
 public:
 
@@ -344,13 +344,13 @@ public:
    * even be simplified.
    */
   void addFormula(TNode n)
-    throw(TypeCheckingException, AssertionException);
+    throw(TypeCheckingException);
 
   /**
    * Expand definitions in n.
    */
   Node expandDefinitions(TNode n, hash_map<Node, Node, NodeHashFunction>& cache)
-    throw(TypeCheckingException, AssertionException);
+    throw(TypeCheckingException);
 
 };/* class SmtEnginePrivate */
 
@@ -358,7 +358,7 @@ public:
 
 using namespace CVC4::smt;
 
-SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) :
+SmtEngine::SmtEngine(ExprManager* em) throw() :
   d_context(em->getContext()),
   d_userLevels(),
   d_userContext(new UserContext()),
@@ -571,7 +571,7 @@ void SmtEngine::setLogic(const std::string& s) throw(ModalException) {
 // tempt people in the code to use the (potentially unlocked)
 // version that's passed in, leading to assert-fails in certain
 // uses of the CVC4 library.
-void SmtEngine::setLogicInternal() throw(AssertionException) {
+void SmtEngine::setLogicInternal() throw() {
   Assert(!d_fullyInited, "setting logic in SmtEngine but the engine has already finished initializing for this run");
 
   d_logic.lock();
@@ -926,7 +926,7 @@ void SmtEngine::defineFunction(Expr func,
 }
 
 Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashFunction>& cache)
-  throw(TypeCheckingException, AssertionException) {
+  throw(TypeCheckingException) {
 
   if(n.getKind() != kind::APPLY && n.getNumChildren() == 0) {
     // don't bother putting in the cache
@@ -1315,7 +1315,7 @@ void SmtEnginePrivate::unconstrainedSimp() {
 
 
 void SmtEnginePrivate::constrainSubtypes(TNode top, std::vector<Node>& assertions)
-  throw(AssertionException) {
+  throw() {
 
   Trace("constrainSubtypes") << "constrainSubtypes(): looking at " << top << endl;
 
@@ -1373,7 +1373,7 @@ void SmtEnginePrivate::constrainSubtypes(TNode top, std::vector<Node>& assertion
 
 // returns false if simpflication led to "false"
 bool SmtEnginePrivate::simplifyAssertions()
-  throw(TypeCheckingException, AssertionException) {
+  throw(TypeCheckingException) {
   Assert(d_smt.d_pendingPops == 0);
   try {
 
@@ -1660,7 +1660,7 @@ void SmtEnginePrivate::processAssertions() {
 }
 
 void SmtEnginePrivate::addFormula(TNode n)
-  throw(TypeCheckingException, AssertionException) {
+  throw(TypeCheckingException) {
 
   Trace("smt") << "SmtEnginePrivate::addFormula(" << n << ")" << endl;
 
@@ -1865,7 +1865,7 @@ Expr SmtEngine::expandDefinitions(const Expr& e) throw(TypeCheckingException) {
 }
 
 Expr SmtEngine::getValue(const Expr& e)
-  throw(ModalException, AssertionException) {
+  throw(ModalException) {
   Assert(e.getExprManager() == d_exprManager);
   SmtScope smts(this);
 
@@ -1906,7 +1906,7 @@ Expr SmtEngine::getValue(const Expr& e)
   return Expr(d_exprManager, new Node(resultNode));
 }
 
-bool SmtEngine::addToAssignment(const Expr& e) throw(AssertionException) {
+bool SmtEngine::addToAssignment(const Expr& e) throw() {
   SmtScope smts(this);
   finalOptionsAreSet();
   doPendingPops();
@@ -1935,7 +1935,7 @@ bool SmtEngine::addToAssignment(const Expr& e) throw(AssertionException) {
   return true;
 }
 
-CVC4::SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) {
+CVC4::SExpr SmtEngine::getAssignment() throw(ModalException) {
   Trace("smt") << "SMT getAssignment()" << endl;
   SmtScope smts(this);
   finalOptionsAreSet();
@@ -2014,7 +2014,7 @@ void SmtEngine::addToModelCommand(Command* c) {
   }
 }
 
-Model* SmtEngine::getModel() throw(ModalException, AssertionException) {
+Model* SmtEngine::getModel() throw(ModalException) {
   Trace("smt") << "SMT getModel()" << endl;
   SmtScope smts(this);
 
@@ -2040,7 +2040,7 @@ Model* SmtEngine::getModel() throw(ModalException, AssertionException) {
   return d_theoryEngine->getModel();
 }
 
-void SmtEngine::checkModel() throw(InternalErrorException) {
+void SmtEngine::checkModel() {
   // --check-model implies --interactive, which enables the assertion list,
   // so we should be ok.
   Assert(d_assertionList != NULL, "don't have an assertion list to check in SmtEngine::checkModel()");
@@ -2157,7 +2157,7 @@ void SmtEngine::checkModel() throw(InternalErrorException) {
   Notice() << "SmtEngine::checkModel(): all assertions checked out OK !" << endl;
 }
 
-Proof* SmtEngine::getProof() throw(ModalException, AssertionException) {
+Proof* SmtEngine::getProof() throw(ModalException) {
   Trace("smt") << "SMT getProof()" << endl;
   SmtScope smts(this);
   finalOptionsAreSet();
@@ -2185,7 +2185,7 @@ Proof* SmtEngine::getProof() throw(ModalException, AssertionException) {
 }
 
 vector<Expr> SmtEngine::getAssertions()
-  throw(ModalException, AssertionException) {
+  throw(ModalException) {
   SmtScope smts(this);
   finalOptionsAreSet();
   if(Dump.isOn("benchmark")) {
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 0214cddd3..e906863ad 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -219,7 +219,7 @@ class CVC4_PUBLIC SmtEngine {
    * Check that a generated Model (via getModel()) actually satisfies
    * all user assertions.
    */
-  void checkModel() throw(InternalErrorException);
+  void checkModel();
 
   /**
    * This is something of an "init" procedure, but is idempotent; call
@@ -275,7 +275,7 @@ class CVC4_PUBLIC SmtEngine {
    * Internally handle the setting of a logic.  This function should always
    * be called when d_logic is updated.
    */
-  void setLogicInternal() throw(AssertionException);
+  void setLogicInternal() throw();
 
   friend class ::CVC4::smt::SmtEnginePrivate;
   friend class ::CVC4::smt::SmtScope;
@@ -300,7 +300,7 @@ public:
   /**
    * Construct an SmtEngine with the given expression manager.
    */
-  SmtEngine(ExprManager* em) throw(AssertionException);
+  SmtEngine(ExprManager* em) throw();
 
   /**
    * Destruct the SMT engine.
@@ -394,7 +394,7 @@ public:
    * by a SAT or INVALID query).  Only permitted if the SmtEngine is
    * set to operate interactively and produce-models is on.
    */
-  Expr getValue(const Expr& e) throw(ModalException, AssertionException);
+  Expr getValue(const Expr& e) throw(ModalException);
 
   /**
    * Add a function to the set of expressions whose value is to be
@@ -405,34 +405,34 @@ public:
    * this function returns true if the expression was added and false
    * if this request was ignored.
    */
-  bool addToAssignment(const Expr& e) throw(AssertionException);
+  bool addToAssignment(const Expr& e) throw();
 
   /**
    * Get the assignment (only if immediately preceded by a SAT or
    * INVALID query).  Only permitted if the SmtEngine is set to
    * operate interactively and produce-assignments is on.
    */
-  CVC4::SExpr getAssignment() throw(ModalException, AssertionException);
+  CVC4::SExpr getAssignment() throw(ModalException);
 
   /**
    * Get the model (only if immediately preceded by a SAT
    * or INVALID query).  Only permitted if CVC4 was built with model
    * support and produce-models is on.
    */
-  Model* getModel() throw(ModalException, AssertionException);
+  Model* getModel() throw(ModalException);
 
   /**
    * Get the last proof (only if immediately preceded by an UNSAT
    * or VALID query).  Only permitted if CVC4 was built with proof
    * support and produce-proofs is on.
    */
-  Proof* getProof() throw(ModalException, AssertionException);
+  Proof* getProof() throw(ModalException);
 
   /**
    * Get the current set of assertions.  Only permitted if the
    * SmtEngine is set to operate interactively.
    */
-  std::vector<Expr> getAssertions() throw(ModalException, AssertionException);
+  std::vector<Expr> getAssertions() throw(ModalException);
 
   /**
    * Push a user-level context.