test/unit/expr/node_self_iterator_black.h

   1 /*********************                                                        */
   2 /*! \file node_self_iterator_black.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Morgan Deters, Christopher L. Conway, 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 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
  23 using namespace CVC4;
  24 using namespace CVC4::kind;
  25 using namespace CVC4::expr;
  26 using namespace std;
  27
  28 class NodeSelfIteratorBlack : public CxxTest::TestSuite {
  29 private:
  30
  31   NodeManager* d_nodeManager;
  32   NodeManagerScope* d_scope;
  33   TypeNode* d_booleanType;
  34   TypeNode* d_realType;
  35
  36  public:
  37   void setUp() override
  38   {
  39     d_nodeManager = new NodeManager(NULL);
  40     d_scope = new NodeManagerScope(d_nodeManager);
  41     d_booleanType = new TypeNode(d_nodeManager->booleanType());
  42     d_realType = new TypeNode(d_nodeManager->realType());
  43   }
  44
  45   void tearDown() override
  46   {
  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.andNode(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 };