Documentation

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

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

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

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

Instances For

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

Std.Sat.AIG.Entrypoint α

Equations

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

Instances For

instance Std.Tactic.BVDecide.BVPred.instLawfulOperatorGetLsbDTargetBlastGetLsbD {α : Type} [Hashable α] [DecidableEq α] :

Std.Sat.AIG.LawfulOperator α Std.Tactic.BVDecide.BVPred.GetLsbDTarget Std.Tactic.BVDecide.BVPred.blastGetLsbD

Equations

⋯ = ⋯