This module contains the verification of the `BitVec` expressions (`BVExpr`) bitblaster from `Impl.Expr`.

source
@[reducible, inline]
abbrev Std.Tactic.BVDecide.BVExpr.Cache.Inv (assign : Assignment) (aig : Sat.AIG BVBit) (cache : Cache aig) :
Prop
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
theorem Std.Tactic.BVDecide.BVExpr.Cache.Inv_empty {assign : Assignment} (aig : Sat.AIG BVBit) :
Inv assign aig empty
source
theorem Std.Tactic.BVDecide.BVExpr.Cache.Inv_cast {aig1 : Sat.AIG BVBit} {assign : Assignment} {aig2 : Sat.AIG BVBit} (cache : Cache aig1) (hpref : Sat.AIG.IsPrefix aig1.decls aig2.decls) (hinv : Inv assign aig1 cache) :
Inv assign aig2 (cache.cast ⋯)
source
theorem Std.Tactic.BVDecide.BVExpr.Cache.Inv_insert {aig : Sat.AIG BVBit} {w : Nat} {assign : Assignment} (cache : Cache aig) (expr : BVExpr w) (refs : aig.RefVec w) (hinv : Inv assign aig cache) (hrefs : ∀ (idx : Nat) (hidx : idx < w), ⟦assign.toAIGAssignment, { aig := aig, ref := refs.get idx hidx }⟧ = (eval assign expr).getLsbD idx) :
Inv assign aig (cache.insert expr refs)
source
theorem Std.Tactic.BVDecide.BVExpr.Cache.get?_eq_some_iff {aig : Sat.AIG BVBit} {w : Nat} {refs : aig.RefVec w} (cache : Cache aig) (expr : BVExpr w) :
cache.get? expr = some refs ↔ cache.map.get? { w := w, expr := expr } = some refs.refs
source
theorem Std.Tactic.BVDecide.BVExpr.Cache.denote_eq_eval_of_get?_eq_some_of_Inv {aig : Sat.AIG BVBit} {w : Nat} {assign : Assignment} (cache : Cache aig) (expr : BVExpr w) (refs : aig.RefVec w) (hsome : cache.get? expr = some refs) (hinv : Inv assign aig cache) (i : Nat) (h : i < w) :
⟦assign.toAIGAssignment, { aig := aig, ref := refs.get i h }⟧ = (eval assign expr).getLsbD i
source
theorem Std.Tactic.BVDecide.BVExpr.bitblast.goCache_val_eq_bitblast {w : Nat} (aig : Sat.AIG BVBit) (expr : BVExpr w) (cache : Cache aig) :
goCache aig expr cache = bitblast aig { val := expr, cache := cache }
source
theorem Std.Tactic.BVDecide.BVExpr.bitblast.go_denote_mem_prefix {w : Nat} {inv : Bool} (aig : Sat.AIG BVBit) (expr : BVExpr w) (assign : Assignment) (cache : Cache aig) (start : Nat) (hstart : start < aig.decls.size) :
⟦assign.toAIGAssignment, { aig := (go aig expr cache).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.BVExpr.bitblast.goCache_denote_mem_prefix {w : Nat} {inv : Bool} (aig : Sat.AIG BVBit) (expr : BVExpr w) (assign : Assignment) (cache : Cache aig) (start : Nat) (hstart : start < aig.decls.size) :
⟦assign.toAIGAssignment, { aig := (goCache aig expr cache).result.val.aig, ref := { gate := start, invert := inv, hgate := ⋯ } }⟧ = ⟦assign.toAIGAssignment, { aig := aig, ref := { gate := start, invert := inv, hgate := hstart } }⟧
source
@[irreducible]
theorem Std.Tactic.BVDecide.BVExpr.bitblast.goCache_Inv_of_Inv {aig : Sat.AIG BVBit} {assign : Assignment} {w : Nat} (cache : Cache aig) (hinv : Cache.Inv assign aig cache) (expr : BVExpr w) :
Cache.Inv assign (goCache aig expr cache).result.val.aig (goCache aig expr cache).cache
source
@[irreducible]
theorem Std.Tactic.BVDecide.BVExpr.bitblast.go_Inv_of_Inv {aig : Sat.AIG BVBit} {assign : Assignment} {w : Nat} (cache : Cache aig) (hinv : Cache.Inv assign aig cache) (expr : BVExpr w) :
Cache.Inv assign (go aig expr cache).result.val.aig (go aig expr cache).cache
source
@[irreducible]
theorem Std.Tactic.BVDecide.BVExpr.bitblast.goCache_denote_eq {w : Nat} (aig : Sat.AIG BVBit) (expr : BVExpr w) (assign : Assignment) (cache : Cache aig) (hinv : Cache.Inv assign aig cache) (idx : Nat) (hidx : idx < w) :
⟦assign.toAIGAssignment, { aig := (goCache aig expr cache).result.val.aig, ref := (goCache aig expr cache).result.val.vec.get idx hidx }⟧ = (eval assign expr).getLsbD idx
source
@[irreducible]
theorem Std.Tactic.BVDecide.BVExpr.bitblast.go_denote_eq {w : Nat} (aig : Sat.AIG BVBit) (expr : BVExpr w) (assign : Assignment) (cache : Cache aig) (hinv : Cache.Inv assign aig cache) (idx : Nat) (hidx : idx < w) :
⟦assign.toAIGAssignment, { aig := (go aig expr cache).result.val.aig, ref := (go aig expr cache).result.val.vec.get idx hidx }⟧ = (eval assign expr).getLsbD idx
source
theorem Std.Tactic.BVDecide.BVExpr.bitblast_aig_IsPrefix {w : Nat} (aig : Sat.AIG BVBit) (input : WithCache (BVExpr w) aig) :
Sat.AIG.IsPrefix aig.decls (bitblast aig input).result.val.aig.decls
source
theorem Std.Tactic.BVDecide.BVExpr.bitblast_denote_mem_prefix {w : Nat} {inv : Bool} (aig : Sat.AIG BVBit) (input : WithCache (BVExpr w) aig) (assign : 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.BVExpr.bitblast_Inv_of_Inv {w : Nat} {aig : Sat.AIG BVBit} {assign : Assignment} (input : WithCache (BVExpr w) aig) (hinv : Cache.Inv assign aig input.cache) :
Cache.Inv assign (bitblast aig input).result.val.aig (bitblast aig input).cache
source
theorem Std.Tactic.BVDecide.BVExpr.denote_bitblast {w : Nat} (aig : Sat.AIG BVBit) (input : WithCache (BVExpr w) aig) (assign : Assignment) (hinv : Cache.Inv assign aig input.cache) (idx : Nat) (hidx : idx < w) :
⟦assign.toAIGAssignment, { aig := (bitblast aig input).result.val.aig, ref := (bitblast aig input).result.val.vec.get idx hidx }⟧ = (eval assign input.val).getLsbD idx