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 : Sat.AIG α) (len : Nat) :
Type
Instances For
    source
    def Std.Tactic.BVDecide.BVExpr.bitblast.blastExtract {α : Type} [Hashable α] [DecidableEq α] {newWidth : Nat} (aig : Sat.AIG α) (target : ExtractTarget aig newWidth) :
    Sat.AIG.RefVecEntry α newWidth
    Equations
      Instances For
        source
        @[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
          Instances For
            source
            instance Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorExtractTargetBlastExtract {α : Type} [Hashable α] [DecidableEq α] :
            Sat.AIG.LawfulVecOperator α ExtractTarget fun {len : Nat} => blastExtract