From 94dd1d61bd65cb039c105febc3bc77cdf696f5d5 Mon Sep 17 00:00:00 2001
From: Alex Keizer <alex@keizer.dev>
Date: Tue, 15 Oct 2024 03:51:14 -0500
Subject: [PATCH] feat: bv_decide inequality regression tests (#5714)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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>
---
 tests/bench/bv_decide_inequality.lean    | 53 ++++++++++++++++++++++++
 tests/bench/speedcenter.exec.velcom.yaml |  6 +++
 2 files changed, 59 insertions(+)
 create mode 100644 tests/bench/bv_decide_inequality.lean

diff --git a/tests/bench/bv_decide_inequality.lean b/tests/bench/bv_decide_inequality.lean
new file mode 100644
index 0000000000..023de494a5
--- /dev/null
+++ b/tests/bench/bv_decide_inequality.lean
@@ -0,0 +1,53 @@
+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
diff --git a/tests/bench/speedcenter.exec.velcom.yaml b/tests/bench/speedcenter.exec.velcom.yaml
index 2cdc6ba067..ce08a96f6a 100644
--- a/tests/bench/speedcenter.exec.velcom.yaml
+++ b/tests/bench/speedcenter.exec.velcom.yaml
@@ -356,3 +356,9 @@
   run_config:
     <<: *time
     cmd: lean bv_decide_mod.lean
+- attributes:
+    description: bv_decide_inequality.lean
+    tags: [fast]
+  run_config:
+    <<: *time
+    cmd: lean bv_decide_inequality.lean