This module contains the implementation of a bitblaster for BitVec.getLsbD
.
structure
Std.Tactic.BVDecide.BVPred.GetLsbDTarget
{α : Type}
[Hashable α]
[DecidableEq α]
(aig : Sat.AIG α)
:
def
Std.Tactic.BVDecide.BVPred.blastGetLsbD
{α : Type}
[Hashable α]
[DecidableEq α]
(aig : Sat.AIG α)
(target : GetLsbDTarget aig)
: