added experimental "make lcov" target (it runs only unit tests); better coverage for util and context classes; implemented some output functionality that was missing; reclassified some tests white -> black or black -> public; other minor fixes

1 files changed, 0 insertions, 422 deletions

diff --git a/test/unit/expr/expr_black.h b/test/unit/expr/expr_black.h
deleted file mode 100644
index 936381cd6..000000000
--- a/test/unit/expr/expr_black.h
+++ /dev/null
@@ -1,422 +0,0 @@
-/*********************                                                        */
-/** expr_black.h
- ** Original author: mdeters
- ** 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::Expr.
- **/
-
-#include <cxxtest/TestSuite.h>
-
-#include <sstream>
-#include <string>
-
-#include "expr/expr_manager.h"
-#include "expr/expr.h"
-#include "util/Assert.h"
-#include "util/exception.h"
-
-using namespace CVC4;
-using namespace CVC4::kind;
-using namespace std;
-
-class ExprBlack : public CxxTest::TestSuite {
-private:
-
-  ExprManager* d_em;
-
-  Expr* a;
-  Expr* b;
-  Expr* c;
-  Expr* mult;
-  Expr* plus;
-  Expr* d;
-  Expr* null;
-
-  Expr* i1;
-  Expr* i2;
-  Expr* r1;
-  Expr* r2;
-
-public:
-
-  void setUp() {
-    try {
-      d_em = new ExprManager;
-
-      a = new Expr(d_em->mkVar("a",d_em->booleanType()));
-      b = new Expr(d_em->mkVar("b", d_em->booleanType()));
-      c = new Expr(d_em->mkExpr(MULT, *a, *b));
-      mult = new Expr(d_em->mkConst(MULT));
-      plus = new Expr(d_em->mkConst(PLUS));
-      d = new Expr(d_em->mkExpr(APPLY_UF, *plus, *b, *c));
-      null = new Expr;
-
-      i1 = new Expr(d_em->mkConst(Integer("0")));
-      i2 = new Expr(d_em->mkConst(Integer(23)));
-      r1 = new Expr(d_em->mkConst(Rational(1, 5)));
-      r2 = new Expr(d_em->mkConst(Rational("0")));
-    } catch(Exception e) {
-      cerr << "Exception during setUp():" << endl << e;
-      throw;
-    }
-  }
-
-  void tearDown() {
-    try {
-      delete r2;
-      delete r1;
-      delete i2;
-      delete i1;
-
-      delete null;
-      delete d;
-      delete plus;
-      delete mult;
-      delete c;
-      delete b;
-      delete a;
-
-      delete d_em;
-    } catch(Exception e) {
-      cerr << "Exception during tearDown():" << endl << e;
-      throw;
-    }
-  }
-
-  void testDefaultCtor() {
-    /* Expr(); */
-    Expr e;
-    TS_ASSERT(e.isNull());
-  }
-
-  void testCtors() {
-    TS_ASSERT(!a->isNull());
-    TS_ASSERT(!b->isNull());
-
-    /* Expr(); */
-    Expr e;
-    TS_ASSERT(e.isNull());
-
-    /* Expr(const Expr& e) */
-    Expr e2(e);
-    TS_ASSERT(e == e2);
-    TS_ASSERT(e2 == e);
-    TS_ASSERT(!(e2 < e));
-    TS_ASSERT(!(e < e2));
-    TS_ASSERT(e.isNull());
-    TS_ASSERT(e2.isNull());
-    Expr f = d_em->mkExpr(PLUS, *a, *b);
-    Expr f2 = f;
-    TS_ASSERT(!f.isNull());
-    TS_ASSERT(!f2.isNull());
-    TS_ASSERT(f == f2);
-    TS_ASSERT(f2 == f);
-    TS_ASSERT(!(f2 < f));
-    TS_ASSERT(!(f < f2));
-    TS_ASSERT(f == d_em->mkExpr(PLUS, *a, *b));
-  }
-
-  void testAssignment() {
-    /* Expr& operator=(const Expr& e); */
-    Expr e = d_em->mkExpr(PLUS, *a, *b);
-    Expr f;
-    TS_ASSERT(f.isNull());
-    f = e;
-    TS_ASSERT(!f.isNull());
-    TS_ASSERT(e == f);
-    TS_ASSERT(f == e);
-    TS_ASSERT(!(f < e));
-    TS_ASSERT(!(e < f));
-    TS_ASSERT(f == d_em->mkExpr(PLUS, *a, *b));
-  }
-
-  void testEquality() {
-    /* bool operator==(const Expr& e) const; */
-    /* bool operator!=(const Expr& e) const; */
-
-    TS_ASSERT(*a == *a);
-    TS_ASSERT(*b == *b);
-    TS_ASSERT(!(*a != *a));
-    TS_ASSERT(!(*b != *b));
-
-    TS_ASSERT(*a != *b);
-    TS_ASSERT(*b != *a);
-    TS_ASSERT(!(*a == *b));
-    TS_ASSERT(!(*b == *a));
-  }
-
-  void testComparison() {
-    /* bool operator<(const Expr& e) const; */
-
-    TS_ASSERT(*null < *a);
-    TS_ASSERT(*null < *b);
-    TS_ASSERT(*null < *c);
-    TS_ASSERT(*null < *d);
-    TS_ASSERT(*null < *plus);
-    TS_ASSERT(*null < *mult);
-    TS_ASSERT(*null < *i1);
-    TS_ASSERT(*null < *i2);
-    TS_ASSERT(*null < *r1);
-    TS_ASSERT(*null < *r2);
-
-    TS_ASSERT(*a < *b);
-    TS_ASSERT(*a < *c);
-    TS_ASSERT(*a < *d);
-    TS_ASSERT(!(*b < *a));
-    TS_ASSERT(!(*c < *a));
-    TS_ASSERT(!(*d < *a));
-
-    TS_ASSERT(*b < *c);
-    TS_ASSERT(*b < *d);
-    TS_ASSERT(!(*c < *b));
-    TS_ASSERT(!(*d < *b));
-
-    TS_ASSERT(*c < *d);
-    TS_ASSERT(!(*d < *c));
-
-    TS_ASSERT(*mult < *c);
-    TS_ASSERT(*mult < *d);
-    TS_ASSERT(*plus < *d);
-    TS_ASSERT(!(*c < *mult));
-    TS_ASSERT(!(*d < *mult));
-    TS_ASSERT(!(*d < *plus));
-
-    TS_ASSERT(!(*null < *null));
-    TS_ASSERT(!(*a < *a));
-    TS_ASSERT(!(*b < *b));
-    TS_ASSERT(!(*c < *c));
-    TS_ASSERT(!(*plus < *plus));
-    TS_ASSERT(!(*mult < *mult));
-    TS_ASSERT(!(*d < *d));
-  }
-
-  void testGetKind() {
-    /* Kind getKind() const; */
-
-    TS_ASSERT(a->getKind() == VARIABLE);
-    TS_ASSERT(b->getKind() == VARIABLE);
-    TS_ASSERT(c->getKind() == MULT);
-    TS_ASSERT(mult->getKind() == BUILTIN);
-    TS_ASSERT(plus->getKind() == BUILTIN);
-    TS_ASSERT(d->getKind() == APPLY_UF);
-    TS_ASSERT(null->getKind() == NULL_EXPR);
-
-    TS_ASSERT(i1->getKind() == CONST_INTEGER);
-    TS_ASSERT(i2->getKind() == CONST_INTEGER);
-    TS_ASSERT(r1->getKind() == CONST_RATIONAL);
-    TS_ASSERT(r2->getKind() == CONST_RATIONAL);
-  }
-
-  void testGetNumChildren() {
-    /* size_t getNumChildren() const; */
-
-    TS_ASSERT(a->getNumChildren() == 0);
-    TS_ASSERT(b->getNumChildren() == 0);
-    TS_ASSERT(c->getNumChildren() == 2);
-    TS_ASSERT(mult->getNumChildren() == 0);
-    TS_ASSERT(plus->getNumChildren() == 0);
-    TS_ASSERT(d->getNumChildren() == 2);
-    TS_ASSERT(null->getNumChildren() == 0);
-
-    TS_ASSERT(i1->getNumChildren() == 0);
-    TS_ASSERT(i2->getNumChildren() == 0);
-    TS_ASSERT(r1->getNumChildren() == 0);
-    TS_ASSERT(r2->getNumChildren() == 0);
-  }
-
-  void testOperatorFunctions() {
-    /* bool hasOperator() const; */
-    /* Expr getOperator() const; */
-
-    TS_ASSERT(!a->hasOperator());
-    TS_ASSERT(!b->hasOperator());
-    TS_ASSERT(c->hasOperator());
-    TS_ASSERT(!mult->hasOperator());
-    TS_ASSERT(!plus->hasOperator());
-    TS_ASSERT(d->hasOperator());
-    TS_ASSERT(!null->hasOperator());
-
-    TS_ASSERT_THROWS(a->getOperator(), IllegalArgumentException);
-    TS_ASSERT_THROWS(b->getOperator(), IllegalArgumentException);
-    TS_ASSERT(c->getOperator() == *mult);
-    TS_ASSERT_THROWS(plus->getOperator(), IllegalArgumentException);
-    TS_ASSERT_THROWS(mult->getOperator(), IllegalArgumentException);
-    TS_ASSERT(d->getOperator() == *plus);
-    TS_ASSERT_THROWS(null->getOperator(), IllegalArgumentException);
-  }
-
-  void testGetType() {
-    /* Type* getType() const; */
-
-    TS_ASSERT(a->getType() == d_em->booleanType());
-    TS_ASSERT(b->getType() == d_em->booleanType());
-    TS_ASSERT(c->getType() == NULL);
-    TS_ASSERT(mult->getType() == NULL);
-    TS_ASSERT(plus->getType() == NULL);
-    TS_ASSERT(d->getType() == NULL);
-#ifdef CVC4_ASSERTIONS
-    TS_ASSERT_THROWS(null->getType(), AssertionException);
-#endif /* CVC4_ASSERTIONS */
-
-    TS_ASSERT(i1->getType() == NULL);
-    TS_ASSERT(i2->getType() == NULL);
-    TS_ASSERT(r1->getType() == NULL);
-    TS_ASSERT(r2->getType() == NULL);
-  }
-
-  void testToString() {
-    /* std::string toString() const; */
-
-    TS_ASSERT(a->toString() == "a");
-    TS_ASSERT(b->toString() == "b");
-    TS_ASSERT(c->toString() == "(MULT a b)");
-    TS_ASSERT(mult->toString() == "(BUILTIN MULT)");
-    TS_ASSERT(plus->toString() == "(BUILTIN PLUS)");
-    TS_ASSERT(d->toString() == "(APPLY_UF (BUILTIN PLUS) b (MULT a b))");
-    TS_ASSERT(null->toString() == "null");
-
-    TS_ASSERT(i1->toString() == "(CONST_INTEGER 0)");
-    TS_ASSERT(i2->toString() == "(CONST_INTEGER 23)");
-    TS_ASSERT(r1->toString() == "(CONST_RATIONAL 1/5)");
-    TS_ASSERT(r2->toString() == "(CONST_RATIONAL 0)");
-  }
-
-  void testToStream() {
-    /* void toStream(std::ostream& out) const; */
-
-    stringstream sa, sb, sc, smult, splus, sd, snull;
-    stringstream si1, si2, sr1, sr2;
-    a->toStream(sa);
-    b->toStream(sb);
-    c->toStream(sc);
-    mult->toStream(smult);
-    plus->toStream(splus);
-    d->toStream(sd);
-    null->toStream(snull);
-
-    i1->toStream(si1);
-    i2->toStream(si2);
-    r1->toStream(sr1);
-    r2->toStream(sr2);
-
-    TS_ASSERT(sa.str() == "a");
-    TS_ASSERT(sb.str() == "b");
-    TS_ASSERT(sc.str() == "(MULT a b)");
-    TS_ASSERT(smult.str() == "(BUILTIN MULT)");
-    TS_ASSERT(splus.str() == "(BUILTIN PLUS)");
-    TS_ASSERT(sd.str() == "(APPLY_UF (BUILTIN PLUS) b (MULT a b))");
-    TS_ASSERT(snull.str() == "null");
-
-    TS_ASSERT(si1.str() == "(CONST_INTEGER 0)");
-    TS_ASSERT(si2.str() == "(CONST_INTEGER 23)");
-    TS_ASSERT(sr1.str() == "(CONST_RATIONAL 1/5)");
-    TS_ASSERT(sr2.str() == "(CONST_RATIONAL 0)");
-  }
-
-  void testIsNull() {
-    /* bool isNull() const; */
-
-    TS_ASSERT(!a->isNull());
-    TS_ASSERT(!b->isNull());
-    TS_ASSERT(!c->isNull());
-    TS_ASSERT(!mult->isNull());
-    TS_ASSERT(!plus->isNull());
-    TS_ASSERT(!d->isNull());
-    TS_ASSERT(null->isNull());
-  }
-
-  void testIsConst() {
-    /* bool isConst() const; */
-
-    TS_ASSERT(!a->isConst());
-    TS_ASSERT(!b->isConst());
-    TS_ASSERT(!c->isConst());
-    TS_ASSERT(mult->isConst());
-    TS_ASSERT(plus->isConst());
-    TS_ASSERT(!d->isConst());
-    TS_ASSERT(!null->isConst());
-  }
-
-  void testIsAtomic() {
-    /* bool isAtomic() const; */
-
-    TS_ASSERT(a->isAtomic());
-    TS_ASSERT(b->isAtomic());
-    TS_ASSERT(c->isAtomic());
-    TS_ASSERT(mult->isAtomic());
-    TS_ASSERT(plus->isAtomic());
-    TS_ASSERT(d->isAtomic());
-#ifdef CVC4_ASSERTIONS
-    TS_ASSERT_THROWS(null->isAtomic(), IllegalArgumentException);
-#endif /* CVC4_ASSERTIONS */
-
-    TS_ASSERT(i1->isAtomic());
-    TS_ASSERT(i2->isAtomic());
-    TS_ASSERT(r1->isAtomic());
-    TS_ASSERT(r2->isAtomic());
-
-    Expr x = d_em->mkExpr(AND, *a, *b);
-    Expr y = d_em->mkExpr(ITE, *a, *b, *c);
-    Expr z = d_em->mkExpr(IFF, x, y);
-
-    TS_ASSERT(!x.isAtomic());
-    TS_ASSERT(!y.isAtomic());
-    TS_ASSERT(!z.isAtomic());
-
-    Expr w1 = d_em->mkExpr(PLUS, d_em->mkExpr(ITE, z, *i1, *i2), *i2);
-    Expr w2 = d_em->mkExpr(PLUS, d_em->mkExpr(MULT, *i1, *i2), *i2);
-
-    TS_ASSERT(!w1.isAtomic());
-    TS_ASSERT(w2.isAtomic());
-  }
-
-  void testGetConst() {
-    /* template <class T>
-       const T& getConst() const; */
-
-    TS_ASSERT_THROWS(a->getConst<Kind>(), IllegalArgumentException);
-    TS_ASSERT_THROWS(b->getConst<Kind>(), IllegalArgumentException);
-    TS_ASSERT_THROWS(c->getConst<Kind>(), IllegalArgumentException);
-    TS_ASSERT(mult->getConst<Kind>() == MULT);
-    TS_ASSERT_THROWS(mult->getConst<Integer>(), IllegalArgumentException);
-    TS_ASSERT(plus->getConst<Kind>() == PLUS);
-    TS_ASSERT_THROWS(plus->getConst<Rational>(), IllegalArgumentException);
-    TS_ASSERT_THROWS(d->getConst<Kind>(), IllegalArgumentException);
-    TS_ASSERT_THROWS(null->getConst<Kind>(), IllegalArgumentException);
-
-    TS_ASSERT(i1->getConst<Integer>() == 0);
-    TS_ASSERT(i2->getConst<Integer>() == 23);
-    TS_ASSERT(r1->getConst<Rational>() == Rational(1, 5));
-    TS_ASSERT(r2->getConst<Rational>() == Rational("0"));
-
-    TS_ASSERT_THROWS(i1->getConst<Kind>(), IllegalArgumentException);
-    TS_ASSERT_THROWS(i2->getConst<Kind>(), IllegalArgumentException);
-    TS_ASSERT_THROWS(r1->getConst<Kind>(), IllegalArgumentException);
-    TS_ASSERT_THROWS(r2->getConst<Kind>(), IllegalArgumentException);
-  }
-
-  void testGetExprManager() {
-    /* ExprManager* getExprManager() const; */
-
-    TS_ASSERT(a->getExprManager() == d_em);
-    TS_ASSERT(b->getExprManager() == d_em);
-    TS_ASSERT(c->getExprManager() == d_em);
-    TS_ASSERT(mult->getExprManager() == d_em);
-    TS_ASSERT(plus->getExprManager() == d_em);
-    TS_ASSERT(d->getExprManager() == d_em);
-    TS_ASSERT(null->getExprManager() == NULL);
-
-    TS_ASSERT(i1->getExprManager() == d_em);
-    TS_ASSERT(i2->getExprManager() == d_em);
-    TS_ASSERT(r1->getExprManager() == d_em);
-    TS_ASSERT(r2->getExprManager() == d_em);
-  }
-};