This module contains the theory of the cached gate creation functions, mostly enabled by the `LawfulOperator` framework. It is mainly concerned with proving lemmas about the denotational semantics of the gate functions in different scenarios.

source
theorem Std.Sat.AIG.mkNotCached_le_size {α : Type} [Hashable α] [DecidableEq α] (aig : AIG α) (gate : aig.Ref) :
aig.decls.size ≤ (aig.mkNotCached gate).aig.decls.size
source
theorem Std.Sat.AIG.mkNotCached_decl_eq {α : Type} [Hashable α] [DecidableEq α] (idx : Nat) (aig : AIG α) (gate : aig.Ref) {h : idx < aig.decls.size} {h2 : idx < (aig.mkNotCached gate).aig.decls.size} :
(aig.mkNotCached gate).aig.decls[idx] = aig.decls[idx]
source
instance Std.Sat.AIG.instLawfulOperatorRefMkNotCached {α : Type} [Hashable α] [DecidableEq α] :
LawfulOperator α Ref mkNotCached
source
@[simp]
theorem Std.Sat.AIG.denote_mkNotCached {α : Type} [Hashable α] [DecidableEq α] {assign : α → Bool} {aig : AIG α} {gate : aig.Ref} :
⟦assign, aig.mkNotCached gate⟧ = !⟦assign, { aig := aig, ref := gate }⟧
source
theorem Std.Sat.AIG.mkAndCached_le_size {α : Type} [Hashable α] [DecidableEq α] (aig : AIG α) (input : aig.BinaryInput) :
aig.decls.size ≤ (aig.mkAndCached input).aig.decls.size
source
theorem Std.Sat.AIG.mkAndCached_decl_eq {α : Type} [Hashable α] [DecidableEq α] (idx : Nat) (aig : AIG α) (input : aig.BinaryInput) {h : idx < aig.decls.size} {h2 : idx < (aig.mkAndCached input).aig.decls.size} :
(aig.mkAndCached input).aig.decls[idx] = aig.decls[idx]
source
instance Std.Sat.AIG.instLawfulOperatorBinaryInputMkAndCached {α : Type} [Hashable α] [DecidableEq α] :
LawfulOperator α BinaryInput mkAndCached
source
@[simp]
theorem Std.Sat.AIG.denote_mkAndCached {α : Type} [Hashable α] [DecidableEq α] {assign : α → Bool} {aig : AIG α} {input : aig.BinaryInput} :
⟦assign, aig.mkAndCached input⟧ = (⟦assign, { aig := aig, ref := input.lhs }⟧ && ⟦assign, { aig := aig, ref := input.rhs }⟧)
source
theorem Std.Sat.AIG.mkOrCached_le_size {α : Type} [Hashable α] [DecidableEq α] (aig : AIG α) (input : aig.BinaryInput) :
aig.decls.size ≤ (aig.mkOrCached input).aig.decls.size
source
theorem Std.Sat.AIG.mkOrCached_decl_eq {α : Type} [Hashable α] [DecidableEq α] (idx : Nat) (aig : AIG α) (input : aig.BinaryInput) {h : idx < aig.decls.size} {h2 : idx < (aig.mkOrCached input).aig.decls.size} :
(aig.mkOrCached input).aig.decls[idx] = aig.decls[idx]
source
instance Std.Sat.AIG.instLawfulOperatorBinaryInputMkOrCached {α : Type} [Hashable α] [DecidableEq α] :
LawfulOperator α BinaryInput mkOrCached
source
@[simp]
theorem Std.Sat.AIG.denote_mkOrCached {α : Type} [Hashable α] [DecidableEq α] {assign : α → Bool} {aig : AIG α} {input : aig.BinaryInput} :
⟦assign, aig.mkOrCached input⟧ = (⟦assign, { aig := aig, ref := input.lhs }⟧ || ⟦assign, { aig := aig, ref := input.rhs }⟧)
source
theorem Std.Sat.AIG.mkXorCached_le_size {α : Type} [Hashable α] [DecidableEq α] (aig : AIG α) {input : aig.BinaryInput} :
aig.decls.size ≤ (aig.mkXorCached input).aig.decls.size
source
theorem Std.Sat.AIG.mkXorCached_decl_eq {α : Type} [Hashable α] [DecidableEq α] (idx : Nat) (aig : AIG α) (input : aig.BinaryInput) {h : idx < aig.decls.size} {h2 : idx < (aig.mkXorCached input).aig.decls.size} :
(aig.mkXorCached input).aig.decls[idx] = aig.decls[idx]
source
instance Std.Sat.AIG.instLawfulOperatorBinaryInputMkXorCached {α : Type} [Hashable α] [DecidableEq α] :
LawfulOperator α BinaryInput mkXorCached
source
@[simp]
theorem Std.Sat.AIG.denote_mkXorCached {α : Type} [Hashable α] [DecidableEq α] {assign : α → Bool} {aig : AIG α} {input : aig.BinaryInput} :
⟦assign, aig.mkXorCached input⟧ = (⟦assign, { aig := aig, ref := input.lhs }⟧ ^^ ⟦assign, { aig := aig, ref := input.rhs }⟧)
source
theorem Std.Sat.AIG.mkBEqCached_le_size {α : Type} [Hashable α] [DecidableEq α] (aig : AIG α) {input : aig.BinaryInput} :
aig.decls.size ≤ (aig.mkBEqCached input).aig.decls.size
source
theorem Std.Sat.AIG.mkBEqCached_decl_eq {α : Type} [Hashable α] [DecidableEq α] (idx : Nat) (aig : AIG α) (input : aig.BinaryInput) {h : idx < aig.decls.size} {h2 : idx < (aig.mkBEqCached input).aig.decls.size} :
(aig.mkBEqCached input).aig.decls[idx] = aig.decls[idx]
source
instance Std.Sat.AIG.instLawfulOperatorBinaryInputMkBEqCached {α : Type} [Hashable α] [DecidableEq α] :
LawfulOperator α BinaryInput mkBEqCached
source
@[simp]
theorem Std.Sat.AIG.denote_mkBEqCached {α : Type} [Hashable α] [DecidableEq α] {assign : α → Bool} {aig : AIG α} {input : aig.BinaryInput} :
⟦assign, aig.mkBEqCached input⟧ = (⟦assign, { aig := aig, ref := input.lhs }⟧ == ⟦assign, { aig := aig, ref := input.rhs }⟧)
source
theorem Std.Sat.AIG.mkImpCached_le_size {α : Type} [Hashable α] [DecidableEq α] (aig : AIG α) (input : aig.BinaryInput) :
aig.decls.size ≤ (aig.mkImpCached input).aig.decls.size
source
theorem Std.Sat.AIG.mkImpCached_decl_eq {α : Type} [Hashable α] [DecidableEq α] (idx : Nat) (aig : AIG α) (input : aig.BinaryInput) {h : idx < aig.decls.size} {h2 : idx < (aig.mkImpCached input).aig.decls.size} :
(aig.mkImpCached input).aig.decls[idx] = aig.decls[idx]
source
instance Std.Sat.AIG.instLawfulOperatorBinaryInputMkImpCached {α : Type} [Hashable α] [DecidableEq α] :
LawfulOperator α BinaryInput mkImpCached
source
@[simp]
theorem Std.Sat.AIG.denote_mkImpCached {α : Type} [Hashable α] [DecidableEq α] {assign : α → Bool} {aig : AIG α} {input : aig.BinaryInput} :
⟦assign, aig.mkImpCached input⟧ = (!⟦assign, { aig := aig, ref := input.lhs }⟧ || ⟦assign, { aig := aig, ref := input.rhs }⟧)