From 8c2584bcf702859605f0a0a48de3cad0670bd9bd Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Tue, 19 Feb 2019 10:51:53 +0000 Subject: [PATCH 1/4] eliminate a few ref incs/decs plus remove unused variable --- src/tactic/bv/elim_small_bv_tactic.cpp | 9 ++------- 1 file changed, 2 insertions(+), 7 deletions(-) diff --git a/src/tactic/bv/elim_small_bv_tactic.cpp b/src/tactic/bv/elim_small_bv_tactic.cpp index a9f94ca3f..9608ab0f7 100644 --- a/src/tactic/bv/elim_small_bv_tactic.cpp +++ b/src/tactic/bv/elim_small_bv_tactic.cpp @@ -37,7 +37,6 @@ class elim_small_bv_tactic : public tactic { bv_util m_util; th_rewriter m_simp; ref m_mc; - goal * m_goal; unsigned m_max_bits; unsigned long long m_max_steps; unsigned long long m_max_memory; // in bytes @@ -53,7 +52,6 @@ class elim_small_bv_tactic : public tactic { m_bindings(_m), m_num_eliminated(0) { updt_params(p); - m_goal = nullptr; m_max_steps = UINT_MAX; } @@ -76,7 +74,7 @@ class elim_small_bv_tactic : public tactic { TRACE("elim_small_bv", tout << "replace idx " << idx << " with " << mk_ismt2_pp(replacement, m) << " in " << mk_ismt2_pp(e, m) << std::endl;); expr_ref res(m); - expr_ref_vector substitution(m); + ptr_vector substitution; substitution.resize(num_decls, nullptr); substitution[num_decls - idx - 1] = replacement; @@ -152,9 +150,7 @@ class elim_small_bv_tactic : public tactic { expr_ref_vector new_bodies(m); for (unsigned j = 0; j < bv_sz && !max_steps_exceeded(num_steps); j ++) { expr_ref n(m_util.mk_numeral(j, bv_sz), m); - expr_ref nb(m); - nb = replace_var(uv, num_decls, max_var_idx_p1, i, s, body, n); - new_bodies.push_back(nb); + new_bodies.push_back(replace_var(uv, num_decls, max_var_idx_p1, i, s, body, n)); num_steps++; } @@ -250,7 +246,6 @@ public: fail_if_unsat_core_generation("elim-small-bv", g); m_rw.cfg().m_produce_models = g->models_enabled(); - m_rw.m_cfg.m_goal = g.get(); expr_ref new_curr(m); proof_ref new_pr(m); unsigned size = g->size(); From 8e4ef19f45380aec024a8835e13150928b5f6ebc Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Tue, 19 Feb 2019 10:54:41 +0000 Subject: [PATCH 2/4] fix debug build --- src/tactic/bv/elim_small_bv_tactic.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/tactic/bv/elim_small_bv_tactic.cpp b/src/tactic/bv/elim_small_bv_tactic.cpp index 9608ab0f7..256586896 100644 --- a/src/tactic/bv/elim_small_bv_tactic.cpp +++ b/src/tactic/bv/elim_small_bv_tactic.cpp @@ -92,7 +92,7 @@ class elim_small_bv_tactic : public tactic { TRACE("elim_small_bv", tout << "substitution: " << std::endl; for (unsigned k = 0; k < substitution.size(); k++) { - expr * se = substitution[k].get(); + expr * se = substitution[k]; tout << k << " = "; if (se == 0) tout << "0"; else tout << mk_ismt2_pp(se, m); From edf0df634d5564cff49b463851081f5a135261f2 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Tue, 19 Feb 2019 13:18:20 +0000 Subject: [PATCH 3/4] simplifications to refs --- src/ackermannization/lackr.cpp | 2 +- src/ackermannization/lackr_model_constructor.cpp | 10 +++------- src/util/obj_ref.h | 6 ++---- src/util/ref_buffer.h | 6 ++++++ src/util/ref_vector.h | 4 ++-- 5 files changed, 14 insertions(+), 14 deletions(-) diff --git a/src/ackermannization/lackr.cpp b/src/ackermannization/lackr.cpp index a965fc261..4fe7797d4 100644 --- a/src/ackermannization/lackr.cpp +++ b/src/ackermannization/lackr.cpp @@ -122,7 +122,7 @@ bool lackr::ackr(app * const t1, app * const t2) { TRACE("ackermannize", tout << "ackr constr abs:" << mk_ismt2_pp(cga, m_m, 2) << "\n";); if (m_m.is_true(cga)) return false; m_st.m_ackrs_sz++; - m_ackrs.push_back(cga); + m_ackrs.push_back(std::move(cga)); return true; } diff --git a/src/ackermannization/lackr_model_constructor.cpp b/src/ackermannization/lackr_model_constructor.cpp index df0aac15e..f24a53cdb 100644 --- a/src/ackermannization/lackr_model_constructor.cpp +++ b/src/ackermannization/lackr_model_constructor.cpp @@ -237,7 +237,7 @@ struct lackr_model_constructor::imp { // handle functions if (m_ackr_helper.should_ackermannize(a)) { // handle uninterpreted app_ref key(m_m.mk_app(a->get_decl(), values.c_ptr()), m_m); - if (!make_value_uninterpreted_function(a, values, key.get(), result)) { + if (!make_value_uninterpreted_function(a, key.get(), result)) { return false; } } @@ -284,7 +284,6 @@ struct lackr_model_constructor::imp { } bool make_value_uninterpreted_function(app* a, - expr_ref_vector& values, app* key, expr_ref& result) { // get ackermann constant @@ -370,15 +369,12 @@ lackr_model_constructor::lackr_model_constructor(ast_manager& m, ackr_info_ref i {} lackr_model_constructor::~lackr_model_constructor() { - if (m_imp) dealloc(m_imp); + dealloc(m_imp); } bool lackr_model_constructor::check(model_ref& abstr_model) { m_conflicts.reset(); - if (m_imp) { - dealloc(m_imp); - m_imp = nullptr; - } + dealloc(m_imp); m_imp = alloc(lackr_model_constructor::imp, m_m, m_info, abstr_model, m_conflicts); const bool rv = m_imp->check(); m_state = rv ? CHECKED : CONFLICT; diff --git a/src/util/obj_ref.h b/src/util/obj_ref.h index 8908f2cdd..e3b0d0710 100644 --- a/src/util/obj_ref.h +++ b/src/util/obj_ref.h @@ -94,10 +94,8 @@ public: obj_ref & operator=(obj_ref && n) { SASSERT(&m_manager == &n.m_manager); - if (this != &n) { - std::swap(m_obj, n.m_obj); - n.reset(); - } + std::swap(m_obj, n.m_obj); + n.reset(); return *this; } diff --git a/src/util/ref_buffer.h b/src/util/ref_buffer.h index 4768c3f28..49213cc62 100644 --- a/src/util/ref_buffer.h +++ b/src/util/ref_buffer.h @@ -58,6 +58,12 @@ public: inc_ref(n); m_buffer.push_back(n); } + + template + void push_back(obj_ref && n) { + m_buffer.push_back(n.get()); + n.steal(); + } void pop_back() { SASSERT(!m_buffer.empty()); diff --git a/src/util/ref_vector.h b/src/util/ref_vector.h index d0e9a8f55..732ec20dd 100644 --- a/src/util/ref_vector.h +++ b/src/util/ref_vector.h @@ -99,8 +99,8 @@ public: return *this; } - template - ref_vector_core& push_back(obj_ref && n) { + template + ref_vector_core& push_back(obj_ref && n) { m_nodes.push_back(n.get()); n.steal(); return *this; From 61272fdc0cfa742adc25f8059c40d3d82f7b7888 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Tue, 19 Feb 2019 13:36:39 +0000 Subject: [PATCH 4/4] remove a few more inc/dec refs --- src/ast/rewriter/der.cpp | 6 ++---- src/ast/rewriter/distribute_forall.cpp | 3 +-- src/ast/rewriter/var_subst.cpp | 7 ++----- src/tactic/core/distribute_forall_tactic.cpp | 6 ++---- 4 files changed, 7 insertions(+), 15 deletions(-) diff --git a/src/ast/rewriter/der.cpp b/src/ast/rewriter/der.cpp index 027846c31..c95c07f63 100644 --- a/src/ast/rewriter/der.cpp +++ b/src/ast/rewriter/der.cpp @@ -374,13 +374,11 @@ void der::apply_substitution(quantifier * q, expr_ref & r) { expr_ref_buffer new_patterns(m_manager); expr_ref_buffer new_no_patterns(m_manager); for (unsigned j = 0; j < q->get_num_patterns(); j++) { - expr_ref new_pat = m_subst(q->get_pattern(j), m_subst_map.size(), m_subst_map.c_ptr()); - new_patterns.push_back(new_pat); + new_patterns.push_back(m_subst(q->get_pattern(j), m_subst_map.size(), m_subst_map.c_ptr())); } for (unsigned j = 0; j < q->get_num_no_patterns(); j++) { - expr_ref new_nopat = m_subst(q->get_no_pattern(j), m_subst_map.size(), m_subst_map.c_ptr()); - new_no_patterns.push_back(new_nopat); + new_no_patterns.push_back(m_subst(q->get_no_pattern(j), m_subst_map.size(), m_subst_map.c_ptr())); } r = m_manager.update_quantifier(q, new_patterns.size(), new_patterns.c_ptr(), diff --git a/src/ast/rewriter/distribute_forall.cpp b/src/ast/rewriter/distribute_forall.cpp index 54d7e2eca..c621579cb 100644 --- a/src/ast/rewriter/distribute_forall.cpp +++ b/src/ast/rewriter/distribute_forall.cpp @@ -126,8 +126,7 @@ void distribute_forall::reduce1_quantifier(quantifier * q) { br.mk_not(arg, not_arg); quantifier_ref tmp_q(m_manager); tmp_q = m_manager.update_quantifier(q, not_arg); - expr_ref new_q = elim_unused_vars(m_manager, tmp_q, params_ref()); - new_args.push_back(new_q); + new_args.push_back(elim_unused_vars(m_manager, tmp_q, params_ref())); } expr_ref result(m_manager); // m_bsimp.mk_and actually constructs a (not (or ...)) formula, diff --git a/src/ast/rewriter/var_subst.cpp b/src/ast/rewriter/var_subst.cpp index cbd79e08c..ff479b565 100644 --- a/src/ast/rewriter/var_subst.cpp +++ b/src/ast/rewriter/var_subst.cpp @@ -135,17 +135,14 @@ expr_ref unused_vars_eliminator::operator()(quantifier* q) { return result; } - expr_ref tmp(m); expr_ref_buffer new_patterns(m); expr_ref_buffer new_no_patterns(m); for (unsigned i = 0; i < num_patterns; i++) { - tmp = m_subst(q->get_pattern(i), var_mapping.size(), var_mapping.c_ptr()); - new_patterns.push_back(tmp); + new_patterns.push_back(m_subst(q->get_pattern(i), var_mapping.size(), var_mapping.c_ptr())); } for (unsigned i = 0; i < num_no_patterns; i++) { - tmp = m_subst(q->get_no_pattern(i), var_mapping.size(), var_mapping.c_ptr()); - new_no_patterns.push_back(tmp); + new_no_patterns.push_back(m_subst(q->get_no_pattern(i), var_mapping.size(), var_mapping.c_ptr())); } result = m.mk_quantifier(q->get_kind(), diff --git a/src/tactic/core/distribute_forall_tactic.cpp b/src/tactic/core/distribute_forall_tactic.cpp index c2688f741..800644d9e 100644 --- a/src/tactic/core/distribute_forall_tactic.cpp +++ b/src/tactic/core/distribute_forall_tactic.cpp @@ -49,8 +49,7 @@ class distribute_forall_tactic : public tactic { expr * not_arg = m.mk_not(arg); quantifier_ref tmp_q(m); tmp_q = m.update_quantifier(old_q, not_arg); - expr_ref new_q = elim_unused_vars(m, tmp_q, params_ref()); - new_args.push_back(new_q); + new_args.push_back(elim_unused_vars(m, tmp_q, params_ref())); } result = m.mk_and(new_args.size(), new_args.c_ptr()); return true; @@ -68,8 +67,7 @@ class distribute_forall_tactic : public tactic { expr * arg = to_app(new_body)->get_arg(i); quantifier_ref tmp_q(m); tmp_q = m.update_quantifier(old_q, arg); - expr_ref new_q = elim_unused_vars(m, tmp_q, params_ref()); - new_args.push_back(new_q); + new_args.push_back(elim_unused_vars(m, tmp_q, params_ref())); } result = m.mk_and(new_args.size(), new_args.c_ptr()); return true;