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 : Bool)
(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 : Bool)
(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
Equations
- Std.Sat.AIG.instLawfulOperatorRefMkNotCached = { le_size := ⋯, decl_eq := ⋯ }
@[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]
instance
Std.Sat.AIG.instLawfulOperatorBinaryInputMkAndCached
{α : Type}
[Hashable α]
[DecidableEq α]
:
Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.BinaryInput Std.Sat.AIG.mkAndCached
Equations
- Std.Sat.AIG.instLawfulOperatorBinaryInputMkAndCached = { le_size := ⋯, decl_eq := ⋯ }
@[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]
instance
Std.Sat.AIG.instLawfulOperatorBinaryInputMkOrCached
{α : Type}
[Hashable α]
[DecidableEq α]
:
Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.BinaryInput Std.Sat.AIG.mkOrCached
Equations
- Std.Sat.AIG.instLawfulOperatorBinaryInputMkOrCached = { le_size := ⋯, decl_eq := ⋯ }
@[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]
instance
Std.Sat.AIG.instLawfulOperatorBinaryInputMkXorCached
{α : Type}
[Hashable α]
[DecidableEq α]
:
Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.BinaryInput Std.Sat.AIG.mkXorCached
Equations
- Std.Sat.AIG.instLawfulOperatorBinaryInputMkXorCached = { le_size := ⋯, decl_eq := ⋯ }
@[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]
instance
Std.Sat.AIG.instLawfulOperatorBinaryInputMkBEqCached
{α : Type}
[Hashable α]
[DecidableEq α]
:
Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.BinaryInput Std.Sat.AIG.mkBEqCached
Equations
- Std.Sat.AIG.instLawfulOperatorBinaryInputMkBEqCached = { le_size := ⋯, decl_eq := ⋯ }
@[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]
instance
Std.Sat.AIG.instLawfulOperatorBinaryInputMkImpCached
{α : Type}
[Hashable α]
[DecidableEq α]
:
Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.BinaryInput Std.Sat.AIG.mkImpCached
Equations
- Std.Sat.AIG.instLawfulOperatorBinaryInputMkImpCached = { le_size := ⋯, decl_eq := ⋯ }
@[simp]
theorem
Std.Sat.AIG.denote_mkImpCached
{α : Type}
[Hashable α]
[DecidableEq α]
{assign : α → Bool}
{aig : Std.Sat.AIG α}
{input : aig.BinaryInput}
: