summaryrefslogtreecommitdiff
path: root/test/unit/context
diff options
context:
space:
mode:
Diffstat (limited to 'test/unit/context')
-rw-r--r--test/unit/context/cdmap_black.h398
-rw-r--r--test/unit/context/cdo_black.h57
-rw-r--r--test/unit/context/context_black.h14
3 files changed, 455 insertions, 14 deletions
diff --git a/test/unit/context/cdmap_black.h b/test/unit/context/cdmap_black.h
new file mode 100644
index 000000000..7040e4cc1
--- /dev/null
+++ b/test/unit/context/cdmap_black.h
@@ -0,0 +1,398 @@
+/********************* */
+/** cdmap_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::context::CDMap<>.
+ **/
+
+#include <cxxtest/TestSuite.h>
+
+#include "context/cdmap.h"
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::context;
+
+class CDMapBlack : public CxxTest::TestSuite {
+
+ Context* d_context;
+
+public:
+
+ void setUp() {
+ d_context = new Context;
+ //Debug.on("cdmap");
+ }
+
+ void tearDown() {
+ delete d_context;
+ }
+
+ void testSimpleSequence() {
+ CDMap<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());
+
+ {
+ 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());
+
+ 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());
+
+ {
+ 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());
+
+ 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());
+
+ {
+ 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());
+
+ 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());
+
+ 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());
+
+ 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());
+
+ 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());
+ }
+
+ // no intervening find() in this one
+ // (under the theory that this could trigger a bug)
+ void testSimpleSequenceFewerFinds() {
+ CDMap<int, int> map(d_context);
+
+ map.insert(3, 4);
+
+ {
+ d_context->push();
+
+ map.insert(5, 6);
+ map.insert(9, 8);
+
+ {
+ d_context->push();
+
+ 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());
+
+ {
+ d_context->push();
+
+ d_context->pop();
+ }
+
+ d_context->pop();
+ }
+
+ d_context->pop();
+ }
+ }
+
+ void testObliterate() {
+ CDMap<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());
+
+ {
+ 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());
+
+ 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());
+
+ {
+ 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());
+
+ 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());
+
+ 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());
+
+ {
+ 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());
+
+ 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());
+
+ 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());
+
+ 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 testObliteratePrimordial() {
+ CDMap<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());
+
+ {
+ 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());
+
+ 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());
+
+ {
+ 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());
+
+ 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());
+
+ 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());
+
+ {
+ 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());
+
+ 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());
+
+ 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());
+
+ 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() {
+ CDMap<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());
+
+ {
+ 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());
+
+ 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());
+
+ {
+ 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());
+
+ 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());
+
+ 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());
+
+ {
+ 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());
+
+ 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());
+
+ 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());
+
+ 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());
+ }
+};
diff --git a/test/unit/context/cdo_black.h b/test/unit/context/cdo_black.h
new file mode 100644
index 000000000..4cdb8f343
--- /dev/null
+++ b/test/unit/context/cdo_black.h
@@ -0,0 +1,57 @@
+/********************* */
+/** cdo_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::context::CDO<>.
+ **/
+
+#include <cxxtest/TestSuite.h>
+
+#include <vector>
+#include <iostream>
+#include "context/context.h"
+#include "context/cdlist.h"
+#include "context/cdo.h"
+#include "util/Assert.h"
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::context;
+
+class CDOBlack : public CxxTest::TestSuite {
+private:
+
+ Context* d_context;
+
+public:
+
+ void setUp() {
+ d_context = new Context;
+ }
+
+ void tearDown() {
+ delete d_context;
+ }
+
+ void testIntCDO() {
+ // Test that push/pop maintains the original value
+ CDO<int> a1(d_context);
+ a1 = 5;
+ TS_ASSERT(d_context->getLevel() == 0);
+ d_context->push();
+ a1 = 10;
+ TS_ASSERT(d_context->getLevel() == 1);
+ TS_ASSERT(a1 == 10);
+ d_context->pop();
+ TS_ASSERT(d_context->getLevel() == 0);
+ TS_ASSERT(a1 == 5);
+ }
+};
diff --git a/test/unit/context/context_black.h b/test/unit/context/context_black.h
index c9b47e400..338c09849 100644
--- a/test/unit/context/context_black.h
+++ b/test/unit/context/context_black.h
@@ -41,20 +41,6 @@ public:
delete d_context;
}
- void testIntCDO() {
- // Test that push/pop maintains the original value
- CDO<int> a1(d_context);
- a1 = 5;
- TS_ASSERT(d_context->getLevel() == 0);
- d_context->push();
- a1 = 10;
- TS_ASSERT(d_context->getLevel() == 1);
- TS_ASSERT(a1 == 10);
- d_context->pop();
- TS_ASSERT(d_context->getLevel() == 0);
- TS_ASSERT(a1 == 5);
- }
-
void testContextPushPop() {
// Test what happens when the context is popped below 0
// the interface doesn't declare any exceptions
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback