GCC Code Coverage Report
Directory: . Exec Total Coverage
File: test/unit/node/node_white.cpp Lines: 35 35 100.0 %
Date: 2021-03-22 Branches: 108 344 31.4 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file node_white.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Aina Niemetz
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 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
16
class TestNodeWhiteNode : public TestNode
30
{
31
};
32
33
13
TEST_F(TestNodeWhiteNode, null) { ASSERT_EQ(Node::null(), Node::s_null); }
34
35
13
TEST_F(TestNodeWhiteNode, copy_ctor) { Node e(Node::s_null); }
36
37
13
TEST_F(TestNodeWhiteNode, builder)
38
{
39
4
  NodeBuilder<> b;
40
2
  ASSERT_TRUE(b.d_nv->getId() == 0);
41
2
  ASSERT_TRUE(b.d_nv->getKind() == UNDEFINED_KIND);
42
2
  ASSERT_EQ(b.d_nv->d_nchildren, 0u);
43
  /* etc. */
44
}
45
46
13
TEST_F(TestNodeWhiteNode, iterators)
47
{
48
4
  Node x = d_nodeManager->mkVar("x", d_nodeManager->integerType());
49
4
  Node y = d_nodeManager->mkVar("y", d_nodeManager->integerType());
50
4
  Node x_plus_y = d_nodeManager->mkNode(PLUS, x, y);
51
4
  Node two = d_nodeManager->mkConst(Rational(2));
52
4
  Node x_times_2 = d_nodeManager->mkNode(MULT, x, two);
53
54
4
  Node n = d_nodeManager->mkNode(PLUS, x_times_2, x_plus_y, y);
55
56
2
  Node::iterator i;
57
58
2
  i = std::find(n.begin(), n.end(), x_plus_y);
59
2
  ASSERT_TRUE(i != n.end());
60
2
  ASSERT_TRUE(*i == x_plus_y);
61
62
2
  i = std::find(n.begin(), n.end(), x);
63
2
  ASSERT_TRUE(i == n.end());
64
65
2
  i = std::find(x_times_2.begin(), x_times_2.end(), two);
66
2
  ASSERT_TRUE(i != x_times_2.end());
67
2
  ASSERT_TRUE(*i == two);
68
69
2
  i = std::find(n.begin(), n.end(), y);
70
2
  ASSERT_TRUE(i != n.end());
71
2
  ASSERT_TRUE(*i == y);
72
73
4
  std::vector<Node> v;
74
2
  copy(n.begin(), n.end(), back_inserter(v));
75
2
  ASSERT_EQ(n.getNumChildren(), v.size());
76
2
  ASSERT_EQ(3, v.size());
77
2
  ASSERT_EQ(v[0], x_times_2);
78
2
  ASSERT_EQ(v[1], x_plus_y);
79
2
  ASSERT_EQ(v[2], y);
80
}
81
}  // namespace test
82
33947
}  // namespace CVC4