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#(<td class="coverFn"><a href=".*">)(.*)(</a></td>)#$$_=`c++filt "$$2"`;chomp;print "$$1<xmp>$$_</xmp>$$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,(<td class="coverFn"><a href=".*">)(.*)(</a></td>),$$_=`c++filt "$$2"`;chomp;print "$$1<xmp>$$_</xmp>$$3";,e'
CDList(const CDList<T>& l) :
ContextObj(l),
d_list(NULL),
+ d_callDestructor(l.d_callDestructor),
d_size(l.d_size),
d_sizeAlloc(0) {
}
}
};/* 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 <class Key, class Data, class HashFcn>
- 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
// 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
if(x->d_nchildren == 1) {
Assert(y->d_nchildren == 0);
return compare(y, x);
- return *reinterpret_cast<T*>(x->d_children[0]) == y->getConst<T>();
} else if(y->d_nchildren == 1) {
Assert(x->d_nchildren == 0);
return x->getConst<T>() == *reinterpret_cast<T*>(y->d_children[0]);
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)));
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)));
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)));
# All unit tests
UNIT_TESTS = \
- expr/expr_black \
+ expr/expr_public \
expr/node_white \
expr/node_black \
expr/kind_black \
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
# 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))
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:
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); }
void testCDList99() { listTest(99); }
void listTest(int N) {
- CDList<int> list(d_context);
+ listTest(N, true);
+ listTest(N, false);
+ }
+
+ void listTest(int N, bool callDestructor) {
+ CDList<int> list(d_context, callDestructor);
TS_ASSERT(list.empty());
for(int i = 0; i < N; ++i) {
}
}
- void tearDown() {
- delete d_context;
+ void testDtorCalled() {
+ bool shouldRemainFalse = false;
+ bool shouldFlipToTrue = false;
+ bool alsoFlipToTrue = false;
+ bool shouldAlsoRemainFalse = false;
+ bool aThirdFalse = false;
+
+ CDList<DtorSensitiveObject> listT(d_context, true);
+ CDList<DtorSensitiveObject> 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);
}
};
--- /dev/null
+/********************* */
+/** 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 <cxxtest/TestSuite.h>
+
+#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<int, int> 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);
+ }
+};
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;
+ }
};
+++ /dev/null
-/********************* */
-/** 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);
- }
-};
--- /dev/null
+/********************* */
+/** 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 <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 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 <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);
+ }
+};
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());
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);
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);
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));
}
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());
}
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);
d_euf->check(d_level);
}
-
-
-
};
#include <cxxtest/TestSuite.h>
+#include <string>
+#include <cstring>
+
#include "util/Assert.h"
using namespace CVC4;
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 );
+ }
+
};
--- /dev/null
+/********************* */
+/** 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 <cxxtest/TestSuite.h>
+
+#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();
+ }
+
+};
+++ /dev/null
-/********************* */
-/** 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 <cxxtest/TestSuite.h>
-
-#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();
- }
-
-};
--- /dev/null
+/********************* */
+/** 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 <cxxtest/TestSuite.h>
+
+#include <iostream>
+#include <sstream>
+
+#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!"));
+ }
+};
--- /dev/null
+/********************* */
+/** 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 <cxxtest/TestSuite.h>
+
+#include <iostream>
+#include <sstream>
+
+#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 */
+
+ }
+};
+++ /dev/null
-/********************* */
-/** 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 <cxxtest/TestSuite.h>
-
-#include <iostream>
-#include <sstream>
-
-#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 */
- }
-
-};
projects / cvc5.git / commitdiff