- 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().

1 files changed, 88 insertions, 0 deletions

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 */