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