diff options
| author | Morgan Deters <mdeters@gmail.com> | 2010-05-27 21:19:36 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2010-05-27 21:19:36 +0000 |
| commit | 6ac90a806f563981bc25fe06bb0dde35d62da7a9 (patch) | |
| tree | cbf5f3b1d4877cd6a7469356cfabbea5242d1d8f /test/unit | |
| parent | 671a3d6d5ae8a89a1bb846a78f5ec9c064edc655 (diff) | |
Remove isAtomic() as per 4/27/2010 meeting. Add comments about its potential design for later. Resolves bug 113, invalidates bugs 93 and 94.
Diffstat (limited to 'test/unit')
| -rw-r--r-- | test/unit/expr/attribute_white.h | 8 | ||||
| -rw-r--r-- | test/unit/expr/expr_public.h | 33 |
2 files changed, 0 insertions, 41 deletions
diff --git a/test/unit/expr/attribute_white.h b/test/unit/expr/attribute_white.h index 43bcc7fe3..509f0b02d 100644 --- a/test/unit/expr/attribute_white.h +++ b/test/unit/expr/attribute_white.h @@ -105,20 +105,12 @@ public: TS_ASSERT_LESS_THAN(theory::uf::ECAttr::s_id, lastId); 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); diff --git a/test/unit/expr/expr_public.h b/test/unit/expr/expr_public.h index 1930e2bb1..00f20dbe6 100644 --- a/test/unit/expr/expr_public.h +++ b/test/unit/expr/expr_public.h @@ -348,39 +348,6 @@ public: TS_ASSERT(!null->isConst()); } - void testIsAtomic() { - /* bool isAtomic() const; */ - - TS_ASSERT(a_bool->isAtomic()); - TS_ASSERT(b_bool->isAtomic()); - TS_ASSERT(c_bool_mult->isAtomic()); - TS_ASSERT(mult_op->isAtomic()); - TS_ASSERT(plus_op->isAtomic()); - TS_ASSERT(d_apply_fun_bool->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_bool, *b_bool); - Expr y = d_em->mkExpr(ITE, *a_bool, *b_bool, *c_bool_mult); - 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; */ |