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.

@[simp]

theorem Std.Sat.AIG.BinaryInput_asGateInput_lhs {α : Type} [Hashable α] [DecidableEq α] {aig : Std.Sat.AIG α} (input : aig.BinaryInput) (linv rinv : Bool) : (input.asGateInput linv rinv).lhs = { ref := input.lhs, inv := linv }

@[simp]

theorem Std.Sat.AIG.BinaryInput_asGateInput_rhs {α : Type} [Hashable α] [DecidableEq α] {aig : Std.Sat.AIG α} (input : aig.BinaryInput) (linv rinv : Bool) : (input.asGateInput linv rinv).rhs = { ref := input.rhs, inv := rinv }

theorem Std.Sat.AIG.mkNotCached_le_size {α : Type} [Hashable α] [DecidableEq α] (aig : Std.Sat.AIG α) (gate : aig.Ref) : aig.decls.size ≤ (aig.mkNotCached gate).aig.decls.size

theorem Std.Sat.AIG.mkNotCached_decl_eq {α : Type} [Hashable α] [DecidableEq α] (idx : Nat) (aig : Std.Sat.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]

instance Std.Sat.AIG.instLawfulOperatorRefMkNotCached {α : Type} [Hashable α] [DecidableEq α] : Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.Ref Std.Sat.AIG.mkNotCached

@[simp]

theorem Std.Sat.AIG.denote_mkNotCached {α : Type} [Hashable α] [DecidableEq α] {assign : α → Bool} {aig : Std.Sat.AIG α} {gate : aig.Ref} : ⟦assign, aig.mkNotCached gate⟧ = !⟦assign, { aig := aig, ref := { gate := gate.gate, hgate := ⋯ } }⟧

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

theorem Std.Sat.AIG.mkAndCached_decl_eq {α : Type} [Hashable α] [DecidableEq α] (idx : Nat) (aig : Std.Sat.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]

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

@[simp]

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

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

theorem Std.Sat.AIG.mkOrCached_decl_eq {α : Type} [Hashable α] [DecidableEq α] (idx : Nat) (aig : Std.Sat.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]

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

@[simp]

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

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

theorem Std.Sat.AIG.mkXorCached_decl_eq {α : Type} [Hashable α] [DecidableEq α] (idx : Nat) (aig : Std.Sat.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]

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

@[simp]

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

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

theorem Std.Sat.AIG.mkBEqCached_decl_eq {α : Type} [Hashable α] [DecidableEq α] (idx : Nat) (aig : Std.Sat.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]

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

@[simp]

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

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

theorem Std.Sat.AIG.mkImpCached_decl_eq {α : Type} [Hashable α] [DecidableEq α] (idx : Nat) (aig : Std.Sat.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]

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

@[simp]

theorem Std.Sat.AIG.denote_mkImpCached {α : Type} [Hashable α] [DecidableEq α] {assign : α → Bool} {aig : Std.Sat.AIG α} {input : aig.BinaryInput} : ⟦assign, aig.mkImpCached input⟧ = (!⟦assign, { aig := aig, ref := { gate := input.lhs.gate, hgate := ⋯ } }⟧ || ⟦assign, { aig := aig, ref := { gate := input.rhs.gate, hgate := ⋯ } }⟧)