Constant-fold unsigned division/remainder in bv_utils#9025
Open
tautschnig wants to merge 1 commit into
Open
Conversation
tautschnig
requested review from
kroening,
martin-cs and
peterschrammel
as code owners
There was a problem hiding this comment.
Pull request overview
This PR adds a constant-folding fast path to bv_utilst::unsigned_divider so that divisions/remainders of two constant bitvectors produce constant bitvector literals (instead of introducing fresh SAT variables plus a q*d + r == n multiplier constraint), improving downstream simplification and avoiding hard variable×variable multipliers when constant divisions feed later arithmetic.
Changes:
- Add a fast path in
bv_utilst::unsigned_dividerto directly compute quotient/remainder when both operands are constant and divisor is non-zero. - Add unit tests ensuring constant folding occurs for
100/7, and that division-by-zero still uses the existing nondeterministic encoding.
Reviewed changes
Copilot reviewed 2 out of 2 changed files in this pull request and generated 2 comments.
| File | Description |
|---|---|
| src/solvers/flattening/bv_utils.cpp | Implements constant-folding fast path for unsigned division/remainder on constant operands. |
| unit/solvers/flattening/bv_utils.cpp | Adds regression tests for constant folding and division-by-zero non-folding behavior. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## develop #9025 +/- ##
===========================================
- Coverage 80.60% 80.60% -0.01%
===========================================
Files 1711 1712 +1
Lines 189466 189538 +72
Branches 73 73
===========================================
+ Hits 152719 152776 +57
- Misses 36747 36762 +15 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
tautschnig
force-pushed
the
bvutils-constant-fold-div
branch
from
7198d09 to
90c9c1f
Compare
bv_utilst::unsigned_divider always allocated fresh variables for the quotient and remainder, with a quotient*divisor + rem == dividend multiplier constraint, even when both operands are constant. The result was therefore never a constant literal, so a constant division feeding a later multiply produced a (hard) variable*variable multiplier instead of folding away. Add a fast path: when both operands are constant (and the divisor is non-zero), compute the quotient and remainder directly as constants. Division by zero falls through to the existing nondeterministic encoding, so semantics are unchanged. The constant-bv reconstruction goes through binary2integer to mirror build_constant's use of integer2binary. Make the long-standing equal-width assumption shared by the rest of unsigned_divider (unsigned_multiplier_no_overflow / equal(sum, op0)) explicit by asserting op0.size() == op1.size() at the top of the function; this also rules out an out-of-bounds read in the new fast path. Unit-test coverage in unit/solvers/flattening/bv_utils.cpp pins: - 100 / 7 folds to constant 14 rem 2; - exact division 100 / 5 folds to 20 rem 0; - divide-by-one folds to numerator rem 0; - a non-constant divisor bypasses the fast path (guarding the is_constant(op0) && is_constant(op1) conjunction); - divide-by-zero keeps fresh variables for both quotient and remainder. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
tautschnig
force-pushed
the
bvutils-constant-fold-div
branch
from
90c9c1f to
5edac12
Compare
kroening
reviewed
Jun 10, 2026
| // Reconstruct each operand into mp_integer via binary2integer, mirroring | ||
| // the inverse used by build_constant (which calls integer2binary). | ||
| std::string s0(width, '0'), s1(width, '0'); | ||
| for(std::size_t i = 0; i < width; i++) |
Collaborator
There was a problem hiding this comment.
It might make sense to add bv_utilst::from_constant or the like.
kroening
approved these changes
Jun 10, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
bv_utilst::unsigned_divider always allocated fresh variables for the quotient and remainder, with a quotientdivisor + rem == dividend multiplier constraint, even when both operands are constant. The result was therefore never a constant literal, so a constant division feeding a later multiply produced a (hard) variablevariable multiplier instead of folding away.
Add a fast path: when both operands are constant (and the divisor is non-zero), compute the quotient and remainder directly as constants. Division by zero falls through to the existing nondeterministic encoding, so semantics are unchanged.