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

6 files changed, 370 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 */
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);
+  }
+
+};