Documentation

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

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

source
structure Std.Tactic.BVDecide.BVExpr.bitblast.ExtractTarget {α : Type} [Hashable α] [DecidableEq α] (aig : Std.Sat.AIG α) (len : Nat) :
Type
  • w : Nat
  • vec : aig.RefVec self.w
  • start : Nat
Instances For
source
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.
source
@[irreducible]
def Std.Tactic.BVDecide.BVExpr.bitblast.blastExtract.go {α : Type} [Hashable α] [DecidableEq α] {newWidth : Nat} {aig : Std.Sat.AIG α} {w : Nat} (input : aig.RefVec w) (start : 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.
source
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 := ⋯ }