fix unit tests

diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp
index 48f773c548d8af04094ca268a05719283570c670..50bd5016d36f97a7828465f4e97b387fcea6234d 100644 (file)
--- a/src/printer/ast/ast_printer.cpp
+++ b/src/printer/ast/ast_printer.cpp
@@ -80,11 +80,6 @@ void AstPrinter::toStream(std::ostream& out, TNode n,
 
   // variable
   if(n.getMetaKind() == kind::metakind::VARIABLE) {
-    if(n.getKind() != kind::VARIABLE &&
-       n.getKind() != kind::SORT_TYPE) {
-      out << n.getKind() << ':';
-    }
-
     string s;
     if(n.getAttribute(expr::VarNameAttr(), s)) {
       out << s;

diff --git a/test/unit/context/stacking_map_black.h b/test/unit/context/stacking_map_black.h
index f0feb12930d511b31e9ce912c79debda3789c2dc..fd7d3cc42a54eab335d786f070cce351f6c2b290 100644 (file)
--- a/test/unit/context/stacking_map_black.h
+++ b/test/unit/context/stacking_map_black.h
@@ -46,13 +46,13 @@ public:
     d_scope = new NodeManagerScope(d_nm);
     d_mapPtr = new StackingMap<TNode, TNode, TNodeHashFunction>(d_ctxt);
 
-    a = d_nm->mkVar("a", d_nm->realType());
-    b = d_nm->mkVar("b", d_nm->realType());
-    c = d_nm->mkVar("c", d_nm->realType());
-    d = d_nm->mkVar("d", d_nm->realType());
-    e = d_nm->mkVar("e", d_nm->realType());
-    f = d_nm->mkVar("f", d_nm->realType());
-    g = d_nm->mkVar("g", d_nm->realType());
+    a = d_nm->mkSkolem("a", d_nm->realType());
+    b = d_nm->mkSkolem("b", d_nm->realType());
+    c = d_nm->mkSkolem("c", d_nm->realType());
+    d = d_nm->mkSkolem("d", d_nm->realType());
+    e = d_nm->mkSkolem("e", d_nm->realType());
+    f = d_nm->mkSkolem("f", d_nm->realType());
+    g = d_nm->mkSkolem("g", d_nm->realType());
   }
 
   void tearDown() {

diff --git a/test/unit/context/stacking_vector_black.h b/test/unit/context/stacking_vector_black.h
index 5f410881ba8ec0d5327ae3c30b11fbc4baf6d9ab..3dd59dc91daef64be27762034ff32bac36ca474b 100644 (file)
--- a/test/unit/context/stacking_vector_black.h
+++ b/test/unit/context/stacking_vector_black.h
@@ -46,13 +46,13 @@ public:
     d_scope = new NodeManagerScope(d_nm);
     d_vectorPtr = new StackingVector<TNode>(d_ctxt);
 
-    a = d_nm->mkVar("a", d_nm->realType());
-    b = d_nm->mkVar("b", d_nm->realType());
-    c = d_nm->mkVar("c", d_nm->realType());
-    d = d_nm->mkVar("d", d_nm->realType());
-    e = d_nm->mkVar("e", d_nm->realType());
-    f = d_nm->mkVar("f", d_nm->realType());
-    g = d_nm->mkVar("g", d_nm->realType());
+    a = d_nm->mkSkolem("a", d_nm->realType());
+    b = d_nm->mkSkolem("b", d_nm->realType());
+    c = d_nm->mkSkolem("c", d_nm->realType());
+    d = d_nm->mkSkolem("d", d_nm->realType());
+    e = d_nm->mkSkolem("e", d_nm->realType());
+    f = d_nm->mkSkolem("f", d_nm->realType());
+    g = d_nm->mkSkolem("g", d_nm->realType());
   }
 
   void tearDown() {

diff --git a/test/unit/expr/attribute_black.h b/test/unit/expr/attribute_black.h
index 8e7f897959784d5cfef4d7857112685853a7367f..93fbe049a45082e1f2a25e05c61c8b14d3f88df2 100644 (file)
--- a/test/unit/expr/attribute_black.h
+++ b/test/unit/expr/attribute_black.h
@@ -74,7 +74,7 @@ public:
 
   void testDeallocation() {
     TypeNode booleanType = d_nodeManager->booleanType();
-    Node* node = new Node(d_nodeManager->mkVar(booleanType));
+    Node* node = new Node(d_nodeManager->mkSkolem(booleanType));
     MyData* data;
     MyData* data1;
     MyDataAttribute attr;
@@ -92,7 +92,7 @@ public:
   typedef expr::CDAttribute<CDPrimitiveIntAttributeId,uint64_t> CDPrimitiveIntAttribute;
   void testInts(){
     TypeNode booleanType = d_nodeManager->booleanType();
-    Node* node = new Node(d_nodeManager->mkVar(booleanType));
+    Node* node = new Node(d_nodeManager->mkSkolem(booleanType));
     const uint64_t val = 63489;
     uint64_t data0 = 0;
     uint64_t data1 = 0;
@@ -120,9 +120,9 @@ public:
   typedef expr::CDAttribute<CDTNodeAttributeId, TNode> CDTNodeAttribute;
   void testTNodes(){
     TypeNode booleanType = d_nodeManager->booleanType();
-    Node* node = new Node(d_nodeManager->mkVar(booleanType));
+    Node* node = new Node(d_nodeManager->mkSkolem(booleanType));
 
-    Node val(d_nodeManager->mkVar(booleanType));
+    Node val(d_nodeManager->mkSkolem(booleanType));
     TNode data0;
     TNode data1;
 
@@ -155,7 +155,7 @@ public:
   typedef expr::CDAttribute<CDPtrAttributeId, Foo*> CDPtrAttribute;
   void testPtrs(){
     TypeNode booleanType = d_nodeManager->booleanType();
-    Node* node = new Node(d_nodeManager->mkVar(booleanType));
+    Node* node = new Node(d_nodeManager->mkSkolem(booleanType));
 
     Foo* val = new Foo(63489);
     Foo* data0 = NULL;
@@ -186,7 +186,7 @@ public:
   typedef expr::CDAttribute<CDConstPtrAttributeId, const Foo*> CDConstPtrAttribute;
   void testConstPtrs(){
     TypeNode booleanType = d_nodeManager->booleanType();
-    Node* node = new Node(d_nodeManager->mkVar(booleanType));
+    Node* node = new Node(d_nodeManager->mkSkolem(booleanType));
 
     const Foo* val = new Foo(63489);
     const Foo* data0 = NULL;
@@ -216,7 +216,7 @@ public:
   typedef expr::CDAttribute<CDStringAttributeId, std::string> CDStringAttribute;
   void testStrings(){
     TypeNode booleanType = d_nodeManager->booleanType();
-    Node* node = new Node(d_nodeManager->mkVar(booleanType));
+    Node* node = new Node(d_nodeManager->mkSkolem(booleanType));
 
     std::string val("63489");
     std::string data0;
@@ -245,7 +245,7 @@ public:
   typedef expr::CDAttribute<CDBoolAttributeId, bool> CDBoolAttribute;
   void testBools(){
     TypeNode booleanType = d_nodeManager->booleanType();
-    Node* node = new Node(d_nodeManager->mkVar(booleanType));
+    Node* node = new Node(d_nodeManager->mkSkolem(booleanType));
 
     bool val = true;
     bool data0 = false;

diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h
index f617ebd5b555f6b214158fbf5c61bbb87c86df27..53af9db5397a4f249ebd9ad30bc44eafaa5c7a62 100644 (file)
--- a/test/unit/expr/node_black.h
+++ b/test/unit/expr/node_black.h
@@ -102,12 +102,12 @@ public:
   void testOperatorEquals() {
     Node a, b, c;
 
-    b = d_nodeManager->mkVar(*d_booleanType);
+    b = d_nodeManager->mkSkolem(*d_booleanType);
 
     a = b;
     c = a;
 
-    Node d = d_nodeManager->mkVar(*d_booleanType);
+    Node d = d_nodeManager->mkSkolem(*d_booleanType);
 
     TS_ASSERT(a==a);
     TS_ASSERT(a==b);
@@ -142,12 +142,12 @@ public:
 
     Node a, b, c;
 
-    b = d_nodeManager->mkVar(*d_booleanType);
+    b = d_nodeManager->mkSkolem(*d_booleanType);
 
     a = b;
     c = a;
 
-    Node d = d_nodeManager->mkVar(*d_booleanType);
+    Node d = d_nodeManager->mkSkolem(*d_booleanType);
 
     /*structed assuming operator == works */
     TS_ASSERT(iff(a!=a, !(a==a)));
@@ -204,7 +204,7 @@ public:
   /*tests:   Node& operator=(const Node&); */
   void testOperatorAssign() {
     Node a, b;
-    Node c = d_nodeManager->mkNode(NOT, d_nodeManager->mkVar(*d_booleanType));
+    Node c = d_nodeManager->mkNode(NOT, d_nodeManager->mkSkolem(*d_booleanType));
 
     b = c;
     TS_ASSERT(b==c);
@@ -220,8 +220,8 @@ public:
     /* We don't have access to the ids so we can't test the implementation
      * in the black box tests. */
 
-    Node a = d_nodeManager->mkVar("a", d_nodeManager->booleanType());
-    Node b = d_nodeManager->mkVar("b", d_nodeManager->booleanType());
+    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));
@@ -268,8 +268,8 @@ public:
     /* Node eqNode(const Node& right) const; */
 
     TypeNode t = d_nodeManager->mkSort();
-    Node left = d_nodeManager->mkVar(t);
-    Node right = d_nodeManager->mkVar(t);
+    Node left = d_nodeManager->mkSkolem(t);
+    Node right = d_nodeManager->mkSkolem(t);
     Node eq = left.eqNode(right);
 
     TS_ASSERT(EQUAL == eq.getKind());
@@ -326,8 +326,8 @@ public:
   void testIteNode() {
     /*Node iteNode(const Node& thenpart, const Node& elsepart) const;*/
 
-    Node a = d_nodeManager->mkVar(*d_booleanType);
-    Node b = d_nodeManager->mkVar(*d_booleanType);
+    Node a = d_nodeManager->mkSkolem(*d_booleanType);
+    Node b = d_nodeManager->mkSkolem(*d_booleanType);
 
     Node cnd = d_nodeManager->mkNode(OR, a, b);
     Node thenBranch = d_nodeManager->mkConst(true);
@@ -389,8 +389,8 @@ public:
   void testGetKind() {
     /*inline Kind getKind() const; */
 
-    Node a = d_nodeManager->mkVar(*d_booleanType);
-    Node b = d_nodeManager->mkVar(*d_booleanType);
+    Node a = d_nodeManager->mkSkolem(*d_booleanType);
+    Node b = d_nodeManager->mkSkolem(*d_booleanType);
 
     Node n = d_nodeManager->mkNode(NOT, a);
     TS_ASSERT(NOT == n.getKind());
@@ -398,8 +398,8 @@ public:
     n = d_nodeManager->mkNode(IFF, a, b);
     TS_ASSERT(IFF == n.getKind());
 
-    Node x = d_nodeManager->mkVar(*d_realType);
-    Node y = d_nodeManager->mkVar(*d_realType);
+    Node x = d_nodeManager->mkSkolem(*d_realType);
+    Node y = d_nodeManager->mkSkolem(*d_realType);
 
     n = d_nodeManager->mkNode(PLUS, x, y);
     TS_ASSERT(PLUS == n.getKind());
@@ -413,8 +413,8 @@ public:
     TypeNode booleanType = d_nodeManager->booleanType();
     TypeNode predType = d_nodeManager->mkFunctionType(sort, booleanType);
 
-    Node f = d_nodeManager->mkVar(predType);
-    Node a = d_nodeManager->mkVar(sort);
+    Node f = d_nodeManager->mkSkolem(predType);
+    Node a = d_nodeManager->mkSkolem(sort);
     Node fa = d_nodeManager->mkNode(kind::APPLY_UF, f, a);
 
     TS_ASSERT( fa.hasOperator() );
@@ -476,9 +476,9 @@ public:
   // test iterators
   void testIterator() {
     NodeBuilder<> b;
-    Node x = d_nodeManager->mkVar(*d_booleanType);
-    Node y = d_nodeManager->mkVar(*d_booleanType);
-    Node z = d_nodeManager->mkVar(*d_booleanType);
+    Node x = d_nodeManager->mkSkolem(*d_booleanType);
+    Node y = d_nodeManager->mkSkolem(*d_booleanType);
+    Node z = d_nodeManager->mkSkolem(*d_booleanType);
     Node n = b << x << y << z << kind::AND;
 
     { // iterator
@@ -503,9 +503,9 @@ public:
   void testKindedIterator() {
     TypeNode integerType = d_nodeManager->integerType();
 
-    Node x = d_nodeManager->mkVar("x", integerType);
-    Node y = d_nodeManager->mkVar("y", integerType);
-    Node z = d_nodeManager->mkVar("z", 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);
 
@@ -525,10 +525,10 @@ public:
   void testToString() {
     TypeNode booleanType = d_nodeManager->booleanType();
 
-    Node w = d_nodeManager->mkVar("w", booleanType);
-    Node x = d_nodeManager->mkVar("x", booleanType);
-    Node y = d_nodeManager->mkVar("y", booleanType);
-    Node z = d_nodeManager->mkVar("z", booleanType);
+    Node w = d_nodeManager->mkSkolem("w", booleanType);
+    Node x = d_nodeManager->mkSkolem("x", booleanType);
+    Node y = d_nodeManager->mkSkolem("y", booleanType);
+    Node z = d_nodeManager->mkSkolem("z", booleanType);
     Node m = NodeBuilder<>() << w << x << kind::OR;
     Node n = NodeBuilder<>() << m << y << z << kind::AND;
 
@@ -538,10 +538,10 @@ public:
   void testToStream() {
     TypeNode booleanType = d_nodeManager->booleanType();
 
-    Node w = d_nodeManager->mkVar("w", booleanType);
-    Node x = d_nodeManager->mkVar("x", booleanType);
-    Node y = d_nodeManager->mkVar("y", booleanType);
-    Node z = d_nodeManager->mkVar("z", booleanType);
+    Node w = d_nodeManager->mkSkolem("w", booleanType);
+    Node x = d_nodeManager->mkSkolem("x", booleanType);
+    Node y = d_nodeManager->mkSkolem("y", booleanType);
+    Node z = d_nodeManager->mkSkolem("z", booleanType);
     Node m = NodeBuilder<>() << x << y << kind::OR;
     Node n = NodeBuilder<>() << w << m << z << kind::AND;
     Node o = NodeBuilder<>() << n << n << kind::XOR;
@@ -600,10 +600,10 @@ public:
     TypeNode intType = d_nodeManager->integerType();
     TypeNode fnType = d_nodeManager->mkFunctionType(intType, intType);
 
-    Node x = d_nodeManager->mkVar("x", intType);
-    Node y = d_nodeManager->mkVar("y", intType);
-    Node f = d_nodeManager->mkVar("f", fnType);
-    Node g = d_nodeManager->mkVar("g", fnType);
+    Node x = d_nodeManager->mkSkolem("x", intType);
+    Node y = d_nodeManager->mkSkolem("y", intType);
+    Node f = d_nodeManager->mkSkolem("f", fnType);
+    Node g = d_nodeManager->mkSkolem("g", fnType);
     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);
@@ -644,7 +644,7 @@ public:
 //  This is for demonstrating what a certain type of user error looks like.
 //   Node level0(){
 //     NodeBuilder<> nb(kind::AND);
-//     Node x = d_nodeManager->mkVar(*d_booleanType);
+//     Node x = d_nodeManager->mkSkolem(*d_booleanType);
 //     nb << x;
 //     nb << x;
 //     return Node(nb.constructNode());

diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h
index c6d6d815e5733840c91e1f4dff592b16e2df5fd2..fc9fdd2a6bd7ebb124b0a32bd79ef59e8fa7f2f2 100644 (file)
--- a/test/unit/expr/node_builder_black.h
+++ b/test/unit/expr/node_builder_black.h
@@ -246,9 +246,9 @@ public:
 
   void testIterator() {
     NodeBuilder<> b;
-    Node x = d_nm->mkVar(*d_booleanType);
-    Node y = d_nm->mkVar(*d_booleanType);
-    Node z = d_nm->mkVar(*d_booleanType);
+    Node x = d_nm->mkSkolem(*d_booleanType);
+    Node y = d_nm->mkSkolem(*d_booleanType);
+    Node z = d_nm->mkSkolem(*d_booleanType);
     b << x << y << z << AND;
 
     {
@@ -274,7 +274,7 @@ public:
     NodeBuilder<> noKind;
     TS_ASSERT_EQUALS(noKind.getKind(), UNDEFINED_KIND);
 
-    Node x( d_nm->mkVar( *d_integerType ) );
+    Node x( d_nm->mkSkolem( *d_integerType ) );
     noKind << x << x;
     //     push_back(noKind, K);
     TS_ASSERT_EQUALS(noKind.getKind(), UNDEFINED_KIND);
@@ -297,7 +297,7 @@ public:
 
   void testGetNumChildren() {
     /* unsigned getNumChildren() const; */
-    Node x( d_nm->mkVar( *d_integerType ) );
+    Node x( d_nm->mkSkolem( *d_integerType ) );
 
     NodeBuilder<> nb;
 #ifdef CVC4_ASSERTIONS
@@ -515,16 +515,16 @@ public:
   }
 
   void testAppend() {
-    Node x = d_nm->mkVar(*d_booleanType);
-    Node y = d_nm->mkVar(*d_booleanType);
-    Node z = d_nm->mkVar(*d_booleanType);
+    Node x = d_nm->mkSkolem(*d_booleanType);
+    Node y = d_nm->mkSkolem(*d_booleanType);
+    Node z = d_nm->mkSkolem(*d_booleanType);
     Node m = d_nm->mkNode(AND, y, z, x);
     Node n = d_nm->mkNode(OR, d_nm->mkNode(NOT, x), y, z);
     Node o = d_nm->mkNode(XOR, y, x);
 
-    Node r = d_nm->mkVar(*d_realType);
-    Node s = d_nm->mkVar(*d_realType);
-    Node t = d_nm->mkVar(*d_realType);
+    Node r = d_nm->mkSkolem(*d_realType);
+    Node s = d_nm->mkSkolem(*d_realType);
+    Node t = d_nm->mkSkolem(*d_realType);
 
     Node p = d_nm->mkNode(EQUAL, d_nm->mkConst<Rational>(0),
                           d_nm->mkNode(PLUS, r, d_nm->mkNode(UMINUS, s), t));
@@ -599,13 +599,13 @@ public:
   void testLeftistBuilding() {
     NodeBuilder<> nb;
 
-    Node a = d_nm->mkVar(*d_booleanType);
+    Node a = d_nm->mkSkolem(*d_booleanType);
 
-    Node b = d_nm->mkVar(*d_booleanType);
-    Node c = d_nm->mkVar(*d_booleanType);
+    Node b = d_nm->mkSkolem(*d_booleanType);
+    Node c = d_nm->mkSkolem(*d_booleanType);
 
-    Node d = d_nm->mkVar(*d_realType);
-    Node e = d_nm->mkVar(*d_realType);
+    Node d = d_nm->mkSkolem(*d_realType);
+    Node e = d_nm->mkSkolem(*d_realType);
 
     nb << a << NOT
        << b << c << OR
@@ -628,14 +628,14 @@ public:
   }
 
   void testConvenienceBuilders() {
-    Node a = d_nm->mkVar(*d_booleanType);
+    Node a = d_nm->mkSkolem(*d_booleanType);
 
-    Node b = d_nm->mkVar(*d_booleanType);
-    Node c = d_nm->mkVar(*d_booleanType);
+    Node b = d_nm->mkSkolem(*d_booleanType);
+    Node c = d_nm->mkSkolem(*d_booleanType);
 
-    Node d = d_nm->mkVar(*d_realType);
-    Node e = d_nm->mkVar(*d_realType);
-    Node f = d_nm->mkVar(*d_realType);
+    Node d = d_nm->mkSkolem(*d_realType);
+    Node e = d_nm->mkSkolem(*d_realType);
+    Node f = d_nm->mkSkolem(*d_realType);
 
     Node m = a && b;
     TS_ASSERT_EQUALS(m, d_nm->mkNode(AND, a, b));

diff --git a/test/unit/expr/node_manager_black.h b/test/unit/expr/node_manager_black.h
index cca2ff4fcfdbab43354ce8846e6502ace26a91c1..d392050f85419e57b6f093c9be50fb591d50e863 100644 (file)
--- a/test/unit/expr/node_manager_black.h
+++ b/test/unit/expr/node_manager_black.h
@@ -53,7 +53,7 @@ public:
   }
 
   void testMkNodeNot() {
-    Node x = d_nodeManager->mkVar("x",d_nodeManager->booleanType());
+    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);
@@ -61,8 +61,8 @@ public:
   }
 
   void testMkNodeBinary() {
-    Node x = d_nodeManager->mkVar("x",d_nodeManager->booleanType());
-    Node y = d_nodeManager->mkVar("y",d_nodeManager->booleanType());
+    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);
@@ -71,9 +71,9 @@ public:
   }
 
   void testMkNodeThreeChildren() {
-    Node x = d_nodeManager->mkVar("x",d_nodeManager->booleanType());
-    Node y = d_nodeManager->mkVar("y",d_nodeManager->booleanType());
-    Node z = d_nodeManager->mkVar("z",d_nodeManager->booleanType());
+    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);
@@ -83,10 +83,10 @@ public:
   }
 
   void testMkNodeFourChildren() {
-    Node x1 = d_nodeManager->mkVar("x1",d_nodeManager->booleanType());
-    Node x2 = d_nodeManager->mkVar("x2",d_nodeManager->booleanType());
-    Node x3 = d_nodeManager->mkVar("x3",d_nodeManager->booleanType());
-    Node x4 = d_nodeManager->mkVar("x4",d_nodeManager->booleanType());
+    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 );
@@ -97,11 +97,11 @@ public:
   }
 
   void testMkNodeFiveChildren() {
-    Node x1 = d_nodeManager->mkVar("x1",d_nodeManager->booleanType());
-    Node x2 = d_nodeManager->mkVar("x2",d_nodeManager->booleanType());
-    Node x3 = d_nodeManager->mkVar("x3",d_nodeManager->booleanType());
-    Node x4 = d_nodeManager->mkVar("x4",d_nodeManager->booleanType());
-    Node x5 = d_nodeManager->mkVar("x5",d_nodeManager->booleanType());
+    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);
@@ -113,9 +113,9 @@ public:
   }
 
   void testMkNodeVectorOfNodeChildren() {
-    Node x1 = d_nodeManager->mkVar("x1",d_nodeManager->booleanType());
-    Node x2 = d_nodeManager->mkVar("x2",d_nodeManager->booleanType());
-    Node x3 = d_nodeManager->mkVar("x3",d_nodeManager->booleanType());
+    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);
@@ -129,9 +129,9 @@ public:
   }
 
   void testMkNodeVectorOfTNodeChildren() {
-    Node x1 = d_nodeManager->mkVar("x1",d_nodeManager->booleanType());
-    Node x2 = d_nodeManager->mkVar("x2",d_nodeManager->booleanType());
-    Node x3 = d_nodeManager->mkVar("x3",d_nodeManager->booleanType());
+    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);
@@ -146,16 +146,16 @@ public:
 
   void testMkVarWithNoName() {
     TypeNode booleanType = d_nodeManager->booleanType();
-    Node x = d_nodeManager->mkVar(booleanType);
-    TS_ASSERT_EQUALS(x.getKind(),VARIABLE);
+    Node x = d_nodeManager->mkSkolem(booleanType);
+    TS_ASSERT_EQUALS(x.getKind(),SKOLEM);
     TS_ASSERT_EQUALS(x.getNumChildren(),0u);
     TS_ASSERT_EQUALS(x.getType(),booleanType);
   }
 
   void testMkVarWithName() {
     TypeNode booleanType = d_nodeManager->booleanType();
-    Node x = d_nodeManager->mkVar("x", booleanType);
-    TS_ASSERT_EQUALS(x.getKind(),VARIABLE);
+    Node x = d_nodeManager->mkSkolem("x", booleanType);
+    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);
@@ -337,7 +337,7 @@ public:
   /* This test is only valid if assertions are enabled. */
   void testMkNodeTooFew() {
 #ifdef CVC4_ASSERTIONS
-    Node x = d_nodeManager->mkVar( d_nodeManager->booleanType() );
+    Node x = d_nodeManager->mkSkolem( d_nodeManager->booleanType() );
     TS_ASSERT_THROWS( d_nodeManager->mkNode(AND, x), AssertionException );
 #endif
   }
@@ -349,7 +349,7 @@ public:
     const unsigned int max = metakind::getUpperBoundForKind(AND);
     TypeNode boolType = d_nodeManager->booleanType();
     for( unsigned int i = 0; i <= max; ++i ) {
-      vars.push_back( d_nodeManager->mkVar(boolType) );
+      vars.push_back( d_nodeManager->mkSkolem(boolType) );
     }
     TS_ASSERT_THROWS( d_nodeManager->mkNode(AND, vars), AssertionException );
 #endif

diff --git a/test/unit/expr/node_self_iterator_black.h b/test/unit/expr/node_self_iterator_black.h
index 9cc09f88454b875192f254798c6ad5158ccc3c59..97bff659cdc211fa38d7cb193a64b6da21bec2f7 100644 (file)
--- a/test/unit/expr/node_self_iterator_black.h
+++ b/test/unit/expr/node_self_iterator_black.h
@@ -57,8 +57,8 @@ public:
   }
 
   void testSelfIteration() {
-    Node x = d_nodeManager->mkVar("x", *d_booleanType);
-    Node y = d_nodeManager->mkVar("y", *d_booleanType);
+    Node x = d_nodeManager->mkSkolem("x", *d_booleanType);
+    Node y = d_nodeManager->mkSkolem("y", *d_booleanType);
     Node x_and_y = x && y;
     NodeSelfIterator i = x_and_y, j = NodeSelfIterator::self(x_and_y);
     TS_ASSERT(i != x_and_y.end());

diff --git a/test/unit/util/boolean_simplification_black.h b/test/unit/util/boolean_simplification_black.h
index 8dafd202e28d02c9ddde3ad80c5328115725bb0f..8f2d0d97fa893d256642d4a0348f97ea954d3ce4 100644 (file)
--- a/test/unit/util/boolean_simplification_black.h
+++ b/test/unit/util/boolean_simplification_black.h
@@ -76,17 +76,17 @@ public:
     d_nm = new NodeManager(d_context, NULL);
     d_scope = new NodeManagerScope(d_nm);
 
-    a = d_nm->mkVar("a", d_nm->booleanType());
-    b = d_nm->mkVar("b", d_nm->booleanType());
-    c = d_nm->mkVar("c", d_nm->booleanType());
-    d = d_nm->mkVar("d", d_nm->booleanType());
-    e = d_nm->mkVar("e", d_nm->booleanType());
-    f = d_nm->mkVar("f", d_nm->mkFunctionType(d_nm->booleanType(),
-                                              d_nm->booleanType()));
-    g = d_nm->mkVar("g", d_nm->mkFunctionType(d_nm->booleanType(),
-                                              d_nm->booleanType()));
-    h = d_nm->mkVar("h", d_nm->mkFunctionType(d_nm->booleanType(),
-                                              d_nm->booleanType()));
+    a = d_nm->mkSkolem("a", d_nm->booleanType());
+    b = d_nm->mkSkolem("b", d_nm->booleanType());
+    c = d_nm->mkSkolem("c", d_nm->booleanType());
+    d = d_nm->mkSkolem("d", d_nm->booleanType());
+    e = d_nm->mkSkolem("e", d_nm->booleanType());
+    f = d_nm->mkSkolem("f", d_nm->mkFunctionType(d_nm->booleanType(),
+                                                 d_nm->booleanType()));
+    g = d_nm->mkSkolem("g", d_nm->mkFunctionType(d_nm->booleanType(),
+                                                 d_nm->booleanType()));
+    h = d_nm->mkSkolem("h", d_nm->mkFunctionType(d_nm->booleanType(),
+                                                 d_nm->booleanType()));
     fa = d_nm->mkNode(kind::APPLY_UF, f, a);
     fb = d_nm->mkNode(kind::APPLY_UF, f, b);
     fc = d_nm->mkNode(kind::APPLY_UF, f, c);