test/unit/expr/node_white.h

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