GCC Code Coverage Report
Directory: . Exec Total Coverage
File: test/unit/node/node_manager_white.cpp Lines: 32 32 100.0 %
Date: 2021-03-23 Branches: 126 418 30.1 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file node_manager_white.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Aina Niemetz, 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 White box testing of CVC4::NodeManager.
13
 **
14
 ** White box testing of CVC4::NodeManager.
15
 **/
16
17
#include <string>
18
19
#include "expr/node_manager.h"
20
#include "test_node.h"
21
#include "util/integer.h"
22
#include "util/rational.h"
23
24
namespace CVC4 {
25
26
using namespace CVC4::expr;
27
28
namespace test {
29
30
12
class TestNodeWhiteNodeManager : public TestNode
31
{
32
};
33
34
12
TEST_F(TestNodeWhiteNodeManager, mkConst_rational)
35
{
36
4
  Rational i("3");
37
4
  Node n = d_nodeManager->mkConst(i);
38
4
  Node m = d_nodeManager->mkConst(i);
39
2
  ASSERT_EQ(n.getId(), m.getId());
40
}
41
42
12
TEST_F(TestNodeWhiteNodeManager, oversized_node_builder)
43
{
44
4
  NodeBuilder<> nb;
45
46
2
  ASSERT_NO_THROW(nb.realloc(15));
47
2
  ASSERT_NO_THROW(nb.realloc(25));
48
2
  ASSERT_NO_THROW(nb.realloc(256));
49
#ifdef CVC4_ASSERTIONS
50
2
  ASSERT_DEATH(nb.realloc(100), "toSize > d_nvMaxChildren");
51
#endif /* CVC4_ASSERTIONS */
52
2
  ASSERT_NO_THROW(nb.realloc(257));
53
2
  ASSERT_NO_THROW(nb.realloc(4000));
54
2
  ASSERT_NO_THROW(nb.realloc(20000));
55
2
  ASSERT_NO_THROW(nb.realloc(60000));
56
2
  ASSERT_NO_THROW(nb.realloc(65535));
57
2
  ASSERT_NO_THROW(nb.realloc(65536));
58
2
  ASSERT_NO_THROW(nb.realloc(67108863));
59
#ifdef CVC4_ASSERTIONS
60
2
  ASSERT_DEATH(nb.realloc(67108863), "toSize > d_nvMaxChildren");
61
#endif /* CVC4_ASSERTIONS */
62
}
63
64
12
TEST_F(TestNodeWhiteNodeManager, topological_sort)
65
{
66
4
  TypeNode boolType = d_nodeManager->booleanType();
67
4
  Node i = d_nodeManager->mkSkolem("i", boolType);
68
4
  Node j = d_nodeManager->mkSkolem("j", boolType);
69
4
  Node n1 = d_nodeManager->mkNode(kind::AND, j, j);
70
4
  Node n2 = d_nodeManager->mkNode(kind::AND, i, n1);
71
72
  {
73
4
    std::vector<NodeValue*> roots = {n1.d_nv};
74
2
    ASSERT_EQ(NodeManager::TopologicalSort(roots), roots);
75
  }
76
77
  {
78
4
    std::vector<NodeValue*> roots = {n2.d_nv, n1.d_nv};
79
4
    std::vector<NodeValue*> result = {n1.d_nv, n2.d_nv};
80
2
    ASSERT_EQ(NodeManager::TopologicalSort(roots), result);
81
  }
82
}
83
}  // namespace test
84
25308
}  // namespace CVC4