test/unit/expr/node_manager_white.h

   1 /*********************                                                        */
   2 /*! \file node_manager_white.h
   3  ** \verbatim
   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
  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
  23 #include "util/rational.h"
  24 #include "util/integer.h"
  25
  26 using namespace CVC4;
  27 using namespace CVC4::expr;
  28
  29 class NodeManagerWhite : public CxxTest::TestSuite {
  30
  31   NodeManager* d_nm;
  32   NodeManagerScope* d_scope;
  33
  34 public:
  35
  36   void setUp() {
  37     d_nm = new NodeManager(NULL);
  38     d_scope = new NodeManagerScope(d_nm);
  39   }
  40
  41   void tearDown() {
  42     delete d_scope;
  43     delete d_nm;
  44   }
  45
  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
  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 };