This module contains the verification of the bitblaster for BitVec.replicate from Impl.Operations.Replicate.

@[irreducible]

theorem Std.Tactic.BVDecide.BVExpr.bitblast.blastReplicate.go_get_aux {α : Type} [Hashable α] [DecidableEq α] {w : Nat} (aig : Sat.AIG α) (n curr : Nat) (hcurr : curr ≤ n) (input : aig.RefVec w) (s : aig.RefVec (w * curr)) (idx : Nat) (hidx : idx < w * curr) : (go n input curr hcurr s).get idx ⋯ = s.get idx hidx

@[irreducible]

theorem Std.Tactic.BVDecide.BVExpr.bitblast.blastReplicate.go_get {α : Type} [Hashable α] [DecidableEq α] {w : Nat} (aig : Sat.AIG α) (n curr : Nat) (hcurr : curr ≤ n) (input : aig.RefVec w) (s : aig.RefVec (w * curr)) (idx : Nat) (hidx1 : idx < w * n) : w * curr ≤ idx → (go n input curr hcurr s).get idx hidx1 = input.get (idx % w) ⋯

@[simp]

theorem Std.Tactic.BVDecide.BVExpr.bitblast.denote_blastReplicate {α : Type} [Hashable α] [DecidableEq α] {newWidth : Nat} (aig : Sat.AIG α) (target : ReplicateTarget aig newWidth) (assign : α → Bool) (idx : Nat) (hidx : idx < newWidth) : ⟦assign, { aig := (blastReplicate aig target).aig, ref := (blastReplicate aig target).vec.get idx hidx }⟧ = ⟦assign, { aig := aig, ref := target.inner.get (idx % target.w) ⋯ }⟧