HepLean 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 : Std.Sat.AIG α) (combined : Nat) :
Type
  • w : Nat
  • n : Nat
  • inner : aig.RefVec self.w
  • h : combined = self.w * self.n
Instances For
    source
    theorem Std.Tactic.BVDecide.BVExpr.bitblast.ReplicateTarget.h {α : Type} [Hashable α] [DecidableEq α] {aig : Std.Sat.AIG α} {combined : Nat} (self : Std.Tactic.BVDecide.BVExpr.bitblast.ReplicateTarget aig combined) :
    combined = self.w * self.n
    source
    def Std.Tactic.BVDecide.BVExpr.bitblast.blastReplicate {α : Type} [Hashable α] [DecidableEq α] {newWidth : Nat} (aig : Std.Sat.AIG α) (target : Std.Tactic.BVDecide.BVExpr.bitblast.ReplicateTarget 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.blastReplicate.go {α : Type} [Hashable α] [DecidableEq α] {aig : Std.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
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        instance Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorReplicateTargetBlastReplicate {α : Type} [Hashable α] [DecidableEq α] :
        Std.Sat.AIG.LawfulVecOperator α Std.Tactic.BVDecide.BVExpr.bitblast.ReplicateTarget fun {len : Nat} => Std.Tactic.BVDecide.BVExpr.bitblast.blastReplicate
        Equations
        • Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorReplicateTargetBlastReplicate = { le_size := ⋯, decl_eq := ⋯ }