This module contains the theory of the cached AIG node creation functions. It is mainly concerned with proving lemmas about the denotational semantics of the gate functions in different scenarios, in particular reductions to the semantics of the non cached versions.

theorem Std.Sat.AIG.denote_mkAtom_cached {α : Type} [Hashable α] [DecidableEq α] {v : α} {assign : α → Bool} {aig : AIG α} {hit : CacheHit aig.decls (Decl.atom v)} : aig.cache.get? (Decl.atom v) = some hit → ⟦assign, { aig := aig, ref := { gate := hit.idx, invert := false, hgate := ⋯ } }⟧ = ⟦assign, aig.mkAtom v⟧

If we find a cached atom declaration in the AIG, denoting it is equivalent to denoting AIG.mkAtom.

theorem Std.Sat.AIG.mkAtomCached_hit_aig {α : Type} [Hashable α] [DecidableEq α] {var : α} (aig : AIG α) {hit : CacheHit aig.decls (Decl.atom var)} (hcache : aig.cache.get? (Decl.atom var) = some hit) : (aig.mkAtomCached var).aig = aig

mkAtomCached does not modify the input AIG upon a cache hit.

theorem Std.Sat.AIG.mkAtomCached_miss_aig {α : Type} [Hashable α] [DecidableEq α] {var : α} (aig : AIG α) (hcache : aig.cache.get? (Decl.atom var) = none) : (aig.mkAtomCached var).aig.decls = aig.decls.push (Decl.atom var)

mkAtomCached pushes to the input AIG upon a cache miss.

theorem Std.Sat.AIG.mkAtomCached_decl_eq {α : Type} [Hashable α] [DecidableEq α] (aig : AIG α) (var : α) (idx : Nat) {h : idx < aig.decls.size} {hbound : idx < (aig.mkAtomCached var).aig.decls.size} : (aig.mkAtomCached var).aig.decls[idx] = aig.decls[idx]

The AIG produced by AIG.mkAtomCached agrees with the input AIG on all indices that are valid for both.

theorem Std.Sat.AIG.mkAtomCached_le_size {α : Type} [Hashable α] [DecidableEq α] (aig : AIG α) (var : α) : aig.decls.size ≤ (aig.mkAtomCached var).aig.decls.size

AIG.mkAtomCached never shrinks the underlying AIG.

instance Std.Sat.AIG.instLawfulOperatorMkAtomCached {α : Type} [Hashable α] [DecidableEq α] : LawfulOperator α (fun (x : AIG α) => α) mkAtomCached

@[simp]

theorem Std.Sat.AIG.mkAtomCached_eval_eq_mkAtom_eval {α : Type} [Hashable α] [DecidableEq α] {assign : α → Bool} {var : α} {aig : AIG α} : ⟦assign, aig.mkAtomCached var⟧ = ⟦assign, aig.mkAtom var⟧

The central equality theorem between mkAtomCached and mkAtom.

@[simp]

theorem Std.Sat.AIG.denote_mkConstCached {α : Type} [Hashable α] [DecidableEq α] {assign : α → Bool} {val : Bool} {aig : AIG α} : ⟦assign, { aig := aig, ref := aig.mkConstCached val }⟧ = val

The central equality theorem between mkConstCached and mkConst.

theorem Std.Sat.AIG.denote_mkGate_cached {α : Type} [Hashable α] [DecidableEq α] {assign : α → Bool} {aig : AIG α} {input : aig.BinaryInput} {hit : CacheHit aig.decls (Decl.gate (Fanin.mk input.lhs.gate input.lhs.invert) (Fanin.mk input.rhs.gate input.rhs.invert))} : aig.cache.get? (Decl.gate (Fanin.mk input.lhs.gate input.lhs.invert) (Fanin.mk input.rhs.gate input.rhs.invert)) = some hit → ⟦assign, { aig := aig, ref := { gate := hit.idx, invert := false, hgate := ⋯ } }⟧ = ⟦assign, aig.mkGate input⟧

If we find a cached gate declaration in the AIG, denoting it is equivalent to denoting AIG.mkGate.

theorem Std.Sat.AIG.mkGateCached.go_le_size {α : Type} [Hashable α] [DecidableEq α] (aig : AIG α) (input : aig.BinaryInput) : aig.decls.size ≤ (go aig input).aig.decls.size

theorem Std.Sat.AIG.mkGateCached_le_size {α : Type} [Hashable α] [DecidableEq α] (aig : AIG α) (input : aig.BinaryInput) : aig.decls.size ≤ (aig.mkGateCached input).aig.decls.size

AIG.mkGateCached never shrinks the underlying AIG.

theorem Std.Sat.AIG.mkGateCached.go_decl_eq {α : Type} [Hashable α] [DecidableEq α] (aig : AIG α) (input : aig.BinaryInput) (idx : Nat) (h1 : idx < (go aig input).aig.decls.size) (h2 : idx < aig.decls.size) : (go aig input).aig.decls[idx] = aig.decls[idx]

theorem Std.Sat.AIG.mkGateCached_decl_eq {α : Type} [Hashable α] [DecidableEq α] (aig : AIG α) (input : aig.BinaryInput) (idx : Nat) (h1 : idx < (aig.mkGateCached input).aig.decls.size) (h2 : idx < aig.decls.size) : (aig.mkGateCached input).aig.decls[idx] = aig.decls[idx]

The AIG produced by AIG.mkGateCached agrees with the input AIG on all indices that are valid for both.

instance Std.Sat.AIG.instLawfulOperatorBinaryInputMkGateCached {α : Type} [Hashable α] [DecidableEq α] : LawfulOperator α BinaryInput mkGateCached

theorem Std.Sat.AIG.mkGateCached.go_eval_eq_mkGate_eval {α : Type} [Hashable α] [DecidableEq α] {assign : α → Bool} {aig : AIG α} {input : aig.BinaryInput} : ⟦assign, go aig input⟧ = ⟦assign, aig.mkGate input⟧

@[simp]

theorem Std.Sat.AIG.mkGateCached_eval_eq_mkGate_eval {α : Type} [Hashable α] [DecidableEq α] {assign : α → Bool} {aig : AIG α} {input : aig.BinaryInput} : ⟦assign, aig.mkGateCached input⟧ = ⟦assign, aig.mkGate input⟧

The central equality theorem between mkGateCached and mkGate.