test/unit/expr/node_self_iterator_black.h

   1 /*********************                                                        */
   2 /*! \file node_self_iterator_black.h
   3  ** \verbatim
   4  ** Original author: Morgan Deters
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): none
   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 Black box testing of CVC4::expr::NodeSelfIterator
  13  **
  14  ** Black box testing of CVC4::expr::NodeSelfIterator
  15  **/
  16
  17 #include <cxxtest/TestSuite.h>
  18
  19 #include "expr/node.h"
  20 #include "expr/node_self_iterator.h"
  21 #include "expr/node_builder.h"
  22 #include "expr/convenience_node_builders.h"
  23
  24 using namespace CVC4;
  25 using namespace CVC4::kind;
  26 using namespace CVC4::expr;
  27 using namespace std;
  28
  29 class NodeSelfIteratorBlack : public CxxTest::TestSuite {
  30 private:
  31
  32   NodeManager* d_nodeManager;
  33   NodeManagerScope* d_scope;
  34   TypeNode* d_booleanType;
  35   TypeNode* d_realType;
  36
  37 public:
  38
  39   void setUp() {
  40     d_nodeManager = new NodeManager(NULL);
  41     d_scope = new NodeManagerScope(d_nodeManager);
  42     d_booleanType = new TypeNode(d_nodeManager->booleanType());
  43     d_realType = new TypeNode(d_nodeManager->realType());
  44   }
  45
  46   void tearDown() {
  47     delete d_booleanType;
  48     delete d_scope;
  49     delete d_nodeManager;
  50   }
  51
  52   void testSelfIteration() {
  53     Node x = d_nodeManager->mkSkolem("x", *d_booleanType);
  54     Node y = d_nodeManager->mkSkolem("y", *d_booleanType);
  55     Node x_and_y = x && y;
  56     NodeSelfIterator i = x_and_y, j = NodeSelfIterator::self(x_and_y);
  57     TS_ASSERT(i != x_and_y.end());
  58     TS_ASSERT(j != x_and_y.end());
  59     TS_ASSERT(*i == x_and_y);
  60     TS_ASSERT(*j == x_and_y);
  61     TS_ASSERT(*i++ == x_and_y);
  62     TS_ASSERT(*j++ == x_and_y);
  63     TS_ASSERT(i == NodeSelfIterator::selfEnd(x_and_y));
  64     TS_ASSERT(j == NodeSelfIterator::selfEnd(x_and_y));
  65     TS_ASSERT(i == x_and_y.end());
  66     TS_ASSERT(j == x_and_y.end());
  67
  68     i = x_and_y.begin();
  69     TS_ASSERT(i != x_and_y.end());
  70     TS_ASSERT(*i == x);
  71     TS_ASSERT(*++i == y);
  72     TS_ASSERT(++i == x_and_y.end());
  73   }
  74
  75 };