diff options
author | Tim King <taking@cs.nyu.edu> | 2010-02-25 01:05:40 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2010-02-25 01:05:40 +0000 |
commit | f716b67e7bedd90c4dd43617158c0f55c1811334 (patch) | |
tree | a0a6755d1ebad6ddebbdf96d9bcc05d591fba72a /test | |
parent | ff9bda51dfb047af2005f464847edd61314bb50c (diff) |
Created basic node builder and kind tests. Also fixed a couple of node builder problems.
Diffstat (limited to 'test')
-rw-r--r-- | test/unit/Makefile.am | 2 | ||||
-rw-r--r-- | test/unit/expr/kind_black.h | 89 | ||||
-rw-r--r-- | test/unit/expr/node_builder_black.h | 517 |
3 files changed, 608 insertions, 0 deletions
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index 591a85202..9fba9f7ff 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -2,6 +2,8 @@ UNIT_TESTS = \ expr/node_white \ expr/node_black \ + expr/kind_black \ + expr/node_builder_black \ parser/parser_black \ context/context_black \ context/context_mm_black \ diff --git a/test/unit/expr/kind_black.h b/test/unit/expr/kind_black.h new file mode 100644 index 000000000..35c5fde16 --- /dev/null +++ b/test/unit/expr/kind_black.h @@ -0,0 +1,89 @@ +/********************* */ +/** kind_black.h + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** + ** Black box testing of CVC4::Kind. + **/ + +#include <cxxtest/TestSuite.h> + +#include <iostream> +#include <string> +#include <sstream> + +#include "expr/kind.h" + +using namespace CVC4; +using namespace std; + +class KindBlack : public CxxTest::TestSuite { + Kind undefined; + Kind null; + Kind last; + + //easier to define in setup + int beyond; + Kind unknown; +public: + void setUp() { + undefined = UNDEFINED_KIND; + null = NULL_EXPR; + last = LAST_KIND; + beyond = ((int) LAST_KIND) + 1; + unknown = (Kind) beyond; + } + + + void testEquality(){ + + TS_ASSERT_EQUALS(undefined, UNDEFINED_KIND); + TS_ASSERT_EQUALS(last, LAST_KIND); + } + + void testOrder(){ + TS_ASSERT_LESS_THAN(int(undefined), int(null)); + TS_ASSERT_LESS_THAN(int(null), int(last)); + TS_ASSERT_LESS_THAN(int(undefined), int(last)); + TS_ASSERT_LESS_THAN(int(last), int(unknown)); + } + + bool stringIsAsExpected(Kind k, const char * s){ + stringstream act; + stringstream exp; + + act << k; + exp << s; + + string actCreated = act.str(); + string expCreated = exp.str(); + return actCreated == expCreated; + } + + void testOperatorLtLt() { + + TS_ASSERT(stringIsAsExpected(undefined, "UNDEFINED_KIND")); + TS_ASSERT(stringIsAsExpected(null, "NULL")); + TS_ASSERT(stringIsAsExpected(last, "LAST_KIND")); + + } + void testOperatorLtLtConcat() { + + stringstream act, exp; + act << undefined << null << last << unknown; + exp << "UNDEFINED_KIND" << "NULL" << "LAST_KIND" << "UNKNOWNKIND!"<< beyond; + + string actCreated = act.str(); + string expCreated = exp.str(); + + TS_ASSERT_EQUALS(actCreated, expCreated); + } + +}; diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h new file mode 100644 index 000000000..10d761166 --- /dev/null +++ b/test/unit/expr/node_builder_black.h @@ -0,0 +1,517 @@ +/********************* */ +/** node__builder_black.h + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** + ** Black box testing of CVC4::NodeBuilder. + **/ + +#include <cxxtest/TestSuite.h> + +//Used in some of the tests +#include <vector> +#include <limits.h> +#include <sstream> + +#include "expr/node_builder.h" +#include "expr/node_manager.h" +#include "expr/node.h" +#include "expr/kind.h" + +using namespace CVC4; +using namespace std; + +class NodeBuilderBlack : public CxxTest::TestSuite { +private: + + NodeManagerScope *d_scope; + NodeManager *d_nm; + +public: + + void setUp() { + d_nm = new NodeManager(); + d_scope = new NodeManagerScope(d_nm); + specKind = PLUS; + } + + void tearDown() { + delete d_nm; + delete d_scope; + } + + + template <unsigned N> + void push_back(NodeBuilder<N>& nb, int n){ + for(int i=0; i<n; ++i){ + nb << Node::null(); + } + } + +#define K 30 +#define LARGE_K UINT_MAX/40 + + Kind specKind; + + /** + * Tests just constructors. No modification is done to the node. + */ + void testNodeConstructors(){ + + //inline NodeBuilder(); + //inline NodeBuilder(Kind k); + //inline NodeBuilder(const NodeBuilder<nchild_thresh>& nb); + //template <unsigned N> inline NodeBuilder(const NodeBuilder<N>& nb); + //inline NodeBuilder(NodeManager* nm); + //inline NodeBuilder(NodeManager* nm, Kind k); + + /* default size tests */ + NodeBuilder<> def; + TS_ASSERT_EQUALS(def.getKind(), UNDEFINED_KIND); + TS_ASSERT_EQUALS(def.getNumChildren(), 0); + 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.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.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.begin(), from_nm_kind.end()); + + + /* Non-default size tests */ + + NodeBuilder<K> ws; + TS_ASSERT_EQUALS(ws.getKind(), UNDEFINED_KIND); + TS_ASSERT_EQUALS(ws.getNumChildren(), 0); + 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.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.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.begin(), ws_from_nm_kind.end()); + + + /* Extreme size tests */ + NodeBuilder<0> ws_size_0(); + + NodeBuilder<LARGE_K> ws_size_large(); + + /* CopyConstructors */ + + NodeBuilder<> copy(def); + TS_ASSERT_EQUALS(copy.getKind(), UNDEFINED_KIND); + TS_ASSERT_EQUALS(copy.getNumChildren(), 0); + 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.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.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.begin(), cp_from_smaller.end()); + + } + + void testDestructor(){ + //inline ~NodeBuilder(); + NodeBuilder<K>* nb = new NodeBuilder<K>(); + delete nb; + //Not sure what to test other than survival + } + + void testBeginEnd(){ + /* Test begin and ends without resizing */ + NodeBuilder<K> ws; + TS_ASSERT_EQUALS(ws.begin(), ws.end()); + + push_back(ws, K); + TS_ASSERT_DIFFERS(ws.begin(), ws.end()); + + NodeBuilder<K>::iterator iter = ws.begin(); + for(int 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){ + TS_ASSERT_DIFFERS(citer, ws.end()); + ++citer; + } + TS_ASSERT_EQUALS(citer, ws.end()); + + /* Do the same tests and make sure that resizing occurs */ + + NodeBuilder<> smaller; + TS_ASSERT_EQUALS(smaller.begin(), smaller.end()); + + push_back(smaller, K); + TS_ASSERT_DIFFERS(smaller.begin(), smaller.end()); + + NodeBuilder<>::iterator smaller_iter = smaller.begin(); + for(int 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){ + TS_ASSERT_DIFFERS(smaller_citer, smaller.end()); + ++smaller_citer; + } + TS_ASSERT_EQUALS(smaller_citer, smaller.end()); + } + + void testIterator(){ + TS_WARN( "TODO: This test still needs to be written!" ); + } + + void testGetKind(){ + /* Kind getKind() const; */ + NodeBuilder<> noKind; + TS_ASSERT_EQUALS(noKind.getKind(), UNDEFINED_KIND); + push_back(noKind, K); + TS_ASSERT_EQUALS(noKind.getKind(), UNDEFINED_KIND); + + noKind << specKind; + TS_ASSERT_EQUALS(noKind.getKind(), specKind); + + Node n = noKind; + + TS_ASSERT_THROWS_ANYTHING(noKind.getKind();); + + + + NodeBuilder<> spec(specKind); + TS_ASSERT_EQUALS(spec.getKind(), specKind); + push_back(spec, K); + TS_ASSERT_EQUALS(spec.getKind(), specKind); + + } + + void testGetNumChildren(){ + /* unsigned getNumChildren() const; */ + + NodeBuilder<> noKind; + TS_ASSERT_EQUALS(noKind.getNumChildren(), 0); + push_back(noKind, K); + + TS_ASSERT_EQUALS(noKind.getNumChildren(), K); + + push_back(noKind, K); + TS_ASSERT_EQUALS(noKind.getNumChildren(), K+K); + + noKind.clear(); + TS_ASSERT_EQUALS(noKind.getNumChildren(), 0); + push_back(noKind, K); + + TS_ASSERT_EQUALS(noKind.getNumChildren(), K); + + push_back(noKind, K); + TS_ASSERT_EQUALS(noKind.getNumChildren(), K+K); + + + noKind << specKind; + Node n = noKind; + TS_ASSERT_THROWS_ANYTHING(noKind.getNumChildren();); + } + + void testOperatorSquare(){ + /* + Node operator[](int i) const { + Assert(i >= 0 && i < d_ev->getNumChildren()); + return Node(d_ev->d_children[i]); + } + */ + NodeBuilder<> arr(specKind); + + Node i_0 = d_nm->mkNode(FALSE); + Node i_2 = d_nm->mkNode(TRUE); + Node i_K = d_nm->mkNode(NOT); + + + TS_ASSERT_THROWS_ANYTHING(arr[-1];); + TS_ASSERT_THROWS_ANYTHING(arr[0];); + + + arr << i_0; + + TS_ASSERT_EQUALS(arr[0], i_0); + + push_back(arr,1); + + arr << i_2; + + TS_ASSERT_EQUALS(arr[0], i_0); + TS_ASSERT_EQUALS(arr[2], i_2); + + push_back(arr, K-3); + + TS_ASSERT_EQUALS(arr[0], i_0); + TS_ASSERT_EQUALS(arr[2], i_2); + for(int i=3;i<K;++i) TS_ASSERT_EQUALS(arr[i], Node::null()); + + arr << i_K; + + + TS_ASSERT_EQUALS(arr[0], i_0); + TS_ASSERT_EQUALS(arr[2], i_2); + for(int i=3;i<K;++i) TS_ASSERT_EQUALS(arr[i], Node::null()); + TS_ASSERT_EQUALS(arr[K], i_K); + + Node n = arr; + TS_ASSERT_THROWS_ANYTHING(arr[0];); + } + + void testClear(){ + /* void clear(Kind k = UNDEFINED_KIND); */ + NodeBuilder<> nb; + + + TS_ASSERT_EQUALS(nb.getKind(), UNDEFINED_KIND); + TS_ASSERT_EQUALS(nb.getNumChildren(), 0); + TS_ASSERT_EQUALS(nb.begin(), nb.end()); + + nb << specKind; + push_back(nb, K); + + TS_ASSERT_EQUALS(nb.getKind(), specKind); + TS_ASSERT_EQUALS(nb.getNumChildren(), K); + TS_ASSERT_DIFFERS(nb.begin(), nb.end()); + + nb.clear(); + + TS_ASSERT_EQUALS(nb.getKind(), UNDEFINED_KIND); + TS_ASSERT_EQUALS(nb.getNumChildren(), 0); + TS_ASSERT_EQUALS(nb.begin(), nb.end()); + + nb << specKind; + push_back(nb, K); + + TS_ASSERT_EQUALS(nb.getKind(), specKind); + TS_ASSERT_EQUALS(nb.getNumChildren(), K); + TS_ASSERT_DIFFERS(nb.begin(), nb.end()); + + nb.clear(specKind); + + TS_ASSERT_EQUALS(nb.getKind(), specKind); + TS_ASSERT_EQUALS(nb.getNumChildren(), 0); + TS_ASSERT_EQUALS(nb.begin(), nb.end()); + + push_back(nb, K); + Node n = nb; + nb.clear(); + + + TS_ASSERT_EQUALS(nb.getKind(), UNDEFINED_KIND); + TS_ASSERT_EQUALS(nb.getNumChildren(), 0); + TS_ASSERT_EQUALS(nb.begin(), nb.end()); + + } + + void testStreamInsertionKind(){ + /* NodeBuilder& operator<<(const Kind& k); */ + + NodeBuilder<> spec(specKind); + TS_ASSERT_THROWS_ANYTHING( spec << PLUS; ); + + NodeBuilder<> noSpec; + noSpec << specKind; + TS_ASSERT_EQUALS(noSpec.getKind(), specKind); + + + NodeBuilder<> modified; + push_back(modified, K); + modified << specKind; + TS_ASSERT_EQUALS(modified.getKind(), specKind); + + NodeBuilder<> nb(specKind); + Node n = nb; + nb.clear(PLUS); + TS_ASSERT_THROWS_ANYTHING(nb << PLUS;); + + NodeBuilder<> testRef; + TS_ASSERT_EQUALS((testRef << specKind).getKind(), specKind); + + + NodeBuilder<> testTwo; + TS_ASSERT_THROWS_ANYTHING(testTwo << specKind << PLUS;); + + NodeBuilder<> testMixOrder1; + TS_ASSERT_EQUALS((testMixOrder1<< specKind << d_nm->mkNode(TRUE)).getKind(), + specKind); + NodeBuilder<> testMixOrder2; + TS_ASSERT_EQUALS((testMixOrder2<< d_nm->mkNode(TRUE)<<specKind).getKind(), + specKind); + } + + void testStreamInsertionNode(){ + /* 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.begin(), nb.end()); + push_back(nb,K); + TS_ASSERT_EQUALS(nb.getKind(), specKind); + TS_ASSERT_EQUALS(nb.getNumChildren(), K); + TS_ASSERT_DIFFERS(nb.begin(), nb.end()); + + Node n = nb; + TS_ASSERT_THROWS_ANYTHING(nb << n;); + + + NodeBuilder<> overflow(specKind); + TS_ASSERT_EQUALS(overflow.getKind(), specKind); + TS_ASSERT_EQUALS(overflow.getNumChildren(), 0); + 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_DIFFERS(overflow.begin(), overflow.end()); + + } + + void testAppend(){ + /* + NodeBuilder& append(const Node& n) { + Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion"); + Debug("prop") << "append: " << this << " " << n << "[" << n.d_ev << "]" << std::endl; + allocateEvIfNecessaryForAppend(); + NodeValue* ev = n.d_ev; + ev->inc(); + d_ev->d_children[d_ev->d_nchildren++] = ev; + return *this; + } + */ + /* + + template <class Iterator> + NodeBuilder& append(const Iterator& begin, const Iterator& end) { + Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion"); + for(Iterator i = begin; i != end; ++i) { + append(*i); + } + return *this; + } + + */ + TS_WARN( "TODO: This test still needs to be written!" ); + } + + void testOperatorNodeCast(){ + /* operator Node();*/ + NodeBuilder<K> implicit(specKind); + NodeBuilder<K> explic(specKind); + + push_back(implicit, K); + push_back(explic, K); + + Node nimpl = implicit; + Node nexplicit = (Node) explic; + + TS_ASSERT_EQUALS(nimpl.getKind(), specKind); + TS_ASSERT_EQUALS(nimpl.getNumChildren(), K); + + TS_ASSERT_EQUALS(nexplicit.getKind(), specKind); + TS_ASSERT_EQUALS(nexplicit.getNumChildren(), K); + + TS_ASSERT_THROWS_ANYTHING(Node blah = implicit); + } + + void testToStream(){ + /* inline void toStream(std::ostream& out) const { + d_ev->toStream(out); + } + */ + + NodeBuilder<K> a(specKind); + NodeBuilder<K> b(specKind); + NodeBuilder<K> c(TRUE); + string astr, bstr, cstr; + stringstream astream, bstream, cstream; + + push_back(a,K/2); + push_back(b,K/2); + push_back(c,K/2); + + + a.toStream(astream); + b.toStream(bstream); + c.toStream(cstream); + + + astr = astream.str(); + bstr = bstream.str(); + cstr = cstream.str(); + + TS_ASSERT_EQUALS(astr, bstr); + TS_ASSERT_DIFFERS(astr, cstr); + + + a.clear(specKind); + b.clear(specKind); + c.clear(specKind); + astream.flush(); + bstream.flush(); + cstream.flush(); + + + push_back(a,2*K); + push_back(b,2*K); + push_back(c,2*K+1); + + + a.toStream(astream); + b.toStream(bstream); + c.toStream(cstream); + + + astr = astream.str(); + bstr = bstream.str(); + cstr = cstream.str(); + + TS_ASSERT_EQUALS(astr, bstr); + TS_ASSERT_DIFFERS(astr, cstr); + } +}; |