1 /*++ 2 Copyright (c) 2015 Microsoft Corporation 3 4 Module Name: 5 6 scoped_vector.h 7 8 Abstract: 9 10 Vector that restores during backtracking. 11 12 Author: 13 14 Nikolaj Bjorner (nbjorner) 2015-12-13 15 16 Revision History: 17 18 --*/ 19 #pragma once 20 21 #include "util/vector.h" 22 23 template<typename T> 24 class scoped_vector { 25 unsigned m_size = 0; 26 unsigned m_elems_start = 0; 27 unsigned_vector m_sizes; 28 vector<T> m_elems; 29 unsigned_vector m_elems_lim; 30 unsigned_vector m_index; 31 unsigned_vector m_src, m_dst; 32 unsigned_vector m_src_lim; 33 public: 34 // m_index : External-Index -> Internal-Index 35 // m_index.size() = max(m_sizes) 36 // m_src[i] -> m_dst[i] // trail into m_index updates 37 // m_src_lim last index to be updated. 38 push_scope()39 void push_scope() { 40 m_elems_start = m_elems.size(); 41 m_sizes.push_back(m_size); 42 m_src_lim.push_back(m_src.size()); 43 m_elems_lim.push_back(m_elems_start); 44 } 45 pop_scope(unsigned num_scopes)46 void pop_scope(unsigned num_scopes) { 47 if (num_scopes == 0) return; 48 unsigned new_size = m_sizes.size() - num_scopes; 49 unsigned src_lim = m_src_lim[new_size]; 50 51 for (unsigned i = m_src.size(); i > src_lim; ) { 52 --i; 53 m_index[m_src[i]] = m_dst[i]; 54 } 55 m_src.shrink(src_lim); 56 m_dst.shrink(src_lim); 57 m_src_lim.shrink(new_size); 58 59 m_elems.shrink(m_elems_lim[new_size]); 60 m_elems_lim.resize(new_size); 61 m_elems_start = m_elems.size(); 62 63 m_size = m_sizes[new_size]; 64 m_sizes.shrink(new_size); 65 } 66 67 T const& operator[](unsigned idx) const { 68 SASSERT(idx < m_size); 69 return m_elems[m_index[idx]]; 70 } 71 72 // breaks abstraction, caller must ensure backtracking. ref(unsigned idx)73 T& ref(unsigned idx) { 74 SASSERT(idx < m_size); 75 return m_elems[m_index[idx]]; 76 } 77 set(unsigned idx,T const & t)78 void set(unsigned idx, T const& t) { 79 SASSERT(idx < m_size); 80 unsigned n = m_index[idx]; 81 if (n >= m_elems_start) { 82 m_elems[n] = t; 83 } 84 else { 85 set_index(idx, m_elems.size()); 86 m_elems.push_back(t); 87 } 88 SASSERT(invariant()); 89 } 90 set(unsigned idx,T && t)91 void set(unsigned idx, T && t) { 92 SASSERT(idx < m_size); 93 unsigned n = m_index[idx]; 94 if (n >= m_elems_start) { 95 m_elems[n] = std::move(t); 96 } 97 else { 98 set_index(idx, m_elems.size()); 99 m_elems.push_back(std::move(t)); 100 } 101 SASSERT(invariant()); 102 } 103 104 class iterator { 105 scoped_vector const& m_vec; 106 unsigned m_index; 107 public: iterator(scoped_vector const & v,unsigned idx)108 iterator(scoped_vector const& v, unsigned idx): m_vec(v), m_index(idx) {} 109 110 bool operator==(iterator const& other) const { return &other.m_vec == &m_vec && other.m_index == m_index; } 111 bool operator!=(iterator const& other) const { return &other.m_vec != &m_vec || other.m_index != m_index; } 112 T const& operator*() { return m_vec[m_index]; } 113 114 iterator & operator++() { 115 ++m_index; 116 return *this; 117 } 118 119 iterator operator++(int) { 120 iterator r = *this; 121 ++m_index; 122 return r; 123 } 124 }; 125 begin()126 iterator begin() const { return iterator(*this, 0); } end()127 iterator end() const { return iterator(*this, m_size); } 128 push_back(T const & t)129 void push_back(T const& t) { 130 set_index(m_size, m_elems.size()); 131 m_elems.push_back(t); 132 ++m_size; 133 SASSERT(invariant()); 134 } 135 push_back(T && t)136 void push_back(T && t) { 137 set_index(m_size, m_elems.size()); 138 m_elems.push_back(std::move(t)); 139 ++m_size; 140 SASSERT(invariant()); 141 } 142 pop_back()143 void pop_back() { 144 SASSERT(m_size > 0); 145 if (m_index[m_size-1] == m_elems.size()-1 && 146 m_elems.size() > m_elems_start) { 147 m_elems.pop_back(); 148 } 149 --m_size; 150 SASSERT(invariant()); 151 } 152 erase_and_swap(unsigned i)153 void erase_and_swap(unsigned i) { 154 if (i + 1 < size()) { 155 auto n = m_elems[m_index[size() - 1]]; 156 set(i, std::move(n)); 157 } 158 pop_back(); 159 } 160 size()161 unsigned size() const { return m_size; } 162 empty()163 bool empty() const { return m_size == 0; } 164 165 private: set_index(unsigned src,unsigned dst)166 void set_index(unsigned src, unsigned dst) { 167 while (src >= m_index.size()) { 168 m_index.push_back(0); 169 } 170 SASSERT(src < m_index.size()); 171 if (src < m_elems_start) { 172 m_src.push_back(src); 173 m_dst.push_back(m_index[src]); 174 } 175 m_index[src] = dst; 176 } 177 invariant()178 bool invariant() const { 179 return 180 m_size <= m_elems.size() && 181 m_elems_start <= m_elems.size(); 182 } 183 }; 184