test/unit/node/node_traversal_black.cpp

   1 /*********************                                                        */
   2 /*! \file node_traversal_black.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Aina Niemetz, Alex Ozdemir, Andres Noetzli
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief Black box testing of node traversal iterators.
  13  **/
  14
  15 #include <algorithm>
  16 #include <cstddef>
  17 #include <iterator>
  18 #include <sstream>
  19 #include <string>
  20 #include <vector>
  21
  22 #include "expr/node.h"
  23 #include "expr/node_builder.h"
  24 #include "expr/node_manager.h"
  25 #include "expr/node_traversal.h"
  26 #include "expr/node_value.h"
  27 #include "test_node.h"
  28
  29 namespace cvc5 {
  30
  31 using namespace kind;
  32
  33 namespace test {
  34
  35 class TestNodeBlackNodeTraversalPostorder : public TestNode
  36 {
  37 };
  38
  39 class TestNodeBlackNodeTraversalPreorder : public TestNode
  40 {
  41 };
  42
  43 TEST_F(TestNodeBlackNodeTraversalPostorder, preincrement_iteration)
  44 {
  45   const Node tb = d_nodeManager->mkConst(true);
  46   const Node eb = d_nodeManager->mkConst(false);
  47   const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
  48
  49   auto traversal = NodeDfsIterable(cnd, VisitOrder::POSTORDER);
  50   NodeDfsIterator i = traversal.begin();
  51   NodeDfsIterator end = traversal.end();
  52   ASSERT_EQ(*i, tb);
  53   ASSERT_FALSE(i == end);
  54   ++i;
  55   ASSERT_EQ(*i, eb);
  56   ASSERT_FALSE(i == end);
  57   ++i;
  58   ASSERT_EQ(*i, cnd);
  59   ASSERT_FALSE(i == end);
  60   ++i;
  61   ASSERT_TRUE(i == end);
  62 }
  63
  64 TEST_F(TestNodeBlackNodeTraversalPostorder, postincrement_iteration)
  65 {
  66   const Node tb = d_nodeManager->mkConst(true);
  67   const Node eb = d_nodeManager->mkConst(false);
  68   const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
  69
  70   auto traversal = NodeDfsIterable(cnd, VisitOrder::POSTORDER);
  71   NodeDfsIterator i = traversal.begin();
  72   NodeDfsIterator end = traversal.end();
  73   ASSERT_EQ(*(i++), tb);
  74   ASSERT_EQ(*(i++), eb);
  75   ASSERT_EQ(*(i++), cnd);
  76   ASSERT_TRUE(i == end);
  77 }
  78
  79 TEST_F(TestNodeBlackNodeTraversalPostorder, postorder_is_default)
  80 {
  81   const Node tb = d_nodeManager->mkConst(true);
  82   const Node eb = d_nodeManager->mkConst(false);
  83   const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
  84
  85   auto traversal = NodeDfsIterable(cnd);
  86   NodeDfsIterator i = traversal.begin();
  87   NodeDfsIterator end = traversal.end();
  88   ASSERT_EQ(*i, tb);
  89   ASSERT_FALSE(i == end);
  90 }
  91
  92 TEST_F(TestNodeBlackNodeTraversalPostorder, range_for_loop)
  93 {
  94   const Node tb = d_nodeManager->mkConst(true);
  95   const Node eb = d_nodeManager->mkConst(false);
  96   const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
  97
  98   size_t count = 0;
  99   for (auto i : NodeDfsIterable(cnd, VisitOrder::POSTORDER))
 100   {
 101     ++count;
 102   }
 103   ASSERT_EQ(count, 3);
 104 }
 105
 106 TEST_F(TestNodeBlackNodeTraversalPostorder, count_if_with_loop)
 107 {
 108   const Node tb = d_nodeManager->mkConst(true);
 109   const Node eb = d_nodeManager->mkConst(false);
 110   const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
 111
 112   size_t count = 0;
 113   for (auto i : NodeDfsIterable(cnd, VisitOrder::POSTORDER))
 114   {
 115     if (i.isConst())
 116     {
 117       ++count;
 118     }
 119   }
 120   ASSERT_EQ(count, 2);
 121 }
 122
 123 TEST_F(TestNodeBlackNodeTraversalPostorder, stl_count_if)
 124 {
 125   const Node tb = d_nodeManager->mkConst(true);
 126   const Node eb = d_nodeManager->mkConst(false);
 127   const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
 128   const Node top = d_nodeManager->mkNode(XOR, cnd, cnd);
 129
 130   auto traversal = NodeDfsIterable(top, VisitOrder::POSTORDER);
 131
 132   size_t count = std::count_if(
 133       traversal.begin(), traversal.end(), [](TNode n) { return n.isConst(); });
 134   ASSERT_EQ(count, 2);
 135 }
 136
 137 TEST_F(TestNodeBlackNodeTraversalPostorder, stl_copy)
 138 {
 139   const Node tb = d_nodeManager->mkConst(true);
 140   const Node eb = d_nodeManager->mkConst(false);
 141   const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
 142   const Node top = d_nodeManager->mkNode(XOR, cnd, cnd);
 143   std::vector<TNode> expected = {tb, eb, cnd, top};
 144
 145   auto traversal = NodeDfsIterable(top, VisitOrder::POSTORDER);
 146
 147   std::vector<TNode> actual;
 148   std::copy(traversal.begin(), traversal.end(), std::back_inserter(actual));
 149   ASSERT_EQ(actual, expected);
 150 }
 151
 152 TEST_F(TestNodeBlackNodeTraversalPostorder, skip_if)
 153 {
 154   const Node tb = d_nodeManager->mkConst(true);
 155   const Node eb = d_nodeManager->mkConst(false);
 156   const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
 157   const Node top = d_nodeManager->mkNode(XOR, cnd, cnd);
 158   std::vector<TNode> expected = {top};
 159
 160   auto traversal = NodeDfsIterable(
 161       top, VisitOrder::POSTORDER, [&cnd](TNode n) { return n == cnd; });
 162
 163   std::vector<TNode> actual;
 164   std::copy(traversal.begin(), traversal.end(), std::back_inserter(actual));
 165   ASSERT_EQ(actual, expected);
 166 }
 167
 168 TEST_F(TestNodeBlackNodeTraversalPostorder, skip_all)
 169 {
 170   const Node tb = d_nodeManager->mkConst(true);
 171   const Node eb = d_nodeManager->mkConst(false);
 172   const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
 173   const Node top = d_nodeManager->mkNode(XOR, cnd, cnd);
 174   std::vector<TNode> expected = {};
 175
 176   auto traversal =
 177       NodeDfsIterable(top, VisitOrder::POSTORDER, [](TNode n) { return true; });
 178
 179   std::vector<TNode> actual;
 180   std::copy(traversal.begin(), traversal.end(), std::back_inserter(actual));
 181   ASSERT_EQ(actual, expected);
 182 }
 183
 184 TEST_F(TestNodeBlackNodeTraversalPreorder, preincrement_iteration)
 185 {
 186   const Node tb = d_nodeManager->mkConst(true);
 187   const Node eb = d_nodeManager->mkConst(false);
 188   const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
 189
 190   auto traversal = NodeDfsIterable(cnd, VisitOrder::PREORDER);
 191   NodeDfsIterator i = traversal.begin();
 192   NodeDfsIterator end = traversal.end();
 193   ASSERT_EQ(*i, cnd);
 194   ASSERT_FALSE(i == end);
 195   ++i;
 196   ASSERT_EQ(*i, tb);
 197   ASSERT_FALSE(i == end);
 198   ++i;
 199   ASSERT_EQ(*i, eb);
 200   ASSERT_FALSE(i == end);
 201   ++i;
 202   ASSERT_TRUE(i == end);
 203 }
 204
 205 TEST_F(TestNodeBlackNodeTraversalPreorder, postincrement_iteration)
 206 {
 207   const Node tb = d_nodeManager->mkConst(true);
 208   const Node eb = d_nodeManager->mkConst(false);
 209   const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
 210
 211   auto traversal = NodeDfsIterable(cnd, VisitOrder::PREORDER);
 212   NodeDfsIterator i = traversal.begin();
 213   NodeDfsIterator end = traversal.end();
 214   ASSERT_EQ(*(i++), cnd);
 215   ASSERT_EQ(*(i++), tb);
 216   ASSERT_EQ(*(i++), eb);
 217   ASSERT_TRUE(i == end);
 218 }
 219
 220 TEST_F(TestNodeBlackNodeTraversalPreorder, range_for_loop)
 221 {
 222   const Node tb = d_nodeManager->mkConst(true);
 223   const Node eb = d_nodeManager->mkConst(false);
 224   const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
 225
 226   size_t count = 0;
 227   for (auto i : NodeDfsIterable(cnd, VisitOrder::PREORDER))
 228   {
 229     ++count;
 230   }
 231   ASSERT_EQ(count, 3);
 232 }
 233
 234 TEST_F(TestNodeBlackNodeTraversalPreorder, count_if_with_loop)
 235 {
 236   const Node tb = d_nodeManager->mkConst(true);
 237   const Node eb = d_nodeManager->mkConst(false);
 238   const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
 239
 240   size_t count = 0;
 241   for (auto i : NodeDfsIterable(cnd, VisitOrder::PREORDER))
 242   {
 243     if (i.isConst())
 244     {
 245       ++count;
 246     }
 247   }
 248   ASSERT_EQ(count, 2);
 249 }
 250
 251 TEST_F(TestNodeBlackNodeTraversalPreorder, stl_count_if)
 252 {
 253   const Node tb = d_nodeManager->mkConst(true);
 254   const Node eb = d_nodeManager->mkConst(false);
 255   const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
 256   const Node top = d_nodeManager->mkNode(XOR, cnd, cnd);
 257
 258   auto traversal = NodeDfsIterable(top, VisitOrder::PREORDER);
 259
 260   size_t count = std::count_if(
 261       traversal.begin(), traversal.end(), [](TNode n) { return n.isConst(); });
 262   ASSERT_EQ(count, 2);
 263 }
 264
 265 TEST_F(TestNodeBlackNodeTraversalPreorder, stl_copy)
 266 {
 267   const Node tb = d_nodeManager->mkConst(true);
 268   const Node eb = d_nodeManager->mkConst(false);
 269   const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
 270   const Node top = d_nodeManager->mkNode(XOR, cnd, cnd);
 271   std::vector<TNode> expected = {top, cnd, tb, eb};
 272
 273   auto traversal = NodeDfsIterable(top, VisitOrder::PREORDER);
 274
 275   std::vector<TNode> actual;
 276   std::copy(traversal.begin(), traversal.end(), std::back_inserter(actual));
 277   ASSERT_EQ(actual, expected);
 278 }
 279
 280 TEST_F(TestNodeBlackNodeTraversalPreorder, skip_if)
 281 {
 282   const Node tb = d_nodeManager->mkConst(true);
 283   const Node eb = d_nodeManager->mkConst(false);
 284   const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
 285   const Node top = d_nodeManager->mkNode(XOR, cnd, cnd);
 286   std::vector<TNode> expected = {top, cnd, eb};
 287
 288   auto traversal = NodeDfsIterable(
 289       top, VisitOrder::PREORDER, [&tb](TNode n) { return n == tb; });
 290
 291   std::vector<TNode> actual;
 292   std::copy(traversal.begin(), traversal.end(), std::back_inserter(actual));
 293   ASSERT_EQ(actual, expected);
 294 }
 295 }  // namespace test
 296 }  // namespace cvc5