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

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

Equations

• Std.Tactic.BVDecide.BVExpr.bitblast.blastNot aig s = Std.Sat.AIG.RefVec.map aig { vec := s, func := Std.Sat.AIG.mkNotCached, lawful := ⋯, chainable := ⋯ }

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