diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-04-04 19:55:47 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-04-04 19:55:47 +0000 |
commit | 42c58baf0a2a96c1f3bd797d64834d02adfb9a59 (patch) | |
tree | a65529c9cd8399c8e78a4501eace01c150336942 /test/unit/expr | |
parent | 73be7b6b5a9c98cc5a32dcfb3050b9656bf10243 (diff) |
* Node::isAtomic() now looks at an "atomic" attribute of arguments
instead of assuming it's atomic based on kind. Atomicity is
determined at node building time. Fixes bug #81. If this is
determined to make node building too slow, we can allocate another
attribute "AtomicHasBeenComputed" to lazily compute atomicity.
* TheoryImpl<> has gone away. Theory implementations now derive from
Theory directly and share a single RegisteredAttr attribute for term
registration (which shouldn't overlap: every term is "owned" by
exactly one Theory). Fixes bug #79.
* Additional atomicity tests in ExprBlack unit test.
* More appropriate whitebox testing for attribute ID assignment
(AttributeWhite unit test).
* Better (and more correct) assertion checking in NodeBuilderBlack.
* run-regression script now checks exit status against what's provided
in "% EXIT: " gesture in .cvc input files, and stderr against
"% EXPECT-ERROR: ". These can be used to support intended failures.
Fixes bug #84. Also add "% EXIT: " gestures to all .cvc regressions
in repository.
* Solved some "control reaches end of non-void function" warnings in
src/parser/bounded_token_buffer.cpp by replacing
"AlwaysAssert(false)" with "Unreachable()" (which is known
statically to never return normally).
* Regression tests now use the cvc4 binary under
builds/$(CURRENT_BUILD)/src/main instead of the one in bin/ which
may not be properly installed yet at that point of the build.
(Partially fixes bug #46.)
* -fvisibility=hidden is now included by configure.ac instead of each
Makefile.am, which will make it easier to support platforms
(e.g. cygwin) that do things a different way.
* TheoryUF code formatting. (re: my code review bug #64)
* CDMap<> is leaking memory again, pending a fix for bug #85 in the
context subsystem. (To avoid serious errors, can't free context
objects.)
* add ContextWhite unit test for bug #85 (though it's currently
"defanged," awaiting the bugfix)
* Minor documentation, other cleanup.
Diffstat (limited to 'test/unit/expr')
-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 |
3 files changed, 97 insertions, 34 deletions
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) |