diff --git a/src/ast/rewriter/quant_hoist.cpp b/src/ast/rewriter/quant_hoist.cpp index 3bd3cb3bc..b5cf57927 100644 --- a/src/ast/rewriter/quant_hoist.cpp +++ b/src/ast/rewriter/quant_hoist.cpp @@ -66,7 +66,7 @@ public: TRACE("qe_verbose", tout << mk_pp(fml, m) << "\n"; tout << mk_pp(result, m) << "\n";); - fml = result; + fml = std::move(result); } void extract_quantifier(quantifier* q, app_ref_vector& vars, expr_ref& result, bool use_fresh) { diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h index 1a761e5d1..ebe52f52a 100644 --- a/src/ast/rewriter/rewriter_def.h +++ b/src/ast/rewriter/rewriter_def.h @@ -448,7 +448,7 @@ void rewriter_tpl::process_app(app * t, frame & fr) { m_r = result_stack().back(); if (!is_ground(m_r)) { m_inv_shifter(m_r, num_args, tmp); - m_r = tmp; + m_r = std::move(tmp); } result_stack().shrink(fr.m_spos); result_stack().push_back(m_r); diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp index 0f4be71c9..4fbf77ec9 100644 --- a/src/ast/rewriter/th_rewriter.cpp +++ b/src/ast/rewriter/th_rewriter.cpp @@ -776,7 +776,7 @@ void th_rewriter::reset() { void th_rewriter::operator()(expr_ref & term) { expr_ref result(term.get_manager()); m_imp->operator()(term, result); - term = result; + term = std::move(result); } void th_rewriter::operator()(expr * t, expr_ref & result) { diff --git a/src/qe/qe_lite.cpp b/src/qe/qe_lite.cpp index 494773f5d..3223706d4 100644 --- a/src/qe/qe_lite.cpp +++ b/src/qe/qe_lite.cpp @@ -2297,14 +2297,14 @@ public: vars.resize(j); } else { - fml = tmp; + fml = std::move(tmp); } } void operator()(expr_ref& fml, proof_ref& pr) { expr_ref tmp(m); m_elim_star(fml, tmp, pr); - fml = tmp; + fml = std::move(tmp); } void operator()(uint_set const& index_set, bool index_of_bound, expr_ref& fml) { diff --git a/src/tactic/ufbv/ufbv_rewriter_tactic.cpp b/src/tactic/ufbv/ufbv_rewriter_tactic.cpp index e9db976f9..9e41cee7c 100644 --- a/src/tactic/ufbv/ufbv_rewriter_tactic.cpp +++ b/src/tactic/ufbv/ufbv_rewriter_tactic.cpp @@ -21,74 +21,19 @@ Notes: #include "tactic/ufbv/ufbv_rewriter_tactic.h" class ufbv_rewriter_tactic : public tactic { - - struct imp { - ast_manager & m_manager; - - imp(ast_manager & m, params_ref const & p) : m_manager(m) { - updt_params(p); - } - - ast_manager & m() const { return m_manager; } - - void operator()(goal_ref const & g, - goal_ref_buffer & result) { - SASSERT(g->is_well_sorted()); - tactic_report report("ufbv-rewriter", *g); - fail_if_unsat_core_generation("ufbv-rewriter", g); - - bool produce_proofs = g->proofs_enabled(); - - ufbv_rewriter dem(m_manager); - - expr_ref_vector forms(m_manager), new_forms(m_manager); - proof_ref_vector proofs(m_manager), new_proofs(m_manager); - - unsigned size = g->size(); - for (unsigned i = 0; i < size; i++) { - forms.push_back(g->form(i)); - proofs.push_back(g->pr(i)); - } - - dem(forms.size(), forms.c_ptr(), proofs.c_ptr(), new_forms, new_proofs); - - g->reset(); - for (unsigned i = 0; i < new_forms.size(); i++) - g->assert_expr(new_forms.get(i), produce_proofs ? new_proofs.get(i) : nullptr, nullptr); - - // CMW: Remark: The demodulator could potentially - // remove all references to a variable. - - g->inc_depth(); - result.push_back(g.get()); - TRACE("ufbv-rewriter", g->display(tout);); - SASSERT(g->is_well_sorted()); - } - - void updt_params(params_ref const & p) { - } - }; - - imp * m_imp; - params_ref m_params; + ast_manager & m_manager; + params_ref m_params; public: ufbv_rewriter_tactic(ast_manager & m, params_ref const & p): - m_params(p) { - m_imp = alloc(imp, m, p); - } + m_manager(m), m_params(p) {} tactic * translate(ast_manager & m) override { return alloc(ufbv_rewriter_tactic, m, m_params); } - ~ufbv_rewriter_tactic() override { - dealloc(m_imp); - } - void updt_params(params_ref const & p) override { m_params = p; - m_imp->updt_params(p); } void collect_param_descrs(param_descrs & r) override { @@ -97,16 +42,40 @@ public: insert_produce_proofs(r); } - void operator()(goal_ref const & in, goal_ref_buffer & result) override { - (*m_imp)(in, result); + void operator()(goal_ref const & g, goal_ref_buffer & result) override { + SASSERT(g->is_well_sorted()); + tactic_report report("ufbv-rewriter", *g); + fail_if_unsat_core_generation("ufbv-rewriter", g); + + bool produce_proofs = g->proofs_enabled(); + + ufbv_rewriter dem(m_manager); + + expr_ref_vector forms(m_manager), new_forms(m_manager); + proof_ref_vector proofs(m_manager), new_proofs(m_manager); + + unsigned size = g->size(); + for (unsigned i = 0; i < size; i++) { + forms.push_back(g->form(i)); + proofs.push_back(g->pr(i)); + } + + dem(forms.size(), forms.c_ptr(), proofs.c_ptr(), new_forms, new_proofs); + + g->reset(); + for (unsigned i = 0; i < new_forms.size(); i++) + g->assert_expr(new_forms.get(i), produce_proofs ? new_proofs.get(i) : nullptr, nullptr); + + // CMW: Remark: The demodulator could potentially + // remove all references to a variable. + + g->inc_depth(); + result.push_back(g.get()); + TRACE("ufbv-rewriter", g->display(tout);); + SASSERT(g->is_well_sorted()); } - void cleanup() override { - ast_manager & m = m_imp->m(); - imp * d = alloc(imp, m, m_params); - std::swap(d, m_imp); - dealloc(d); - } + void cleanup() override {} }; diff --git a/src/util/obj_ref.h b/src/util/obj_ref.h index 409a77fc0..885601375 100644 --- a/src/util/obj_ref.h +++ b/src/util/obj_ref.h @@ -92,6 +92,15 @@ public: return *this; } + obj_ref & operator=(obj_ref && n) { + SASSERT(&m_manager == &n.m_manager); + if (this != &n) { + std::swap(m_obj, n.m_obj); + n.reset(); + } + return *this; + } + void reset() { dec_ref(); m_obj = nullptr;