From: Morgan Deters Date: Sat, 25 Aug 2012 21:27:17 +0000 (+0000) Subject: fix unit tests X-Git-Tag: cvc5-1.0.0~7845 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3cbd118238dbe1a68c53a970169488bee2b63ae7;p=cvc5.git fix unit tests --- diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp index 48f773c54..50bd5016d 100644 --- 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 f0feb1293..fd7d3cc42 100644 --- 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(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 5f410881b..3dd59dc91 100644 --- 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(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 8e7f89795..93fbe049a 100644 --- 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 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 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 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 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 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 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 f617ebd5b..53af9db53 100644 --- 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(amkSort(); - 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 c6d6d815e..fc9fdd2a6 100644 --- 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(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 cca2ff4fc..d392050f8 100644 --- 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 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 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 9cc09f884..97bff659c 100644 --- 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 8dafd202e..8f2d0d97f 100644 --- 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);