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

- w : Nat
- n : Nat
- inner : aig.RefVec self.w
- h : combined = self.w * self.n

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

- 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 : 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 α] :
Sat.AIG.LawfulVecOperator α ReplicateTarget fun {len : Nat} => blastReplicate