This module contains the implementation of a bitblaster for BitVec.clz.

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

Equations

• Std.Tactic.BVDecide.BVExpr.bitblast.blastClz aig x = Std.Tactic.BVDecide.BVExpr.bitblast.blastClz.go aig x 0 (Std.Tactic.BVDecide.BVExpr.bitblast.blastConst aig ↑w)

@[irreducible]

def Std.Tactic.BVDecide.BVExpr.bitblast.blastClz.go {α : Type} [Hashable α] [DecidableEq α] {w : Nat} (aig : Sat.AIG α) (x : aig.RefVec w) (curr : Nat) (acc : aig.RefVec w) : Sat.AIG.RefVecEntry α w

Equations

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

theorem Std.Tactic.BVDecide.BVExpr.bitblast.blastClz.go_le_size {α : Type} [Hashable α] [DecidableEq α] {w : Nat} (aig : Sat.AIG α) (curr : Nat) (acc xc : aig.RefVec w) : aig.decls.size ≤ (go aig xc curr acc).aig.decls.size

theorem Std.Tactic.BVDecide.BVExpr.bitblast.blastClz.go_decl_eq {α : Type} [Hashable α] [DecidableEq α] {w : Nat} (aig : Sat.AIG α) (curr : Nat) (acc xc : aig.RefVec w) (idx : Nat) (h1 : idx < (go aig xc curr acc).aig.decls.size) (h2 : idx < aig.decls.size) : (go aig xc curr acc).aig.decls[idx] = aig.decls[idx]

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