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.

2 files changed, 29 insertions, 29 deletions

diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp
index 9660986cf..c4ae81927 100644
--- a/src/theory/logic_info.cpp
+++ b/src/theory/logic_info.cpp
@@ -76,7 +76,7 @@ LogicInfo::LogicInfo(const char* logicString) throw(IllegalArgumentException) :
 }
 
 std::string LogicInfo::getLogicString() const {
-  Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried");
+  CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
   if(d_logicString == "") {
     size_t seen = 0; // make sure we support all the active theories
 
@@ -129,7 +129,7 @@ std::string LogicInfo::getLogicString() const {
 }
 
 void LogicInfo::setLogicString(std::string logicString) throw(IllegalArgumentException) {
-  Assert(!d_locked, "This LogicInfo is locked, and cannot be modified");
+  CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
   for(TheoryId id = THEORY_FIRST; id < THEORY_LAST; ++id) {
     d_theories[id] = false;// ensure it's cleared
   }
@@ -244,17 +244,17 @@ void LogicInfo::setLogicString(std::string logicString) throw(IllegalArgumentExc
 }
 
 void LogicInfo::enableEverything() {
-  Assert(!d_locked, "This LogicInfo is locked, and cannot be modified");
+  CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
   *this = LogicInfo();
 }
 
 void LogicInfo::disableEverything() {
-  Assert(!d_locked, "This LogicInfo is locked, and cannot be modified");
+  CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
   *this = LogicInfo("");
 }
 
 void LogicInfo::enableTheory(theory::TheoryId theory) {
-  Assert(!d_locked, "This LogicInfo is locked, and cannot be modified");
+  CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
   if(!d_theories[theory]) {
     if(isTrueTheory(theory)) {
       ++d_sharingTheories;
@@ -265,7 +265,7 @@ void LogicInfo::enableTheory(theory::TheoryId theory) {
 }
 
 void LogicInfo::disableTheory(theory::TheoryId theory) {
-  Assert(!d_locked, "This LogicInfo is locked, and cannot be modified");
+  CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
   if(d_theories[theory]) {
     if(isTrueTheory(theory)) {
       Assert(d_sharingTheories > 0);
@@ -281,14 +281,14 @@ void LogicInfo::disableTheory(theory::TheoryId theory) {
 }
 
 void LogicInfo::enableIntegers() {
-  Assert(!d_locked, "This LogicInfo is locked, and cannot be modified");
+  CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
   d_logicString = "";
   enableTheory(THEORY_ARITH);
   d_integers = true;
 }
 
 void LogicInfo::disableIntegers() {
-  Assert(!d_locked, "This LogicInfo is locked, and cannot be modified");
+  CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
   d_logicString = "";
   d_integers = false;
   if(!d_reals) {
@@ -297,14 +297,14 @@ void LogicInfo::disableIntegers() {
 }
 
 void LogicInfo::enableReals() {
-  Assert(!d_locked, "This LogicInfo is locked, and cannot be modified");
+  CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
   d_logicString = "";
   enableTheory(THEORY_ARITH);
   d_reals = true;
 }
 
 void LogicInfo::disableReals() {
-  Assert(!d_locked, "This LogicInfo is locked, and cannot be modified");
+  CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
   d_logicString = "";
   d_reals = false;
   if(!d_integers) {
@@ -313,21 +313,21 @@ void LogicInfo::disableReals() {
 }
 
 void LogicInfo::arithOnlyDifference() {
-  Assert(!d_locked, "This LogicInfo is locked, and cannot be modified");
+  CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
   d_logicString = "";
   d_linear = true;
   d_differenceLogic = true;
 }
 
 void LogicInfo::arithOnlyLinear() {
-  Assert(!d_locked, "This LogicInfo is locked, and cannot be modified");
+  CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
   d_logicString = "";
   d_linear = true;
   d_differenceLogic = false;
 }
 
 void LogicInfo::arithNonLinear() {
-  Assert(!d_locked, "This LogicInfo is locked, and cannot be modified");
+  CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
   d_logicString = "";
   d_linear = false;
   d_differenceLogic = false;
diff --git a/src/theory/logic_info.h b/src/theory/logic_info.h
index 36b71e931..8cd326039 100644
--- a/src/theory/logic_info.h
+++ b/src/theory/logic_info.h
@@ -105,25 +105,25 @@ public:
 
   /** Is sharing enabled for this logic? */
   bool isSharingEnabled() const {
-    Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried");
+    CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
     return d_sharingTheories > 1;
   }
 
   /** Is the given theory module active in this logic? */
   bool isTheoryEnabled(theory::TheoryId theory) const {
-    Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried");
+    CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
     return d_theories[theory];
   }
 
   /** Is this a quantified logic? */
   bool isQuantified() const {
-    Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried");
+    CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
     return isTheoryEnabled(theory::THEORY_QUANTIFIERS) || isTheoryEnabled(theory::THEORY_REWRITERULES);
   }
 
   /** Is this the all-inclusive logic? */
   bool hasEverything() const {
-    Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried");
+    CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
     LogicInfo everything;
     everything.lock();
     return *this == everything;
@@ -131,7 +131,7 @@ public:
 
   /** Is this the all-exclusive logic?  (Here, that means propositional logic) */
   bool hasNothing() const {
-    Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried");
+    CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
     LogicInfo nothing("");
     nothing.lock();
     return *this == nothing;
@@ -143,7 +143,7 @@ public:
    * use "isPure(theory) && !isQuantified()".
    */
   bool isPure(theory::TheoryId theory) const {
-    Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried");
+    CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
     // the third and fourth conjucts are really just to rule out the misleading
     // case where you ask isPure(THEORY_BOOL) and get true even in e.g. QF_LIA
     return isTheoryEnabled(theory) && !isSharingEnabled() &&
@@ -155,22 +155,22 @@ public:
 
   /** Are integers in this logic? */
   bool areIntegersUsed() const {
-    Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried");
+    CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
     return d_integers;
   }
   /** Are reals in this logic? */
   bool areRealsUsed() const {
-    Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried");
+    CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
     return d_reals;
   }
   /** Does this logic only linear arithmetic? */
   bool isLinear() const {
-    Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried");
+    CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
     return d_linear || d_differenceLogic;
   }
   /** Does this logic only permit difference reasoning? (implies linear) */
   bool isDifferenceLogic() const {
-    Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried");
+    CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
     return d_differenceLogic;
   }
 
@@ -252,13 +252,13 @@ public:
 
   /** Are these two LogicInfos equal? */
   bool operator==(const LogicInfo& other) const {
-    Assert(isLocked() && other.isLocked(), "This LogicInfo isn't locked yet, and cannot be queried");
+    CheckArgument(isLocked() && other.isLocked(), *this, "This LogicInfo isn't locked yet, and cannot be queried");
     for(theory::TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) {
       if(d_theories[id] != other.d_theories[id]) {
         return false;
       }
     }
-    Assert(d_sharingTheories == other.d_sharingTheories, "LogicInfo internal inconsistency");
+    CheckArgument(d_sharingTheories == other.d_sharingTheories, *this, "LogicInfo internal inconsistency");
     if(isTheoryEnabled(theory::THEORY_ARITH)) {
       return
         d_integers == other.d_integers &&
@@ -283,13 +283,13 @@ public:
   }
   /** Is this LogicInfo "less than or equal" the other? */
   bool operator<=(const LogicInfo& other) const {
-    Assert(isLocked() && other.isLocked(), "This LogicInfo isn't locked yet, and cannot be queried");
+    CheckArgument(isLocked() && other.isLocked(), *this, "This LogicInfo isn't locked yet, and cannot be queried");
     for(theory::TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) {
       if(d_theories[id] && !other.d_theories[id]) {
         return false;
       }
     }
-    Assert(d_sharingTheories <= other.d_sharingTheories, "LogicInfo internal inconsistency");
+    CheckArgument(d_sharingTheories <= other.d_sharingTheories, *this, "LogicInfo internal inconsistency");
     if(isTheoryEnabled(theory::THEORY_ARITH) && other.isTheoryEnabled(theory::THEORY_ARITH)) {
       return
         (!d_integers || other.d_integers) &&
@@ -302,13 +302,13 @@ public:
   }
   /** Is this LogicInfo "greater than or equal" the other? */
   bool operator>=(const LogicInfo& other) const {
-    Assert(isLocked() && other.isLocked(), "This LogicInfo isn't locked yet, and cannot be queried");
+    CheckArgument(isLocked() && other.isLocked(), *this, "This LogicInfo isn't locked yet, and cannot be queried");
     for(theory::TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) {
       if(!d_theories[id] && other.d_theories[id]) {
         return false;
       }
     }
-    Assert(d_sharingTheories >= other.d_sharingTheories, "LogicInfo internal inconsistency");
+    CheckArgument(d_sharingTheories >= other.d_sharingTheories, *this, "LogicInfo internal inconsistency");
     if(isTheoryEnabled(theory::THEORY_ARITH) && other.isTheoryEnabled(theory::THEORY_ARITH)) {
       return
         (d_integers || !other.d_integers) &&