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

feat: improve bv_normalize rules for Prop and == #5506

Merged
merged 3 commits into from
Sep 28, 2024
Merged

feat: improve bv_normalize rules for Prop and == #5506

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
fbc26cd
feat: == and != simproc for BitVec
hargoniX Sep 28, 2024
2dcfaba
feat: reorganize and improve bv_normalize Prop simpset
hargoniX Sep 28, 2024
b7218fa
test: fix example by @bollu
hargoniX Sep 28, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 8 additions & 0 deletions src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/BitVec.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -228,8 +228,16 @@ builtin_dsimproc [simp, seval] reduceOfNat (BitVec.ofNat _ _) := fun e => do
if bv.toNat == v then return .continue -- already normalized
return .done <| toExpr (BitVec.ofNat n v)

/-- Simplification procedure for `=` on `BitVec`s. -/
builtin_simproc [simp, seval] reduceEq (( _ : BitVec _) = _) := reduceBinPred ``Eq 3 (. = .)
/-- Simplification procedure for `≠` on `BitVec`s. -/
builtin_simproc [simp, seval] reduceNe (( _ : BitVec _) ≠ _) := reduceBinPred ``Ne 3 (. ≠ .)
/-- Simplification procedure for `==` on `BitVec`s. -/
builtin_dsimproc [simp, seval] reduceBEq (( _ : BitVec _) == _) :=
reduceBoolPred ``BEq.beq 4 (· == ·)
/-- Simplification procedure for `!=` on `BitVec`s. -/
builtin_dsimproc [simp, seval] reduceBNe (( _ : BitVec _) != _) :=
reduceBoolPred ``bne 4 (· != ·)

/-- Simplification procedure for `<` on `BitVec`s. -/
builtin_simproc [simp, seval] reduceLT (( _ : BitVec _) < _) := reduceBinPred ``LT.lt 4 (· < ·)
Expand Down
16 changes: 14 additions & 2 deletions src/Std/Tactic/BVDecide/Normalize/Prop.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,16 +13,28 @@ This module contains the `Prop` simplifying part of the `bv_normalize` simp set.
namespace Std.Tactic.BVDecide
namespace Frontend.Normalize

attribute [bv_normalize] not_true
attribute [bv_normalize] ite_true
attribute [bv_normalize] ite_false
attribute [bv_normalize] dite_true
attribute [bv_normalize] dite_false
attribute [bv_normalize] and_true
attribute [bv_normalize] true_and
attribute [bv_normalize] and_false
attribute [bv_normalize] false_and
attribute [bv_normalize] or_true
attribute [bv_normalize] true_or
attribute [bv_normalize] eq_iff_iff
attribute [bv_normalize] or_false
attribute [bv_normalize] false_or
attribute [bv_normalize] iff_true
attribute [bv_normalize] true_iff
attribute [bv_normalize] iff_false
attribute [bv_normalize] false_iff
attribute [bv_normalize] false_implies
attribute [bv_normalize] implies_true
attribute [bv_normalize] true_implies
attribute [bv_normalize] not_true
attribute [bv_normalize] not_false_iff
attribute [bv_normalize] eq_iff_iff

end Frontend.Normalize
end Std.Tactic.BVDecide
4 changes: 4 additions & 0 deletions tests/lean/run/bv_decide_rewriter.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,3 +9,7 @@ example (z : BitVec 64) : True := by
have : z + (2 * x) = y := by
bv_decide
exact True.intro

example :
¬ (0 ≤ 0 + 16#64 ∧ 0 ≤ 0 + 16#64 ∧ (0 + 16#64 ≤ 0 ∨ 0 ≥ 0 + 16#64 ∨ 16#64 = 0 ∨ 16#64 = 0)) := by
bv_normalize
Loading