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, 18 insertions, 9 deletions

diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h
index fc7d838a1..2857dc5d8 100644
--- a/src/expr/kind_template.h
+++ b/src/expr/kind_template.h
@@ -24,7 +24,7 @@
 #include <iostream>
 #include <sstream>
 
-#include "util/Assert.h"
+#include "util/exception.h"
 
 namespace CVC4 {
 namespace kind {
@@ -100,6 +100,7 @@ struct KindHashFunction {
  */
 enum TypeConstant {
 ${type_constant_list}
+#line 104 "${template}"
   LAST_TYPE
 };/* enum TypeConstant */
 
@@ -115,6 +116,7 @@ struct TypeConstantHashFunction {
 inline std::ostream& operator<<(std::ostream& out, TypeConstant typeConstant) {
   switch(typeConstant) {
 ${type_constant_descriptions}
+#line 120 "${template}"
   default:
     out << "UNKNOWN_TYPE_CONSTANT";
     break;
@@ -126,8 +128,9 @@ namespace theory {
 
 enum TheoryId {
 ${theory_enum}
+#line 132 "${template}"
   THEORY_LAST
-};
+};/* enum TheoryId */
 
 const TheoryId THEORY_FIRST = static_cast<TheoryId>(0);
 const TheoryId THEORY_SAT_SOLVER = THEORY_LAST;
@@ -139,6 +142,7 @@ inline TheoryId& operator ++ (TheoryId& id) {
 inline std::ostream& operator<<(std::ostream& out, TheoryId theoryId) {
   switch(theoryId) {
 ${theory_descriptions}
+#line 146 "${template}"
   default:
     out << "UNKNOWN_THEORY";
     break;
@@ -148,23 +152,28 @@ ${theory_descriptions}
 
 inline TheoryId kindToTheoryId(::CVC4::Kind k) {
   switch(k) {
+  case kind::UNDEFINED_KIND:
+  case kind::NULL_EXPR:
+    break;
 ${kind_to_theory_id}
-  default:
-    Unhandled(k);
+#line 160 "${template}"
+  case kind::LAST_KIND:
+    break;
   }
+  throw IllegalArgumentException("", "k", __PRETTY_FUNCTION__, "bad kind");
 }
 
 inline TheoryId typeConstantToTheoryId(::CVC4::TypeConstant typeConstant) {
   switch(typeConstant) {
 ${type_constant_to_theory_id}
-  default:
-    Unhandled(typeConstant);
+#line 170 "${template}"
+  case LAST_TYPE:
+    break;
   }
+  throw IllegalArgumentException("", "k", __PRETTY_FUNCTION__, "bad type constant");
 }
 
-}/* theory namespace */
-
-
+}/* CVC4::theory namespace */
 }/* CVC4 namespace */
 
 #endif /* __CVC4__KIND_H */