Merge pull request #8789 from Z3Prover/succ_int_mult

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

src/ast/rewriter/arith_rewriter.cpp

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

src/test/arith_rewriter.cpp

@@ -33,6 +33,21 @@ static expr_ref parse_fml(ast_manager& m, char const* str) {
 static char const* example1 = "(<= (+ (* 1.3 x y) (* 2.3 y y) (* (- 1.1 x x))) 2.2)";
 static char const* example2 = "(= (+ 4 3 (- (* 3 x x) (* 5 y)) y) 0)";
 
+static expr_ref parse_int_fml(ast_manager& m, char const* str) {
+    expr_ref result(m);
+    cmd_context ctx(false, &m);
+    ctx.set_ignore_check(true);
+    std::ostringstream buffer;
+    buffer << "(declare-const I Int)\n"
+           << "(declare-const S Int)\n"
+           << "(assert " << str << ")\n";
+    std::istringstream is(buffer.str());
+    VERIFY(parse_smt2_commands(ctx, is));
+    ENSURE(!ctx.assertions().empty());
+    result = ctx.assertions().get(0);
+    return result;
+}
+
 
 void tst_arith_rewriter() {
     ast_manager m;
@@ -56,4 +71,16 @@ void tst_arith_rewriter() {
     fml = parse_fml(m, example2);
     rw(fml);
     std::cout << mk_pp(fml, m) << "\n";
+
+    // Issue #7507: (>= (* I (+ I 1)) 0) should simplify to true
+    fml = parse_int_fml(m, "(>= (* I (+ I 1)) 0)");
+    rw(fml);
+    std::cout << "consecutive product >= 0: " << mk_pp(fml, m) << "\n";
+    ENSURE(m.is_true(fml));
+
+    // (>= (* I (+ I (- 1))) 0) should also simplify to true (x*(x-1))
+    fml = parse_int_fml(m, "(>= (* I (+ I (- 1))) 0)");
+    rw(fml);
+    std::cout << "consecutive product (minus) >= 0: " << mk_pp(fml, m) << "\n";
+    ENSURE(m.is_true(fml));
 }