test/unit/expr/node_manager_white.h

   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-2020 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 "test_utils.h"
  23 #include "util/integer.h"
  24 #include "util/rational.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   void setUp() override
  36   {
  37     d_nm = new NodeManager(NULL);
  38     d_scope = new NodeManagerScope(d_nm);
  39   }
  40
  41   void tearDown() override
  42   {
  43     delete d_scope;
  44     delete d_nm;
  45   }
  46
  47   void testMkConstRational() {
  48     Rational i("3");
  49     Node n = d_nm->mkConst(i);
  50     Node m = d_nm->mkConst(i);
  51     TS_ASSERT_EQUALS(n.getId(), m.getId());
  52   }
  53
  54   void testOversizedNodeBuilder() {
  55     NodeBuilder<> nb;
  56
  57     TS_ASSERT_THROWS_NOTHING(nb.realloc(15));
  58     TS_ASSERT_THROWS_NOTHING(nb.realloc(25));
  59     TS_ASSERT_THROWS_NOTHING(nb.realloc(256));
  60 #ifdef CVC4_ASSERTIONS
  61     TS_UTILS_EXPECT_ABORT(nb.realloc(100));
  62 #endif /* CVC4_ASSERTIONS */
  63     TS_ASSERT_THROWS_NOTHING(nb.realloc(257));
  64     TS_ASSERT_THROWS_NOTHING(nb.realloc(4000));
  65     TS_ASSERT_THROWS_NOTHING(nb.realloc(20000));
  66     TS_ASSERT_THROWS_NOTHING(nb.realloc(60000));
  67     TS_ASSERT_THROWS_NOTHING(nb.realloc(65535));
  68     TS_ASSERT_THROWS_NOTHING(nb.realloc(65536));
  69     TS_ASSERT_THROWS_NOTHING(nb.realloc(67108863));
  70 #ifdef CVC4_ASSERTIONS
  71     TS_UTILS_EXPECT_ABORT(nb.realloc(67108863));
  72 #endif /* CVC4_ASSERTIONS */
  73   }
  74
  75   void testTopologicalSort()
  76   {
  77     TypeNode boolType = d_nm->booleanType();
  78     Node i = d_nm->mkSkolem("i", boolType);
  79     Node j = d_nm->mkSkolem("j", boolType);
  80     Node n1 = d_nm->mkNode(kind::AND, j, j);
  81     Node n2 = d_nm->mkNode(kind::AND, i, n1);
  82
  83     {
  84       std::vector<NodeValue*> roots = {n1.d_nv};
  85       TS_ASSERT_EQUALS(NodeManager::TopologicalSort(roots), roots);
  86     }
  87
  88     {
  89       std::vector<NodeValue*> roots = {n2.d_nv, n1.d_nv};
  90       std::vector<NodeValue*> result = {n1.d_nv, n2.d_nv};
  91       TS_ASSERT_EQUALS(NodeManager::TopologicalSort(roots), result);
  92     }
  93   }
  94 };