From 0eb82499822544f96877f317bbbcd4cb7c644614 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Sat, 27 Feb 2010 23:43:24 +0000 Subject: A bag of unrelated fixes to bring trunk more in-line with recent policy discussion (no dead code, no unimplemented unit tests...), and other fixes: * src/expr/node_builder.h: uncomment AndNodeBuilder, OrNodeBuilder, PlusNodeBuilder, and MultNodeBuilder. (These had been dead code for awhile.) * src/expr/node_value.cpp: toString() is much more reasonable now, printing S-exprs and using variable names (instead of printing raw pointer values). Next, we'll want to define a pretty-printing theory interface and perhaps hook this up to that. * test/unit/expr/node_black.h: implement testIterator(), testToString(), and testToStream(). * test/unit/expr/node_builder_black.h: implement testIterator() and testAppend(), and add some code to avoid the warnings on clear() for unused NodeBuilders. * src/expr/node_builder.h: redefine "iterator" to be over Nodes rather than over NodeValues. Doesn't make sense to expose the underlying NodeValues. This shouldn't affect anyone, no one was using NodeBuilder iterators. * fix some comments in source code --- test/unit/expr/node_black.h | 53 ++++++++++++---- test/unit/expr/node_builder_black.h | 118 ++++++++++++++++++++++++------------ 2 files changed, 121 insertions(+), 50 deletions(-) (limited to 'test/unit') diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h index 90358a622..c11d5cf86 100644 --- a/test/unit/expr/node_black.h +++ b/test/unit/expr/node_black.h @@ -17,6 +17,7 @@ //Used in some of the tests #include +#include #include "expr/expr_manager.h" #include "expr/node_value.h" @@ -449,24 +450,52 @@ public: } void testIterator(){ - /*typedef NodeValue::node_iterator iterator; */ - /*typedef NodeValue::node_iterator const_iterator; */ - - /*inline iterator begin(); */ - /*inline iterator end(); */ - /*inline const_iterator begin() const; */ - /*inline const_iterator end() const; */ + NodeBuilder<> b; + Node x = d_nodeManager->mkVar(); + Node y = d_nodeManager->mkVar(); + Node z = d_nodeManager->mkVar(); + Node n = b << x << y << z << kind::AND; + + { // iterator + Node::iterator i = n.begin(); + TS_ASSERT(*i++ == x); + TS_ASSERT(*i++ == y); + TS_ASSERT(*i++ == z); + TS_ASSERT(i == n.end()); + } - TS_WARN( "TODO: This test still needs to be written!" ); + { // same for const iterator + const Node& c = n; + Node::const_iterator i = c.begin(); + TS_ASSERT(*i++ == x); + TS_ASSERT(*i++ == y); + TS_ASSERT(*i++ == z); + TS_ASSERT(i == n.end()); + } } void testToString(){ - /*inline std::string toString() const; */ - TS_WARN( "TODO: This test still needs to be written!" ); + Node w = d_nodeManager->mkVar(NULL, "w"); + Node x = d_nodeManager->mkVar(NULL, "x"); + Node y = d_nodeManager->mkVar(NULL, "y"); + Node z = d_nodeManager->mkVar(NULL, "z"); + Node m = NodeBuilder<>() << w << x << kind::OR; + Node n = NodeBuilder<>() << m << y << z << kind::AND; + + TS_ASSERT(n.toString() == "(AND (OR w x) y z)"); } void testToStream(){ - /*inline void toStream(std::ostream&) const;*/ - TS_WARN( "TODO: This test still needs to be written!" ); + NodeBuilder<> b; + Node w = d_nodeManager->mkVar(NULL, "w"); + Node x = d_nodeManager->mkVar(NULL, "x"); + Node y = d_nodeManager->mkVar(NULL, "y"); + Node z = d_nodeManager->mkVar(NULL, "z"); + Node m = NodeBuilder<>() << x << y << kind::OR; + Node n = NodeBuilder<>() << w << m << z << kind::AND; + + stringstream sstr; + n.toStream(sstr); + TS_ASSERT(sstr.str() == "(AND w (OR x y) z)"); } }; diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h index 5dc327a67..e956806b8 100644 --- a/test/unit/expr/node_builder_black.h +++ b/test/unit/expr/node_builder_black.h @@ -24,6 +24,7 @@ #include "expr/node_manager.h" #include "expr/node.h" #include "expr/kind.h" +#include "util/Assert.h" using namespace CVC4; using namespace CVC4::kind; @@ -203,7 +204,28 @@ public: } void testIterator(){ - TS_WARN( "TODO: This test still needs to be written!" ); + NodeBuilder<> b; + Node x = d_nm->mkVar(); + Node y = d_nm->mkVar(); + Node z = d_nm->mkVar(); + b << x << y << z << kind::AND; + + { + NodeBuilder<>::iterator i = b.begin(); + TS_ASSERT(*i++ == x); + TS_ASSERT(*i++ == y); + TS_ASSERT(*i++ == z); + TS_ASSERT(i == b.end()); + } + + { + const NodeBuilder<>& c = b; + NodeBuilder<>::const_iterator i = c.begin(); + TS_ASSERT(*i++ == x); + TS_ASSERT(*i++ == y); + TS_ASSERT(*i++ == z); + TS_ASSERT(i == b.end()); + } } void testGetKind(){ @@ -241,6 +263,8 @@ public: push_back(noKind, K); TS_ASSERT_EQUALS(noKind.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(), 0); push_back(noKind, K); @@ -250,10 +274,9 @@ public: push_back(noKind, K); TS_ASSERT_EQUALS(noKind.getNumChildren(), K+K); - noKind << specKind; - Node n = noKind; - TS_ASSERT_THROWS_ANYTHING(noKind.getNumChildren();); + n = noKind; + TS_ASSERT_THROWS_ANYTHING( noKind.getNumChildren() ); } void testOperatorSquare(){ @@ -319,6 +342,7 @@ public: TS_ASSERT_EQUALS(nb.getNumChildren(), K); TS_ASSERT_DIFFERS(nb.begin(), nb.end()); + Node n = nb;// avoid warning on clear() nb.clear(); TS_ASSERT_EQUALS(nb.getKind(), UNDEFINED_KIND); @@ -332,6 +356,7 @@ public: TS_ASSERT_EQUALS(nb.getNumChildren(), K); TS_ASSERT_DIFFERS(nb.begin(), nb.end()); + n = nb;// avoid warning on clear() nb.clear(specKind); TS_ASSERT_EQUALS(nb.getKind(), specKind); @@ -339,10 +364,9 @@ public: TS_ASSERT_EQUALS(nb.begin(), nb.end()); push_back(nb, K); - Node n = nb; + n = nb;// avoid warning on clear() nb.clear(); - TS_ASSERT_EQUALS(nb.getKind(), UNDEFINED_KIND); TS_ASSERT_EQUALS(nb.getNumChildren(), 0); TS_ASSERT_EQUALS(nb.begin(), nb.end()); @@ -366,9 +390,9 @@ public: TS_ASSERT_EQUALS(modified.getKind(), specKind); NodeBuilder<> nb(specKind); - Node n = nb; + Node n = nb;// avoid warning on clear() nb.clear(PLUS); - TS_ASSERT_THROWS_ANYTHING(nb << PLUS;); + TS_ASSERT_THROWS_ANYTHING( nb << PLUS; ); NodeBuilder<> testRef; TS_ASSERT_EQUALS((testRef << specKind).getKind(), specKind); @@ -414,30 +438,53 @@ public: } void testAppend(){ - /* - NodeBuilder& append(const Node& n) { - Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion"); - Debug("prop") << "append: " << this << " " << n << "[" << n.d_ev << "]" << std::endl; - allocateEvIfNecessaryForAppend(); - NodeValue* ev = n.d_ev; - ev->inc(); - d_ev->d_children[d_ev->d_nchildren++] = ev; - return *this; - } - */ - /* - - template - NodeBuilder& append(const Iterator& begin, const Iterator& end) { - Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion"); - for(Iterator i = begin; i != end; ++i) { - append(*i); - } - return *this; - } - - */ - TS_WARN( "TODO: This test still needs to be written!" ); + Node x = d_nm->mkVar(); + Node y = d_nm->mkVar(); + Node z = d_nm->mkVar(); + Node m = d_nm->mkNode(AND, y, z, x); + Node n = d_nm->mkNode(OR, d_nm->mkNode(NOT, x), y, z); + Node o = d_nm->mkNode(XOR, y, x, z); + Node p = d_nm->mkNode(PLUS, z, d_nm->mkNode(UMINUS, x), z); + Node q = d_nm->mkNode(AND, x, z, d_nm->mkNode(NOT, y)); + + NodeBuilder<> b; + + // test append(TNode) + b.append(n).append(o).append(q); + + TS_ASSERT(b.getNumChildren() == 3); + TS_ASSERT(b[0] == n); + TS_ASSERT(b[1] == o); + TS_ASSERT(b[2] == q); + + vector v; + v.push_back(m); + v.push_back(p); + v.push_back(q); + // test append(vector) + b.append(v); + + TS_ASSERT(b.getNumChildren() == 6); + TS_ASSERT(b[0] == n); + TS_ASSERT(b[1] == o); + TS_ASSERT(b[2] == q); + TS_ASSERT(b[3] == m); + TS_ASSERT(b[4] == p); + TS_ASSERT(b[5] == q); + + // test append(iterator, iterator) + b.append(v.rbegin(), v.rend()); + + TS_ASSERT(b.getNumChildren() == 9); + TS_ASSERT(b[0] == n); + TS_ASSERT(b[1] == o); + TS_ASSERT(b[2] == q); + TS_ASSERT(b[3] == m); + TS_ASSERT(b[4] == p); + TS_ASSERT(b[5] == q); + TS_ASSERT(b[6] == q); + TS_ASSERT(b[7] == p); + TS_ASSERT(b[8] == m); } void testOperatorNodeCast(){ @@ -476,12 +523,10 @@ public: push_back(b,K/2); push_back(c,K/2); - a.toStream(astream); b.toStream(bstream); c.toStream(cstream); - astr = astream.str(); bstr = bstream.str(); cstr = cstream.str(); @@ -489,7 +534,7 @@ public: TS_ASSERT_EQUALS(astr, bstr); TS_ASSERT_DIFFERS(astr, cstr); - + Node n = a; n = b; n = c;// avoid warning on clear() a.clear(specKind); b.clear(specKind); c.clear(specKind); @@ -497,17 +542,14 @@ public: bstream.flush(); cstream.flush(); - push_back(a,2*K); push_back(b,2*K); push_back(c,2*K+1); - a.toStream(astream); b.toStream(bstream); c.toStream(cstream); - astr = astream.str(); bstr = bstream.str(); cstr = cstream.str(); -- cgit v1.2.3