Documentation

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

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

source
structure Std.Tactic.BVDecide.BVExpr.bitblast.ReplicateTarget {α : Type} [Hashable α] [DecidableEq α] (aig : Sat.AIG α) (combined : Nat) :
Type
Instances For
    source
    def Std.Tactic.BVDecide.BVExpr.bitblast.blastReplicate {α : Type} [Hashable α] [DecidableEq α] {newWidth : Nat} (aig : Sat.AIG α) (target : ReplicateTarget aig newWidth) :
    Sat.AIG.RefVecEntry α newWidth
    Equations
      Instances For
        source
        @[irreducible]
        def Std.Tactic.BVDecide.BVExpr.bitblast.blastReplicate.go {α : Type} [Hashable α] [DecidableEq α] {aig : Sat.AIG α} {w : Nat} (n : Nat) (input : aig.RefVec w) (curr : Nat) (hcurr : curr ≤ n) (s : aig.RefVec (w * curr)) :
        aig.RefVec (w * n)
        Equations
          Instances For
            source
            instance Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorReplicateTargetBlastReplicate {α : Type} [Hashable α] [DecidableEq α] :
            Sat.AIG.LawfulVecOperator α ReplicateTarget fun {len : Nat} => blastReplicate