mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-25 10:05:32 +00:00
Code Activity

fix #2391

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-07-11 09:26:22 +01:00
parent adb91ae93c
commit 9474833c98
1 changed files with 16 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -181,6 +181,10 @@ struct purify_arith_proc {
return true;
}
struct div_def {
expr* x, *y, *d;
div_def(expr* x, expr* y, expr* d): x(x), y(y), d(d) {}
};
struct rw_cfg : public default_rewriter_cfg {
purify_arith_proc & m_owner;
@ -189,6 +193,7 @@ struct purify_arith_proc {
expr_ref_vector m_pinned;
expr_ref_vector m_new_cnstrs;
proof_ref_vector m_new_cnstr_prs;
svector<div_def> m_divs;
expr_ref m_subst;
proof_ref m_subst_pr;
expr_ref_vector m_new_vars;
@ -303,6 +308,7 @@ struct purify_arith_proc {
EQ(k, u().mk_div(x, mk_real_zero()))));
push_cnstr_pr(result_pr);
}
m_divs.push_back(div_def(x, y, k));
}
void process_idiv(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
@ -768,6 +774,16 @@ struct purify_arith_proc {
for (unsigned i = 0; i < sz; i++) {
m_goal.assert_expr(r.cfg().m_new_cnstrs.get(i), m_produce_proofs ? r.cfg().m_new_cnstr_prs.get(i) : nullptr, nullptr);
}
auto const& divs = r.cfg().m_divs;
for (unsigned i = 0; i < divs.size(); ++i) {
auto const& p1 = divs[i];
for (unsigned j = i + 1; j < divs.size(); ++j) {
auto const& p2 = divs[j];
m_goal.assert_expr(m().mk_implies(
m().mk_and(m().mk_eq(p1.x, p2.x), m().mk_eq(p1.y, p2.y)),
m().mk_eq(p1.d, p2.d)));
}
}
// add generic_model_converter to eliminate auxiliary variables from model
if (produce_models) {