94dd1d61bd
This takes a few standalone bitvector problems, about inequalties, from LNSym, and adds them as a benchmark to prevent further regressions with bv_decide. These problems are particularly interesting, because they've previously had a bad interaction with bv_decides normalization pass, see https://github.com/leanprover/lean4/issues/5664. --------- Co-authored-by: Henrik Böving <hargonix@gmail.com>
53 lines
1.7 KiB
Text
53 lines
1.7 KiB
Text
import Std.Tactic.BVDecide
|
||
|
||
/-! Smaller real-world problems taken from https://github.com/leanprover/LNSym,
|
||
which previously had a bad interaction with the normalization pass -/
|
||
|
||
variable (a1 a2 b1 b2 a b c d k n : BitVec 64)
|
||
|
||
example :
|
||
(!decide (b1 - a1 ≤ a2 - a1) && !decide (b2 - a1 ≤ a2 - a1) && !decide (a1 - b1 ≤ b2 - b1) &&
|
||
!decide (a2 - b1 ≤ b2 - b1)) =
|
||
(!decide (a1 - b1 ≤ b2 - b1) && !decide (a2 - b1 ≤ b2 - b1) && !decide (b1 - a1 ≤ a2 - a1) &&
|
||
!decide (b2 - a1 ≤ a2 - a1)) := by
|
||
bv_decide
|
||
|
||
example :
|
||
a2 - a1 < b1 - a1
|
||
→ a2 - a1 < b2 - a1
|
||
→ b2 - b1 < a1 - b1
|
||
→ b2 - b1 < a2 - b1
|
||
→ ¬a1 = b1 := by
|
||
bv_decide
|
||
|
||
example : ¬a = b ↔ 0#64 < b - a ∧ 0#64 < a - b := by
|
||
bv_decide
|
||
|
||
example :
|
||
b - a < c - a → b - a < d - a → d - c < a - c → d - c < b - c
|
||
→ (0#64 < c - a ∧ 0#64 < d - a) ∧ d - c < a - c := by
|
||
bv_decide
|
||
|
||
set_option sat.timeout 120 in
|
||
example :
|
||
n < 18446744073709551615#64 - k →
|
||
((a + k - a < a + k + 1#64 - a ∧ a + k - a < a + k + 1#64 + n - a) ∧
|
||
a + k + 1#64 + n - (a + k + 1#64) < a - (a + k + 1#64)) ∧
|
||
a + k + 1#64 + n - (a + k + 1#64) < a + k - (a + k + 1#64) := by
|
||
bv_decide
|
||
|
||
example :
|
||
n < 18446744073709551615 →
|
||
(0#64 < addr + 1#64 - addr ∧ 0#64 < addr + 1#64 + n - addr)
|
||
∧ addr + 1#64 + n - (addr + 1#64) < addr - (addr + 1#64) := by
|
||
bv_decide
|
||
|
||
set_option sat.timeout 120 in
|
||
example :
|
||
a2 - a1 < b1 - a1 → a2 - a1 < b2 - a1 →
|
||
b2 - b1 < a1 - b1 → b2 - b1 < a2 - b1 →
|
||
b2 - b1 = 18446744073709551615#64 ∨ c2 - b1 ≤ b2 - b1 ∧ c1 - b1 ≤ c2 - b1 →
|
||
((a2 - a1 < c1 - a1 ∧ a2 - a1 < c2 - a1)
|
||
∧ c2 - c1 < a1 - c1)
|
||
∧ c2 - c1 < a2 - c1 := by
|
||
bv_decide
|