google test: expr: Migrate node_black. (#5764)

3 files changed, 786 insertions, 784 deletions

diff --git a/test/unit/expr/CMakeLists.txt b/test/unit/expr/CMakeLists.txt
index 440874166..aa7e06ef0 100644
--- a/test/unit/expr/CMakeLists.txt
+++ b/test/unit/expr/CMakeLists.txt
@@ -15,7 +15,7 @@ cvc4_add_unit_test_black(attribute_black expr)
 cvc4_add_unit_test_white(attribute_white expr)
 cvc4_add_unit_test_black(kind_black expr)
 cvc4_add_unit_test_black(kind_map_black expr)
-cvc4_add_cxx_unit_test_black(node_black expr)
+cvc4_add_unit_test_black(node_black expr)
 cvc4_add_unit_test_black(node_algorithm_black expr)
 cvc4_add_cxx_unit_test_black(node_builder_black expr)
 cvc4_add_cxx_unit_test_black(node_manager_black expr)
diff --git a/test/unit/expr/node_black.cpp b/test/unit/expr/node_black.cpp
new file mode 100644
index 000000000..d45cf603f
--- /dev/null
+++ b/test/unit/expr/node_black.cpp
@@ -0,0 +1,785 @@
+/*********************                                                        */
+/*! \file node_black.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Aina Niemetz, Morgan Deters, Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Black box testing of CVC4::Node.
+ **
+ ** Black box testing of CVC4::Node.
+ **/
+
+#include <algorithm>
+#include <sstream>
+#include <string>
+#include <vector>
+
+#include "api/cvc4cpp.h"
+#include "expr/dtype.h"
+#include "expr/expr_manager.h"
+#include "expr/node.h"
+#include "expr/node_builder.h"
+#include "expr/node_manager.h"
+#include "expr/node_value.h"
+#include "smt/smt_engine.h"
+#include "test_node.h"
+#include "test_utils.h"
+#include "theory/rewriter.h"
+
+namespace CVC4 {
+
+using namespace CVC4::kind;
+
+namespace test {
+
+namespace {
+/** Returns N skolem nodes from 'nodeManager' with the same `type`. */
+std::vector<Node> makeNSkolemNodes(NodeManager* nodeManager,
+                                   uint32_t n,
+                                   TypeNode type)
+{
+  std::vector<Node> skolems;
+  for (uint32_t i = 0; i < n; i++)
+  {
+    skolems.push_back(nodeManager->mkSkolem(
+        "skolem_", type, "Created by makeNSkolemNodes()"));
+  }
+  return skolems;
+}
+}  // namespace
+
+class TestNodeBlackNode : public TestNodeBlack
+{
+ protected:
+  void SetUp() override
+  {
+    TestNodeBlack::SetUp();
+    // setup an SMT engine so that options are in scope
+    Options opts;
+    char* argv[2];
+    argv[0] = strdup("");
+    argv[1] = strdup("--output-lang=ast");
+    Options::parseOptions(&opts, 2, argv);
+    free(argv[0]);
+    free(argv[1]);
+    d_smt.reset(new SmtEngine(d_nodeManager.get(), &opts));
+  }
+
+  std::unique_ptr<SmtEngine> d_smt;
+
+  bool imp(bool a, bool b) const { return (!a) || (b); }
+  bool iff(bool a, bool b) const { return (a && b) || ((!a) && (!b)); }
+
+  void testNaryExpForSize(Kind k, uint32_t n)
+  {
+    NodeBuilder<> nbz(k);
+    Node trueNode = d_nodeManager->mkConst(true);
+    for (uint32_t i = 0; i < n; ++i)
+    {
+      nbz << trueNode;
+    }
+    Node result = nbz;
+    ASSERT_EQ(n, result.getNumChildren());
+  }
+};
+
+TEST_F(TestNodeBlackNode, null) { Node::null(); }
+
+TEST_F(TestNodeBlackNode, is_null)
+{
+  Node a = Node::null();
+  ASSERT_TRUE(a.isNull());
+
+  Node b = Node();
+  ASSERT_TRUE(b.isNull());
+
+  Node c = b;
+  ASSERT_TRUE(c.isNull());
+}
+
+TEST_F(TestNodeBlackNode, copy_ctor) { Node e(Node::null()); }
+
+TEST_F(TestNodeBlackNode, dtor)
+{
+  /* No access to internals? Only test that this is crash free. */
+  Node* n;
+  ASSERT_NO_FATAL_FAILURE(n = new Node());
+  delete n;
+}
+
+/* operator== */
+TEST_F(TestNodeBlackNode, operator_equals)
+{
+  Node a, b, c;
+
+  b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType());
+
+  a = b;
+  c = a;
+
+  Node d = d_nodeManager->mkSkolem("d", d_nodeManager->booleanType());
+
+  ASSERT_TRUE(a == a);
+  ASSERT_TRUE(a == b);
+  ASSERT_TRUE(a == c);
+
+  ASSERT_TRUE(b == a);
+  ASSERT_TRUE(b == b);
+  ASSERT_TRUE(b == c);
+
+  ASSERT_TRUE(c == a);
+  ASSERT_TRUE(c == b);
+  ASSERT_TRUE(c == c);
+
+  ASSERT_TRUE(d == d);
+
+  ASSERT_FALSE(d == a);
+  ASSERT_FALSE(d == b);
+  ASSERT_FALSE(d == c);
+
+  ASSERT_FALSE(a == d);
+  ASSERT_FALSE(b == d);
+  ASSERT_FALSE(c == d);
+}
+
+/* operator!= */
+TEST_F(TestNodeBlackNode, operator_not_equals)
+{
+  Node a, b, c;
+
+  b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType());
+
+  a = b;
+  c = a;
+
+  Node d = d_nodeManager->mkSkolem("d", d_nodeManager->booleanType());
+
+  /*structed assuming operator == works */
+  ASSERT_TRUE(iff(a != a, !(a == a)));
+  ASSERT_TRUE(iff(a != b, !(a == b)));
+  ASSERT_TRUE(iff(a != c, !(a == c)));
+
+  ASSERT_TRUE(iff(b != a, !(b == a)));
+  ASSERT_TRUE(iff(b != b, !(b == b)));
+  ASSERT_TRUE(iff(b != c, !(b == c)));
+
+  ASSERT_TRUE(iff(c != a, !(c == a)));
+  ASSERT_TRUE(iff(c != b, !(c == b)));
+  ASSERT_TRUE(iff(c != c, !(c == c)));
+
+  ASSERT_TRUE(!(d != d));
+
+  ASSERT_TRUE(d != a);
+  ASSERT_TRUE(d != b);
+  ASSERT_TRUE(d != c);
+}
+
+/* operator[] */
+TEST_F(TestNodeBlackNode, operator_square)
+{
+#ifdef CVC4_ASSERTIONS
+  // Basic bounds check on a node w/out children
+  ASSERT_DEATH(Node::null()[-1], "i >= 0 && unsigned\\(i\\) < d_nchildren");
+  ASSERT_DEATH(Node::null()[0], "i >= 0 && unsigned\\(i\\) < d_nchildren");
+#endif
+
+  // Basic access check
+  Node tb = d_nodeManager->mkConst(true);
+  Node eb = d_nodeManager->mkConst(false);
+  Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
+  Node ite = cnd.iteNode(tb, eb);
+
+  ASSERT_EQ(tb, cnd[0]);
+  ASSERT_EQ(eb, cnd[1]);
+
+  ASSERT_EQ(cnd, ite[0]);
+  ASSERT_EQ(tb, ite[1]);
+  ASSERT_EQ(eb, ite[2]);
+
+#ifdef CVC4_ASSERTIONS
+  // Bounds check on a node with children
+  ASSERT_DEATH(ite == ite[-1], "i >= 0 && unsigned\\(i\\) < d_nchildren");
+  ASSERT_DEATH(ite == ite[4], "i >= 0 && unsigned\\(i\\) < d_nchildren");
+#endif
+}
+
+/* operator= */
+TEST_F(TestNodeBlackNode, operator_assign)
+{
+  Node a, b;
+  Node c = d_nodeManager->mkNode(
+      NOT, d_nodeManager->mkSkolem("c", d_nodeManager->booleanType()));
+
+  b = c;
+  ASSERT_EQ(b, c);
+
+  a = b = c;
+
+  ASSERT_EQ(a, b);
+  ASSERT_EQ(a, c);
+}
+
+/* operator< */
+TEST_F(TestNodeBlackNode, operator_less_than)
+{
+  // We don't have access to the ids so we can't test the implementation
+  // in the black box tests.
+
+  Node a = d_nodeManager->mkSkolem("a", d_nodeManager->booleanType());
+  Node b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType());
+
+  ASSERT_TRUE(a < b || b < a);
+  ASSERT_TRUE(!(a < b && b < a));
+
+  Node c = d_nodeManager->mkNode(AND, a, b);
+  Node d = d_nodeManager->mkNode(AND, a, b);
+
+  ASSERT_FALSE(c < d);
+  ASSERT_FALSE(d < c);
+
+  // simple test of descending descendant property
+  Node child = d_nodeManager->mkConst(true);
+  Node parent = d_nodeManager->mkNode(NOT, child);
+
+  ASSERT_TRUE(child < parent);
+
+  // slightly less simple test of DD property
+  std::vector<Node> chain;
+  const int N = 500;
+  Node curr = d_nodeManager->mkNode(OR, a, b);
+  chain.push_back(curr);
+  for (int i = 0; i < N; ++i)
+  {
+    curr = d_nodeManager->mkNode(AND, curr, curr);
+    chain.push_back(curr);
+  }
+
+  for (int i = 0; i < N; ++i)
+  {
+    for (int j = i + 1; j < N; ++j)
+    {
+      Node chain_i = chain[i];
+      Node chain_j = chain[j];
+      ASSERT_TRUE(chain_i < chain_j);
+    }
+  }
+}
+
+TEST_F(TestNodeBlackNode, eqNode)
+{
+  TypeNode t = d_nodeManager->mkSort();
+  Node left = d_nodeManager->mkSkolem("left", t);
+  Node right = d_nodeManager->mkSkolem("right", t);
+  Node eq = left.eqNode(right);
+
+  ASSERT_EQ(EQUAL, eq.getKind());
+  ASSERT_EQ(2, eq.getNumChildren());
+
+  ASSERT_EQ(eq[0], left);
+  ASSERT_EQ(eq[1], right);
+}
+
+TEST_F(TestNodeBlackNode, notNode)
+{
+  Node child = d_nodeManager->mkConst(true);
+  Node parent = child.notNode();
+
+  ASSERT_EQ(NOT, parent.getKind());
+  ASSERT_EQ(1, parent.getNumChildren());
+
+  ASSERT_EQ(parent[0], child);
+}
+
+TEST_F(TestNodeBlackNode, andNode)
+{
+  Node left = d_nodeManager->mkConst(true);
+  Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkConst(false)));
+  Node eq = left.andNode(right);
+
+  ASSERT_EQ(AND, eq.getKind());
+  ASSERT_EQ(2, eq.getNumChildren());
+
+  ASSERT_EQ(*(eq.begin()), left);
+  ASSERT_EQ(*(++eq.begin()), right);
+}
+
+TEST_F(TestNodeBlackNode, orNode)
+{
+  Node left = d_nodeManager->mkConst(true);
+  Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkConst(false)));
+  Node eq = left.orNode(right);
+
+  ASSERT_EQ(OR, eq.getKind());
+  ASSERT_EQ(2, eq.getNumChildren());
+
+  ASSERT_EQ(*(eq.begin()), left);
+  ASSERT_EQ(*(++eq.begin()), right);
+}
+
+TEST_F(TestNodeBlackNode, iteNode)
+{
+  Node a = d_nodeManager->mkSkolem("a", d_nodeManager->booleanType());
+  Node b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType());
+
+  Node cnd = d_nodeManager->mkNode(OR, a, b);
+  Node thenBranch = d_nodeManager->mkConst(true);
+  Node elseBranch = d_nodeManager->mkNode(NOT, d_nodeManager->mkConst(false));
+  Node ite = cnd.iteNode(thenBranch, elseBranch);
+
+  ASSERT_EQ(ITE, ite.getKind());
+  ASSERT_EQ(3, ite.getNumChildren());
+
+  ASSERT_EQ(*(ite.begin()), cnd);
+  ASSERT_EQ(*(++ite.begin()), thenBranch);
+  ASSERT_EQ(*(++(++ite.begin())), elseBranch);
+}
+
+TEST_F(TestNodeBlackNode, iffNode)
+{
+  Node left = d_nodeManager->mkConst(true);
+  Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkConst(false)));
+  Node eq = left.eqNode(right);
+
+  ASSERT_EQ(EQUAL, eq.getKind());
+  ASSERT_EQ(2, eq.getNumChildren());
+
+  ASSERT_EQ(*(eq.begin()), left);
+  ASSERT_EQ(*(++eq.begin()), right);
+}
+
+TEST_F(TestNodeBlackNode, impNode)
+{
+  Node left = d_nodeManager->mkConst(true);
+  Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkConst(false)));
+  Node eq = left.impNode(right);
+
+  ASSERT_EQ(IMPLIES, eq.getKind());
+  ASSERT_EQ(2, eq.getNumChildren());
+
+  ASSERT_EQ(*(eq.begin()), left);
+  ASSERT_EQ(*(++eq.begin()), right);
+}
+
+TEST_F(TestNodeBlackNode, xorNode)
+{
+  Node left = d_nodeManager->mkConst(true);
+  Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkConst(false)));
+  Node eq = left.xorNode(right);
+
+  ASSERT_EQ(XOR, eq.getKind());
+  ASSERT_EQ(2, eq.getNumChildren());
+
+  ASSERT_EQ(*(eq.begin()), left);
+  ASSERT_EQ(*(++eq.begin()), right);
+}
+
+TEST_F(TestNodeBlackNode, getKind)
+{
+  Node a = d_nodeManager->mkSkolem("a", d_nodeManager->booleanType());
+  Node b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType());
+
+  Node n = d_nodeManager->mkNode(NOT, a);
+  ASSERT_EQ(NOT, n.getKind());
+
+  n = d_nodeManager->mkNode(EQUAL, a, b);
+  ASSERT_EQ(EQUAL, n.getKind());
+
+  Node x = d_nodeManager->mkSkolem("x", d_nodeManager->realType());
+  Node y = d_nodeManager->mkSkolem("y", d_nodeManager->realType());
+
+  n = d_nodeManager->mkNode(PLUS, x, y);
+  ASSERT_EQ(PLUS, n.getKind());
+
+  n = d_nodeManager->mkNode(UMINUS, x);
+  ASSERT_EQ(UMINUS, n.getKind());
+}
+
+TEST_F(TestNodeBlackNode, getOperator)
+{
+  TypeNode sort = d_nodeManager->mkSort("T");
+  TypeNode booleanType = d_nodeManager->booleanType();
+  TypeNode predType = d_nodeManager->mkFunctionType(sort, booleanType);
+
+  Node f = d_nodeManager->mkSkolem("f", predType);
+  Node a = d_nodeManager->mkSkolem("a", sort);
+  Node fa = d_nodeManager->mkNode(kind::APPLY_UF, f, a);
+
+  ASSERT_TRUE(fa.hasOperator());
+  ASSERT_FALSE(f.hasOperator());
+  ASSERT_FALSE(a.hasOperator());
+
+  ASSERT_EQ(fa.getNumChildren(), 1);
+  ASSERT_EQ(f.getNumChildren(), 0);
+  ASSERT_EQ(a.getNumChildren(), 0);
+
+  ASSERT_EQ(f, fa.getOperator());
+#ifdef CVC4_ASSERTIONS
+  ASSERT_THROW(f.getOperator(), IllegalArgumentException);
+  ASSERT_THROW(a.getOperator(), IllegalArgumentException);
+#endif
+}
+
+TEST_F(TestNodeBlackNode, getNumChildren)
+{
+  Node trueNode = d_nodeManager->mkConst(true);
+
+  ASSERT_EQ(0, (Node::null()).getNumChildren());
+  ASSERT_EQ(1, trueNode.notNode().getNumChildren());
+  ASSERT_EQ(2, trueNode.andNode(trueNode).getNumChildren());
+
+  srand(0);
+  for (uint32_t i = 0; i < 500; ++i)
+  {
+    uint32_t n = rand() % 1000 + 2;
+    testNaryExpForSize(AND, n);
+  }
+
+#ifdef CVC4_ASSERTIONS
+  ASSERT_DEATH(testNaryExpForSize(AND, 0),
+               "getNumChildren\\(\\) >= "
+               "kind::metakind::getLowerBoundForKind\\(getKind\\(\\)\\)");
+  ASSERT_DEATH(testNaryExpForSize(AND, 1),
+               "getNumChildren\\(\\) >= "
+               "kind::metakind::getLowerBoundForKind\\(getKind\\(\\)\\)");
+  ASSERT_DEATH(testNaryExpForSize(NOT, 0),
+               "getNumChildren\\(\\) >= "
+               "kind::metakind::getLowerBoundForKind\\(getKind\\(\\)\\)");
+  ASSERT_DEATH(testNaryExpForSize(NOT, 2),
+               "getNumChildren\\(\\) <= "
+               "kind::metakind::getUpperBoundForKind\\(getKind\\(\\)\\)");
+#endif /* CVC4_ASSERTIONS */
+}
+
+TEST_F(TestNodeBlackNode, iterator)
+{
+  NodeBuilder<> b;
+  Node x = d_nodeManager->mkSkolem("x", d_nodeManager->booleanType());
+  Node y = d_nodeManager->mkSkolem("y", d_nodeManager->booleanType());
+  Node z = d_nodeManager->mkSkolem("z", d_nodeManager->booleanType());
+  Node n = b << x << y << z << kind::AND;
+
+  {  // iterator
+    Node::iterator i = n.begin();
+    ASSERT_EQ(*i++, x);
+    ASSERT_EQ(*i++, y);
+    ASSERT_EQ(*i++, z);
+    ASSERT_EQ(i, n.end());
+  }
+
+  {  // same for const iterator
+    const Node& c = n;
+    Node::const_iterator i = c.begin();
+    ASSERT_EQ(*i++, x);
+    ASSERT_EQ(*i++, y);
+    ASSERT_EQ(*i++, z);
+    ASSERT_EQ(i, n.end());
+  }
+}
+
+TEST_F(TestNodeBlackNode, kinded_iterator)
+{
+  TypeNode integerType = d_nodeManager->integerType();
+
+  Node x = d_nodeManager->mkSkolem("x", integerType);
+  Node y = d_nodeManager->mkSkolem("y", integerType);
+  Node z = d_nodeManager->mkSkolem("z", integerType);
+  Node plus_x_y_z = d_nodeManager->mkNode(kind::PLUS, x, y, z);
+  Node x_minus_y = d_nodeManager->mkNode(kind::MINUS, x, y);
+
+  {  // iterator
+    Node::kinded_iterator i = plus_x_y_z.begin(PLUS);
+    ASSERT_EQ(*i++, x);
+    ASSERT_EQ(*i++, y);
+    ASSERT_EQ(*i++, z);
+    ASSERT_TRUE(i == plus_x_y_z.end(PLUS));
+
+    i = x.begin(PLUS);
+    ASSERT_EQ(*i++, x);
+    ASSERT_TRUE(i == x.end(PLUS));
+  }
+}
+
+TEST_F(TestNodeBlackNode, toString)
+{
+  TypeNode booleanType = d_nodeManager->booleanType();
+
+  Node w = d_nodeManager->mkSkolem(
+      "w", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
+  Node x = d_nodeManager->mkSkolem(
+      "x", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
+  Node y = d_nodeManager->mkSkolem(
+      "y", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
+  Node z = d_nodeManager->mkSkolem(
+      "z", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
+  Node m = NodeBuilder<>() << w << x << kind::OR;
+  Node n = NodeBuilder<>() << m << y << z << kind::AND;
+
+  ASSERT_EQ(n.toString(), "(AND (OR w x) y z)");
+}
+
+TEST_F(TestNodeBlackNode, toStream)
+{
+  TypeNode booleanType = d_nodeManager->booleanType();
+
+  Node w = d_nodeManager->mkSkolem(
+      "w", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
+  Node x = d_nodeManager->mkSkolem(
+      "x", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
+  Node y = d_nodeManager->mkSkolem(
+      "y", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
+  Node z = d_nodeManager->mkSkolem(
+      "z", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
+  Node m = NodeBuilder<>() << x << y << kind::OR;
+  Node n = NodeBuilder<>() << w << m << z << kind::AND;
+  Node o = NodeBuilder<>() << n << n << kind::XOR;
+
+  std::stringstream sstr;
+  sstr << Node::dag(false);
+  n.toStream(sstr);
+  ASSERT_EQ(sstr.str(), "(AND w (OR x y) z)");
+
+  sstr.str(std::string());
+  o.toStream(sstr, -1, 0);
+  ASSERT_EQ(sstr.str(), "(XOR (AND w (OR x y) z) (AND w (OR x y) z))");
+
+  sstr.str(std::string());
+  sstr << n;
+  ASSERT_EQ(sstr.str(), "(AND w (OR x y) z)");
+
+  sstr.str(std::string());
+  sstr << o;
+  ASSERT_EQ(sstr.str(), "(XOR (AND w (OR x y) z) (AND w (OR x y) z))");
+
+  sstr.str(std::string());
+  sstr << Node::setdepth(0) << n;
+  ASSERT_EQ(sstr.str(), "(AND w (OR x y) z)");
+
+  sstr.str(std::string());
+  sstr << Node::setdepth(0) << o;
+  ASSERT_EQ(sstr.str(), "(XOR (AND w (OR x y) z) (AND w (OR x y) z))");
+
+  sstr.str(std::string());
+  sstr << Node::setdepth(1) << n;
+  ASSERT_EQ(sstr.str(), "(AND w (OR (...) (...)) z)");
+
+  sstr.str(std::string());
+  sstr << Node::setdepth(1) << o;
+  ASSERT_EQ(sstr.str(),
+            "(XOR (AND (...) (...) (...)) (AND (...) (...) (...)))");
+
+  sstr.str(std::string());
+  sstr << Node::setdepth(2) << n;
+  ASSERT_EQ(sstr.str(), "(AND w (OR x y) z)");
+
+  sstr.str(std::string());
+  sstr << Node::setdepth(2) << o;
+  ASSERT_EQ(sstr.str(),
+            "(XOR (AND w (OR (...) (...)) z) (AND w (OR (...) (...)) z))");
+
+  sstr.str(std::string());
+  sstr << Node::setdepth(3) << n;
+  ASSERT_EQ(sstr.str(), "(AND w (OR x y) z)");
+
+  sstr.str(std::string());
+  sstr << Node::setdepth(3) << o;
+  ASSERT_EQ(sstr.str(), "(XOR (AND w (OR x y) z) (AND w (OR x y) z))");
+}
+
+TEST_F(TestNodeBlackNode, dagifier)
+{
+  TypeNode intType = d_nodeManager->integerType();
+  TypeNode fnType = d_nodeManager->mkFunctionType(intType, intType);
+
+  Node x =
+      d_nodeManager->mkSkolem("x", intType, "", NodeManager::SKOLEM_EXACT_NAME);
+  Node y =
+      d_nodeManager->mkSkolem("y", intType, "", NodeManager::SKOLEM_EXACT_NAME);
+  Node f =
+      d_nodeManager->mkSkolem("f", fnType, "", NodeManager::SKOLEM_EXACT_NAME);
+  Node g =
+      d_nodeManager->mkSkolem("g", fnType, "", NodeManager::SKOLEM_EXACT_NAME);
+  Node fx = d_nodeManager->mkNode(APPLY_UF, f, x);
+  Node fy = d_nodeManager->mkNode(APPLY_UF, f, y);
+  Node gx = d_nodeManager->mkNode(APPLY_UF, g, x);
+  Node gy = d_nodeManager->mkNode(APPLY_UF, g, y);
+  Node fgx = d_nodeManager->mkNode(APPLY_UF, f, gx);
+  Node ffx = d_nodeManager->mkNode(APPLY_UF, f, fx);
+  Node fffx = d_nodeManager->mkNode(APPLY_UF, f, ffx);
+  Node fffx_eq_x = d_nodeManager->mkNode(EQUAL, fffx, x);
+  Node fffx_eq_y = d_nodeManager->mkNode(EQUAL, fffx, y);
+  Node fx_eq_gx = d_nodeManager->mkNode(EQUAL, fx, gx);
+  Node x_eq_y = d_nodeManager->mkNode(EQUAL, x, y);
+  Node fgx_eq_gy = d_nodeManager->mkNode(EQUAL, fgx, gy);
+
+  Node n = d_nodeManager->mkNode(
+      OR, fffx_eq_x, fffx_eq_y, fx_eq_gx, x_eq_y, fgx_eq_gy);
+
+  std::stringstream sstr;
+  sstr << Node::setdepth(-1) << Node::setlanguage(language::output::LANG_CVC4);
+  sstr << Node::dag(false) << n;  // never dagify
+  ASSERT_EQ(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))");
+}
+
+TEST_F(TestNodeBlackNode, for_each_over_nodes_as_node)
+{
+  const std::vector<Node> skolems =
+      makeNSkolemNodes(d_nodeManager.get(), 3, d_nodeManager->integerType());
+  Node add = d_nodeManager->mkNode(kind::PLUS, skolems);
+  std::vector<Node> children;
+  for (Node child : add)
+  {
+    children.push_back(child);
+  }
+  ASSERT_TRUE(children.size() == skolems.size()
+              && std::equal(children.begin(), children.end(), skolems.begin()));
+}
+
+TEST_F(TestNodeBlackNode, for_each_over_nodes_as_tnode)
+{
+  const std::vector<Node> skolems =
+      makeNSkolemNodes(d_nodeManager.get(), 3, d_nodeManager->integerType());
+  Node add = d_nodeManager->mkNode(kind::PLUS, skolems);
+  std::vector<TNode> children;
+  for (TNode child : add)
+  {
+    children.push_back(child);
+  }
+  ASSERT_TRUE(children.size() == skolems.size()
+              && std::equal(children.begin(), children.end(), skolems.begin()));
+}
+
+TEST_F(TestNodeBlackNode, for_each_over_tnodes_as_node)
+{
+  const std::vector<Node> skolems =
+      makeNSkolemNodes(d_nodeManager.get(), 3, d_nodeManager->integerType());
+  Node add_node = d_nodeManager->mkNode(kind::PLUS, skolems);
+  TNode add_tnode = add_node;
+  std::vector<Node> children;
+  for (Node child : add_tnode)
+  {
+    children.push_back(child);
+  }
+  ASSERT_TRUE(children.size() == skolems.size()
+              && std::equal(children.begin(), children.end(), skolems.begin()));
+}
+
+TEST_F(TestNodeBlackNode, for_each_over_tnodes_as_tnode)
+{
+  const std::vector<Node> skolems =
+      makeNSkolemNodes(d_nodeManager.get(), 3, d_nodeManager->integerType());
+  Node add_node = d_nodeManager->mkNode(kind::PLUS, skolems);
+  TNode add_tnode = add_node;
+  std::vector<TNode> children;
+  for (TNode child : add_tnode)
+  {
+    children.push_back(child);
+  }
+  ASSERT_TRUE(children.size() == skolems.size()
+              && std::equal(children.begin(), children.end(), skolems.begin()));
+}
+
+TEST_F(TestNodeBlackNode, isConst)
+{
+  // more complicated "constants" exist in datatypes and arrays theories
+  DType list("list");
+  std::shared_ptr<DTypeConstructor> consC =
+      std::make_shared<DTypeConstructor>("cons");
+  consC->addArg("car", d_nodeManager->integerType());
+  consC->addArgSelf("cdr");
+  list.addConstructor(consC);
+  list.addConstructor(std::make_shared<DTypeConstructor>("nil"));
+  TypeNode listType = d_nodeManager->mkDatatypeType(list);
+  const std::vector<std::shared_ptr<DTypeConstructor> >& lcons =
+      listType.getDType().getConstructors();
+  Node cons = lcons[0]->getConstructor();
+  Node nil = lcons[1]->getConstructor();
+  Node x = d_nodeManager->mkSkolem("x", d_nodeManager->integerType());
+  Node cons_x_nil =
+      d_nodeManager->mkNode(APPLY_CONSTRUCTOR,
+                            cons,
+                            x,
+                            d_nodeManager->mkNode(APPLY_CONSTRUCTOR, nil));
+  Node cons_1_nil =
+      d_nodeManager->mkNode(APPLY_CONSTRUCTOR,
+                            cons,
+                            d_nodeManager->mkConst(Rational(1)),
+                            d_nodeManager->mkNode(APPLY_CONSTRUCTOR, nil));
+  Node cons_1_cons_2_nil = d_nodeManager->mkNode(
+      APPLY_CONSTRUCTOR,
+      cons,
+      d_nodeManager->mkConst(Rational(1)),
+      d_nodeManager->mkNode(APPLY_CONSTRUCTOR,
+                            cons,
+                            d_nodeManager->mkConst(Rational(2)),
+                            d_nodeManager->mkNode(APPLY_CONSTRUCTOR, nil)));
+  ASSERT_TRUE(d_nodeManager->mkNode(APPLY_CONSTRUCTOR, nil).isConst());
+  ASSERT_FALSE(cons_x_nil.isConst());
+  ASSERT_TRUE(cons_1_nil.isConst());
+  ASSERT_TRUE(cons_1_cons_2_nil.isConst());
+
+  TypeNode arrType = d_nodeManager->mkArrayType(d_nodeManager->integerType(),
+                                                d_nodeManager->integerType());
+  Node zero = d_nodeManager->mkConst(Rational(0));
+  Node one = d_nodeManager->mkConst(Rational(1));
+  Node storeAll = d_nodeManager->mkConst(ArrayStoreAll(arrType, zero));
+  ASSERT_TRUE(storeAll.isConst());
+
+  Node arr = d_nodeManager->mkNode(STORE, storeAll, zero, zero);
+  ASSERT_FALSE(arr.isConst());
+  arr = d_nodeManager->mkNode(STORE, storeAll, zero, one);
+  ASSERT_TRUE(arr.isConst());
+  Node arr2 = d_nodeManager->mkNode(STORE, arr, one, zero);
+  ASSERT_FALSE(arr2.isConst());
+  arr2 = d_nodeManager->mkNode(STORE, arr, zero, one);
+  ASSERT_FALSE(arr2.isConst());
+
+  arrType = d_nodeManager->mkArrayType(d_nodeManager->mkBitVectorType(1),
+                                       d_nodeManager->mkBitVectorType(1));
+  zero = d_nodeManager->mkConst(BitVector(1, unsigned(0)));
+  one = d_nodeManager->mkConst(BitVector(1, unsigned(1)));
+  storeAll = d_nodeManager->mkConst(ArrayStoreAll(arrType, zero));
+  ASSERT_TRUE(storeAll.isConst());
+
+  arr = d_nodeManager->mkNode(STORE, storeAll, zero, zero);
+  ASSERT_FALSE(arr.isConst());
+  arr = d_nodeManager->mkNode(STORE, storeAll, zero, one);
+  ASSERT_TRUE(arr.isConst());
+  arr2 = d_nodeManager->mkNode(STORE, arr, one, zero);
+  ASSERT_FALSE(arr2.isConst());
+  arr2 = d_nodeManager->mkNode(STORE, arr, one, one);
+  ASSERT_FALSE(arr2.isConst());
+  arr2 = d_nodeManager->mkNode(STORE, arr, zero, one);
+  ASSERT_FALSE(arr2.isConst());
+}
+
+namespace {
+Node level0(NodeManager* nm)
+{
+  NodeBuilder<> nb(kind::AND);
+  Node x = nm->mkSkolem("x", nm->booleanType());
+  nb << x;
+  nb << x;
+  return Node(nb.constructNode());
+}
+TNode level1(NodeManager* nm) { return level0(nm); }
+}  // namespace
+
+/**
+ * This is for demonstrating what a certain type of user error looks like.
+ */
+TEST_F(TestNodeBlackNode, node_tnode_usage)
+{
+  Node n;
+  ASSERT_NO_FATAL_FAILURE(n = level0(d_nodeManager.get()));
+  ASSERT_DEATH(n = level1(d_nodeManager.get()), "d_nv->d_rc > 0");
+}
+
+}  // namespace test
+}  // namespace CVC4
diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h
deleted file mode 100644
index 4e4a39654..000000000
--- a/test/unit/expr/node_black.h
+++ /dev/null
@@ -1,783 +0,0 @@
-/*********************                                                        */
-/*! \file node_black.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Tim King, Morgan Deters, Andrew Reynolds
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Black box testing of CVC4::Node.
- **
- ** Black box testing of CVC4::Node.
- **/
-
-#include <cxxtest/TestSuite.h>
-
-// Used in some of the tests
-#include <algorithm>
-#include <sstream>
-#include <string>
-#include <vector>
-
-#include "api/cvc4cpp.h"
-#include "expr/dtype.h"
-#include "expr/expr_manager.h"
-#include "expr/node.h"
-#include "expr/node_builder.h"
-#include "expr/node_manager.h"
-#include "expr/node_value.h"
-#include "smt/smt_engine.h"
-#include "test_utils.h"
-#include "theory/rewriter.h"
-
-using namespace CVC4;
-using namespace CVC4::kind;
-using namespace std;
-
-namespace {
-
-// Returns N skolem nodes from 'nodeManager' with the same `type`.
-std::vector<Node> makeNSkolemNodes(NodeManager* nodeManager, int N,
-                                   TypeNode type) {
-  std::vector<Node> skolems;
-  for (int i = 0; i < N; i++) {
-    skolems.push_back(nodeManager->mkSkolem(/*prefix=*/"skolem_", type,
-                                            "Created by makeNSkolemNodes()"));
-  }
-  return skolems;
-}
-
-}  // namespace
-
-class NodeBlack : public CxxTest::TestSuite {
- private:
-  NodeManager* d_nodeManager;
-  api::Solver* d_slv;
- public:
-  void setUp() override
-  {
-    // setup a SMT engine so that options are in scope
-    Options opts;
-    char* argv[2];
-    argv[0] = strdup("");
-    argv[1] = strdup("--output-lang=ast");
-    Options::parseOptions(&opts, 2, argv);
-    free(argv[0]);
-    free(argv[1]);
-
-    d_slv = new api::Solver(&opts);
-    d_nodeManager = d_slv->getSmtEngine()->getNodeManager();
-  }
-
-  void tearDown() override { 
-    delete d_slv;
-  }
-
-  bool imp(bool a, bool b) const { return (!a) || (b); }
-  bool iff(bool a, bool b) const { return (a && b) || ((!a) && (!b)); }
-
-  void testNull() { Node::null(); }
-
-  void testIsNull() {
-    /* bool isNull() const; */
-
-    Node a = Node::null();
-    TS_ASSERT(a.isNull());
-
-    Node b = Node();
-    TS_ASSERT(b.isNull());
-
-    Node c = b;
-
-    TS_ASSERT(c.isNull());
-  }
-
-  void testCopyCtor() { Node e(Node::null()); }
-
-  void testDestructor() {
-    /* No access to internals ?
-     * Makes sense to only test that this is crash free.
-     */
-
-    Node* n = new Node();
-    delete n;
-  }
-
-  /*tests:  bool operator==(const Node& e) const  */
-  void testOperatorEquals() {
-    Node a, b, c;
-
-    b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType());
-
-    a = b;
-    c = a;
-
-    Node d = d_nodeManager->mkSkolem("d", d_nodeManager->booleanType());
-
-    TS_ASSERT(a == a);
-    TS_ASSERT(a == b);
-    TS_ASSERT(a == c);
-
-    TS_ASSERT(b == a);
-    TS_ASSERT(b == b);
-    TS_ASSERT(b == c);
-
-    TS_ASSERT(c == a);
-    TS_ASSERT(c == b);
-    TS_ASSERT(c == c);
-
-    TS_ASSERT(d == d);
-
-    TS_ASSERT(!(d == a));
-    TS_ASSERT(!(d == b));
-    TS_ASSERT(!(d == c));
-
-    TS_ASSERT(!(a == d));
-    TS_ASSERT(!(b == d));
-    TS_ASSERT(!(c == d));
-  }
-
-  /* operator!= */
-  void testOperatorNotEquals() {
-    Node a, b, c;
-
-    b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType());
-
-    a = b;
-    c = a;
-
-    Node d = d_nodeManager->mkSkolem("d", d_nodeManager->booleanType());
-
-    /*structed assuming operator == works */
-    TS_ASSERT(iff(a != a, !(a == a)));
-    TS_ASSERT(iff(a != b, !(a == b)));
-    TS_ASSERT(iff(a != c, !(a == c)));
-
-    TS_ASSERT(iff(b != a, !(b == a)));
-    TS_ASSERT(iff(b != b, !(b == b)));
-    TS_ASSERT(iff(b != c, !(b == c)));
-
-    TS_ASSERT(iff(c != a, !(c == a)));
-    TS_ASSERT(iff(c != b, !(c == b)));
-    TS_ASSERT(iff(c != c, !(c == c)));
-
-    TS_ASSERT(!(d != d));
-
-    TS_ASSERT(d != a);
-    TS_ASSERT(d != b);
-    TS_ASSERT(d != c);
-  }
-
-  void testOperatorSquare() {
-    /*Node operator[](int i) const */
-
-#ifdef CVC4_ASSERTIONS
-    // Basic bounds check on a node w/out children
-    TS_UTILS_EXPECT_ABORT(Node::null()[-1]);
-    TS_UTILS_EXPECT_ABORT(Node::null()[0]);
-#endif /* CVC4_ASSERTIONS */
-
-    // Basic access check
-    Node tb = d_nodeManager->mkConst(true);
-    Node eb = d_nodeManager->mkConst(false);
-    Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
-    Node ite = cnd.iteNode(tb, eb);
-
-    TS_ASSERT(tb == cnd[0]);
-    TS_ASSERT(eb == cnd[1]);
-
-    TS_ASSERT(cnd == ite[0]);
-    TS_ASSERT(tb == ite[1]);
-    TS_ASSERT(eb == ite[2]);
-
-#ifdef CVC4_ASSERTIONS
-    // Bounds check on a node with children
-    TS_UTILS_EXPECT_ABORT(ite == ite[-1]);
-    TS_UTILS_EXPECT_ABORT(ite == ite[4]);
-#endif /* CVC4_ASSERTIONS */
-  }
-
-  /*tests:   Node& operator=(const Node&); */
-  void testOperatorAssign() {
-    Node a, b;
-    Node c = d_nodeManager->mkNode(
-        NOT, d_nodeManager->mkSkolem("c", d_nodeManager->booleanType()));
-
-    b = c;
-    TS_ASSERT(b == c);
-
-    a = b = c;
-
-    TS_ASSERT(a == b);
-    TS_ASSERT(a == c);
-  }
-
-  void testOperatorLessThan() {
-    /* We don't have access to the ids so we can't test the implementation
-     * in the black box tests. */
-
-    Node a = d_nodeManager->mkSkolem("a", d_nodeManager->booleanType());
-    Node b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType());
-
-    TS_ASSERT(a < b || b < a);
-    TS_ASSERT(!(a < b && b < a));
-
-    Node c = d_nodeManager->mkNode(AND, a, b);
-    Node d = d_nodeManager->mkNode(AND, a, b);
-
-    TS_ASSERT(!(c < d));
-    TS_ASSERT(!(d < c));
-
-    /* TODO:
-     * Less than has the rather difficult to test property that subexpressions
-     * are less than enclosing expressions.
-     *
-     * But what would be a convincing test of this property?
-     */
-
-    // simple test of descending descendant property
-    Node child = d_nodeManager->mkConst(true);
-    Node parent = d_nodeManager->mkNode(NOT, child);
-
-    TS_ASSERT(child < parent);
-
-    // slightly less simple test of DD property
-    std::vector<Node> chain;
-    const int N = 500;
-    Node curr = d_nodeManager->mkNode(OR, a, b);
-    chain.push_back(curr);
-    for (int i = 0; i < N; ++i) {
-      curr = d_nodeManager->mkNode(AND, curr, curr);
-      chain.push_back(curr);
-    }
-
-    for (int i = 0; i < N; ++i) {
-      for (int j = i + 1; j < N; ++j) {
-        Node chain_i = chain[i];
-        Node chain_j = chain[j];
-        TS_ASSERT(chain_i < chain_j);
-      }
-    }
-  }
-
-  void testEqNode() {
-    /* Node eqNode(const Node& right) const; */
-
-    TypeNode t = d_nodeManager->mkSort();
-    Node left = d_nodeManager->mkSkolem("left", t);
-    Node right = d_nodeManager->mkSkolem("right", t);
-    Node eq = left.eqNode(right);
-
-    TS_ASSERT(EQUAL == eq.getKind());
-    TS_ASSERT(2 == eq.getNumChildren());
-
-    TS_ASSERT(eq[0] == left);
-    TS_ASSERT(eq[1] == right);
-  }
-
-  void testNotNode() {
-    /* Node notNode() const; */
-
-    Node child = d_nodeManager->mkConst(true);
-    Node parent = child.notNode();
-
-    TS_ASSERT(NOT == parent.getKind());
-    TS_ASSERT(1 == parent.getNumChildren());
-
-    TS_ASSERT(parent[0] == child);
-  }
-  void testAndNode() {
-    /*Node andNode(const Node& right) const;*/
-
-    Node left = d_nodeManager->mkConst(true);
-    Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkConst(false)));
-    Node eq = left.andNode(right);
-
-    TS_ASSERT(AND == eq.getKind());
-    TS_ASSERT(2 == eq.getNumChildren());
-
-    TS_ASSERT(*(eq.begin()) == left);
-    TS_ASSERT(*(++eq.begin()) == right);
-  }
-
-  void testOrNode() {
-    /*Node orNode(const Node& right) const;*/
-
-    Node left = d_nodeManager->mkConst(true);
-    Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkConst(false)));
-    Node eq = left.orNode(right);
-
-    TS_ASSERT(OR == eq.getKind());
-    TS_ASSERT(2 == eq.getNumChildren());
-
-    TS_ASSERT(*(eq.begin()) == left);
-    TS_ASSERT(*(++eq.begin()) == right);
-  }
-
-  void testIteNode() {
-    /*Node iteNode(const Node& thenpart, const Node& elsepart) const;*/
-
-    Node a = d_nodeManager->mkSkolem("a", d_nodeManager->booleanType());
-    Node b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType());
-
-    Node cnd = d_nodeManager->mkNode(OR, a, b);
-    Node thenBranch = d_nodeManager->mkConst(true);
-    Node elseBranch = d_nodeManager->mkNode(NOT, d_nodeManager->mkConst(false));
-    Node ite = cnd.iteNode(thenBranch, elseBranch);
-
-    TS_ASSERT(ITE == ite.getKind());
-    TS_ASSERT(3 == ite.getNumChildren());
-
-    TS_ASSERT(*(ite.begin()) == cnd);
-    TS_ASSERT(*(++ite.begin()) == thenBranch);
-    TS_ASSERT(*(++(++ite.begin())) == elseBranch);
-  }
-
-  void testIffNode() {
-    /*  Node eqNode(const Node& right) const; */
-
-    Node left = d_nodeManager->mkConst(true);
-    Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkConst(false)));
-    Node eq = left.eqNode(right);
-
-    TS_ASSERT(EQUAL == eq.getKind());
-    TS_ASSERT(2 == eq.getNumChildren());
-
-    TS_ASSERT(*(eq.begin()) == left);
-    TS_ASSERT(*(++eq.begin()) == right);
-  }
-
-  void testImpNode() {
-    /* Node impNode(const Node& right) const; */
-    Node left = d_nodeManager->mkConst(true);
-    Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkConst(false)));
-    Node eq = left.impNode(right);
-
-    TS_ASSERT(IMPLIES == eq.getKind());
-    TS_ASSERT(2 == eq.getNumChildren());
-
-    TS_ASSERT(*(eq.begin()) == left);
-    TS_ASSERT(*(++eq.begin()) == right);
-  }
-
-  void testXorNode() {
-    /*Node xorNode(const Node& right) const;*/
-    Node left = d_nodeManager->mkConst(true);
-    Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkConst(false)));
-    Node eq = left.xorNode(right);
-
-    TS_ASSERT(XOR == eq.getKind());
-    TS_ASSERT(2 == eq.getNumChildren());
-
-    TS_ASSERT(*(eq.begin()) == left);
-    TS_ASSERT(*(++eq.begin()) == right);
-  }
-
-  void testGetKind() {
-    /*inline Kind getKind() const; */
-
-    Node a = d_nodeManager->mkSkolem("a", d_nodeManager->booleanType());
-    Node b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType());
-
-    Node n = d_nodeManager->mkNode(NOT, a);
-    TS_ASSERT(NOT == n.getKind());
-
-    n = d_nodeManager->mkNode(EQUAL, a, b);
-    TS_ASSERT(EQUAL == n.getKind());
-
-    Node x = d_nodeManager->mkSkolem("x", d_nodeManager->realType());
-    Node y = d_nodeManager->mkSkolem("y", d_nodeManager->realType());
-
-    n = d_nodeManager->mkNode(PLUS, x, y);
-    TS_ASSERT(PLUS == n.getKind());
-
-    n = d_nodeManager->mkNode(UMINUS, x);
-    TS_ASSERT(UMINUS == n.getKind());
-  }
-
-  void testGetOperator() {
-    TypeNode sort = d_nodeManager->mkSort("T");
-    TypeNode booleanType = d_nodeManager->booleanType();
-    TypeNode predType = d_nodeManager->mkFunctionType(sort, booleanType);
-
-    Node f = d_nodeManager->mkSkolem("f", predType);
-    Node a = d_nodeManager->mkSkolem("a", sort);
-    Node fa = d_nodeManager->mkNode(kind::APPLY_UF, f, a);
-
-    TS_ASSERT(fa.hasOperator());
-    TS_ASSERT(!f.hasOperator());
-    TS_ASSERT(!a.hasOperator());
-
-    TS_ASSERT(fa.getNumChildren() == 1);
-    TS_ASSERT(f.getNumChildren() == 0);
-    TS_ASSERT(a.getNumChildren() == 0);
-
-    TS_ASSERT(f == fa.getOperator());
-#ifdef CVC4_ASSERTIONS
-    TS_ASSERT_THROWS(f.getOperator(), IllegalArgumentException&);
-    TS_ASSERT_THROWS(a.getOperator(), IllegalArgumentException&);
-#endif /* CVC4_ASSERTIONS */
-  }
-
-  void testNaryExpForSize(Kind k, unsigned N) {
-    NodeBuilder<> nbz(k);
-    Node trueNode = d_nodeManager->mkConst(true);
-    for (unsigned i = 0; i < N; ++i) {
-      nbz << trueNode;
-    }
-    Node result = nbz;
-    TS_ASSERT(N == result.getNumChildren());
-  }
-
-  void testNumChildren() {
-    /*inline size_t getNumChildren() const;*/
-
-    Node trueNode = d_nodeManager->mkConst(true);
-
-    // test 0
-    TS_ASSERT(0 == (Node::null()).getNumChildren());
-
-    // test 1
-    TS_ASSERT(1 == trueNode.notNode().getNumChildren());
-
-    // test 2
-    TS_ASSERT(2 == trueNode.andNode(trueNode).getNumChildren());
-
-    // Bigger tests
-
-    srand(0);
-    int trials = 500;
-    for (int i = 0; i < trials; ++i) {
-      unsigned N = rand() % 1000 + 2;
-      testNaryExpForSize(AND, N);
-    }
-
-#ifdef CVC4_ASSERTIONS
-    TS_UTILS_EXPECT_ABORT(testNaryExpForSize(AND, 0));
-    TS_UTILS_EXPECT_ABORT(testNaryExpForSize(AND, 1));
-    TS_UTILS_EXPECT_ABORT(testNaryExpForSize(NOT, 0));
-    TS_UTILS_EXPECT_ABORT(testNaryExpForSize(NOT, 2));
-#endif /* CVC4_ASSERTIONS */
-  }
-
-  // test iterators
-  void testIterator() {
-    NodeBuilder<> b;
-    Node x = d_nodeManager->mkSkolem("x", d_nodeManager->booleanType());
-    Node y = d_nodeManager->mkSkolem("y", d_nodeManager->booleanType());
-    Node z = d_nodeManager->mkSkolem("z", d_nodeManager->booleanType());
-    Node n = b << x << y << z << kind::AND;
-
-    {  // iterator
-      Node::iterator i = n.begin();
-      TS_ASSERT(*i++ == x);
-      TS_ASSERT(*i++ == y);
-      TS_ASSERT(*i++ == z);
-      TS_ASSERT(i == n.end());
-    }
-
-    {  // same for const iterator
-      const Node& c = n;
-      Node::const_iterator i = c.begin();
-      TS_ASSERT(*i++ == x);
-      TS_ASSERT(*i++ == y);
-      TS_ASSERT(*i++ == z);
-      TS_ASSERT(i == n.end());
-    }
-  }
-
-  // test the special "kinded-iterator"
-  void testKindedIterator() {
-    TypeNode integerType = d_nodeManager->integerType();
-
-    Node x = d_nodeManager->mkSkolem("x", integerType);
-    Node y = d_nodeManager->mkSkolem("y", integerType);
-    Node z = d_nodeManager->mkSkolem("z", integerType);
-    Node plus_x_y_z = d_nodeManager->mkNode(kind::PLUS, x, y, z);
-    Node x_minus_y = d_nodeManager->mkNode(kind::MINUS, x, y);
-
-    {  // iterator
-      Node::kinded_iterator i = plus_x_y_z.begin(PLUS);
-      TS_ASSERT(*i++ == x);
-      TS_ASSERT(*i++ == y);
-      TS_ASSERT(*i++ == z);
-      TS_ASSERT(i == plus_x_y_z.end(PLUS));
-
-      i = x.begin(PLUS);
-      TS_ASSERT(*i++ == x);
-      TS_ASSERT(i == x.end(PLUS));
-    }
-  }
-
-  void testToString() {
-    TypeNode booleanType = d_nodeManager->booleanType();
-
-    Node w = d_nodeManager->mkSkolem("w", booleanType, "",
-                                     NodeManager::SKOLEM_EXACT_NAME);
-    Node x = d_nodeManager->mkSkolem("x", booleanType, "",
-                                     NodeManager::SKOLEM_EXACT_NAME);
-    Node y = d_nodeManager->mkSkolem("y", booleanType, "",
-                                     NodeManager::SKOLEM_EXACT_NAME);
-    Node z = d_nodeManager->mkSkolem("z", booleanType, "",
-                                     NodeManager::SKOLEM_EXACT_NAME);
-    Node m = NodeBuilder<>() << w << x << kind::OR;
-    Node n = NodeBuilder<>() << m << y << z << kind::AND;
-
-    TS_ASSERT(n.toString() == "(AND (OR w x) y z)");
-  }
-
-  void testToStream() {
-    TypeNode booleanType = d_nodeManager->booleanType();
-
-    Node w = d_nodeManager->mkSkolem("w", booleanType, "",
-                                     NodeManager::SKOLEM_EXACT_NAME);
-    Node x = d_nodeManager->mkSkolem("x", booleanType, "",
-                                     NodeManager::SKOLEM_EXACT_NAME);
-    Node y = d_nodeManager->mkSkolem("y", booleanType, "",
-                                     NodeManager::SKOLEM_EXACT_NAME);
-    Node z = d_nodeManager->mkSkolem("z", booleanType, "",
-                                     NodeManager::SKOLEM_EXACT_NAME);
-    Node m = NodeBuilder<>() << x << y << kind::OR;
-    Node n = NodeBuilder<>() << w << m << z << kind::AND;
-    Node o = NodeBuilder<>() << n << n << kind::XOR;
-
-    stringstream sstr;
-    sstr << Node::dag(false);
-    n.toStream(sstr);
-    TS_ASSERT(sstr.str() == "(AND w (OR x y) z)");
-
-    sstr.str(string());
-    o.toStream(sstr, -1, 0);
-    TS_ASSERT(sstr.str() == "(XOR (AND w (OR x y) z) (AND w (OR x y) z))");
-
-    sstr.str(string());
-    sstr << n;
-    TS_ASSERT(sstr.str() == "(AND w (OR x y) z)");
-
-    sstr.str(string());
-    sstr << o;
-    TS_ASSERT(sstr.str() == "(XOR (AND w (OR x y) z) (AND w (OR x y) z))");
-
-    sstr.str(string());
-    sstr << Node::setdepth(0) << n;
-    TS_ASSERT(sstr.str() == "(AND w (OR x y) z)");
-
-    sstr.str(string());
-    sstr << Node::setdepth(0) << o;
-    TS_ASSERT(sstr.str() == "(XOR (AND w (OR x y) z) (AND w (OR x y) z))");
-
-    sstr.str(string());
-    sstr << Node::setdepth(1) << n;
-    TS_ASSERT(sstr.str() == "(AND w (OR (...) (...)) z)");
-
-    sstr.str(string());
-    sstr << Node::setdepth(1) << o;
-    TS_ASSERT(sstr.str() ==
-              "(XOR (AND (...) (...) (...)) (AND (...) (...) (...)))");
-
-    sstr.str(string());
-    sstr << Node::setdepth(2) << n;
-    TS_ASSERT(sstr.str() == "(AND w (OR x y) z)");
-
-    sstr.str(string());
-    sstr << Node::setdepth(2) << o;
-    TS_ASSERT(sstr.str() ==
-              "(XOR (AND w (OR (...) (...)) z) (AND w (OR (...) (...)) z))");
-
-    sstr.str(string());
-    sstr << Node::setdepth(3) << n;
-    TS_ASSERT(sstr.str() == "(AND w (OR x y) z)");
-
-    sstr.str(string());
-    sstr << Node::setdepth(3) << o;
-    TS_ASSERT(sstr.str() == "(XOR (AND w (OR x y) z) (AND w (OR x y) z))");
-  }
-
-  void testDagifier() {
-    TypeNode intType = d_nodeManager->integerType();
-    TypeNode fnType = d_nodeManager->mkFunctionType(intType, intType);
-
-    Node x = d_nodeManager->mkSkolem("x", intType, "",
-                                     NodeManager::SKOLEM_EXACT_NAME);
-    Node y = d_nodeManager->mkSkolem("y", intType, "",
-                                     NodeManager::SKOLEM_EXACT_NAME);
-    Node f = d_nodeManager->mkSkolem("f", fnType, "",
-                                     NodeManager::SKOLEM_EXACT_NAME);
-    Node g = d_nodeManager->mkSkolem("g", fnType, "",
-                                     NodeManager::SKOLEM_EXACT_NAME);
-    Node fx = d_nodeManager->mkNode(APPLY_UF, f, x);
-    Node fy = d_nodeManager->mkNode(APPLY_UF, f, y);
-    Node gx = d_nodeManager->mkNode(APPLY_UF, g, x);
-    Node gy = d_nodeManager->mkNode(APPLY_UF, g, y);
-    Node fgx = d_nodeManager->mkNode(APPLY_UF, f, gx);
-    Node ffx = d_nodeManager->mkNode(APPLY_UF, f, fx);
-    Node fffx = d_nodeManager->mkNode(APPLY_UF, f, ffx);
-    Node fffx_eq_x = d_nodeManager->mkNode(EQUAL, fffx, x);
-    Node fffx_eq_y = d_nodeManager->mkNode(EQUAL, fffx, y);
-    Node fx_eq_gx = d_nodeManager->mkNode(EQUAL, fx, gx);
-    Node x_eq_y = d_nodeManager->mkNode(EQUAL, x, y);
-    Node fgx_eq_gy = d_nodeManager->mkNode(EQUAL, fgx, gy);
-
-    Node n = d_nodeManager->mkNode(OR, fffx_eq_x, fffx_eq_y, fx_eq_gx, x_eq_y,
-                                   fgx_eq_gy);
-
-    stringstream sstr;
-    sstr << Node::setdepth(-1)
-         << Node::setlanguage(language::output::LANG_CVC4);
-    sstr << Node::dag(false) << n;  // never dagify
-    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))");
-  }
-
-  void testForEachOverNodeAsNodes() {
-    const std::vector<Node> skolems =
-        makeNSkolemNodes(d_nodeManager, 3, d_nodeManager->integerType());
-    Node add = d_nodeManager->mkNode(kind::PLUS, skolems);
-    std::vector<Node> children;
-    for (Node child : add) {
-      children.push_back(child);
-    }
-    TS_ASSERT(children.size() == skolems.size() &&
-              std::equal(children.begin(), children.end(), skolems.begin()));
-  }
-
-  void testForEachOverNodeAsTNodes() {
-    const std::vector<Node> skolems =
-        makeNSkolemNodes(d_nodeManager, 3, d_nodeManager->integerType());
-    Node add = d_nodeManager->mkNode(kind::PLUS, skolems);
-    std::vector<TNode> children;
-    for (TNode child : add) {
-      children.push_back(child);
-    }
-    TS_ASSERT(children.size() == skolems.size() &&
-              std::equal(children.begin(), children.end(), skolems.begin()));
-  }
-
-  void testForEachOverTNodeAsNode() {
-    const std::vector<Node> skolems =
-        makeNSkolemNodes(d_nodeManager, 3, d_nodeManager->integerType());
-    Node add_node = d_nodeManager->mkNode(kind::PLUS, skolems);
-    TNode add_tnode = add_node;
-    std::vector<Node> children;
-    for (Node child : add_tnode) {
-      children.push_back(child);
-    }
-    TS_ASSERT(children.size() == skolems.size() &&
-              std::equal(children.begin(), children.end(), skolems.begin()));
-  }
-
-  void testForEachOverTNodeAsTNodes() {
-    const std::vector<Node> skolems =
-        makeNSkolemNodes(d_nodeManager, 3, d_nodeManager->integerType());
-    Node add_node = d_nodeManager->mkNode(kind::PLUS, skolems);
-    TNode add_tnode = add_node;
-    std::vector<TNode> children;
-    for (TNode child : add_tnode) {
-      children.push_back(child);
-    }
-    TS_ASSERT(children.size() == skolems.size() &&
-              std::equal(children.begin(), children.end(), skolems.begin()));
-  }
-
-  void testIsConst()
-  {
-    // more complicated "constants" exist in datatypes and arrays theories
-    DType list("list");
-    std::shared_ptr<DTypeConstructor> consC =
-        std::make_shared<DTypeConstructor>("cons");
-    consC->addArg("car", d_nodeManager->integerType());
-    consC->addArgSelf("cdr");
-    list.addConstructor(consC);
-    list.addConstructor(std::make_shared<DTypeConstructor>("nil"));
-    TypeNode listType = d_nodeManager->mkDatatypeType(list);
-    const std::vector<std::shared_ptr<DTypeConstructor> >& lcons =
-        listType.getDType().getConstructors();
-    Node cons = lcons[0]->getConstructor();
-    Node nil = lcons[1]->getConstructor();
-    Node x = d_nodeManager->mkSkolem("x", d_nodeManager->integerType());
-    Node cons_x_nil =
-        d_nodeManager->mkNode(APPLY_CONSTRUCTOR,
-                              cons,
-                              x,
-                              d_nodeManager->mkNode(APPLY_CONSTRUCTOR, nil));
-    Node cons_1_nil =
-        d_nodeManager->mkNode(APPLY_CONSTRUCTOR,
-                              cons,
-                              d_nodeManager->mkConst(Rational(1)),
-                              d_nodeManager->mkNode(APPLY_CONSTRUCTOR, nil));
-    Node cons_1_cons_2_nil = d_nodeManager->mkNode(
-        APPLY_CONSTRUCTOR,
-        cons,
-        d_nodeManager->mkConst(Rational(1)),
-        d_nodeManager->mkNode(APPLY_CONSTRUCTOR,
-                              cons,
-                              d_nodeManager->mkConst(Rational(2)),
-                              d_nodeManager->mkNode(APPLY_CONSTRUCTOR, nil)));
-    TS_ASSERT(d_nodeManager->mkNode(APPLY_CONSTRUCTOR, nil).isConst());
-    TS_ASSERT(!cons_x_nil.isConst());
-    TS_ASSERT(cons_1_nil.isConst());
-    TS_ASSERT(cons_1_cons_2_nil.isConst());
-
-    TypeNode arrType = d_nodeManager->mkArrayType(d_nodeManager->integerType(),
-                                                  d_nodeManager->integerType());
-    Node zero = d_nodeManager->mkConst(Rational(0));
-    Node one = d_nodeManager->mkConst(Rational(1));
-    Node storeAll = d_nodeManager->mkConst(ArrayStoreAll(arrType, zero));
-    TS_ASSERT(storeAll.isConst());
-
-    Node arr = d_nodeManager->mkNode(STORE, storeAll, zero, zero);
-    TS_ASSERT(!arr.isConst());
-    arr = d_nodeManager->mkNode(STORE, storeAll, zero, one);
-    TS_ASSERT(arr.isConst());
-    Node arr2 = d_nodeManager->mkNode(STORE, arr, one, zero);
-    TS_ASSERT(!arr2.isConst());
-    arr2 = d_nodeManager->mkNode(STORE, arr, zero, one);
-    TS_ASSERT(!arr2.isConst());
-
-    arrType = d_nodeManager->mkArrayType(d_nodeManager->mkBitVectorType(1),
-                                         d_nodeManager->mkBitVectorType(1));
-    zero = d_nodeManager->mkConst(BitVector(1, unsigned(0)));
-    one = d_nodeManager->mkConst(BitVector(1, unsigned(1)));
-    storeAll = d_nodeManager->mkConst(ArrayStoreAll(arrType, zero));
-    TS_ASSERT(storeAll.isConst());
-
-    arr = d_nodeManager->mkNode(STORE, storeAll, zero, zero);
-    TS_ASSERT(!arr.isConst());
-    arr = d_nodeManager->mkNode(STORE, storeAll, zero, one);
-    TS_ASSERT(arr.isConst());
-    arr2 = d_nodeManager->mkNode(STORE, arr, one, zero);
-    TS_ASSERT(!arr2.isConst());
-    arr2 = d_nodeManager->mkNode(STORE, arr, one, one);
-    TS_ASSERT(!arr2.isConst());
-    arr2 = d_nodeManager->mkNode(STORE, arr, zero, one);
-    TS_ASSERT(!arr2.isConst());
-  }
-
-  //  This Test is designed to fail in a way that will cause a segfault,
-  //  so it is commented out.
-  //  This is for demonstrating what a certain type of user error looks like.
-  //   Node level0(){
-  //     NodeBuilder<> nb(kind::AND);
-  //     Node x = d_nodeManager->mkSkolem("x", d_nodeManager->booleanType());
-  //     nb << x;
-  //     nb << x;
-  //     return Node(nb.constructNode());
-  //   }
-
-  //   TNode level1(){
-  //     return level0();
-  //   }
-
-  //   void testChaining() {
-  //     Node res = level1();
-
-  //     TS_ASSERT(res.getKind() == kind::NULL_EXPR);
-  //     TS_ASSERT(res != Node::null());
-
-  //     cerr << "I finished both tests now watch as I crash" << endl;
-  //   }
-};