mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 20:18:18 +00:00
Code Activity

another revision of purify_arith, fix #4144

Browse source
This commit is contained in:
Nikolaj Bjorner 2020-04-29 12:06:17 -07:00
parent 3fc001baea
commit 0e77074e84
1 changed files with 44 additions and 24 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

68
src/tactic/arith/purify_arith_tactic.cpp
View file

@ -190,6 +190,7 @@ struct purify_arith_proc {
struct rw_cfg : public default_rewriter_cfg { struct rw_cfg : public default_rewriter_cfg {
purify_arith_proc & m_owner; purify_arith_proc & m_owner;
obj_hashtable<func_decl> m_cannot_purify;
obj_map<app, expr*> m_app2fresh; obj_map<app, expr*> m_app2fresh;
obj_map<app, proof*> m_app2pr; obj_map<app, proof*> m_app2pr;
expr_ref_vector m_pinned; expr_ref_vector m_pinned;
@ -211,6 +212,7 @@ struct purify_arith_proc {
m_subst(o.m()), m_subst(o.m()),
m_subst_pr(o.m()), m_subst_pr(o.m()),
m_new_vars(o.m()) { m_new_vars(o.m()) {
init_cannot_purify();
} }
ast_manager & m() { return m_owner.m(); } ast_manager & m() { return m_owner.m(); }
@ -222,6 +224,30 @@ struct purify_arith_proc {
bool elim_root_objs() const { return m_owner.m_elim_root_objs; } bool elim_root_objs() const { return m_owner.m_elim_root_objs; }
bool elim_inverses() const { return m_owner.m_elim_inverses; } bool elim_inverses() const { return m_owner.m_elim_inverses; }
void init_cannot_purify() {
struct proc {
rw_cfg& o;
proc(rw_cfg& o):o(o) {}
void operator()(app* a) {
for (expr* arg : *a) {
if (!is_ground(arg)) {
o.m_cannot_purify.insert(a->get_decl());
break;
}
}
}
void operator()(expr* ) {}
};
expr_fast_mark1 visited;
proc p(*this);
unsigned sz = m_owner.m_goal.size();
for (unsigned i = 0; i < sz; i++) {
expr* f = m_owner.m_goal.form(i);
for_each_expr_core<proc, expr_fast_mark1, true, true>(p, visited, f);
}
}
expr * mk_fresh_var(bool is_int) { expr * mk_fresh_var(bool is_int) {
expr * r = m().mk_fresh_const(nullptr, is_int ? u().mk_int() : u().mk_real()); expr * r = m().mk_fresh_const(nullptr, is_int ? u().mk_int() : u().mk_real());
m_new_vars.push_back(r); m_new_vars.push_back(r);
@ -661,6 +687,8 @@ struct purify_arith_proc {
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
if (f->get_family_id() != u().get_family_id()) if (f->get_family_id() != u().get_family_id())
return BR_FAILED; return BR_FAILED;
if (m_cannot_purify.contains(f))
return BR_FAILED;
switch (f->get_decl_kind()) { switch (f->get_decl_kind()) {
case OP_DIV: case OP_DIV:
process_div(f, num, args, result, result_pr); process_div(f, num, args, result, result_pr);
@ -693,7 +721,7 @@ struct purify_arith_proc {
bool get_subst(expr * s, expr * & t, proof * & t_pr) { bool get_subst(expr * s, expr * & t, proof * & t_pr) {
if (is_quantifier(s)) { if (is_quantifier(s)) {
m_owner.process_quantifier(to_quantifier(s), m_subst, m_subst_pr); m_owner.process_quantifier(*this, to_quantifier(s), m_subst, m_subst_pr);
t = m_subst.get(); t = m_subst.get();
t_pr = m_subst_pr.get(); t_pr = m_subst_pr.get();
return true; return true;
@ -718,34 +746,26 @@ struct purify_arith_proc {
} }
}; };
void process_quantifier(quantifier * q, expr_ref & result, proof_ref & result_pr) { struct rw_rec : public rewriter_tpl<rw_cfg> {
rw_cfg& m_cfg;
rw_rec(rw_cfg& cfg):
rewriter_tpl<rw_cfg>(cfg.m(), cfg.produce_proofs(), cfg),
m_cfg(cfg) {
}
};
void process_quantifier(rw_cfg& cfg, quantifier * q, expr_ref & result, proof_ref & result_pr) {
result_pr = nullptr; result_pr = nullptr;
rw r(*this); rw_rec r(cfg);
expr_ref new_body(m()); expr_ref new_body(m());
proof_ref new_body_pr(m()); proof_ref new_body_pr(m());
r(q->get_expr(), new_body, new_body_pr); r(q->get_expr(), new_body, new_body_pr);
unsigned num_vars = r.cfg().m_new_vars.size();
expr_ref_vector & cnstrs = r.cfg().m_new_cnstrs;
TRACE("purify_arith", TRACE("purify_arith",
tout << "num_vars: " << num_vars << "\n";
tout << "body: " << mk_ismt2_pp(q->get_expr(), m()) << "\nnew_body: " << new_body << "\n";); tout << "body: " << mk_ismt2_pp(q->get_expr(), m()) << "\nnew_body: " << new_body << "\n";);
if (num_vars == 0) { result = m().update_quantifier(q, new_body);
cnstrs.push_back(new_body); if (m_produce_proofs) {
new_body = m().mk_and(cnstrs); result_pr = m().mk_rewrite(q->get_expr(), new_body);
result = m().update_quantifier(q, new_body); result_pr = m().mk_quant_intro(q, to_quantifier(result.get()), result_pr);
if (m_produce_proofs) {
auto& cnstr_prs = r.cfg().m_new_cnstr_prs;
result_pr = m().mk_rewrite_star(q->get_expr(), new_body, cnstr_prs.size(), cnstr_prs.c_ptr());
result_pr = m().mk_quant_intro(q, to_quantifier(result.get()), result_pr);
r.cfg().push_cnstr_pr(result_pr);
}
}
else {
result = q;
if (m_produce_proofs) {
result_pr = m().mk_reflexivity(q);
}
} }
} }
@ -765,7 +785,7 @@ struct purify_arith_proc {
m_goal.update(i, new_curr, new_pr, m_goal.dep(i)); m_goal.update(i, new_curr, new_pr, m_goal.dep(i));
} }
// add cnstraints // add constraints
sz = r.cfg().m_new_cnstrs.size(); sz = r.cfg().m_new_cnstrs.size();
TRACE("purify_arith", tout << r.cfg().m_new_cnstrs << "\n";); TRACE("purify_arith", tout << r.cfg().m_new_cnstrs << "\n";);
TRACE("purify_arith", tout << r.cfg().m_new_cnstr_prs << "\n";); TRACE("purify_arith", tout << r.cfg().m_new_cnstr_prs << "\n";);