Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

feat: bitblasting theorems for signed comparisons #4201

Merged
merged 9 commits into from
May 23, 2024
Merged

feat: bitblasting theorems for signed comparisons #4201

merged 9 commits into from
May 23, 2024

Conversation

alexkeizer
Copy link
Contributor

Prove theorems that relate BitVec.slt and sle to carry, so that these signed comparisons may be bitblasted in LeanSAT.

This PR is stacked on top of #4200. For the diff without changes from that PR, see: opencompl/lean4@opencompl:lean4:bitvec-toInt-iff-msb...bitvec-slt-blast

@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 May 17, 2024
@leanprover-community-mathlib4-bot
Copy link
Collaborator

leanprover-community-mathlib4-bot commented May 17, 2024 •
edited
Loading

Mathlib CI status (docs):

  • ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2024-05-17 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. (2024-05-17 16:42:25)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase f97a7d4234bd76bc0f61e43b8c6a78117c1376df --onto ff37e5d512efcd3981290270a2fc3ecb100bbd0c. (2024-05-22 15:30:15)

@kim-em
Copy link
Collaborator

kim-em commented May 21, 2024

Otherwise, LGTM.

@kim-em kim-em added the awaiting-author Waiting for PR author to address issues label May 21, 2024
@alexkeizer
Copy link
Contributor Author

@semorrison I've addressed all your comments. As soon as #4200 is merged, we can rebase this PR and it should be ready to go, too

@alexkeizer alexkeizer marked this pull request as ready for review May 22, 2024 18:14
@alexkeizer
Copy link
Contributor Author

@semorrison I've rebased, this should be ready to merge

@kim-em kim-em removed the awaiting-author Waiting for PR author to address issues label May 23, 2024
@kim-em kim-em added this pull request to the merge queue May 23, 2024
Merged via the queue into leanprover:master with commit 4fa3b3c May 23, 2024
12 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@kim-em kim-em kim-em left review comments

Assignees
No one assigned
Labels
toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@alexkeizer @leanprover-community-mathlib4-bot @kim-em