mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-09 12:50:32 +00:00
Code Activity

ufbv_rewriter_tactic: remove unneeded imp class

Browse source
This commit is contained in:
Nuno Lopes 2018-06-26 18:05:14 +01:00
parent 2b31024dab
commit 6c64e138b0
1 changed files with 35 additions and 66 deletions
Download patch file Download diff file Expand all files Collapse all files

101
src/tactic/ufbv/ufbv_rewriter_tactic.cpp
View file

@ -21,74 +21,19 @@ Notes:
#include "tactic/ufbv/ufbv_rewriter_tactic.h" #include "tactic/ufbv/ufbv_rewriter_tactic.h"
class ufbv_rewriter_tactic : public tactic { class ufbv_rewriter_tactic : public tactic {
ast_manager & m_manager;
struct imp { params_ref m_params;
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;
public: public:
ufbv_rewriter_tactic(ast_manager & m, params_ref const & p): ufbv_rewriter_tactic(ast_manager & m, params_ref const & p):
m_params(p) { m_manager(m), m_params(p) {}
m_imp = alloc(imp, m, p);
}
tactic * translate(ast_manager & m) override { tactic * translate(ast_manager & m) override {
return alloc(ufbv_rewriter_tactic, m, m_params); return alloc(ufbv_rewriter_tactic, m, m_params);
} }
~ufbv_rewriter_tactic() override {
dealloc(m_imp);
}
void updt_params(params_ref const & p) override { void updt_params(params_ref const & p) override {
m_params = p; m_params = p;
m_imp->updt_params(p);
} }
void collect_param_descrs(param_descrs & r) override { void collect_param_descrs(param_descrs & r) override {
@ -97,16 +42,40 @@ public:
insert_produce_proofs(r); insert_produce_proofs(r);
} }
void operator()(goal_ref const & in, goal_ref_buffer & result) override { void operator()(goal_ref const & g, goal_ref_buffer & result) override {
(*m_imp)(in, 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 cleanup() override { void cleanup() override {}
ast_manager & m = m_imp->m();
imp * d = alloc(imp, m, m_params);
std::swap(d, m_imp);
dealloc(d);
}
}; };