mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

degree reduction simplification to help int-blasting

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-01-03 13:46:27 -08:00
parent 698c627359
commit 1cdefa81b7
3 changed files with 31 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

32
src/ast/rewriter/arith_rewriter.cpp
View file

@ -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;

2
src/ast/rewriter/arith_rewriter.h
View file

@ -103,7 +103,7 @@ class arith_rewriter : public poly_rewriter<arith_rewriter_core> {
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<expr>& args);
void remove_divisor(expr* d, ptr_buffer<expr>& args);

14
src/sat/smt/intblast_solver.cpp
View file

@ -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);
}