mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-28 00:48:45 +00:00
Code Activity

remove some uneeded constructors

Browse source
This commit is contained in:
Nuno Lopes 2024-12-22 15:06:58 +00:00
parent fb5bbb8074
commit 97c70ba501
5 changed files with 8 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/smt/theory_array.cpp
View file

@ -27,14 +27,11 @@ namespace smt {
theory_array::theory_array(context& ctx): theory_array::theory_array(context& ctx):
theory_array_base(ctx), theory_array_base(ctx),
m_params(ctx.get_fparams()), m_params(ctx.get_fparams()),
m_find(*this), m_find(*this) {
m_trail_stack(),
m_final_check_idx(0) {
} }
theory_array::~theory_array() { theory_array::~theory_array() {
std::for_each(m_var_data.begin(), m_var_data.end(), delete_proc<var_data>()); std::for_each(m_var_data.begin(), m_var_data.end(), delete_proc<var_data>());
m_var_data.reset();
} }
void theory_array::init_search_eh() { void theory_array::init_search_eh() {

9
src/smt/theory_array.h
View file

@ -42,17 +42,16 @@ namespace smt {
ptr_vector<enode> m_stores; ptr_vector<enode> m_stores;
ptr_vector<enode> m_parent_selects; ptr_vector<enode> m_parent_selects;
ptr_vector<enode> m_parent_stores; ptr_vector<enode> m_parent_stores;
bool m_prop_upward; bool m_prop_upward = false;
bool m_is_array; bool m_is_array = false;
bool m_is_select; bool m_is_select = false;
var_data():m_prop_upward(false), m_is_array(false), m_is_select(false) {}
}; };
ptr_vector<var_data> m_var_data; ptr_vector<var_data> m_var_data;
theory_array_params& m_params; theory_array_params& m_params;
theory_array_stats m_stats; theory_array_stats m_stats;
th_union_find m_find; th_union_find m_find;
trail_stack m_trail_stack; trail_stack m_trail_stack;
unsigned m_final_check_idx; unsigned m_final_check_idx = 0;
theory_var mk_var(enode * n) override; theory_var mk_var(enode * n) override;
bool internalize_atom(app * atom, bool gate_ctx) override; bool internalize_atom(app * atom, bool gate_ctx) override;

5
src/smt/theory_array_bapa.cpp
View file

@ -98,10 +98,9 @@ namespace smt {
class theory_array_bapa::imp { class theory_array_bapa::imp {
struct sz_info { struct sz_info {
bool m_is_leaf; // has it been split into disjoint subsets already? bool m_is_leaf = true; // has it been split into disjoint subsets already?
rational m_size; // set to >= integer if fixed in final check, otherwise -1 rational m_size = rational::minus_one(); // set to >= integer if fixed in final check, otherwise -1
obj_map<enode, expr*> m_selects; obj_map<enode, expr*> m_selects;
sz_info(): m_is_leaf(true), m_size(rational::minus_one()) {}
}; };
typedef std::pair<func_decl*, func_decl*> func_decls; typedef std::pair<func_decl*, func_decl*> func_decls;

1
src/smt/theory_array_full.cpp
View file

@ -34,7 +34,6 @@ namespace smt {
theory_array_full::~theory_array_full() { theory_array_full::~theory_array_full() {
std::for_each(m_var_data_full.begin(), m_var_data_full.end(), delete_proc<var_data_full>()); std::for_each(m_var_data_full.begin(), m_var_data_full.end(), delete_proc<var_data_full>());
m_var_data_full.reset();
} }
theory* theory_array_full::mk_fresh(context* new_ctx) { theory* theory_array_full::mk_fresh(context* new_ctx) {

2
src/smt/theory_array_full.h
View file

@ -23,7 +23,7 @@ Revision History:
namespace smt { namespace smt {
class theory_array_full : public theory_array { class theory_array_full final : public theory_array {
struct var_data_full { struct var_data_full {
ptr_vector<enode> m_maps; ptr_vector<enode> m_maps;
ptr_vector<enode> m_consts; ptr_vector<enode> m_consts;