- 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().
cdo.h \
cdlist.h \
cdmap.h \
- cdset.h
+ cdset.h \
+ cdvector.h
--- /dev/null
+
+
+#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 */
sexpr.h \
stats.h \
stats.cpp \
- triple.h
+ triple.h \
+ dynamic_array.h
BUILT_SOURCES = \
rational.h \
--- /dev/null
+
+#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 */
context/cdlist_black \
context/cdmap_black \
context/cdmap_white \
+ context/cdvector_black \
util/assert_white \
util/bitvector_black \
util/configuration_black \
--- /dev/null
+
+#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);
+ }
+
+};
projects / cvc5.git / commitdiff