From: Tim King Date: Thu, 25 Feb 2010 01:05:40 +0000 (+0000) Subject: Created basic node builder and kind tests. Also fixed a couple of node builder problems. X-Git-Tag: cvc5-1.0.0~9224 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f716b67e7bedd90c4dd43617158c0f55c1811334;p=cvc5.git Created basic node builder and kind tests. Also fixed a couple of node builder problems. --- diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index d79d5ad54..cd34c415b 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -214,6 +214,7 @@ public: operator Node(); inline void toStream(std::ostream& out) const { + Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion"); d_nv->toStream(out); } @@ -448,9 +449,9 @@ inline NodeBuilder::NodeBuilder(const NodeBuilder& nb) : if(nb.d_nv->d_nchildren > nchild_thresh) { realloc(nb.d_size, false); - std::copy(nb.d_nv->ev_begin(), nb.d_nv->ev_end(), d_nv->nv_begin()); + std::copy(nb.d_nv->nv_begin(), nb.d_nv->nv_end(), d_nv->nv_begin()); } else { - std::copy(nb.d_nv->ev_begin(), nb.d_nv->ev_end(), d_inlineNv.nv_begin()); + std::copy(nb.d_nv->nv_begin(), nb.d_nv->nv_end(), d_inlineNv.nv_begin()); } d_nv->d_kind = nb.d_nv->d_kind; d_nv->d_nchildren = nb.d_nv->d_nchildren; @@ -648,6 +649,7 @@ NodeBuilder::operator Node() {// not const template inline std::ostream& operator<<(std::ostream& out, const NodeBuilder& b) { + b.toStream(out); return out; } 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 + +#include +#include +#include + +#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 + +//Used in some of the tests +#include +#include +#include + +#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 + void push_back(NodeBuilder& nb, int n){ + for(int i=0; i& nb); + //template inline NodeBuilder(const NodeBuilder& 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 ws; + TS_ASSERT_EQUALS(ws.getKind(), UNDEFINED_KIND); + TS_ASSERT_EQUALS(ws.getNumChildren(), 0); + TS_ASSERT_EQUALS(ws.begin(), ws.end()); + + NodeBuilder 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 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 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 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 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 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 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* nb = new NodeBuilder(); + delete nb; + //Not sure what to test other than survival + } + + void testBeginEnd(){ + /* Test begin and ends without resizing */ + NodeBuilder ws; + TS_ASSERT_EQUALS(ws.begin(), ws.end()); + + push_back(ws, K); + TS_ASSERT_DIFFERS(ws.begin(), ws.end()); + + NodeBuilder::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::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 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)< 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 + 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 implicit(specKind); + NodeBuilder 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 a(specKind); + NodeBuilder b(specKind); + NodeBuilder 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); + } +};