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

4 files changed, 242 insertions, 2 deletions

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 <class T>
+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 <class T>
+struct HistoryElement{
+public:
+  UpdatableElement<T> d_cached;
+  unsigned d_index;
+  HistoryElement(const UpdatableElement<T>& 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<T>.
+ */
+template <class T>
+class CDVector {
+private:
+  typedef DynamicArray< UpdatableElement<T> > CurrentVector;
+  typedef DynamicArray< HistoryElement<T> > HistoryVector;
+
+  Context* d_context;
+
+  DynamicArray< UpdatableElement<T> > d_current;
+  DynamicArray< HistoryElement<T> > d_history;
+
+  CDO<unsigned> d_historySize;
+
+
+private:
+  void restoreConsistency() {
+    Assert(d_history.size() >= d_historySize.get());
+    while(d_history.size() > d_historySize.get()) {
+      const HistoryElement<T>& 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<T>(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<T>(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 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 */