feat: support all the SMTLIB BitVec divison/remainder operations in b…

…v_decide (#5869)
leanprover · Oct 28, 2024 · c57d054 · c57d054
1 parent 2f1dc87
commit c57d054
Show file tree

Hide file tree

Showing 3 changed files with 73 additions and 0 deletions.
diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
@@ -2383,6 +2383,11 @@ theorem umod_eq_and {x y : BitVec 1} : x % y = x &&& (~~~y) := by
     rcases hy with rfl | rfl <;>
       rfl
 
+/-! ### smtUDiv -/
+
+theorem smtUDiv_eq (x y : BitVec w) : smtUDiv x y = if y = 0#w then allOnes w else x / y := by
+  simp [smtUDiv]
+
 /-! ### sdiv -/
 
 /-- Equation theorem for `sdiv` in terms of `udiv`. -/
@@ -2439,6 +2444,28 @@ theorem sdiv_self {x : BitVec w} :
       rcases x.msb with msb | msb <;> simp
     · rcases x.msb with msb | msb <;> simp [h]
 
+/-! ### smtSDiv -/
+
+theorem smtSDiv_eq (x y : BitVec w) : smtSDiv x y =
+  match x.msb, y.msb with
+  | false, false => smtUDiv x y
+  | false, true  => -(smtUDiv x (-y))
+  | true,  false => -(smtUDiv (-x) y)
+  | true,  true  => smtUDiv (-x) (-y) := by
+  rw [BitVec.smtSDiv]
+  rcases x.msb <;> rcases y.msb <;> simp
+
+/-! ### srem -/
+
+theorem srem_eq (x y : BitVec w) : srem x y =
+  match x.msb, y.msb with
+  | false, false => x % y
+  | false, true  => x % (-y)
+  | true,  false => - ((-x) % y)
+  | true,  true  => -((-x) % (-y)) := by
+  rw [BitVec.srem]
+  rcases x.msb <;> rcases y.msb <;> simp
+
 /-! ### smod -/
 
 /-- Equation theorem for `smod` in terms of `umod`. -/

diff --git a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean
@@ -84,6 +84,40 @@ theorem BitVec.smod_umod (x y : BitVec w) :
   rw [BitVec.smod_eq]
   cases x.msb <;> cases y.msb <;> simp
 
+attribute [bv_normalize] BitVec.smtUDiv_eq
+
+@[bv_normalize]
+theorem BitVec.smtSDiv_smtUDiv (x y : BitVec w) :
+    x.smtSDiv y =
+      if x.msb then
+        if y.msb then
+          (-x).smtUDiv (-y)
+        else
+          -((-x).smtUDiv y)
+      else
+        if y.msb then
+          -(x.smtUDiv (-y))
+        else
+          x.smtUDiv y := by
+  rw [BitVec.smtSDiv_eq]
+  cases x.msb <;> cases y.msb <;> simp
+
+@[bv_normalize]
+theorem BitVec.srem_umod (x y : BitVec w) :
+    x.srem y =
+      if x.msb then
+        if y.msb then
+          -((-x) % (-y))
+        else
+          -((-x) % y)
+      else
+        if y.msb then
+          x % (-y)
+        else
+          x % y := by
+  rw [BitVec.srem_eq]
+  cases x.msb <;> cases y.msb <;> simp
+
 attribute [bv_normalize] Bool.cond_eq_if
 attribute [bv_normalize] BitVec.abs_eq
 

diff --git a/tests/lean/run/bv_arith.lean b/tests/lean/run/bv_arith.lean
@@ -60,3 +60,15 @@ theorem arith_unit_14 (x y : BitVec 8) (hx : x.msb = true) (hy : y.msb = true) :
 
 theorem arith_unit_15 (x : BitVec 32) : BitVec.sle x (BitVec.abs x) := by
   bv_decide
+
+theorem arith_unit_16 (x y : BitVec 8)  (hy : y ≠ 0) : x.smtUDiv y = x / y := by
+  bv_decide
+
+theorem arith_unit_17 (x y : BitVec 8)  (hy : y = 0) : x.smtUDiv y = -1#8 := by
+  bv_decide
+
+theorem arith_unit_18 (x y : BitVec 8)  (hx : x.msb = true) (h : y.msb = true) : x.smtSDiv y = (-x).smtUDiv (-y) := by
+  bv_decide
+
+theorem arith_unit_19 (x y : BitVec 8)  (hx : x.msb = true) (h : y.msb = true) : x.srem y = -((-x) % (-y)) := by
+  bv_decide