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

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

• Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorReplicateTargetBlastReplicate

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.

@[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.

instance Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorReplicateTargetBlastReplicate {α : Type} [Hashable α] [DecidableEq α] : Sat.AIG.LawfulVecOperator α ReplicateTarget fun {len : Nat} => blastReplicate