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