diff options
author | Alex Ozdemir <aozdemir@hmc.edu> | 2020-06-19 22:45:32 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-06-19 22:45:32 -0700 |
commit | 3bc4a541b6c3a35fae987cc068e0e01937d5c4b1 (patch) | |
tree | 56f19ac241b31904cf52f46c60c1798fadc4c18f /test | |
parent | 3d44636a3080831bd8ea4c6b2d4f60adf6b37e9d (diff) |
Use traversal iterators in IntToBv (#4169)
This commit rips the traversal machinery out of Int-to-Bv, replacing it with traversal iterators.
Also, cleaned `childrenTypesChanged` a bit.
While basically I just cut out some lines, the diff is rather messy (I think the diffing tool doesn't like indentation changes).
Diffstat (limited to 'test')
-rw-r--r-- | test/unit/expr/node_traversal_black.h | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/test/unit/expr/node_traversal_black.h b/test/unit/expr/node_traversal_black.h index 02f8db6a3..6f5dfaf04 100644 --- a/test/unit/expr/node_traversal_black.h +++ b/test/unit/expr/node_traversal_black.h @@ -177,6 +177,22 @@ class NodePostorderTraversalBlack : public CxxTest::TestSuite std::copy(traversal.begin(), traversal.end(), std::back_inserter(actual)); TS_ASSERT_EQUALS(actual, expected); } + + void testSkipAll() + { + Node tb = d_nodeManager->mkConst(true); + Node eb = d_nodeManager->mkConst(false); + Node cnd = d_nodeManager->mkNode(XOR, tb, eb); + Node top = d_nodeManager->mkNode(XOR, cnd, cnd); + std::vector<TNode> expected = {}; + + auto traversal = NodeDfsIterable(top, VisitOrder::POSTORDER, + [](TNode n) { return true; }); + + std::vector<TNode> actual; + std::copy(traversal.begin(), traversal.end(), std::back_inserter(actual)); + TS_ASSERT_EQUALS(actual, expected); + } }; class NodePreorderTraversalBlack : public CxxTest::TestSuite |