Std.Sat.AIG.CachedGatesLemmas

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

@[simp]

theorem Std.Sat.AIG.BinaryInput_asGateInput_lhs {α : Type} [Hashable α] [DecidableEq α] {aig : Std.Sat.AIG α} (input : aig.BinaryInput) (linv : Bool) (rinv : Bool) :

(input.asGateInput linv rinv).lhs = { ref := input.lhs, inv := linv }

source

@[simp]

theorem Std.Sat.AIG.BinaryInput_asGateInput_rhs {α : Type} [Hashable α] [DecidableEq α] {aig : Std.Sat.AIG α} (input : aig.BinaryInput) (linv : Bool) (rinv : Bool) :

(input.asGateInput linv rinv).rhs = { ref := input.rhs, inv := rinv }

source

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

source

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]

source

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

Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.Ref Std.Sat.AIG.mkNotCached

Equations

⋯ = ⋯

source

@[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 := ⋯ } }⟧

source

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

source

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]

source

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

Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.BinaryInput Std.Sat.AIG.mkAndCached

Equations

⋯ = ⋯

source

@[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 }⟧)

source

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

source

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]

source

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

Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.BinaryInput Std.Sat.AIG.mkOrCached

Equations

⋯ = ⋯

source

@[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 }⟧)

source

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

source

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]

source

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

Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.BinaryInput Std.Sat.AIG.mkXorCached

Equations

⋯ = ⋯

source

@[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 }⟧)

source

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

source

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]

source

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

Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.BinaryInput Std.Sat.AIG.mkBEqCached

Equations

⋯ = ⋯

source

@[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 }⟧)

source

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

source

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]

source

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

Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.BinaryInput Std.Sat.AIG.mkImpCached

Equations

⋯ = ⋯

source

@[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 := ⋯ } }⟧)