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

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

Equations

• Std.Tactic.BVDecide.BVExpr.bitblast.blastNot aig s = Std.Sat.AIG.RefVec.map aig (Std.Sat.AIG.RefVec.MapTarget.mk s Std.Sat.AIG.mkNotCached)

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