src/context/cdvector.h

   1 /*********************                                                        */
   2 /*! \file cdvector.h
   3  ** \verbatim
   4  ** Original author: taking
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
   9  ** Courant Institute of Mathematical Sciences
  10  ** New York University
  11  ** See the file COPYING in the top-level source directory for licensing
  12  ** information.\endverbatim
  13  **
  14  ** \brief [[ Add one-line brief description here ]]
  15  **
  16  ** [[ Add lengthier description here ]]
  17  ** \todo document this file
  18  **/
  19
  20 #include "cvc4_private.h"
  21
  22 #ifndef __CVC4__CONTEXT__CDVECTOR_H
  23 #define __CVC4__CONTEXT__CDVECTOR_H
  24
  25 #include "context/context.h"
  26 #include "context/cdo.h"
  27 #include "util/Assert.h"
  28 #include "util/dynamic_array.h"
  29
  30 namespace CVC4 {
  31 namespace context {
  32
  33 template <class T>
  34 struct UpdatableElement {
  35 public:
  36   T d_data;
  37   int d_contextLevelOfLastUpdate;
  38
  39   UpdatableElement(const T& data) :
  40     d_data(data),
  41     d_contextLevelOfLastUpdate(0) {
  42   }
  43 };/* struct UpdatableElement<T> */
  44
  45 template <class T>
  46 struct HistoryElement {
  47 public:
  48   UpdatableElement<T> d_cached;
  49   unsigned d_index;
  50   HistoryElement(const UpdatableElement<T>& cache, unsigned index) :
  51     d_cached(cache), d_index(index) {
  52   }
  53 };/* struct HistoryElement<T> */
  54
  55
  56 /**
  57  * Generic context-dependent dynamic vector.
  58  * It provides the ability to destructively update the i'th item.
  59  * Note that the size of the vector never decreases.
  60  *
  61  * This is quite different than CDList<T>.
  62  */
  63 template <class T>
  64 class CDVector {
  65 private:
  66   typedef DynamicArray< UpdatableElement<T> > CurrentVector;
  67   typedef DynamicArray< HistoryElement<T> > HistoryVector;
  68
  69   Context* d_context;
  70
  71   DynamicArray< UpdatableElement<T> > d_current;
  72   DynamicArray< HistoryElement<T> > d_history;
  73
  74   CDO<unsigned> d_historySize;
  75
  76 private:
  77   void restoreConsistency() {
  78     Assert(d_history.size() >= d_historySize.get());
  79     while(d_history.size() > d_historySize.get()) {
  80       const HistoryElement<T>& back = d_history.back();
  81       d_current[back.d_index] = back.d_cached;
  82       d_history.pop_back();
  83     }
  84   }
  85
  86   bool isConsistent() const {
  87     return d_history.size() == d_historySize.get();
  88   }
  89
  90   void makeConsistent() {
  91     if(!isConsistent()) {
  92       restoreConsistency();
  93     }
  94     Assert(isConsistent());
  95   }
  96
  97 public:
  98   CDVector(Context* c, bool callDestructor = false) :
  99     d_context(c),
 100     d_current(callDestructor),
 101     d_history(callDestructor),
 102     d_historySize(c, 0) {
 103   }
 104
 105   unsigned size() const {
 106     return d_current.size();
 107   }
 108
 109   /**
 110    * Return true iff there are no valid objects in the list.
 111    */
 112   bool empty() const {
 113     return d_current.empty();
 114   }
 115
 116   /**
 117    * Add an item to the end of the list.
 118    * Assigns its state at level 0 to be equal to data.
 119    */
 120   void push_back(const T& data) {
 121     d_current.push_back(UpdatableElement<T>(data));
 122   }
 123
 124   /**
 125    * Access to the ith item in the list.
 126    */
 127   const T& operator[](unsigned i) {
 128     return get(i);
 129   }
 130
 131   const T& get(unsigned i) {
 132     Assert(i < size(), "index out of bounds in CDVector::get()");
 133     makeConsistent();
 134     return d_current[i].d_data;
 135   }
 136
 137   void set(unsigned index, const T& data) {
 138     Assert(index < size(), "index out of bounds in CDVector::set()");
 139     makeConsistent();
 140
 141     if(d_current[index].d_contextLevelOfLastUpdate == d_context->getLevel()) {
 142       d_current[index].d_data = data;
 143     }else{
 144       d_history.push_back(HistoryElement<T>(d_current[index], index));
 145       d_historySize.set(d_historySize.get() + 1);
 146
 147       d_current[index].d_data = data;
 148       d_current[index].d_contextLevelOfLastUpdate = d_context->getLevel();
 149     }
 150   }
 151
 152 };/* class CDVector<T> */
 153
 154 }/* CVC4::context namespace */
 155 }/* CVC4 namespace */
 156
 157 #endif /* __CVC4__CONTEXT__CDVECTOR_H */