mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-23 14:11:28 +00:00
Code Activity

add rewrite to eliminate quot-rem tautologies

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-11-07 08:04:03 -08:00
parent a3ec6a0f1b
commit 5d36f53cd3
2 changed files with 34 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1037,7 +1037,38 @@ br_status arith_rewriter::mk_add_core(unsigned num_args, expr * const * args, ex
} }
} }
// k * (div x k) = x - (mod x k)
br_status arith_rewriter::mk_mul_div(unsigned num_args, expr *const *args, expr_ref &result) {
if (num_args <= 1)
return BR_FAILED;
expr* x = nullptr, *y = nullptr;
rational r, q;
for (unsigned i = 0; i < num_args; ++i) {
auto arg = args[i];
if (m_util.is_idiv(arg, x, y) && m_util.is_numeral(y, r) && r > 0) {
for (unsigned j = 0; j < num_args; ++j) {
if (m_util.is_numeral(args[j], q) && q == r) {
// r * div(x, r) = (x - mod(x, r))
expr_ref_buffer new_args(m);
for (unsigned k = 0; k < num_args; ++k) {
if (k != i && k != j)
new_args.push_back(args[i]);
}
new_args.push_back(m_util.mk_sub(x, m_util.mk_mod(x, y)));
result = m.mk_app(get_fid(), OP_MUL, new_args.size(), new_args.data());
return BR_REWRITE2;
}
}
}
}
return BR_FAILED;
}
br_status arith_rewriter::mk_mul_core(unsigned num_args, expr * const * args, expr_ref & result) { br_status arith_rewriter::mk_mul_core(unsigned num_args, expr * const * args, expr_ref & result) {
br_status st = mk_mul_div(num_args, args, result);
if (st != BR_FAILED)
return st;
if (is_anum_simp_target(num_args, args)) { if (is_anum_simp_target(num_args, args)) {
expr_ref_buffer new_args(m); expr_ref_buffer new_args(m);
anum_manager & am = m_util.am(); anum_manager & am = m_util.am();
@ -1074,7 +1105,7 @@ br_status arith_rewriter::mk_mul_core(unsigned num_args, expr * const * args, ex
} }
new_args.push_back(m_util.mk_numeral(am, r, false)); new_args.push_back(m_util.mk_numeral(am, r, false));
br_status st = poly_rewriter<arith_rewriter_core>::mk_mul_core(new_args.size(), new_args.data(), result); st = poly_rewriter<arith_rewriter_core>::mk_mul_core(new_args.size(), new_args.data(), result);
if (st == BR_FAILED) { if (st == BR_FAILED) {
result = m.mk_app(get_fid(), OP_MUL, new_args.size(), new_args.data()); result = m.mk_app(get_fid(), OP_MUL, new_args.size(), new_args.data());
return BR_DONE; return BR_DONE;

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

@ -113,6 +113,7 @@ class arith_rewriter : public poly_rewriter<arith_rewriter_core> {
bool get_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); expr_ref remove_divisor(expr* arg, expr* num, expr* den);
void flat_mul(expr* e, ptr_buffer<expr>& args); void flat_mul(expr* e, ptr_buffer<expr>& args);
br_status mk_mul_div(unsigned num_args, expr * const * args, expr_ref & result);
void remove_divisor(expr* d, ptr_buffer<expr>& args); void remove_divisor(expr* d, ptr_buffer<expr>& args);
bool mk_eq_mod(expr* arg1, expr* arg2, expr_ref& result); bool mk_eq_mod(expr* arg1, expr* arg2, expr_ref& result);
@ -141,6 +142,7 @@ public:
br_status mk_add_core(unsigned num_args, expr * const * args, expr_ref & result); br_status mk_add_core(unsigned num_args, expr * const * args, expr_ref & result);
br_status mk_mul_core(unsigned num_args, expr * const * args, expr_ref & result); br_status mk_mul_core(unsigned num_args, expr * const * args, expr_ref & result);
void mk_eq(expr * arg1, expr * arg2, expr_ref & result) { void mk_eq(expr * arg1, expr * arg2, expr_ref & result) {
if (mk_eq_core(arg1, arg2, result) == BR_FAILED) if (mk_eq_core(arg1, arg2, result) == BR_FAILED)
result = m_util.mk_eq(arg1, arg2); result = m_util.mk_eq(arg1, arg2);