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

structure Std.Tactic.BVDecide.BVExpr.bitblast.ExtractTarget {α : Type} [Hashable α] [DecidableEq α] (aig : Sat.AIG α) (len : Nat) : Type

• w : Nat
• vec : aig.RefVec self.w
• start : Nat

def Std.Tactic.BVDecide.BVExpr.bitblast.blastExtract {α : Type} [Hashable α] [DecidableEq α] {newWidth : Nat} (aig : Sat.AIG α) (target : ExtractTarget aig newWidth) : Sat.AIG.RefVecEntry α newWidth

Equations

• One or more equations did not get rendered due to their size.

@[irreducible]

def Std.Tactic.BVDecide.BVExpr.bitblast.blastExtract.go {α : Type} [Hashable α] [DecidableEq α] {newWidth : Nat} {aig : Sat.AIG α} {w : Nat} (input : aig.RefVec w) (start curr : Nat) (hcurr : curr ≤ newWidth) (s : aig.RefVec curr) : aig.RefVec newWidth

Equations

• One or more equations did not get rendered due to their size.

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