Documentation

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.

@[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} :
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
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} :
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
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} :
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
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} :
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
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} :
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
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} :
assign, aig.mkImpCached input = (!assign, { aig := aig, ref := { gate := input.lhs.gate, hgate := } } || assign, { aig := aig, ref := { gate := input.rhs.gate, hgate := } })