This module contains the logic to turn a BoolExpr Nat into an AIG with maximum subterm sharing, through the use of a cache that re-uses sub-circuits if possible.

@[specialize #[]]

def Std.Tactic.BVDecide.ofBoolExprCached {β : Type} [Hashable β] [DecidableEq β] {α : Type} (expr : BoolExpr α) (atomHandler : Sat.AIG β → α → Sat.AIG.Entrypoint β) [Sat.AIG.LawfulOperator β (fun (x : Sat.AIG β) => α) atomHandler] : Sat.AIG.Entrypoint β

Turn a BoolExpr into an Entrypoint.

Equations

• Std.Tactic.BVDecide.ofBoolExprCached expr atomHandler = (Std.Tactic.BVDecide.ofBoolExprCached.go Std.Sat.AIG.empty expr atomHandler).val

@[specialize #[]]

def Std.Tactic.BVDecide.ofBoolExprCached.go {β : Type} [Hashable β] [DecidableEq β] {α : Type} (aig : Sat.AIG β) (expr : BoolExpr α) (atomHandler : Sat.AIG β → α → Sat.AIG.Entrypoint β) [Sat.AIG.LawfulOperator β (fun (x : Sat.AIG β) => α) atomHandler] : aig.ExtendingEntrypoint

Equations

• One or more equations did not get rendered due to their size.
• Std.Tactic.BVDecide.ofBoolExprCached.go aig (Std.Tactic.BVDecide.BoolExpr.literal var) atomHandler = ⟨atomHandler aig var, ⋯⟩
• Std.Tactic.BVDecide.ofBoolExprCached.go aig (Std.Tactic.BVDecide.BoolExpr.const val) atomHandler = ⟨aig.mkConstCached val, ⋯⟩

theorem Std.Tactic.BVDecide.ofBoolExprCached.go_le_size {α β : Type} [Hashable β] [DecidableEq β] (atomHandler : Sat.AIG β → α → Sat.AIG.Entrypoint β) [Sat.AIG.LawfulOperator β (fun (x : Sat.AIG β) => α) atomHandler] (expr : BoolExpr α) (aig : Sat.AIG β) : aig.decls.size ≤ (go aig expr atomHandler).val.aig.decls.size

theorem Std.Tactic.BVDecide.ofBoolExprCached.go_decl_eq {α β : Type} [Hashable β] [DecidableEq β] (atomHandler : Sat.AIG β → α → Sat.AIG.Entrypoint β) [Sat.AIG.LawfulOperator β (fun (x : Sat.AIG β) => α) atomHandler] {expr : BoolExpr α} (idx : Nat) (aig : Sat.AIG β) (h : idx < aig.decls.size) (hbounds : idx < (go aig expr atomHandler).val.aig.decls.size) : (go aig expr atomHandler).val.aig.decls[idx] = aig.decls[idx]

theorem Std.Tactic.BVDecide.ofBoolExprCached.go_isPrefix_aig {α β : Type} [Hashable β] [DecidableEq β] (atomHandler : Sat.AIG β → α → Sat.AIG.Entrypoint β) [Sat.AIG.LawfulOperator β (fun (x : Sat.AIG β) => α) atomHandler] {expr : BoolExpr α} {aig : Sat.AIG β} : Sat.AIG.IsPrefix aig.decls (go aig expr atomHandler).val.aig.decls

theorem Std.Tactic.BVDecide.ofBoolExprCached.go_denote_mem_prefix {α β : Type} [Hashable β] [DecidableEq β] (atomHandler : Sat.AIG β → α → Sat.AIG.Entrypoint β) [Sat.AIG.LawfulOperator β (fun (x : Sat.AIG β) => α) atomHandler] {assign : β → Bool} {aig : Sat.AIG β} {expr : BoolExpr α} {start : Nat} {hstart : start < aig.decls.size} : ⟦assign, { aig := (go aig expr atomHandler).val.aig, ref := { gate := start, hgate := ⋯ } }⟧ = ⟦assign, { aig := aig, ref := { gate := start, hgate := hstart } }⟧

@[simp]

theorem Std.Tactic.BVDecide.ofBoolExprCached.go_denote_entry {α β : Type} [Hashable β] [DecidableEq β] (atomHandler : Sat.AIG β → α → Sat.AIG.Entrypoint β) [Sat.AIG.LawfulOperator β (fun (x : Sat.AIG β) => α) atomHandler] {assign : β → Bool} {expr : BoolExpr α} (entry : Sat.AIG.Entrypoint β) {h : entry.ref.gate < (go entry.aig expr atomHandler).val.aig.decls.size} : ⟦assign, { aig := (go entry.aig expr atomHandler).val.aig, ref := { gate := entry.ref.gate, hgate := h } }⟧ = ⟦assign, entry⟧