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 v

If we find a cached atom declaration in the AIG, denoting it yields the value of the atom.

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.denote_mkAtomCached {α : Type} [Hashable α] [DecidableEq α] {assign : α → Bool} {var : α} {aig : AIG α} : ⟦assign, aig.mkAtomCached var⟧ = assign var

Denoting mkAtomCached yields the value of the atom.

@[simp]

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

Denoting mkConstCached yields the constant.

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 := aig, ref := input.lhs }⟧ && ⟦assign, { aig := aig, ref := input.rhs }⟧)

If we find a cached gate declaration in the AIG, denoting it yields the conjunction of its inputs.

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.denote_gate_push {α : Type} [Hashable α] [DecidableEq α] {assign : α → Bool} {aig1 aig2 : AIG α} {input : aig1.BinaryInput} {hidx : aig1.decls.size < aig2.decls.size} (h : aig2.decls = aig1.decls.push (Decl.gate (Fanin.mk input.lhs.gate input.lhs.invert) (Fanin.mk input.rhs.gate input.rhs.invert))) : ⟦assign, { aig := aig2, ref := { gate := aig1.decls.size, invert := false, hgate := hidx } }⟧ = (⟦assign, { aig := aig1, ref := input.lhs }⟧ && ⟦assign, { aig := aig1, ref := input.rhs }⟧)

Denoting a gate that was just pushed onto an AIG yields the conjunction of its inputs.

theorem Std.Sat.AIG.mkGateCached.denote_go {α : Type} [Hashable α] [DecidableEq α] {assign : α → Bool} {aig : AIG α} {input : aig.BinaryInput} : ⟦assign, go aig input⟧ = (⟦assign, { aig := aig, ref := input.lhs }⟧ && ⟦assign, { aig := aig, ref := input.rhs }⟧)

@[simp]

theorem Std.Sat.AIG.denote_mkGateCached {α : Type} [Hashable α] [DecidableEq α] {assign : α → Bool} {aig : AIG α} {input : aig.BinaryInput} : ⟦assign, aig.mkGateCached input⟧ = (⟦assign, { aig := aig, ref := input.lhs }⟧ && ⟦assign, { aig := aig, ref := input.rhs }⟧)

Denoting mkGateCached yields the conjunction of its inputs.