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 : Std.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 : Std.Sat.AIG α) (input : Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.ShiftConcatInput aig w) : Std.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 α] : Std.Sat.AIG.LawfulVecOperator α Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.ShiftConcatInput fun {len : Nat} => Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastShiftConcat

Equations

• ⋯ = ⋯

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

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

theorem Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.BlastDivSubtractShiftOutput.hle {α : Type} [Hashable α] [DecidableEq α] {old : Std.Sat.AIG α} {w : Nat} (self : Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.BlastDivSubtractShiftOutput old w) : old.decls.size ≤ self.aig.decls.size

def Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastDivSubtractShift {α : Type} [Hashable α] [DecidableEq α] {w : Nat} (aig : Std.Sat.AIG α) (falseRef : aig.Ref) (trueRef : aig.Ref) (n : aig.RefVec w) (d : aig.RefVec w) (wn : Nat) (wr : Nat) (q : aig.RefVec w) (r : aig.RefVec w) : Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.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 : Std.Sat.AIG α) (falseRef : aig.Ref) (trueRef : aig.Ref) (n : aig.RefVec w) (d : aig.RefVec w) (wn : Nat) (wr : Nat) (q : aig.RefVec w) (r : aig.RefVec w) : aig.decls.size ≤ (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastDivSubtractShift aig falseRef trueRef 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 : Std.Sat.AIG α) (falseRef : aig.Ref) (trueRef : aig.Ref) (n : aig.RefVec w) (d : aig.RefVec w) (wn : Nat) (wr : Nat) (q : aig.RefVec w) (r : aig.RefVec w) (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastDivSubtractShift aig falseRef trueRef n d wn wr q r).aig.decls.size) : (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastDivSubtractShift aig falseRef trueRef n d wn wr q r).aig.decls[idx] = aig.decls[idx]

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

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

theorem Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.BlastUdivOutput.hle {α : Type} [Hashable α] [DecidableEq α] {old : Std.Sat.AIG α} {w : Nat} (self : Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.BlastUdivOutput old w) : old.decls.size ≤ self.aig.decls.size

def Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.go {α : Type} [Hashable α] [DecidableEq α] {w : Nat} (aig : Std.Sat.AIG α) (curr : Nat) (falseRef : aig.Ref) (trueRef : aig.Ref) (n : aig.RefVec w) (d : aig.RefVec w) (wn : Nat) (wr : Nat) (q : aig.RefVec w) (r : aig.RefVec w) : Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.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 falseRef trueRef n d wn wr q r = { aig := aig, q := q, r := r, hle := ⋯ }

@[irreducible]

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

@[irreducible]

theorem Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.go_decl_eq {α : Type} [Hashable α] [DecidableEq α] {w : Nat} (aig : Std.Sat.AIG α) (curr : Nat) (falseRef : aig.Ref) (trueRef : aig.Ref) (n : aig.RefVec w) (d : aig.RefVec w) (wn : Nat) (wr : Nat) (q : aig.RefVec w) (r : aig.RefVec w) (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.go aig curr falseRef trueRef n d wn wr q r).aig.decls.size) : (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.go aig curr falseRef trueRef 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 : Std.Sat.AIG α) (input : aig.BinaryRefVec w) : Std.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 α] : Std.Sat.AIG.LawfulVecOperator α Std.Sat.AIG.BinaryRefVec fun {len : Nat} => Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv

Equations

• ⋯ = ⋯