test/unit/expr/node_manager_black.h

   1 /*********************                                                        */
   2 /*! \file node_manager_black.h
   3  ** \verbatim
   4  ** Original author: Christopher L. Conway
   5  ** Major contributors: Morgan Deters, Dejan Jovanovic
   6  ** Minor contributors (to current version): Tim King
   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::NodeManager.
  13  **
  14  ** White box testing of CVC4::NodeManager.
  15  **/
  16
  17 #include <cxxtest/TestSuite.h>
  18
  19 #include <string>
  20 #include <vector>
  21
  22 #include "expr/node_manager.h"
  23 #include "expr/node_manager_attributes.h"
  24 #include "context/context.h"
  25
  26 #include "util/rational.h"
  27 #include "util/integer.h"
  28
  29 using namespace CVC4;
  30 using namespace CVC4::expr;
  31 using namespace CVC4::kind;
  32 using namespace CVC4::context;
  33
  34 class NodeManagerBlack : public CxxTest::TestSuite {
  35
  36   Context* d_context;
  37   NodeManager* d_nodeManager;
  38   NodeManagerScope* d_scope;
  39
  40 public:
  41
  42   void setUp() {
  43     d_context = new Context;
  44     d_nodeManager = new NodeManager(d_context, NULL);
  45     d_scope = new NodeManagerScope(d_nodeManager);
  46   }
  47
  48   void tearDown() {
  49     delete d_scope;
  50     delete d_nodeManager;
  51     delete d_context;
  52   }
  53
  54   void testMkNodeNot() {
  55     Node x = d_nodeManager->mkSkolem("x",d_nodeManager->booleanType());
  56     Node n = d_nodeManager->mkNode(NOT, x);
  57     TS_ASSERT_EQUALS( n.getNumChildren(), 1u );
  58     TS_ASSERT_EQUALS( n.getKind(), NOT);
  59     TS_ASSERT_EQUALS( n[0], x);
  60   }
  61
  62   void testMkNodeBinary() {
  63     Node x = d_nodeManager->mkSkolem("x",d_nodeManager->booleanType());
  64     Node y = d_nodeManager->mkSkolem("y",d_nodeManager->booleanType());
  65     Node n = d_nodeManager->mkNode(IMPLIES, x, y);
  66     TS_ASSERT_EQUALS( n.getNumChildren(), 2u );
  67     TS_ASSERT_EQUALS( n.getKind(), IMPLIES);
  68     TS_ASSERT_EQUALS( n[0], x);
  69     TS_ASSERT_EQUALS( n[1], y);
  70   }
  71
  72   void testMkNodeThreeChildren() {
  73     Node x = d_nodeManager->mkSkolem("x",d_nodeManager->booleanType());
  74     Node y = d_nodeManager->mkSkolem("y",d_nodeManager->booleanType());
  75     Node z = d_nodeManager->mkSkolem("z",d_nodeManager->booleanType());
  76     Node n = d_nodeManager->mkNode(AND, x, y, z);
  77     TS_ASSERT_EQUALS( n.getNumChildren(), 3u );
  78     TS_ASSERT_EQUALS( n.getKind(), AND);
  79     TS_ASSERT_EQUALS( n[0], x);
  80     TS_ASSERT_EQUALS( n[1], y);
  81     TS_ASSERT_EQUALS( n[2], z);
  82   }
  83
  84   void testMkNodeFourChildren() {
  85     Node x1 = d_nodeManager->mkSkolem("x1",d_nodeManager->booleanType());
  86     Node x2 = d_nodeManager->mkSkolem("x2",d_nodeManager->booleanType());
  87     Node x3 = d_nodeManager->mkSkolem("x3",d_nodeManager->booleanType());
  88     Node x4 = d_nodeManager->mkSkolem("x4",d_nodeManager->booleanType());
  89     Node n = d_nodeManager->mkNode(AND, x1, x2, x3, x4);
  90     TS_ASSERT_EQUALS( n.getNumChildren(), 4u );
  91     TS_ASSERT_EQUALS( n.getKind(), AND );
  92     TS_ASSERT_EQUALS( n[0], x1 );
  93     TS_ASSERT_EQUALS( n[1], x2 );
  94     TS_ASSERT_EQUALS( n[2], x3 );
  95     TS_ASSERT_EQUALS( n[3], x4 );
  96   }
  97
  98   void testMkNodeFiveChildren() {
  99     Node x1 = d_nodeManager->mkSkolem("x1",d_nodeManager->booleanType());
 100     Node x2 = d_nodeManager->mkSkolem("x2",d_nodeManager->booleanType());
 101     Node x3 = d_nodeManager->mkSkolem("x3",d_nodeManager->booleanType());
 102     Node x4 = d_nodeManager->mkSkolem("x4",d_nodeManager->booleanType());
 103     Node x5 = d_nodeManager->mkSkolem("x5",d_nodeManager->booleanType());
 104     Node n = d_nodeManager->mkNode(AND, x1, x2, x3, x4, x5);
 105     TS_ASSERT_EQUALS( n.getNumChildren(), 5u );
 106     TS_ASSERT_EQUALS( n.getKind(), AND);
 107     TS_ASSERT_EQUALS( n[0], x1);
 108     TS_ASSERT_EQUALS( n[1], x2);
 109     TS_ASSERT_EQUALS( n[2], x3);
 110     TS_ASSERT_EQUALS( n[3], x4);
 111     TS_ASSERT_EQUALS( n[4], x5);
 112   }
 113
 114   void testMkNodeVectorOfNodeChildren() {
 115     Node x1 = d_nodeManager->mkSkolem("x1",d_nodeManager->booleanType());
 116     Node x2 = d_nodeManager->mkSkolem("x2",d_nodeManager->booleanType());
 117     Node x3 = d_nodeManager->mkSkolem("x3",d_nodeManager->booleanType());
 118     std::vector<Node> args;
 119     args.push_back(x1);
 120     args.push_back(x2);
 121     args.push_back(x3);
 122     Node n = d_nodeManager->mkNode(AND, args);
 123     TS_ASSERT_EQUALS( n.getNumChildren(), args.size() );
 124     TS_ASSERT_EQUALS( n.getKind(), AND);
 125     for( unsigned i = 0; i < args.size(); ++i ) {
 126       TS_ASSERT_EQUALS( n[i], args[i]);
 127     }
 128   }
 129
 130   void testMkNodeVectorOfTNodeChildren() {
 131     Node x1 = d_nodeManager->mkSkolem("x1",d_nodeManager->booleanType());
 132     Node x2 = d_nodeManager->mkSkolem("x2",d_nodeManager->booleanType());
 133     Node x3 = d_nodeManager->mkSkolem("x3",d_nodeManager->booleanType());
 134     std::vector<TNode> args;
 135     args.push_back(x1);
 136     args.push_back(x2);
 137     args.push_back(x3);
 138     Node n = d_nodeManager->mkNode(AND, args);
 139     TS_ASSERT_EQUALS( n.getNumChildren(), args.size() );
 140     TS_ASSERT_EQUALS( n.getKind(), AND);
 141     for( unsigned i = 0; i < args.size(); ++i ) {
 142       TS_ASSERT_EQUALS( n[i], args[i]);
 143     }
 144   }
 145
 146   void testMkVarWithName() {
 147     TypeNode booleanType = d_nodeManager->booleanType();
 148     Node x = d_nodeManager->mkSkolem("x", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
 149     TS_ASSERT_EQUALS(x.getKind(),SKOLEM);
 150     TS_ASSERT_EQUALS(x.getNumChildren(),0u);
 151     TS_ASSERT_EQUALS(x.getAttribute(VarNameAttr()),"x");
 152     TS_ASSERT_EQUALS(x.getType(),booleanType);
 153   }
 154
 155   void testMkConstBool() {
 156     Node tt = d_nodeManager->mkConst(true);
 157     TS_ASSERT_EQUALS(tt.getConst<bool>(),true);
 158     Node ff = d_nodeManager->mkConst(false);
 159     TS_ASSERT_EQUALS(ff.getConst<bool>(),false);
 160   }
 161
 162   void testMkConstRat() {
 163     Rational r("3/2");
 164     Node n = d_nodeManager->mkConst(r);
 165     TS_ASSERT_EQUALS(n.getConst<Rational>(),r);
 166   }
 167
 168   void testHasOperator() {
 169     TS_ASSERT( NodeManager::hasOperator(AND) );
 170     TS_ASSERT( NodeManager::hasOperator(OR) );
 171     TS_ASSERT( NodeManager::hasOperator(NOT) );
 172     TS_ASSERT( NodeManager::hasOperator(APPLY_UF) );
 173     TS_ASSERT( !NodeManager::hasOperator(VARIABLE) );
 174   }
 175
 176   void testBooleanType() {
 177     TypeNode t = d_nodeManager->booleanType();
 178     TypeNode t2 = d_nodeManager->booleanType();
 179     TypeNode t3 = d_nodeManager->mkSort("T");
 180     TS_ASSERT( t.isBoolean() );
 181     TS_ASSERT( !t.isFunction() );
 182     TS_ASSERT( !t.isNull() );
 183     TS_ASSERT( !t.isPredicate() );
 184     TS_ASSERT( !t.isSort() );
 185     TS_ASSERT_EQUALS(t, t2);
 186     TS_ASSERT( t != t3 );
 187
 188     TypeNode bt = t;
 189     TS_ASSERT_EQUALS( bt, t);
 190   }
 191
 192   void testMkFunctionTypeBoolToBool() {
 193     TypeNode booleanType = d_nodeManager->booleanType();
 194     TypeNode t = d_nodeManager->mkFunctionType(booleanType,booleanType);
 195     TypeNode t2 = d_nodeManager->mkFunctionType(booleanType,booleanType);
 196
 197     TS_ASSERT( !t.isBoolean() );
 198     TS_ASSERT( t.isFunction() );
 199     TS_ASSERT( !t.isNull() );
 200     TS_ASSERT( t.isPredicate() );
 201     TS_ASSERT( !t.isSort() );
 202
 203     TS_ASSERT_EQUALS( t, t2 );
 204
 205     TypeNode ft = t;
 206     TS_ASSERT_EQUALS( ft, t );
 207     TS_ASSERT_EQUALS(ft.getArgTypes().size(), 1u);
 208     TS_ASSERT_EQUALS(ft.getArgTypes()[0], booleanType);
 209     TS_ASSERT_EQUALS(ft.getRangeType(), booleanType);
 210
 211   }
 212
 213   void testMkFunctionTypeVectorOfArgsWithReturnType() {
 214     TypeNode a = d_nodeManager->mkSort();
 215     TypeNode b = d_nodeManager->mkSort();
 216     TypeNode c = d_nodeManager->mkSort();
 217
 218     std::vector<TypeNode> argTypes;
 219     argTypes.push_back(a);
 220     argTypes.push_back(b);
 221
 222     TypeNode t = d_nodeManager->mkFunctionType(argTypes,c);
 223     TypeNode t2 = d_nodeManager->mkFunctionType(argTypes,c);
 224
 225     TS_ASSERT( !t.isBoolean() );
 226     TS_ASSERT( t.isFunction() );
 227     TS_ASSERT( !t.isNull() );
 228     TS_ASSERT( !t.isPredicate() );
 229     TS_ASSERT( !t.isSort() );
 230
 231     TS_ASSERT_EQUALS( t, t2 );
 232
 233     TypeNode ft = t;
 234     TS_ASSERT_EQUALS( ft, t );
 235     TS_ASSERT_EQUALS(ft.getArgTypes().size(), argTypes.size());
 236     TS_ASSERT_EQUALS(ft.getArgTypes()[0], a);
 237     TS_ASSERT_EQUALS(ft.getArgTypes()[1], b);
 238     TS_ASSERT_EQUALS(ft.getRangeType(), c);
 239
 240   }
 241
 242   void testMkFunctionTypeVectorOfArguments() {
 243     TypeNode a = d_nodeManager->mkSort();
 244     TypeNode b = d_nodeManager->mkSort();
 245     TypeNode c = d_nodeManager->mkSort();
 246
 247     std::vector<TypeNode> types;
 248     types.push_back(a);
 249     types.push_back(b);
 250     types.push_back(c);
 251
 252     TypeNode t = d_nodeManager->mkFunctionType(types);
 253     TypeNode t2 = d_nodeManager->mkFunctionType(types);
 254
 255     TS_ASSERT( !t.isBoolean() );
 256     TS_ASSERT( t.isFunction() );
 257     TS_ASSERT( !t.isNull() );
 258     TS_ASSERT( !t.isPredicate() );
 259     TS_ASSERT( !t.isSort() );
 260
 261     TS_ASSERT_EQUALS( t, t2 );
 262
 263     TypeNode ft = t;
 264     TS_ASSERT_EQUALS( ft, t );
 265     TS_ASSERT_EQUALS(ft.getArgTypes().size(), types.size()-1);
 266     TS_ASSERT_EQUALS(ft.getArgTypes()[0], a);
 267     TS_ASSERT_EQUALS(ft.getArgTypes()[1], b);
 268     TS_ASSERT_EQUALS(ft.getRangeType(), c);
 269   }
 270
 271   void testMkPredicateType() {
 272     TypeNode a = d_nodeManager->mkSort("a");
 273     TypeNode b = d_nodeManager->mkSort("b");
 274     TypeNode c = d_nodeManager->mkSort("c");
 275     TypeNode booleanType = d_nodeManager->booleanType();
 276
 277     std::vector<TypeNode> argTypes;
 278     argTypes.push_back(a);
 279     argTypes.push_back(b);
 280     argTypes.push_back(c);
 281
 282     TypeNode t = d_nodeManager->mkPredicateType(argTypes);
 283     TypeNode t2 = d_nodeManager->mkPredicateType(argTypes);
 284
 285     TS_ASSERT( !t.isBoolean() );
 286     TS_ASSERT( t.isFunction() );
 287     TS_ASSERT( !t.isNull() );
 288     TS_ASSERT( t.isPredicate() );
 289     TS_ASSERT( !t.isSort() );
 290
 291     TS_ASSERT_EQUALS( t, t2 );
 292
 293     TypeNode ft = t;
 294     TS_ASSERT_EQUALS( ft, t );
 295     TS_ASSERT_EQUALS(ft.getArgTypes().size(), argTypes.size());
 296     TS_ASSERT_EQUALS(ft.getArgTypes()[0], a);
 297     TS_ASSERT_EQUALS(ft.getArgTypes()[1], b);
 298     TS_ASSERT_EQUALS(ft.getArgTypes()[2], c);
 299     TS_ASSERT_EQUALS(ft.getRangeType(), booleanType);
 300
 301   }
 302
 303   /* This test is only valid if assertions are enabled. */
 304   void testMkNodeTooFew() {
 305 #ifdef CVC4_ASSERTIONS
 306     Node x = d_nodeManager->mkSkolem( "x", d_nodeManager->booleanType() );
 307     TS_ASSERT_THROWS( d_nodeManager->mkNode(AND, x), AssertionException );
 308 #endif
 309   }
 310
 311   /* This test is only valid if assertions are enabled. */
 312   void testMkNodeTooMany() {
 313 #ifdef CVC4_ASSERTIONS
 314     std::vector<Node> vars;
 315     const unsigned int max = metakind::getUpperBoundForKind(AND);
 316     TypeNode boolType = d_nodeManager->booleanType();
 317     Node skolem = d_nodeManager->mkSkolem("i", boolType);
 318     for( unsigned int i = 0; i <= max; ++i ) {
 319       vars.push_back( skolem );
 320     }
 321     TS_ASSERT_THROWS( d_nodeManager->mkNode(AND, vars), AssertionException );
 322 #endif
 323   }
 324
 325 };