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

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

• w : Nat
• vec : aig.RefVec self.w
• hi : Nat
• lo : Nat
• hnew : newWidth = self.hi - self.lo + 1

theorem Std.Tactic.BVDecide.BVExpr.bitblast.ExtractTarget.hnew {α : Type} [Hashable α] [DecidableEq α] {aig : Std.Sat.AIG α} {newWidth : Nat} (self : Std.Tactic.BVDecide.BVExpr.bitblast.ExtractTarget aig newWidth) : newWidth = self.hi - self.lo + 1

def Std.Tactic.BVDecide.BVExpr.bitblast.blastExtract {α : Type} [Hashable α] [DecidableEq α] {newWidth : Nat} (aig : Std.Sat.AIG α) (target : Std.Tactic.BVDecide.BVExpr.bitblast.ExtractTarget aig newWidth) : Std.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 : Std.Sat.AIG α} {w : Nat} (input : aig.RefVec w) (lo : Nat) (falseRef : aig.Ref) (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 α] : Std.Sat.AIG.LawfulVecOperator α Std.Tactic.BVDecide.BVExpr.bitblast.ExtractTarget fun {len : Nat} => Std.Tactic.BVDecide.BVExpr.bitblast.blastExtract

Equations

• Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorExtractTargetBlastExtract = { le_size := ⋯, decl_eq := ⋯ }