Documentation

Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Udiv

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

  • lhs : aig.RefVec len
  • bit : aig.Ref
Equations
  • One or more equations did not get rendered due to their size.
theorem 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
  • 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
def Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastDivSubtractShift {α : Type} [Hashable α] [DecidableEq α] {w : Nat} (aig : Std.Sat.AIG α) (falseRef trueRef : aig.Ref) (n d : aig.RefVec w) (wn wr : Nat) (q r : aig.RefVec 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 trueRef : aig.Ref) (n d : aig.RefVec w) (wn wr : Nat) (q 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 trueRef : aig.Ref) (n d : aig.RefVec w) (wn wr : Nat) (q 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]
  • aig : Std.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 : Std.Sat.AIG α) (curr : Nat) (falseRef trueRef : aig.Ref) (n d : aig.RefVec w) (wn wr : Nat) (q r : aig.RefVec w) :
Equations
@[irreducible]
theorem Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.go_le_size {α : Type} [Hashable α] [DecidableEq α] {w : Nat} (aig : Std.Sat.AIG α) (curr : Nat) (falseRef trueRef : aig.Ref) (n d : aig.RefVec w) (wn wr : Nat) (q 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 trueRef : aig.Ref) (n d : aig.RefVec w) (wn wr : Nat) (q 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) :
theorem 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