1 files changed, 60 insertions, 15 deletions

diff --git a/src/util/dynamic_array.h b/src/util/dynamic_array.h
index c0a8cf260..2c8b842e4 100644
--- a/src/util/dynamic_array.h
+++ b/src/util/dynamic_array.h
@@ -2,10 +2,10 @@
 /*! \file dynamic_array.h
  ** \verbatim
  ** Original author: taking
- ** Major contributors: none
+ ** Major contributors: mdeters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
@@ -17,11 +17,10 @@
  ** \todo document this file
  **/
 
-
 #include "cvc4_private.h"
 
-#ifndef __CVC4__UTIL__DYNAMICARRAY_H
-#define __CVC4__UTIL__DYNAMICARRAY_H
+#ifndef __CVC4__UTIL__DYNAMIC_ARRAY_H
+#define __CVC4__UTIL__DYNAMIC_ARRAY_H
 
 #include "util/Assert.h"
 
@@ -29,14 +28,14 @@ namespace CVC4 {
 
 template <class T>
 class DynamicArray {
-private:
+protected:
   T* d_arr;
   unsigned d_size;
   unsigned d_allocated;
 
   bool d_callDestructor;
 
-  void grow(){
+  void grow() {
     bool empty = (d_arr == NULL);
     d_allocated = empty ? 15 : d_allocated * 2 + 1;
     unsigned allocSize = sizeof(T) * d_allocated;
@@ -48,14 +47,14 @@ private:
   }
 
 public:
-  DynamicArray(bool deallocate = false):
+  DynamicArray(bool callDestructor = false) :
     d_arr(NULL),
     d_size(0),
     d_allocated(0),
-    d_callDestructor(deallocate){
+    d_callDestructor(callDestructor) {
   }
 
-  ~DynamicArray(){
+  virtual ~DynamicArray() {
     if(d_callDestructor) {
       for(unsigned i = 0; i < d_size; ++i) {
         d_arr[i].~T();
@@ -83,12 +82,17 @@ public:
     ++d_size;
   }
 
+  const T& operator[](unsigned i) const {
+    Assert(i < d_size, "index out of bounds in DynamicArray::operator[]");
+    return d_arr[i];
+  }
+
   T& operator[](unsigned i) {
     Assert(i < d_size, "index out of bounds in DynamicArray::operator[]");
     return d_arr[i];
   }
 
-  const T& back() const{
+  const T& back() const {
     Assert(d_size > 0, "DynamicArray::back() called on empty list");
     return d_arr[d_size - 1];
   }
@@ -96,12 +100,53 @@ public:
   void pop_back() {
     Assert(d_size > 0, "DynamicArray::back() called on empty list");
     --d_size;
-    if(d_callDestructor){
-      d_arr[d_size].~T();;
+    if(d_callDestructor) {
+      d_arr[d_size].~T();
+    }
+  }
+
+  typedef T* iterator;
+  typedef const T* const_iterator;
+
+  iterator begin() { return d_arr; }
+  iterator end() { return d_arr + d_size; }
+  const_iterator begin() const { return d_arr; }
+  const_iterator end() const { return d_arr + d_size; }
+
+};/* class DynamicArray<T> */
+
+template <class T, class Ctor = T>
+class DynamicGrowingArray : public DynamicArray<T> {
+  Ctor d_ctor;
+
+public:
+  DynamicGrowingArray(bool callDestructor, const Ctor& c) :
+    DynamicArray<T>(callDestructor),
+    d_ctor(c) {
+  }
+
+  DynamicGrowingArray(bool callDestructor = false) :
+    DynamicArray<T>(callDestructor),
+    d_ctor() {
+  }
+
+  T& operator[](unsigned i) {
+    while(this->d_allocated <= i) {
+      this->grow();
+    }
+    while(this->d_size <= i) {
+      ::new((void*)(this->d_arr + this->d_size)) T(d_ctor);
+      ++this->d_size;
     }
+    return this->d_arr[i];
+  }
+
+  const T& operator[](unsigned i) const {
+    Assert(this->d_size > i);
+    return this->d_arr[i];
   }
-};/* CVC4::DynamicArray */
+};/* CVC4::DynamicGrowingArray */
 
 }/* CVC4 namespace */
 
-#endif /* __CVC4__UTIL__DYNAMICARRAY_H */
+#endif /* __CVC4__UTIL__DYNAMIC_ARRAY_H */