diff --git a/src/ackermannization/ackermannize_bv_tactic.cpp b/src/ackermannization/ackermannize_bv_tactic.cpp index 3ffee518e..98417cc7b 100644 --- a/src/ackermannization/ackermannize_bv_tactic.cpp +++ b/src/ackermannization/ackermannize_bv_tactic.cpp @@ -35,7 +35,7 @@ public: fail_if_proof_generation("ackermannize", g); TRACE("ackermannize", g->display(tout << "in\n");); - expr_ref_vector flas(m); + ptr_vector flas; const unsigned sz = g->size(); for (unsigned i = 0; i < sz; i++) flas.push_back(g->form(i)); lackr lackr(m, m_p, m_st, flas, nullptr); diff --git a/src/ackermannization/ackr_model_converter.cpp b/src/ackermannization/ackr_model_converter.cpp index 9e87a1a69..c5e04ab23 100644 --- a/src/ackermannization/ackr_model_converter.cpp +++ b/src/ackermannization/ackr_model_converter.cpp @@ -134,7 +134,7 @@ void ackr_model_converter::add_entry(model_evaluator & evaluator, info->abstract(arg, aarg); expr_ref arg_value(m); evaluator(aarg, arg_value); - args.push_back(arg_value); + args.push_back(std::move(arg_value)); } if (fi->get_entry(args.c_ptr()) == nullptr) { TRACE("ackr_model", diff --git a/src/ackermannization/lackr.cpp b/src/ackermannization/lackr.cpp index b739af9d3..8c18df7b2 100644 --- a/src/ackermannization/lackr.cpp +++ b/src/ackermannization/lackr.cpp @@ -23,8 +23,8 @@ #include "ast/for_each_expr.h" #include "model/model_smt2_pp.h" -lackr::lackr(ast_manager& m, params_ref p, lackr_stats& st, expr_ref_vector& formulas, - solver * uffree_solver) +lackr::lackr(ast_manager& m, const params_ref& p, lackr_stats& st, + const ptr_vector& formulas, solver * uffree_solver) : m_m(m) , m_p(p) , m_formulas(formulas) @@ -173,11 +173,10 @@ void lackr::abstract() { } m_info->seal(); // perform abstraction of the formulas - const unsigned sz = m_formulas.size(); - for (unsigned i = 0; i < sz; ++i) { + for (expr * f : m_formulas) { expr_ref a(m_m); - m_info->abstract(m_formulas.get(i), a); - m_abstr.push_back(a); + m_info->abstract(f, a); + m_abstr.push_back(std::move(a)); } } @@ -249,13 +248,9 @@ lbool lackr::lazy() { // Collect all uninterpreted terms, skipping 0-arity. // bool lackr::collect_terms() { - ptr_vector stack; + ptr_vector stack = m_formulas; expr * curr; expr_mark visited; - for(unsigned i = 0; i < m_formulas.size(); ++i) { - stack.push_back(m_formulas.get(i)); - TRACE("lackr", tout << "infla: " <& formulas, solver * uffree_solver); ~lackr(); void updt_params(params_ref const & _p); @@ -82,7 +82,7 @@ class lackr { typedef ackr_helper::app_set app_set; ast_manager& m_m; params_ref m_p; - expr_ref_vector m_formulas; + const ptr_vector& m_formulas; expr_ref_vector m_abstr; fun2terms_map m_fun2terms; ackr_info_ref m_info; diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index 5993e9fdd..295977a06 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -218,10 +218,9 @@ namespace api { // Corner case bug: n may be in m_last_result, and this is the only reference to n. // When, we execute reset() it is deleted // To avoid this bug, I bump the reference counter before reseting m_last_result - m().inc_ref(n); + ast_ref node(n, m()); m_last_result.reset(); - m_last_result.push_back(n); - m().dec_ref(n); + m_last_result.push_back(std::move(node)); } else { m_ast_trail.push_back(n); diff --git a/src/ast/ast_smt2_pp.cpp b/src/ast/ast_smt2_pp.cpp index 5cd09263d..3a55bbb0b 100644 --- a/src/ast/ast_smt2_pp.cpp +++ b/src/ast/ast_smt2_pp.cpp @@ -1199,7 +1199,7 @@ void mk_smt2_format(unsigned sz, expr * const* es, smt2_pp_environment & env, pa for (unsigned i = 0; i < sz; ++i) { format_ref fr(fm(m)); pr(es[i], num_vars, var_prefix, fr, var_names); - fmts.push_back(fr); + fmts.push_back(std::move(fr)); } r = mk_seq(m, fmts.c_ptr(), fmts.c_ptr() + fmts.size(), f2f()); } diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index b079fc2ca..dd3f35a2a 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -3108,12 +3108,12 @@ void fpa2bv_converter::mk_to_ieee_bv_unspecified(func_decl * f, unsigned num, ex expr_ref exp_bv(m), exp_all_ones(m); exp_bv = m_bv_util.mk_extract(ebits+sbits-2, sbits-1, result); exp_all_ones = m.mk_eq(exp_bv, m_bv_util.mk_bv_neg(m_bv_util.mk_numeral(1, ebits))); - m_extra_assertions.push_back(exp_all_ones); + m_extra_assertions.push_back(std::move(exp_all_ones)); expr_ref sig_bv(m), sig_is_non_zero(m); sig_bv = m_bv_util.mk_extract(sbits-2, 0, result); sig_is_non_zero = m.mk_not(m.mk_eq(sig_bv, m_bv_util.mk_numeral(0, sbits-1))); - m_extra_assertions.push_back(sig_is_non_zero); + m_extra_assertions.push_back(std::move(sig_is_non_zero)); } TRACE("fpa2bv_to_ieee_bv_unspecified", tout << "result=" << mk_ismt2_pp(result, m) << std::endl;); diff --git a/src/ast/rewriter/bv_trailing.cpp b/src/ast/rewriter/bv_trailing.cpp index ad9350eca..433ef6f66 100644 --- a/src/ast/rewriter/bv_trailing.cpp +++ b/src/ast/rewriter/bv_trailing.cpp @@ -125,7 +125,7 @@ struct bv_trailing::imp { for (unsigned i = 0; i < num; ++i) { expr * const curr = a->get_arg(i); VERIFY(to_rm == remove_trailing(curr, to_rm, tmp, depth - 1)); - new_args.push_back(tmp); + new_args.push_back(std::move(tmp)); } result = m.mk_app(m_util.get_fid(), OP_BADD, new_args.size(), new_args.c_ptr()); return to_rm; @@ -150,7 +150,7 @@ struct bv_trailing::imp { numeral c_val; unsigned c_sz; if (!m_util.is_numeral(tmp, c_val, c_sz) || !c_val.is_one()) - new_args.push_back(tmp); + new_args.push_back(std::move(tmp)); const unsigned sz = m_util.get_bv_size(coefficient); const unsigned new_sz = sz - retv; @@ -204,7 +204,7 @@ struct bv_trailing::imp { expr_ref_vector new_args(m); for (unsigned j = 0; j < i; ++j) new_args.push_back(a->get_arg(j)); - if (new_last) new_args.push_back(new_last); + if (new_last) new_args.push_back(std::move(new_last)); result = new_args.size() == 1 ? new_args.get(0) : m_util.mk_concat(new_args.size(), new_args.c_ptr()); return retv; diff --git a/src/ast/substitution/substitution.cpp b/src/ast/substitution/substitution.cpp index 39e9e07a2..7e981aab8 100644 --- a/src/ast/substitution/substitution.cpp +++ b/src/ast/substitution/substitution.cpp @@ -196,16 +196,16 @@ void substitution::apply(unsigned num_actual_offsets, unsigned const * deltas, e expr_ref_vector pats(m_manager), no_pats(m_manager); for (unsigned i = 0; i < q->get_num_patterns(); ++i) { subst.apply(num_actual_offsets, deltas, expr_offset(q->get_pattern(i), off), s1, t1, er); - pats.push_back(er); + pats.push_back(std::move(er)); } for (unsigned i = 0; i < q->get_num_no_patterns(); ++i) { subst.apply(num_actual_offsets, deltas, expr_offset(q->get_no_pattern(i), off), s1, t1, er); - no_pats.push_back(er); + no_pats.push_back(std::move(er)); } subst.apply(num_actual_offsets, deltas, body, s1, t1, er); er = m_manager.update_quantifier(q, pats.size(), pats.c_ptr(), no_pats.size(), no_pats.c_ptr(), er); m_todo.pop_back(); - m_new_exprs.push_back(er); + m_new_exprs.push_back(std::move(er)); m_apply_cache.insert(n, er); break; } diff --git a/src/qe/qe_lite.cpp b/src/qe/qe_lite.cpp index 3223706d4..da45d17ca 100644 --- a/src/qe/qe_lite.cpp +++ b/src/qe/qe_lite.cpp @@ -320,8 +320,8 @@ namespace eq { << "sz is " << sz << "\n" << "subst_map[inx]: " << mk_pp(m_subst_map.get(inx), m) << "\n";); SASSERT(m_subst_map.get(inx) == nullptr); - m_subst_map[inx] = r; m_subst.update_inv_binding_at(inx, r); + m_subst_map[inx] = std::move(r); } } @@ -470,7 +470,7 @@ namespace eq { m_var2pos[idx] = i; def_count++; largest_vinx = std::max(idx, largest_vinx); - m_new_exprs.push_back(t); + m_new_exprs.push_back(std::move(t)); } else if (!m.is_value(m_map[idx])) { // check if the new definition is simpler @@ -482,7 +482,7 @@ namespace eq { m_pos2var[i] = idx; m_var2pos[idx] = i; m_map[idx] = t; - m_new_exprs.push_back(t); + m_new_exprs.push_back(std::move(t)); } // -- prefer ground else if (is_app(t) && to_app(t)->is_ground() && @@ -492,7 +492,7 @@ namespace eq { m_pos2var[i] = idx; m_var2pos[idx] = i; m_map[idx] = t; - m_new_exprs.push_back(t); + m_new_exprs.push_back(std::move(t)); } // -- prefer constants else if (is_uninterp_const(t) @@ -501,7 +501,7 @@ namespace eq { m_pos2var[i] = idx; m_var2pos[idx] = i; m_map[idx] = t; - m_new_exprs.push_back(t); + m_new_exprs.push_back(std::move(t)); } TRACE ("qe_def", tout << "Replacing definition of VAR " << idx << " from " diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index fd9b27069..73a3c27bd 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -1594,7 +1594,7 @@ namespace smt { for (literal lit : m_assigned_literals) { expr_ref e(m_manager); literal2expr(lit, e); - assignments.push_back(e); + assignments.push_back(std::move(e)); } } @@ -4180,7 +4180,7 @@ namespace smt { SASSERT(get_justification(guess.var()).get_kind() == b_justification::AXIOM); expr_ref lit(m_manager); literal2expr(guess, lit); - result.push_back(lit); + result.push_back(std::move(lit)); } } diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 48b689bd7..4f7c8073e 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -1115,8 +1115,6 @@ namespace smt { void internalize_assertions(); - void assert_assumption(expr * a); - bool validate_assumptions(expr_ref_vector const& asms); void init_assumptions(expr_ref_vector const& asms); @@ -1129,8 +1127,6 @@ namespace smt { void reset_assumptions(); - void reset_clause(); - void add_theory_assumptions(expr_ref_vector & theory_assumptions); lbool mk_unsat_core(lbool result); @@ -1585,8 +1581,6 @@ namespace smt { //proof * const * get_asserted_formula_proofs() const { return m_asserted_formulas.get_formula_proofs(); } - void get_assumptions_core(ptr_vector & result); - void get_assertions(ptr_vector & result) { m_asserted_formulas.get_assertions(result); } void display(std::ostream & out) const; diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp index 19247c1d9..29c624bb2 100644 --- a/src/smt/smt_context_pp.cpp +++ b/src/smt/smt_context_pp.cpp @@ -409,11 +409,11 @@ namespace smt { for (unsigned i = 0; i < num_antecedents; i++) { literal l = antecedents[i]; literal2expr(l, n); - fmls.push_back(n); + fmls.push_back(std::move(n)); } if (consequent != false_literal) { literal2expr(~consequent, n); - fmls.push_back(n); + fmls.push_back(std::move(n)); } if (logic != symbol::null) out << "(set-logic " << logic << ")\n"; visitor.collect(fmls); diff --git a/src/smt/smt_justification.cpp b/src/smt/smt_justification.cpp index 4ac176a2b..fc9307792 100644 --- a/src/smt/smt_justification.cpp +++ b/src/smt/smt_justification.cpp @@ -281,7 +281,7 @@ namespace smt { for (unsigned i = 0; i < m_num_literals; i++) { expr_ref l(m); ctx.literal2expr(m_literals[i], l); - lits.push_back(l); + lits.push_back(std::move(l)); } if (lits.size() == 1) return m.mk_th_lemma(m_th_id, lits.get(0), 0, nullptr, m_params.size(), m_params.c_ptr()); @@ -407,12 +407,7 @@ namespace smt { for (unsigned i = 0; i < m_num_literals; i++) { bool sign = GET_TAG(m_literals[i]) != 0; expr * v = UNTAG(expr*, m_literals[i]); - expr_ref l(m); - if (sign) - l = m.mk_not(v); - else - l = v; - lits.push_back(l); + lits.push_back(sign ? m.mk_not(v) : v); } if (lits.size() == 1) return m.mk_th_lemma(m_th_id, lits.get(0), 0, nullptr, m_params.size(), m_params.c_ptr()); diff --git a/src/tactic/smtlogics/qfufbv_tactic.cpp b/src/tactic/smtlogics/qfufbv_tactic.cpp index 3bd28ad6d..a4e169856 100644 --- a/src/tactic/smtlogics/qfufbv_tactic.cpp +++ b/src/tactic/smtlogics/qfufbv_tactic.cpp @@ -62,7 +62,7 @@ public: TRACE("qfufbv_ackr_tactic", g->display(tout << "goal:\n");); // running implementation - expr_ref_vector flas(m); + ptr_vector flas; const unsigned sz = g->size(); for (unsigned i = 0; i < sz; i++) flas.push_back(g->form(i)); scoped_ptr uffree_solver = setup_sat(); diff --git a/src/util/ref_vector.h b/src/util/ref_vector.h index f340d8886..1e6525a06 100644 --- a/src/util/ref_vector.h +++ b/src/util/ref_vector.h @@ -99,6 +99,13 @@ public: return *this; } + template + ref_vector_core& push_back(obj_ref && n) { + m_nodes.push_back(n.get()); + n.steal(); + return *this; + } + void pop_back() { SASSERT(!m_nodes.empty()); T * n = m_nodes.back(); @@ -253,6 +260,13 @@ public: return *this; } + template + element_ref & operator=(obj_ref && n) { + m_manager.dec_ref(m_ref); + m_ref = n.steal(); + return *this; + } + T * get() const { return m_ref; } @@ -288,9 +302,8 @@ public: return *this; } -private: // prevent abuse: - ref_vector & operator=(ref_vector const & other); + ref_vector & operator=(ref_vector const & other) = delete; }; template