Documentation

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

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

  • w : Nat
  • vec : aig.RefVec self.w
  • start : Nat
Instances For
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[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
        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 := }