From a7dc50362b14baf780d17a0c962958c46d9f3350 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 31 Dec 2019 11:53:05 -0800 Subject: [PATCH] fix #2836 --- src/ast/arith_decl_plugin.cpp | 10 ++++++++ src/ast/arith_decl_plugin.h | 2 ++ src/sat/sat_solver/inc_sat_solver.cpp | 4 +-- src/tactic/arith/purify_arith_tactic.cpp | 32 +++++++++++++++++++----- 4 files changed, 40 insertions(+), 8 deletions(-) diff --git a/src/ast/arith_decl_plugin.cpp b/src/ast/arith_decl_plugin.cpp index ec3881a71..e7f96614f 100644 --- a/src/ast/arith_decl_plugin.cpp +++ b/src/ast/arith_decl_plugin.cpp @@ -838,3 +838,13 @@ func_decl* arith_util::mk_idiv0() { sort* rs[2] = { mk_int(), mk_int() }; return m_manager.mk_func_decl(m_afid, OP_IDIV0, 0, nullptr, 2, rs, mk_int()); } + +func_decl* arith_util::mk_rem0() { + sort* rs[2] = { mk_int(), mk_int() }; + return m_manager.mk_func_decl(m_afid, OP_REM0, 0, nullptr, 2, rs, mk_int()); +} + +func_decl* arith_util::mk_mod0() { + sort* rs[2] = { mk_int(), mk_int() }; + return m_manager.mk_func_decl(m_afid, OP_MOD0, 0, nullptr, 2, rs, mk_int()); +} diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h index 2c3dc9d09..5d6f102f1 100644 --- a/src/ast/arith_decl_plugin.h +++ b/src/ast/arith_decl_plugin.h @@ -367,8 +367,10 @@ public: sort * mk_int() { return m_manager.mk_sort(m_afid, INT_SORT); } sort * mk_real() { return m_manager.mk_sort(m_afid, REAL_SORT); } + func_decl* mk_rem0(); func_decl* mk_div0(); func_decl* mk_idiv0(); + func_decl* mk_mod0(); func_decl* mk_ipower0(); func_decl* mk_rpower0(); diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 6dcfd0c75..d1f4d9595 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -556,8 +556,8 @@ public: mk_card2bv_tactic(m, m_params), // updates model converter using_params(mk_simplify_tactic(m), simp2_p), mk_max_bv_sharing_tactic(m), - mk_bit_blaster_tactic(m, m_bb_rewriter.get()), // updates model converter - using_params(mk_simplify_tactic(m), simp2_p)); + mk_bit_blaster_tactic(m, m_bb_rewriter.get()) + ); while (m_bb_rewriter->get_num_scopes() < m_num_scopes) { m_bb_rewriter->push(); } diff --git a/src/tactic/arith/purify_arith_tactic.cpp b/src/tactic/arith/purify_arith_tactic.cpp index 0ce270f4e..0cfa53d88 100644 --- a/src/tactic/arith/purify_arith_tactic.cpp +++ b/src/tactic/arith/purify_arith_tactic.cpp @@ -181,9 +181,9 @@ struct purify_arith_proc { return true; } - struct div_def { + struct bin_def { expr* x, *y, *d; - div_def(expr* x, expr* y, expr* d): x(x), y(y), d(d) {} + bin_def(expr* x, expr* y, expr* d): x(x), y(y), d(d) {} }; struct rw_cfg : public default_rewriter_cfg { @@ -193,7 +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, m_idivs; + svector m_divs, m_idivs, m_mods; expr_ref m_ipower0, m_rpower0; expr_ref m_subst; proof_ref m_subst_pr; @@ -311,7 +311,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)); + m_divs.push_back(bin_def(x, y, k)); } void process_idiv(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { @@ -334,6 +334,7 @@ struct purify_arith_proc { expr * x = args[0]; expr * y = args[1]; + m_mods.push_back(bin_def(x, y, k2)); // (div x y) --> k1 | y = 0 \/ x = k1 * y + k2, // y = 0 \/ 0 <= k2, // y = 0 \/ k2 < |y|, @@ -364,7 +365,7 @@ struct purify_arith_proc { push_cnstr(OR(NOT(EQ(y, zero)), EQ(k2, u().mk_mod(x, zero)))); push_cnstr_pr(mod_pr); } - m_idivs.push_back(div_def(x, y, k1)); + m_idivs.push_back(bin_def(x, y, k1)); } void process_mod(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { @@ -785,8 +786,9 @@ 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; + auto const& divs = r.cfg().m_divs; auto const& idivs = r.cfg().m_idivs; + auto const& mods = r.cfg().m_mods; for (unsigned i = 0; i < divs.size(); ++i) { auto const& p1 = divs[i]; for (unsigned j = i + 1; j < divs.size(); ++j) { @@ -796,6 +798,15 @@ struct purify_arith_proc { m().mk_eq(p1.d, p2.d))); } } + for (unsigned i = 0; i < mods.size(); ++i) { + auto const& p1 = mods[i]; + for (unsigned j = i + 1; j < mods.size(); ++j) { + auto const& p2 = mods[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))); + } + } for (unsigned i = 0; i < idivs.size(); ++i) { auto const& p1 = idivs[i]; for (unsigned j = i + 1; j < idivs.size(); ++j) { @@ -825,6 +836,15 @@ struct purify_arith_proc { } fmc->add(u().mk_div0(), body); } + if (!mods.empty()) { + expr_ref body(u().mk_int(0), m()); + expr_ref v0(m().mk_var(0, u().mk_int()), m()); + expr_ref v1(m().mk_var(1, u().mk_int()), m()); + for (auto const& p : divs) { + body = m().mk_ite(m().mk_and(m().mk_eq(v0, p.x), m().mk_eq(v1, p.y)), p.d, body); + } + fmc->add(u().mk_mod0(), body); + } if (!idivs.empty()) { expr_ref body(u().mk_int(0), m()); expr_ref v0(m().mk_var(0, u().mk_int()), m());