1 /*********************                                                        */
2 /*! \file node_manager_white.h
3  ** \verbatim
4  ** Top contributors (to current version):
5  **   Morgan Deters, Andres Noetzli, Tim King
6  ** This file is part of the CVC4 project.
7  ** Copyright (c) 2009-2019 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 <cxxtest/TestSuite.h>
18 
19 #include <string>
20 
21 #include "expr/node_manager.h"
22 #include "util/integer.h"
23 #include "util/rational.h"
24 
25 using namespace CVC4;
26 using namespace CVC4::expr;
27 
28 class NodeManagerWhite : public CxxTest::TestSuite {
29 
30   NodeManager* d_nm;
31   NodeManagerScope* d_scope;
32 
33  public:
setUp()34   void setUp() override
35   {
36     d_nm = new NodeManager(NULL);
37     d_scope = new NodeManagerScope(d_nm);
38   }
39 
tearDown()40   void tearDown() override
41   {
42     delete d_scope;
43     delete d_nm;
44   }
45 
testMkConstRational()46   void testMkConstRational() {
47     Rational i("3");
48     Node n = d_nm->mkConst(i);
49     Node m = d_nm->mkConst(i);
50     TS_ASSERT_EQUALS(n.getId(), m.getId());
51   }
52 
testOversizedNodeBuilder()53   void testOversizedNodeBuilder() {
54     NodeBuilder<> nb;
55 
56     TS_ASSERT_THROWS_NOTHING(nb.realloc(15));
57     TS_ASSERT_THROWS_NOTHING(nb.realloc(25));
58     TS_ASSERT_THROWS_NOTHING(nb.realloc(256));
59 #ifdef CVC4_ASSERTIONS
60     TS_ASSERT_THROWS(nb.realloc(100), AssertionException&);
61 #endif /* CVC4_ASSERTIONS */
62     TS_ASSERT_THROWS_NOTHING(nb.realloc(257));
63     TS_ASSERT_THROWS_NOTHING(nb.realloc(4000));
64     TS_ASSERT_THROWS_NOTHING(nb.realloc(20000));
65     TS_ASSERT_THROWS_NOTHING(nb.realloc(60000));
66     TS_ASSERT_THROWS_NOTHING(nb.realloc(65535));
67     TS_ASSERT_THROWS_NOTHING(nb.realloc(65536));
68     TS_ASSERT_THROWS_NOTHING(nb.realloc(67108863));
69 #ifdef CVC4_ASSERTIONS
70     TS_ASSERT_THROWS(nb.realloc(67108863), AssertionException&);
71 #endif /* CVC4_ASSERTIONS */
72   }
73 
testTopologicalSort()74   void testTopologicalSort()
75   {
76     TypeNode boolType = d_nm->booleanType();
77     Node i = d_nm->mkSkolem("i", boolType);
78     Node j = d_nm->mkSkolem("j", boolType);
79     Node n1 = d_nm->mkNode(kind::AND, j, j);
80     Node n2 = d_nm->mkNode(kind::AND, i, n1);
81 
82     {
83       std::vector<NodeValue*> roots = {n1.d_nv};
84       TS_ASSERT_EQUALS(NodeManager::TopologicalSort(roots), roots);
85     }
86 
87     {
88       std::vector<NodeValue*> roots = {n2.d_nv, n1.d_nv};
89       std::vector<NodeValue*> result = {n1.d_nv, n2.d_nv};
90       TS_ASSERT_EQUALS(NodeManager::TopologicalSort(roots), result);
91     }
92   }
93 };
94