summaryrefslogtreecommitdiff
path: root/test/unit/expr/node_black.h
diff options
context:
space:
mode:
Diffstat (limited to 'test/unit/expr/node_black.h')
-rw-r--r--test/unit/expr/node_black.h62
1 files changed, 31 insertions, 31 deletions
diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h
index 53af9db53..1518efadf 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->mkSkolem(*d_booleanType);
+ b = d_nodeManager->mkSkolem("b", *d_booleanType);
a = b;
c = a;
- Node d = d_nodeManager->mkSkolem(*d_booleanType);
+ Node d = d_nodeManager->mkSkolem("d", *d_booleanType);
TS_ASSERT(a==a);
TS_ASSERT(a==b);
@@ -142,12 +142,12 @@ public:
Node a, b, c;
- b = d_nodeManager->mkSkolem(*d_booleanType);
+ b = d_nodeManager->mkSkolem("b", *d_booleanType);
a = b;
c = a;
- Node d = d_nodeManager->mkSkolem(*d_booleanType);
+ Node d = d_nodeManager->mkSkolem("d", *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->mkSkolem(*d_booleanType));
+ Node c = d_nodeManager->mkNode(NOT, d_nodeManager->mkSkolem("c", *d_booleanType));
b = c;
TS_ASSERT(b==c);
@@ -268,8 +268,8 @@ public:
/* Node eqNode(const Node& right) const; */
TypeNode t = d_nodeManager->mkSort();
- Node left = d_nodeManager->mkSkolem(t);
- Node right = d_nodeManager->mkSkolem(t);
+ Node left = d_nodeManager->mkSkolem("left", t);
+ Node right = d_nodeManager->mkSkolem("right", 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->mkSkolem(*d_booleanType);
- Node b = d_nodeManager->mkSkolem(*d_booleanType);
+ Node a = d_nodeManager->mkSkolem("a", *d_booleanType);
+ Node b = d_nodeManager->mkSkolem("b", *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->mkSkolem(*d_booleanType);
- Node b = d_nodeManager->mkSkolem(*d_booleanType);
+ Node a = d_nodeManager->mkSkolem("a", *d_booleanType);
+ Node b = d_nodeManager->mkSkolem("b", *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->mkSkolem(*d_realType);
- Node y = d_nodeManager->mkSkolem(*d_realType);
+ Node x = d_nodeManager->mkSkolem("x", *d_realType);
+ Node y = d_nodeManager->mkSkolem("y", *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->mkSkolem(predType);
- Node a = d_nodeManager->mkSkolem(sort);
+ 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() );
@@ -476,9 +476,9 @@ public:
// test iterators
void testIterator() {
NodeBuilder<> b;
- Node x = d_nodeManager->mkSkolem(*d_booleanType);
- Node y = d_nodeManager->mkSkolem(*d_booleanType);
- Node z = d_nodeManager->mkSkolem(*d_booleanType);
+ Node x = d_nodeManager->mkSkolem("x", *d_booleanType);
+ Node y = d_nodeManager->mkSkolem("y", *d_booleanType);
+ Node z = d_nodeManager->mkSkolem("z", *d_booleanType);
Node n = b << x << y << z << kind::AND;
{ // iterator
@@ -525,10 +525,10 @@ public:
void testToString() {
TypeNode booleanType = d_nodeManager->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 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;
@@ -538,10 +538,10 @@ public:
void testToStream() {
TypeNode booleanType = d_nodeManager->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 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;
@@ -600,10 +600,10 @@ public:
TypeNode intType = d_nodeManager->integerType();
TypeNode fnType = d_nodeManager->mkFunctionType(intType, intType);
- 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 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);
@@ -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->mkSkolem(*d_booleanType);
+// Node x = d_nodeManager->mkSkolem("x", *d_booleanType);
// nb << x;
// nb << x;
// return Node(nb.constructNode());
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback