This module contains the implementation of a bitblaster for `BitVec.getLsbD`.

source
structure Std.Tactic.BVDecide.BVPred.GetLsbDTarget {α : Type} [Hashable α] [DecidableEq α] (aig : Sat.AIG α) :
Type

- w : Nat
- vec : aig.RefVec self.w
- idx : Nat

Instances For

source
def Std.Tactic.BVDecide.BVPred.blastGetLsbD {α : Type} [Hashable α] [DecidableEq α] (aig : Sat.AIG α) (target : GetLsbDTarget aig) :
aig.Ref
Equations

- Std.Tactic.BVDecide.BVPred.blastGetLsbD aig target = if h : target.idx < target.w then target.vec.get target.idx h else aig.mkConstCached false

Instances For