This module contains the implementation of a bitblaster for BitVec.udiv. The implemented circuit is a shift subtractor.

structure Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.ShiftConcatInput {α : Type} [Hashable α] [DecidableEq α] (aig : Sat.AIG α) (len : Nat) : Type

• lhs : aig.RefVec len
• bit : aig.Ref

def Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastShiftConcat {α : Type} [Hashable α] [DecidableEq α] {w : Nat} (aig : Sat.AIG α) (input : ShiftConcatInput aig w) : Sat.AIG.RefVecEntry α w

Equations

• One or more equations did not get rendered due to their size.

instance Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.instLawfulVecOperatorShiftConcatInputBlastShiftConcat {α : Type} [Hashable α] [DecidableEq α] : Sat.AIG.LawfulVecOperator α ShiftConcatInput fun {len : Nat} => blastShiftConcat

structure Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.BlastDivSubtractShiftOutput {α : Type} [Hashable α] [DecidableEq α] (old : Sat.AIG α) (w : Nat) : Type

• aig : Sat.AIG α
• wn : Nat
• wr : Nat
• q : self.aig.RefVec w
• r : self.aig.RefVec w
• hle : old.decls.size ≤ self.aig.decls.size

def Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastDivSubtractShift {α : Type} [Hashable α] [DecidableEq α] {w : Nat} (aig : Sat.AIG α) (n d : aig.RefVec w) (wn wr : Nat) (q r : aig.RefVec w) : BlastDivSubtractShiftOutput aig w

Equations

• One or more equations did not get rendered due to their size.

theorem Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastDivSubtractShift_le_size {α : Type} [Hashable α] [DecidableEq α] {w : Nat} (aig : Sat.AIG α) (n d : aig.RefVec w) (wn wr : Nat) (q r : aig.RefVec w) : aig.decls.size ≤ (blastDivSubtractShift aig n d wn wr q r).aig.decls.size

theorem Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastDivSubtractShift_decl_eq {α : Type} [Hashable α] [DecidableEq α] {w : Nat} (aig : Sat.AIG α) (n d : aig.RefVec w) (wn wr : Nat) (q r : aig.RefVec w) (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < (blastDivSubtractShift aig n d wn wr q r).aig.decls.size) : (blastDivSubtractShift aig n d wn wr q r).aig.decls[idx] = aig.decls[idx]

structure Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.BlastUdivOutput {α : Type} [Hashable α] [DecidableEq α] (old : Sat.AIG α) (w : Nat) : Type

• aig : Sat.AIG α
• q : self.aig.RefVec w
• r : self.aig.RefVec w
• hle : old.decls.size ≤ self.aig.decls.size

def Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.go {α : Type} [Hashable α] [DecidableEq α] {w : Nat} (aig : Sat.AIG α) (curr : Nat) (n d : aig.RefVec w) (wn wr : Nat) (q r : aig.RefVec w) : BlastUdivOutput aig w

Equations

• One or more equations did not get rendered due to their size.
• Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.go aig 0 n d wn wr q r = { aig := aig, q := q, r := r, hle := ⋯ }

theorem Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.go_le_size {α : Type} [Hashable α] [DecidableEq α] {w : Nat} (aig : Sat.AIG α) (curr : Nat) (n d : aig.RefVec w) (wn wr : Nat) (q r : aig.RefVec w) : aig.decls.size ≤ (go aig curr n d wn wr q r).aig.decls.size

theorem Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.go_decl_eq {α : Type} [Hashable α] [DecidableEq α] {w : Nat} (aig : Sat.AIG α) (curr : Nat) (n d : aig.RefVec w) (wn wr : Nat) (q r : aig.RefVec w) (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < (go aig curr n d wn wr q r).aig.decls.size) : (go aig curr n d wn wr q r).aig.decls[idx] = aig.decls[idx]

def Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv {α : Type} [Hashable α] [DecidableEq α] {w : Nat} (aig : Sat.AIG α) (input : aig.BinaryRefVec w) : Sat.AIG.RefVecEntry α w

Equations

• One or more equations did not get rendered due to their size.

instance Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorBinaryRefVecBlastUdiv {α : Type} [Hashable α] [DecidableEq α] : Sat.AIG.LawfulVecOperator α Sat.AIG.BinaryRefVec fun {len : Nat} => blastUdiv