test/unit/expr/node_black.h

   1 /*********************                                                        */
   2 /*! \file node_black.h
   3  ** \verbatim
   4  ** Original author: Morgan Deters
   5  ** Major contributors: Tim King
   6  ** Minor contributors (to current version): Christopher L. Conway, 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 Black box testing of CVC4::Node.
  13  **
  14  ** Black box testing of CVC4::Node.
  15  **/
  16
  17 #include <cxxtest/TestSuite.h>
  18
  19 //Used in some of the tests
  20 #include <vector>
  21 #include <sstream>
  22
  23 #include "expr/expr_manager.h"
  24 #include "expr/node_value.h"
  25 #include "expr/node_builder.h"
  26 #include "expr/node_manager.h"
  27 #include "expr/node.h"
  28 #include "smt/smt_options_handler.h"
  29
  30 using namespace CVC4;
  31 using namespace CVC4::kind;
  32 using namespace std;
  33
  34 class NodeBlack : public CxxTest::TestSuite {
  35 private:
  36
  37   Options opts;
  38   smt::SmtOptionsHandler* d_handler;
  39   NodeManager* d_nodeManager;
  40   NodeManagerScope* d_scope;
  41   TypeNode* d_booleanType;
  42   TypeNode* d_realType;
  43
  44 public:
  45
  46   void setUp() {
  47 #warning "TODO: Discuss the effects of this change with Clark."
  48     d_handler = new smt::SmtOptionsHandler(NULL);
  49
  50     char *argv[2];
  51     argv[0] = strdup("");
  52     argv[1] = strdup("--output-language=ast");
  53     opts.parseOptions(2, argv, d_handler);
  54     free(argv[0]);
  55     free(argv[1]);
  56
  57     d_nodeManager = new NodeManager(NULL, opts);
  58     d_scope = new NodeManagerScope(d_nodeManager);
  59     d_booleanType = new TypeNode(d_nodeManager->booleanType());
  60     d_realType = new TypeNode(d_nodeManager->realType());
  61   }
  62
  63   void tearDown() {
  64     delete d_booleanType;
  65     delete d_scope;
  66     delete d_nodeManager;
  67     delete d_handler;
  68   }
  69
  70   bool imp(bool a, bool b) const {
  71     return (!a) || (b);
  72   }
  73   bool iff(bool a, bool b) const {
  74     return (a && b) || ((!a)&&(!b));
  75   }
  76
  77   void testNull() {
  78     Node::null();
  79   }
  80
  81   void testIsNull() {
  82     /* bool isNull() const; */
  83
  84     Node a = Node::null();
  85     TS_ASSERT(a.isNull());
  86
  87     Node b = Node();
  88     TS_ASSERT(b.isNull());
  89
  90     Node c = b;
  91
  92     TS_ASSERT(c.isNull());
  93   }
  94
  95   void testCopyCtor() {
  96     Node e(Node::null());
  97   }
  98
  99   void testDestructor() {
 100     /* No access to internals ?
 101      * Makes sense to only test that this is crash free.
 102      */
 103
 104     Node *n = new Node();
 105     delete n;
 106
 107   }
 108
 109   /*tests:  bool operator==(const Node& e) const  */
 110   void testOperatorEquals() {
 111     Node a, b, c;
 112
 113     b = d_nodeManager->mkSkolem("b", *d_booleanType);
 114
 115     a = b;
 116     c = a;
 117
 118     Node d = d_nodeManager->mkSkolem("d", *d_booleanType);
 119
 120     TS_ASSERT(a==a);
 121     TS_ASSERT(a==b);
 122     TS_ASSERT(a==c);
 123
 124     TS_ASSERT(b==a);
 125     TS_ASSERT(b==b);
 126     TS_ASSERT(b==c);
 127
 128
 129
 130     TS_ASSERT(c==a);
 131     TS_ASSERT(c==b);
 132     TS_ASSERT(c==c);
 133
 134
 135     TS_ASSERT(d==d);
 136
 137     TS_ASSERT(!(d==a));
 138     TS_ASSERT(!(d==b));
 139     TS_ASSERT(!(d==c));
 140
 141     TS_ASSERT(!(a==d));
 142     TS_ASSERT(!(b==d));
 143     TS_ASSERT(!(c==d));
 144
 145   }
 146
 147   /* operator!= */
 148   void testOperatorNotEquals() {
 149
 150
 151     Node a, b, c;
 152
 153     b = d_nodeManager->mkSkolem("b", *d_booleanType);
 154
 155     a = b;
 156     c = a;
 157
 158     Node d = d_nodeManager->mkSkolem("d", *d_booleanType);
 159
 160     /*structed assuming operator == works */
 161     TS_ASSERT(iff(a!=a, !(a==a)));
 162     TS_ASSERT(iff(a!=b, !(a==b)));
 163     TS_ASSERT(iff(a!=c, !(a==c)));
 164
 165
 166     TS_ASSERT(iff(b!=a, !(b==a)));
 167     TS_ASSERT(iff(b!=b, !(b==b)));
 168     TS_ASSERT(iff(b!=c, !(b==c)));
 169
 170
 171     TS_ASSERT(iff(c!=a, !(c==a)));
 172     TS_ASSERT(iff(c!=b, !(c==b)));
 173     TS_ASSERT(iff(c!=c, !(c==c)));
 174
 175     TS_ASSERT(!(d!=d));
 176
 177     TS_ASSERT(d!=a);
 178     TS_ASSERT(d!=b);
 179     TS_ASSERT(d!=c);
 180
 181   }
 182
 183   void testOperatorSquare() {
 184     /*Node operator[](int i) const */
 185
 186 #ifdef CVC4_ASSERTIONS
 187     //Basic bounds check on a node w/out children
 188     TS_ASSERT_THROWS(Node::null()[-1], AssertionException);
 189     TS_ASSERT_THROWS(Node::null()[0], AssertionException);
 190 #endif /* CVC4_ASSERTIONS */
 191
 192     //Basic access check
 193     Node tb = d_nodeManager->mkConst(true);
 194     Node eb = d_nodeManager->mkConst(false);
 195     Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
 196     Node ite = cnd.iteNode(tb, eb);
 197
 198     TS_ASSERT(tb == cnd[0]);
 199     TS_ASSERT(eb == cnd[1]);
 200
 201     TS_ASSERT(cnd == ite[0]);
 202     TS_ASSERT(tb == ite[1]);
 203     TS_ASSERT(eb == ite[2]);
 204
 205 #ifdef CVC4_ASSERTIONS
 206     //Bounds check on a node with children
 207     TS_ASSERT_THROWS(ite == ite[-1], AssertionException);
 208     TS_ASSERT_THROWS(ite == ite[4], AssertionException);
 209 #endif /* CVC4_ASSERTIONS */
 210   }
 211
 212   /*tests:   Node& operator=(const Node&); */
 213   void testOperatorAssign() {
 214     Node a, b;
 215     Node c = d_nodeManager->mkNode(NOT, d_nodeManager->mkSkolem("c", *d_booleanType));
 216
 217     b = c;
 218     TS_ASSERT(b==c);
 219
 220
 221     a = b = c;
 222
 223     TS_ASSERT(a==b);
 224     TS_ASSERT(a==c);
 225   }
 226
 227   void testOperatorLessThan() {
 228     /* We don't have access to the ids so we can't test the implementation
 229      * in the black box tests. */
 230
 231     Node a = d_nodeManager->mkSkolem("a", d_nodeManager->booleanType());
 232     Node b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType());
 233
 234     TS_ASSERT(a<b || b<a);
 235     TS_ASSERT(!(a<b && b<a));
 236
 237     Node c = d_nodeManager->mkNode(AND, a, b);
 238     Node d = d_nodeManager->mkNode(AND, a, b);
 239
 240     TS_ASSERT(!(c<d));
 241     TS_ASSERT(!(d<c));
 242
 243     /* TODO:
 244      * Less than has the rather difficult to test property that subexpressions
 245      * are less than enclosing expressions.
 246      *
 247      * But what would be a convincing test of this property?
 248      */
 249
 250     // simple test of descending descendant property
 251     Node child = d_nodeManager->mkConst(true);
 252     Node parent = d_nodeManager->mkNode(NOT, child);
 253
 254     TS_ASSERT(child < parent);
 255
 256     // slightly less simple test of DD property
 257     std::vector<Node> chain;
 258     const int N = 500;
 259     Node curr = d_nodeManager->mkNode(OR, a, b);
 260     chain.push_back(curr);
 261     for(int i = 0; i < N; ++i) {
 262       curr = d_nodeManager->mkNode(AND, curr, curr);
 263       chain.push_back(curr);
 264     }
 265
 266     for(int i = 0; i < N; ++i) {
 267       for(int j = i + 1; j < N; ++j) {
 268         Node chain_i = chain[i];
 269         Node chain_j = chain[j];
 270         TS_ASSERT(chain_i < chain_j);
 271       }
 272     }
 273   }
 274
 275   void testEqNode() {
 276     /* Node eqNode(const Node& right) const; */
 277
 278     TypeNode t = d_nodeManager->mkSort();
 279     Node left = d_nodeManager->mkSkolem("left", t);
 280     Node right = d_nodeManager->mkSkolem("right", t);
 281     Node eq = left.eqNode(right);
 282
 283     TS_ASSERT(EQUAL == eq.getKind());
 284     TS_ASSERT(2 == eq.getNumChildren());
 285
 286     TS_ASSERT(eq[0] == left);
 287     TS_ASSERT(eq[1] == right);
 288   }
 289
 290   void testNotNode() {
 291     /* Node notNode() const; */
 292
 293     Node child = d_nodeManager->mkConst(true);
 294     Node parent = child.notNode();
 295
 296     TS_ASSERT(NOT == parent.getKind());
 297     TS_ASSERT(1   == parent.getNumChildren());
 298
 299     TS_ASSERT(parent[0] == child);
 300
 301   }
 302   void testAndNode() {
 303     /*Node andNode(const Node& right) const;*/
 304
 305     Node left = d_nodeManager->mkConst(true);
 306     Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkConst(false)));
 307     Node eq = left.andNode(right);
 308
 309
 310     TS_ASSERT(AND == eq.getKind());
 311     TS_ASSERT(2   == eq.getNumChildren());
 312
 313     TS_ASSERT(*(eq.begin()) == left);
 314     TS_ASSERT(*(++eq.begin()) == right);
 315
 316   }
 317
 318   void testOrNode() {
 319     /*Node orNode(const Node& right) const;*/
 320
 321     Node left = d_nodeManager->mkConst(true);
 322     Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkConst(false)));
 323     Node eq = left.orNode(right);
 324
 325
 326     TS_ASSERT(OR  == eq.getKind());
 327     TS_ASSERT(2   == eq.getNumChildren());
 328
 329     TS_ASSERT(*(eq.begin()) == left);
 330     TS_ASSERT(*(++eq.begin()) == right);
 331
 332   }
 333
 334   void testIteNode() {
 335     /*Node iteNode(const Node& thenpart, const Node& elsepart) const;*/
 336
 337     Node a = d_nodeManager->mkSkolem("a", *d_booleanType);
 338     Node b = d_nodeManager->mkSkolem("b", *d_booleanType);
 339
 340     Node cnd = d_nodeManager->mkNode(OR, a, b);
 341     Node thenBranch = d_nodeManager->mkConst(true);
 342     Node elseBranch = d_nodeManager->mkNode(NOT, d_nodeManager->mkConst(false));
 343     Node ite = cnd.iteNode(thenBranch, elseBranch);
 344
 345     TS_ASSERT(ITE == ite.getKind());
 346     TS_ASSERT(3 == ite.getNumChildren());
 347
 348     TS_ASSERT(*(ite.begin()) == cnd);
 349     TS_ASSERT(*(++ite.begin()) == thenBranch);
 350     TS_ASSERT(*(++(++ite.begin())) == elseBranch);
 351   }
 352
 353   void testIffNode() {
 354     /*  Node iffNode(const Node& right) const; */
 355
 356     Node left = d_nodeManager->mkConst(true);
 357     Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkConst(false)));
 358     Node eq = left.iffNode(right);
 359
 360
 361     TS_ASSERT(IFF == eq.getKind());
 362     TS_ASSERT(2   == eq.getNumChildren());
 363
 364     TS_ASSERT(*(eq.begin()) == left);
 365     TS_ASSERT(*(++eq.begin()) == right);
 366   }
 367
 368
 369   void testImpNode() {
 370     /* Node impNode(const Node& right) const; */
 371     Node left = d_nodeManager->mkConst(true);
 372     Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkConst(false)));
 373     Node eq = left.impNode(right);
 374
 375
 376     TS_ASSERT(IMPLIES == eq.getKind());
 377     TS_ASSERT(2 == eq.getNumChildren());
 378
 379     TS_ASSERT(*(eq.begin()) == left);
 380     TS_ASSERT(*(++eq.begin()) == right);
 381   }
 382
 383   void testXorNode() {
 384     /*Node xorNode(const Node& right) const;*/
 385     Node left = d_nodeManager->mkConst(true);
 386     Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkConst(false)));
 387     Node eq = left.xorNode(right);
 388
 389
 390     TS_ASSERT(XOR == eq.getKind());
 391     TS_ASSERT(2   == eq.getNumChildren());
 392
 393     TS_ASSERT(*(eq.begin()) == left);
 394     TS_ASSERT(*(++eq.begin()) == right);
 395   }
 396
 397   void testGetKind() {
 398     /*inline Kind getKind() const; */
 399
 400     Node a = d_nodeManager->mkSkolem("a", *d_booleanType);
 401     Node b = d_nodeManager->mkSkolem("b", *d_booleanType);
 402
 403     Node n = d_nodeManager->mkNode(NOT, a);
 404     TS_ASSERT(NOT == n.getKind());
 405
 406     n = d_nodeManager->mkNode(IFF, a, b);
 407     TS_ASSERT(IFF == n.getKind());
 408
 409     Node x = d_nodeManager->mkSkolem("x", *d_realType);
 410     Node y = d_nodeManager->mkSkolem("y", *d_realType);
 411
 412     n = d_nodeManager->mkNode(PLUS, x, y);
 413     TS_ASSERT(PLUS == n.getKind());
 414
 415     n = d_nodeManager->mkNode(UMINUS, x);
 416     TS_ASSERT(UMINUS == n.getKind());
 417   }
 418
 419   void testGetOperator() {
 420     TypeNode sort = d_nodeManager->mkSort("T");
 421     TypeNode booleanType = d_nodeManager->booleanType();
 422     TypeNode predType = d_nodeManager->mkFunctionType(sort, booleanType);
 423
 424     Node f = d_nodeManager->mkSkolem("f", predType);
 425     Node a = d_nodeManager->mkSkolem("a", sort);
 426     Node fa = d_nodeManager->mkNode(kind::APPLY_UF, f, a);
 427
 428     TS_ASSERT( fa.hasOperator() );
 429     TS_ASSERT( !f.hasOperator() );
 430     TS_ASSERT( !a.hasOperator() );
 431
 432     TS_ASSERT( fa.getNumChildren() == 1 );
 433     TS_ASSERT( f.getNumChildren() == 0 );
 434     TS_ASSERT( a.getNumChildren() == 0 );
 435
 436     TS_ASSERT( f == fa.getOperator() );
 437 #ifdef CVC4_ASSERTIONS
 438     TS_ASSERT_THROWS( f.getOperator(), IllegalArgumentException );
 439     TS_ASSERT_THROWS( a.getOperator(), IllegalArgumentException );
 440 #endif /* CVC4_ASSERTIONS */
 441   }
 442
 443   void testNaryExpForSize(Kind k, unsigned N) {
 444     NodeBuilder<> nbz(k);
 445     Node trueNode = d_nodeManager->mkConst(true);
 446     for(unsigned i = 0; i < N; ++i) {
 447       nbz << trueNode;
 448     }
 449     Node result = nbz;
 450     TS_ASSERT( N == result.getNumChildren() );
 451   }
 452
 453   void testNumChildren() {
 454     /*inline size_t getNumChildren() const;*/
 455
 456     Node trueNode = d_nodeManager->mkConst(true);
 457
 458     //test 0
 459     TS_ASSERT(0 == (Node::null()).getNumChildren());
 460
 461     //test 1
 462     TS_ASSERT(1 == trueNode.notNode().getNumChildren());
 463
 464     //test 2
 465     TS_ASSERT(2 == trueNode.andNode(trueNode).getNumChildren());
 466
 467     //Bigger tests
 468
 469     srand(0);
 470     int trials = 500;
 471     for(int i = 0; i < trials; ++i) {
 472       unsigned N = rand() % 1000 + 2;
 473       testNaryExpForSize(AND, N);
 474     }
 475
 476 #ifdef CVC4_ASSERTIONS
 477     TS_ASSERT_THROWS( testNaryExpForSize(AND, 0), AssertionException );
 478     TS_ASSERT_THROWS( testNaryExpForSize(AND, 1), AssertionException );
 479     TS_ASSERT_THROWS( testNaryExpForSize(NOT, 0), AssertionException );
 480     TS_ASSERT_THROWS( testNaryExpForSize(NOT, 2), AssertionException );
 481 #endif /* CVC4_ASSERTIONS */
 482   }
 483
 484   // test iterators
 485   void testIterator() {
 486     NodeBuilder<> b;
 487     Node x = d_nodeManager->mkSkolem("x", *d_booleanType);
 488     Node y = d_nodeManager->mkSkolem("y", *d_booleanType);
 489     Node z = d_nodeManager->mkSkolem("z", *d_booleanType);
 490     Node n = b << x << y << z << kind::AND;
 491
 492     { // iterator
 493       Node::iterator i = n.begin();
 494       TS_ASSERT(*i++ == x);
 495       TS_ASSERT(*i++ == y);
 496       TS_ASSERT(*i++ == z);
 497       TS_ASSERT(i == n.end());
 498     }
 499
 500     { // same for const iterator
 501       const Node& c = n;
 502       Node::const_iterator i = c.begin();
 503       TS_ASSERT(*i++ == x);
 504       TS_ASSERT(*i++ == y);
 505       TS_ASSERT(*i++ == z);
 506       TS_ASSERT(i == n.end());
 507     }
 508   }
 509
 510   // test the special "kinded-iterator"
 511   void testKindedIterator() {
 512     TypeNode integerType = d_nodeManager->integerType();
 513
 514     Node x = d_nodeManager->mkSkolem("x", integerType);
 515     Node y = d_nodeManager->mkSkolem("y", integerType);
 516     Node z = d_nodeManager->mkSkolem("z", integerType);
 517     Node plus_x_y_z = d_nodeManager->mkNode(kind::PLUS, x, y, z);
 518     Node x_minus_y = d_nodeManager->mkNode(kind::MINUS, x, y);
 519
 520     { // iterator
 521       Node::kinded_iterator i = plus_x_y_z.begin(PLUS);
 522       TS_ASSERT(*i++ == x);
 523       TS_ASSERT(*i++ == y);
 524       TS_ASSERT(*i++ == z);
 525       TS_ASSERT(i == plus_x_y_z.end(PLUS));
 526
 527       i = x.begin(PLUS);
 528       TS_ASSERT(*i++ == x);
 529       TS_ASSERT(i == x.end(PLUS));
 530     }
 531   }
 532
 533   void testToString() {
 534     TypeNode booleanType = d_nodeManager->booleanType();
 535
 536     Node w = d_nodeManager->mkSkolem("w", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
 537     Node x = d_nodeManager->mkSkolem("x", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
 538     Node y = d_nodeManager->mkSkolem("y", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
 539     Node z = d_nodeManager->mkSkolem("z", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
 540     Node m = NodeBuilder<>() << w << x << kind::OR;
 541     Node n = NodeBuilder<>() << m << y << z << kind::AND;
 542
 543     TS_ASSERT(n.toString() == "(AND (OR w x) y z)");
 544   }
 545
 546   void testToStream() {
 547     TypeNode booleanType = d_nodeManager->booleanType();
 548
 549     Node w = d_nodeManager->mkSkolem("w", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
 550     Node x = d_nodeManager->mkSkolem("x", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
 551     Node y = d_nodeManager->mkSkolem("y", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
 552     Node z = d_nodeManager->mkSkolem("z", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
 553     Node m = NodeBuilder<>() << x << y << kind::OR;
 554     Node n = NodeBuilder<>() << w << m << z << kind::AND;
 555     Node o = NodeBuilder<>() << n << n << kind::XOR;
 556
 557     stringstream sstr;
 558     sstr << Node::dag(false);
 559     n.toStream(sstr);
 560     TS_ASSERT(sstr.str() == "(AND w (OR x y) z)");
 561
 562     sstr.str(string());
 563     o.toStream(sstr, -1, false, 0);
 564     TS_ASSERT(sstr.str() == "(XOR (AND w (OR x y) z) (AND w (OR x y) z))");
 565
 566     sstr.str(string());
 567     sstr << n;
 568     TS_ASSERT(sstr.str() == "(AND w (OR x y) z)");
 569
 570     sstr.str(string());
 571     sstr << o;
 572     TS_ASSERT(sstr.str() == "(XOR (AND w (OR x y) z) (AND w (OR x y) z))");
 573
 574     sstr.str(string());
 575     sstr << Node::setdepth(0) << n;
 576     TS_ASSERT(sstr.str() == "(AND w (OR x y) z)");
 577
 578     sstr.str(string());
 579     sstr << Node::setdepth(0) << o;
 580     TS_ASSERT(sstr.str() == "(XOR (AND w (OR x y) z) (AND w (OR x y) z))");
 581
 582     sstr.str(string());
 583     sstr << Node::setdepth(1) << n;
 584     TS_ASSERT(sstr.str() == "(AND w (OR (...) (...)) z)");
 585
 586     sstr.str(string());
 587     sstr << Node::setdepth(1) << o;
 588     TS_ASSERT(sstr.str() == "(XOR (AND (...) (...) (...)) (AND (...) (...) (...)))");
 589
 590     sstr.str(string());
 591     sstr << Node::setdepth(2) << n;
 592     TS_ASSERT(sstr.str() == "(AND w (OR x y) z)");
 593
 594     sstr.str(string());
 595     sstr << Node::setdepth(2) << o;
 596     TS_ASSERT(sstr.str() == "(XOR (AND w (OR (...) (...)) z) (AND w (OR (...) (...)) z))");
 597
 598     sstr.str(string());
 599     sstr << Node::setdepth(3) << n;
 600     TS_ASSERT(sstr.str() == "(AND w (OR x y) z)");
 601
 602     sstr.str(string());
 603     sstr << Node::setdepth(3) << o;
 604     TS_ASSERT(sstr.str() == "(XOR (AND w (OR x y) z) (AND w (OR x y) z))");
 605   }
 606
 607   void testDagifier() {
 608     TypeNode intType = d_nodeManager->integerType();
 609     TypeNode fnType = d_nodeManager->mkFunctionType(intType, intType);
 610
 611     Node x = d_nodeManager->mkSkolem("x", intType, "", NodeManager::SKOLEM_EXACT_NAME);
 612     Node y = d_nodeManager->mkSkolem("y", intType, "", NodeManager::SKOLEM_EXACT_NAME);
 613     Node f = d_nodeManager->mkSkolem("f", fnType, "", NodeManager::SKOLEM_EXACT_NAME);
 614     Node g = d_nodeManager->mkSkolem("g", fnType, "", NodeManager::SKOLEM_EXACT_NAME);
 615     Node fx = d_nodeManager->mkNode(APPLY_UF, f, x);
 616     Node fy = d_nodeManager->mkNode(APPLY_UF, f, y);
 617     Node gx = d_nodeManager->mkNode(APPLY_UF, g, x);
 618     Node gy = d_nodeManager->mkNode(APPLY_UF, g, y);
 619     Node fgx = d_nodeManager->mkNode(APPLY_UF, f, gx);
 620     Node ffx = d_nodeManager->mkNode(APPLY_UF, f, fx);
 621     Node fffx = d_nodeManager->mkNode(APPLY_UF, f, ffx);
 622     Node fffx_eq_x = d_nodeManager->mkNode(EQUAL, fffx, x);
 623     Node fffx_eq_y = d_nodeManager->mkNode(EQUAL, fffx, y);
 624     Node fx_eq_gx = d_nodeManager->mkNode(EQUAL, fx, gx);
 625     Node x_eq_y = d_nodeManager->mkNode(EQUAL, x, y);
 626     Node fgx_eq_gy = d_nodeManager->mkNode(EQUAL, fgx, gy);
 627
 628     Node n = d_nodeManager->mkNode(OR, fffx_eq_x, fffx_eq_y, fx_eq_gx, x_eq_y, fgx_eq_gy);
 629
 630     stringstream sstr;
 631     sstr << Node::setdepth(-1) << Node::setlanguage(language::output::LANG_CVC4);
 632     sstr << Node::dag(false) << n; // never dagify
 633     TS_ASSERT(sstr.str() == "(f(f(f(x))) = x) OR (f(f(f(x))) = y) OR (f(x) = g(x)) OR (x = y) OR (f(g(x)) = g(y))");
 634
 635     sstr.str(string());
 636     sstr << Node::dag(true) << n; // always dagify
 637     TS_ASSERT(sstr.str() == "LET _let_0 = f(x), _let_1 = g(x), _let_2 = f(f(_let_0)) IN (_let_2 = x) OR (_let_2 = y) OR (_let_0 = _let_1) OR (x = y) OR (f(_let_1) = g(y))");
 638
 639     sstr.str(string());
 640     sstr << Node::dag(2) << n; // dagify subexprs occurring > 2 times
 641     TS_ASSERT(sstr.str() == "LET _let_0 = f(x) IN (f(f(_let_0)) = x) OR (f(f(_let_0)) = y) OR (_let_0 = g(x)) OR (x = y) OR (f(g(x)) = g(y))");
 642
 643     Warning() << Node::setdepth(-1) << Node::setlanguage(language::output::LANG_CVC4) << Node::dag(2) << n << std::endl;
 644     sstr.str(string());
 645     sstr << Node::dag(3) << n; // dagify subexprs occurring > 3 times
 646     TS_ASSERT(sstr.str() == "(f(f(f(x))) = x) OR (f(f(f(x))) = y) OR (f(x) = g(x)) OR (x = y) OR (f(g(x)) = g(y))");
 647     Warning() << Node::setdepth(-1) << Node::setlanguage(language::output::LANG_CVC4) << Node::dag(2) << n << std::endl;
 648   }
 649
 650 //  This Test is designed to fail in a way that will cause a segfault,
 651 //  so it is commented out.
 652 //  This is for demonstrating what a certain type of user error looks like.
 653 //   Node level0(){
 654 //     NodeBuilder<> nb(kind::AND);
 655 //     Node x = d_nodeManager->mkSkolem("x", *d_booleanType);
 656 //     nb << x;
 657 //     nb << x;
 658 //     return Node(nb.constructNode());
 659 //   }
 660
 661 //   TNode level1(){
 662 //     return level0();
 663 //   }
 664
 665 //   void testChaining() {
 666 //     Node res = level1();
 667
 668 //     TS_ASSERT(res.getKind() == kind::NULL_EXPR);
 669 //     TS_ASSERT(res != Node::null());
 670
 671 //     cerr << "I finished both tests now watch as I crash" << endl;
 672 //   }
 673 };