diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-03-16 20:24:37 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-03-16 20:24:37 +0000 |
commit | 9576517676138a8ca2887a967f1b056662ef6754 (patch) | |
tree | f0040a8189d20496dcaa760055b2b818f8a57525 /test/unit/expr/node_black.h | |
parent | 12ad4cf2de936acbf8c21117804c69b2deaa7272 (diff) |
* test/unit/Makefile.am, test/unit/expr/attribute_white.h,
test/unit/expr/node_white.h: add whitebox attribute test (pulled out
attribute stuff from node_white)
* test/unit/parser/parser_black.h: fix memory leaks uncovered by
valgrind
* src/theory/interrupted.h: actually make this "lightweight" (not
derived from CVC4::Exception), as promised in my last commit
* src/theory/uf/theory_uf.h, test/unit/expr/attribute_black.h: match
the new-style cleanup function definition
* src/expr/attribute.cpp, src/expr/attribute.h: support for attribute
deletion, custom cleanup functions, clearer cleanup function
definition.
* src/expr/node_manager.h, src/expr/node_manager.cpp: reclaim
remaining zombies in dtor, rename NodeValueSet ==> "NodeValuePool",
and enable freeing of NodeValues
* src/expr/type.h, src/expr/type.cpp: reference-counting for types,
customized cleanup function for types, also code cleanup
* (various): changed "const Type*" to "Type*" (to enable
reference-counting etc. Types are still immutable.)
* src/util/output.h: add ::isOn()-- which queries whether a
Debug/Trace flag is currently on or not.
* src/smt/smt_engine.cpp, src/parser/antlr_parser.cpp,
src/expr/type.cpp, src/expr/expr_manager.cpp, various others:
minor code cleanup
Diffstat (limited to 'test/unit/expr/node_black.h')
-rw-r--r-- | test/unit/expr/node_black.h | 131 |
1 files changed, 67 insertions, 64 deletions
diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h index c1ece1145..21c19a8f9 100644 --- a/test/unit/expr/node_black.h +++ b/test/unit/expr/node_black.h @@ -72,7 +72,7 @@ public: TS_ASSERT(b.isNull()); Node c = b; - + TS_ASSERT(c.isNull()); } @@ -93,7 +93,7 @@ public: /*tests: bool operator==(const Node& e) const */ void testOperatorEquals() { Node a, b, c; - + b = d_nodeManager->mkVar(); a = b; @@ -113,7 +113,7 @@ public: TS_ASSERT(c==a); TS_ASSERT(c==b); - TS_ASSERT(c==c); + TS_ASSERT(c==c); TS_ASSERT(d==d); @@ -133,7 +133,7 @@ public: Node a, b, c; - + b = d_nodeManager->mkVar(); a = b; @@ -142,19 +142,19 @@ public: Node d = d_nodeManager->mkVar(); /*structed assuming operator == works */ - TS_ASSERT(iff(a!=a,!(a==a))); - TS_ASSERT(iff(a!=b,!(a==b))); - TS_ASSERT(iff(a!=c,!(a==c))); + TS_ASSERT(iff(a!=a, !(a==a))); + TS_ASSERT(iff(a!=b, !(a==b))); + TS_ASSERT(iff(a!=c, !(a==c))); - TS_ASSERT(iff(b!=a,!(b==a))); - TS_ASSERT(iff(b!=b,!(b==b))); - TS_ASSERT(iff(b!=c,!(b==c))); + TS_ASSERT(iff(b!=a, !(b==a))); + TS_ASSERT(iff(b!=b, !(b==b))); + TS_ASSERT(iff(b!=c, !(b==c))); - TS_ASSERT(iff(c!=a,!(c==a))); - TS_ASSERT(iff(c!=b,!(c==b))); - TS_ASSERT(iff(c!=c,!(c==c))); + TS_ASSERT(iff(c!=a, !(c==a))); + TS_ASSERT(iff(c!=b, !(c==b))); + TS_ASSERT(iff(c!=c, !(c==c))); TS_ASSERT(!(d!=d)); @@ -164,7 +164,7 @@ public: } - void testOperatorSquare() { + void testOperatorSquare() { /*Node operator[](int i) const */ #ifdef CVC4_ASSERTIONS @@ -177,7 +177,7 @@ public: Node tb = d_nodeManager->mkNode(TRUE); Node eb = d_nodeManager->mkNode(FALSE); Node cnd = d_nodeManager->mkNode(XOR, tb, eb); - Node ite = cnd.iteNode(tb,eb); + Node ite = cnd.iteNode(tb, eb); TS_ASSERT(tb == cnd[0]); TS_ASSERT(eb == cnd[1]); @@ -188,8 +188,8 @@ public: #ifdef CVC4_ASSERTIONS //Bounds check on a node with children - TS_ASSERT_THROWS(ite == ite[-1],AssertionException); - TS_ASSERT_THROWS(ite == ite[4],AssertionException); + TS_ASSERT_THROWS(ite == ite[-1], AssertionException); + TS_ASSERT_THROWS(ite == ite[4], AssertionException); #endif /* CVC4_ASSERTIONS */ } @@ -197,23 +197,23 @@ public: void testOperatorAssign() { Node a, b; Node c = d_nodeManager->mkNode(NOT); - + b = c; TS_ASSERT(b==c); - + a = b = c; TS_ASSERT(a==b); TS_ASSERT(a==c); } - + void testOperatorLessThan() { /* We don't have access to the ids so we can't test the implementation - * in the black box tests. + * in the black box tests. */ - + Node a = d_nodeManager->mkVar(); Node b = d_nodeManager->mkVar(); @@ -225,14 +225,14 @@ public: TS_ASSERT(!(c<d)); TS_ASSERT(!(d<c)); - + /* TODO: * Less than has the rather difficult to test property that subexpressions * are less than enclosing expressions. * * But what would be a convincing test of this property? */ - + //Simple test of descending descendant property Node child = d_nodeManager->mkNode(TRUE); Node parent = d_nodeManager->mkNode(NOT, child); @@ -245,9 +245,9 @@ public: Node curr = d_nodeManager->mkNode(NULL_EXPR); for(int i=0;i<N;i++) { chain.push_back(curr); - curr = d_nodeManager->mkNode(AND,curr); + curr = d_nodeManager->mkNode(AND, curr); } - + for(int i=0;i<N;i++) { for(int j=i+1;j<N;j++) { Node chain_i = chain[i]; @@ -255,16 +255,16 @@ public: TS_ASSERT(chain_i<chain_j); } } - + } void testEqNode() { /*Node eqNode(const Node& right) const;*/ Node left = d_nodeManager->mkNode(TRUE); - Node right = d_nodeManager->mkNode(NOT,(d_nodeManager->mkNode(FALSE))); + Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkNode(FALSE))); Node eq = left.eqNode(right); - + TS_ASSERT(EQUAL == eq.getKind()); TS_ASSERT(2 == eq.getNumChildren()); @@ -283,31 +283,31 @@ public: TS_ASSERT(1 == parent.getNumChildren()); TS_ASSERT(parent[0] == child); - + } void testAndNode() { /*Node andNode(const Node& right) const;*/ - + Node left = d_nodeManager->mkNode(TRUE); - Node right = d_nodeManager->mkNode(NOT,(d_nodeManager->mkNode(FALSE))); + Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkNode(FALSE))); Node eq = left.andNode(right); - + TS_ASSERT(AND == eq.getKind()); TS_ASSERT(2 == eq.getNumChildren()); TS_ASSERT(*(eq.begin()) == left); TS_ASSERT(*(++eq.begin()) == right); - + } void testOrNode() { /*Node orNode(const Node& right) const;*/ - + Node left = d_nodeManager->mkNode(TRUE); - Node right = d_nodeManager->mkNode(NOT,(d_nodeManager->mkNode(FALSE))); + Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkNode(FALSE))); Node eq = left.orNode(right); - + TS_ASSERT(OR == eq.getKind()); TS_ASSERT(2 == eq.getNumChildren()); @@ -322,9 +322,9 @@ public: Node cnd = d_nodeManager->mkNode(PLUS); Node thenBranch = d_nodeManager->mkNode(TRUE); - Node elseBranch = d_nodeManager->mkNode(NOT,(d_nodeManager->mkNode(FALSE))); - Node ite = cnd.iteNode(thenBranch,elseBranch); - + Node elseBranch = d_nodeManager->mkNode(NOT, (d_nodeManager->mkNode(FALSE))); + Node ite = cnd.iteNode(thenBranch, elseBranch); + TS_ASSERT(ITE == ite.getKind()); TS_ASSERT(3 == ite.getNumChildren()); @@ -336,11 +336,11 @@ public: void testIffNode() { /* Node iffNode(const Node& right) const; */ - + Node left = d_nodeManager->mkNode(TRUE); - Node right = d_nodeManager->mkNode(NOT,(d_nodeManager->mkNode(FALSE))); + Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkNode(FALSE))); Node eq = left.iffNode(right); - + TS_ASSERT(IFF == eq.getKind()); TS_ASSERT(2 == eq.getNumChildren()); @@ -349,13 +349,13 @@ public: TS_ASSERT(*(++eq.begin()) == right); } - + void testImpNode() { /* Node impNode(const Node& right) const; */ Node left = d_nodeManager->mkNode(TRUE); - Node right = d_nodeManager->mkNode(NOT,(d_nodeManager->mkNode(FALSE))); + Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkNode(FALSE))); Node eq = left.impNode(right); - + TS_ASSERT(IMPLIES == eq.getKind()); TS_ASSERT(2 == eq.getNumChildren()); @@ -367,9 +367,9 @@ public: void testXorNode() { /*Node xorNode(const Node& right) const;*/ Node left = d_nodeManager->mkNode(TRUE); - Node right = d_nodeManager->mkNode(NOT,(d_nodeManager->mkNode(FALSE))); + Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkNode(FALSE))); Node eq = left.xorNode(right); - + TS_ASSERT(XOR == eq.getKind()); TS_ASSERT(2 == eq.getNumChildren()); @@ -394,13 +394,13 @@ public: void testGetOperator() { - const Type* sort = d_nodeManager->mkSort("T"); - const Type* booleanType = d_nodeManager->booleanType(); - const Type* predType = d_nodeManager->mkFunctionType(sort,booleanType); + Type* sort = d_nodeManager->mkSort("T"); + Type* booleanType = d_nodeManager->booleanType(); + Type* predType = d_nodeManager->mkFunctionType(sort, booleanType); Node f = d_nodeManager->mkVar(predType); Node a = d_nodeManager->mkVar(booleanType); - Node fa = d_nodeManager->mkNode(kind::APPLY,f,a); + Node fa = d_nodeManager->mkNode(kind::APPLY, f, a); TS_ASSERT( fa.hasOperator() ); TS_ASSERT( !f.hasOperator() ); @@ -410,7 +410,7 @@ public: TS_ASSERT_THROWS( f.getOperator(), AssertionException ); TS_ASSERT_THROWS( a.getOperator(), AssertionException ); } - + void testNaryExpForSize(Kind k, int N){ NodeBuilder<> nbz(k); for(int i=0;i<N;i++){ @@ -434,13 +434,13 @@ public: //Bigger tests - srand(0); + srand(0); int trials = 500; for(int i=0;i<trials; i++){ int N = rand() % 1000; testNaryExpForSize(NOT, N); } - + } void testIterator(){ @@ -469,10 +469,12 @@ public: } void testToString(){ - Node w = d_nodeManager->mkVar(NULL, "w"); - Node x = d_nodeManager->mkVar(NULL, "x"); - Node y = d_nodeManager->mkVar(NULL, "y"); - Node z = d_nodeManager->mkVar(NULL, "z"); + Type* booleanType = d_nodeManager->booleanType(); + + Node w = d_nodeManager->mkVar(booleanType, "w"); + Node x = d_nodeManager->mkVar(booleanType, "x"); + Node y = d_nodeManager->mkVar(booleanType, "y"); + Node z = d_nodeManager->mkVar(booleanType, "z"); Node m = NodeBuilder<>() << w << x << kind::OR; Node n = NodeBuilder<>() << m << y << z << kind::AND; @@ -480,11 +482,12 @@ public: } void testToStream(){ - NodeBuilder<> b; - Node w = d_nodeManager->mkVar(NULL, "w"); - Node x = d_nodeManager->mkVar(NULL, "x"); - Node y = d_nodeManager->mkVar(NULL, "y"); - Node z = d_nodeManager->mkVar(NULL, "z"); + Type* booleanType = d_nodeManager->booleanType(); + + Node w = d_nodeManager->mkVar(booleanType, "w"); + Node x = d_nodeManager->mkVar(booleanType, "x"); + Node y = d_nodeManager->mkVar(booleanType, "y"); + Node z = d_nodeManager->mkVar(booleanType, "z"); Node m = NodeBuilder<>() << x << y << kind::OR; Node n = NodeBuilder<>() << w << m << z << kind::AND; |