#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!" );
+ }
};
projects / cvc5.git / commitdiff