diff options
Diffstat (limited to 'test/unit/expr/node_black.h')
-rw-r--r-- | test/unit/expr/node_black.h | 401 |
1 files changed, 401 insertions, 0 deletions
diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h index aa99c70c4..7cb744d02 100644 --- a/test/unit/expr/node_black.h +++ b/test/unit/expr/node_black.h @@ -15,18 +15,419 @@ #include <cxxtest/TestSuite.h> +//Used in some of the tests +#include <vector> + +#include "expr/node_value.h" +#include "expr/node_builder.h" +#include "expr/node_manager.h" #include "expr/node.h" using namespace CVC4; +using namespace std; class NodeBlack : public CxxTest::TestSuite { +private: + + NodeManagerScope *d_scope; + NodeManager *d_nm; + public: + void setUp() { + d_nm = new NodeManager(); + d_scope = new NodeManagerScope(d_nm); + } + + void tearDown(){ + delete d_nm; + delete d_scope; + } + + bool imp(bool a, bool b) const { + return (!a) || (b); + } + bool iff(bool a, bool b) const { + return (a && b) || ((!a)&&(!b)); + } + void testNull() { Node::null(); } + void testIsNull(){ + /* bool isNull() const; */ + + Node a = Node::null(); + TS_ASSERT(a.isNull()); + + Node b = Node(); + TS_ASSERT(b.isNull()); + + } + void testCopyCtor() { Node e(Node::null()); } + + void testDestructor(){ + /* No access to internals ? + * Makes sense to only test that this is crash free. + */ + + Node *n = new Node(); + delete n; + + } + + /*tests: bool operator==(const Node& e) const */ + void testOperatorEquals(){ + Node a, b, c; + + b = d_nm->mkVar(); + + a = b; + c = a; + + Node d = d_nm->mkVar(); + + TS_ASSERT(a==a); + TS_ASSERT(a==b); + TS_ASSERT(a==c); + + TS_ASSERT(b==a); + TS_ASSERT(b==b); + TS_ASSERT(b==c); + + + + TS_ASSERT(c==a); + TS_ASSERT(c==b); + TS_ASSERT(c==c); + + + TS_ASSERT(d==d); + + TS_ASSERT(!(d==a)); + TS_ASSERT(!(d==b)); + TS_ASSERT(!(d==c)); + + TS_ASSERT(!(a==d)); + TS_ASSERT(!(b==d)); + TS_ASSERT(!(c==d)); + + } + + /* operator!= */ + void testOperatorNotEquals(){ + + + Node a, b, c; + + b = d_nm->mkVar(); + + a = b; + c = a; + + Node d = d_nm->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(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(!(d!=d)); + + TS_ASSERT(d!=a); + TS_ASSERT(d!=b); + TS_ASSERT(d!=c); + + } + + /*tests: Node& operator=(const Node&); */ + void testOperatorAssign(){ + Node a, b; + Node c = d_nm->mkNode(UNDEFINED_KIND); + + a = b = c; + + TS_ASSERT(a==b); + TS_ASSERT(b==c); + 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. + */ + + + Node a = d_nm->mkVar(); + Node b = d_nm->mkVar(); + + TS_ASSERT(a<b || b<a); + TS_ASSERT(!(a<b && b<a)); + + Node c = d_nm->mkNode(UNDEFINED_KIND); + Node d = d_nm->mkNode(UNDEFINED_KIND); + + 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_nm->mkNode(TRUE); + Node parent = d_nm->mkNode(NOT, child); + + TS_ASSERT(child < parent); + + //Slightly less simple test of DD property. + std::vector<Node> chain; + int N = 500; + Node curr = d_nm->mkNode(UNDEFINED_KIND); + for(int i=0;i<N;i++){ + chain.push_back(curr); + curr = d_nm->mkNode(AND,curr); + } + + for(int i=0;i<N;i++){ + for(int j=i+1;j<N;j++){ + Node chain_i = chain[i]; + Node chain_j = chain[j]; + TS_ASSERT(chain_i<chain_j); + } + } + + } + + void testHash(){ + /* Not sure how to test this except survial... */ + Node a; + a.hash(); + cout << "testing hash" << endl; + } + + + + void testEqExpr(){ + /*Node eqExpr(const Node& right) const;*/ + + Node left = d_nm->mkNode(TRUE); + Node right = d_nm->mkNode(NOT,(d_nm->mkNode(FALSE))); + Node eq = left.eqExpr(right); + + + TS_ASSERT(EQUAL == eq.getKind()); + TS_ASSERT(2 == eq.numChildren()); + + TS_ASSERT(*(eq.begin()) == left); + TS_ASSERT(*(++eq.begin()) == right); + } + + void testNotExpr(){ + /* Node notExpr() const;*/ + + Node child = d_nm->mkNode(TRUE); + Node parent = child.notExpr(); + + TS_ASSERT(NOT == parent.getKind()); + TS_ASSERT(1 == parent.numChildren()); + + TS_ASSERT(*(parent.begin()) == child); + + } + void testAndExpr(){ + /*Node andExpr(const Node& right) const;*/ + + Node left = d_nm->mkNode(TRUE); + Node right = d_nm->mkNode(NOT,(d_nm->mkNode(FALSE))); + Node eq = left.andExpr(right); + + + TS_ASSERT(AND == eq.getKind()); + TS_ASSERT(2 == eq.numChildren()); + + TS_ASSERT(*(eq.begin()) == left); + TS_ASSERT(*(++eq.begin()) == right); + + } + + void testOrExpr(){ + /*Node orExpr(const Node& right) const;*/ + + Node left = d_nm->mkNode(TRUE); + Node right = d_nm->mkNode(NOT,(d_nm->mkNode(FALSE))); + Node eq = left.orExpr(right); + + + TS_ASSERT(OR == eq.getKind()); + TS_ASSERT(2 == eq.numChildren()); + + TS_ASSERT(*(eq.begin()) == left); + TS_ASSERT(*(++eq.begin()) == right); + + } + + void testIteExpr(){ + /*Node iteExpr(const Node& thenpart, const Node& elsepart) const;*/ + + Node cnd = d_nm->mkNode(PLUS); + Node thenBranch = d_nm->mkNode(TRUE); + Node elseBranch = d_nm->mkNode(NOT,(d_nm->mkNode(FALSE))); + Node ite = cnd.iteExpr(thenBranch,elseBranch); + + + TS_ASSERT(ITE == ite.getKind()); + TS_ASSERT(3 == ite.numChildren()); + + TS_ASSERT(*(ite.begin()) == cnd); + TS_ASSERT(*(++ite.begin()) == thenBranch); + TS_ASSERT(*(++(++ite.begin())) == elseBranch); + } + + void testIffExpr(){ + /* Node iffExpr(const Node& right) const; */ + + Node left = d_nm->mkNode(TRUE); + Node right = d_nm->mkNode(NOT,(d_nm->mkNode(FALSE))); + Node eq = left.iffExpr(right); + + + TS_ASSERT(IFF == eq.getKind()); + TS_ASSERT(2 == eq.numChildren()); + + TS_ASSERT(*(eq.begin()) == left); + TS_ASSERT(*(++eq.begin()) == right); + } + + + void testImpExpr(){ + /* Node impExpr(const Node& right) const; */ + Node left = d_nm->mkNode(TRUE); + Node right = d_nm->mkNode(NOT,(d_nm->mkNode(FALSE))); + Node eq = left.impExpr(right); + + + TS_ASSERT(IMPLIES == eq.getKind()); + TS_ASSERT(2 == eq.numChildren()); + + TS_ASSERT(*(eq.begin()) == left); + TS_ASSERT(*(++eq.begin()) == right); + } + + void testXorExpr(){ + /*Node xorExpr(const Node& right) const;*/ + Node left = d_nm->mkNode(TRUE); + Node right = d_nm->mkNode(NOT,(d_nm->mkNode(FALSE))); + Node eq = left.xorExpr(right); + + + TS_ASSERT(XOR == eq.getKind()); + TS_ASSERT(2 == eq.numChildren()); + + TS_ASSERT(*(eq.begin()) == left); + TS_ASSERT(*(++eq.begin()) == right); + } + + void testPlusExpr(){ + /*Node plusExpr(const Node& right) const;*/ + TS_WARN( "TODO: No implementation to test." ); + } + + void testUMinusExpr(){ + /*Node uMinusExpr() const;*/ + TS_WARN( "TODO: No implementation to test." ); + } + void testMultExpr(){ + /* Node multExpr(const Node& right) const;*/ + TS_WARN( "TODO: No implementation to test." ); + } + + void testKindSingleton(Kind k){ + Node n = d_nm->mkNode(k); + TS_ASSERT(k == n.getKind()); + } + + void testGetKind(){ + /*inline Kind getKind() const; */ + + testKindSingleton(NOT); + testKindSingleton(NULL_EXPR); + testKindSingleton(ITE); + testKindSingleton(SKOLEM); + testKindSingleton(UNDEFINED_KIND); + /* undefined kind does not work? */ + } + + void testNaryExpForSize(Kind k, int N){ + NodeBuilder<> nbz(k); + for(int i=0;i<N;i++){ + nbz << Node::null(); + } + Node result = nbz; + TS_ASSERT( N == result.numChildren()); + } + + void testNumChildren(){ + /*inline size_t numChildren() const;*/ + + //test 0 + TS_ASSERT(0 == (Node::null()).numChildren()); + + //test 1 + + TS_ASSERT(1 == (Node::null().notExpr()).numChildren()); + + //test 2 + + TS_ASSERT(2 == (Node::null().andExpr(Node::null())).numChildren() ); + + //Bigger tests + + srand(0); + int trials = 500; + for(int i=0;i<trials; i++){ + int N = rand() % 1000; + testNaryExpForSize(NOT, N); + } + + } + + void testIterator(){ + /*typedef NodeValue::node_iterator iterator; */ + /*typedef NodeValue::node_iterator const_iterator; */ + + /*inline iterator begin(); */ + /*inline iterator end(); */ + /*inline const_iterator begin() const; */ + /*inline const_iterator end() const; */ + + TS_WARN( "TODO: This test still needs to be written!" ); + } + + void testToString(){ + /*inline std::string toString() const; */ + TS_WARN( "TODO: This test still needs to be written!" ); + } + + void testToStream(){ + /*inline void toStream(std::ostream&) const;*/ + TS_WARN( "TODO: This test still needs to be written!" ); + } }; |