3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 03:07:07 +00:00
This commit is contained in:
Nikolaj Bjorner 2018-06-27 11:25:04 -07:00
commit 91ef84b8c9
6 changed files with 49 additions and 71 deletions

View file

@ -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) {

View file

@ -448,7 +448,7 @@ void rewriter_tpl<Config>::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);

View file

@ -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) {

View file

@ -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) {

View file

@ -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 {}
};

View file

@ -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;