From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Tue, 9 Feb 2021 20:04:13 +0000 (-0800)
Subject: google test: expr: Migrate node_manager_black. (#5857)
X-Git-Tag: cvc5-1.0.0~2299
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e302b6b1664d3a28c3f42de911f3c13e7b5d0605;p=cvc5.git

google test: expr: Migrate node_manager_black. (#5857)
---

diff --git a/test/unit/expr/CMakeLists.txt b/test/unit/expr/CMakeLists.txt
index 81ce20ed3..51e6edefe 100644
--- a/test/unit/expr/CMakeLists.txt
+++ b/test/unit/expr/CMakeLists.txt
@@ -18,7 +18,7 @@ cvc4_add_unit_test_black(kind_map_black expr)
 cvc4_add_unit_test_black(node_black expr)
 cvc4_add_unit_test_black(node_algorithm_black expr)
 cvc4_add_unit_test_black(node_builder_black expr)
-cvc4_add_cxx_unit_test_black(node_manager_black expr)
+cvc4_add_unit_test_black(node_manager_black expr)
 cvc4_add_unit_test_white(node_manager_white expr)
 cvc4_add_unit_test_black(node_self_iterator_black expr)
 cvc4_add_unit_test_black(node_traversal_black expr)
diff --git a/test/unit/expr/node_manager_black.cpp b/test/unit/expr/node_manager_black.cpp
new file mode 100644
index 000000000..09463a28e
--- /dev/null
+++ b/test/unit/expr/node_manager_black.cpp
@@ -0,0 +1,334 @@
+/*********************                                                        */
+/*! \file node_manager_black.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Aina Niemetz, Christopher L. Conway, Dejan Jovanovic
+ ** 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::NodeManager.
+ **
+ ** Black box testing of CVC4::NodeManager.
+ **/
+
+#include <string>
+#include <vector>
+
+#include "base/output.h"
+#include "expr/node_manager.h"
+#include "expr/node_manager_attributes.h"
+#include "test_node.h"
+#include "test_utils.h"
+#include "util/integer.h"
+#include "util/rational.h"
+
+namespace CVC4 {
+
+using namespace kind;
+using namespace expr;
+
+namespace test {
+
+class TestNodeBlackNodeManager : public TestNodeBlack
+{
+};
+
+TEST_F(TestNodeBlackNodeManager, mkNode_not)
+{
+  Node x = d_nodeManager->mkSkolem("x", d_nodeManager->booleanType());
+  Node n = d_nodeManager->mkNode(NOT, x);
+  ASSERT_EQ(n.getNumChildren(), 1u);
+  ASSERT_EQ(n.getKind(), NOT);
+  ASSERT_EQ(n[0], x);
+}
+
+TEST_F(TestNodeBlackNodeManager, mkNode_binary)
+{
+  Node x = d_nodeManager->mkSkolem("x", d_nodeManager->booleanType());
+  Node y = d_nodeManager->mkSkolem("y", d_nodeManager->booleanType());
+  Node n = d_nodeManager->mkNode(IMPLIES, x, y);
+  ASSERT_EQ(n.getNumChildren(), 2u);
+  ASSERT_EQ(n.getKind(), IMPLIES);
+  ASSERT_EQ(n[0], x);
+  ASSERT_EQ(n[1], y);
+}
+
+TEST_F(TestNodeBlackNodeManager, mkNode_three_children)
+{
+  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 = d_nodeManager->mkNode(AND, x, y, z);
+  ASSERT_EQ(n.getNumChildren(), 3u);
+  ASSERT_EQ(n.getKind(), AND);
+  ASSERT_EQ(n[0], x);
+  ASSERT_EQ(n[1], y);
+  ASSERT_EQ(n[2], z);
+}
+
+TEST_F(TestNodeBlackNodeManager, mkNode_four_children)
+{
+  Node x1 = d_nodeManager->mkSkolem("x1", d_nodeManager->booleanType());
+  Node x2 = d_nodeManager->mkSkolem("x2", d_nodeManager->booleanType());
+  Node x3 = d_nodeManager->mkSkolem("x3", d_nodeManager->booleanType());
+  Node x4 = d_nodeManager->mkSkolem("x4", d_nodeManager->booleanType());
+  Node n = d_nodeManager->mkNode(AND, x1, x2, x3, x4);
+  ASSERT_EQ(n.getNumChildren(), 4u);
+  ASSERT_EQ(n.getKind(), AND);
+  ASSERT_EQ(n[0], x1);
+  ASSERT_EQ(n[1], x2);
+  ASSERT_EQ(n[2], x3);
+  ASSERT_EQ(n[3], x4);
+}
+
+TEST_F(TestNodeBlackNodeManager, mkNode_five_children)
+{
+  Node x1 = d_nodeManager->mkSkolem("x1", d_nodeManager->booleanType());
+  Node x2 = d_nodeManager->mkSkolem("x2", d_nodeManager->booleanType());
+  Node x3 = d_nodeManager->mkSkolem("x3", d_nodeManager->booleanType());
+  Node x4 = d_nodeManager->mkSkolem("x4", d_nodeManager->booleanType());
+  Node x5 = d_nodeManager->mkSkolem("x5", d_nodeManager->booleanType());
+  Node n = d_nodeManager->mkNode(AND, x1, x2, x3, x4, x5);
+  ASSERT_EQ(n.getNumChildren(), 5u);
+  ASSERT_EQ(n.getKind(), AND);
+  ASSERT_EQ(n[0], x1);
+  ASSERT_EQ(n[1], x2);
+  ASSERT_EQ(n[2], x3);
+  ASSERT_EQ(n[3], x4);
+  ASSERT_EQ(n[4], x5);
+}
+
+TEST_F(TestNodeBlackNodeManager, mkNode_vector_of_node)
+{
+  Node x1 = d_nodeManager->mkSkolem("x1", d_nodeManager->booleanType());
+  Node x2 = d_nodeManager->mkSkolem("x2", d_nodeManager->booleanType());
+  Node x3 = d_nodeManager->mkSkolem("x3", d_nodeManager->booleanType());
+  std::vector<Node> args;
+  args.push_back(x1);
+  args.push_back(x2);
+  args.push_back(x3);
+  Node n = d_nodeManager->mkNode(AND, args);
+  ASSERT_EQ(n.getNumChildren(), args.size());
+  ASSERT_EQ(n.getKind(), AND);
+  for (unsigned i = 0; i < args.size(); ++i)
+  {
+    ASSERT_EQ(n[i], args[i]);
+  }
+}
+
+TEST_F(TestNodeBlackNodeManager, mkNode_vector_of_tnode)
+{
+  Node x1 = d_nodeManager->mkSkolem("x1", d_nodeManager->booleanType());
+  Node x2 = d_nodeManager->mkSkolem("x2", d_nodeManager->booleanType());
+  Node x3 = d_nodeManager->mkSkolem("x3", d_nodeManager->booleanType());
+  std::vector<TNode> args;
+  args.push_back(x1);
+  args.push_back(x2);
+  args.push_back(x3);
+  Node n = d_nodeManager->mkNode(AND, args);
+  ASSERT_EQ(n.getNumChildren(), args.size());
+  ASSERT_EQ(n.getKind(), AND);
+  for (unsigned i = 0; i < args.size(); ++i)
+  {
+    ASSERT_EQ(n[i], args[i]);
+  }
+}
+
+TEST_F(TestNodeBlackNodeManager, mkSkolem_with_name)
+{
+  Node x = d_nodeManager->mkSkolem(
+      "x", *d_boolTypeNode, "", NodeManager::SKOLEM_EXACT_NAME);
+  ASSERT_EQ(x.getKind(), SKOLEM);
+  ASSERT_EQ(x.getNumChildren(), 0u);
+  ASSERT_EQ(x.getAttribute(VarNameAttr()), "x");
+  ASSERT_EQ(x.getType(), *d_boolTypeNode);
+}
+
+TEST_F(TestNodeBlackNodeManager, mkConst_bool)
+{
+  Node tt = d_nodeManager->mkConst(true);
+  ASSERT_EQ(tt.getConst<bool>(), true);
+  Node ff = d_nodeManager->mkConst(false);
+  ASSERT_EQ(ff.getConst<bool>(), false);
+}
+
+TEST_F(TestNodeBlackNodeManager, mkConst_rational)
+{
+  Rational r("3/2");
+  Node n = d_nodeManager->mkConst(r);
+  ASSERT_EQ(n.getConst<Rational>(), r);
+}
+
+TEST_F(TestNodeBlackNodeManager, hasOperator)
+{
+  ASSERT_TRUE(NodeManager::hasOperator(AND));
+  ASSERT_TRUE(NodeManager::hasOperator(OR));
+  ASSERT_TRUE(NodeManager::hasOperator(NOT));
+  ASSERT_TRUE(NodeManager::hasOperator(APPLY_UF));
+  ASSERT_TRUE(!NodeManager::hasOperator(VARIABLE));
+}
+
+TEST_F(TestNodeBlackNodeManager, booleanType)
+{
+  TypeNode t = d_nodeManager->booleanType();
+  TypeNode t2 = d_nodeManager->booleanType();
+  TypeNode t3 = d_nodeManager->mkSort("T");
+  ASSERT_TRUE(t.isBoolean());
+  ASSERT_FALSE(t.isFunction());
+  ASSERT_FALSE(t.isNull());
+  ASSERT_FALSE(t.isPredicate());
+  ASSERT_FALSE(t.isSort());
+  ASSERT_EQ(t, t2);
+  ASSERT_NE(t, t3);
+
+  TypeNode bt = t;
+  ASSERT_EQ(bt, t);
+}
+
+TEST_F(TestNodeBlackNodeManager, mkFunctionType_bool_to_bool)
+{
+  TypeNode booleanType = d_nodeManager->booleanType();
+  TypeNode t = d_nodeManager->mkFunctionType(booleanType, booleanType);
+  TypeNode t2 = d_nodeManager->mkFunctionType(booleanType, booleanType);
+
+  ASSERT_FALSE(t.isBoolean());
+  ASSERT_TRUE(t.isFunction());
+  ASSERT_FALSE(t.isNull());
+  ASSERT_TRUE(t.isPredicate());
+  ASSERT_FALSE(t.isSort());
+
+  ASSERT_EQ(t, t2);
+
+  TypeNode ft = t;
+  ASSERT_EQ(ft, t);
+  ASSERT_EQ(ft.getArgTypes().size(), 1u);
+  ASSERT_EQ(ft.getArgTypes()[0], booleanType);
+  ASSERT_EQ(ft.getRangeType(), booleanType);
+}
+
+TEST_F(TestNodeBlackNodeManager, mkFunctionType_vector_args_with_return_type)
+{
+  TypeNode a = d_nodeManager->mkSort();
+  TypeNode b = d_nodeManager->mkSort();
+  TypeNode c = d_nodeManager->mkSort();
+
+  std::vector<TypeNode> argTypes;
+  argTypes.push_back(a);
+  argTypes.push_back(b);
+
+  TypeNode t = d_nodeManager->mkFunctionType(argTypes, c);
+  TypeNode t2 = d_nodeManager->mkFunctionType(argTypes, c);
+
+  ASSERT_FALSE(t.isBoolean());
+  ASSERT_TRUE(t.isFunction());
+  ASSERT_FALSE(t.isNull());
+  ASSERT_FALSE(t.isPredicate());
+  ASSERT_FALSE(t.isSort());
+
+  ASSERT_EQ(t, t2);
+
+  TypeNode ft = t;
+  ASSERT_EQ(ft, t);
+  ASSERT_EQ(ft.getArgTypes().size(), argTypes.size());
+  ASSERT_EQ(ft.getArgTypes()[0], a);
+  ASSERT_EQ(ft.getArgTypes()[1], b);
+  ASSERT_EQ(ft.getRangeType(), c);
+}
+
+TEST_F(TestNodeBlackNodeManager, mkFunctionType_vector_of_arguments)
+{
+  TypeNode a = d_nodeManager->mkSort();
+  TypeNode b = d_nodeManager->mkSort();
+  TypeNode c = d_nodeManager->mkSort();
+
+  std::vector<TypeNode> types;
+  types.push_back(a);
+  types.push_back(b);
+  types.push_back(c);
+
+  TypeNode t = d_nodeManager->mkFunctionType(types);
+  TypeNode t2 = d_nodeManager->mkFunctionType(types);
+
+  ASSERT_FALSE(t.isBoolean());
+  ASSERT_TRUE(t.isFunction());
+  ASSERT_FALSE(t.isNull());
+  ASSERT_FALSE(t.isPredicate());
+  ASSERT_FALSE(t.isSort());
+
+  ASSERT_EQ(t, t2);
+
+  TypeNode ft = t;
+  ASSERT_EQ(ft, t);
+  ASSERT_EQ(ft.getArgTypes().size(), types.size() - 1);
+  ASSERT_EQ(ft.getArgTypes()[0], a);
+  ASSERT_EQ(ft.getArgTypes()[1], b);
+  ASSERT_EQ(ft.getRangeType(), c);
+}
+
+TEST_F(TestNodeBlackNodeManager, mkPredicateType)
+{
+  TypeNode a = d_nodeManager->mkSort("a");
+  TypeNode b = d_nodeManager->mkSort("b");
+  TypeNode c = d_nodeManager->mkSort("c");
+  TypeNode booleanType = d_nodeManager->booleanType();
+
+  std::vector<TypeNode> argTypes;
+  argTypes.push_back(a);
+  argTypes.push_back(b);
+  argTypes.push_back(c);
+
+  TypeNode t = d_nodeManager->mkPredicateType(argTypes);
+  TypeNode t2 = d_nodeManager->mkPredicateType(argTypes);
+
+  ASSERT_FALSE(t.isBoolean());
+  ASSERT_TRUE(t.isFunction());
+  ASSERT_FALSE(t.isNull());
+  ASSERT_TRUE(t.isPredicate());
+  ASSERT_FALSE(t.isSort());
+
+  ASSERT_EQ(t, t2);
+
+  TypeNode ft = t;
+  ASSERT_EQ(ft, t);
+  ASSERT_EQ(ft.getArgTypes().size(), argTypes.size());
+  ASSERT_EQ(ft.getArgTypes()[0], a);
+  ASSERT_EQ(ft.getArgTypes()[1], b);
+  ASSERT_EQ(ft.getArgTypes()[2], c);
+  ASSERT_EQ(ft.getRangeType(), booleanType);
+}
+
+/* This test is only valid if assertions are enabled. */
+TEST_F(TestNodeBlackNodeManager, mkNode_too_few_children)
+{
+#ifdef CVC4_ASSERTIONS
+  Node x = d_nodeManager->mkSkolem("x", d_nodeManager->booleanType());
+  ASSERT_DEATH(d_nodeManager->mkNode(AND, x),
+               "Nodes with kind AND must have at least 2 children");
+#endif
+}
+
+/* This test is only valid if assertions are enabled. */
+TEST_F(TestNodeBlackNodeManager, mkNode_too_many_children)
+{
+#ifdef CVC4_ASSERTIONS
+  std::vector<Node> vars;
+  const unsigned int max = metakind::getUpperBoundForKind(AND);
+  TypeNode boolType = d_nodeManager->booleanType();
+  Node skolem_i = d_nodeManager->mkSkolem("i", boolType);
+  Node skolem_j = d_nodeManager->mkSkolem("j", boolType);
+  Node andNode = skolem_i.andNode(skolem_j);
+  Node orNode = skolem_i.orNode(skolem_j);
+  while (vars.size() <= max)
+  {
+    vars.push_back(andNode);
+    vars.push_back(skolem_j);
+    vars.push_back(orNode);
+  }
+  ASSERT_DEATH(d_nodeManager->mkNode(AND, vars), "toSize > d_nvMaxChildren");
+#endif
+}
+}  // namespace test
+}  // namespace CVC4
diff --git a/test/unit/expr/node_manager_black.h b/test/unit/expr/node_manager_black.h
deleted file mode 100644
index be9500337..000000000
--- a/test/unit/expr/node_manager_black.h
+++ /dev/null
@@ -1,326 +0,0 @@
-/*********************                                                        */
-/*! \file node_manager_black.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Christopher L. Conway, Dejan Jovanovic, Morgan Deters
- ** 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 White box testing of CVC4::NodeManager.
- **
- ** White box testing of CVC4::NodeManager.
- **/
-
-#include <cxxtest/TestSuite.h>
-
-#include <string>
-#include <vector>
-
-#include "base/output.h"
-#include "expr/node_manager.h"
-#include "expr/node_manager_attributes.h"
-#include "test_utils.h"
-#include "util/integer.h"
-#include "util/rational.h"
-
-using namespace CVC4;
-using namespace CVC4::expr;
-using namespace CVC4::kind;
-
-class NodeManagerBlack : public CxxTest::TestSuite {
-
-  NodeManager* d_nodeManager;
-  NodeManagerScope* d_scope;
-
- public:
-  void setUp() override
-  {
-    d_nodeManager = new NodeManager(NULL);
-    d_scope = new NodeManagerScope(d_nodeManager);
-  }
-
-  void tearDown() override
-  {
-    delete d_scope;
-    delete d_nodeManager;
-  }
-
-  void testMkNodeNot() {
-    Node x = d_nodeManager->mkSkolem("x",d_nodeManager->booleanType());
-    Node n = d_nodeManager->mkNode(NOT, x);
-    TS_ASSERT_EQUALS( n.getNumChildren(), 1u );
-    TS_ASSERT_EQUALS( n.getKind(), NOT);
-    TS_ASSERT_EQUALS( n[0], x);
-  }
-
-  void testMkNodeBinary() {
-    Node x = d_nodeManager->mkSkolem("x",d_nodeManager->booleanType());
-    Node y = d_nodeManager->mkSkolem("y",d_nodeManager->booleanType());
-    Node n = d_nodeManager->mkNode(IMPLIES, x, y);
-    TS_ASSERT_EQUALS( n.getNumChildren(), 2u );
-    TS_ASSERT_EQUALS( n.getKind(), IMPLIES);
-    TS_ASSERT_EQUALS( n[0], x);
-    TS_ASSERT_EQUALS( n[1], y);
-  }
-
-  void testMkNodeThreeChildren() {
-    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 = d_nodeManager->mkNode(AND, x, y, z);
-    TS_ASSERT_EQUALS( n.getNumChildren(), 3u );
-    TS_ASSERT_EQUALS( n.getKind(), AND);
-    TS_ASSERT_EQUALS( n[0], x);
-    TS_ASSERT_EQUALS( n[1], y);
-    TS_ASSERT_EQUALS( n[2], z);
-  }
-
-  void testMkNodeFourChildren() {
-    Node x1 = d_nodeManager->mkSkolem("x1",d_nodeManager->booleanType());
-    Node x2 = d_nodeManager->mkSkolem("x2",d_nodeManager->booleanType());
-    Node x3 = d_nodeManager->mkSkolem("x3",d_nodeManager->booleanType());
-    Node x4 = d_nodeManager->mkSkolem("x4",d_nodeManager->booleanType());
-    Node n = d_nodeManager->mkNode(AND, x1, x2, x3, x4);
-    TS_ASSERT_EQUALS( n.getNumChildren(), 4u );
-    TS_ASSERT_EQUALS( n.getKind(), AND );
-    TS_ASSERT_EQUALS( n[0], x1 );
-    TS_ASSERT_EQUALS( n[1], x2 );
-    TS_ASSERT_EQUALS( n[2], x3 );
-    TS_ASSERT_EQUALS( n[3], x4 );
-  }
-
-  void testMkNodeFiveChildren() {
-    Node x1 = d_nodeManager->mkSkolem("x1",d_nodeManager->booleanType());
-    Node x2 = d_nodeManager->mkSkolem("x2",d_nodeManager->booleanType());
-    Node x3 = d_nodeManager->mkSkolem("x3",d_nodeManager->booleanType());
-    Node x4 = d_nodeManager->mkSkolem("x4",d_nodeManager->booleanType());
-    Node x5 = d_nodeManager->mkSkolem("x5",d_nodeManager->booleanType());
-    Node n = d_nodeManager->mkNode(AND, x1, x2, x3, x4, x5);
-    TS_ASSERT_EQUALS( n.getNumChildren(), 5u );
-    TS_ASSERT_EQUALS( n.getKind(), AND);
-    TS_ASSERT_EQUALS( n[0], x1);
-    TS_ASSERT_EQUALS( n[1], x2);
-    TS_ASSERT_EQUALS( n[2], x3);
-    TS_ASSERT_EQUALS( n[3], x4);
-    TS_ASSERT_EQUALS( n[4], x5);
-  }
-
-  void testMkNodeVectorOfNodeChildren() {
-    Node x1 = d_nodeManager->mkSkolem("x1",d_nodeManager->booleanType());
-    Node x2 = d_nodeManager->mkSkolem("x2",d_nodeManager->booleanType());
-    Node x3 = d_nodeManager->mkSkolem("x3",d_nodeManager->booleanType());
-    std::vector<Node> args;
-    args.push_back(x1);
-    args.push_back(x2);
-    args.push_back(x3);
-    Node n = d_nodeManager->mkNode(AND, args);
-    TS_ASSERT_EQUALS( n.getNumChildren(), args.size() );
-    TS_ASSERT_EQUALS( n.getKind(), AND);
-    for( unsigned i = 0; i < args.size(); ++i ) {
-      TS_ASSERT_EQUALS( n[i], args[i]);
-    }
-  }
-
-  void testMkNodeVectorOfTNodeChildren() {
-    Node x1 = d_nodeManager->mkSkolem("x1",d_nodeManager->booleanType());
-    Node x2 = d_nodeManager->mkSkolem("x2",d_nodeManager->booleanType());
-    Node x3 = d_nodeManager->mkSkolem("x3",d_nodeManager->booleanType());
-    std::vector<TNode> args;
-    args.push_back(x1);
-    args.push_back(x2);
-    args.push_back(x3);
-    Node n = d_nodeManager->mkNode(AND, args);
-    TS_ASSERT_EQUALS( n.getNumChildren(), args.size() );
-    TS_ASSERT_EQUALS( n.getKind(), AND);
-    for( unsigned i = 0; i < args.size(); ++i ) {
-      TS_ASSERT_EQUALS( n[i], args[i]);
-    }
-  }
-
-  void testMkVarWithName() {
-    TypeNode booleanType = d_nodeManager->booleanType();
-    Node x = d_nodeManager->mkSkolem("x", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
-    TS_ASSERT_EQUALS(x.getKind(),SKOLEM);
-    TS_ASSERT_EQUALS(x.getNumChildren(),0u);
-    TS_ASSERT_EQUALS(x.getAttribute(VarNameAttr()),"x");
-    TS_ASSERT_EQUALS(x.getType(),booleanType);
-  }
-
-  void testMkConstBool() {
-    Node tt = d_nodeManager->mkConst(true);
-    TS_ASSERT_EQUALS(tt.getConst<bool>(),true);
-    Node ff = d_nodeManager->mkConst(false);
-    TS_ASSERT_EQUALS(ff.getConst<bool>(),false);
-  }
-
-  void testMkConstRat() {
-    Rational r("3/2");
-    Node n = d_nodeManager->mkConst(r);
-    TS_ASSERT_EQUALS(n.getConst<Rational>(),r);
-  }
-
-  void testHasOperator() {
-    TS_ASSERT( NodeManager::hasOperator(AND) );
-    TS_ASSERT( NodeManager::hasOperator(OR) );
-    TS_ASSERT( NodeManager::hasOperator(NOT) );
-    TS_ASSERT( NodeManager::hasOperator(APPLY_UF) );
-    TS_ASSERT( !NodeManager::hasOperator(VARIABLE) );
-  }
-
-  void testBooleanType() {
-    TypeNode t = d_nodeManager->booleanType();
-    TypeNode t2 = d_nodeManager->booleanType();
-    TypeNode t3 = d_nodeManager->mkSort("T");
-    TS_ASSERT( t.isBoolean() );
-    TS_ASSERT( !t.isFunction() );
-    TS_ASSERT( !t.isNull() );
-    TS_ASSERT( !t.isPredicate() );
-    TS_ASSERT( !t.isSort() );
-    TS_ASSERT_EQUALS(t, t2);
-    TS_ASSERT( t != t3 );
-
-    TypeNode bt = t;
-    TS_ASSERT_EQUALS( bt, t);
-  }
-
-  void testMkFunctionTypeBoolToBool() {
-    TypeNode booleanType = d_nodeManager->booleanType();
-    TypeNode t = d_nodeManager->mkFunctionType(booleanType,booleanType);
-    TypeNode t2 = d_nodeManager->mkFunctionType(booleanType,booleanType);
-
-    TS_ASSERT( !t.isBoolean() );
-    TS_ASSERT( t.isFunction() );
-    TS_ASSERT( !t.isNull() );
-    TS_ASSERT( t.isPredicate() );
-    TS_ASSERT( !t.isSort() );
-
-    TS_ASSERT_EQUALS( t, t2 );
-
-    TypeNode ft = t;
-    TS_ASSERT_EQUALS( ft, t );
-    TS_ASSERT_EQUALS(ft.getArgTypes().size(), 1u);
-    TS_ASSERT_EQUALS(ft.getArgTypes()[0], booleanType);
-    TS_ASSERT_EQUALS(ft.getRangeType(), booleanType);
-
-  }
-
-  void testMkFunctionTypeVectorOfArgsWithReturnType() {
-    TypeNode a = d_nodeManager->mkSort();
-    TypeNode b = d_nodeManager->mkSort();
-    TypeNode c = d_nodeManager->mkSort();
-
-    std::vector<TypeNode> argTypes;
-    argTypes.push_back(a);
-    argTypes.push_back(b);
-
-    TypeNode t = d_nodeManager->mkFunctionType(argTypes,c);
-    TypeNode t2 = d_nodeManager->mkFunctionType(argTypes,c);
-
-    TS_ASSERT( !t.isBoolean() );
-    TS_ASSERT( t.isFunction() );
-    TS_ASSERT( !t.isNull() );
-    TS_ASSERT( !t.isPredicate() );
-    TS_ASSERT( !t.isSort() );
-
-    TS_ASSERT_EQUALS( t, t2 );
-
-    TypeNode ft = t;
-    TS_ASSERT_EQUALS( ft, t );
-    TS_ASSERT_EQUALS(ft.getArgTypes().size(), argTypes.size());
-    TS_ASSERT_EQUALS(ft.getArgTypes()[0], a);
-    TS_ASSERT_EQUALS(ft.getArgTypes()[1], b);
-    TS_ASSERT_EQUALS(ft.getRangeType(), c);
-
-  }
-
-  void testMkFunctionTypeVectorOfArguments() {
-    TypeNode a = d_nodeManager->mkSort();
-    TypeNode b = d_nodeManager->mkSort();
-    TypeNode c = d_nodeManager->mkSort();
-
-    std::vector<TypeNode> types;
-    types.push_back(a);
-    types.push_back(b);
-    types.push_back(c);
-
-    TypeNode t = d_nodeManager->mkFunctionType(types);
-    TypeNode t2 = d_nodeManager->mkFunctionType(types);
-
-    TS_ASSERT( !t.isBoolean() );
-    TS_ASSERT( t.isFunction() );
-    TS_ASSERT( !t.isNull() );
-    TS_ASSERT( !t.isPredicate() );
-    TS_ASSERT( !t.isSort() );
-
-    TS_ASSERT_EQUALS( t, t2 );
-
-    TypeNode ft = t;
-    TS_ASSERT_EQUALS( ft, t );
-    TS_ASSERT_EQUALS(ft.getArgTypes().size(), types.size()-1);
-    TS_ASSERT_EQUALS(ft.getArgTypes()[0], a);
-    TS_ASSERT_EQUALS(ft.getArgTypes()[1], b);
-    TS_ASSERT_EQUALS(ft.getRangeType(), c);
-  }
-
-  void testMkPredicateType() {
-    TypeNode a = d_nodeManager->mkSort("a");
-    TypeNode b = d_nodeManager->mkSort("b");
-    TypeNode c = d_nodeManager->mkSort("c");
-    TypeNode booleanType = d_nodeManager->booleanType();
-
-    std::vector<TypeNode> argTypes;
-    argTypes.push_back(a);
-    argTypes.push_back(b);
-    argTypes.push_back(c);
-
-    TypeNode t = d_nodeManager->mkPredicateType(argTypes);
-    TypeNode t2 = d_nodeManager->mkPredicateType(argTypes);
-
-    TS_ASSERT( !t.isBoolean() );
-    TS_ASSERT( t.isFunction() );
-    TS_ASSERT( !t.isNull() );
-    TS_ASSERT( t.isPredicate() );
-    TS_ASSERT( !t.isSort() );
-
-    TS_ASSERT_EQUALS( t, t2 );
-
-    TypeNode ft = t;
-    TS_ASSERT_EQUALS( ft, t );
-    TS_ASSERT_EQUALS(ft.getArgTypes().size(), argTypes.size());
-    TS_ASSERT_EQUALS(ft.getArgTypes()[0], a);
-    TS_ASSERT_EQUALS(ft.getArgTypes()[1], b);
-    TS_ASSERT_EQUALS(ft.getArgTypes()[2], c);
-    TS_ASSERT_EQUALS(ft.getRangeType(), booleanType);
-
-  }
-
-  /* This test is only valid if assertions are enabled. */
-  void testMkNodeTooFew() {
-#ifdef CVC4_ASSERTIONS
-    Node x = d_nodeManager->mkSkolem( "x", d_nodeManager->booleanType() );
-    TS_UTILS_EXPECT_ABORT(d_nodeManager->mkNode(AND, x));
-#endif
-  }
-
-  /* This test is only valid if assertions are enabled. */
-  void testMkNodeTooMany() {
-#ifdef CVC4_ASSERTIONS
-    std::vector<Node> vars;
-    const unsigned int max = metakind::getUpperBoundForKind(AND);
-    TypeNode boolType = d_nodeManager->booleanType();
-    Node skolem_i = d_nodeManager->mkSkolem("i", boolType);
-    Node skolem_j = d_nodeManager->mkSkolem("j", boolType);
-    Node andNode = skolem_i.andNode(skolem_j);
-    Node orNode = skolem_i.orNode(skolem_j);
-    while (vars.size() <= max) {
-      vars.push_back(andNode);
-      vars.push_back(skolem_j);
-      vars.push_back(orNode);
-    }
-    TS_UTILS_EXPECT_ABORT(d_nodeManager->mkNode(AND, vars));
-#endif
-  }
-};