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.
    Instances For
      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.
      Instances For
        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 := ⋯ }