This module contains the verification of the BitVec.getLsb
bitblaster from Impl.Operations.Extract
.
theorem
Std.Tactic.BVDecide.BVPred.denote_getD_eq_getLsbD
{α : Type}
[Hashable α]
[DecidableEq α]
{w : Nat}
(aig : Std.Sat.AIG α)
(assign : α → Bool)
(x : BitVec w)
(xv : aig.RefVec w)
(falseRef : aig.Ref)
(hx : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := xv.get idx hidx }⟧ = x.getLsbD idx)
(hfalse : ⟦assign, { aig := aig, ref := falseRef }⟧ = false)
(idx : Nat)
:
⟦assign, { aig := aig, ref := xv.getD idx falseRef }⟧ = x.getLsbD idx
@[simp]
theorem
Std.Tactic.BVDecide.BVPred.denote_blastGetLsbD
{α : Type}
[Hashable α]
[DecidableEq α]
(aig : Std.Sat.AIG α)
(target : Std.Tactic.BVDecide.BVPred.GetLsbDTarget aig)
(assign : α → Bool)
:
⟦assign, Std.Tactic.BVDecide.BVPred.blastGetLsbD aig target⟧ = if h : target.idx < target.w then ⟦assign, { aig := aig, ref := target.vec.get target.idx h }⟧ else false