summaryrefslogtreecommitdiff
path: root/test/unit/expr
diff options
context:
space:
mode:
Diffstat (limited to 'test/unit/expr')
-rw-r--r--test/unit/expr/attribute_white.h4
-rw-r--r--test/unit/expr/node_black.h6
-rw-r--r--test/unit/expr/node_builder_black.h68
-rw-r--r--test/unit/expr/node_manager_black.h30
-rw-r--r--test/unit/expr/node_white.h2
5 files changed, 53 insertions, 57 deletions
diff --git a/test/unit/expr/attribute_white.h b/test/unit/expr/attribute_white.h
index e0d9d6bf4..e3b7811a4 100644
--- a/test/unit/expr/attribute_white.h
+++ b/test/unit/expr/attribute_white.h
@@ -149,8 +149,6 @@ public:
}
void testCDAttributes() {
- AttributeManager& am = d_nm->d_attrManager;
-
//Debug.on("boolattr");
Node a = d_nm->mkVar(d_booleanType);
@@ -279,8 +277,6 @@ public:
}
void testAttributes() {
- AttributeManager& am = d_nm->d_attrManager;
-
//Debug.on("boolattr");
Node a = d_nm->mkVar(d_booleanType);
diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h
index 17657683d..23d1daf4e 100644
--- a/test/unit/expr/node_black.h
+++ b/test/unit/expr/node_black.h
@@ -423,10 +423,10 @@ public:
#endif /* CVC4_ASSERTIONS */
}
- void testNaryExpForSize(Kind k, int N) {
+ void testNaryExpForSize(Kind k, unsigned N) {
NodeBuilder<> nbz(k);
Node trueNode = d_nodeManager->mkConst(true);
- for(int i = 0; i < N; ++i) {
+ for(unsigned i = 0; i < N; ++i) {
nbz << trueNode;
}
Node result = nbz;
@@ -452,7 +452,7 @@ public:
srand(0);
int trials = 500;
for(int i = 0; i < trials; ++i) {
- int N = rand() % 1000 + 2;
+ unsigned N = rand() % 1000 + 2;
testNaryExpForSize(AND, N);
}
diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h
index eec6949f0..4521f3bf6 100644
--- a/test/unit/expr/node_builder_black.h
+++ b/test/unit/expr/node_builder_black.h
@@ -64,8 +64,8 @@ public:
}
}
-#define K 30
-#define LARGE_K UINT_MAX/40
+#define K 30u
+#define LARGE_K UINT_MAX / 40
Kind specKind;
@@ -84,23 +84,23 @@ public:
/* default size tests */
NodeBuilder<> def;
TS_ASSERT_EQUALS(def.getKind(), UNDEFINED_KIND);
- TS_ASSERT_EQUALS(def.getNumChildren(), 0);
+ TS_ASSERT_EQUALS(def.getNumChildren(), 0u);
TS_ASSERT_EQUALS(def.begin(), def.end());
NodeBuilder<> spec(specKind);
TS_ASSERT_EQUALS(spec.getKind(), specKind);
- TS_ASSERT_EQUALS(spec.getNumChildren(), 0);
+ TS_ASSERT_EQUALS(spec.getNumChildren(), 0u);
TS_ASSERT_EQUALS(spec.begin(), spec.end());
NodeBuilder<> from_nm(d_nm);
TS_ASSERT_EQUALS(from_nm.getKind(), UNDEFINED_KIND);
- TS_ASSERT_EQUALS(from_nm.getNumChildren(), 0);
+ TS_ASSERT_EQUALS(from_nm.getNumChildren(), 0u);
TS_ASSERT_EQUALS(from_nm.begin(), from_nm.end());
NodeBuilder<> from_nm_kind(d_nm, specKind);
TS_ASSERT_EQUALS(from_nm_kind.getKind(), specKind);
- TS_ASSERT_EQUALS(from_nm_kind.getNumChildren(), 0);
+ TS_ASSERT_EQUALS(from_nm_kind.getNumChildren(), 0u);
TS_ASSERT_EQUALS(from_nm_kind.begin(), from_nm_kind.end());
@@ -108,23 +108,23 @@ public:
NodeBuilder<K> ws;
TS_ASSERT_EQUALS(ws.getKind(), UNDEFINED_KIND);
- TS_ASSERT_EQUALS(ws.getNumChildren(), 0);
+ TS_ASSERT_EQUALS(ws.getNumChildren(), 0u);
TS_ASSERT_EQUALS(ws.begin(), ws.end());
NodeBuilder<K> ws_kind(specKind);
TS_ASSERT_EQUALS(ws_kind.getKind(), specKind);
- TS_ASSERT_EQUALS(ws_kind.getNumChildren(), 0);
+ TS_ASSERT_EQUALS(ws_kind.getNumChildren(), 0u);
TS_ASSERT_EQUALS(ws_kind.begin(), ws_kind.end());
NodeBuilder<K> ws_from_nm(d_nm);
TS_ASSERT_EQUALS(ws_from_nm.getKind(), UNDEFINED_KIND);
- TS_ASSERT_EQUALS(ws_from_nm.getNumChildren(), 0);
+ TS_ASSERT_EQUALS(ws_from_nm.getNumChildren(), 0u);
TS_ASSERT_EQUALS(ws_from_nm.begin(), ws_from_nm.end());
NodeBuilder<K> ws_from_nm_kind(d_nm, specKind);
TS_ASSERT_EQUALS(ws_from_nm_kind.getKind(), specKind);
- TS_ASSERT_EQUALS(ws_from_nm_kind.getNumChildren(), 0);
+ TS_ASSERT_EQUALS(ws_from_nm_kind.getNumChildren(), 0u);
TS_ASSERT_EQUALS(ws_from_nm_kind.begin(), ws_from_nm_kind.end());
@@ -137,23 +137,23 @@ public:
NodeBuilder<> copy(def);
TS_ASSERT_EQUALS(copy.getKind(), UNDEFINED_KIND);
- TS_ASSERT_EQUALS(copy.getNumChildren(), 0);
+ TS_ASSERT_EQUALS(copy.getNumChildren(), 0u);
TS_ASSERT_EQUALS(copy.begin(), copy.end());
NodeBuilder<K> cp_ws(ws);
TS_ASSERT_EQUALS(cp_ws.getKind(), UNDEFINED_KIND);
- TS_ASSERT_EQUALS(cp_ws.getNumChildren(), 0);
+ TS_ASSERT_EQUALS(cp_ws.getNumChildren(), 0u);
TS_ASSERT_EQUALS(cp_ws.begin(), cp_ws.end());
NodeBuilder<K-10> cp_from_larger(ws);
TS_ASSERT_EQUALS(cp_from_larger.getKind(), UNDEFINED_KIND);
- TS_ASSERT_EQUALS(cp_from_larger.getNumChildren(), 0);
+ TS_ASSERT_EQUALS(cp_from_larger.getNumChildren(), 0u);
TS_ASSERT_EQUALS(cp_from_larger.begin(), cp_from_larger.end());
NodeBuilder<K+10> cp_from_smaller(ws);
TS_ASSERT_EQUALS(cp_from_smaller.getKind(), UNDEFINED_KIND);
- TS_ASSERT_EQUALS(cp_from_smaller.getNumChildren(), 0);
+ TS_ASSERT_EQUALS(cp_from_smaller.getNumChildren(), 0u);
TS_ASSERT_EQUALS(cp_from_smaller.begin(), cp_from_smaller.end());
}
@@ -174,14 +174,14 @@ public:
TS_ASSERT_DIFFERS(ws.begin(), ws.end());
NodeBuilder<K>::iterator iter = ws.begin();
- for(int i = 0; i < K; ++i){
+ for(unsigned i = 0; i < K; ++i){
TS_ASSERT_DIFFERS(iter, ws.end());
++iter;
}
TS_ASSERT_EQUALS(iter, ws.end());
NodeBuilder<K>::const_iterator citer = ws.begin();
- for(int i = 0; i < K; ++i){
+ for(unsigned i = 0; i < K; ++i){
TS_ASSERT_DIFFERS(citer, ws.end());
++citer;
}
@@ -196,14 +196,14 @@ public:
TS_ASSERT_DIFFERS(smaller.begin(), smaller.end());
NodeBuilder<>::iterator smaller_iter = smaller.begin();
- for(int i = 0; i < K; ++i){
+ for(unsigned i = 0; i < K; ++i){
TS_ASSERT_DIFFERS(smaller_iter, smaller.end());
++smaller_iter;
}
TS_ASSERT_EQUALS(iter, ws.end());
NodeBuilder<>::const_iterator smaller_citer = smaller.begin();
- for(int i = 0; i < K; ++i){
+ for(unsigned i = 0; i < K; ++i){
TS_ASSERT_DIFFERS(smaller_citer, smaller.end());
++smaller_citer;
}
@@ -261,24 +261,24 @@ public:
/* unsigned getNumChildren() const; */
NodeBuilder<> noKind;
- TS_ASSERT_EQUALS(noKind.getNumChildren(), 0);
+ TS_ASSERT_EQUALS(noKind.getNumChildren(), 0u);
push_back(noKind, K);
TS_ASSERT_EQUALS(noKind.getNumChildren(), K);
push_back(noKind, K);
- TS_ASSERT_EQUALS(noKind.getNumChildren(), K+K);
+ TS_ASSERT_EQUALS(noKind.getNumChildren(), K + K);
noKind << AND;// avoid exception on marking it used
Node n = noKind;// avoid warning on clear()
noKind.clear();
- TS_ASSERT_EQUALS(noKind.getNumChildren(), 0);
+ TS_ASSERT_EQUALS(noKind.getNumChildren(), 0u);
push_back(noKind, K);
TS_ASSERT_EQUALS(noKind.getNumChildren(), K);
push_back(noKind, K);
- TS_ASSERT_EQUALS(noKind.getNumChildren(), K+K);
+ TS_ASSERT_EQUALS(noKind.getNumChildren(), K + K);
#ifdef CVC4_ASSERTIONS
noKind << specKind;
@@ -320,7 +320,7 @@ public:
TS_ASSERT_EQUALS(arr[0], i_0);
TS_ASSERT_EQUALS(arr[2], i_2);
- for(int i = 3; i < K; ++i) {
+ for(unsigned i = 3; i < K; ++i) {
TS_ASSERT_EQUALS(arr[i], d_nm->mkConst(true));
}
@@ -328,7 +328,7 @@ public:
TS_ASSERT_EQUALS(arr[0], i_0);
TS_ASSERT_EQUALS(arr[2], i_2);
- for(int i = 3; i < K; ++i) {
+ for(unsigned i = 3; i < K; ++i) {
TS_ASSERT_EQUALS(arr[i], d_nm->mkConst(true));
}
TS_ASSERT_EQUALS(arr[K], i_K);
@@ -344,7 +344,7 @@ public:
NodeBuilder<> nb;
TS_ASSERT_EQUALS(nb.getKind(), UNDEFINED_KIND);
- TS_ASSERT_EQUALS(nb.getNumChildren(), 0);
+ TS_ASSERT_EQUALS(nb.getNumChildren(), 0u);
TS_ASSERT_EQUALS(nb.begin(), nb.end());
nb << specKind;
@@ -358,7 +358,7 @@ public:
nb.clear();
TS_ASSERT_EQUALS(nb.getKind(), UNDEFINED_KIND);
- TS_ASSERT_EQUALS(nb.getNumChildren(), 0);
+ TS_ASSERT_EQUALS(nb.getNumChildren(), 0u);
TS_ASSERT_EQUALS(nb.begin(), nb.end());
nb << specKind;
@@ -372,7 +372,7 @@ public:
nb.clear(specKind);
TS_ASSERT_EQUALS(nb.getKind(), specKind);
- TS_ASSERT_EQUALS(nb.getNumChildren(), 0);
+ TS_ASSERT_EQUALS(nb.getNumChildren(), 0u);
TS_ASSERT_EQUALS(nb.begin(), nb.end());
push_back(nb, K);
@@ -380,7 +380,7 @@ public:
nb.clear();
TS_ASSERT_EQUALS(nb.getKind(), UNDEFINED_KIND);
- TS_ASSERT_EQUALS(nb.getNumChildren(), 0);
+ TS_ASSERT_EQUALS(nb.getNumChildren(), 0u);
TS_ASSERT_EQUALS(nb.begin(), nb.end());
}
@@ -437,7 +437,7 @@ public:
/* NodeBuilder& operator<<(const Node& n); */
NodeBuilder<K> nb(specKind);
TS_ASSERT_EQUALS(nb.getKind(), specKind);
- TS_ASSERT_EQUALS(nb.getNumChildren(), 0);
+ TS_ASSERT_EQUALS(nb.getNumChildren(), 0u);
TS_ASSERT_EQUALS(nb.begin(), nb.end());
push_back(nb,K);
TS_ASSERT_EQUALS(nb.getKind(), specKind);
@@ -451,13 +451,13 @@ public:
NodeBuilder<> overflow(specKind);
TS_ASSERT_EQUALS(overflow.getKind(), specKind);
- TS_ASSERT_EQUALS(overflow.getNumChildren(), 0);
+ TS_ASSERT_EQUALS(overflow.getNumChildren(), 0u);
TS_ASSERT_EQUALS(overflow.begin(), overflow.end());
push_back(overflow,5*K+1);
TS_ASSERT_EQUALS(overflow.getKind(), specKind);
- TS_ASSERT_EQUALS(overflow.getNumChildren(), 5*K+1);
+ TS_ASSERT_EQUALS(overflow.getNumChildren(), 5 * K + 1);
TS_ASSERT_DIFFERS(overflow.begin(), overflow.end());
}
@@ -598,16 +598,16 @@ public:
Node f = d_nm->mkVar(d_booleanType);
Node m = a && b;
- Node n = a && b || c;
+ Node n = (a && b) || c;
Node o = d + e - b;
- Node p = a && o || c;
+ Node p = (a && o) || c;
Node x = d + e + o - m;
Node y = f - a - c + e;
Node q = a && b && c;
- Node r = e && d && b && a || x && y || f || q && a;
+ Node r = (e && d && b && a) || (x && y) || f || (q && a);
TS_ASSERT_EQUALS(m, d_nm->mkNode(AND, a, b));
TS_ASSERT_EQUALS(n, d_nm->mkNode(OR, m, c));
diff --git a/test/unit/expr/node_manager_black.h b/test/unit/expr/node_manager_black.h
index 3e65be0b7..e059fa509 100644
--- a/test/unit/expr/node_manager_black.h
+++ b/test/unit/expr/node_manager_black.h
@@ -52,7 +52,7 @@ public:
void testMkNode1() {
Node x = d_nodeManager->mkVar("x",d_nodeManager->booleanType());
Node n = d_nodeManager->mkNode(NOT, x);
- TS_ASSERT_EQUALS( n.getNumChildren(), 1 );
+ TS_ASSERT_EQUALS( n.getNumChildren(), 1u );
TS_ASSERT_EQUALS( n.getKind(), NOT);
TS_ASSERT_EQUALS( n[0], x);
}
@@ -61,7 +61,7 @@ public:
Node x = d_nodeManager->mkVar("x",d_nodeManager->booleanType());
Node y = d_nodeManager->mkVar("y",d_nodeManager->booleanType());
Node n = d_nodeManager->mkNode(IMPLIES, x, y);
- TS_ASSERT_EQUALS( n.getNumChildren(), 2 );
+ TS_ASSERT_EQUALS( n.getNumChildren(), 2u );
TS_ASSERT_EQUALS( n.getKind(), IMPLIES);
TS_ASSERT_EQUALS( n[0], x);
TS_ASSERT_EQUALS( n[1], y);
@@ -72,7 +72,7 @@ public:
Node y = d_nodeManager->mkVar("y",d_nodeManager->booleanType());
Node z = d_nodeManager->mkVar("z",d_nodeManager->booleanType());
Node n = d_nodeManager->mkNode(AND, x, y, z);
- TS_ASSERT_EQUALS( n.getNumChildren(), 3 );
+ TS_ASSERT_EQUALS( n.getNumChildren(), 3u );
TS_ASSERT_EQUALS( n.getKind(), AND);
TS_ASSERT_EQUALS( n[0], x);
TS_ASSERT_EQUALS( n[1], y);
@@ -85,12 +85,12 @@ public:
Node x3 = d_nodeManager->mkVar("x3",d_nodeManager->booleanType());
Node x4 = d_nodeManager->mkVar("x4",d_nodeManager->booleanType());
Node n = d_nodeManager->mkNode(AND, x1, x2, x3, x4);
- TS_ASSERT_EQUALS( n.getNumChildren(), 4 );
- 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.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 testMkNode5() {
@@ -100,7 +100,7 @@ public:
Node x4 = d_nodeManager->mkVar("x4",d_nodeManager->booleanType());
Node x5 = d_nodeManager->mkVar("x5",d_nodeManager->booleanType());
Node n = d_nodeManager->mkNode(AND, x1, x2, x3, x4, x5);
- TS_ASSERT_EQUALS( n.getNumChildren(), 5 );
+ TS_ASSERT_EQUALS( n.getNumChildren(), 5u );
TS_ASSERT_EQUALS( n.getKind(), AND);
TS_ASSERT_EQUALS( n[0], x1);
TS_ASSERT_EQUALS( n[1], x2);
@@ -120,7 +120,7 @@ public:
Node n = d_nodeManager->mkNode(AND, args);
TS_ASSERT_EQUALS( n.getNumChildren(), args.size() );
TS_ASSERT_EQUALS( n.getKind(), AND);
- for( int i=0; i < args.size(); ++i ) {
+ for( unsigned i = 0; i < args.size(); ++i ) {
TS_ASSERT_EQUALS( n[i], args[i]);
}
}
@@ -136,7 +136,7 @@ public:
Node n = d_nodeManager->mkNode(AND, args);
TS_ASSERT_EQUALS( n.getNumChildren(), args.size() );
TS_ASSERT_EQUALS( n.getKind(), AND);
- for( int i=0; i < args.size(); ++i ) {
+ for( unsigned i = 0; i < args.size(); ++i ) {
TS_ASSERT_EQUALS( n[i], args[i]);
}
}
@@ -145,7 +145,7 @@ public:
Type* booleanType = d_nodeManager->booleanType();
Node x = d_nodeManager->mkVar(booleanType);
TS_ASSERT_EQUALS(x.getKind(),VARIABLE);
- TS_ASSERT_EQUALS(x.getNumChildren(),0);
+ TS_ASSERT_EQUALS(x.getNumChildren(),0u);
TS_ASSERT_EQUALS(x.getType(),booleanType);
}
@@ -153,7 +153,7 @@ public:
Type* booleanType = d_nodeManager->booleanType();
Node x = d_nodeManager->mkVar("x", booleanType);
TS_ASSERT_EQUALS(x.getKind(),VARIABLE);
- TS_ASSERT_EQUALS(x.getNumChildren(),0);
+ TS_ASSERT_EQUALS(x.getNumChildren(),0u);
TS_ASSERT_EQUALS(x.getAttribute(VarNameAttr()),"x");
TS_ASSERT_EQUALS(x.getType(),booleanType);
}
@@ -219,7 +219,7 @@ public:
TS_ASSERT( t->isFunction() );
FunctionType* ft = (FunctionType*)t;
- TS_ASSERT_EQUALS(ft->getArgTypes().size(), 1);
+ TS_ASSERT_EQUALS(ft->getArgTypes().size(), 1u);
TS_ASSERT_EQUALS(ft->getArgTypes()[0], booleanType);
TS_ASSERT_EQUALS(ft->getRangeType(), booleanType);
diff --git a/test/unit/expr/node_white.h b/test/unit/expr/node_white.h
index 28dbde933..9facd00f6 100644
--- a/test/unit/expr/node_white.h
+++ b/test/unit/expr/node_white.h
@@ -51,7 +51,7 @@ public:
}
void testNull() {
- Node::s_null;
+ TS_ASSERT_EQUALS(Node::null(), Node::s_null);
}
void testCopyCtor() {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback