This module contains the verification of the bitblaster for predicates over `BitVec` expressions (`BVPred`) from `Impl.Pred`.

source
theorem Std.Tactic.BVDecide.BVPred.bitblast_aig_IsPrefix (aig : Sat.AIG BVBit) (input : BVExpr.WithCache BVPred aig) :
Sat.AIG.IsPrefix aig.decls (bitblast aig input).result.val.aig.decls
source
theorem Std.Tactic.BVDecide.BVPred.bitblast_denote_mem_prefix {inv : Bool} (aig : Sat.AIG BVBit) (input : BVExpr.WithCache BVPred aig) (assign : BVExpr.Assignment) (start : Nat) (hstart : start < aig.decls.size) :
⟦assign.toAIGAssignment, { aig := (bitblast aig input).result.val.aig, ref := { gate := start, invert := inv, hgate := ⋯ } }⟧ = ⟦assign.toAIGAssignment, { aig := aig, ref := { gate := start, invert := inv, hgate := hstart } }⟧
source
theorem Std.Tactic.BVDecide.BVPred.bitblast_Inv_of_Inv {aig : Sat.AIG BVBit} {assign : BVExpr.Assignment} (input : BVExpr.WithCache BVPred aig) (hinv : BVExpr.Cache.Inv assign aig input.cache) :
BVExpr.Cache.Inv assign (bitblast aig input).result.val.aig (bitblast aig input).cache
source
theorem Std.Tactic.BVDecide.BVPred.denote_bitblast (aig : Sat.AIG BVBit) (input : BVExpr.WithCache BVPred aig) (assign : BVExpr.Assignment) (hinv : BVExpr.Cache.Inv assign aig input.cache) :
⟦assign.toAIGAssignment, { aig := (bitblast aig input).result.val.aig, ref := (bitblast aig input).result.val.ref }⟧ = eval assign input.val