summaryrefslogtreecommitdiff
path: root/test/unit
diff options
context:
space:
mode:
Diffstat (limited to 'test/unit')
-rw-r--r--test/unit/context/cdmap_black.h836
-rw-r--r--test/unit/expr/attribute_black.h60
-rw-r--r--test/unit/expr/attribute_white.h137
3 files changed, 64 insertions, 969 deletions
diff --git a/test/unit/context/cdmap_black.h b/test/unit/context/cdmap_black.h
index 1b9e1fa7b..d0db0cc0f 100644
--- a/test/unit/context/cdmap_black.h
+++ b/test/unit/context/cdmap_black.h
@@ -16,178 +16,97 @@
#include <cxxtest/TestSuite.h>
+#include <map>
+
+#include "base/cvc4_assert.h"
+#include "context/context.h"
#include "context/cdhashmap.h"
#include "context/cdlist.h"
-using namespace std;
-using namespace CVC4;
-using namespace CVC4::context;
+using CVC4::AssertionException;
+using CVC4::context::Context;
+using CVC4::context::CDHashMap;
class CDMapBlack : public CxxTest::TestSuite {
-
Context* d_context;
-public:
-
+ public:
void setUp() {
d_context = new Context;
- //Debug.on("context");
- //Debug.on("gc");
- //Debug.on("pushpop");
+ // Debug.on("context");
+ // Debug.on("gc");
+ // Debug.on("pushpop");
}
- void tearDown() {
- delete d_context;
+ void tearDown() { delete d_context; }
+
+ // Returns the elements in a CDHashMap.
+ static std::map<int, int> GetElements(const CDHashMap<int, int>& map) {
+ return std::map<int, int>{map.begin(), map.end()};
+ }
+
+ // Returns true if the elements in map are the same as expected.
+ // NOTE: This is mostly to help the type checker for matching expected within
+ // a TS_ASSERT.
+ static bool ElementsAre(const CDHashMap<int, int>& map,
+ const std::map<int, int>& expected) {
+ return GetElements(map) == expected;
}
void testSimpleSequence() {
CDHashMap<int, int> map(d_context);
-
- TS_ASSERT(map.find(3) == map.end());
- TS_ASSERT(map.find(5) == map.end());
- TS_ASSERT(map.find(9) == map.end());
- TS_ASSERT(map.find(1) == map.end());
- TS_ASSERT(map.find(23) == map.end());
+ TS_ASSERT(ElementsAre(map, {}));
map.insert(3, 4);
-
- TS_ASSERT(map.find(3) != map.end());
- TS_ASSERT(map.find(5) == map.end());
- TS_ASSERT(map.find(9) == map.end());
- TS_ASSERT(map.find(1) == map.end());
- TS_ASSERT(map.find(23) == map.end());
- TS_ASSERT(map[3] == 4);
+ TS_ASSERT(ElementsAre(map, {{3, 4}}));
{
d_context->push();
-
- TS_ASSERT(map.find(3) != map.end());
- TS_ASSERT(map.find(5) == map.end());
- TS_ASSERT(map.find(9) == map.end());
- TS_ASSERT(map.find(1) == map.end());
- TS_ASSERT(map.find(23) == map.end());
- TS_ASSERT(map[3] == 4);
+ TS_ASSERT(ElementsAre(map, {{3, 4}}));
map.insert(5, 6);
map.insert(9, 8);
-
- TS_ASSERT(map.find(3) != map.end());
- TS_ASSERT(map.find(5) != map.end());
- TS_ASSERT(map.find(9) != map.end());
- TS_ASSERT(map.find(1) == map.end());
- TS_ASSERT(map.find(23) == map.end());
- TS_ASSERT(map[3] == 4);
- TS_ASSERT(map[5] == 6);
- TS_ASSERT(map[9] == 8);
+ TS_ASSERT(ElementsAre(map, {{3, 4}, {5, 6}, {9, 8}}));
{
d_context->push();
-
- TS_ASSERT(map.find(3) != map.end());
- TS_ASSERT(map.find(5) != map.end());
- TS_ASSERT(map.find(9) != map.end());
- TS_ASSERT(map.find(1) == map.end());
- TS_ASSERT(map.find(23) == map.end());
- TS_ASSERT(map[3] == 4);
- TS_ASSERT(map[5] == 6);
- TS_ASSERT(map[9] == 8);
+ TS_ASSERT(ElementsAre(map, {{3, 4}, {5, 6}, {9, 8}}));
map.insert(1, 2);
-
- TS_ASSERT(map.find(3) != map.end());
- TS_ASSERT(map.find(5) != map.end());
- TS_ASSERT(map.find(9) != map.end());
- TS_ASSERT(map.find(1) != map.end());
- TS_ASSERT(map.find(23) == map.end());
- TS_ASSERT(map[3] == 4);
- TS_ASSERT(map[5] == 6);
- TS_ASSERT(map[9] == 8);
- TS_ASSERT(map[1] == 2);
+ TS_ASSERT(ElementsAre(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}}));
{
d_context->push();
-
- TS_ASSERT(map.find(3) != map.end());
- TS_ASSERT(map.find(5) != map.end());
- TS_ASSERT(map.find(9) != map.end());
- TS_ASSERT(map.find(1) != map.end());
- TS_ASSERT(map.find(23) == map.end());
- TS_ASSERT(map[3] == 4);
- TS_ASSERT(map[5] == 6);
- TS_ASSERT(map[9] == 8);
- TS_ASSERT(map[1] == 2);
+ TS_ASSERT(ElementsAre(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}}));
map.insertAtContextLevelZero(23, 317);
map.insert(1, 45);
- TS_ASSERT(map.find(3) != map.end());
- TS_ASSERT(map.find(5) != map.end());
- TS_ASSERT(map.find(9) != map.end());
- TS_ASSERT(map.find(1) != map.end());
- TS_ASSERT(map.find(23) != map.end());
- TS_ASSERT(map[3] == 4);
- TS_ASSERT(map[5] == 6);
- TS_ASSERT(map[9] == 8);
- TS_ASSERT(map[1] == 45);
- TS_ASSERT(map[23] == 317);
-
+ TS_ASSERT(
+ ElementsAre(map, {{1, 45}, {3, 4}, {5, 6}, {9, 8}, {23, 317}}));
map.insert(23, 324);
- TS_ASSERT(map.find(3) != map.end());
- TS_ASSERT(map.find(5) != map.end());
- TS_ASSERT(map.find(9) != map.end());
- TS_ASSERT(map.find(1) != map.end());
- TS_ASSERT(map.find(23) != map.end());
- TS_ASSERT(map[3] == 4);
- TS_ASSERT(map[5] == 6);
- TS_ASSERT(map[9] == 8);
- TS_ASSERT(map[1] == 45);
- TS_ASSERT(map[23] == 324);
-
+ TS_ASSERT(
+ ElementsAre(map, {{1, 45}, {3, 4}, {5, 6}, {9, 8}, {23, 324}}));
d_context->pop();
}
- TS_ASSERT(map.find(3) != map.end());
- TS_ASSERT(map.find(5) != map.end());
- TS_ASSERT(map.find(9) != map.end());
- TS_ASSERT(map.find(1) != map.end());
- TS_ASSERT(map.find(23) != map.end());
- TS_ASSERT(map[3] == 4);
- TS_ASSERT(map[5] == 6);
- TS_ASSERT(map[9] == 8);
- TS_ASSERT(map[1] == 2);
- TS_ASSERT(map[23] == 317);
-
+ TS_ASSERT(
+ ElementsAre(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}, {23, 317}}));
d_context->pop();
}
- TS_ASSERT(map.find(3) != map.end());
- TS_ASSERT(map.find(5) != map.end());
- TS_ASSERT(map.find(9) != map.end());
- TS_ASSERT(map.find(1) == map.end());
- TS_ASSERT(map.find(23) != map.end());
- TS_ASSERT(map[3] == 4);
- TS_ASSERT(map[5] == 6);
- TS_ASSERT(map[9] == 8);
- TS_ASSERT(map[23] == 317);
-
+ TS_ASSERT(ElementsAre(map, {{3, 4}, {5, 6}, {9, 8}, {23, 317}}));
d_context->pop();
}
- TS_ASSERT(map.find(3) != map.end());
- TS_ASSERT(map.find(5) == map.end());
- TS_ASSERT(map.find(9) == map.end());
- TS_ASSERT(map.find(1) == map.end());
- TS_ASSERT(map.find(23) != map.end());
- TS_ASSERT(map[3] == 4);
- TS_ASSERT(map[23] == 317);
+ TS_ASSERT(ElementsAre(map, {{3, 4}, {23, 317}}));
}
// no intervening find() in this one
// (under the theory that this could trigger a bug)
void testSimpleSequenceFewerFinds() {
CDHashMap<int, int> map(d_context);
-
map.insert(3, 4);
{
@@ -201,18 +120,9 @@ public:
map.insert(1, 2);
- TS_ASSERT(map.find(1) != map.end());
- TS_ASSERT(map.find(9) != map.end());
- TS_ASSERT(map.find(5) != map.end());
- TS_ASSERT(map.find(7) == map.end());
- TS_ASSERT(map.find(23) == map.end());
- TS_ASSERT(map[1] == 2);
- TS_ASSERT(map[9] == 8);
- TS_ASSERT(map[5] == 6);
-
+ TS_ASSERT(ElementsAre(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}}));
{
d_context->push();
-
d_context->pop();
}
@@ -223,416 +133,34 @@ public:
}
}
- void testObliterate() {
- CDHashMap<int, int> map(d_context);
-
- map.insert(3, 4);
-
- TS_ASSERT(map.find(3) != map.end());
- TS_ASSERT(map.find(5) == map.end());
- TS_ASSERT(map.find(9) == map.end());
- TS_ASSERT(map.find(1) == map.end());
- TS_ASSERT(map.find(23) == map.end());
- TS_ASSERT(map[3] == 4);
-
- {
- d_context->push();
-
- TS_ASSERT(map.find(3) != map.end());
- TS_ASSERT(map.find(5) == map.end());
- TS_ASSERT(map.find(9) == map.end());
- TS_ASSERT(map.find(1) == map.end());
- TS_ASSERT(map.find(23) == map.end());
- TS_ASSERT(map[3] == 4);
-
- map.insert(5, 6);
- map.insert(9, 8);
-
- TS_ASSERT(map.find(3) != map.end());
- TS_ASSERT(map.find(5) != map.end());
- TS_ASSERT(map.find(9) != map.end());
- TS_ASSERT(map.find(1) == map.end());
- TS_ASSERT(map.find(23) == map.end());
- TS_ASSERT(map[3] == 4);
- TS_ASSERT(map[5] == 6);
- TS_ASSERT(map[9] == 8);
-
- {
- d_context->push();
-
- TS_ASSERT(map.find(3) != map.end());
- TS_ASSERT(map.find(5) != map.end());
- TS_ASSERT(map.find(9) != map.end());
- TS_ASSERT(map.find(1) == map.end());
- TS_ASSERT(map.find(23) == map.end());
- TS_ASSERT(map[3] == 4);
- TS_ASSERT(map[5] == 6);
- TS_ASSERT(map[9] == 8);
-
- map.insertAtContextLevelZero(23, 317);
- map.insert(1, 2);
-
- TS_ASSERT(map.find(3) != map.end());
- TS_ASSERT(map.find(5) != map.end());
- TS_ASSERT(map.find(9) != map.end());
- TS_ASSERT(map.find(1) != map.end());
- TS_ASSERT(map.find(23) != map.end());
- TS_ASSERT(map[3] == 4);
- TS_ASSERT(map[5] == 6);
- TS_ASSERT(map[9] == 8);
- TS_ASSERT(map[1] == 2);
- TS_ASSERT(map[23] == 317);
-
- map.obliterate(5);
-
- TS_ASSERT(map.find(3) != map.end());
- TS_ASSERT(map.find(5) == map.end());
- TS_ASSERT(map.find(9) != map.end());
- TS_ASSERT(map.find(1) != map.end());
- TS_ASSERT(map.find(23) != map.end());
- TS_ASSERT(map[3] == 4);
- TS_ASSERT(map[9] == 8);
- TS_ASSERT(map[1] == 2);
- TS_ASSERT(map[23] == 317);
-
- {
- d_context->push();
-
- TS_ASSERT(map.find(3) != map.end());
- TS_ASSERT(map.find(5) == map.end());
- TS_ASSERT(map.find(9) != map.end());
- TS_ASSERT(map.find(1) != map.end());
- TS_ASSERT(map.find(23) != map.end());
- TS_ASSERT(map[3] == 4);
- TS_ASSERT(map[9] == 8);
- TS_ASSERT(map[1] == 2);
- TS_ASSERT(map[23] == 317);
-
- d_context->pop();
- }
-
- TS_ASSERT(map.find(3) != map.end());
- TS_ASSERT(map.find(5) == map.end());
- TS_ASSERT(map.find(9) != map.end());
- TS_ASSERT(map.find(1) != map.end());
- TS_ASSERT(map.find(23) != map.end());
- TS_ASSERT(map[3] == 4);
- TS_ASSERT(map[9] == 8);
- TS_ASSERT(map[1] == 2);
- TS_ASSERT(map[23] == 317);
-
- map.obliterate(23);
-
- TS_ASSERT(map.find(3) != map.end());
- TS_ASSERT(map.find(5) == map.end());
- TS_ASSERT(map.find(9) != map.end());
- TS_ASSERT(map.find(1) != map.end());
- TS_ASSERT(map.find(23) == map.end());
- TS_ASSERT(map[3] == 4);
- TS_ASSERT(map[9] == 8);
- TS_ASSERT(map[1] == 2);
-
- d_context->pop();
- }
-
- TS_ASSERT(map.find(3) != map.end());
- TS_ASSERT(map.find(5) == map.end());
- TS_ASSERT(map.find(9) != map.end());
- TS_ASSERT(map.find(1) == map.end());
- TS_ASSERT(map.find(23) == map.end());
- TS_ASSERT(map[3] == 4);
- TS_ASSERT(map[9] == 8);
-
- d_context->pop();
- }
-
- TS_ASSERT(map.find(3) != map.end());
- TS_ASSERT(map.find(5) == map.end());
- TS_ASSERT(map.find(9) == map.end());
- TS_ASSERT(map.find(1) == map.end());
- TS_ASSERT(map.find(23) == map.end());
- TS_ASSERT(map[3] == 4);
- }
-
- void testObliteratePrimordial() {
- CDHashMap<int, int> map(d_context);
-
- map.insert(3, 4);
-
- TS_ASSERT(map.find(3) != map.end());
- TS_ASSERT(map.find(5) == map.end());
- TS_ASSERT(map.find(9) == map.end());
- TS_ASSERT(map.find(1) == map.end());
- TS_ASSERT(map[3] == 4);
-
- {
- d_context->push();
-
- TS_ASSERT(map.find(3) != map.end());
- TS_ASSERT(map.find(5) == map.end());
- TS_ASSERT(map.find(9) == map.end());
- TS_ASSERT(map.find(1) == map.end());
- TS_ASSERT(map[3] == 4);
-
- map.insert(5, 6);
- map.insert(9, 8);
-
- TS_ASSERT(map.find(3) != map.end());
- TS_ASSERT(map.find(5) != map.end());
- TS_ASSERT(map.find(9) != map.end());
- TS_ASSERT(map.find(1) == map.end());
- TS_ASSERT(map[3] == 4);
- TS_ASSERT(map[5] == 6);
- TS_ASSERT(map[9] == 8);
-
- {
- d_context->push();
-
- TS_ASSERT(map.find(3) != map.end());
- TS_ASSERT(map.find(5) != map.end());
- TS_ASSERT(map.find(9) != map.end());
- TS_ASSERT(map.find(1) == map.end());
- TS_ASSERT(map[3] == 4);
- TS_ASSERT(map[5] == 6);
- TS_ASSERT(map[9] == 8);
- map.insert(1, 2);
-
- TS_ASSERT(map.find(3) != map.end());
- TS_ASSERT(map.find(5) != map.end());
- TS_ASSERT(map.find(9) != map.end());
- TS_ASSERT(map.find(1) != map.end());
- TS_ASSERT(map[3] == 4);
- TS_ASSERT(map[5] == 6);
- TS_ASSERT(map[9] == 8);
- TS_ASSERT(map[1] == 2);
-
- map.obliterate(3);
-
- TS_ASSERT(map.find(3) == map.end());
- TS_ASSERT(map.find(5) != map.end());
- TS_ASSERT(map.find(9) != map.end());
- TS_ASSERT(map.find(1) != map.end());
- TS_ASSERT(map[5] == 6);
- TS_ASSERT(map[9] == 8);
- TS_ASSERT(map[1] == 2);
-
- {
- d_context->push();
-
- TS_ASSERT(map.find(3) == map.end());
- TS_ASSERT(map.find(5) != map.end());
- TS_ASSERT(map.find(9) != map.end());
- TS_ASSERT(map.find(1) != map.end());
- TS_ASSERT(map[5] == 6);
- TS_ASSERT(map[9] == 8);
- TS_ASSERT(map[1] == 2);
-
- d_context->pop();
- }
-
- TS_ASSERT(map.find(3) == map.end());
- TS_ASSERT(map.find(5) != map.end());
- TS_ASSERT(map.find(9) != map.end());
- TS_ASSERT(map.find(1) != map.end());
- TS_ASSERT(map[5] == 6);
- TS_ASSERT(map[9] == 8);
- TS_ASSERT(map[1] == 2);
-
- d_context->pop();
- }
-
- TS_ASSERT(map.find(3) == map.end());
- TS_ASSERT(map.find(5) != map.end());
- TS_ASSERT(map.find(9) != map.end());
- TS_ASSERT(map.find(1) == map.end());
- TS_ASSERT(map[5] == 6);
- TS_ASSERT(map[9] == 8);
-
- d_context->pop();
- }
-
- TS_ASSERT(map.find(3) == map.end());
- TS_ASSERT(map.find(5) == map.end());
- TS_ASSERT(map.find(9) == map.end());
- TS_ASSERT(map.find(1) == map.end());
- }
-
- void testObliterateCurrent() {
- CDHashMap<int, int> map(d_context);
-
- map.insert(3, 4);
-
- TS_ASSERT(map.find(3) != map.end());
- TS_ASSERT(map.find(5) == map.end());
- TS_ASSERT(map.find(9) == map.end());
- TS_ASSERT(map.find(1) == map.end());
- TS_ASSERT(map[3] == 4);
-
- {
- d_context->push();
-
- TS_ASSERT(map.find(3) != map.end());
- TS_ASSERT(map.find(5) == map.end());
- TS_ASSERT(map.find(9) == map.end());
- TS_ASSERT(map.find(1) == map.end());
- TS_ASSERT(map[3] == 4);
-
- map.insert(5, 6);
- map.insert(9, 8);
-
- TS_ASSERT(map.find(3) != map.end());
- TS_ASSERT(map.find(5) != map.end());
- TS_ASSERT(map.find(9) != map.end());
- TS_ASSERT(map.find(1) == map.end());
- TS_ASSERT(map[3] == 4);
- TS_ASSERT(map[5] == 6);
- TS_ASSERT(map[9] == 8);
-
- {
- d_context->push();
-
- TS_ASSERT(map.find(3) != map.end());
- TS_ASSERT(map.find(5) != map.end());
- TS_ASSERT(map.find(9) != map.end());
- TS_ASSERT(map.find(1) == map.end());
- TS_ASSERT(map[3] == 4);
- TS_ASSERT(map[5] == 6);
- TS_ASSERT(map[9] == 8);
-
- map.insert(1, 2);
-
- TS_ASSERT(map.find(3) != map.end());
- TS_ASSERT(map.find(5) != map.end());
- TS_ASSERT(map.find(9) != map.end());
- TS_ASSERT(map.find(1) != map.end());
- TS_ASSERT(map[3] == 4);
- TS_ASSERT(map[5] == 6);
- TS_ASSERT(map[9] == 8);
- TS_ASSERT(map[1] == 2);
-
- map.obliterate(1);
-
- TS_ASSERT(map.find(3) != map.end());
- TS_ASSERT(map.find(5) != map.end());
- TS_ASSERT(map.find(9) != map.end());
- TS_ASSERT(map.find(1) == map.end());
- TS_ASSERT(map[3] == 4);
- TS_ASSERT(map[5] == 6);
- TS_ASSERT(map[9] == 8);
-
- {
- d_context->push();
-
- TS_ASSERT(map.find(3) != map.end());
- TS_ASSERT(map.find(5) != map.end());
- TS_ASSERT(map.find(9) != map.end());
- TS_ASSERT(map.find(1) == map.end());
- TS_ASSERT(map[3] == 4);
- TS_ASSERT(map[5] == 6);
- TS_ASSERT(map[9] == 8);
-
- d_context->pop();
- }
-
- TS_ASSERT(map.find(3) != map.end());
- TS_ASSERT(map.find(5) != map.end());
- TS_ASSERT(map.find(9) != map.end());
- TS_ASSERT(map.find(1) == map.end());
- TS_ASSERT(map[3] == 4);
- TS_ASSERT(map[5] == 6);
- TS_ASSERT(map[9] == 8);
-
- d_context->pop();
- }
-
- TS_ASSERT(map.find(3) != map.end());
- TS_ASSERT(map.find(5) != map.end());
- TS_ASSERT(map.find(9) != map.end());
- TS_ASSERT(map.find(1) == map.end());
- TS_ASSERT(map[3] == 4);
- TS_ASSERT(map[5] == 6);
- TS_ASSERT(map[9] == 8);
-
- d_context->pop();
- }
-
- TS_ASSERT(map.find(3) != map.end());
- TS_ASSERT(map.find(5) == map.end());
- TS_ASSERT(map.find(9) == map.end());
- TS_ASSERT(map.find(1) == map.end());
- TS_ASSERT(map[3] == 4);
- }
-
void testInsertAtContextLevelZero() {
CDHashMap<int, int> map(d_context);
map.insert(3, 4);
- TS_ASSERT(map.find(3) != map.end());
- TS_ASSERT(map.find(5) == map.end());
- TS_ASSERT(map.find(9) == map.end());
- TS_ASSERT(map.find(1) == map.end());
- TS_ASSERT(map.find(23) == map.end());
- TS_ASSERT(map[3] == 4);
-
+ TS_ASSERT(ElementsAre(map, {{3, 4}}));
{
d_context->push();
-
- TS_ASSERT(map.find(3) != map.end());
- TS_ASSERT(map.find(5) == map.end());
- TS_ASSERT(map.find(9) == map.end());
- TS_ASSERT(map.find(1) == map.end());
- TS_ASSERT(map.find(23) == map.end());
- TS_ASSERT(map[3] == 4);
+ TS_ASSERT(ElementsAre(map, {{3, 4}}));
map.insert(5, 6);
map.insert(9, 8);
- TS_ASSERT(map.find(3) != map.end());
- TS_ASSERT(map.find(5) != map.end());
- TS_ASSERT(map.find(9) != map.end());
- TS_ASSERT(map.find(1) == map.end());
- TS_ASSERT(map.find(23) == map.end());
- TS_ASSERT(map[3] == 4);
- TS_ASSERT(map[5] == 6);
- TS_ASSERT(map[9] == 8);
+ TS_ASSERT(ElementsAre(map, {{3, 4}, {5, 6}, {9, 8}}));
{
d_context->push();
- TS_ASSERT(map.find(3) != map.end());
- TS_ASSERT(map.find(5) != map.end());
- TS_ASSERT(map.find(9) != map.end());
- TS_ASSERT(map.find(1) == map.end());
- TS_ASSERT(map.find(23) == map.end());
- TS_ASSERT(map[3] == 4);
- TS_ASSERT(map[5] == 6);
- TS_ASSERT(map[9] == 8);
+ TS_ASSERT(ElementsAre(map, {{3, 4}, {5, 6}, {9, 8}}));
map.insert(1, 2);
- TS_ASSERT(map.find(3) != map.end());
- TS_ASSERT(map.find(5) != map.end());
- TS_ASSERT(map.find(9) != map.end());
- TS_ASSERT(map.find(1) != map.end());
- TS_ASSERT(map.find(23) == map.end());
- TS_ASSERT(map[3] == 4);
- TS_ASSERT(map[5] == 6);
- TS_ASSERT(map[9] == 8);
- TS_ASSERT(map[1] == 2);
+ TS_ASSERT(ElementsAre(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}}));
map.insertAtContextLevelZero(23, 317);
- TS_ASSERT(map.find(3) != map.end());
- TS_ASSERT(map.find(5) != map.end());
- TS_ASSERT(map.find(9) != map.end());
- TS_ASSERT(map.find(1) != map.end());
- TS_ASSERT(map.find(23) != map.end());
- TS_ASSERT(map[3] == 4);
- TS_ASSERT(map[5] == 6);
- TS_ASSERT(map[9] == 8);
- TS_ASSERT(map[1] == 2);
- TS_ASSERT(map[23] == 317);
+ TS_ASSERT(
+ ElementsAre(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}, {23, 317}}));
TS_ASSERT_THROWS(map.insertAtContextLevelZero(23, 317),
AssertionException);
@@ -640,278 +168,42 @@ public:
AssertionException);
map.insert(23, 472);
- TS_ASSERT(map.find(3) != map.end());
- TS_ASSERT(map.find(5) != map.end());
- TS_ASSERT(map.find(9) != map.end());
- TS_ASSERT(map.find(1) != map.end());
- TS_ASSERT(map.find(23) != map.end());
- TS_ASSERT(map[3] == 4);
- TS_ASSERT(map[5] == 6);
- TS_ASSERT(map[9] == 8);
- TS_ASSERT(map[1] == 2);
- TS_ASSERT(map[23] == 472);
-
+ TS_ASSERT(
+ ElementsAre(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}, {23, 472}}));
{
d_context->push();
- TS_ASSERT(map.find(3) != map.end());
- TS_ASSERT(map.find(5) != map.end());
- TS_ASSERT(map.find(9) != map.end());
- TS_ASSERT(map.find(1) != map.end());
- TS_ASSERT(map.find(23) != map.end());
- TS_ASSERT(map[3] == 4);
- TS_ASSERT(map[5] == 6);
- TS_ASSERT(map[9] == 8);
- TS_ASSERT(map[1] == 2);
- TS_ASSERT(map[23] == 472);
+ TS_ASSERT(
+ ElementsAre(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}, {23, 472}}));
TS_ASSERT_THROWS(map.insertAtContextLevelZero(23, 0),
AssertionException);
map.insert(23, 1024);
- TS_ASSERT(map.find(3) != map.end());
- TS_ASSERT(map.find(5) != map.end());
- TS_ASSERT(map.find(9) != map.end());
- TS_ASSERT(map.find(1) != map.end());
- TS_ASSERT(map.find(23) != map.end());
- TS_ASSERT(map[3] == 4);
- TS_ASSERT(map[5] == 6);
- TS_ASSERT(map[9] == 8);
- TS_ASSERT(map[1] == 2);
- TS_ASSERT(map[23] == 1024);
-
+ TS_ASSERT(
+ ElementsAre(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}, {23, 1024}}));
d_context->pop();
}
-
- TS_ASSERT(map.find(3) != map.end());
- TS_ASSERT(map.find(5) != map.end());
- TS_ASSERT(map.find(9) != map.end());
- TS_ASSERT(map.find(1) != map.end());
- TS_ASSERT(map.find(23) != map.end());
- TS_ASSERT(map[3] == 4);
- TS_ASSERT(map[5] == 6);
- TS_ASSERT(map[9] == 8);
- TS_ASSERT(map[1] == 2);
- TS_ASSERT(map[23] == 472);
-
+ TS_ASSERT(
+ ElementsAre(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}, {23, 472}}));
d_context->pop();
}
- TS_ASSERT(map.find(3) != map.end());
- TS_ASSERT(map.find(5) != map.end());
- TS_ASSERT(map.find(9) != map.end());
- TS_ASSERT(map.find(1) == map.end());
- TS_ASSERT(map.find(23) != map.end());
- TS_ASSERT(map[3] == 4);
- TS_ASSERT(map[5] == 6);
- TS_ASSERT(map[9] == 8);
- TS_ASSERT(map[23] == 317);
-
- TS_ASSERT_THROWS(map.insertAtContextLevelZero(23, 0),
- AssertionException);
- map.insert(23, 477);
-
- TS_ASSERT(map.find(3) != map.end());
- TS_ASSERT(map.find(5) != map.end());
- TS_ASSERT(map.find(9) != map.end());
- TS_ASSERT(map.find(1) == map.end());
- TS_ASSERT(map.find(23) != map.end());
- TS_ASSERT(map[3] == 4);
- TS_ASSERT(map[5] == 6);
- TS_ASSERT(map[9] == 8);
- TS_ASSERT(map[23] == 477);
-
- d_context->pop();
- }
-
- TS_ASSERT_THROWS(map.insertAtContextLevelZero(23, 0),
- AssertionException);
-
- TS_ASSERT(map.find(3) != map.end());
- TS_ASSERT(map.find(5) == map.end());
- TS_ASSERT(map.find(9) == map.end());
- TS_ASSERT(map.find(1) == map.end());
- TS_ASSERT(map.find(23) != map.end());
- TS_ASSERT(map[3] == 4);
- TS_ASSERT(map[23] == 317);
- }
-
- void testObliterateInsertedAtContextLevelZero() {
- CDHashMap<int, int> map(d_context);
-
- map.insert(3, 4);
-
- TS_ASSERT(map.find(3) != map.end());
- TS_ASSERT(map.find(5) == map.end());
- TS_ASSERT(map.find(9) == map.end());
- TS_ASSERT(map.find(1) == map.end());
- TS_ASSERT(map.find(23) == map.end());
- TS_ASSERT(map[3] == 4);
-
- {
- d_context->push();
-
- TS_ASSERT(map.find(3) != map.end());
- TS_ASSERT(map.find(5) == map.end());
- TS_ASSERT(map.find(9) == map.end());
- TS_ASSERT(map.find(1) == map.end());
- TS_ASSERT(map.find(23) == map.end());
- TS_ASSERT(map[3] == 4);
-
- map.insert(5, 6);
- map.insert(9, 8);
-
- TS_ASSERT(map.find(3) != map.end());
- TS_ASSERT(map.find(5) != map.end());
- TS_ASSERT(map.find(9) != map.end());
- TS_ASSERT(map.find(1) == map.end());
- TS_ASSERT(map.find(23) == map.end());
- TS_ASSERT(map[3] == 4);
- TS_ASSERT(map[5] == 6);
- TS_ASSERT(map[9] == 8);
-
- {
- d_context->push();
-
- TS_ASSERT(map.find(3) != map.end());
- TS_ASSERT(map.find(5) != map.end());
- TS_ASSERT(map.find(9) != map.end());
- TS_ASSERT(map.find(1) == map.end());
- TS_ASSERT(map.find(23) == map.end());
- TS_ASSERT(map[3] == 4);
- TS_ASSERT(map[5] == 6);
- TS_ASSERT(map[9] == 8);
-
- map.insert(1, 2);
-
- TS_ASSERT(map.find(3) != map.end());
- TS_ASSERT(map.find(5) != map.end());
- TS_ASSERT(map.find(9) != map.end());
- TS_ASSERT(map.find(1) != map.end());
- TS_ASSERT(map.find(23) == map.end());
- TS_ASSERT(map[3] == 4);
- TS_ASSERT(map[5] == 6);
- TS_ASSERT(map[9] == 8);
- TS_ASSERT(map[1] == 2);
-
- map.insertAtContextLevelZero(23, 317);
-
- TS_ASSERT(map.find(3) != map.end());
- TS_ASSERT(map.find(5) != map.end());
- TS_ASSERT(map.find(9) != map.end());
- TS_ASSERT(map.find(1) != map.end());
- TS_ASSERT(map.find(23) != map.end());
- TS_ASSERT(map[3] == 4);
- TS_ASSERT(map[5] == 6);
- TS_ASSERT(map[9] == 8);
- TS_ASSERT(map[1] == 2);
- TS_ASSERT(map[23] == 317);
-
- TS_ASSERT_THROWS(map.insertAtContextLevelZero(23, 317),
- AssertionException);
- TS_ASSERT_THROWS(map.insertAtContextLevelZero(23, 472),
- AssertionException);
- map.insert(23, 472);
-
- TS_ASSERT(map.find(3) != map.end());
- TS_ASSERT(map.find(5) != map.end());
- TS_ASSERT(map.find(9) != map.end());
- TS_ASSERT(map.find(1) != map.end());
- TS_ASSERT(map.find(23) != map.end());
- TS_ASSERT(map[3] == 4);
- TS_ASSERT(map[5] == 6);
- TS_ASSERT(map[9] == 8);
- TS_ASSERT(map[1] == 2);
- TS_ASSERT(map[23] == 472);
-
- {
- d_context->push();
-
- TS_ASSERT(map.find(3) != map.end());
- TS_ASSERT(map.find(5) != map.end());
- TS_ASSERT(map.find(9) != map.end());
- TS_ASSERT(map.find(1) != map.end());
- TS_ASSERT(map.find(23) != map.end());
- TS_ASSERT(map[3] == 4);
- TS_ASSERT(map[5] == 6);
- TS_ASSERT(map[9] == 8);
- TS_ASSERT(map[1] == 2);
- TS_ASSERT(map[23] == 472);
-
- TS_ASSERT_THROWS(map.insertAtContextLevelZero(23, 0),
- AssertionException);
- map.insert(23, 1024);
-
- TS_ASSERT(map.find(3) != map.end());
- TS_ASSERT(map.find(5) != map.end());
- TS_ASSERT(map.find(9) != map.end());
- TS_ASSERT(map.find(1) != map.end());
- TS_ASSERT(map.find(23) != map.end());
- TS_ASSERT(map[3] == 4);
- TS_ASSERT(map[5] == 6);
- TS_ASSERT(map[9] == 8);
- TS_ASSERT(map[1] == 2);
- TS_ASSERT(map[23] == 1024);
-
- d_context->pop();
- }
- TS_ASSERT(map.find(3) != map.end());
- TS_ASSERT(map.find(5) != map.end());
- TS_ASSERT(map.find(9) != map.end());
- TS_ASSERT(map.find(1) != map.end());
- TS_ASSERT(map.find(23) != map.end());
- TS_ASSERT(map[3] == 4);
- TS_ASSERT(map[5] == 6);
- TS_ASSERT(map[9] == 8);
- TS_ASSERT(map[1] == 2);
- TS_ASSERT(map[23] == 472);
-
- map.obliterate(23);
-
- TS_ASSERT(map.find(3) != map.end());
- TS_ASSERT(map.find(5) != map.end());
- TS_ASSERT(map.find(9) != map.end());
- TS_ASSERT(map.find(1) != map.end());
- TS_ASSERT(map.find(23) == map.end());
- TS_ASSERT(map[3] == 4);
- TS_ASSERT(map[5] == 6);
- TS_ASSERT(map[9] == 8);
- TS_ASSERT(map[1] == 2);
+ TS_ASSERT(
+ ElementsAre(map, {{3, 4}, {5, 6}, {9, 8}, {23, 317}}));
- d_context->pop();
- }
-
- TS_ASSERT(map.find(3) != map.end());
- TS_ASSERT(map.find(5) != map.end());
- TS_ASSERT(map.find(9) != map.end());
- TS_ASSERT(map.find(1) == map.end());
- TS_ASSERT(map.find(23) == map.end());
- TS_ASSERT(map[3] == 4);
- TS_ASSERT(map[5] == 6);
- TS_ASSERT(map[9] == 8);
-
- // reinsert as a normal map entry
+ TS_ASSERT_THROWS(map.insertAtContextLevelZero(23, 0), AssertionException);
map.insert(23, 477);
- TS_ASSERT(map.find(3) != map.end());
- TS_ASSERT(map.find(5) != map.end());
- TS_ASSERT(map.find(9) != map.end());
- TS_ASSERT(map.find(1) == map.end());
- TS_ASSERT(map.find(23) != map.end());
- TS_ASSERT(map[3] == 4);
- TS_ASSERT(map[5] == 6);
- TS_ASSERT(map[9] == 8);
- TS_ASSERT(map[23] == 477);
-
+ TS_ASSERT(
+ ElementsAre(map, {{3, 4}, {5, 6}, {9, 8}, {23, 477}}));
d_context->pop();
}
- TS_ASSERT(map.find(3) != map.end());
- TS_ASSERT(map.find(5) == map.end());
- TS_ASSERT(map.find(9) == map.end());
- TS_ASSERT(map.find(1) == map.end());
- TS_ASSERT(map.find(23) == map.end());
- TS_ASSERT(map[3] == 4);
+ TS_ASSERT_THROWS(map.insertAtContextLevelZero(23, 0), AssertionException);
+
+ TS_ASSERT(
+ ElementsAre(map, {{3, 4}, {23, 317}}));
}
};
diff --git a/test/unit/expr/attribute_black.h b/test/unit/expr/attribute_black.h
index d919bcbe3..d3f043f36 100644
--- a/test/unit/expr/attribute_black.h
+++ b/test/unit/expr/attribute_black.h
@@ -88,10 +88,7 @@ public:
}
struct PrimitiveIntAttributeId {};
- struct CDPrimitiveIntAttributeId {};
-
typedef expr::Attribute<PrimitiveIntAttributeId,uint64_t> PrimitiveIntAttribute;
- typedef expr::CDAttribute<CDPrimitiveIntAttributeId,uint64_t> CDPrimitiveIntAttribute;
void testInts(){
TypeNode booleanType = d_nodeManager->booleanType();
Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType));
@@ -105,21 +102,12 @@ public:
TS_ASSERT(node->getAttribute(attr, data1));
TS_ASSERT_EQUALS(data1, val);
- uint64_t data2 = 0;
- uint64_t data3 = 0;
- CDPrimitiveIntAttribute cdattr;
- TS_ASSERT(!node->getAttribute(cdattr, data2));
- node->setAttribute(cdattr, val);
- TS_ASSERT(node->getAttribute(cdattr, data3));
- TS_ASSERT_EQUALS(data3, val);
delete node;
}
struct TNodeAttributeId {};
- struct CDTNodeAttributeId {};
typedef expr::Attribute<TNodeAttributeId, TNode> TNodeAttribute;
- typedef expr::CDAttribute<CDTNodeAttributeId, TNode> CDTNodeAttribute;
void testTNodes(){
TypeNode booleanType = d_nodeManager->booleanType();
Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType));
@@ -134,13 +122,6 @@ public:
TS_ASSERT(node->getAttribute(attr, data1));
TS_ASSERT_EQUALS(data1, val);
- TNode data2;
- TNode data3;
- CDTNodeAttribute cdattr;
- TS_ASSERT(!node->getAttribute(cdattr, data2));
- node->setAttribute(cdattr, val);
- TS_ASSERT(node->getAttribute(cdattr, data3));
- TS_ASSERT_EQUALS(data3, val);
delete node;
}
@@ -152,10 +133,8 @@ public:
};
struct PtrAttributeId {};
- struct CDPtrAttributeId {};
typedef expr::Attribute<PtrAttributeId, Foo*> PtrAttribute;
- typedef expr::CDAttribute<CDPtrAttributeId, Foo*> CDPtrAttribute;
void testPtrs(){
TypeNode booleanType = d_nodeManager->booleanType();
Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType));
@@ -170,25 +149,14 @@ public:
TS_ASSERT(node->getAttribute(attr, data1));
TS_ASSERT_EQUALS(data1, val);
- Foo* data2 = NULL;
- Foo* data3 = NULL;
- CDPtrAttribute cdattr;
- TS_ASSERT(!node->getAttribute(cdattr, data2));
- node->setAttribute(cdattr, val);
- TS_ASSERT(node->getAttribute(cdattr, data3));
- TS_ASSERT(data3 != NULL);
- TS_ASSERT_EQUALS(63489, data3->getBar());
- TS_ASSERT_EQUALS(data3, val);
delete node;
delete val;
}
struct ConstPtrAttributeId {};
- struct CDConstPtrAttributeId {};
typedef expr::Attribute<ConstPtrAttributeId, const Foo*> ConstPtrAttribute;
- typedef expr::CDAttribute<CDConstPtrAttributeId, const Foo*> CDConstPtrAttribute;
void testConstPtrs(){
TypeNode booleanType = d_nodeManager->booleanType();
Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType));
@@ -203,22 +171,12 @@ public:
TS_ASSERT(node->getAttribute(attr, data1));
TS_ASSERT_EQUALS(data1, val);
- const Foo* data2 = NULL;
- const Foo* data3 = NULL;
- CDConstPtrAttribute cdattr;
- TS_ASSERT(!node->getAttribute(cdattr, data2));
- node->setAttribute(cdattr, val);
- TS_ASSERT(node->getAttribute(cdattr, data3));
- TS_ASSERT_EQUALS(data3, val);
delete node;
delete val;
}
struct StringAttributeId {};
- struct CDStringAttributeId {};
-
typedef expr::Attribute<StringAttributeId, std::string> StringAttribute;
- typedef expr::CDAttribute<CDStringAttributeId, std::string> CDStringAttribute;
void testStrings(){
TypeNode booleanType = d_nodeManager->booleanType();
Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType));
@@ -233,21 +191,11 @@ public:
TS_ASSERT(node->getAttribute(attr, data1));
TS_ASSERT_EQUALS(data1, val);
- std::string data2;
- std::string data3;
- CDStringAttribute cdattr;
- TS_ASSERT(!node->getAttribute(cdattr, data2));
- node->setAttribute(cdattr, val);
- TS_ASSERT(node->getAttribute(cdattr, data3));
- TS_ASSERT_EQUALS(data3, val);
delete node;
}
struct BoolAttributeId {};
- struct CDBoolAttributeId {};
-
typedef expr::Attribute<BoolAttributeId, bool> BoolAttribute;
- typedef expr::CDAttribute<CDBoolAttributeId, bool> CDBoolAttribute;
void testBools(){
TypeNode booleanType = d_nodeManager->booleanType();
Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType));
@@ -263,14 +211,6 @@ public:
TS_ASSERT(node->getAttribute(attr, data1));
TS_ASSERT_EQUALS(data1, val);
- bool data2 = false;
- bool data3 = false;
- CDBoolAttribute cdattr;
- TS_ASSERT(node->getAttribute(cdattr, data2));
- TS_ASSERT_EQUALS(false, data2);
- node->setAttribute(cdattr, val);
- TS_ASSERT(node->getAttribute(cdattr, data3));
- TS_ASSERT_EQUALS(data3, val);
delete node;
}
diff --git a/test/unit/expr/attribute_white.h b/test/unit/expr/attribute_white.h
index e4786b8e3..60a83b5c7 100644
--- a/test/unit/expr/attribute_white.h
+++ b/test/unit/expr/attribute_white.h
@@ -47,18 +47,12 @@ struct Test5;
typedef Attribute<Test1, std::string> TestStringAttr1;
typedef Attribute<Test2, std::string> TestStringAttr2;
-// it would be nice to have CDAttribute<> for context-dependence
-typedef CDAttribute<Test1, bool> TestCDFlag;
-
typedef Attribute<Test1, bool> TestFlag1;
typedef Attribute<Test2, bool> TestFlag2;
typedef Attribute<Test3, bool> TestFlag3;
typedef Attribute<Test4, bool> TestFlag4;
typedef Attribute<Test5, bool> TestFlag5;
-typedef CDAttribute<Test1, bool> TestFlag1cd;
-typedef CDAttribute<Test2, bool> TestFlag2cd;
-
class AttributeWhite : public CxxTest::TestSuite {
ExprManager* d_em;
@@ -127,11 +121,6 @@ public:
TS_ASSERT_DIFFERS(TestFlag4::s_id, TestFlag5::s_id);
lastId = attr::LastAttributeId<bool, true>::getId();
- TS_ASSERT_LESS_THAN(TestFlag1cd::s_id, lastId);
- TS_ASSERT_LESS_THAN(TestFlag2cd::s_id, lastId);
- TS_ASSERT_DIFFERS(TestFlag1cd::s_id, TestFlag2cd::s_id);
- cout << "1: " << TestFlag1cd::s_id << endl;
- cout << "2: " << TestFlag2cd::s_id << endl;
lastId = attr::LastAttributeId<Node, false>::getId();
// TS_ASSERT_LESS_THAN(theory::PreRewriteCache::s_id, lastId);
@@ -149,132 +138,6 @@ public:
TS_ASSERT_LESS_THAN(TypeAttr::s_id, lastId);
}
- void testCDAttributes() {
- //Debug.on("cdboolattr");
-
- Node a = d_nm->mkVar(*d_booleanType);
- Node b = d_nm->mkVar(*d_booleanType);
- Node c = d_nm->mkVar(*d_booleanType);
-
- Debug("cdboolattr") << "get flag 1 on a (should be F)\n";
- TS_ASSERT(! a.getAttribute(TestFlag1cd()));
- Debug("cdboolattr") << "get flag 1 on b (should be F)\n";
- TS_ASSERT(! b.getAttribute(TestFlag1cd()));
- Debug("cdboolattr") << "get flag 1 on c (should be F)\n";
- TS_ASSERT(! c.getAttribute(TestFlag1cd()));
-
- d_smtEngine->push(); // level 1
-
- // test that all boolean flags are FALSE to start
- Debug("cdboolattr") << "get flag 1 on a (should be F)\n";
- TS_ASSERT(! a.getAttribute(TestFlag1cd()));
- Debug("cdboolattr") << "get flag 1 on b (should be F)\n";
- TS_ASSERT(! b.getAttribute(TestFlag1cd()));
- Debug("cdboolattr") << "get flag 1 on c (should be F)\n";
- TS_ASSERT(! c.getAttribute(TestFlag1cd()));
-
- // test that they all HAVE the boolean attributes
- TS_ASSERT(a.hasAttribute(TestFlag1cd()));
- TS_ASSERT(b.hasAttribute(TestFlag1cd()));
- TS_ASSERT(c.hasAttribute(TestFlag1cd()));
-
- // test two-arg version of hasAttribute()
- bool bb = false;
- Debug("cdboolattr") << "get flag 1 on a (should be F)\n";
- TS_ASSERT(a.getAttribute(TestFlag1cd(), bb));
- TS_ASSERT(! bb);
- Debug("cdboolattr") << "get flag 1 on b (should be F)\n";
- TS_ASSERT(b.getAttribute(TestFlag1cd(), bb));
- TS_ASSERT(! bb);
- Debug("cdboolattr") << "get flag 1 on c (should be F)\n";
- TS_ASSERT(c.getAttribute(TestFlag1cd(), bb));
- TS_ASSERT(! bb);
-
- // setting boolean flags
- Debug("cdboolattr") << "set flag 1 on a to T\n";
- a.setAttribute(TestFlag1cd(), true);
- Debug("cdboolattr") << "set flag 1 on b to F\n";
- b.setAttribute(TestFlag1cd(), false);
- Debug("cdboolattr") << "set flag 1 on c to F\n";
- c.setAttribute(TestFlag1cd(), false);
-
- Debug("cdboolattr") << "get flag 1 on a (should be T)\n";
- TS_ASSERT(a.getAttribute(TestFlag1cd()));
- Debug("cdboolattr") << "get flag 1 on b (should be F)\n";
- TS_ASSERT(! b.getAttribute(TestFlag1cd()));
- Debug("cdboolattr") << "get flag 1 on c (should be F)\n";
- TS_ASSERT(! c.getAttribute(TestFlag1cd()));
-
- d_smtEngine->push(); // level 2
-
- Debug("cdboolattr") << "get flag 1 on a (should be T)\n";
- TS_ASSERT(a.getAttribute(TestFlag1cd()));
- Debug("cdboolattr") << "get flag 1 on b (should be F)\n";
- TS_ASSERT(! b.getAttribute(TestFlag1cd()));
- Debug("cdboolattr") << "get flag 1 on c (should be F)\n";
- TS_ASSERT(! c.getAttribute(TestFlag1cd()));
-
- Debug("cdboolattr") << "set flag 1 on a to F\n";
- a.setAttribute(TestFlag1cd(), false);
- Debug("cdboolattr") << "set flag 1 on b to T\n";
- b.setAttribute(TestFlag1cd(), true);
-
- Debug("cdboolattr") << "get flag 1 on a (should be F)\n";
- TS_ASSERT(! a.getAttribute(TestFlag1cd()));
- Debug("cdboolattr") << "get flag 1 on b (should be T)\n";
- TS_ASSERT(b.getAttribute(TestFlag1cd()));
- Debug("cdboolattr") << "get flag 1 on c (should be F)\n";
- TS_ASSERT(! c.getAttribute(TestFlag1cd()));
-
- d_smtEngine->push(); // level 3
-
- Debug("cdboolattr") << "get flag 1 on a (should be F)\n";
- TS_ASSERT(! a.getAttribute(TestFlag1cd()));
- Debug("cdboolattr") << "get flag 1 on b (should be T)\n";
- TS_ASSERT(b.getAttribute(TestFlag1cd()));
- Debug("cdboolattr") << "get flag 1 on c (should be F)\n";
- TS_ASSERT(! c.getAttribute(TestFlag1cd()));
-
- Debug("cdboolattr") << "set flag 1 on c to T\n";
- c.setAttribute(TestFlag1cd(), true);
-
- Debug("cdboolattr") << "get flag 1 on a (should be F)\n";
- TS_ASSERT(! a.getAttribute(TestFlag1cd()));
- Debug("cdboolattr") << "get flag 1 on b (should be T)\n";
- TS_ASSERT(b.getAttribute(TestFlag1cd()));
- Debug("cdboolattr") << "get flag 1 on c (should be T)\n";
- TS_ASSERT(c.getAttribute(TestFlag1cd()));
-
- d_smtEngine->pop(); // level 2
-
- Debug("cdboolattr") << "get flag 1 on a (should be F)\n";
- TS_ASSERT(! a.getAttribute(TestFlag1cd()));
- Debug("cdboolattr") << "get flag 1 on b (should be T)\n";
- TS_ASSERT(b.getAttribute(TestFlag1cd()));
- Debug("cdboolattr") << "get flag 1 on c (should be F)\n";
- TS_ASSERT(! c.getAttribute(TestFlag1cd()));
-
- d_smtEngine->pop(); // level 1
-
- Debug("cdboolattr") << "get flag 1 on a (should be T)\n";
- TS_ASSERT(a.getAttribute(TestFlag1cd()));
- Debug("cdboolattr") << "get flag 1 on b (should be F)\n";
- TS_ASSERT(! b.getAttribute(TestFlag1cd()));
- Debug("cdboolattr") << "get flag 1 on c (should be F)\n";
- TS_ASSERT(! c.getAttribute(TestFlag1cd()));
-
- d_smtEngine->pop(); // level 0
-
- Debug("cdboolattr") << "get flag 1 on a (should be F)\n";
- TS_ASSERT(! a.getAttribute(TestFlag1cd()));
- Debug("cdboolattr") << "get flag 1 on b (should be F)\n";
- TS_ASSERT(! b.getAttribute(TestFlag1cd()));
- Debug("cdboolattr") << "get flag 1 on c (should be F)\n";
- TS_ASSERT(! c.getAttribute(TestFlag1cd()));
-
- TS_ASSERT_THROWS( d_smtEngine->pop(), ModalException );
- }
-
void testAttributes() {
//Debug.on("boolattr");
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback