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 /src/util | |
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 'src/util')
-rw-r--r-- | src/util/Makefile.am | 3 | ||||
-rw-r--r-- | src/util/dynamic_array.h | 88 |
2 files changed, 90 insertions, 1 deletions
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 T> +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 */ |