From 9474833c989797de64fe47faba4a726b8cdc8ea6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 11 Jul 2019 09:26:22 +0100 Subject: [PATCH] fix #2391 Signed-off-by: Nikolaj Bjorner --- src/tactic/arith/purify_arith_tactic.cpp | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/src/tactic/arith/purify_arith_tactic.cpp b/src/tactic/arith/purify_arith_tactic.cpp index 18947787b..3d993392c 100644 --- a/src/tactic/arith/purify_arith_tactic.cpp +++ b/src/tactic/arith/purify_arith_tactic.cpp @@ -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 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) {