From eaceded5f141748a959a81bf91572ce79141aa97 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 12 Jul 2026 13:35:57 -0700 Subject: [PATCH] Issue 438 (#10085) Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> --- src/ast/bv_decl_plugin.cpp | 27 ++++++++++ src/ast/bv_decl_plugin.h | 20 ++++++++ src/ast/simplifiers/CMakeLists.txt | 1 + src/ast/simplifiers/bv_divrem_bounds.cpp | 43 ++++++++++++++++ src/ast/simplifiers/bv_divrem_bounds.h | 64 ++++++++++++++++++++++++ src/sat/smt/bv_internalize.cpp | 24 +++++++-- src/sat/smt/bv_solver.h | 1 + src/smt/theory_bv.cpp | 31 +++++++++--- src/smt/theory_bv.h | 1 + src/tactic/bv/CMakeLists.txt | 1 + src/tactic/bv/bv_divrem_bounds_tactic.h | 63 +++++++++++++++++++++++ src/tactic/smtlogics/qfaufbv_tactic.cpp | 2 + src/tactic/smtlogics/qfbv_tactic.cpp | 2 + 13 files changed, 269 insertions(+), 11 deletions(-) create mode 100644 src/ast/simplifiers/bv_divrem_bounds.cpp create mode 100644 src/ast/simplifiers/bv_divrem_bounds.h create mode 100644 src/tactic/bv/bv_divrem_bounds_tactic.h diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp index bb65581cce..74368ecec5 100644 --- a/src/ast/bv_decl_plugin.cpp +++ b/src/ast/bv_decl_plugin.cpp @@ -997,3 +997,30 @@ app* bv_util::mk_bv_rotate_right(expr* arg, unsigned n) { parameter p(n); return m_manager.mk_app(get_fid(), OP_ROTATE_RIGHT, 1, &p, 1, &arg); } + +void bv_util::mk_bv_divrem_bound(expr* t, expr_ref_vector& clause) { + clause.reset(); + if (!is_app(t) || !is_bv_divrem(t)) + return; + expr* a = to_app(t)->get_arg(0); + expr* b = to_app(t)->get_arg(1); + if (is_numeral(b)) + return; + expr* bound = nullptr; + // Use ¬(b ≤u t) instead of (t bound as the disjunction (b = 0) \/ bound + clause.push_back(m_manager.mk_eq(b, mk_zero(b->get_sort()))); + clause.push_back(bound); +} diff --git a/src/ast/bv_decl_plugin.h b/src/ast/bv_decl_plugin.h index 225fda0d60..8900c53d0a 100644 --- a/src/ast/bv_decl_plugin.h +++ b/src/ast/bv_decl_plugin.h @@ -473,6 +473,7 @@ public: app * mk_ule(expr * arg1, expr * arg2) { return m_manager.mk_app(get_fid(), OP_ULEQ, arg1, arg2); } + app * mk_ult(expr * arg1, expr * arg2) { return m_manager.mk_app(get_fid(), OP_ULT, arg1, arg2); } app * mk_sle(expr * arg1, expr * arg2) { return m_manager.mk_app(get_fid(), OP_SLEQ, arg1, arg2); } app * mk_slt(expr * arg1, expr * arg2) { return m_manager.mk_app(get_fid(), OP_SLT, arg1, arg2); } app * mk_extract(unsigned high, unsigned low, expr * n) { @@ -499,6 +500,25 @@ public: app * mk_bv_not(expr * arg) { return m_manager.mk_app(get_fid(), OP_BNOT, arg); } app * mk_bv_neg(expr * arg) { return m_manager.mk_app(get_fid(), OP_BNEG, arg); } + // absolute value: ite(arg get_sort()), arg), arg, mk_bv_neg(arg)); } + // Magnitude-bound clause for a division/remainder term t with a symbolic (non-numeral) + // divisor. Fills clause with the disjuncts { divisor = 0, bound }, encoding + // divisor != 0 => bound, where bound is expressed using only OP_ULEQ and OP_NOT(OP_ULEQ) + // (so it can be internalized by theory_bv::internalize_atom): + // urem: ¬(b ≤u t) srem/smod: ¬(|b| ≤u |t|) + // udiv: t ≤u a sdiv: |t| ≤u |a| + // Leaves clause empty if t is not a division/remainder operator or the divisor is a + // numeral. The bound is a bit-vector theory axiom (implied for a non-zero divisor); the + // unsigned comparison on absolute values keeps it sound at INT_MIN. + bool is_bv_divrem(expr* t) const { + return is_bv_urem(t) || is_bv_uremi(t) || is_bv_srem(t) || is_bv_sremi(t) || + is_bv_smod(t) || is_bv_smodi(t) || is_bv_udiv(t) || is_bv_udivi(t) || + is_bv_sdiv(t) || is_bv_sdivi(t); + } + void mk_bv_divrem_bound(expr* t, expr_ref_vector& clause); app * mk_bv_urem(expr * arg1, expr * arg2) const { return m_manager.mk_app(get_fid(), OP_BUREM, arg1, arg2); } app * mk_bv_srem(expr * arg1, expr * arg2) const { return m_manager.mk_app(get_fid(), OP_BSREM, arg1, arg2); } app * mk_bv_smod(expr * arg1, expr * arg2) const { return m_manager.mk_app(get_fid(), OP_BSMOD, arg1, arg2); } diff --git a/src/ast/simplifiers/CMakeLists.txt b/src/ast/simplifiers/CMakeLists.txt index aae8227e4c..c3dbfa9141 100644 --- a/src/ast/simplifiers/CMakeLists.txt +++ b/src/ast/simplifiers/CMakeLists.txt @@ -6,6 +6,7 @@ z3_add_component(simplifiers bound_propagator.cpp bound_simplifier.cpp bv_bounds_simplifier.cpp + bv_divrem_bounds.cpp bv_slice.cpp card2bv.cpp demodulator_simplifier.cpp diff --git a/src/ast/simplifiers/bv_divrem_bounds.cpp b/src/ast/simplifiers/bv_divrem_bounds.cpp new file mode 100644 index 0000000000..c11f508251 --- /dev/null +++ b/src/ast/simplifiers/bv_divrem_bounds.cpp @@ -0,0 +1,43 @@ +/*++ +Copyright (c) 2026 Microsoft Corporation + +Module Name: + + bv_divrem_bounds.cpp + +Abstract: + + Simplifier that adds range/bound lemmas for bit-vector division and + remainder terms with a non-constant divisor. See bv_divrem_bounds.h. + +Author: + + Nikolaj Bjorner (nbjorner) + +--*/ +#include "ast/simplifiers/bv_divrem_bounds.h" +#include "ast/for_each_expr.h" + +namespace bv { + + void divrem_bounds::reduce() { + expr_ref_vector targets(m), fmls(m), clause(m); + for (unsigned i : indices()) + fmls.push_back(m_fmls[i].fml()); + for (expr* e : subterms::ground(fmls)) + if (m_util.is_bv_divrem(e)) + targets.push_back(e); + for (expr* t : targets) { + m_util.mk_bv_divrem_bound(t, clause); + if (clause.empty()) + continue; + expr_ref lemma(m.mk_or(clause), m); + // the lemma is a bit-vector theory axiom (valid with no premises) + proof_ref pr(m); + if (m.proofs_enabled()) + pr = m.mk_th_lemma(m_util.get_fid(), lemma, 0, nullptr); + m_fmls.add(dependent_expr(m, lemma, pr, nullptr)); + ++m_num_lemmas; + } + } +} diff --git a/src/ast/simplifiers/bv_divrem_bounds.h b/src/ast/simplifiers/bv_divrem_bounds.h new file mode 100644 index 0000000000..88c046e2d7 --- /dev/null +++ b/src/ast/simplifiers/bv_divrem_bounds.h @@ -0,0 +1,64 @@ +/*++ +Copyright (c) 2026 Microsoft Corporation + +Module Name: + + bv_divrem_bounds.h + +Abstract: + + Simplifier that adds range/bound lemmas for bit-vector division and + remainder terms with a non-constant divisor. + + Bit-blasting a division circuit with a symbolic divisor hides the algebraic + fact that the remainder magnitude is bounded by the divisor magnitude. For a + divisor b that is not a numeral the following facts hold and are added as + (implied) lemmas so that a downstream bit-blasting + SAT solver can reason + about the magnitudes without unfolding the division circuit: + + b != 0 => bvult (bvurem a b) b (unsigned remainder) + b != 0 => bvult |bvsrem a b| |b| (signed remainder) + b != 0 => bvult |bvsmod a b| |b| (signed modulo) + b != 0 => bvule (bvudiv a b) a (unsigned quotient) + b != 0 => bvule |bvsdiv a b| |a| (signed quotient) + + where |x| = ite(x & ibin, std::function& iun) { bv_rewriter_params p(s().params()); expr* arg1 = n->get_arg(0); diff --git a/src/sat/smt/bv_solver.h b/src/sat/smt/bv_solver.h index 71019981e5..75d5a8d8d8 100644 --- a/src/sat/smt/bv_solver.h +++ b/src/sat/smt/bv_solver.h @@ -288,6 +288,7 @@ namespace bv { void internalize_bit2bool(app* n); void internalize_overflow(app* n); void internalize_udiv_i(app* n); + void assert_bv_divrem_bound_axiom(app* n); template void internalize_le(app* n); void assert_bv2int_axiom(app * n); diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp index f09be95069..83d5fd28e1 100644 --- a/src/smt/theory_bv.cpp +++ b/src/smt/theory_bv.cpp @@ -908,15 +908,15 @@ namespace smt { case OP_BADD: internalize_add(term); return true; case OP_BSUB: internalize_sub(term); return true; case OP_BMUL: internalize_mul(term); return true; - case OP_BSDIV_I: internalize_sdiv(term); return true; + case OP_BSDIV_I: internalize_sdiv(term); if (!ctx.relevancy()) assert_bv_divrem_bound_axiom(term); return true; #if ENABLE_QUOT_REM_ENCODING - case OP_BUDIV_I: internalize_udiv_quot_rem(term); return true; + case OP_BUDIV_I: internalize_udiv_quot_rem(term); if (!ctx.relevancy()) assert_bv_divrem_bound_axiom(term); return true; #else - case OP_BUDIV_I: internalize_udiv(term); return true; + case OP_BUDIV_I: internalize_udiv(term); if (!ctx.relevancy()) assert_bv_divrem_bound_axiom(term); return true; #endif - case OP_BSREM_I: internalize_srem(term); return true; - case OP_BUREM_I: internalize_urem(term); return true; - case OP_BSMOD_I: internalize_smod(term); return true; + case OP_BSREM_I: internalize_srem(term); if (!ctx.relevancy()) assert_bv_divrem_bound_axiom(term); return true; + case OP_BUREM_I: internalize_urem(term); if (!ctx.relevancy()) assert_bv_divrem_bound_axiom(term); return true; + case OP_BSMOD_I: internalize_smod(term); if (!ctx.relevancy()) assert_bv_divrem_bound_axiom(term); return true; case OP_BAND: internalize_and(term); return true; case OP_BOR: internalize_or(term); return true; case OP_BNOT: internalize_not(term); return true; @@ -1395,6 +1395,11 @@ namespace smt { void theory_bv::relevant_eh(expr * n) { TRACE(arith, tout << "relevant: #" << n->get_id() << " " << ctx.e_internalized(n) << ": " << mk_bounded_pp(n, m) << "\n";); TRACE(bv, tout << "relevant: #" << n->get_id() << " " << ctx.e_internalized(n) << ": " << mk_pp(n, m) << "\n";); + if (ctx.relevancy() && m_util.is_bv_divrem(n)) { + ctx.mark_as_relevant(to_app(n)->get_arg(0)); + ctx.mark_as_relevant(to_app(n)->get_arg(1)); + assert_bv_divrem_bound_axiom(to_app(n)); + } if (m.is_bool(n)) { if (!ctx.b_internalized(n)) return; @@ -2070,5 +2075,19 @@ namespace smt { } #endif + // Add, on the fly, the magnitude bound axioms for division/remainder operators. + // Uses the shared bv_util::mk_bv_divrem_bound clause builder so the axiom matches the + // one produced by the bv-divrem-bounds simplifier. Only fires for a symbolic divisor. + void theory_bv::assert_bv_divrem_bound_axiom(app * n) { + expr_ref_vector clause(m); + m_util.mk_bv_divrem_bound(n, clause); + if (clause.empty()) + return; + literal_vector lits; + for (expr* e : clause) + lits.push_back(mk_literal(e)); + ctx.mk_th_axiom(get_id(), lits.size(), lits.data()); + } + } diff --git a/src/smt/theory_bv.h b/src/smt/theory_bv.h index 6d64b7a14d..b7b3d15f0c 100644 --- a/src/smt/theory_bv.h +++ b/src/smt/theory_bv.h @@ -229,6 +229,7 @@ namespace smt { void assert_int2bv_axiom(app* n); void assert_bv2int_axiom(app* n); void assert_udiv_quot_rem_axiom(app * n); + void assert_bv_divrem_bound_axiom(app * n); protected: diff --git a/src/tactic/bv/CMakeLists.txt b/src/tactic/bv/CMakeLists.txt index d5920b88e9..8f7c74a48f 100644 --- a/src/tactic/bv/CMakeLists.txt +++ b/src/tactic/bv/CMakeLists.txt @@ -18,6 +18,7 @@ z3_add_component(bv_tactics bv1_blaster_tactic.h bv_bound_chk_tactic.h bv_bounds_tactic.h + bv_divrem_bounds_tactic.h bv_size_reduction_tactic.h bv_slice_tactic.h bvarray2uf_tactic.h diff --git a/src/tactic/bv/bv_divrem_bounds_tactic.h b/src/tactic/bv/bv_divrem_bounds_tactic.h new file mode 100644 index 0000000000..2c6f9e77a6 --- /dev/null +++ b/src/tactic/bv/bv_divrem_bounds_tactic.h @@ -0,0 +1,63 @@ +/*++ +Copyright (c) 2026 Microsoft Corporation + +Module Name: + + bv_divrem_bounds_tactic.h + +Abstract: + + Tactic wrapper around the bv::divrem_bounds simplifier. It adds range + lemmas for bit-vector division and remainder terms with a non-constant + divisor. See ast/simplifiers/bv_divrem_bounds.h for details. + +Author: + + Nikolaj Bjorner (nbjorner) + +Tactic Documentation + +## Tactic bv-divrem-bounds + +### Short Description + +Add range lemmas for bit-vector division/remainder terms with a symbolic divisor. + +### Long Description + +For a divisor `b` that is not a numeral, the remainder magnitude is bounded by +the divisor magnitude and the unsigned quotient is bounded by the dividend. +These facts are hidden once a division circuit is bit-blasted, so the tactic +emits them as implied lemmas up front, letting a downstream SAT solver reason +about magnitudes without unfolding the circuit. + +### Example + +```z3 +(declare-const a (_ BitVec 8)) +(declare-const b (_ BitVec 8)) +(declare-const c (_ BitVec 8)) +(assert (= (bvsrem a (bvadd b c)) #x05)) +(apply bv-divrem-bounds) +``` + +--*/ +#pragma once + +#include "util/params.h" +#include "tactic/tactic.h" +#include "tactic/dependent_expr_state_tactic.h" +#include "ast/simplifiers/bv_divrem_bounds.h" + +class ast_manager; +class tactic; + +inline tactic* mk_bv_divrem_bounds_tactic(ast_manager& m, params_ref const& p = params_ref()) { + return alloc(dependent_expr_state_tactic, m, p, + [](auto& m, auto& p, auto& s) -> dependent_expr_simplifier* { return alloc(bv::divrem_bounds, m, s); }); +} + +/* + ADD_TACTIC("bv-divrem-bounds", "add range lemmas for bit-vector division/remainder terms with a symbolic divisor.", "mk_bv_divrem_bounds_tactic(m, p)") + ADD_SIMPLIFIER("bv-divrem-bounds", "add range lemmas for bit-vector division/remainder terms with a symbolic divisor.", "alloc(bv::divrem_bounds, m, s)") +*/ diff --git a/src/tactic/smtlogics/qfaufbv_tactic.cpp b/src/tactic/smtlogics/qfaufbv_tactic.cpp index acad15fd67..216214e883 100644 --- a/src/tactic/smtlogics/qfaufbv_tactic.cpp +++ b/src/tactic/smtlogics/qfaufbv_tactic.cpp @@ -23,6 +23,7 @@ Notes: #include "tactic/core/elim_uncnstr_tactic.h" #include "tactic/bv/max_bv_sharing_tactic.h" #include "tactic/bv/bv_size_reduction_tactic.h" +#include "tactic/bv/bv_divrem_bounds_tactic.h" #include "tactic/core/ctx_simplify_tactic.h" #include "tactic/smtlogics/qfbv_tactic.h" #include "tactic/smtlogics/smt_tactic.h" @@ -42,6 +43,7 @@ static tactic * mk_qfaufbv_preamble(ast_manager & m, params_ref const & p) { mk_propagate_values_tactic(m), mk_solve_eqs_tactic(m), mk_elim_uncnstr_tactic(m), + mk_bv_divrem_bounds_tactic(m), // sound to use? if_no_proofs(if_no_unsat_cores(mk_reduce_args_tactic(m))), if_no_proofs(if_no_unsat_cores(mk_bv_size_reduction_tactic(m))), using_params(mk_simplify_tactic(m), simp2_p), diff --git a/src/tactic/smtlogics/qfbv_tactic.cpp b/src/tactic/smtlogics/qfbv_tactic.cpp index 07784eb3b5..5fe94e1f16 100644 --- a/src/tactic/smtlogics/qfbv_tactic.cpp +++ b/src/tactic/smtlogics/qfbv_tactic.cpp @@ -25,6 +25,7 @@ Notes: #include "tactic/bv/bv1_blaster_tactic.h" #include "tactic/bv/max_bv_sharing_tactic.h" #include "tactic/bv/bv_size_reduction_tactic.h" +#include "tactic/bv/bv_divrem_bounds_tactic.h" #include "tactic/aig/aig_tactic.h" #include "sat/tactic/sat_tactic.h" #include "sat/sat_solver/inc_sat_solver.h" @@ -63,6 +64,7 @@ static tactic * mk_qfbv_preamble(ast_manager& m, params_ref const& p) { using_params(mk_propagate_values_tactic(m), flat_and_or_p), using_params(mk_solve_eqs_tactic(m), solve_eq_p), mk_elim_uncnstr_tactic(m), + mk_bv_divrem_bounds_tactic(m), if_no_proofs(if_no_unsat_cores(mk_bv_size_reduction_tactic(m))), using_params(mk_simplify_tactic(m), simp2_p),