From: Tim King Date: Mon, 27 Sep 2010 21:10:47 +0000 (+0000) Subject: - This update adds DynamicArray. This is a bare bones heap allocated array that... X-Git-Tag: cvc5-1.0.0~8848 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=595751a1814cc9375318c9c158caf6426eeda791;p=cvc5.git - This update adds DynamicArray. This is a bare bones heap allocated array that dynamically can increase in size. This has functionality similar to vector. The main difference is that it can be constructed in an ill-formed manner. This means that it can generalize CDList. - CDVector 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 >. 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>::push_back(val) sets back() at the current context level to val and back() at context level 0 to the default constructor T(). --- diff --git a/src/context/Makefile.am b/src/context/Makefile.am index 7a40bab1b..398de65a3 100644 --- a/src/context/Makefile.am +++ b/src/context/Makefile.am @@ -13,4 +13,5 @@ libcontext_la_SOURCES = \ cdo.h \ cdlist.h \ cdmap.h \ - cdset.h + cdset.h \ + cdvector.h diff --git a/src/context/cdvector.h b/src/context/cdvector.h new file mode 100644 index 000000000..cf88e2ce6 --- /dev/null +++ b/src/context/cdvector.h @@ -0,0 +1,150 @@ + + +#include "cvc4_private.h" + +#ifndef __CVC4__CONTEXT__CDVECTOR_H +#define __CVC4__CONTEXT__CDVECTOR_H + +#include "context/context.h" +#include "context/cdo.h" +#include "util/Assert.h" +#include "util/dynamic_array.h" + +namespace CVC4 { +namespace context { + +template +struct UpdatableElement{ +public: + T d_data; + int d_contextLevelOfLastUpdate; + + UpdatableElement(const T& data) : + d_data(data), + d_contextLevelOfLastUpdate(0){ + } + + // UpdatableElement() : + // d_data(), + // d_contextLevelOfLastUpdate(0){ + // } +}; + +template +struct HistoryElement{ +public: + UpdatableElement d_cached; + unsigned d_index; + HistoryElement(const UpdatableElement& cache, unsigned index) : + d_cached(cache), d_index(index) + {} + + // HistoryElement() : + // d_cached(), d_index(0) + // {} +}; + + +/** + * Generic context-dependent dynamic vector. + * It provides the ability to destructively update the i'th item. + * Note that the size of the vector never decreases. + * + * This is quite different than CDList. + */ +template +class CDVector { +private: + typedef DynamicArray< UpdatableElement > CurrentVector; + typedef DynamicArray< HistoryElement > HistoryVector; + + Context* d_context; + + DynamicArray< UpdatableElement > d_current; + DynamicArray< HistoryElement > d_history; + + CDO d_historySize; + + +private: + void restoreConsistency() { + Assert(d_history.size() >= d_historySize.get()); + while(d_history.size() > d_historySize.get()) { + const HistoryElement& back = d_history.back(); + d_current[back.d_index] = back.d_cached; + d_history.pop_back(); + } + } + + bool isConsistent() const{ + return d_history.size() == d_historySize.get(); + } + + void makeConsistent() { + if(!isConsistent()){ + restoreConsistency(); + } + Assert(isConsistent()); + } + +public: + CDVector(Context* c, bool callDestructor = false) : + d_context(c), + d_current(callDestructor), + d_history(callDestructor), + d_historySize(c,0){ + } + + unsigned size() const { + return d_current.size(); + } + + /** + * Return true iff there are no valid objects in the list. + */ + bool empty() const { + return d_current.empty(); + } + + /** + * Add an item to the end of the list. + * Assigns its state at level 0 to be equal to data. + */ + void push_back(const T& data) { + d_current.push_back(UpdatableElement(data)); + } + + /** + * Access to the ith item in the list. + */ + const T& operator[](unsigned i){ + return get(i); + } + + const T& get(unsigned i) { + Assert(i < size(), "index out of bounds in CDVector::get()"); + makeConsistent(); + return d_current[i].d_data; + } + + void set(unsigned index, const T& data){ + Assert(index < size(), "index out of bounds in CDVector::set()"); + makeConsistent(); + + if(d_current[index].d_contextLevelOfLastUpdate == d_context->getLevel() ){ + d_current[index].d_data = data; + }else{ + d_history.push_back(HistoryElement(d_current[index], index)); + d_historySize.set(d_historySize.get() + 1); + + d_current[index].d_data = data; + d_current[index].d_contextLevelOfLastUpdate = d_context->getLevel(); + } + } + +};/* class CDVector */ + +}/* CVC4::context namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__CONTEXT__CDVECTOR_H */ diff --git a/src/util/Makefile.am b/src/util/Makefile.am index e41c6effc..bac0064bf 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -34,7 +34,8 @@ libutil_la_SOURCES = \ sexpr.h \ stats.h \ stats.cpp \ - triple.h + triple.h \ + dynamic_array.h BUILT_SOURCES = \ rational.h \ diff --git a/src/util/dynamic_array.h b/src/util/dynamic_array.h new file mode 100644 index 000000000..8672fa1e9 --- /dev/null +++ b/src/util/dynamic_array.h @@ -0,0 +1,88 @@ + +#include "cvc4_private.h" + +#ifndef __CVC4__UTIL__DYNAMICARRAY_H +#define __CVC4__UTIL__DYNAMICARRAY_H + +#include "util/Assert.h" + +namespace CVC4 { + +template +class DynamicArray { +private: + T* d_arr; + unsigned d_size; + unsigned d_allocated; + + bool d_callDestructor; + + void grow(){ + bool empty = (d_arr == NULL); + d_allocated = empty ? d_allocated = 15 : d_allocated * 2 + 1; + unsigned allocSize = sizeof(T) * d_allocated; + T* tmpList = (T*) (empty ? malloc(allocSize) :realloc(d_arr, allocSize)); + if(tmpList == NULL) { + throw std::bad_alloc(); + } + d_arr = tmpList; + } + +public: + DynamicArray(bool deallocate = false): + d_arr(NULL), + d_size(0), + d_allocated(0), + d_callDestructor(deallocate){ + } + + ~DynamicArray(){ + if(d_callDestructor) { + for(unsigned i = 0; i < d_size; ++i) { + d_arr[i].~T(); + } + } + free(d_arr); + } + + + unsigned size() const{ + return d_size; + } + + bool empty() const{ + return size() == 0; + } + + void push_back(const T& data) { + if(d_size == d_allocated) { + grow(); + } + Assert(d_size < d_allocated); + + ::new((void*)(d_arr + d_size)) T(data); + ++d_size; + } + + T& operator[](unsigned i) { + Assert(i < d_size, "index out of bounds in DynamicArray::operator[]"); + return d_arr[i]; + } + + const T& back() const{ + Assert(d_size > 0, "DynamicArray::back() called on empty list"); + return d_arr[d_size - 1]; + } + + void pop_back() { + Assert(d_size > 0, "DynamicArray::back() called on empty list"); + --d_size; + if(d_callDestructor){ + d_arr[d_size].~T();; + } + } +};/* CVC4::DynamicArray */ + +}/* CVC4 namespace */ + +#endif /* __CVC4__UTIL__DYNAMICARRAY_H */ 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 + +#include +#include + +#include + +#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 copy(CDVector& v){ + vector ret; + for(unsigned i=0; i < v.size(); ++i){ + ret.push_back(v[i]); + } + return ret; + } + + void equal(vector& copy, CDVector& 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 vec(d_context, callDestructor); + vector< vector > 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 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); + } + +};