From: Morgan Deters Date: Fri, 9 Apr 2010 16:25:32 +0000 (+0000) Subject: added experimental "make lcov" target (it runs only unit tests); better coverage... X-Git-Tag: cvc5-1.0.0~9121 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e390a4207d3858927354b3d4b40d540c00f8064c;p=cvc5.git 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 --- diff --git a/Makefile.am b/Makefile.am index 5aec4e904..c10bc1263 100644 --- a/Makefile.am +++ b/Makefile.am @@ -11,3 +11,48 @@ SUBDIRS = src test contrib regress0 regress1 regress2 regress3: all (cd test && $(MAKE) $(AM_MAKEFLAGS) $@) || exit 1 +LCOV = lcov +GENHTML = genhtml + +LCOV_EXCLUDES = \ + "$(CXXTEST)/*" \ + "/usr/include/*" \ + "$(abs_top_builddir)/test/*" + +# lcov 1.7 has some bugs that we have to work around (can't do +# baseline measurement, merge between different test-names doesn't +# work...) +.PHONY: lcov +lcov: all + $(LCOV) -z -d . + $(MAKE) check -C test/unit + $(LCOV) -c -d . -t cvc4_units -o cvc4-coverage-full.info + $(LCOV) -o cvc4-coverage.info -r cvc4-coverage-full.info $(LCOV_EXCLUDES) + mkdir -p "@top_srcdir@/html" + $(GENHTML) -o "@top_srcdir@/html" cvc4-coverage.info + @echo "De-mangling C++ symbols..." + @find "@top_srcdir@/html" -name '*.func.html' | \ + xargs perl -pi -e 's#()(.*)()#$$_=`c++filt "$$2"`;chomp;print "$$1$$_$$3\n";#e' + +# when we get a working lcov, we can do better stats for +# modules/test-types; unfortunately lcov 1.8 directory paths +# are broken(?) or at least different than 1.7 +.PHONY: lcov18 +lcov18: all + @for testtype in public black white; do \ + echo; echo "=== Collecting coverage data from $$testtype unit tests ==="; \ + echo $(LCOV) -z -d .; \ + $(LCOV) -z -d . || exit 1; \ + echo $(MAKE) check -C test/unit TEST_SUFFIX=_$$testtype || exit 1; \ + $(MAKE) check -C test/unit TEST_SUFFIX=_$$testtype || exit 1; \ + echo $(LCOV) -c -d . -t $$testtype -o cvc4-coverage-$$testtype-full.info || exit 1; \ + $(LCOV) -c -d . -t $$testtype -o cvc4-coverage-$$testtype-full.info || exit 1; \ + echo $(LCOV) -o cvc4-coverage-$$testtype.info -r cvc4-coverage-$$testtype-full.info $(LCOV_EXCLUDES); \ + $(LCOV) -o cvc4-coverage-$$testtype.info -r cvc4-coverage-$$testtype-full.info $(LCOV_EXCLUDES) || exit 1; \ + echo; \ + done + mkdir -p "@top_srcdir@/html" + $(GENHTML) -o "@top_srcdir@/html" cvc4-coverage-public.info cvc4-coverage-black.info cvc4-coverage-white.info + @echo "De-mangling C++ symbols..." + @find "@top_srcdir@/html" -name '*.func.html' | \ + xargs perl -pi -e 's,()(.*)(),$$_=`c++filt "$$2"`;chomp;print "$$1$$_$$3";,e' diff --git a/src/context/cdlist.h b/src/context/cdlist.h index b0161c562..a2abc08d8 100644 --- a/src/context/cdlist.h +++ b/src/context/cdlist.h @@ -95,6 +95,7 @@ private: CDList(const CDList& l) : ContextObj(l), d_list(NULL), + d_callDestructor(l.d_callDestructor), d_size(l.d_size), d_sizeAlloc(0) { } diff --git a/src/context/cdmap.h b/src/context/cdmap.h index 75f6eb2ae..4621d7fc5 100644 --- a/src/context/cdmap.h +++ b/src/context/cdmap.h @@ -140,24 +140,6 @@ public: } };/* class CDOmap<> */ -// Dummy subclass of ContextObj to serve as our data class -class CDMapData : public ContextObj { - // befriend CDMap<> so that it can allocate us - template - friend class CDMap; - - ContextObj* save(ContextMemoryManager* pCMM) { - return new(pCMM) CDMapData(*this); - } - - void restore(ContextObj* data) {} - -public: - - CDMapData(Context* context) : ContextObj(context) {} - CDMapData(const ContextObj& co) : ContextObj(co) {} - ~CDMapData() throw(AssertionException) { destroy(); } -}; /** * Generic templated class for a map which must be saved and restored @@ -181,11 +163,13 @@ class CDMap : public ContextObj { // Nothing to save; the elements take care of themselves virtual ContextObj* save(ContextMemoryManager* pCMM) { - return new(pCMM) CDMapData(*this); + Unreachable(); } // Similarly, nothing to restore - virtual void restore(ContextObj* data) {} + virtual void restore(ContextObj* data) { + Unreachable(); + } void emptyTrash() { //FIXME multithreading diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h index 96152d075..fda2801be 100644 --- a/src/expr/metakind_template.h +++ b/src/expr/metakind_template.h @@ -199,7 +199,6 @@ inline bool NodeValueConstCompare::compare(const ::CVC4::expr::NodeValu if(x->d_nchildren == 1) { Assert(y->d_nchildren == 0); return compare(y, x); - return *reinterpret_cast(x->d_children[0]) == y->getConst(); } else if(y->d_nchildren == 1) { Assert(x->d_nchildren == 0); return x->getConst() == *reinterpret_cast(y->d_children[0]); diff --git a/src/util/output.h b/src/util/output.h index 6315389e8..79bdd788e 100644 --- a/src/util/output.h +++ b/src/util/output.h @@ -172,8 +172,8 @@ class CVC4_PUBLIC NoticeC { public: NoticeC(std::ostream* os) : d_os(os) {} - void operator()(const char*); - void operator()(std::string); + void operator()(const char* s) { *d_os << s; } + void operator()(std::string s) { *d_os << s; } void printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3))); @@ -193,8 +193,8 @@ class CVC4_PUBLIC ChatC { public: ChatC(std::ostream* os) : d_os(os) {} - void operator()(const char*); - void operator()(std::string); + void operator()(const char* s) { *d_os << s; } + void operator()(std::string s) { *d_os << s; } void printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3))); @@ -215,10 +215,29 @@ class CVC4_PUBLIC TraceC { public: TraceC(std::ostream* os) : d_os(os) {} - void operator()(const char* tag, const char*); - void operator()(const char* tag, std::string); - void operator()(std::string tag, const char*); - void operator()(std::string tag, std::string); + void operator()(const char* tag, const char* s) { + if(!d_tags.empty() && d_tags.find(std::string(tag)) != d_tags.end()) { + *d_os << s; + } + } + + void operator()(const char* tag, const std::string& s) { + if(!d_tags.empty() && d_tags.find(std::string(tag)) != d_tags.end()) { + *d_os << s; + } + } + + void operator()(const std::string& tag, const char* s) { + if(!d_tags.empty() && d_tags.find(tag) != d_tags.end()) { + *d_os << s; + } + } + + void operator()(const std::string& tag, const std::string& s) { + if(!d_tags.empty() && d_tags.find(tag) != d_tags.end()) { + *d_os << s; + } + } void printf(const char* tag, const char* fmt, ...) __attribute__ ((format(printf, 3, 4))); void printf(std::string tag, const char* fmt, ...) __attribute__ ((format(printf, 3, 4))); diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index c52ac5d1c..3f0816560 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -1,6 +1,6 @@ # All unit tests UNIT_TESTS = \ - expr/expr_black \ + expr/expr_public \ expr/node_white \ expr/node_black \ expr/kind_black \ @@ -16,11 +16,13 @@ UNIT_TESTS = \ context/cdo_black \ context/cdlist_black \ context/cdmap_black \ + context/cdmap_white \ theory/theory_black \ theory/theory_uf_white \ util/assert_white \ - util/configuration_white \ - util/output_white \ + util/configuration_black \ + util/output_black \ + util/exception_black \ util/integer_black \ util/integer_white \ util/rational_white diff --git a/test/unit/Makefile.tests b/test/unit/Makefile.tests index 4f2f3dd5f..e3ec536ce 100644 --- a/test/unit/Makefile.tests +++ b/test/unit/Makefile.tests @@ -8,7 +8,7 @@ # It's a pain to make automake happy. # Add "filtered" tests to the set of TESTS -TESTS = $(filter $(TEST_PREFIX)%,$(UNIT_TESTS)) +TESTS = $(filter $(TEST_PREFIX)%,$(filter %$(TEST_SUFFIX),$(UNIT_TESTS))) # subsets of the tests, based on name WHITE_TESTS = $(filter %_white,$(UNIT_TESTS)) diff --git a/test/unit/context/cdlist_black.h b/test/unit/context/cdlist_black.h index f31d5f273..418357630 100644 --- a/test/unit/context/cdlist_black.h +++ b/test/unit/context/cdlist_black.h @@ -23,6 +23,14 @@ using namespace std; using namespace CVC4::context; + +struct DtorSensitiveObject { + bool& d_dtorCalled; + DtorSensitiveObject(bool& dtorCalled) : d_dtorCalled(dtorCalled) {} + ~DtorSensitiveObject() { d_dtorCalled = true; } +}; + + class CDListBlack : public CxxTest::TestSuite { private: @@ -34,6 +42,10 @@ public: d_context = new Context(); } + void tearDown() { + delete d_context; + } + // test at different sizes. this triggers grow() behavior differently. // grow() was completely broken in revision 256 void testCDList10() { listTest(10); } @@ -44,7 +56,12 @@ public: void testCDList99() { listTest(99); } void listTest(int N) { - CDList list(d_context); + listTest(N, true); + listTest(N, false); + } + + void listTest(int N, bool callDestructor) { + CDList list(d_context, callDestructor); TS_ASSERT(list.empty()); for(int i = 0; i < N; ++i) { @@ -66,7 +83,46 @@ public: } } - void tearDown() { - delete d_context; + void testDtorCalled() { + bool shouldRemainFalse = false; + bool shouldFlipToTrue = false; + bool alsoFlipToTrue = false; + bool shouldAlsoRemainFalse = false; + bool aThirdFalse = false; + + CDList listT(d_context, true); + CDList listF(d_context, false); + + DtorSensitiveObject shouldRemainFalseDSO(shouldRemainFalse); + DtorSensitiveObject shouldFlipToTrueDSO(shouldFlipToTrue); + DtorSensitiveObject alsoFlipToTrueDSO(alsoFlipToTrue); + DtorSensitiveObject shouldAlsoRemainFalseDSO(shouldAlsoRemainFalse); + DtorSensitiveObject aThirdFalseDSO(aThirdFalse); + + listT.push_back(shouldAlsoRemainFalseDSO); + listF.push_back(shouldAlsoRemainFalseDSO); + + d_context->push(); + + listT.push_back(shouldFlipToTrueDSO); + listT.push_back(alsoFlipToTrueDSO); + + listF.push_back(shouldRemainFalseDSO); + listF.push_back(shouldAlsoRemainFalseDSO); + listF.push_back(aThirdFalseDSO); + + TS_ASSERT_EQUALS(shouldRemainFalse, false); + TS_ASSERT_EQUALS(shouldFlipToTrue, false); + TS_ASSERT_EQUALS(alsoFlipToTrue, false); + TS_ASSERT_EQUALS(shouldAlsoRemainFalse, false); + TS_ASSERT_EQUALS(aThirdFalse, false); + + d_context->pop(); + + TS_ASSERT_EQUALS(shouldRemainFalse, false); + TS_ASSERT_EQUALS(shouldFlipToTrue, true); + TS_ASSERT_EQUALS(alsoFlipToTrue, true); + TS_ASSERT_EQUALS(shouldAlsoRemainFalse, false); + TS_ASSERT_EQUALS(aThirdFalse, false); } }; diff --git a/test/unit/context/cdmap_white.h b/test/unit/context/cdmap_white.h new file mode 100644 index 000000000..9a920ede8 --- /dev/null +++ b/test/unit/context/cdmap_white.h @@ -0,0 +1,52 @@ +/********************* */ +/** cdmap_white.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. + ** + ** White box testing of CVC4::context::CDMap<>. + **/ + +#include + +#include "context/cdmap.h" +#include "util/Assert.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::context; + +class CDMapWhite : public CxxTest::TestSuite { + + Context* d_context; + +public: + + void setUp() { + d_context = new Context; + } + + void tearDown() { + delete d_context; + } + + void testUnreachableSaveAndRestore() { + CDMap map(d_context); + + TS_ASSERT_THROWS_NOTHING(map.makeCurrent()); + + TS_ASSERT_THROWS(map.update(), UnreachableCodeException); + + TS_ASSERT_THROWS(map.save(d_context->getCMM()), UnreachableCodeException); + TS_ASSERT_THROWS(map.restore(&map), UnreachableCodeException); + + d_context->push(); + TS_ASSERT_THROWS(map.makeCurrent(), UnreachableCodeException); + } +}; diff --git a/test/unit/context/context_black.h b/test/unit/context/context_black.h index 549d99369..37c94aaad 100644 --- a/test/unit/context/context_black.h +++ b/test/unit/context/context_black.h @@ -60,4 +60,55 @@ public: d_context->push(); i = 5; } + + void testPreNotify() { + struct MyContextNotifyObj : ContextNotifyObj { + int nCalls; + + MyContextNotifyObj(Context* context, bool pre) : + ContextNotifyObj(context, pre), + nCalls(0) { + } + + void notify() { + ++nCalls; + } + } a(d_context, true), b(d_context, false); + + { + MyContextNotifyObj c(d_context, true), d(d_context, false); + + TS_ASSERT_EQUALS(a.nCalls, 0); + TS_ASSERT_EQUALS(b.nCalls, 0); + TS_ASSERT_EQUALS(c.nCalls, 0); + TS_ASSERT_EQUALS(d.nCalls, 0); + + d_context->push(); + d_context->push(); + + TS_ASSERT_EQUALS(a.nCalls, 0); + TS_ASSERT_EQUALS(b.nCalls, 0); + TS_ASSERT_EQUALS(c.nCalls, 0); + TS_ASSERT_EQUALS(d.nCalls, 0); + + d_context->pop(); + + TS_ASSERT_EQUALS(a.nCalls, 1); + TS_ASSERT_EQUALS(b.nCalls, 1); + TS_ASSERT_EQUALS(c.nCalls, 1); + TS_ASSERT_EQUALS(d.nCalls, 1); + + d_context->pop(); + + TS_ASSERT_EQUALS(a.nCalls, 2); + TS_ASSERT_EQUALS(b.nCalls, 2); + TS_ASSERT_EQUALS(c.nCalls, 2); + TS_ASSERT_EQUALS(d.nCalls, 2); + } + + // we do this to get full code coverage of destruction paths + delete d_context; + + d_context = NULL; + } }; 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 - -#include -#include - -#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 - const T& getConst() const; */ - - TS_ASSERT_THROWS(a->getConst(), IllegalArgumentException); - TS_ASSERT_THROWS(b->getConst(), IllegalArgumentException); - TS_ASSERT_THROWS(c->getConst(), IllegalArgumentException); - TS_ASSERT(mult->getConst() == MULT); - TS_ASSERT_THROWS(mult->getConst(), IllegalArgumentException); - TS_ASSERT(plus->getConst() == PLUS); - TS_ASSERT_THROWS(plus->getConst(), IllegalArgumentException); - TS_ASSERT_THROWS(d->getConst(), IllegalArgumentException); - TS_ASSERT_THROWS(null->getConst(), IllegalArgumentException); - - TS_ASSERT(i1->getConst() == 0); - TS_ASSERT(i2->getConst() == 23); - TS_ASSERT(r1->getConst() == Rational(1, 5)); - TS_ASSERT(r2->getConst() == Rational("0")); - - TS_ASSERT_THROWS(i1->getConst(), IllegalArgumentException); - TS_ASSERT_THROWS(i2->getConst(), IllegalArgumentException); - TS_ASSERT_THROWS(r1->getConst(), IllegalArgumentException); - TS_ASSERT_THROWS(r2->getConst(), 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); - } -}; diff --git a/test/unit/expr/expr_public.h b/test/unit/expr/expr_public.h new file mode 100644 index 000000000..fd36a7cfa --- /dev/null +++ b/test/unit/expr/expr_public.h @@ -0,0 +1,422 @@ +/********************* */ +/** expr_public.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. + ** + ** Public black-box testing of CVC4::Expr. + **/ + +#include + +#include +#include + +#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 ExprPublic : 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 + const T& getConst() const; */ + + TS_ASSERT_THROWS(a->getConst(), IllegalArgumentException); + TS_ASSERT_THROWS(b->getConst(), IllegalArgumentException); + TS_ASSERT_THROWS(c->getConst(), IllegalArgumentException); + TS_ASSERT(mult->getConst() == MULT); + TS_ASSERT_THROWS(mult->getConst(), IllegalArgumentException); + TS_ASSERT(plus->getConst() == PLUS); + TS_ASSERT_THROWS(plus->getConst(), IllegalArgumentException); + TS_ASSERT_THROWS(d->getConst(), IllegalArgumentException); + TS_ASSERT_THROWS(null->getConst(), IllegalArgumentException); + + TS_ASSERT(i1->getConst() == 0); + TS_ASSERT(i2->getConst() == 23); + TS_ASSERT(r1->getConst() == Rational(1, 5)); + TS_ASSERT(r2->getConst() == Rational("0")); + + TS_ASSERT_THROWS(i1->getConst(), IllegalArgumentException); + TS_ASSERT_THROWS(i2->getConst(), IllegalArgumentException); + TS_ASSERT_THROWS(r1->getConst(), IllegalArgumentException); + TS_ASSERT_THROWS(r2->getConst(), 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); + } +}; diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h index 24c8e407c..097724d48 100644 --- a/test/unit/theory/theory_black.h +++ b/test/unit/theory/theory_black.h @@ -243,7 +243,7 @@ public: TS_ASSERT_EQUALS(got, x_eq_f_f_x); - TS_ASSERT_EQUALS(7, d_dummy->d_registered.size()); + TS_ASSERT_EQUALS(7u, d_dummy->d_registered.size()); TS_ASSERT(d_dummy->d_registered.find(f_f_x) != d_dummy->d_registered.end()); TS_ASSERT(d_dummy->d_registered.find(x_eq_f_f_x) != d_dummy->d_registered.end()); diff --git a/test/unit/theory/theory_uf_white.h b/test/unit/theory/theory_uf_white.h index c02214a25..f5da06a0b 100644 --- a/test/unit/theory/theory_uf_white.h +++ b/test/unit/theory/theory_uf_white.h @@ -154,13 +154,13 @@ public: d_euf->check(d_level); //Test that no additional calls to the output channel occurred. - TS_ASSERT_EQUALS(1, d_outputChannel.getNumCalls()); + TS_ASSERT_EQUALS(1u, d_outputChannel.getNumCalls()); d_euf->assertFact( f5_x_eq_x ); d_euf->check(d_level); - TS_ASSERT_EQUALS(2, d_outputChannel.getNumCalls()); + TS_ASSERT_EQUALS(2u, d_outputChannel.getNumCalls()); TS_ASSERT_EQUALS(CONFLICT, d_outputChannel.getIthCallType(0)); TS_ASSERT_EQUALS(CONFLICT, d_outputChannel.getIthCallType(1)); Node firstConflict = d_outputChannel.getIthNode(0); @@ -189,7 +189,7 @@ public: d_euf->assertFact(f_f_f_x_neq_f_x); d_euf->check(d_level); - TS_ASSERT_EQUALS(1, d_outputChannel.getNumCalls()); + TS_ASSERT_EQUALS(1u, d_outputChannel.getNumCalls()); TS_ASSERT_EQUALS(CONFLICT, d_outputChannel.getIthCallType(0)); Node realConflict = d_outputChannel.getIthNode(0); @@ -205,7 +205,7 @@ public: d_euf->assertFact(x_neq_x); d_euf->check(d_level); - TS_ASSERT_EQUALS(1, d_outputChannel.getNumCalls()); + TS_ASSERT_EQUALS(1u, d_outputChannel.getNumCalls()); TS_ASSERT_EQUALS(x_neq_x, d_outputChannel.getIthNode(0)); TS_ASSERT_EQUALS(CONFLICT, d_outputChannel.getIthCallType(0)); } @@ -218,7 +218,7 @@ public: d_euf->assertFact(x_eq_x); d_euf->check(d_level); - TS_ASSERT_EQUALS(0, d_outputChannel.getNumCalls()); + TS_ASSERT_EQUALS(0u, d_outputChannel.getNumCalls()); } @@ -251,7 +251,7 @@ public: d_euf->assertFact( f1_x_neq_x ); d_euf->check(d_level); - TS_ASSERT_EQUALS(1, d_outputChannel.getNumCalls()); + TS_ASSERT_EQUALS(1u, d_outputChannel.getNumCalls()); TS_ASSERT_EQUALS(CONFLICT, d_outputChannel.getIthCallType(0)); Node realConflict = d_outputChannel.getIthNode(0); TS_ASSERT_EQUALS(expectedConflict, realConflict); @@ -282,7 +282,4 @@ public: d_euf->check(d_level); } - - - }; diff --git a/test/unit/util/assert_white.h b/test/unit/util/assert_white.h index 9425daa44..d001c5a84 100644 --- a/test/unit/util/assert_white.h +++ b/test/unit/util/assert_white.h @@ -15,6 +15,9 @@ #include +#include +#include + #include "util/Assert.h" using namespace CVC4; @@ -39,9 +42,44 @@ public: TS_ASSERT_THROWS( Unimplemented(), UnimplementedOperationException ); TS_ASSERT_THROWS( IllegalArgument("x"), IllegalArgumentException ); TS_ASSERT_THROWS( CheckArgument(false, "x"), IllegalArgumentException ); - TS_ASSERT_THROWS( AlwaysAssertArgument(false, "x"), IllegalArgumentException ); + TS_ASSERT_THROWS( AlwaysAssertArgument(false, "x"), + IllegalArgumentException ); TS_ASSERT_THROWS_NOTHING( AssertArgument(true, "x") ); TS_ASSERT_THROWS_NOTHING( AssertArgument(true, "x") ); } + void testReallyLongAssert() { + string msg(1034, 'x'); + try { + AlwaysAssert(false, msg.c_str()); + TS_FAIL("Should have thrown an exception !"); + } catch(AssertionException& e) { + // we don't want to match on the entire string, because it may + // have an absolute path to the unit test binary, line number + // info, etc. + const char* theString = e.toString().c_str(); + const char* firstPart = + "Assertion failure\nvoid AssertWhite::testReallyLongAssert()\n"; + string lastPartStr = "\n\n false\n" + msg; + const char* lastPart = lastPartStr.c_str(); + TS_ASSERT(strncmp(theString, firstPart, strlen(firstPart)) == 0); + TS_ASSERT(strncmp(theString + strlen(theString) - strlen(lastPart), + lastPart, strlen(lastPart)) == 0); + } catch(...) { + TS_FAIL("Threw the wrong kind of exception !"); + } + } + + void testUnreachable() { + TS_ASSERT_THROWS( Unreachable(), UnreachableCodeException ); + TS_ASSERT_THROWS( Unreachable("hello"), UnreachableCodeException ); + TS_ASSERT_THROWS( Unreachable("hello %s", "world"), UnreachableCodeException ); + + int x = 5; + TS_ASSERT_THROWS( Unhandled(), UnhandledCaseException ); + TS_ASSERT_THROWS( Unhandled(x), UnhandledCaseException ); + TS_ASSERT_THROWS( Unhandled("foo"), UnhandledCaseException ); + TS_ASSERT_THROWS( Unhandled("foo %s baz", "bar"), UnhandledCaseException ); + } + }; diff --git a/test/unit/util/configuration_black.h b/test/unit/util/configuration_black.h new file mode 100644 index 000000000..5ee4cf095 --- /dev/null +++ b/test/unit/util/configuration_black.h @@ -0,0 +1,95 @@ +/********************* */ +/** configuration_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::Configuration. + **/ + +#include + +#include "util/configuration.h" + +using namespace CVC4; +using namespace std; + +class ConfigurationBlack : public CxxTest::TestSuite { + +public: + + void testStaticFlags() { + const bool debug = +#ifdef CVC4_DEBUG + true; +#else /* CVC4_DEBUG */ + false; +#endif /* CVC4_DEBUG */ + + const bool tracing = +#ifdef CVC4_TRACING + true; +#else /* CVC4_TRACING */ + false; +#endif /* CVC4_TRACING */ + + const bool muzzled = +#ifdef CVC4_MUZZLE + true; +#else /* CVC4_MUZZLE */ + false; +#endif /* CVC4_MUZZLE */ + + const bool assertions = +#ifdef CVC4_ASSERTIONS + true; +#else /* CVC4_ASSERTIONS */ + false; +#endif /* CVC4_ASSERTIONS */ + + const bool coverage = +#ifdef CVC4_COVERAGE + true; +#else /* CVC4_COVERAGE */ + false; +#endif /* CVC4_COVERAGE */ + + const bool profiling = +#ifdef CVC4_PROFILING + true; +#else /* CVC4_PROFILING */ + false; +#endif /* CVC4_PROFILING */ + + TS_ASSERT( Configuration::isDebugBuild() == debug ); + TS_ASSERT( Configuration::isTracingBuild() == tracing ); + TS_ASSERT( Configuration::isMuzzledBuild() == muzzled ); + TS_ASSERT( Configuration::isAssertionBuild() == assertions ); + TS_ASSERT( Configuration::isCoverageBuild() == coverage ); + TS_ASSERT( Configuration::isProfilingBuild() == profiling ); + } + + void testPackageName() { + TS_ASSERT( Configuration::getPackageName() == "cvc4" ); + } + + void testVersions() { + // just test that the functions exist + Configuration::getVersionString(); + Configuration::getVersionMajor(); + Configuration::getVersionMinor(); + Configuration::getVersionRelease(); + } + + void testAbout() { + // just test that the function exists + Configuration::about(); + } + +}; diff --git a/test/unit/util/configuration_white.h b/test/unit/util/configuration_white.h deleted file mode 100644 index 04cacc155..000000000 --- a/test/unit/util/configuration_white.h +++ /dev/null @@ -1,95 +0,0 @@ -/********************* */ -/** configuration_white.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. - ** - ** White box testing of CVC4::Configuration. - **/ - -#include - -#include "util/configuration.h" - -using namespace CVC4; -using namespace std; - -class ConfigurationWhite : public CxxTest::TestSuite { - -public: - - void testStaticFlags() { - const bool debug = -#ifdef CVC4_DEBUG - true; -#else /* CVC4_DEBUG */ - false; -#endif /* CVC4_DEBUG */ - - const bool tracing = -#ifdef CVC4_TRACING - true; -#else /* CVC4_TRACING */ - false; -#endif /* CVC4_TRACING */ - - const bool muzzled = -#ifdef CVC4_MUZZLE - true; -#else /* CVC4_MUZZLE */ - false; -#endif /* CVC4_MUZZLE */ - - const bool assertions = -#ifdef CVC4_ASSERTIONS - true; -#else /* CVC4_ASSERTIONS */ - false; -#endif /* CVC4_ASSERTIONS */ - - const bool coverage = -#ifdef CVC4_COVERAGE - true; -#else /* CVC4_COVERAGE */ - false; -#endif /* CVC4_COVERAGE */ - - const bool profiling = -#ifdef CVC4_PROFILING - true; -#else /* CVC4_PROFILING */ - false; -#endif /* CVC4_PROFILING */ - - TS_ASSERT( Configuration::isDebugBuild() == debug ); - TS_ASSERT( Configuration::isTracingBuild() == tracing ); - TS_ASSERT( Configuration::isMuzzledBuild() == muzzled ); - TS_ASSERT( Configuration::isAssertionBuild() == assertions ); - TS_ASSERT( Configuration::isCoverageBuild() == coverage ); - TS_ASSERT( Configuration::isProfilingBuild() == profiling ); - } - - void testPackageName() { - TS_ASSERT( Configuration::getPackageName() == "cvc4" ); - } - - void testVersions() { - // just test that the functions exist - Configuration::getVersionString(); - Configuration::getVersionMajor(); - Configuration::getVersionMinor(); - Configuration::getVersionRelease(); - } - - void testAbout() { - // just test that the function exists - Configuration::about(); - } - -}; diff --git a/test/unit/util/exception_black.h b/test/unit/util/exception_black.h new file mode 100644 index 000000000..758a12645 --- /dev/null +++ b/test/unit/util/exception_black.h @@ -0,0 +1,58 @@ +/********************* */ +/** exception_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::Exception. + **/ + +#include + +#include +#include + +#include "util/exception.h" + +using namespace CVC4; +using namespace std; + +class ExceptionBlack : public CxxTest::TestSuite { +public: + + void setUp() { + } + + void tearDown() { + } + + // CVC4::Exception is a simple class, just test it all at once. + void testExceptions() { + Exception e1; + Exception e2(string("foo!")); + Exception e3("bar!"); + + TS_ASSERT_EQUALS(e1.toString(), string("Unknown exception")); + TS_ASSERT_EQUALS(e2.toString(), string("foo!")); + TS_ASSERT_EQUALS(e3.toString(), string("bar!")); + + e1.setMessage("blah"); + e2.setMessage("another"); + e3.setMessage("three of 'em!"); + + stringstream s1, s2, s3; + s1 << e1; + s2 << e2; + s3 << e3; + + TS_ASSERT_EQUALS(s1.str(), string("blah")); + TS_ASSERT_EQUALS(s2.str(), string("another")); + TS_ASSERT_EQUALS(s3.str(), string("three of 'em!")); + } +}; diff --git a/test/unit/util/output_black.h b/test/unit/util/output_black.h new file mode 100644 index 000000000..6e613e9f4 --- /dev/null +++ b/test/unit/util/output_black.h @@ -0,0 +1,304 @@ +/********************* */ +/** output_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 output classes. + **/ + +#include + +#include +#include + +#include "util/output.h" + +using namespace CVC4; +using namespace std; + +class OutputBlack : public CxxTest::TestSuite { + + stringstream d_debugStream; + stringstream d_traceStream; + stringstream d_noticeStream; + stringstream d_chatStream; + stringstream d_messageStream; + stringstream d_warningStream; + +public: + + void setUp() { + Debug.setStream(d_debugStream); + Trace.setStream(d_traceStream); + Notice.setStream(d_noticeStream); + Chat.setStream(d_chatStream); + Message.setStream(d_messageStream); + Warning.setStream(d_warningStream); + + d_debugStream.str(""); + d_traceStream.str(""); + d_noticeStream.str(""); + d_chatStream.str(""); + d_messageStream.str(""); + d_warningStream.str(""); + } + + void tearDown() { + } + + void testOutput() { + Debug.on("foo"); + Debug("foo") << "testing1"; + Debug.off("foo"); + Debug("foo") << "testing2"; + Debug.on("foo"); + Debug("foo") << "testing3"; + + Message() << "a message"; + Warning() << "bad warning!"; + Chat() << "chatty"; + Notice() << "note"; + + Trace.on("foo"); + Trace("foo") << "tracing1"; + Trace.off("foo"); + Trace("foo") << "tracing2"; + Trace.on("foo"); + Trace("foo") << "tracing3"; + +#ifdef CVC4_MUZZLE + + TS_ASSERT( d_debugStream.str() == "" ); + TS_ASSERT( d_messageStream.str() == "" ); + TS_ASSERT( d_warningStream.str() == "" ); + TS_ASSERT( d_chatStream.str() == "" ); + TS_ASSERT( d_noticeStream.str() == "" ); + TS_ASSERT( d_traceStream.str() == "" ); + +#else /* CVC4_MUZZLE */ + +# ifdef CVC4_DEBUG + TS_ASSERT( d_debugStream.str() == "testing1testing3" ); +# else /* CVC4_DEBUG */ + TS_ASSERT( d_debugStream.str() == "" ); +# endif /* CVC4_DEBUG */ + + TS_ASSERT( d_messageStream.str() == "a message" ); + TS_ASSERT( d_warningStream.str() == "bad warning!" ); + TS_ASSERT( d_chatStream.str() == "chatty" ); + TS_ASSERT( d_noticeStream.str() == "note" ); + +# ifdef CVC4_TRACING + TS_ASSERT( d_traceStream.str() == "tracing1tracing3" ); +# else /* CVC4_TRACING */ + TS_ASSERT( d_traceStream.str() == "" ); +# endif /* CVC4_TRACING */ + +#endif /* CVC4_MUZZLE */ + } + + void testPrintf() { + +#ifdef CVC4_MUZZLE + + Debug.off("yo"); + Debug.printf("yo", "hello %s", "world"); + TS_ASSERT_EQUALS(d_debugStream.str(), string()); + d_debugStream.str(""); + Debug.printf(string("yo"), "hello %s", "world"); + TS_ASSERT_EQUALS(d_debugStream.str(), string()); + d_debugStream.str(""); + + Debug.on("yo"); + Debug.printf("yo", "hello %s", "world"); + TS_ASSERT_EQUALS(d_debugStream.str(), string()); + d_debugStream.str(""); + Debug.printf(string("yo"), "hello %s", "world"); + TS_ASSERT_EQUALS(d_debugStream.str(), string()); + d_debugStream.str(""); + + Trace.off("yo"); + Trace.printf("yo", "hello %s", "world"); + TS_ASSERT_EQUALS(d_traceStream.str(), string()); + d_traceStream.str(""); + Trace.printf(string("yo"), "hello %s", "world"); + TS_ASSERT_EQUALS(d_traceStream.str(), string()); + d_traceStream.str(""); + + Trace.on("yo"); + Trace.printf("yo", "hello %s", "world"); + TS_ASSERT_EQUALS(d_traceStream.str(), string()); + d_traceStream.str(""); + Trace.printf(string("yo"), "hello %s", "world"); + TS_ASSERT_EQUALS(d_traceStream.str(), string()); + + Warning.printf("hello %s", "world"); + TS_ASSERT_EQUALS(d_warningStream.str(), string()); + + Chat.printf("hello %s", "world"); + TS_ASSERT_EQUALS(d_chatStream.str(), string()); + + Message.printf("hello %s", "world"); + TS_ASSERT_EQUALS(d_messageStream.str(), string()); + + Notice.printf("hello %s", "world"); + TS_ASSERT_EQUALS(d_noticeStream.str(), string()); + +#else /* CVC4_MUZZLE */ + + Debug.off("yo"); + Debug.printf("yo", "hello %s", "world"); + TS_ASSERT_EQUALS(d_debugStream.str(), string()); + d_debugStream.str(""); + Debug.printf(string("yo"), "hello %s", "world"); + TS_ASSERT_EQUALS(d_debugStream.str(), string()); + d_debugStream.str(""); + + Debug.on("yo"); + Debug.printf("yo", "hello %s", "world"); +#ifdef CVC4_DEBUG + TS_ASSERT_EQUALS(d_debugStream.str(), string("hello world")); +#else /* CVC4_DEBUG */ + TS_ASSERT_EQUALS(d_debugStream.str(), string()); +#endif /* CVC4_DEBUG */ + d_debugStream.str(""); + Debug.printf(string("yo"), "hello %s", "world"); +#ifdef CVC4_DEBUG + TS_ASSERT_EQUALS(d_debugStream.str(), string("hello world")); +#else /* CVC4_DEBUG */ + TS_ASSERT_EQUALS(d_debugStream.str(), string()); +#endif /* CVC4_DEBUG */ + d_debugStream.str(""); + + Trace.off("yo"); + Trace.printf("yo", "hello %s", "world"); + TS_ASSERT_EQUALS(d_traceStream.str(), string()); + d_traceStream.str(""); + Trace.printf(string("yo"), "hello %s", "world"); + TS_ASSERT_EQUALS(d_traceStream.str(), string()); + d_traceStream.str(""); + + Trace.on("yo"); + Trace.printf("yo", "hello %s", "world"); +#ifdef CVC4_TRACING + TS_ASSERT_EQUALS(d_traceStream.str(), string("hello world")); +#else /* CVC4_TRACING */ + TS_ASSERT_EQUALS(d_traceStream.str(), string()); +#endif /* CVC4_TRACING */ + d_traceStream.str(""); + Trace.printf(string("yo"), "hello %s", "world"); +#ifdef CVC4_TRACING + TS_ASSERT_EQUALS(d_traceStream.str(), string("hello world")); +#else /* CVC4_TRACING */ + TS_ASSERT_EQUALS(d_traceStream.str(), string()); +#endif /* CVC4_TRACING */ + + Warning.printf("hello %s", "world"); + TS_ASSERT_EQUALS(d_warningStream.str(), string("hello world")); + + Chat.printf("hello %s", "world"); + TS_ASSERT_EQUALS(d_chatStream.str(), string("hello world")); + + Message.printf("hello %s", "world"); + TS_ASSERT_EQUALS(d_messageStream.str(), string("hello world")); + + Notice.printf("hello %s", "world"); + TS_ASSERT_EQUALS(d_noticeStream.str(), string("hello world")); + +#endif /* CVC4_MUZZLE */ + + } + + void testSimplePrint() { + +#ifdef CVC4_MUZZLE + + Debug.off("yo"); + Debug("yo", "foobar"); + TS_ASSERT_EQUALS(d_debugStream.str(), string()); + d_debugStream.str(""); + Debug.on("yo"); + Debug("yo", "baz foo"); + TS_ASSERT_EQUALS(d_debugStream.str(), string()); + d_debugStream.str(""); + + Trace.off("yo"); + Trace("yo", "foobar"); + TS_ASSERT_EQUALS(d_traceStream.str(), string()); + d_traceStream.str(""); + Trace.on("yo"); + Trace("yo", "baz foo"); + TS_ASSERT_EQUALS(d_traceStream.str(), string()); + d_traceStream.str(""); + + Warning("baz foo"); + TS_ASSERT_EQUALS(d_warningStream.str(), string()); + d_warningStream.str(""); + + Chat("baz foo"); + TS_ASSERT_EQUALS(d_chatStream.str(), string()); + d_chatStream.str(""); + + Message("baz foo"); + TS_ASSERT_EQUALS(d_messageStream.str(), string()); + d_messageStream.str(""); + + Notice("baz foo"); + TS_ASSERT_EQUALS(d_noticeStream.str(), string()); + d_noticeStream.str(""); + +#else /* CVC4_MUZZLE */ + + Debug.off("yo"); + Debug("yo", "foobar"); + TS_ASSERT_EQUALS(d_debugStream.str(), string()); + d_debugStream.str(""); + Debug.on("yo"); + Debug("yo", "baz foo"); +# ifdef CVC4_DEBUG + TS_ASSERT_EQUALS(d_debugStream.str(), string("baz foo")); +# else /* CVC4_DEBUG */ + TS_ASSERT_EQUALS(d_debugStream.str(), string()); +# endif /* CVC4_DEBUG */ + d_debugStream.str(""); + + Trace.off("yo"); + Trace("yo", "foobar"); + TS_ASSERT_EQUALS(d_traceStream.str(), string()); + d_traceStream.str(""); + Trace.on("yo"); + Trace("yo", "baz foo"); +# ifdef CVC4_TRACING + TS_ASSERT_EQUALS(d_traceStream.str(), string("baz foo")); +# else /* CVC4_TRACING */ + TS_ASSERT_EQUALS(d_traceStream.str(), string()); +# endif /* CVC4_TRACING */ + d_traceStream.str(""); + + Warning("baz foo"); + TS_ASSERT_EQUALS(d_warningStream.str(), string("baz foo")); + d_warningStream.str(""); + + Chat("baz foo"); + TS_ASSERT_EQUALS(d_chatStream.str(), string("baz foo")); + d_chatStream.str(""); + + Message("baz foo"); + TS_ASSERT_EQUALS(d_messageStream.str(), string("baz foo")); + d_messageStream.str(""); + + Notice("baz foo"); + TS_ASSERT_EQUALS(d_noticeStream.str(), string("baz foo")); + d_noticeStream.str(""); + +#endif /* CVC4_MUZZLE */ + + } +}; diff --git a/test/unit/util/output_white.h b/test/unit/util/output_white.h deleted file mode 100644 index 7eda3db9d..000000000 --- a/test/unit/util/output_white.h +++ /dev/null @@ -1,97 +0,0 @@ -/********************* */ -/** output_white.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. - ** - ** White box testing of CVC4::Configuration. - **/ - -#include - -#include -#include - -#include "util/output.h" - -using namespace CVC4; -using namespace std; - -class OutputWhite : public CxxTest::TestSuite { - - stringstream d_debugStream; - stringstream d_traceStream; - stringstream d_noticeStream; - stringstream d_chatStream; - stringstream d_messageStream; - stringstream d_warningStream; - -public: - - void setUp() { - Debug.setStream(d_debugStream); - Trace.setStream(d_traceStream); - Notice.setStream(d_noticeStream); - Chat.setStream(d_chatStream); - Message.setStream(d_messageStream); - Warning.setStream(d_warningStream); - } - - void testOutput() { - Debug.on("foo"); - Debug("foo") << "testing1"; - Debug.off("foo"); - Debug("foo") << "testing2"; - Debug.on("foo"); - Debug("foo") << "testing3"; - - Message() << "a message"; - Warning() << "bad warning!"; - Chat() << "chatty"; - Notice() << "note"; - - Trace.on("foo"); - Trace("foo") << "tracing1"; - Trace.off("foo"); - Trace("foo") << "tracing2"; - Trace.on("foo"); - Trace("foo") << "tracing3"; - -#ifdef CVC4_MUZZLE - - TS_ASSERT( d_debugStream.str() == "" ); - TS_ASSERT( d_messageStream.str() == "" ); - TS_ASSERT( d_warningStream.str() == "" ); - TS_ASSERT( d_chatStream.str() == "" ); - TS_ASSERT( d_noticeStream.str() == "" ); - TS_ASSERT( d_traceStream.str() == "" ); - -#else /* CVC4_MUZZLE */ - -# ifdef CVC4_DEBUG - TS_ASSERT( d_debugStream.str() == "testing1testing3" ); -# else /* CVC4_DEBUG */ - TS_ASSERT( d_debugStream.str() == "" ); -# endif /* CVC4_DEBUG */ - - TS_ASSERT( d_messageStream.str() == "a message" ); - TS_ASSERT( d_warningStream.str() == "bad warning!" ); - TS_ASSERT( d_chatStream.str() == "chatty" ); - TS_ASSERT( d_noticeStream.str() == "note" ); - -# ifdef CVC4_TRACING - TS_ASSERT( d_traceStream.str() == "tracing1tracing3" ); -# else /* CVC4_TRACING */ - TS_ASSERT( d_traceStream.str() == "" ); -# endif /* CVC4_TRACING */ - -#endif /* CVC4_MUZZLE */ - } - -};