test/unit/expr/node_white.h

   1 /*********************                                                        */
   2 /*! \file node_white.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Morgan Deters, Tim King, Dejan Jovanovic
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2018 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::Node.
  13  **
  14  ** White box testing of CVC4::Node.
  15  **/
  16
  17 #include <cxxtest/TestSuite.h>
  18
  19 #include <string>
  20
  21 #include "base/cvc4_assert.h"
  22 #include "expr/node.h"
  23 #include "expr/node_builder.h"
  24 #include "expr/node_manager.h"
  25 #include "expr/node_value.h"
  26
  27 using namespace CVC4;
  28 using namespace CVC4::kind;
  29 using namespace CVC4::expr;
  30 using namespace std;
  31
  32 class NodeWhite : public CxxTest::TestSuite {
  33
  34   NodeManager* d_nm;
  35   NodeManagerScope* d_scope;
  36
  37  public:
  38   void setUp() override
  39   {
  40     d_nm = new NodeManager(NULL);
  41     d_scope = new NodeManagerScope(d_nm);
  42   }
  43
  44   void tearDown() override
  45   {
  46     delete d_scope;
  47     delete d_nm;
  48   }
  49
  50   void testNull() {
  51     TS_ASSERT_EQUALS(Node::null(), Node::s_null);
  52   }
  53
  54   void testCopyCtor() {
  55     Node e(Node::s_null);
  56   }
  57
  58   void testBuilder() {
  59     NodeBuilder<> b;
  60     TS_ASSERT(b.d_nv->getId() == 0);
  61     TS_ASSERT(b.d_nv->getKind() == UNDEFINED_KIND);
  62     TS_ASSERT_EQUALS(b.d_nv->d_nchildren, 0u);
  63     /* etc. */
  64   }
  65
  66   void testIterators() {
  67     Node x = d_nm->mkVar("x", d_nm->integerType());
  68     Node y = d_nm->mkVar("y", d_nm->integerType());
  69     Node x_plus_y = d_nm->mkNode(PLUS, x, y);
  70     Node two = d_nm->mkConst(Rational(2));
  71     Node x_times_2 = d_nm->mkNode(MULT, x, two);
  72
  73     Node n = d_nm->mkNode(PLUS, x_times_2, x_plus_y, y);
  74
  75     Node::iterator i;
  76
  77     i = find(n.begin(), n.end(), x_plus_y);
  78     TS_ASSERT(i != n.end());
  79     TS_ASSERT(*i == x_plus_y);
  80
  81     i = find(n.begin(), n.end(), x);
  82     TS_ASSERT(i == n.end());
  83
  84     i = find(x_times_2.begin(), x_times_2.end(), two);
  85     TS_ASSERT(i != x_times_2.end());
  86     TS_ASSERT(*i == two);
  87
  88     i = find(n.begin(), n.end(), y);
  89     TS_ASSERT(i != n.end());
  90     TS_ASSERT(*i == y);
  91
  92     vector<Node> v;
  93     copy(n.begin(), n.end(), back_inserter(v));
  94     TS_ASSERT(n.getNumChildren() == v.size());
  95     TS_ASSERT(3 == v.size());
  96     TS_ASSERT(v[0] == x_times_2);
  97     TS_ASSERT(v[1] == x_plus_y);
  98     TS_ASSERT(v[2] == y);
  99   }
 100 };