diff options
Diffstat (limited to 'test/unit')
-rw-r--r-- | test/unit/Makefile.am | 1 | ||||
-rw-r--r-- | test/unit/context/cdmap_black.h | 2 | ||||
-rw-r--r-- | test/unit/context/context_white.h | 186 | ||||
-rw-r--r-- | test/unit/expr/attribute_white.h | 91 | ||||
-rw-r--r-- | test/unit/expr/expr_black.h | 10 | ||||
-rw-r--r-- | test/unit/expr/node_builder_black.h | 30 | ||||
-rw-r--r-- | test/unit/theory/theory_black.h | 4 |
7 files changed, 288 insertions, 36 deletions
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index 768a56a9b..451100b59 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -10,6 +10,7 @@ UNIT_TESTS = \ expr/attribute_black \ parser/parser_white \ context/context_black \ + context/context_white \ context/context_mm_black \ context/cdo_black \ context/cdlist_black \ diff --git a/test/unit/context/cdmap_black.h b/test/unit/context/cdmap_black.h index 7040e4cc1..262c66fe5 100644 --- a/test/unit/context/cdmap_black.h +++ b/test/unit/context/cdmap_black.h @@ -30,6 +30,8 @@ public: void setUp() { d_context = new Context; //Debug.on("cdmap"); + //Debug.on("gc"); + //Debug.on("pushpop"); } void tearDown() { diff --git a/test/unit/context/context_white.h b/test/unit/context/context_white.h new file mode 100644 index 000000000..3e0928baf --- /dev/null +++ b/test/unit/context/context_white.h @@ -0,0 +1,186 @@ +/********************* */ +/** context_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::Context. + **/ + +#include <cxxtest/TestSuite.h> + +#include "context/context.h" +#include "context/cdo.h" +#include "util/Assert.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::context; + +class ContextWhite : public CxxTest::TestSuite { +private: + + Context* d_context; + +public: + + void setUp() { + d_context = new Context; + } + + void tearDown() { + delete d_context; + } + + void testContextSimple() { + Scope *s = d_context->getTopScope(); + + TS_ASSERT(s == d_context->getBottomScope()); + TS_ASSERT(d_context->getLevel() == 0); + TS_ASSERT(d_context->d_scopeList.size() == 1); + + TS_ASSERT(s->d_pContext == d_context); + TS_ASSERT(s->d_pCMM == d_context->d_pCMM); + TS_ASSERT(s->d_level == 0); + TS_ASSERT(s->d_pContextObjList == NULL); + + CDO<int> a(d_context); + + TS_ASSERT(s->d_pContext == d_context); + TS_ASSERT(s->d_pCMM == d_context->d_pCMM); + TS_ASSERT(s->d_level == 0); + TS_ASSERT(s->d_pContextObjList == &a); + + TS_ASSERT(a.d_pScope == s); + TS_ASSERT(a.d_pContextObjRestore == NULL); + TS_ASSERT(a.d_pContextObjNext == NULL); + TS_ASSERT(a.d_ppContextObjPrev == &s->d_pContextObjList); + + CDO<int> b(d_context); + + TS_ASSERT(s->d_pContext == d_context); + TS_ASSERT(s->d_pCMM == d_context->d_pCMM); + TS_ASSERT(s->d_level == 0); + TS_ASSERT(s->d_pContextObjList == &b); + + TS_ASSERT(a.d_pScope == s); + TS_ASSERT(a.d_pContextObjRestore == NULL); + TS_ASSERT(a.d_pContextObjNext == NULL); + TS_ASSERT(a.d_ppContextObjPrev == &b.d_pContextObjNext); + + TS_ASSERT(b.d_pScope == s); + TS_ASSERT(b.d_pContextObjRestore == NULL); + TS_ASSERT(b.d_pContextObjNext == &a); + TS_ASSERT(b.d_ppContextObjPrev == &s->d_pContextObjList); + + d_context->push(); + Scope* t = d_context->getTopScope(); + TS_ASSERT(s != t); + + TS_ASSERT(s == d_context->getBottomScope()); + TS_ASSERT(d_context->getLevel() == 1); + TS_ASSERT(d_context->d_scopeList.size() == 2); + + TS_ASSERT(s->d_pContext == d_context); + TS_ASSERT(s->d_pCMM == d_context->d_pCMM); + TS_ASSERT(s->d_level == 0); + TS_ASSERT(s->d_pContextObjList == &b); + + TS_ASSERT(t->d_pContext == d_context); + TS_ASSERT(t->d_pCMM == d_context->d_pCMM); + TS_ASSERT(t->d_level == 1); + TS_ASSERT(t->d_pContextObjList == NULL); + + TS_ASSERT(a.d_pScope == s); + TS_ASSERT(a.d_pContextObjRestore == NULL); + TS_ASSERT(a.d_pContextObjNext == NULL); + TS_ASSERT(a.d_ppContextObjPrev == &b.d_pContextObjNext); + + TS_ASSERT(b.d_pScope == s); + TS_ASSERT(b.d_pContextObjRestore == NULL); + TS_ASSERT(b.d_pContextObjNext == &a); + TS_ASSERT(b.d_ppContextObjPrev == &s->d_pContextObjList); + + a = 5; + + TS_ASSERT(t->d_pContext == d_context); + TS_ASSERT(t->d_pCMM == d_context->d_pCMM); + TS_ASSERT(t->d_level == 1); + TS_ASSERT(t->d_pContextObjList == &a); + + TS_ASSERT(a.d_pScope == t); + TS_ASSERT(a.d_pContextObjRestore != NULL); + TS_ASSERT(a.d_pContextObjNext == NULL); + TS_ASSERT(a.d_ppContextObjPrev == &t->d_pContextObjList); + + b = 3; + + TS_ASSERT(t->d_pContext == d_context); + TS_ASSERT(t->d_pCMM == d_context->d_pCMM); + TS_ASSERT(t->d_level == 1); + TS_ASSERT(t->d_pContextObjList == &b); + + TS_ASSERT(a.d_pScope == t); + TS_ASSERT(a.d_pContextObjRestore != NULL); + TS_ASSERT(a.d_pContextObjNext == NULL); + TS_ASSERT(a.d_ppContextObjPrev == &b.d_pContextObjNext); + + TS_ASSERT(b.d_pScope == t); + TS_ASSERT(b.d_pContextObjRestore != NULL); + TS_ASSERT(b.d_pContextObjNext == &a); + TS_ASSERT(b.d_ppContextObjPrev == &t->d_pContextObjList); + + d_context->push(); + Scope* u = d_context->getTopScope(); + TS_ASSERT(u != t); + TS_ASSERT(u != s); + + CDO<int> c(d_context); + c = 4; + + TS_ASSERT(c.d_pScope == u); + TS_ASSERT(c.d_pContextObjRestore != NULL); + TS_ASSERT(c.d_pContextObjNext == NULL); + TS_ASSERT(c.d_ppContextObjPrev == &u->d_pContextObjList); + + d_context->pop(); + + TS_ASSERT(t->d_pContext == d_context); + TS_ASSERT(t->d_pCMM == d_context->d_pCMM); + TS_ASSERT(t->d_level == 1); + TS_ASSERT(t->d_pContextObjList == &b); + + TS_ASSERT(a.d_pScope == t); + TS_ASSERT(a.d_pContextObjRestore != NULL); + TS_ASSERT(a.d_pContextObjNext == NULL); + TS_ASSERT(a.d_ppContextObjPrev == &b.d_pContextObjNext); + + TS_ASSERT(b.d_pScope == t); + TS_ASSERT(b.d_pContextObjRestore != NULL); + TS_ASSERT(b.d_pContextObjNext == &a); + //TS_ASSERT(b.d_ppContextObjPrev == &t->d_pContextObjList);// THIS ONE FAILS + + d_context->pop(); + + TS_ASSERT(s->d_pContext == d_context); + TS_ASSERT(s->d_pCMM == d_context->d_pCMM); + TS_ASSERT(s->d_level == 0); + //TS_ASSERT(s->d_pContextObjList == &b);// THIS ONE FAILS + + TS_ASSERT(a.d_pScope == s); + TS_ASSERT(a.d_pContextObjRestore == NULL); + TS_ASSERT(a.d_pContextObjNext == NULL); + TS_ASSERT(a.d_ppContextObjPrev == &b.d_pContextObjNext); + + TS_ASSERT(b.d_pScope == s); + TS_ASSERT(b.d_pContextObjRestore == NULL); + TS_ASSERT(b.d_pContextObjNext == &a); + TS_ASSERT(b.d_ppContextObjPrev == &s->d_pContextObjList); + } +}; diff --git a/test/unit/expr/attribute_white.h b/test/unit/expr/attribute_white.h index fb18601a3..64c768a13 100644 --- a/test/unit/expr/attribute_white.h +++ b/test/unit/expr/attribute_white.h @@ -17,12 +17,14 @@ #include <string> +#include "context/context.h" #include "expr/node_value.h" #include "expr/node_builder.h" #include "expr/node_manager.h" -#include "expr/node.h" #include "expr/attribute.h" -#include "context/context.h" +#include "expr/node.h" +#include "theory/theory.h" +#include "theory/uf/theory_uf.h" #include "util/Assert.h" using namespace CVC4; @@ -74,24 +76,73 @@ public: } void testAttributeIds() { - TS_ASSERT(VarNameAttr::s_id == 0); - TS_ASSERT(TestStringAttr1::s_id == 1); - TS_ASSERT(TestStringAttr2::s_id == 2); - TS_ASSERT((attr::LastAttributeId<string, false>::s_id == 3)); - - TS_ASSERT(TypeAttr::s_id == 0); - TS_ASSERT((attr::LastAttributeId<void*, false>::s_id == 1)); - - TS_ASSERT(TestFlag1::s_id == 0); - TS_ASSERT(TestFlag2::s_id == 1); - TS_ASSERT(TestFlag3::s_id == 2); - TS_ASSERT(TestFlag4::s_id == 3); - TS_ASSERT(TestFlag5::s_id == 4); - TS_ASSERT((attr::LastAttributeId<bool, false>::s_id == 5)); - - TS_ASSERT(TestFlag1cd::s_id == 0); - TS_ASSERT(TestFlag2cd::s_id == 1); - TS_ASSERT((attr::LastAttributeId<bool, true>::s_id == 2)); + // Test that IDs for (a subset of) attributes in the system are + // unique and that the LastAttributeId (which would be the next ID + // to assign) is greater than all attribute IDs. + + // We used to check ID assignments explicitly. However, between + // compilation modules, you don't get a strong guarantee + // (initialization order is somewhat implementation-specific, and + // anyway you'd have to change the tests anytime you add an + // attribute). So we back off, and just test that they're unique + // and that the next ID to be assigned is strictly greater than + // those that have already been assigned. + + unsigned lastId = attr::LastAttributeId<string, false>::s_id; + TS_ASSERT_LESS_THAN(VarNameAttr::s_id, lastId); + TS_ASSERT_LESS_THAN(TestStringAttr1::s_id, lastId); + TS_ASSERT_LESS_THAN(TestStringAttr2::s_id, lastId); + + TS_ASSERT_DIFFERS(VarNameAttr::s_id, TestStringAttr1::s_id); + TS_ASSERT_DIFFERS(VarNameAttr::s_id, TestStringAttr2::s_id); + TS_ASSERT_DIFFERS(TestStringAttr1::s_id, TestStringAttr2::s_id); + + lastId = attr::LastAttributeId<void*, false>::s_id; + TS_ASSERT_LESS_THAN(NodeManager::TypeAttr::s_id, lastId); + TS_ASSERT_LESS_THAN(theory::uf::ECAttr::s_id, lastId); + TS_ASSERT_DIFFERS(NodeManager::TypeAttr::s_id, theory::uf::ECAttr::s_id); + + lastId = attr::LastAttributeId<bool, false>::s_id; + TS_ASSERT_LESS_THAN(NodeManager::AtomicAttr::s_id, lastId); + TS_ASSERT_LESS_THAN(theory::Theory::PreRegisteredAttr::s_id, lastId); + TS_ASSERT_LESS_THAN(TestFlag1::s_id, lastId); + TS_ASSERT_LESS_THAN(TestFlag2::s_id, lastId); + TS_ASSERT_LESS_THAN(TestFlag3::s_id, lastId); + TS_ASSERT_LESS_THAN(TestFlag4::s_id, lastId); + TS_ASSERT_LESS_THAN(TestFlag5::s_id, lastId); + TS_ASSERT_DIFFERS(NodeManager::AtomicAttr::s_id, + theory::Theory::PreRegisteredAttr::s_id); + TS_ASSERT_DIFFERS(NodeManager::AtomicAttr::s_id, TestFlag1::s_id); + TS_ASSERT_DIFFERS(NodeManager::AtomicAttr::s_id, TestFlag2::s_id); + TS_ASSERT_DIFFERS(NodeManager::AtomicAttr::s_id, TestFlag3::s_id); + TS_ASSERT_DIFFERS(NodeManager::AtomicAttr::s_id, TestFlag4::s_id); + TS_ASSERT_DIFFERS(NodeManager::AtomicAttr::s_id, TestFlag5::s_id); + TS_ASSERT_DIFFERS(theory::Theory::PreRegisteredAttr::s_id, TestFlag1::s_id); + TS_ASSERT_DIFFERS(theory::Theory::PreRegisteredAttr::s_id, TestFlag2::s_id); + TS_ASSERT_DIFFERS(theory::Theory::PreRegisteredAttr::s_id, TestFlag3::s_id); + TS_ASSERT_DIFFERS(theory::Theory::PreRegisteredAttr::s_id, TestFlag4::s_id); + TS_ASSERT_DIFFERS(theory::Theory::PreRegisteredAttr::s_id, TestFlag5::s_id); + TS_ASSERT_DIFFERS(TestFlag1::s_id, TestFlag2::s_id); + TS_ASSERT_DIFFERS(TestFlag1::s_id, TestFlag3::s_id); + TS_ASSERT_DIFFERS(TestFlag1::s_id, TestFlag4::s_id); + TS_ASSERT_DIFFERS(TestFlag1::s_id, TestFlag5::s_id); + TS_ASSERT_DIFFERS(TestFlag2::s_id, TestFlag3::s_id); + TS_ASSERT_DIFFERS(TestFlag2::s_id, TestFlag4::s_id); + TS_ASSERT_DIFFERS(TestFlag2::s_id, TestFlag5::s_id); + TS_ASSERT_DIFFERS(TestFlag3::s_id, TestFlag4::s_id); + TS_ASSERT_DIFFERS(TestFlag3::s_id, TestFlag5::s_id); + TS_ASSERT_DIFFERS(TestFlag4::s_id, TestFlag5::s_id); + + lastId = attr::LastAttributeId<bool, true>::s_id; + TS_ASSERT_LESS_THAN(theory::Theory::RegisteredAttr::s_id, lastId); + TS_ASSERT_LESS_THAN(TestFlag1cd::s_id, lastId); + TS_ASSERT_LESS_THAN(TestFlag2cd::s_id, lastId); + TS_ASSERT_DIFFERS(theory::Theory::RegisteredAttr::s_id, TestFlag1cd::s_id); + TS_ASSERT_DIFFERS(theory::Theory::RegisteredAttr::s_id, TestFlag2cd::s_id); + TS_ASSERT_DIFFERS(TestFlag1cd::s_id, TestFlag2cd::s_id); + + lastId = attr::LastAttributeId<TNode, false>::s_id; + TS_ASSERT_LESS_THAN(theory::RewriteCache::s_id, lastId); } void testCDAttributes() { diff --git a/test/unit/expr/expr_black.h b/test/unit/expr/expr_black.h index e253b4a24..03d4ba31c 100644 --- a/test/unit/expr/expr_black.h +++ b/test/unit/expr/expr_black.h @@ -354,7 +354,9 @@ public: TS_ASSERT(mult->isAtomic()); TS_ASSERT(plus->isAtomic()); TS_ASSERT(d->isAtomic()); - TS_ASSERT(!null->isAtomic()); +#ifdef CVC4_ASSERTIONS + TS_ASSERT_THROWS(null->isAtomic(), IllegalArgumentException); +#endif /* CVC4_ASSERTIONS */ TS_ASSERT(i1->isAtomic()); TS_ASSERT(i2->isAtomic()); @@ -368,6 +370,12 @@ public: 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() { diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h index 81aa424f8..2a7b3623e 100644 --- a/test/unit/expr/node_builder_black.h +++ b/test/unit/expr/node_builder_black.h @@ -244,9 +244,9 @@ public: Node n = noKind; -#ifdef CVC4_DEBUG - TS_ASSERT_THROWS_ANYTHING(noKind.getKind();); -#endif +#ifdef CVC4_ASSERTIONS + TS_ASSERT_THROWS(noKind.getKind(), AssertionException); +#endif /* CVC4_ASSERTIONS */ NodeBuilder<> spec(specKind); TS_ASSERT_EQUALS(spec.getKind(), specKind); @@ -277,11 +277,11 @@ public: push_back(noKind, K); TS_ASSERT_EQUALS(noKind.getNumChildren(), K+K); -#ifdef CVC4_DEBUG +#ifdef CVC4_ASSERTIONS noKind << specKind; n = noKind; - TS_ASSERT_THROWS_ANYTHING( noKind.getNumChildren() ); -#endif + TS_ASSERT_THROWS( noKind.getNumChildren(), AssertionException ); +#endif /* CVC4_ASSERTIONS */ } void testOperatorSquare() { @@ -297,10 +297,10 @@ public: Node i_2 = d_nm->mkConst(true); Node i_K = d_nm->mkNode(NOT, i_0); -#ifdef CVC4_DEBUG - TS_ASSERT_THROWS_ANYTHING(arr[-1];); - TS_ASSERT_THROWS_ANYTHING(arr[0];); -#endif +#ifdef CVC4_ASSERTIONS + TS_ASSERT_THROWS(arr[-1], AssertionException); + TS_ASSERT_THROWS(arr[0], AssertionException); +#endif /* CVC4_ASSERTIONS */ arr << i_0; @@ -330,10 +330,10 @@ public: } TS_ASSERT_EQUALS(arr[K], i_K); -#ifdef CVC4_DEBUG +#ifdef CVC4_ASSERTIONS Node n = arr; - TS_ASSERT_THROWS_ANYTHING(arr[0]); -#endif + TS_ASSERT_THROWS(arr[0], AssertionException); +#endif /* CVC4_ASSERTIONS */ } void testClear() { @@ -469,6 +469,10 @@ public: Node p = d_nm->mkNode(PLUS, z, d_nm->mkNode(UMINUS, x), z); Node q = d_nm->mkNode(AND, x, z, d_nm->mkNode(NOT, y)); +#ifdef CVC4_ASSERTIONS + TS_ASSERT_THROWS(d_nm->mkNode(XOR, y, x, x), AssertionException); +#endif /* CVC4_ASSERTIONS */ + NodeBuilder<> b; // test append(TNode) diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h index 427a22c9d..c6da48291 100644 --- a/test/unit/theory/theory_black.h +++ b/test/unit/theory/theory_black.h @@ -82,13 +82,13 @@ public: } }; -class DummyTheory : public TheoryImpl<DummyTheory> { +class DummyTheory : public Theory { public: set<Node> d_registered; vector<Node> d_getSequence; DummyTheory(Context* ctxt, OutputChannel& out) : - TheoryImpl<DummyTheory>(ctxt, out) { + Theory(ctxt, out) { } void registerTerm(TNode n) { |