Skip to content

Handle symbolic factors and denominators of known sign in is_monotonic - #9664

Open
abadams wants to merge 1 commit into
mainfrom
abadams/monotonic_symbolic_factor
Open

abadams wants to merge 1 commit into
mainfrom
abadams/monotonic_symbolic_factor

Conversation

@abadams

@abadams abadams commented Nov 4, 2026

Copy link
Copy Markdown
Member

Copilot says (description written by GitHub Copilot on behalf of @abadams):

is_monotonic's DerivativeBounds only handled a Mul where one operand is a constant, and a Div by a constant. Anything symbolic, like x / max(k, 1) with a Param k, fell back to "unknown", so sliding window and storage folding gave up on it.

This PR generalizes both cases:

  • Mul: if one operand doesn't depend on the var (its derivative bounds are exactly zero), the result is the other operand's derivative bounds times the constant_integer_bounds of the independent operand.
  • Div: if the denominator doesn't depend on the var and constant_integer_bounds proves it's strictly positive or strictly negative, the quotient moves the same way as the numerator (or the opposite way for a negative denominator), and by at most as much. Rounding matches the existing constant-denominator case: floor for the min, ceil for the max. Both bounds are clamped to include 0, because a step in the numerator can leave the quotient unchanged.

This is a precision improvement, not a miscompile fix. It lets sliding window slide over footprints like f(x / max(k, 1)). In the new sliding_window test, f is computed 35 times instead of 200. is_monotonic gets new check cases.

Found while fuzzing the sliding-window rewrite stack (#9648); split out because it applies to main independently.

Checklist

  • Tests added or updated
  • Documentation updated (if public API changed) — N/A
  • Benchmarks/performance impact considered — N/A

DerivativeBounds only handled a Mul whose other operand was constant and
a Div by a constant. Use constant_integer_bounds on a var-independent
factor or denominator so that e.g. x / max(k, 1) is recognized as
monotonic increasing. This lets sliding window slide over such
footprints.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
@codecov

codecov Bot commented Nov 5, 2026

Copy link
Copy Markdown

Codecov Report

❌ Patch coverage is 91.30435% with 2 lines in your changes missing coverage. Please review.
✅ Project coverage is 72.97%. Comparing base (8ac8ab4) to head (65709de).
⚠️ Report is 1 commits behind head on main.

Files with missing lines Patch % Lines
src/Monotonic.cpp 91.30% 0 Missing and 2 partials ⚠️
Additional details and impacted files
@@            Coverage Diff             @@
##             main    #9664      +/-   ##
==========================================
- Coverage   73.01%   72.97%   -0.04%     
==========================================
  Files         266      266              
  Lines       83355    83374      +19     
  Branches    20474    20480       +6     
==========================================
- Hits        60858    60840      -18     
- Misses      16152    16153       +1     
- Partials     6345     6381      +36     

☔ View full report in Codecov by Harness.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:
  • ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
  • 📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.

This branch has not been deployed

No deployments
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants