From 1cdefa81b7dacdb65ad85097f62fa0ba7cba9739 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 3 Jan 2024 13:46:27 -0800 Subject: [PATCH] degree reduction simplification to help int-blasting Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/arith_rewriter.cpp | 32 ++++++++++++++++++----------- src/ast/rewriter/arith_rewriter.h | 2 +- src/sat/smt/intblast_solver.cpp | 14 +++++++++---- 3 files changed, 31 insertions(+), 17 deletions(-) diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index d8a06ada6..85fb2a3a2 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -1119,7 +1119,7 @@ br_status arith_rewriter::mk_idiv_core(expr * arg1, expr * arg2, expr_ref & resu return BR_REWRITE3; } } - if (divides(arg1, arg2, result)) { + if (get_divides(arg1, arg2, result)) { expr_ref zero(m_util.mk_int(0), m); result = m.mk_ite(m.mk_eq(zero, arg2), m_util.mk_idiv(arg1, zero), result); return BR_REWRITE_FULL; @@ -1137,7 +1137,7 @@ br_status arith_rewriter::mk_idiv_core(expr * arg1, expr * arg2, expr_ref & resu // // implement div ab ac = floor( ab / ac) = floor (b / c) = div b c // -bool arith_rewriter::divides(expr* num, expr* den, expr_ref& result) { +bool arith_rewriter::get_divides(expr* num, expr* den, expr_ref& result) { expr_fast_mark1 mark; rational num_r(1), den_r(1); expr* num_e = nullptr, *den_e = nullptr; @@ -1234,17 +1234,20 @@ br_status arith_rewriter::mk_mod_core(expr * arg1, expr * arg2, expr_ref & resul set_curr_sort(arg1->get_sort()); numeral v1, v2; bool is_int; - if (m_util.is_numeral(arg1, v1, is_int) && m_util.is_numeral(arg2, v2, is_int) && !v2.is_zero()) { + bool is_num1 = m_util.is_numeral(arg1, v1, is_int); + bool is_num2 = m_util.is_numeral(arg2, v2, is_int); + + if (is_num1 && is_num2 && !v2.is_zero()) { result = m_util.mk_numeral(mod(v1, v2), is_int); return BR_DONE; } - if (m_util.is_numeral(arg2, v2, is_int) && is_int && (v2.is_one() || v2.is_minus_one())) { + if (is_num2 && is_int && (v2.is_one() || v2.is_minus_one())) { result = m_util.mk_numeral(numeral(0), true); return BR_DONE; } - if (arg1 == arg2 && !m_util.is_numeral(arg2)) { + if (arg1 == arg2 && !is_num2) { expr_ref zero(m_util.mk_int(0), m); result = m.mk_ite(m.mk_eq(arg2, zero), m_util.mk_mod(zero, zero), zero); return BR_DONE; @@ -1252,13 +1255,13 @@ br_status arith_rewriter::mk_mod_core(expr * arg1, expr * arg2, expr_ref & resul // mod is idempotent on non-zero modulus. expr* t1, *t2; - if (m_util.is_mod(arg1, t1, t2) && t2 == arg2 && m_util.is_numeral(arg2, v2, is_int) && is_int && !v2.is_zero()) { + if (m_util.is_mod(arg1, t1, t2) && t2 == arg2 && is_num2 && is_int && !v2.is_zero()) { result = arg1; return BR_DONE; } // propagate mod inside only if there is something to reduce. - if (m_util.is_numeral(arg2, v2, is_int) && is_int && v2.is_pos() && (is_add(arg1) || is_mul(arg1))) { + if (is_num2 && is_int && v2.is_pos() && (is_add(arg1) || is_mul(arg1))) { TRACE("mod_bug", tout << "mk_mod:\n" << mk_ismt2_pp(arg1, m) << "\n" << mk_ismt2_pp(arg2, m) << "\n";); expr_ref_buffer args(m); bool change = false; @@ -1280,12 +1283,17 @@ br_status arith_rewriter::mk_mod_core(expr * arg1, expr * arg2, expr_ref & resul args.push_back(arg); } } - if (!change) { - return BR_FAILED; // did not find any target for applying simplification + if (change) { + result = m_util.mk_mod(m.mk_app(to_app(arg1)->get_decl(), args.size(), args.data()), arg2); + TRACE("mod_bug", tout << "mk_mod result: " << mk_ismt2_pp(result, m) << "\n";); + return BR_REWRITE3; } - result = m_util.mk_mod(m.mk_app(to_app(arg1)->get_decl(), args.size(), args.data()), arg2); - TRACE("mod_bug", tout << "mk_mod result: " << mk_ismt2_pp(result, m) << "\n";); - return BR_REWRITE3; + } + + expr* x, *y; + if (is_num2 && v2.is_pos() && m_util.is_mul(arg1, x, y) && m_util.is_numeral(x, v1, is_int) && divides(v1, v2)) { + result = m_util.mk_mul(x, m_util.mk_mod(y, m_util.mk_int(v2/v1))); + return BR_REWRITE1; } return BR_FAILED; diff --git a/src/ast/rewriter/arith_rewriter.h b/src/ast/rewriter/arith_rewriter.h index 6066c9eb4..d59486273 100644 --- a/src/ast/rewriter/arith_rewriter.h +++ b/src/ast/rewriter/arith_rewriter.h @@ -103,7 +103,7 @@ class arith_rewriter : public poly_rewriter { expr_ref neg_monomial(expr * e); expr * mk_sin_value(rational const & k); app * mk_sqrt(rational const & k); - bool divides(expr* d, expr* n, expr_ref& result); + bool get_divides(expr* d, expr* n, expr_ref& result); expr_ref remove_divisor(expr* arg, expr* num, expr* den); void flat_mul(expr* e, ptr_buffer& args); void remove_divisor(expr* d, ptr_buffer& args); diff --git a/src/sat/smt/intblast_solver.cpp b/src/sat/smt/intblast_solver.cpp index d6bff7804..f47c3efc0 100644 --- a/src/sat/smt/intblast_solver.cpp +++ b/src/sat/smt/intblast_solver.cpp @@ -226,11 +226,17 @@ namespace intblast { m_solver->assert_expr(a.mk_le(a.mk_int(0), v)); m_solver->assert_expr(a.mk_lt(v, a.mk_int(b))); } - + IF_VERBOSE(2, verbose_stream() << "check\n" << original_es << "\n"); - IF_VERBOSE(3, verbose_stream() << "check\n"; - m_solver->display(verbose_stream()); - verbose_stream() << es << "\n"); + + IF_VERBOSE(2, + { + m_solver->push(); + m_solver->assert_expr(es); + m_solver->display(verbose_stream()) << "(check-sat)\n"; + m_solver->pop(1); + }); + r = m_solver->check_sat(es); }