This module contains the logic to turn a `BVLogicalExpr` into an `AIG` with maximum subterm sharing, through the use of a cache that re-uses sub-circuits if possible. Additionally a term level cache is used to prevent rerunning bitblasting on commong bitvector subexpressions.

source
def Std.Tactic.BVDecide.BVLogicalExpr.bitblast (expr : BVLogicalExpr) :
Sat.AIG.Entrypoint BVBit

Turn a `BoolExpr` into an `Entrypoint`.

Equations

- expr.bitblast = (Std.Tactic.BVDecide.BVLogicalExpr.bitblast.go Std.Sat.AIG.empty expr Std.Tactic.BVDecide.BVExpr.Cache.empty).result.val

Instances For

source
def Std.Tactic.BVDecide.BVLogicalExpr.bitblast.go (aig : Sat.AIG BVBit) (expr : BVLogicalExpr) (cache : BVExpr.Cache aig) :
Return aig
Equations

- One or more equations did not get rendered due to their size.
- Std.Tactic.BVDecide.BVLogicalExpr.bitblast.go aig (Std.Tactic.BVDecide.BoolExpr.literal var) cache = Std.Tactic.BVDecide.BVPred.bitblast aig { val := var, cache := cache }
- Std.Tactic.BVDecide.BVLogicalExpr.bitblast.go aig (Std.Tactic.BVDecide.BoolExpr.const val) cache = { result := ⟨{ aig := aig, ref := aig.mkConstCached val }, ⋯⟩, cache := cache }

Instances For

source
theorem Std.Tactic.BVDecide.BVLogicalExpr.bitblast.go_le_size (aig : Sat.AIG BVBit) (expr : BVLogicalExpr) (cache : BVExpr.Cache aig) :
aig.decls.size ≤ (go aig expr cache).result.val.aig.decls.size
source
theorem Std.Tactic.BVDecide.BVLogicalExpr.bitblast.go_lt_size_of_lt_aig_size {x : Nat} (aig : Sat.AIG BVBit) (expr : BVLogicalExpr) (cache : BVExpr.Cache aig) (h : x < aig.decls.size) :
x < (go aig expr cache).result.val.aig.decls.size
source
theorem Std.Tactic.BVDecide.BVLogicalExpr.bitblast.go_decl_eq {expr : BVLogicalExpr} (idx : Nat) (aig : Sat.AIG BVBit) (cache : BVExpr.Cache aig) (h : idx < aig.decls.size) (hbounds : idx < (go aig expr cache).result.val.aig.decls.size) :
(go aig expr cache).result.val.aig.decls[idx] = aig.decls[idx]
source
theorem Std.Tactic.BVDecide.BVLogicalExpr.bitblast.go_isPrefix_aig {expr : BVLogicalExpr} {aig : Sat.AIG BVBit} (cache : BVExpr.Cache aig) :
Sat.AIG.IsPrefix aig.decls (go aig expr cache).result.val.aig.decls
source
theorem Std.Tactic.BVDecide.BVLogicalExpr.bitblast.go_denote_mem_prefix {assign : BVBit → Bool} {expr : BVLogicalExpr} {start : Nat} {inv : Bool} (aig : Sat.AIG BVBit) (cache : BVExpr.Cache aig) (hstart : start < aig.decls.size) :
⟦assign, { aig := (go aig expr cache).result.val.aig, ref := { gate := start, invert := inv, hgate := ⋯ } }⟧ = ⟦assign, { aig := aig, ref := { gate := start, invert := inv, hgate := hstart } }⟧