some things I had laying around in a directory but never got committed; minor fix-ups to documentation and some node stuff

7 files changed, 130 insertions, 61 deletions

diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index 95f7c0437..252cba43e 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -459,9 +459,9 @@ public:
   inline const_iterator begin() const {
     Assert(!isUsed(), "NodeBuilder is one-shot only; "
            "attempt to access it after conversion");
-    CheckArgument(getKind() != kind::UNDEFINED_KIND,
-                  "Iterators over NodeBuilder<> are undefined "
-                  "until a Kind is set");
+    Assert(getKind() != kind::UNDEFINED_KIND,
+           "Iterators over NodeBuilder<> are undefined "
+           "until a Kind is set");
     return d_nv->begin< NodeTemplate<true> >();
   }
 
@@ -469,9 +469,9 @@ public:
   inline const_iterator end() const {
     Assert(!isUsed(), "NodeBuilder is one-shot only; "
            "attempt to access it after conversion");
-    CheckArgument(getKind() != kind::UNDEFINED_KIND,
-                  "Iterators over NodeBuilder<> are undefined "
-                  "until a Kind is set");
+    Assert(getKind() != kind::UNDEFINED_KIND,
+           "Iterators over NodeBuilder<> are undefined "
+           "until a Kind is set");
     return d_nv->end< NodeTemplate<true> >();
   }
 
@@ -486,9 +486,9 @@ public:
   inline kind::MetaKind getMetaKind() const {
     Assert(!isUsed(), "NodeBuilder is one-shot only; "
            "attempt to access it after conversion");
-    CheckArgument(getKind() != kind::UNDEFINED_KIND,
-                  "The metakind of a NodeBuilder<> is undefined "
-                  "until a Kind is set");
+    Assert(getKind() != kind::UNDEFINED_KIND,
+           "The metakind of a NodeBuilder<> is undefined "
+           "until a Kind is set");
     return d_nv->getMetaKind();
   }
 
@@ -496,19 +496,40 @@ public:
   inline unsigned getNumChildren() const {
     Assert(!isUsed(), "NodeBuilder is one-shot only; "
            "attempt to access it after conversion");
-    CheckArgument(getKind() != kind::UNDEFINED_KIND,
-                  "The number of children of a NodeBuilder<> is undefined "
-                  "until a Kind is set");
+    Assert(getKind() != kind::UNDEFINED_KIND,
+           "The number of children of a NodeBuilder<> is undefined "
+           "until a Kind is set");
     return d_nv->getNumChildren();
   }
 
-  /** Access to children of this Node-under-construction. */
+  /**
+   * Access to the operator of this Node-under-construction.  Only
+   * allowed if this NodeBuilder is unused, and has a defined kind
+   * that is of PARAMETERIZED metakind.
+   */
+  inline Node getOperator() const {
+    Assert(!isUsed(), "NodeBuilder is one-shot only; "
+           "attempt to access it after conversion");
+    Assert(getKind() != kind::UNDEFINED_KIND,
+           "NodeBuilder<> operator access is not permitted "
+           "until a Kind is set");
+    Assert(getMetaKind() == kind::metakind::PARAMETERIZED,
+           "NodeBuilder<> operator access is only permitted "
+           "on parameterized kinds, not `%s'",
+           kind::kindToString(getKind()).c_str());
+    return Node(d_nv->getOperator());
+  }
+
+  /**
+   * Access to children of this Node-under-construction.  Only allowed
+   * if this NodeBuilder is unused and has a defined kind.
+   */
   inline Node getChild(int i) const {
     Assert(!isUsed(), "NodeBuilder is one-shot only; "
            "attempt to access it after conversion");
-    CheckArgument(getKind() != kind::UNDEFINED_KIND,
-                  "NodeBuilder<> child access is not permitted "
-                  "until a Kind is set");
+    Assert(getKind() != kind::UNDEFINED_KIND,
+           "NodeBuilder<> child access is not permitted "
+           "until a Kind is set");
     Assert(i >= 0 && unsigned(i) < d_nv->getNumChildren(),
            "index out of range for NodeBuilder::getChild()");
     return Node(d_nv->getChild(i));
diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index f2da42731..2c11b58d5 100644
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -290,6 +290,7 @@ public:
   template <class T>
   inline const T& getConst() const;
 
+  NodeValue* getOperator() const;
   NodeValue* getChild(int i) const;
 
   void printAst(std::ostream& out, int indent = 0) const;
@@ -432,6 +433,11 @@ inline bool NodeValue::isBeingDeleted() const {
     NodeManager::currentNM()->isCurrentlyDeleting(this);
 }
 
+inline NodeValue* NodeValue::getOperator() const {
+  Assert(getMetaKind() == kind::metakind::PARAMETERIZED);
+  return d_children[0];
+}
+
 inline NodeValue* NodeValue::getChild(int i) const {
   if(getMetaKind() == kind::metakind::PARAMETERIZED) {
     ++i;
diff --git a/src/main/main.cpp b/src/main/main.cpp
index 9c2464b8d..c21a7bdac 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -281,11 +281,7 @@ int runCvc4(int argc, char* argv[]) {
     Message() << Configuration::getPackageName()
               << " " << Configuration::getVersionString();
     if(Configuration::isSubversionBuild()) {
-      Message() << " [subversion " << Configuration::getSubversionBranchName()
-                << " r" << Configuration::getSubversionRevision()
-                << (Configuration::hasSubversionModifications() ?
-                    " (with modifications)" : "")
-                << "]";
+      Message() << " [" << Configuration::getSubversionId() << "]";
     }
     Message() << (Configuration::isDebugBuild() ? " DEBUG" : "")
               << " assertions:"
diff --git a/src/util/configuration.cpp b/src/util/configuration.cpp
index db3c5520e..aa3e6bf6b 100644
--- a/src/util/configuration.cpp
+++ b/src/util/configuration.cpp
@@ -19,6 +19,7 @@
  **/
 
 #include <string>
+#include <sstream>
 
 #include "util/configuration.h"
 #include "util/configuration_private.h"
@@ -124,4 +125,15 @@ bool Configuration::hasSubversionModifications() {
   return SUBVERSION_HAS_MODIFICATIONS;
 }
 
+string Configuration::getSubversionId() {
+  if(! isSubversionBuild()) {
+    return "";
+  }
+
+  stringstream ss;
+  ss << "subversion " << getSubversionBranchName() << " r" << getSubversionRevision()
+     << ( ::CVC4::Configuration::hasSubversionModifications() ? " (with modifications)" : "" );
+  return ss.str();
+}
+
 }/* CVC4 namespace */
diff --git a/src/util/configuration.h b/src/util/configuration.h
index 258431114..31a2ca3d4 100644
--- a/src/util/configuration.h
+++ b/src/util/configuration.h
@@ -87,6 +87,7 @@ public:
   static const char* getSubversionBranchName();
   static unsigned getSubversionRevision();
   static bool hasSubversionModifications();
+  static std::string getSubversionId();
 
 };/* class Configuration */
 
diff --git a/src/util/configuration_private.h b/src/util/configuration_private.h
index 4f7501a08..0421273ca 100644
--- a/src/util/configuration_private.h
+++ b/src/util/configuration_private.h
@@ -20,6 +20,9 @@
 #ifndef __CVC4__CONFIGURATION_PRIVATE_H
 #define __CVC4__CONFIGURATION_PRIVATE_H
 
+#include <string>
+#include "util/configuration.h"
+
 namespace CVC4 {
 
 #ifdef CVC4_DEBUG
@@ -100,14 +103,18 @@ namespace CVC4 {
 #  define USING_TLS false
 #endif /* TLS */
 
-#define CVC4_ABOUT_STRING string("\
-This is CVC4 version " CVC4_RELEASE_STRING "\n\n\
+#define CVC4_ABOUT_STRING ( ::std::string("\
+This is CVC4 version " CVC4_RELEASE_STRING ) + \
+    ( ::CVC4::Configuration::isSubversionBuild() \
+        ? ( ::std::string(" [") + ::CVC4::Configuration::getSubversionId() + "]" ) \
+        : ::std::string("") \
+    ) + "\n\n\
 Copyright (C) 2009, 2010, 2011\n\
   The ACSys Group\n\
   Courant Institute of Mathematical Sciences\n\
   New York University\n\
-  New York, NY  10012  USA\n\n") + \
-    (IS_CLN_BUILD ? "\
+  New York, NY  10012  USA\n\n" + \
+    ( IS_CLN_BUILD ? "\
 This CVC4 library uses CLN as its multi-precision arithmetic library.\n\n\
 CVC4 is open-source and is covered by the BSD license (modified).\n\
 However, CLN, the Class Library for Numbers, is covered by the GPL.  Thus\n\
@@ -116,7 +123,7 @@ consult the CVC4 documentation for instructions about building a version\n\
 of CVC4 that links against GMP, and can be used in such applications.\n" : \
 "This CVC4 library uses GMP as its multi-precision arithmetic library.\n\n\
 CVC4 is open-source and is covered by the BSD license (modified).\n\n\
-THIS SOFTWARE PROVIDED AS-IS, WITHOUT ANY WARRANTIES. USE IT AT YOUR OWN RISK.\n")
+THIS SOFTWARE PROVIDED AS-IS, WITHOUT ANY WARRANTIES. USE IT AT YOUR OWN RISK.\n" ) )
 
 }/* CVC4 namespace */
 
diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h
index 320d4ddbe..c084c4ecb 100644
--- a/test/unit/expr/node_builder_black.h
+++ b/test/unit/expr/node_builder_black.h
@@ -96,9 +96,11 @@ public:
     /* default size tests */
     NodeBuilder<> def;
     TS_ASSERT_EQUALS(def.getKind(), UNDEFINED_KIND);
-    TS_ASSERT_THROWS(def.getNumChildren(), IllegalArgumentException);
-    TS_ASSERT_THROWS(def.begin(), IllegalArgumentException);
-    TS_ASSERT_THROWS(def.end(), IllegalArgumentException);
+#ifdef CVC4_ASSERTIONS
+    TS_ASSERT_THROWS(def.getNumChildren(), AssertionException);
+    TS_ASSERT_THROWS(def.begin(), AssertionException);
+    TS_ASSERT_THROWS(def.end(), AssertionException);
+#endif /* CVC4_ASSERTIONS */
 
     NodeBuilder<> spec(specKind);
     TS_ASSERT_EQUALS(spec.getKind(), specKind);
@@ -108,9 +110,11 @@ public:
 
     NodeBuilder<> from_nm(d_nm);
     TS_ASSERT_EQUALS(from_nm.getKind(), UNDEFINED_KIND);
-    TS_ASSERT_THROWS(from_nm.getNumChildren(), IllegalArgumentException);
-    TS_ASSERT_THROWS(from_nm.begin(), IllegalArgumentException);
-    TS_ASSERT_THROWS(from_nm.end(), IllegalArgumentException);
+#ifdef CVC4_ASSERTIONS
+    TS_ASSERT_THROWS(from_nm.getNumChildren(), AssertionException);
+    TS_ASSERT_THROWS(from_nm.begin(), AssertionException);
+    TS_ASSERT_THROWS(from_nm.end(), AssertionException);
+#endif /* CVC4_ASSERTIONS */
 
     NodeBuilder<> from_nm_kind(d_nm, specKind);
     TS_ASSERT_EQUALS(from_nm_kind.getKind(), specKind);
@@ -122,9 +126,11 @@ public:
 
     NodeBuilder<K> ws;
     TS_ASSERT_EQUALS(ws.getKind(), UNDEFINED_KIND);
-    TS_ASSERT_THROWS(ws.getNumChildren(), IllegalArgumentException);
-    TS_ASSERT_THROWS(ws.begin(), IllegalArgumentException);
-    TS_ASSERT_THROWS(ws.end(), IllegalArgumentException);
+#ifdef CVC4_ASSERTIONS
+    TS_ASSERT_THROWS(ws.getNumChildren(), AssertionException);
+    TS_ASSERT_THROWS(ws.begin(), AssertionException);
+    TS_ASSERT_THROWS(ws.end(), AssertionException);
+#endif /* CVC4_ASSERTIONS */
 
     NodeBuilder<K> ws_kind(specKind);
     TS_ASSERT_EQUALS(ws_kind.getKind(), specKind);
@@ -134,9 +140,11 @@ public:
 
     NodeBuilder<K> ws_from_nm(d_nm);
     TS_ASSERT_EQUALS(ws_from_nm.getKind(), UNDEFINED_KIND);
-    TS_ASSERT_THROWS(ws_from_nm.getNumChildren(), IllegalArgumentException);
-    TS_ASSERT_THROWS(ws_from_nm.begin(), IllegalArgumentException);
-    TS_ASSERT_THROWS(ws_from_nm.end(), IllegalArgumentException);
+#ifdef CVC4_ASSERTIONS
+    TS_ASSERT_THROWS(ws_from_nm.getNumChildren(), AssertionException);
+    TS_ASSERT_THROWS(ws_from_nm.begin(), AssertionException);
+    TS_ASSERT_THROWS(ws_from_nm.end(), AssertionException);
+#endif /* CVC4_ASSERTIONS */
 
     NodeBuilder<K> ws_from_nm_kind(d_nm, specKind);
     TS_ASSERT_EQUALS(ws_from_nm_kind.getKind(), specKind);
@@ -153,27 +161,35 @@ public:
 
     NodeBuilder<> copy(def);
     TS_ASSERT_EQUALS(copy.getKind(), UNDEFINED_KIND);
-    TS_ASSERT_THROWS(copy.getNumChildren(), IllegalArgumentException);
-    TS_ASSERT_THROWS(copy.begin(), IllegalArgumentException);
-    TS_ASSERT_THROWS(copy.end(), IllegalArgumentException);
+#ifdef CVC4_ASSERTIONS
+    TS_ASSERT_THROWS(copy.getNumChildren(), AssertionException);
+    TS_ASSERT_THROWS(copy.begin(), AssertionException);
+    TS_ASSERT_THROWS(copy.end(), AssertionException);
+#endif /* CVC4_ASSERTIONS */
 
     NodeBuilder<K> cp_ws(ws);
     TS_ASSERT_EQUALS(cp_ws.getKind(), UNDEFINED_KIND);
-    TS_ASSERT_THROWS(cp_ws.getNumChildren(), IllegalArgumentException);
-    TS_ASSERT_THROWS(cp_ws.begin(), IllegalArgumentException);
-    TS_ASSERT_THROWS(cp_ws.end(), IllegalArgumentException);
+#ifdef CVC4_ASSERTIONS
+    TS_ASSERT_THROWS(cp_ws.getNumChildren(), AssertionException);
+    TS_ASSERT_THROWS(cp_ws.begin(), AssertionException);
+    TS_ASSERT_THROWS(cp_ws.end(), AssertionException);
+#endif /* CVC4_ASSERTIONS */
 
     NodeBuilder<K-10> cp_from_larger(ws);
     TS_ASSERT_EQUALS(cp_from_larger.getKind(), UNDEFINED_KIND);
-    TS_ASSERT_THROWS(cp_from_larger.getNumChildren(), IllegalArgumentException);
-    TS_ASSERT_THROWS(cp_from_larger.begin(), IllegalArgumentException);
-    TS_ASSERT_THROWS(cp_from_larger.end(), IllegalArgumentException);
+#ifdef CVC4_ASSERTIONS
+    TS_ASSERT_THROWS(cp_from_larger.getNumChildren(), AssertionException);
+    TS_ASSERT_THROWS(cp_from_larger.begin(), AssertionException);
+    TS_ASSERT_THROWS(cp_from_larger.end(), AssertionException);
+#endif /* CVC4_ASSERTIONS */
 
     NodeBuilder<K+10> cp_from_smaller(ws);
     TS_ASSERT_EQUALS(cp_from_smaller.getKind(), UNDEFINED_KIND);
-    TS_ASSERT_THROWS(cp_from_smaller.getNumChildren(), IllegalArgumentException);
-    TS_ASSERT_THROWS(cp_from_smaller.begin(), IllegalArgumentException);
-    TS_ASSERT_THROWS(cp_from_smaller.end(), IllegalArgumentException);
+#ifdef CVC4_ASSERTIONS
+    TS_ASSERT_THROWS(cp_from_smaller.getNumChildren(), AssertionException);
+    TS_ASSERT_THROWS(cp_from_smaller.begin(), AssertionException);
+    TS_ASSERT_THROWS(cp_from_smaller.end(), AssertionException);
+#endif /* CVC4_ASSERTIONS */
   }
 
   void testDestructor() {
@@ -284,7 +300,9 @@ public:
     Node x( d_nm->mkVar( *d_integerType ) );
 
     NodeBuilder<> nb;
-    TS_ASSERT_THROWS(nb.getNumChildren(), IllegalArgumentException);
+#ifdef CVC4_ASSERTIONS
+    TS_ASSERT_THROWS(nb.getNumChildren(), AssertionException);
+#endif /* CVC4_ASSERTIONS */
     nb << PLUS << x << x;
 
     TS_ASSERT_EQUALS(nb.getNumChildren(), 2u);
@@ -294,7 +312,9 @@ public:
 
     Node n = nb;// avoid warning on clear()
     nb.clear();
-    TS_ASSERT_THROWS(nb.getNumChildren(), IllegalArgumentException);
+#ifdef CVC4_ASSERTIONS
+    TS_ASSERT_THROWS(nb.getNumChildren(), AssertionException);
+#endif /* CVC4_ASSERTIONS */
     nb.clear(PLUS);
     TS_ASSERT_EQUALS(nb.getNumChildren(), 0u);
     nb << x << x << x;
@@ -368,9 +388,11 @@ public:
     NodeBuilder<> nb;
 
     TS_ASSERT_EQUALS(nb.getKind(), UNDEFINED_KIND);
-    TS_ASSERT_THROWS(nb.getNumChildren(), IllegalArgumentException);
-    TS_ASSERT_THROWS(nb.begin(), IllegalArgumentException);
-    TS_ASSERT_THROWS(nb.end(), IllegalArgumentException);
+#ifdef CVC4_ASSERTIONS
+    TS_ASSERT_THROWS(nb.getNumChildren(), AssertionException);
+    TS_ASSERT_THROWS(nb.begin(), AssertionException);
+    TS_ASSERT_THROWS(nb.end(), AssertionException);
+#endif /* CVC4_ASSERTIONS */
 
     nb << specKind;
     push_back(nb, K);
@@ -383,9 +405,11 @@ public:
     nb.clear();
 
     TS_ASSERT_EQUALS(nb.getKind(), UNDEFINED_KIND);
-    TS_ASSERT_THROWS(nb.getNumChildren(), IllegalArgumentException);
-    TS_ASSERT_THROWS(nb.begin(), IllegalArgumentException);
-    TS_ASSERT_THROWS(nb.end(), IllegalArgumentException);
+#ifdef CVC4_ASSERTIONS
+    TS_ASSERT_THROWS(nb.getNumChildren(), AssertionException);
+    TS_ASSERT_THROWS(nb.begin(), AssertionException);
+    TS_ASSERT_THROWS(nb.end(), AssertionException);
+#endif /* CVC4_ASSERTIONS */
 
     nb << specKind;
     push_back(nb, K);
@@ -406,9 +430,11 @@ public:
     nb.clear();
 
     TS_ASSERT_EQUALS(nb.getKind(), UNDEFINED_KIND);
-    TS_ASSERT_THROWS(nb.getNumChildren(), IllegalArgumentException);
-    TS_ASSERT_THROWS(nb.begin(), IllegalArgumentException);
-    TS_ASSERT_THROWS(nb.end(), IllegalArgumentException);
+#ifdef CVC4_ASSERTIONS
+    TS_ASSERT_THROWS(nb.getNumChildren(), AssertionException);
+    TS_ASSERT_THROWS(nb.begin(), AssertionException);
+    TS_ASSERT_THROWS(nb.end(), AssertionException);
+#endif /* CVC4_ASSERTIONS */
   }
 
   void testStreamInsertionKind() {