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; 26 unsigned m_elems_start; 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: scoped_vector()34 scoped_vector(): m_size(0), m_elems_start(0) {} 35 36 // m_index : External-Index -> Internal-Index 37 // m_index.size() = max(m_sizes) 38 // m_src[i] -> m_dst[i] // trail into m_index updates 39 // m_src_lim last index to be updated. 40 push_scope()41 void push_scope() { 42 m_elems_start = m_elems.size(); 43 m_sizes.push_back(m_size); 44 m_src_lim.push_back(m_src.size()); 45 m_elems_lim.push_back(m_elems_start); 46 } 47 pop_scope(unsigned num_scopes)48 void pop_scope(unsigned num_scopes) { 49 if (num_scopes == 0) return; 50 unsigned new_size = m_sizes.size() - num_scopes; 51 unsigned src_lim = m_src_lim[new_size]; 52 53 for (unsigned i = m_src.size(); i > src_lim; ) { 54 --i; 55 m_index[m_src[i]] = m_dst[i]; 56 } 57 m_src.shrink(src_lim); 58 m_dst.shrink(src_lim); 59 m_src_lim.shrink(new_size); 60 61 m_elems.shrink(m_elems_lim[new_size]); 62 m_elems_lim.resize(new_size); 63 m_elems_start = m_elems.size(); 64 65 m_size = m_sizes[new_size]; 66 m_sizes.shrink(new_size); 67 } 68 69 T const& operator[](unsigned idx) const { 70 SASSERT(idx < m_size); 71 return m_elems[m_index[idx]]; 72 } 73 74 // breaks abstraction, caller must ensure backtracking. ref(unsigned idx)75 T& ref(unsigned idx) { 76 SASSERT(idx < m_size); 77 return m_elems[m_index[idx]]; 78 } 79 set(unsigned idx,T const & t)80 void set(unsigned idx, T const& t) { 81 SASSERT(idx < m_size); 82 unsigned n = m_index[idx]; 83 if (n >= m_elems_start) { 84 m_elems[n] = t; 85 } 86 else { 87 set_index(idx, m_elems.size()); 88 m_elems.push_back(t); 89 } 90 SASSERT(invariant()); 91 } 92 set(unsigned idx,T && t)93 void set(unsigned idx, T && t) { 94 SASSERT(idx < m_size); 95 unsigned n = m_index[idx]; 96 if (n >= m_elems_start) { 97 m_elems[n] = std::move(t); 98 } 99 else { 100 set_index(idx, m_elems.size()); 101 m_elems.push_back(std::move(t)); 102 } 103 SASSERT(invariant()); 104 } 105 106 class iterator { 107 scoped_vector const& m_vec; 108 unsigned m_index; 109 public: iterator(scoped_vector const & v,unsigned idx)110 iterator(scoped_vector const& v, unsigned idx): m_vec(v), m_index(idx) {} 111 112 bool operator==(iterator const& other) const { return &other.m_vec == &m_vec && other.m_index == m_index; } 113 bool operator!=(iterator const& other) const { return &other.m_vec != &m_vec || other.m_index != m_index; } 114 T const& operator*() { return m_vec[m_index]; } 115 116 iterator & operator++() { 117 ++m_index; 118 return *this; 119 } 120 121 iterator operator++(int) { 122 iterator r = *this; 123 ++m_index; 124 return r; 125 } 126 }; 127 begin()128 iterator begin() const { return iterator(*this, 0); } end()129 iterator end() const { return iterator(*this, m_size); } 130 push_back(T const & t)131 void push_back(T const& t) { 132 set_index(m_size, m_elems.size()); 133 m_elems.push_back(t); 134 ++m_size; 135 SASSERT(invariant()); 136 } 137 push_back(T && t)138 void push_back(T && t) { 139 set_index(m_size, m_elems.size()); 140 m_elems.push_back(std::move(t)); 141 ++m_size; 142 SASSERT(invariant()); 143 } 144 pop_back()145 void pop_back() { 146 SASSERT(m_size > 0); 147 if (m_index[m_size-1] == m_elems.size()-1 && 148 m_elems.size() > m_elems_start) { 149 m_elems.pop_back(); 150 } 151 --m_size; 152 SASSERT(invariant()); 153 } 154 erase_and_swap(unsigned i)155 void erase_and_swap(unsigned i) { 156 if (i + 1 < size()) { 157 auto n = m_elems[m_index[size() - 1]]; 158 set(i, std::move(n)); 159 } 160 pop_back(); 161 } 162 size()163 unsigned size() const { return m_size; } 164 empty()165 bool empty() const { return m_size == 0; } 166 167 private: set_index(unsigned src,unsigned dst)168 void set_index(unsigned src, unsigned dst) { 169 while (src >= m_index.size()) { 170 m_index.push_back(0); 171 } 172 SASSERT(src < m_index.size()); 173 if (src < m_elems_start) { 174 m_src.push_back(src); 175 m_dst.push_back(m_index[src]); 176 } 177 m_index[src] = dst; 178 } 179 invariant()180 bool invariant() const { 181 return 182 m_size <= m_elems.size() && 183 m_elems_start <= m_elems.size(); 184 } 185 }; 186 187