diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-03-02 20:33:26 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-03-02 20:33:26 +0000 |
commit | 2b87789ee57a738cccd89dd9d2d81b065875dc29 (patch) | |
tree | f5376c532490088e5dcc7a37ed318127a0dc8c40 /test/unit/expr/node_builder_black.h | |
parent | 7f5036bb37e13dbc7e176d4fa82ee0736d11e913 (diff) |
* NodeBuilder work: specifically, convenience builders. "a && b && c || d && e"
(etc.) now work for Nodes a, b, c, d, e. Also refcounting fixes for
NodeBuilder in certain cases
* (various places) don't overload __gnu_cxx::hash<>, instead provide
an explicit hash function to hash_maps and hash_sets.
* add a new kind of assert, DtorAssert(), which doesn't throw
exceptions (right now it operates like a usual C assert()). For use
in destructors.
* don't import NodeValue into CVC4 namespace (leave under CVC4::expr::).
* fix some Make rule dependencies
* reformat node.h as per code formatting policy
* added Theory and NodeBuilder unit tests
Diffstat (limited to 'test/unit/expr/node_builder_black.h')
-rw-r--r-- | test/unit/expr/node_builder_black.h | 88 |
1 files changed, 71 insertions, 17 deletions
diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h index 8aff0faf0..871e93dca 100644 --- a/test/unit/expr/node_builder_black.h +++ b/test/unit/expr/node_builder_black.h @@ -15,7 +15,6 @@ #include <cxxtest/TestSuite.h> -//Used in some of the tests #include <vector> #include <limits.h> #include <sstream> @@ -65,7 +64,7 @@ public: /** * Tests just constructors. No modification is done to the node. */ - void testNodeConstructors(){ + void testNodeConstructors() { //inline NodeBuilder(); //inline NodeBuilder(Kind k); @@ -151,14 +150,14 @@ public: } - void testDestructor(){ + void testDestructor() { //inline ~NodeBuilder(); NodeBuilder<K>* nb = new NodeBuilder<K>(); delete nb; //Not sure what to test other than survival } - void testBeginEnd(){ + void testBeginEnd() { /* Test begin and ends without resizing */ NodeBuilder<K> ws; TS_ASSERT_EQUALS(ws.begin(), ws.end()); @@ -203,12 +202,12 @@ public: TS_ASSERT_EQUALS(smaller_citer, smaller.end()); } - void testIterator(){ + void testIterator() { NodeBuilder<> b; Node x = d_nm->mkVar(); Node y = d_nm->mkVar(); Node z = d_nm->mkVar(); - b << x << y << z << kind::AND; + b << x << y << z << AND; { NodeBuilder<>::iterator i = b.begin(); @@ -228,7 +227,7 @@ public: } } - void testGetKind(){ + void testGetKind() { /* Kind getKind() const; */ NodeBuilder<> noKind; TS_ASSERT_EQUALS(noKind.getKind(), UNDEFINED_KIND); @@ -244,15 +243,13 @@ public: TS_ASSERT_THROWS_ANYTHING(noKind.getKind();); #endif - NodeBuilder<> spec(specKind); TS_ASSERT_EQUALS(spec.getKind(), specKind); push_back(spec, K); TS_ASSERT_EQUALS(spec.getKind(), specKind); - } - void testGetNumChildren(){ + void testGetNumChildren() { /* unsigned getNumChildren() const; */ NodeBuilder<> noKind; @@ -282,7 +279,7 @@ public: #endif } - void testOperatorSquare(){ + void testOperatorSquare() { /* Node operator[](int i) const { Assert(i >= 0 && i < d_ev->getNumChildren()); @@ -332,7 +329,7 @@ public: #endif } - void testClear(){ + void testClear() { /* void clear(Kind k = UNDEFINED_KIND); */ NodeBuilder<> nb; @@ -378,7 +375,7 @@ public: } - void testStreamInsertionKind(){ + void testStreamInsertionKind() { /* NodeBuilder& operator<<(const Kind& k); */ #ifdef CVC4_DEBUG @@ -420,7 +417,7 @@ public: specKind); } - void testStreamInsertionNode(){ + void testStreamInsertionNode() { /* NodeBuilder& operator<<(const Node& n); */ NodeBuilder<K> nb(specKind); TS_ASSERT_EQUALS(nb.getKind(), specKind); @@ -449,7 +446,7 @@ public: } - void testAppend(){ + void testAppend() { Node x = d_nm->mkVar(); Node y = d_nm->mkVar(); Node z = d_nm->mkVar(); @@ -499,7 +496,7 @@ public: TS_ASSERT(b[8] == m); } - void testOperatorNodeCast(){ + void testOperatorNodeCast() { /* operator Node();*/ NodeBuilder<K> implicit(specKind); NodeBuilder<K> explic(specKind); @@ -521,7 +518,7 @@ public: #endif } - void testToStream(){ + void testToStream() { /* inline void toStream(std::ostream& out) const { d_ev->toStream(out); } @@ -571,4 +568,61 @@ public: TS_ASSERT_EQUALS(astr, bstr); TS_ASSERT_DIFFERS(astr, cstr); } + + void testConvenienceBuilders() { + Node a = d_nm->mkVar(); + Node b = d_nm->mkVar(); + Node c = d_nm->mkVar(); + Node d = d_nm->mkVar(); + Node e = d_nm->mkVar(); + Node f = d_nm->mkVar(); + + Node m = a && b; + Node n = a && b || c; + Node o = d + e - b; + 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; + + TS_ASSERT_EQUALS(m, d_nm->mkNode(AND, a, b)); + TS_ASSERT_EQUALS(n, d_nm->mkNode(OR, m, c)); + TS_ASSERT_EQUALS(o, d_nm->mkNode(PLUS, d, e, d_nm->mkNode(UMINUS, b))); + TS_ASSERT_EQUALS(p, d_nm->mkNode(OR, d_nm->mkNode(AND, a, o), c)); + + TS_ASSERT_EQUALS(x, d_nm->mkNode(PLUS, d, e, o, d_nm->mkNode(UMINUS, m))); + TS_ASSERT_EQUALS(y, d_nm->mkNode(PLUS, + f, + d_nm->mkNode(UMINUS, a), + d_nm->mkNode(UMINUS, c), + e)); + + TS_ASSERT_EQUALS(q, d_nm->mkNode(AND, a, b, c)); + + TS_ASSERT_EQUALS(r, d_nm->mkNode(OR, + d_nm->mkNode(AND, e, d, b, a), + d_nm->mkNode(AND, x, y), + f, + d_nm->mkNode(AND, q, a))); + + Node assoc1 = (a && b) && c; + Node assoc2 = a && (b && c); + + TS_ASSERT_EQUALS(assoc1, d_nm->mkNode(AND, a, b, c)); + TS_ASSERT_EQUALS(assoc2, d_nm->mkNode(AND, a, d_nm->mkNode(AND, b, c))); + + Node prec1 = (a && b) || c; + Node prec2 = a || (b && c); + Node prec3 = a && (b || c); + Node prec4 = (a || b) && c; + + TS_ASSERT_EQUALS(prec1, d_nm->mkNode(OR, d_nm->mkNode(AND, a, b), c)); + TS_ASSERT_EQUALS(prec2, d_nm->mkNode(OR, a, d_nm->mkNode(AND, b, c))); + TS_ASSERT_EQUALS(prec3, d_nm->mkNode(AND, a, d_nm->mkNode(OR, b, c))); + TS_ASSERT_EQUALS(prec4, d_nm->mkNode(AND, d_nm->mkNode(OR, a, b), c)); + } }; |