Skip to content

feat: add a few more BitVec terms to bv_decide - #15616

Merged
hargoniX merged 1 commit into
masterfrom
hbv/bv_decide_uninterp
Oct 11, 2026
Merged

hargoniX merged 1 commit into
masterfrom
hbv/bv_decide_uninterp

Conversation

@hargoniX

@hargoniX hargoniX commented Oct 11, 2026 •

Copy link
Copy Markdown
Member

This PR adds BitVec.zero, BitVec.ofNat _ (Bool.toNat _), and BitVec.carry to the list of supported terms by bv_decide

Closes: #15580

@hargoniX hargoniX added the changelog-tactics User facing tactics label Oct 11, 2026
@github-actions github-actions Bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Oct 11, 2026
@hargoniX
hargoniX force-pushed the hbv/bv_decide_uninterp branch from 258ed8c to 0edd392 Compare October 11, 2026 13:18
@hargoniX

Copy link
Copy Markdown
Member Author

!bench

@hargoniX
hargoniX marked this pull request as ready for review October 11, 2026 13:18
@leanprover-radar

leanprover-radar commented Oct 11, 2026 •

Copy link
Copy Markdown

Benchmark results for 0edd392 against fe2da21 are in. There are significant results. @hargoniX

  • 🟥 build//instructions: +440.4M (+0.00%)

Large changes (2✅)

  • ✅ compiled/rbmap_checkpoint//task-clock: -434ms (-24.46%)
  • ✅ compiled/rbmap_checkpoint//wall-clock: -447ms (-24.93%)

Small changes (2🟥)

  • 🟥 build/module/Std.Tactic.BVDecide.Normalize.BitVec//instructions: +316.5M (+7.33%) (reduced significance based on *//lines)
  • 🟥 elab/bv_decide_rewriter//maxrss: +10MiB (+1.36%)

@hargoniX
hargoniX added this pull request to the merge queue Oct 11, 2026
Merged via the queue into master with commit 0ec0956 Oct 11, 2026
24 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

changelog-tactics User facing tactics toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Some bv_decide unsupported expressions

2 participants