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 common bitvector subexpressions.

def Std.Tactic.BVDecide.BVLogicalExpr.bitblastWithCache (expr : BVLogicalExpr) (aig : Sat.AIG BVBit) (cache : BVExpr.Cache aig) : Return aig

Equations

• expr.bitblastWithCache aig cache = Std.Tactic.BVDecide.BVLogicalExpr.bitblastWithCache.go aig expr cache

def Std.Tactic.BVDecide.BVLogicalExpr.bitblastWithCache.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.bitblastWithCache.go aig (Std.Tactic.BVDecide.BoolExpr.literal var) cache = Std.Tactic.BVDecide.BVPred.bitblast aig { val := var, cache := cache }
• Std.Tactic.BVDecide.BVLogicalExpr.bitblastWithCache.go aig (Std.Tactic.BVDecide.BoolExpr.const val) cache = { result := ⟨{ aig := aig, ref := aig.mkConstCached val }, ⋯⟩, cache := cache }

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

Turn a BoolExpr into an Entrypoint.

Equations

• expr.bitblast = (expr.bitblastWithCache Std.Sat.AIG.empty Std.Tactic.BVDecide.BVExpr.Cache.empty).result.val

theorem Std.Tactic.BVDecide.BVLogicalExpr.bitblastWithCache.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

theorem Std.Tactic.BVDecide.BVLogicalExpr.bitblastWithCache.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

theorem Std.Tactic.BVDecide.BVLogicalExpr.bitblastWithCache.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]

theorem Std.Tactic.BVDecide.BVLogicalExpr.bitblastWithCache.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

theorem Std.Tactic.BVDecide.BVLogicalExpr.bitblastWithCache.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 } }⟧

theorem Std.Tactic.BVDecide.BVLogicalExpr.bitblastWithCache_isPrefix_aig {expr : BVLogicalExpr} {aig : Sat.AIG BVBit} {cache : BVExpr.Cache aig} : Sat.AIG.IsPrefix aig.decls (expr.bitblastWithCache aig cache).result.val.aig.decls