summaryrefslogtreecommitdiff
path: root/test
diff options
context:
space:
mode:
Diffstat (limited to 'test')
-rw-r--r--test/unit/expr/attribute_black.h16
-rw-r--r--test/unit/expr/node_black.h62
-rw-r--r--test/unit/expr/node_builder_black.h44
-rw-r--r--test/unit/expr/node_manager_black.h14
4 files changed, 64 insertions, 72 deletions
diff --git a/test/unit/expr/attribute_black.h b/test/unit/expr/attribute_black.h
index 93fbe049a..02de21635 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->mkSkolem(booleanType));
+ Node* node = new Node(d_nodeManager->mkSkolem("b", 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->mkSkolem(booleanType));
+ Node* node = new Node(d_nodeManager->mkSkolem("b", 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->mkSkolem(booleanType));
+ Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType));
- Node val(d_nodeManager->mkSkolem(booleanType));
+ Node val(d_nodeManager->mkSkolem("b", 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->mkSkolem(booleanType));
+ Node* node = new Node(d_nodeManager->mkSkolem("b", 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->mkSkolem(booleanType));
+ Node* node = new Node(d_nodeManager->mkSkolem("b", 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->mkSkolem(booleanType));
+ Node* node = new Node(d_nodeManager->mkSkolem("b", 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->mkSkolem(booleanType));
+ Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType));
bool val = true;
bool data0 = false;
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());
diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h
index fc9fdd2a6..97abddc00 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->mkSkolem(*d_booleanType);
- Node y = d_nm->mkSkolem(*d_booleanType);
- Node z = d_nm->mkSkolem(*d_booleanType);
+ Node x = d_nm->mkSkolem("x", *d_booleanType);
+ Node y = d_nm->mkSkolem("z", *d_booleanType);
+ Node z = d_nm->mkSkolem("y", *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->mkSkolem( *d_integerType ) );
+ Node x( d_nm->mkSkolem( "x", *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->mkSkolem( *d_integerType ) );
+ Node x( d_nm->mkSkolem( "x", *d_integerType ) );
NodeBuilder<> nb;
#ifdef CVC4_ASSERTIONS
@@ -515,16 +515,16 @@ public:
}
void testAppend() {
- Node x = d_nm->mkSkolem(*d_booleanType);
- Node y = d_nm->mkSkolem(*d_booleanType);
- Node z = d_nm->mkSkolem(*d_booleanType);
+ Node x = d_nm->mkSkolem("x", *d_booleanType);
+ Node y = d_nm->mkSkolem("y", *d_booleanType);
+ Node z = d_nm->mkSkolem("z", *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->mkSkolem(*d_realType);
- Node s = d_nm->mkSkolem(*d_realType);
- Node t = d_nm->mkSkolem(*d_realType);
+ Node r = d_nm->mkSkolem("r", *d_realType);
+ Node s = d_nm->mkSkolem("s", *d_realType);
+ Node t = d_nm->mkSkolem("t", *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->mkSkolem(*d_booleanType);
+ Node a = d_nm->mkSkolem("a", *d_booleanType);
- Node b = d_nm->mkSkolem(*d_booleanType);
- Node c = d_nm->mkSkolem(*d_booleanType);
+ Node b = d_nm->mkSkolem("b", *d_booleanType);
+ Node c = d_nm->mkSkolem("c", *d_booleanType);
- Node d = d_nm->mkSkolem(*d_realType);
- Node e = d_nm->mkSkolem(*d_realType);
+ Node d = d_nm->mkSkolem("d", *d_realType);
+ Node e = d_nm->mkSkolem("e", *d_realType);
nb << a << NOT
<< b << c << OR
@@ -628,14 +628,14 @@ public:
}
void testConvenienceBuilders() {
- Node a = d_nm->mkSkolem(*d_booleanType);
+ Node a = d_nm->mkSkolem("a", *d_booleanType);
- Node b = d_nm->mkSkolem(*d_booleanType);
- Node c = d_nm->mkSkolem(*d_booleanType);
+ Node b = d_nm->mkSkolem("b", *d_booleanType);
+ Node c = d_nm->mkSkolem("c", *d_booleanType);
- Node d = d_nm->mkSkolem(*d_realType);
- Node e = d_nm->mkSkolem(*d_realType);
- Node f = d_nm->mkSkolem(*d_realType);
+ Node d = d_nm->mkSkolem("d", *d_realType);
+ Node e = d_nm->mkSkolem("e", *d_realType);
+ Node f = d_nm->mkSkolem("f", *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 d392050f8..75c3618ff 100644
--- a/test/unit/expr/node_manager_black.h
+++ b/test/unit/expr/node_manager_black.h
@@ -144,17 +144,9 @@ public:
}
}
- void testMkVarWithNoName() {
- TypeNode booleanType = d_nodeManager->booleanType();
- 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->mkSkolem("x", 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");
@@ -337,7 +329,7 @@ public:
/* This test is only valid if assertions are enabled. */
void testMkNodeTooFew() {
#ifdef CVC4_ASSERTIONS
- Node x = d_nodeManager->mkSkolem( d_nodeManager->booleanType() );
+ Node x = d_nodeManager->mkSkolem( "x", d_nodeManager->booleanType() );
TS_ASSERT_THROWS( d_nodeManager->mkNode(AND, x), AssertionException );
#endif
}
@@ -349,7 +341,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->mkSkolem(boolType) );
+ vars.push_back( d_nodeManager->mkSkolem("i", boolType) );
}
TS_ASSERT_THROWS( d_nodeManager->mkNode(AND, vars), AssertionException );
#endif
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback