Added additional tests to node_black.h. CVC4 currently passes all but 1 test.

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!" );
+  }
 };