1 /********************* */
2 /*! \file node_manager_white.h
4 ** Original author: Morgan Deters
5 ** Major contributors: none
6 ** Minor contributors (to current version): Tim King
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2014 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** information.\endverbatim
12 ** \brief White box testing of CVC4::NodeManager.
14 ** White box testing of CVC4::NodeManager.
17 #include <cxxtest/TestSuite.h>
21 #include "expr/node_manager.h"
23 #include "util/rational.h"
24 #include "util/integer.h"
27 using namespace CVC4::expr
;
29 class NodeManagerWhite
: public CxxTest::TestSuite
{
32 NodeManagerScope
* d_scope
;
37 d_nm
= new NodeManager(NULL
);
38 d_scope
= new NodeManagerScope(d_nm
);
46 void testMkConstRational() {
48 Node n
= d_nm
->mkConst(i
);
49 Node m
= d_nm
->mkConst(i
);
50 TS_ASSERT_EQUALS(n
.getId(), m
.getId());
53 void testOversizedNodeBuilder() {
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 */