diff options
author | Tim King <taking@cs.nyu.edu> | 2010-09-27 21:10:47 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2010-09-27 21:10:47 +0000 |
commit | 595751a1814cc9375318c9c158caf6426eeda791 (patch) | |
tree | 91cd27f6f3de253cea4c8350307d0c8a0ee5383e /test | |
parent | 6e59b60947283d864877c2c2dc883e878913a2d8 (diff) |
- This update adds DynamicArray<T>. This is a bare bones heap allocated array that dynamically can increase in size. This has functionality similar to vector<T>. The main difference is that it can be constructed in an ill-formed manner. This means that it can generalize CDList<T>.
- CDVector<T> has been added. This is intended to allow for context-dependent destructive updates, while the vector size increases are permanent. Behaviorally, this is most similar to vector< CDO<T> >. The differences between the two are: only one ContextObj is registered to the Context, backtracks are done in a lazy fashion, CDVector::push_back(val) sets the value of back() at context level 0 to val where vector<CDO<T>>::push_back(val) sets back() at the current context level to val and back() at context level 0 to the default constructor T().
Diffstat (limited to 'test')
-rw-r--r-- | test/unit/Makefile.am | 1 | ||||
-rw-r--r-- | test/unit/context/cdvector_black.h | 127 |
2 files changed, 128 insertions, 0 deletions
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index 1272be069..d5bf66496 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -26,6 +26,7 @@ UNIT_TESTS = \ context/cdlist_black \ context/cdmap_black \ context/cdmap_white \ + context/cdvector_black \ util/assert_white \ util/bitvector_black \ util/configuration_black \ diff --git a/test/unit/context/cdvector_black.h b/test/unit/context/cdvector_black.h new file mode 100644 index 000000000..8deac3fb3 --- /dev/null +++ b/test/unit/context/cdvector_black.h @@ -0,0 +1,127 @@ + +#include <cxxtest/TestSuite.h> + +#include <vector> +#include <iostream> + +#include <limits.h> + +#include "memory.h" + +#include "context/context.h" +#include "context/cdvector.h" + +using namespace std; +using namespace CVC4::context; +using namespace CVC4::test; + +struct DtorSensitiveObject { + bool& d_dtorCalled; + DtorSensitiveObject(bool& dtorCalled) : d_dtorCalled(dtorCalled) {} + ~DtorSensitiveObject() { d_dtorCalled = true; } +}; + + + +class CDListBlack : public CxxTest::TestSuite { +private: + + Context* d_context; + +public: + + void setUp() { + d_context = new Context(); + } + + void tearDown() { + delete d_context; + } + + void testCDVector17() { vectorTest(17); } + void testCDVector31() { vectorTest(31); } + void testCDVector191() { vectorTest(113); } + + void vectorTest(unsigned P){ + vectorTest(P, 2); + vectorTest(P, 5); + vectorTest(P, P/3 + 1); + } + + void vectorTest(unsigned P, unsigned m){ + for(unsigned g=2; g< P; g++){ + vectorTest(P, g, m, 1, false); + vectorTest(P, g, m, 3, false); + } + } + vector<unsigned> copy(CDVector<unsigned>& v){ + vector<unsigned> ret; + for(unsigned i=0; i < v.size(); ++i){ + ret.push_back(v[i]); + } + return ret; + } + + void equal(vector<unsigned>& copy, CDVector<unsigned>& v){ + TS_ASSERT_EQUALS(copy.size(), v.size()); + for(unsigned i = 0; i < v.size(); ++i){ + TS_ASSERT_EQUALS(copy[i], v[i]); + } + } + + void vectorTest(unsigned P, unsigned g, unsigned m, unsigned r, bool callDestructor) { + CDVector<unsigned> vec(d_context, callDestructor); + vector< vector<unsigned> > copies; + + copies.push_back( copy(vec) ); + d_context->push(); + + TS_ASSERT(vec.empty()); + for(unsigned i = 0; i < P; ++i){ + vec.push_back(i); + TS_ASSERT_EQUALS(vec.size(), i+1); + } + TS_ASSERT(!vec.empty()); + TS_ASSERT_EQUALS(vec.size(), P); + + copies.push_back( copy(vec) ); + d_context->push(); + + for(unsigned i = 0, g_i = 1; i < r*P; ++i, g_i = (g_i * g)% P){ + if(i % m == 0){ + copies.push_back( copy(vec) ); + d_context->push(); + } + + vec.set(g_i, i); + + TS_ASSERT_EQUALS(vec.get(g_i), i); + } + TS_ASSERT_EQUALS(vec.size(), P); + + copies.push_back( copy(vec) ); + + while(d_context->getLevel() >= 1){ + TS_ASSERT_EQUALS(vec.size(), P); + equal(copies[d_context->getLevel()], vec); + d_context->pop(); + } + } + + void testTreeUpdate() { + CDVector<int> vec(d_context); + vec.push_back(-1); + + vec.set(0, 0); + d_context->push(); + d_context->push(); + vec.set(0, 1); + d_context->pop(); + d_context->pop(); + + d_context->push(); + d_context->push(); + TS_ASSERT_EQUALS(vec.get(0), 0); + } + +}; |