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 : Std.Sat.AIG α} {hit : Std.Sat.AIG.CacheHit aig.decls (Std.Sat.AIG.Decl.atom v)} : aig.cache.get? (Std.Sat.AIG.Decl.atom v) = some hit → ⟦assign, { aig := aig, ref := { gate := hit.idx, 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 : Std.Sat.AIG α) {hit : Std.Sat.AIG.CacheHit aig.decls (Std.Sat.AIG.Decl.atom var)} (hcache : aig.cache.get? (Std.Sat.AIG.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 : Std.Sat.AIG α) (hcache : aig.cache.get? (Std.Sat.AIG.Decl.atom var) = none) : (aig.mkAtomCached var).aig.decls = aig.decls.push (Std.Sat.AIG.Decl.atom var)

mkAtomCached pushes to the input AIG upon a cache miss.

theorem Std.Sat.AIG.mkAtomCached_decl_eq {α : Type} [Hashable α] [DecidableEq α] (aig : Std.Sat.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 : Std.Sat.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 α] : Std.Sat.AIG.LawfulOperator α (fun (x : Std.Sat.AIG α) => α) Std.Sat.AIG.mkAtomCached

Equations

• Std.Sat.AIG.instLawfulOperatorMkAtomCached = { le_size := ⋯, decl_eq := ⋯ }

@[simp]

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

The central equality theorem between mkAtomCached and mkAtom.

theorem Std.Sat.AIG.denote_mkConst_cached {α : Type} [Hashable α] [DecidableEq α] {b : Bool} {assign : α → Bool} {aig : Std.Sat.AIG α} {hit : Std.Sat.AIG.CacheHit aig.decls (Std.Sat.AIG.Decl.const b)} : aig.cache.get? (Std.Sat.AIG.Decl.const b) = some hit → ⟦assign, { aig := aig, ref := { gate := hit.idx, hgate := ⋯ } }⟧ = ⟦assign, aig.mkConst b⟧

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

theorem Std.Sat.AIG.mkConstCached_hit_aig {α : Type} [Hashable α] [DecidableEq α] {val : Bool} (aig : Std.Sat.AIG α) {hit : Std.Sat.AIG.CacheHit aig.decls (Std.Sat.AIG.Decl.const val)} (hcache : aig.cache.get? (Std.Sat.AIG.Decl.const val) = some hit) : (aig.mkConstCached val).aig = aig

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

theorem Std.Sat.AIG.mkConstCached_miss_aig {α : Type} [Hashable α] [DecidableEq α] {val : Bool} (aig : Std.Sat.AIG α) (hcache : aig.cache.get? (Std.Sat.AIG.Decl.const val) = none) : (aig.mkConstCached val).aig.decls = aig.decls.push (Std.Sat.AIG.Decl.const val)

mkConstCached pushes to the input AIG upon a cache miss.

theorem Std.Sat.AIG.mkConstCached_decl_eq {α : Type} [Hashable α] [DecidableEq α] (aig : Std.Sat.AIG α) (val : Bool) (idx : Nat) {h : idx < aig.decls.size} {hbound : idx < (aig.mkConstCached val).aig.decls.size} : (aig.mkConstCached val).aig.decls[idx] = aig.decls[idx]

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

theorem Std.Sat.AIG.mkConstCached_le_size {α : Type} [Hashable α] [DecidableEq α] (aig : Std.Sat.AIG α) (val : Bool) : aig.decls.size ≤ (aig.mkConstCached val).aig.decls.size

AIG.mkConstCached never shrinks the underlying AIG.

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

Equations

• Std.Sat.AIG.instLawfulOperatorBoolMkConstCached = { le_size := ⋯, decl_eq := ⋯ }

@[simp]

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

The central equality theorem between mkConstCached and mkConst.

theorem Std.Sat.AIG.denote_mkGate_cached {α : Type} [Hashable α] [DecidableEq α] {assign : α → Bool} {aig : Std.Sat.AIG α} {input : aig.GateInput} {hit : Std.Sat.AIG.CacheHit aig.decls (Std.Sat.AIG.Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv)} : aig.cache.get? (Std.Sat.AIG.Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv) = some hit → ⟦assign, { aig := aig, ref := { gate := hit.idx, 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 : Std.Sat.AIG α) (input : aig.GateInput) : aig.decls.size ≤ (Std.Sat.AIG.mkGateCached.go aig input).aig.decls.size

theorem Std.Sat.AIG.mkGateCached_le_size {α : Type} [Hashable α] [DecidableEq α] (aig : Std.Sat.AIG α) (input : aig.GateInput) : 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 : Std.Sat.AIG α) (input : aig.GateInput) (idx : Nat) (h1 : idx < (Std.Sat.AIG.mkGateCached.go aig input).aig.decls.size) (h2 : idx < aig.decls.size) : (Std.Sat.AIG.mkGateCached.go aig input).aig.decls[idx] = aig.decls[idx]

theorem Std.Sat.AIG.mkGateCached_decl_eq {α : Type} [Hashable α] [DecidableEq α] (aig : Std.Sat.AIG α) (input : aig.GateInput) (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.instLawfulOperatorGateInputMkGateCached {α : Type} [Hashable α] [DecidableEq α] : Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.GateInput Std.Sat.AIG.mkGateCached

Equations

• Std.Sat.AIG.instLawfulOperatorGateInputMkGateCached = { le_size := ⋯, decl_eq := ⋯ }

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

@[simp]

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

The central equality theorem between mkGateCached and mkGate.