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]
theorem
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}
:
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]
theorem
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}
:
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]
theorem
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}
:
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]
theorem
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}
:
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]
theorem
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}
:
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]
theorem
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}
: