test/unit/expr/node_white.cpp

   1 /*********************                                                        */
   2 /*! \file node_white.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Aina Niemetz, Morgan Deters
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 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 White box testing of CVC4::Node.
  13  **
  14  ** White box testing of CVC4::Node.
  15  **/
  16
  17 #include <string>
  18
  19 #include "base/check.h"
  20 #include "test_node.h"
  21
  22 namespace CVC4 {
  23
  24 using namespace kind;
  25 using namespace expr;
  26
  27 namespace test {
  28
  29 class TestNodeWhiteNode : public TestNodeWhite
  30 {
  31 };
  32
  33 TEST_F(TestNodeWhiteNode, null) { ASSERT_EQ(Node::null(), Node::s_null); }
  34
  35 TEST_F(TestNodeWhiteNode, copy_ctor) { Node e(Node::s_null); }
  36
  37 TEST_F(TestNodeWhiteNode, builder)
  38 {
  39   NodeBuilder<> b;
  40   ASSERT_TRUE(b.d_nv->getId() == 0);
  41   ASSERT_TRUE(b.d_nv->getKind() == UNDEFINED_KIND);
  42   ASSERT_EQ(b.d_nv->d_nchildren, 0u);
  43   /* etc. */
  44 }
  45
  46 TEST_F(TestNodeWhiteNode, iterators)
  47 {
  48   Node x = d_nodeManager->mkVar("x", d_nodeManager->integerType());
  49   Node y = d_nodeManager->mkVar("y", d_nodeManager->integerType());
  50   Node x_plus_y = d_nodeManager->mkNode(PLUS, x, y);
  51   Node two = d_nodeManager->mkConst(Rational(2));
  52   Node x_times_2 = d_nodeManager->mkNode(MULT, x, two);
  53
  54   Node n = d_nodeManager->mkNode(PLUS, x_times_2, x_plus_y, y);
  55
  56   Node::iterator i;
  57
  58   i = std::find(n.begin(), n.end(), x_plus_y);
  59   ASSERT_TRUE(i != n.end());
  60   ASSERT_TRUE(*i == x_plus_y);
  61
  62   i = std::find(n.begin(), n.end(), x);
  63   ASSERT_TRUE(i == n.end());
  64
  65   i = std::find(x_times_2.begin(), x_times_2.end(), two);
  66   ASSERT_TRUE(i != x_times_2.end());
  67   ASSERT_TRUE(*i == two);
  68
  69   i = std::find(n.begin(), n.end(), y);
  70   ASSERT_TRUE(i != n.end());
  71   ASSERT_TRUE(*i == y);
  72
  73   std::vector<Node> v;
  74   copy(n.begin(), n.end(), back_inserter(v));
  75   ASSERT_EQ(n.getNumChildren(), v.size());
  76   ASSERT_EQ(3, v.size());
  77   ASSERT_EQ(v[0], x_times_2);
  78   ASSERT_EQ(v[1], x_plus_y);
  79   ASSERT_EQ(v[2], y);
  80 }
  81 }  // namespace test
  82 }  // namespace CVC4