3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00

simplify some constructors/destructors

This commit is contained in:
Nuno Lopes 2021-05-23 12:39:49 +01:00
parent 79201e5ce6
commit 9eb566b401
3 changed files with 11 additions and 49 deletions

View file

@ -81,7 +81,7 @@ public:
} }
} }
buffer(buffer && source) { buffer(buffer && source) noexcept {
if (source.m_buffer == reinterpret_cast<T*>(source.m_initial_buffer)) { if (source.m_buffer == reinterpret_cast<T*>(source.m_initial_buffer)) {
for (unsigned i = 0, sz = source.size(); i < sz; ++i) { for (unsigned i = 0, sz = source.size(); i < sz; ++i) {
push_back(std::move(source.m_buffer[i])); push_back(std::move(source.m_buffer[i]));

View file

@ -22,8 +22,8 @@ Revision History:
template<typename T> template<typename T>
class scoped_vector { class scoped_vector {
unsigned m_size; unsigned m_size = 0;
unsigned m_elems_start; unsigned m_elems_start = 0;
unsigned_vector m_sizes; unsigned_vector m_sizes;
vector<T> m_elems; vector<T> m_elems;
unsigned_vector m_elems_lim; unsigned_vector m_elems_lim;
@ -31,8 +31,6 @@ class scoped_vector {
unsigned_vector m_src, m_dst; unsigned_vector m_src, m_dst;
unsigned_vector m_src_lim; unsigned_vector m_src_lim;
public: public:
scoped_vector(): m_size(0), m_elems_start(0) {}
// m_index : External-Index -> Internal-Index // m_index : External-Index -> Internal-Index
// m_index.size() = max(m_sizes) // m_index.size() = max(m_sizes)
// m_src[i] -> m_dst[i] // trail into m_index updates // m_src[i] -> m_dst[i] // trail into m_index updates
@ -183,4 +181,3 @@ private:
m_elems_start <= m_elems.size(); m_elems_start <= m_elems.size();
} }
}; };

View file

@ -26,8 +26,7 @@ Revision History:
class trail { class trail {
public: public:
virtual ~trail() { virtual ~trail() {}
}
virtual void undo() = 0; virtual void undo() = 0;
}; };
@ -48,9 +47,6 @@ public:
m_value = new_value; m_value = new_value;
} }
~value_trail() override {
}
void undo() override { void undo() override {
m_value = m_old_value; m_value = m_old_value;
} }
@ -69,9 +65,6 @@ public:
m_values(values) { m_values(values) {
} }
~scoped_value_trail() override {
}
void undo() override { void undo() override {
m_value = m_values.back(); m_value = m_values.back();
m_values.pop_back(); m_values.pop_back();
@ -86,9 +79,6 @@ public:
m_value(value) { m_value(value) {
} }
~reset_flag_trail() override {
}
void undo() override { void undo() override {
m_value = false; m_value = false;
} }
@ -121,8 +111,7 @@ public:
m_vector(v), m_vector(v),
m_old_size(v.size()) { m_old_size(v.size()) {
} }
~restore_size_trail() override {
}
void undo() override { void undo() override {
m_vector.shrink(m_old_size); m_vector.shrink(m_old_size);
} }
@ -140,9 +129,6 @@ public:
m_old_value(v[idx]) { m_old_value(v[idx]) {
} }
~vector_value_trail() override {
}
void undo() override { void undo() override {
m_vector[m_idx] = m_old_value; m_vector[m_idx] = m_old_value;
} }
@ -162,9 +148,6 @@ public:
m_old_value(v[i][j]) { m_old_value(v[i][j]) {
} }
~vector2_value_trail() override {
}
void undo() override { void undo() override {
m_vector[m_i][m_j] = m_old_value; m_vector[m_i][m_j] = m_old_value;
} }
@ -177,7 +160,6 @@ class insert_obj_map : public trail {
D* m_obj; D* m_obj;
public: public:
insert_obj_map(obj_map<D,R>& t, D* o) : m_map(t), m_obj(o) {} insert_obj_map(obj_map<D,R>& t, D* o) : m_map(t), m_obj(o) {}
~insert_obj_map() override {}
void undo() override { m_map.remove(m_obj); } void undo() override { m_map.remove(m_obj); }
}; };
@ -188,7 +170,6 @@ class remove_obj_map : public trail {
R m_value; R m_value;
public: public:
remove_obj_map(obj_map<D,R>& t, D* o, R v) : m_map(t), m_obj(o), m_value(v) {} remove_obj_map(obj_map<D,R>& t, D* o, R v) : m_map(t), m_obj(o), m_value(v) {}
~remove_obj_map() override {}
void undo() override { m_map.insert(m_obj, m_value); } void undo() override { m_map.insert(m_obj, m_value); }
}; };
@ -198,7 +179,6 @@ class insert_map : public trail {
D m_obj; D m_obj;
public: public:
insert_map(M& t, D o) : m_map(t), m_obj(o) {} insert_map(M& t, D o) : m_map(t), m_obj(o) {}
~insert_map() override {}
void undo() override { m_map.remove(m_obj); } void undo() override { m_map.remove(m_obj); }
}; };
@ -210,8 +190,7 @@ class insert_ref_map : public trail {
D m_obj; D m_obj;
public: public:
insert_ref_map(Mgr& m, M& t, D o) : m(m), m_map(t), m_obj(o) {} insert_ref_map(Mgr& m, M& t, D o) : m(m), m_map(t), m_obj(o) {}
virtual ~insert_ref_map() {} void undo() override { m_map.remove(m_obj); m.dec_ref(m_obj); }
virtual void undo() { m_map.remove(m_obj); m.dec_ref(m_obj); }
}; };
template<typename Mgr, typename D, typename R> template<typename Mgr, typename D, typename R>
@ -222,8 +201,7 @@ class insert_ref2_map : public trail {
R* m_val; R* m_val;
public: public:
insert_ref2_map(Mgr& m, obj_map<D,R*>& t, D*o, R*r) : m(m), m_map(t), m_obj(o), m_val(r) {} insert_ref2_map(Mgr& m, obj_map<D,R*>& t, D*o, R*r) : m(m), m_map(t), m_obj(o), m_val(r) {}
virtual ~insert_ref2_map() {} void undo() override { m_map.remove(m_obj); m.dec_ref(m_obj); m.dec_ref(m_val); }
virtual void undo() { m_map.remove(m_obj); m.dec_ref(m_obj); m.dec_ref(m_val); }
}; };
@ -250,9 +228,6 @@ public:
m_idx(idx) { m_idx(idx) {
} }
~set_vector_idx_trail() override {
}
void undo() override { void undo() override {
m_vector[m_idx] = nullptr; m_vector[m_idx] = nullptr;
} }
@ -286,7 +261,7 @@ public:
m_value(m_vector[index].back()) { m_value(m_vector[index].back()) {
} }
virtual void undo() { void undo() override {
m_vector[m_index].push_back(m_value); m_vector[m_index].push_back(m_value);
} }
}; };
@ -317,7 +292,7 @@ public:
m_index(index) { m_index(index) {
} }
virtual void undo() { void undo() override {
m_vector[m_index].pop_back(); m_vector[m_index].pop_back();
} }
}; };
@ -351,9 +326,6 @@ public:
m_idx(idx), m_idx(idx),
m_hist(hist) {} m_hist(hist) {}
~history_trail() override {
}
void undo() override { void undo() override {
m_dst[m_idx] = m_hist.back(); m_dst[m_idx] = m_hist.back();
m_hist.pop_back(); m_hist.pop_back();
@ -382,7 +354,7 @@ public:
m_obj(obj) { m_obj(obj) {
} }
virtual void undo() { void undo() override {
m_obj.reset(); m_obj.reset();
} }
}; };
@ -393,7 +365,6 @@ class insert_obj_trail : public trail {
T* m_obj; T* m_obj;
public: public:
insert_obj_trail(obj_hashtable<T>& t, T* o) : m_table(t), m_obj(o) {} insert_obj_trail(obj_hashtable<T>& t, T* o) : m_table(t), m_obj(o) {}
~insert_obj_trail() override {}
void undo() override { m_table.remove(m_obj); } void undo() override { m_table.remove(m_obj); }
}; };
@ -404,8 +375,7 @@ class remove_obj_trail : public trail {
T* m_obj; T* m_obj;
public: public:
remove_obj_trail(obj_hashtable<T>& t, T* o) : m_table(t), m_obj(o) {} remove_obj_trail(obj_hashtable<T>& t, T* o) : m_table(t), m_obj(o) {}
virtual ~remove_obj_trail() {} void undo() override { m_table.insert(m_obj); }
virtual void undo() { m_table.insert(m_obj); }
}; };
@ -425,10 +395,6 @@ class trail_stack {
unsigned_vector m_scopes; unsigned_vector m_scopes;
region m_region; region m_region;
public: public:
trail_stack() {}
~trail_stack() {}
region & get_region() { return m_region; } region & get_region() { return m_region; }
void reset() { void reset() {
@ -457,4 +423,3 @@ public:
m_region.pop_scope(num_scopes); m_region.pop_scope(num_scopes);
} }
}; };