* Added NodeBuilder<>::getChild() to make interface more consistent

  with that of Node.

* If NodeBuilder<> hasn't yet been assigned a Kind, several member functions
  related to children now throw an IllegalArgumentException:

    * getNumChildren()
    * begin()
    * end()
    * operator[]
    * getChild()

  This is because if you later assign the NodeBuilder<> a PARAMETERIZED kind,
  the children are "reinterpreted" -- the first being an operator.  Interface-wise,
  it doesn't make sense to return one thing for nb[0], then later, after setting
  the kind, to return another thing for nb[0].

* Fixed unit tests depending on this behavior.

* Added a warning to the testing summary if unit tests didn't run (because this
  is likely due to compilation problems, and without a warning it looks kind of
  like a test success)

* VERBOSE wasn't exported to the environment for unit test "make check."  Fixed.

diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index fcc6bb3645691ae1a8e362bd8f07bf4e63217c55..877c50d82f4e465c0469ed64104fa86e45fdcdf0 100644 (file)
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -418,6 +418,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");
     return d_nv->begin< NodeTemplate<true> >();
   }
 
@@ -425,6 +428,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");
     return d_nv->end< NodeTemplate<true> >();
   }
 
@@ -439,6 +445,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");
     return d_nv->getMetaKind();
   }
 
@@ -446,18 +455,29 @@ 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");
     return d_nv->getNumChildren();
   }
 
   /** Access to children of this Node-under-construction. */
-  inline Node operator[](int i) const {
+  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(i >= 0 && unsigned(i) < d_nv->getNumChildren(),
-           "index out of range for NodeBuilder[]");
+           "index out of range for NodeBuilder::getChild()");
     return Node(d_nv->getChild(i));
   }
 
+  /** Access to children of this Node-under-construction. */
+  inline Node operator[](int i) const {
+    return getChild(i);
+  }
+
   /**
    * "Reset" this node builder (optionally setting a new kind for it),
    * using the same "inline" memory as at construction time.  This

diff --git a/test/Makefile.am b/test/Makefile.am
index de8e7a98512b891d05389c5b52545a9bedb458b7..2b79c50458b2c452aceeae304223b3c532242ac1 100644 (file)
--- a/test/Makefile.am
+++ b/test/Makefile.am
@@ -34,6 +34,9 @@ check-pre:
 check-local:
        @$(am__tty_colors); \
        echo $${blu}===============================  TESTING SUMMARY  =============================$$std; \
+       if test -s "unit/test-suite.log"; then :; else \
+               echo "$${red}Unit tests did not run; maybe there were compilation problems ?$$std"; \
+        fi; \
        for dir in $(subdirs_to_check); do \
                log=$$dir/test-suite.log; \
                if test -s "$$log"; then \

diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am
index 56c0eae264742c0094fab498c77c3456a8dfd1ef..1f283f4766af66c33e3b9dbb3981bb3a2101b297 100644 (file)
--- a/test/unit/Makefile.am
+++ b/test/unit/Makefile.am
@@ -32,7 +32,7 @@ UNIT_TESTS = \
        util/rational_black \
        util/rational_white
 
-VERBOSE = 1
+export VERBOSE = 1
 
 # Things that aren't tests but that tests rely on and need to
 # go into the distribution

diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h
index a1887118cce1d382e24f767f378a749fe5c94da2..8bde4b04716220eca940e889b7357a4a0891c534 100644 (file)
--- a/test/unit/expr/node_builder_black.h
+++ b/test/unit/expr/node_builder_black.h
@@ -85,8 +85,9 @@ public:
     /* default size tests */
     NodeBuilder<> def;
     TS_ASSERT_EQUALS(def.getKind(), UNDEFINED_KIND);
-    TS_ASSERT_EQUALS(def.getNumChildren(), 0u);
-    TS_ASSERT_EQUALS(def.begin(), def.end());
+    TS_ASSERT_THROWS(def.getNumChildren(), IllegalArgumentException);
+    TS_ASSERT_THROWS(def.begin(), IllegalArgumentException);
+    TS_ASSERT_THROWS(def.end(), IllegalArgumentException);
 
     NodeBuilder<> spec(specKind);
     TS_ASSERT_EQUALS(spec.getKind(), specKind);
@@ -96,8 +97,9 @@ public:
 
     NodeBuilder<> from_nm(d_nm);
     TS_ASSERT_EQUALS(from_nm.getKind(), UNDEFINED_KIND);
-    TS_ASSERT_EQUALS(from_nm.getNumChildren(), 0u);
-    TS_ASSERT_EQUALS(from_nm.begin(), from_nm.end());
+    TS_ASSERT_THROWS(from_nm.getNumChildren(), IllegalArgumentException);
+    TS_ASSERT_THROWS(from_nm.begin(), IllegalArgumentException);
+    TS_ASSERT_THROWS(from_nm.end(), IllegalArgumentException);
 
     NodeBuilder<> from_nm_kind(d_nm, specKind);
     TS_ASSERT_EQUALS(from_nm_kind.getKind(), specKind);
@@ -109,8 +111,9 @@ public:
 
     NodeBuilder<K> ws;
     TS_ASSERT_EQUALS(ws.getKind(), UNDEFINED_KIND);
-    TS_ASSERT_EQUALS(ws.getNumChildren(), 0u);
-    TS_ASSERT_EQUALS(ws.begin(), ws.end());
+    TS_ASSERT_THROWS(ws.getNumChildren(), IllegalArgumentException);
+    TS_ASSERT_THROWS(ws.begin(), IllegalArgumentException);
+    TS_ASSERT_THROWS(ws.end(), IllegalArgumentException);
 
     NodeBuilder<K> ws_kind(specKind);
     TS_ASSERT_EQUALS(ws_kind.getKind(), specKind);
@@ -120,8 +123,9 @@ public:
 
     NodeBuilder<K> ws_from_nm(d_nm);
     TS_ASSERT_EQUALS(ws_from_nm.getKind(), UNDEFINED_KIND);
-    TS_ASSERT_EQUALS(ws_from_nm.getNumChildren(), 0u);
-    TS_ASSERT_EQUALS(ws_from_nm.begin(), ws_from_nm.end());
+    TS_ASSERT_THROWS(ws_from_nm.getNumChildren(), IllegalArgumentException);
+    TS_ASSERT_THROWS(ws_from_nm.begin(), IllegalArgumentException);
+    TS_ASSERT_THROWS(ws_from_nm.end(), IllegalArgumentException);
 
     NodeBuilder<K> ws_from_nm_kind(d_nm, specKind);
     TS_ASSERT_EQUALS(ws_from_nm_kind.getKind(), specKind);
@@ -138,25 +142,27 @@ public:
 
     NodeBuilder<> copy(def);
     TS_ASSERT_EQUALS(copy.getKind(), UNDEFINED_KIND);
-    TS_ASSERT_EQUALS(copy.getNumChildren(), 0u);
-    TS_ASSERT_EQUALS(copy.begin(), copy.end());
+    TS_ASSERT_THROWS(copy.getNumChildren(), IllegalArgumentException);
+    TS_ASSERT_THROWS(copy.begin(), IllegalArgumentException);
+    TS_ASSERT_THROWS(copy.end(), IllegalArgumentException);
 
     NodeBuilder<K> cp_ws(ws);
     TS_ASSERT_EQUALS(cp_ws.getKind(), UNDEFINED_KIND);
-    TS_ASSERT_EQUALS(cp_ws.getNumChildren(), 0u);
-    TS_ASSERT_EQUALS(cp_ws.begin(), cp_ws.end());
-
+    TS_ASSERT_THROWS(cp_ws.getNumChildren(), IllegalArgumentException);
+    TS_ASSERT_THROWS(cp_ws.begin(), IllegalArgumentException);
+    TS_ASSERT_THROWS(cp_ws.end(), IllegalArgumentException);
 
     NodeBuilder<K-10> cp_from_larger(ws);
     TS_ASSERT_EQUALS(cp_from_larger.getKind(), UNDEFINED_KIND);
-    TS_ASSERT_EQUALS(cp_from_larger.getNumChildren(), 0u);
-    TS_ASSERT_EQUALS(cp_from_larger.begin(), cp_from_larger.end());
+    TS_ASSERT_THROWS(cp_from_larger.getNumChildren(), IllegalArgumentException);
+    TS_ASSERT_THROWS(cp_from_larger.begin(), IllegalArgumentException);
+    TS_ASSERT_THROWS(cp_from_larger.end(), IllegalArgumentException);
 
     NodeBuilder<K+10> cp_from_smaller(ws);
     TS_ASSERT_EQUALS(cp_from_smaller.getKind(), UNDEFINED_KIND);
-    TS_ASSERT_EQUALS(cp_from_smaller.getNumChildren(), 0u);
-    TS_ASSERT_EQUALS(cp_from_smaller.begin(), cp_from_smaller.end());
-
+    TS_ASSERT_THROWS(cp_from_smaller.getNumChildren(), IllegalArgumentException);
+    TS_ASSERT_THROWS(cp_from_smaller.begin(), IllegalArgumentException);
+    TS_ASSERT_THROWS(cp_from_smaller.end(), IllegalArgumentException);
   }
 
   void testDestructor() {
@@ -168,7 +174,7 @@ public:
 
   void testBeginEnd() {
     /* Test begin and ends without resizing */
-    NodeBuilder<K> ws;
+    NodeBuilder<K> ws(specKind);
     TS_ASSERT_EQUALS(ws.begin(), ws.end());
 
     push_back(ws, K);
@@ -190,7 +196,7 @@ public:
 
     /* Do the same tests and make sure that resizing occurs */
 
-    NodeBuilder<> smaller;
+    NodeBuilder<> smaller(specKind);
     TS_ASSERT_EQUALS(smaller.begin(), smaller.end());
 
     push_back(smaller, K);
@@ -261,30 +267,32 @@ public:
   void testGetNumChildren() {
     /* unsigned getNumChildren() const; */
 
-    NodeBuilder<> noKind;
-    TS_ASSERT_EQUALS(noKind.getNumChildren(), 0u);
-    push_back(noKind, K);
+    NodeBuilder<> nb;
+    TS_ASSERT_THROWS(nb.getNumChildren(), IllegalArgumentException);
+    nb << specKind;
+    push_back(nb, K);
 
-    TS_ASSERT_EQUALS(noKind.getNumChildren(), K);
+    TS_ASSERT_EQUALS(nb.getNumChildren(), K);
 
-    push_back(noKind, K);
-    TS_ASSERT_EQUALS(noKind.getNumChildren(), K + K);
+    push_back(nb, K);
+    TS_ASSERT_EQUALS(nb.getNumChildren(), K + K);
 
-    noKind << AND;// avoid exception on marking it used
-    Node n = noKind;// avoid warning on clear()
-    noKind.clear();
-    TS_ASSERT_EQUALS(noKind.getNumChildren(), 0u);
-    push_back(noKind, K);
+    Node n = nb;// avoid warning on clear()
+    nb.clear();
+    TS_ASSERT_THROWS(nb.getNumChildren(), IllegalArgumentException);
+    nb.clear(specKind);
+    TS_ASSERT_EQUALS(nb.getNumChildren(), 0u);
+    push_back(nb, K);
 
-    TS_ASSERT_EQUALS(noKind.getNumChildren(), K);
+    TS_ASSERT_EQUALS(nb.getNumChildren(), K);
 
-    push_back(noKind, K);
-    TS_ASSERT_EQUALS(noKind.getNumChildren(), K + K);
+    push_back(nb, K);
+    TS_ASSERT_EQUALS(nb.getNumChildren(), K + K);
 
 #ifdef CVC4_ASSERTIONS
-    noKind << specKind;
-    n = noKind;
-    TS_ASSERT_THROWS( noKind.getNumChildren(), AssertionException );
+    TS_ASSERT_THROWS( nb << specKind, AssertionException );
+    n = nb;
+    TS_ASSERT_THROWS( nb.getNumChildren(), AssertionException );
 #endif /* CVC4_ASSERTIONS */
   }
 
@@ -345,8 +353,9 @@ public:
     NodeBuilder<> nb;
 
     TS_ASSERT_EQUALS(nb.getKind(), UNDEFINED_KIND);
-    TS_ASSERT_EQUALS(nb.getNumChildren(), 0u);
-    TS_ASSERT_EQUALS(nb.begin(), nb.end());
+    TS_ASSERT_THROWS(nb.getNumChildren(), IllegalArgumentException);
+    TS_ASSERT_THROWS(nb.begin(), IllegalArgumentException);
+    TS_ASSERT_THROWS(nb.end(), IllegalArgumentException);
 
     nb << specKind;
     push_back(nb, K);
@@ -359,8 +368,9 @@ public:
     nb.clear();
 
     TS_ASSERT_EQUALS(nb.getKind(), UNDEFINED_KIND);
-    TS_ASSERT_EQUALS(nb.getNumChildren(), 0u);
-    TS_ASSERT_EQUALS(nb.begin(), nb.end());
+    TS_ASSERT_THROWS(nb.getNumChildren(), IllegalArgumentException);
+    TS_ASSERT_THROWS(nb.begin(), IllegalArgumentException);
+    TS_ASSERT_THROWS(nb.end(), IllegalArgumentException);
 
     nb << specKind;
     push_back(nb, K);
@@ -381,9 +391,9 @@ public:
     nb.clear();
 
     TS_ASSERT_EQUALS(nb.getKind(), UNDEFINED_KIND);
-    TS_ASSERT_EQUALS(nb.getNumChildren(), 0u);
-    TS_ASSERT_EQUALS(nb.begin(), nb.end());
-
+    TS_ASSERT_THROWS(nb.getNumChildren(), IllegalArgumentException);
+    TS_ASSERT_THROWS(nb.begin(), IllegalArgumentException);
+    TS_ASSERT_THROWS(nb.end(), IllegalArgumentException);
   }
 
   void testStreamInsertionKind() {
@@ -477,7 +487,7 @@ public:
     TS_ASSERT_THROWS(d_nm->mkNode(XOR, y, x, x), AssertionException);
 #endif /* CVC4_ASSERTIONS */
 
-    NodeBuilder<> b;
+    NodeBuilder<> b(specKind);
 
     // test append(TNode)
     b.append(n).append(o).append(q);

diff --git a/test/unit/expr/node_white.h b/test/unit/expr/node_white.h
index 91a3527972f257153cc41d61ea7026efe8e495ea..d851c191f55ddbf4d40239e0172d59cde3655376 100644 (file)
--- a/test/unit/expr/node_white.h
+++ b/test/unit/expr/node_white.h
@@ -62,7 +62,7 @@ public:
     NodeBuilder<> b;
     TS_ASSERT(b.d_nv->getId() == 0);
     TS_ASSERT(b.d_nv->getKind() == UNDEFINED_KIND);
-    TS_ASSERT(b.d_nv->getNumChildren() == 0);
+    TS_ASSERT_EQUALS(b.d_nv->d_nchildren, 0u);
     /* etc. */
   }
 };