mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-09 06:44:53 +00:00
Code Activity

Fix #7507: simplify (>= product_of_consecutive_ints 0) to true

Browse source 
The arith rewriter now recognizes that x * (x + 1) >= 0 for all
integers, since no integer lies strictly between -1 and 0.

Two changes:
1. is_non_negative: detect products where unpaired factors are
   consecutive integer expressions (differ by exactly 1), handling
   both +1 and -1 offsets and n-ary additions
2. is_separated: return true for (>= non_negative_mul 0), restricted
   to multiplication expressions to avoid disrupting other theories

Also adds regression tests for the new simplification.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This commit is contained in:
Lev Nachmanson 2026-02-26 12:36:28 -10:00
parent 070f760501
commit 21c23e78db
2 changed files with 66 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -292,6 +292,40 @@ bool arith_rewriter::is_non_negative(expr* e) {
}
if (sign)
return false;
// For integer products, check if unpaired factors form consecutive pairs.
// x * (x + 1) >= 0 for all integers since no integer lies strictly between -1 and 0.
if (m_util.is_int(e)) {
expr_mark seen;
ptr_buffer<expr> odd_args;
for (expr* arg : args)
if (mark.is_marked(arg) && !seen.is_marked(arg)) {
seen.mark(arg, true);
odd_args.push_back(arg);
}
if (odd_args.size() == 2) {
auto is_succ = [&](expr* a, expr* b) {
if (!m_util.is_add(b))
return false;
app* add = to_app(b);
rational offset(0);
unsigned num_a = 0;
for (expr* arg : *add) {
rational c;
if (m_util.is_numeral(arg, c))
offset += c;
else if (arg == a)
++num_a;
else
return false;
}
return num_a == 1 && (offset.is_one() || offset.is_minus_one());
};
if (is_succ(odd_args[0], odd_args[1]) || is_succ(odd_args[1], odd_args[0]))
return true;
}
}
for (expr* arg : args)
if (mark.is_marked(arg))
return false;
@ -312,6 +346,11 @@ br_status arith_rewriter::is_separated(expr* arg1, expr* arg2, op_kind kind, exp
bool has_bound = true;
if (!m_util.is_numeral(arg2, r2))
return BR_FAILED;
if (kind == GE && r2.is_zero() && m_util.is_mul(arg1) && is_non_negative(arg1)) {
result = m.mk_true();
return BR_DONE;
}
auto update_bound = [&](expr* arg) {
if (m_util.is_numeral(arg, r1)) {
bound += r1;