feat: bv_decide BitVec.sdiv

src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.lean

@@ -29,6 +29,7 @@ instance : ToExpr BVBinOp where
     | .mul => mkConst ``BVBinOp.mul
     | .udiv => mkConst ``BVBinOp.udiv
     | .umod => mkConst ``BVBinOp.umod
+    | .sdiv => mkConst ``BVBinOp.sdiv
   toTypeExpr := mkConst ``BVBinOp
 
 instance : ToExpr BVUnOp where

src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVExpr.lean

@@ -102,6 +102,8 @@ where
       binaryReflection lhsExpr rhsExpr .udiv ``Std.Tactic.BVDecide.Reflect.BitVec.udiv_congr
     | HMod.hMod _ _ _ _ lhsExpr rhsExpr =>
       binaryReflection lhsExpr rhsExpr .umod ``Std.Tactic.BVDecide.Reflect.BitVec.umod_congr
+    | BitVec.sdiv _ lhsExpr rhsExpr =>
+      binaryReflection lhsExpr rhsExpr .sdiv ``Std.Tactic.BVDecide.Reflect.BitVec.sdiv_congr
     | Complement.complement _ _ innerExpr =>
       unaryReflection innerExpr .not ``Std.Tactic.BVDecide.Reflect.BitVec.not_congr
     | HShiftLeft.hShiftLeft _ β _ _ innerExpr distanceExpr =>

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean

@@ -73,6 +73,10 @@ inductive BVBinOp where
   Unsigned modulo.
   -/
   | umod
+  /--
+  Signed division.
+  -/
+  | sdiv
 
 namespace BVBinOp
 
@@ -84,6 +88,7 @@ def toString : BVBinOp → String
   | mul => "*"
   | udiv => "/ᵤ"
   | umod => "%ᵤ"
+  | sdiv => "/ₛ"
 
 instance : ToString BVBinOp := ⟨toString⟩
 
@@ -98,6 +103,7 @@ def eval : BVBinOp → (BitVec w → BitVec w → BitVec w)
   | mul => (· * ·)
   | udiv => (· / ·)
   | umod => (· % · )
+  | sdiv => BitVec.sdiv
 
 @[simp] theorem eval_and : eval .and = ((· &&& ·) : BitVec w → BitVec w → BitVec w) := by rfl
 @[simp] theorem eval_or : eval .or = ((· ||| ·) : BitVec w → BitVec w → BitVec w) := by rfl
@@ -106,6 +112,7 @@ def eval : BVBinOp → (BitVec w → BitVec w → BitVec w)
 @[simp] theorem eval_mul : eval .mul = ((· * ·) : BitVec w → BitVec w → BitVec w) := by rfl
 @[simp] theorem eval_udiv : eval .udiv = ((· / ·) : BitVec w → BitVec w → BitVec w) := by rfl
 @[simp] theorem eval_umod : eval .umod = ((· % ·) : BitVec w → BitVec w → BitVec w) := by rfl
+@[simp] theorem eval_sdiv : eval .sdiv = (BitVec.sdiv : BitVec w → BitVec w → BitVec w) := by rfl
 
 end BVBinOp
 

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.lean

@@ -21,6 +21,7 @@ import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.SignExtend
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Mul
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Udiv
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Umod
+import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Sdiv
 
 /-!
 This module contains the implementation of a bitblaster for `BitVec` expressions (`BVExpr`).
@@ -117,6 +118,13 @@ where
           dsimp only at hlaig hraig
           omega
         ⟨res, this⟩
+      | .sdiv =>
+        let res := bitblast.blastSdiv aig ⟨lhs, rhs⟩
+        have := by
+          apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := bitblast.blastSdiv)
+          dsimp only at hlaig hraig
+          omega
+        ⟨res, this⟩
     | .un op expr =>
       let ⟨⟨eaig, evec⟩, heaig⟩ := go aig expr
       match op with
@@ -227,7 +235,7 @@ theorem bitblast.go_decl_eq (aig : AIG BVBit) (expr : BVExpr w) :
     rw [AIG.LawfulVecOperator.decl_eq (f := blastConst)]
   | bin lhs op rhs lih rih =>
     match op with
-    | .and | .or | .xor | .add | .mul | .udiv | .umod =>
+    | .and | .or | .xor | .add | .mul | .udiv | .umod | .sdiv =>
       dsimp only [go]
       have := (bitblast.go aig lhs).property
       have := (go (go aig lhs).1.aig rhs).property

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Sdiv.lean

@@ -0,0 +1,230 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+prelude
+import Std.Sat.AIG.If
+import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Neg
+import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Udiv
+
+/-!
+This module contains the implementation of a bitblaster for `BitVec.sdiv`. The implemented
+circuit is the reduction to udiv.
+-/
+
+namespace Std.Tactic.BVDecide
+
+open Std.Sat
+
+namespace BVExpr
+namespace bitblast
+
+variable [Hashable α] [DecidableEq α]
+
+namespace blastSdiv
+
+structure SignBranchInput (aig : AIG α) (len : Nat) where
+  w : Nat
+  lhs : AIG.RefVec aig w
+  rhs : AIG.RefVec aig w
+  lposRpos : AIG.RefVec aig len
+  lposRneg : AIG.RefVec aig len
+  lnegRpos : AIG.RefVec aig len
+  lnegRneg : AIG.RefVec aig len
+  hnezero : w ≠ 0
+
+def signBranch (aig : AIG α) (input : SignBranchInput aig len) : AIG.RefVecEntry α len :=
+  let ⟨w, lhs, rhs, lposRpos, lposRneg, lnegRpos, lnegRneg, hnezero⟩ := input
+  let res := AIG.RefVec.ite aig ⟨rhs.get (w - 1) (by omega), lposRneg, lposRpos⟩
+  let aig := res.aig
+  let lposHalf := res.vec
+  have := AIG.LawfulVecOperator.le_size (f := AIG.RefVec.ite) ..
+  let lhs := lhs.cast this
+  let rhs := rhs.cast this
+  let lnegRneg := lnegRneg.cast this
+  let lnegRpos := lnegRpos.cast this
+
+  let res := AIG.RefVec.ite aig ⟨rhs.get (w - 1) (by omega), lnegRneg, lnegRpos⟩
+  let aig := res.aig
+  let lnegHalf := res.vec
+  have := AIG.LawfulVecOperator.le_size (f := AIG.RefVec.ite) ..
+  let lhs := lhs.cast this
+  let lposHalf := lposHalf.cast this
+
+  AIG.RefVec.ite aig ⟨lhs.get (w - 1) (by omega), lnegHalf, lposHalf⟩
+
+instance : AIG.LawfulVecOperator α SignBranchInput signBranch where
+  le_size := by
+    intros
+    unfold signBranch
+    dsimp only
+    apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := AIG.RefVec.ite)
+    apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := AIG.RefVec.ite)
+    apply AIG.LawfulVecOperator.le_size (f := AIG.RefVec.ite)
+  decl_eq := by
+    intros
+    unfold signBranch
+    dsimp only
+    rw [AIG.LawfulVecOperator.decl_eq (f := AIG.RefVec.ite)]
+    rw [AIG.LawfulVecOperator.decl_eq (f := AIG.RefVec.ite)]
+    rw [AIG.LawfulVecOperator.decl_eq (f := AIG.RefVec.ite)]
+    · apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := AIG.RefVec.ite)
+      assumption
+    · apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := AIG.RefVec.ite)
+      apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := AIG.RefVec.ite)
+      assumption
+
+end blastSdiv
+
+def blastSdiv (aig : AIG α) (input : AIG.BinaryRefVec aig w) : AIG.RefVecEntry α w :=
+  if h : w = 0 then
+    ⟨aig, h ▸ AIG.RefVec.empty⟩
+  else
+    let ⟨lhs, rhs⟩ := input
+    let res := blastNeg aig lhs
+    let aig := res.aig
+    let negLhs := res.vec
+    have := AIG.LawfulVecOperator.le_size (f := blastNeg) ..
+    let lhs := lhs.cast this
+    let rhs := rhs.cast this
+    let res := blastNeg aig rhs
+    let aig := res.aig
+    let negRhs := res.vec
+    have := AIG.LawfulVecOperator.le_size (f := blastNeg) ..
+    let lhs := lhs.cast this
+    let rhs := rhs.cast this
+    let negLhs := negLhs.cast this
+
+    let res := blastUdiv aig ⟨lhs, rhs⟩
+    let aig := res.aig
+    let lposRpos := res.vec
+    have := AIG.LawfulVecOperator.le_size (f := blastUdiv) ..
+    let lhs := lhs.cast this
+    let rhs := rhs.cast this
+    let negRhs := negRhs.cast this
+    let negLhs := negLhs.cast this
+
+    let res := blastUdiv aig ⟨lhs, negRhs⟩
+    let aig := res.aig
+    let ldivnr := res.vec
+    let res := blastNeg aig ldivnr
+    let aig := res.aig
+    let lposRneg := res.vec
+    have := by
+      apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := blastNeg)
+      apply AIG.LawfulVecOperator.le_size (f := blastUdiv)
+    let lhs := lhs.cast this
+    let rhs := rhs.cast this
+    let negRhs := negRhs.cast this
+    let negLhs := negLhs.cast this
+    let lposRpos := lposRpos.cast this
+
+    let res := blastUdiv aig ⟨negLhs, rhs⟩
+    let aig := res.aig
+    let nldivr := res.vec
+    let res := blastNeg aig nldivr
+    let aig := res.aig
+    let lnegRpos := res.vec
+    have := by
+      apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := blastNeg)
+      apply AIG.LawfulVecOperator.le_size (f := blastUdiv)
+    let lhs := lhs.cast this
+    let rhs := rhs.cast this
+    let negRhs := negRhs.cast this
+    let negLhs := negLhs.cast this
+    let lposRpos := lposRpos.cast this
+    let lposRneg := lposRneg.cast this
+
+    let res := blastUdiv aig ⟨negLhs, negRhs⟩
+    let aig := res.aig
+    let lnegRneg := res.vec
+    have := AIG.LawfulVecOperator.le_size (f := blastUdiv) ..
+    let lhs := lhs.cast this
+    let rhs := rhs.cast this
+    let lposRpos := lposRpos.cast this
+    let lposRneg := lposRneg.cast this
+    let lnegRpos := lnegRpos.cast this
+
+    blastSdiv.signBranch aig ⟨w, lhs, rhs, lposRpos, lposRneg, lnegRpos, lnegRneg, h⟩
+
+instance : AIG.LawfulVecOperator α AIG.BinaryRefVec blastSdiv where
+  le_size := by
+    intros
+    unfold blastSdiv
+    dsimp only
+    split
+    · simp
+    · apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := blastSdiv.signBranch)
+      apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := blastUdiv)
+      apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := blastNeg)
+      apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := blastUdiv)
+      apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := blastNeg)
+      apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := blastUdiv)
+      apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := blastUdiv)
+      apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := blastNeg)
+      apply AIG.LawfulVecOperator.le_size (f := blastNeg)
+  decl_eq := by
+    intros
+    unfold blastSdiv
+    dsimp only
+    split
+    · simp
+    · rw [AIG.LawfulVecOperator.decl_eq (f := blastSdiv.signBranch)]
+      rw [AIG.LawfulVecOperator.decl_eq (f := blastUdiv)]
+      rw [AIG.LawfulVecOperator.decl_eq (f := blastNeg)]
+      rw [AIG.LawfulVecOperator.decl_eq (f := blastUdiv)]
+      rw [AIG.LawfulVecOperator.decl_eq (f := blastNeg)]
+      rw [AIG.LawfulVecOperator.decl_eq (f := blastUdiv)]
+      rw [AIG.LawfulVecOperator.decl_eq (f := blastUdiv)]
+      rw [AIG.LawfulVecOperator.decl_eq (f := blastNeg)]
+      rw [AIG.LawfulVecOperator.decl_eq (f := blastNeg)]
+      · apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastNeg)
+        assumption
+      · apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastNeg)
+        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastNeg)
+        assumption
+      · apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastUdiv)
+        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastNeg)
+        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastNeg)
+        assumption
+      · apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastUdiv)
+        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastUdiv)
+        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastNeg)
+        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastNeg)
+        assumption
+      · apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastNeg)
+        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastUdiv)
+        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastUdiv)
+        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastNeg)
+        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastNeg)
+        assumption
+      · apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastUdiv)
+        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastNeg)
+        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastUdiv)
+        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastUdiv)
+        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastNeg)
+        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastNeg)
+        assumption
+      · apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastNeg)
+        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastUdiv)
+        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastNeg)
+        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastUdiv)
+        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastUdiv)
+        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastNeg)
+        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastNeg)
+        assumption
+      · apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastUdiv)
+        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastNeg)
+        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastUdiv)
+        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastNeg)
+        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastUdiv)
+        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastUdiv)
+        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastNeg)
+        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastNeg)
+        assumption
+
+end bitblast
+end BVExpr
+
+end Std.Tactic.BVDecide

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean

@@ -21,6 +21,7 @@ import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.SignExtend
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Mul
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Udiv
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Umod
+import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Sdiv
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
 
 /-!
@@ -218,6 +219,18 @@ theorem go_denote_eq (aig : AIG BVBit) (expr : BVExpr w) (assign : Assignment) :
         · simp [Ref.hgate]
       · intros
         rw [← rih]
+    | sdiv =>
+      simp only [go, eval_bin, BVBinOp.eval_sdiv]
+      apply denote_blastSdiv
+      · intros
+        dsimp only
+        rw [go_denote_mem_prefix]
+        rw [← lih (aig := aig)]
+        · simp
+        · assumption
+        · simp [Ref.hgate]
+      · intros
+        rw [← rih]
   | un op expr ih =>
     cases op with
     | not => simp [go, ih, hidx]