From: Morgan Deters Date: Thu, 3 Jun 2010 13:22:57 +0000 (+0000) Subject: * Added NodeBuilder<>::getChild() to make interface more consistent X-Git-Tag: cvc5-1.0.0~9007 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=25a999fdfd2e38098d0c8dc6b788c9debe4401d5;p=cvc5.git * 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 fcc6bb364..877c50d82 100644 --- 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 >(); } @@ -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 >(); } @@ -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 de8e7a985..2b79c5045 100644 --- 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 56c0eae26..1f283f476 100644 --- 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 a1887118c..8bde4b047 100644 --- 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 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 ws_kind(specKind); TS_ASSERT_EQUALS(ws_kind.getKind(), specKind); @@ -120,8 +123,9 @@ public: NodeBuilder 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 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 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 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 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 ws; + NodeBuilder 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 91a352797..d851c191f 100644 --- 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. */ } };