diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-09-21 21:36:22 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-09-21 21:36:22 +0000 |
commit | bfa08932b23b391fafbfc18eb8033a87e802f0e1 (patch) | |
tree | d1dcba0835f0634c98beb16cb428fe66a66fd534 /test | |
parent | ea9346f840046ee20558afb2a17dd5999d45c5c9 (diff) |
some code cleanup, documentation, review of "kinded-iterator" code, and addition of a unit test
Diffstat (limited to 'test')
-rw-r--r-- | test/unit/expr/node_black.h | 46 |
1 files changed, 38 insertions, 8 deletions
diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h index f1bb7c251..fbc308597 100644 --- a/test/unit/expr/node_black.h +++ b/test/unit/expr/node_black.h @@ -473,6 +473,7 @@ public: #endif /* CVC4_ASSERTIONS */ } + // test iterators void testIterator() { NodeBuilder<> b; Node x = d_nodeManager->mkVar(*d_booleanType); @@ -498,13 +499,42 @@ public: } } + // test the special "kinded-iterator" + void testKindedIterator() { + TypeNode integerType = d_nodeManager->integerType(); + + Node x = d_nodeManager->mkVar("x", integerType); + Node y = d_nodeManager->mkVar("y", integerType); + Node z = d_nodeManager->mkVar("z", integerType); + Node plus_x_y_z = d_nodeManager->mkNode(kind::PLUS, x, y, z); + Node x_minus_y = d_nodeManager->mkNode(kind::MINUS, x, y); + + { // iterator + /* FAILING TEST: + Node::iterator i = plus_x_y_z.begin<PLUS>(); + TS_ASSERT(*i++ == x); + TS_ASSERT(*i++ == y); + TS_ASSERT(*i++ == z); + TS_ASSERT(i == plus_x_y_z.end<PLUS>()); + + i = x.begin<PLUS>(); + TS_ASSERT(*i++ == x); + TS_ASSERT(i == x.end<PLUS>()); + */ + } + + { // same for const iterator + //const Node& c = plus_x_y_z; + } + } + void testToString() { TypeNode booleanType = d_nodeManager->booleanType(); - Node w = d_nodeManager->mkVar("w",booleanType); - Node x = d_nodeManager->mkVar("x",booleanType); - Node y = d_nodeManager->mkVar("y",booleanType); - Node z = d_nodeManager->mkVar("z",booleanType); + Node w = d_nodeManager->mkVar("w", booleanType); + Node x = d_nodeManager->mkVar("x", booleanType); + Node y = d_nodeManager->mkVar("y", booleanType); + Node z = d_nodeManager->mkVar("z", booleanType); Node m = NodeBuilder<>() << w << x << kind::OR; Node n = NodeBuilder<>() << m << y << z << kind::AND; @@ -514,10 +544,10 @@ public: void testToStream() { TypeNode booleanType = d_nodeManager->booleanType(); - Node w = d_nodeManager->mkVar("w",booleanType); - Node x = d_nodeManager->mkVar("x",booleanType); - Node y = d_nodeManager->mkVar("y",booleanType); - Node z = d_nodeManager->mkVar("z",booleanType); + Node w = d_nodeManager->mkVar("w", booleanType); + Node x = d_nodeManager->mkVar("x", booleanType); + Node y = d_nodeManager->mkVar("y", booleanType); + Node z = d_nodeManager->mkVar("z", booleanType); Node m = NodeBuilder<>() << x << y << kind::OR; Node n = NodeBuilder<>() << w << m << z << kind::AND; Node o = NodeBuilder<>() << n << n << kind::XOR; |