Documentation

Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.GetLsbD

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

source
structure Std.Tactic.BVDecide.BVPred.GetLsbDTarget {α : Type} [Hashable α] [DecidableEq α] (aig : Std.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 : Std.Sat.AIG α) (target : Std.Tactic.BVDecide.BVPred.GetLsbDTarget aig) :
    Std.Sat.AIG.Entrypoint α
    Instances For
      source
      theorem Std.Tactic.BVDecide.BVPred.instLawfulOperatorGetLsbDTargetBlastGetLsbD {α : Type} [Hashable α] [DecidableEq α] :
      Std.Sat.AIG.LawfulOperator α Std.Tactic.BVDecide.BVPred.GetLsbDTarget Std.Tactic.BVDecide.BVPred.blastGetLsbD