diff options
Diffstat (limited to 'test/unit/expr/expr_black.h')
-rw-r--r-- | test/unit/expr/expr_black.h | 414 |
1 files changed, 414 insertions, 0 deletions
diff --git a/test/unit/expr/expr_black.h b/test/unit/expr/expr_black.h new file mode 100644 index 000000000..b08b5c6aa --- /dev/null +++ b/test/unit/expr/expr_black.h @@ -0,0 +1,414 @@ +/********************* */ +/** 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(d_em->booleanType(), "a")); + b = new Expr(d_em->mkVar(d_em->booleanType(), "b")); + 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()); + TS_ASSERT(!null->isAtomic()); + + 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(XOR, *a, *b, *c); + Expr z = d_em->mkExpr(IFF, x, y); + + TS_ASSERT(!x.isAtomic()); + TS_ASSERT(!y.isAtomic()); + TS_ASSERT(!z.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); + } +}; |