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 : Std.Tactic.BVDecide.BoolExpr α)
(atomHandler : Std.Sat.AIG β → α → Std.Sat.AIG.Entrypoint β)
[Std.Sat.AIG.LawfulOperator β (fun (x : Std.Sat.AIG β) => α) atomHandler]
:
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
Instances For
@[specialize #[]]
def
Std.Tactic.BVDecide.ofBoolExprCached.go
{β : Type}
[Hashable β]
[DecidableEq β]
{α : Type}
(aig : Std.Sat.AIG β)
(expr : Std.Tactic.BVDecide.BoolExpr α)
(atomHandler : Std.Sat.AIG β → α → Std.Sat.AIG.Entrypoint β)
[Std.Sat.AIG.LawfulOperator β (fun (x : Std.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, ⋯⟩
Instances For
theorem
Std.Tactic.BVDecide.ofBoolExprCached.go_le_size
{α : Type}
{β : Type}
[Hashable β]
[DecidableEq β]
(atomHandler : Std.Sat.AIG β → α → Std.Sat.AIG.Entrypoint β)
[Std.Sat.AIG.LawfulOperator β (fun (x : Std.Sat.AIG β) => α) atomHandler]
(expr : Std.Tactic.BVDecide.BoolExpr α)
(aig : Std.Sat.AIG β)
:
aig.decls.size ≤ (Std.Tactic.BVDecide.ofBoolExprCached.go aig expr atomHandler).val.aig.decls.size
theorem
Std.Tactic.BVDecide.ofBoolExprCached.go_decl_eq
{α : Type}
{β : Type}
[Hashable β]
[DecidableEq β]
(atomHandler : Std.Sat.AIG β → α → Std.Sat.AIG.Entrypoint β)
[Std.Sat.AIG.LawfulOperator β (fun (x : Std.Sat.AIG β) => α) atomHandler]
{expr : Std.Tactic.BVDecide.BoolExpr α}
(idx : Nat)
(aig : Std.Sat.AIG β)
(h : idx < aig.decls.size)
(hbounds : idx < (Std.Tactic.BVDecide.ofBoolExprCached.go aig expr atomHandler).val.aig.decls.size)
:
(Std.Tactic.BVDecide.ofBoolExprCached.go aig expr atomHandler).val.aig.decls[idx] = aig.decls[idx]
theorem
Std.Tactic.BVDecide.ofBoolExprCached.go_isPrefix_aig
{α : Type}
{β : Type}
[Hashable β]
[DecidableEq β]
(atomHandler : Std.Sat.AIG β → α → Std.Sat.AIG.Entrypoint β)
[Std.Sat.AIG.LawfulOperator β (fun (x : Std.Sat.AIG β) => α) atomHandler]
{expr : Std.Tactic.BVDecide.BoolExpr α}
{aig : Std.Sat.AIG β}
:
Std.Sat.AIG.IsPrefix aig.decls (Std.Tactic.BVDecide.ofBoolExprCached.go aig expr atomHandler).val.aig.decls
theorem
Std.Tactic.BVDecide.ofBoolExprCached.go_denote_mem_prefix
{α : Type}
{β : Type}
[Hashable β]
[DecidableEq β]
(atomHandler : Std.Sat.AIG β → α → Std.Sat.AIG.Entrypoint β)
[Std.Sat.AIG.LawfulOperator β (fun (x : Std.Sat.AIG β) => α) atomHandler]
{assign : β → Bool}
{aig : Std.Sat.AIG β}
{expr : Std.Tactic.BVDecide.BoolExpr α}
{start : Nat}
{hstart : start < aig.decls.size}
:
⟦assign,
{ aig := (Std.Tactic.BVDecide.ofBoolExprCached.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}
{β : Type}
[Hashable β]
[DecidableEq β]
(atomHandler : Std.Sat.AIG β → α → Std.Sat.AIG.Entrypoint β)
[Std.Sat.AIG.LawfulOperator β (fun (x : Std.Sat.AIG β) => α) atomHandler]
{assign : β → Bool}
{expr : Std.Tactic.BVDecide.BoolExpr α}
(entry : Std.Sat.AIG.Entrypoint β)
{h : entry.ref.gate < (Std.Tactic.BVDecide.ofBoolExprCached.go entry.aig expr atomHandler).val.aig.decls.size}
:
⟦assign,
{ aig := (Std.Tactic.BVDecide.ofBoolExprCached.go entry.aig expr atomHandler).val.aig,
ref := { gate := entry.ref.gate, hgate := h } }⟧ = ⟦assign, entry⟧