Documentation

Std.Sat.AIG.CachedLemmas

This module contains the theory of the cached AIG node creation functions. It is mainly concerned with proving lemmas about the denotational semantics of the gate functions in different scenarios, in particular reductions to the semantics of the non cached versions.

theorem Std.Sat.AIG.denote_mkAtom_cached {α : Type} [Hashable α] [DecidableEq α] {v : α} {assign : αBool} {aig : Std.Sat.AIG α} {hit : Std.Sat.AIG.CacheHit aig.decls (Std.Sat.AIG.Decl.atom v)} :
aig.cache.get? (Std.Sat.AIG.Decl.atom v) = some hitassign, { aig := aig, ref := { gate := hit.idx, hgate := } } = assign, aig.mkAtom v

If we find a cached atom declaration in the AIG, denoting it is equivalent to denoting AIG.mkAtom.

theorem Std.Sat.AIG.mkAtomCached_hit_aig {α : Type} [Hashable α] [DecidableEq α] {var : α} (aig : Std.Sat.AIG α) {hit : Std.Sat.AIG.CacheHit aig.decls (Std.Sat.AIG.Decl.atom var)} (hcache : aig.cache.get? (Std.Sat.AIG.Decl.atom var) = some hit) :
(aig.mkAtomCached var).aig = aig

mkAtomCached does not modify the input AIG upon a cache hit.

theorem Std.Sat.AIG.mkAtomCached_miss_aig {α : Type} [Hashable α] [DecidableEq α] {var : α} (aig : Std.Sat.AIG α) (hcache : aig.cache.get? (Std.Sat.AIG.Decl.atom var) = none) :
(aig.mkAtomCached var).aig.decls = aig.decls.push (Std.Sat.AIG.Decl.atom var)

mkAtomCached pushes to the input AIG upon a cache miss.

theorem Std.Sat.AIG.mkAtomCached_decl_eq {α : Type} [Hashable α] [DecidableEq α] (aig : Std.Sat.AIG α) (var : α) (idx : Nat) {h : idx < aig.decls.size} {hbound : idx < (aig.mkAtomCached var).aig.decls.size} :
(aig.mkAtomCached var).aig.decls[idx] = aig.decls[idx]

The AIG produced by AIG.mkAtomCached agrees with the input AIG on all indices that are valid for both.

theorem Std.Sat.AIG.mkAtomCached_le_size {α : Type} [Hashable α] [DecidableEq α] (aig : Std.Sat.AIG α) (var : α) :
aig.decls.size (aig.mkAtomCached var).aig.decls.size

AIG.mkAtomCached never shrinks the underlying AIG.

instance Std.Sat.AIG.instLawfulOperatorMkAtomCached {α : Type} [Hashable α] [DecidableEq α] :
Std.Sat.AIG.LawfulOperator α (fun (x : Std.Sat.AIG α) => α) Std.Sat.AIG.mkAtomCached
Equations
  • =
@[simp]
theorem Std.Sat.AIG.mkAtomCached_eval_eq_mkAtom_eval {α : Type} [Hashable α] [DecidableEq α] {assign : αBool} {var : α} {aig : Std.Sat.AIG α} :
assign, aig.mkAtomCached var = assign, aig.mkAtom var

The central equality theorem between mkAtomCached and mkAtom.

theorem Std.Sat.AIG.denote_mkConst_cached {α : Type} [Hashable α] [DecidableEq α] {b : Bool} {assign : αBool} {aig : Std.Sat.AIG α} {hit : Std.Sat.AIG.CacheHit aig.decls (Std.Sat.AIG.Decl.const b)} :
aig.cache.get? (Std.Sat.AIG.Decl.const b) = some hitassign, { aig := aig, ref := { gate := hit.idx, hgate := } } = assign, aig.mkConst b

If we find a cached const declaration in the AIG, denoting it is equivalent to denoting AIG.mkConst.

theorem Std.Sat.AIG.mkConstCached_hit_aig {α : Type} [Hashable α] [DecidableEq α] {val : Bool} (aig : Std.Sat.AIG α) {hit : Std.Sat.AIG.CacheHit aig.decls (Std.Sat.AIG.Decl.const val)} (hcache : aig.cache.get? (Std.Sat.AIG.Decl.const val) = some hit) :
(aig.mkConstCached val).aig = aig

mkConstCached does not modify the input AIG upon a cache hit.

theorem Std.Sat.AIG.mkConstCached_miss_aig {α : Type} [Hashable α] [DecidableEq α] {val : Bool} (aig : Std.Sat.AIG α) (hcache : aig.cache.get? (Std.Sat.AIG.Decl.const val) = none) :
(aig.mkConstCached val).aig.decls = aig.decls.push (Std.Sat.AIG.Decl.const val)

mkConstCached pushes to the input AIG upon a cache miss.

theorem Std.Sat.AIG.mkConstCached_decl_eq {α : Type} [Hashable α] [DecidableEq α] (aig : Std.Sat.AIG α) (val : Bool) (idx : Nat) {h : idx < aig.decls.size} {hbound : idx < (aig.mkConstCached val).aig.decls.size} :
(aig.mkConstCached val).aig.decls[idx] = aig.decls[idx]

The AIG produced by AIG.mkConstCached agrees with the input AIG on all indices that are valid for both.

theorem Std.Sat.AIG.mkConstCached_le_size {α : Type} [Hashable α] [DecidableEq α] (aig : Std.Sat.AIG α) (val : Bool) :
aig.decls.size (aig.mkConstCached val).aig.decls.size

AIG.mkConstCached never shrinks the underlying AIG.

instance Std.Sat.AIG.instLawfulOperatorBoolMkConstCached {α : Type} [Hashable α] [DecidableEq α] :
Std.Sat.AIG.LawfulOperator α (fun (x : Std.Sat.AIG α) => Bool) Std.Sat.AIG.mkConstCached
Equations
  • =
@[simp]
theorem Std.Sat.AIG.mkConstCached_eval_eq_mkConst_eval {α : Type} [Hashable α] [DecidableEq α] {assign : αBool} {val : Bool} {aig : Std.Sat.AIG α} :
assign, aig.mkConstCached val = assign, aig.mkConst val

The central equality theorem between mkConstCached and mkConst.

theorem Std.Sat.AIG.denote_mkGate_cached {α : Type} [Hashable α] [DecidableEq α] {assign : αBool} {aig : Std.Sat.AIG α} {input : aig.GateInput} {hit : Std.Sat.AIG.CacheHit aig.decls (Std.Sat.AIG.Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv)} :
aig.cache.get? (Std.Sat.AIG.Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv) = some hitassign, { aig := aig, ref := { gate := hit.idx, hgate := } } = assign, aig.mkGate input

If we find a cached gate declaration in the AIG, denoting it is equivalent to denoting AIG.mkGate.

theorem Std.Sat.AIG.mkGateCached.go_le_size {α : Type} [Hashable α] [DecidableEq α] (aig : Std.Sat.AIG α) (input : aig.GateInput) :
aig.decls.size (Std.Sat.AIG.mkGateCached.go aig input).aig.decls.size
theorem Std.Sat.AIG.mkGateCached_le_size {α : Type} [Hashable α] [DecidableEq α] (aig : Std.Sat.AIG α) (input : aig.GateInput) :
aig.decls.size (aig.mkGateCached input).aig.decls.size

AIG.mkGateCached never shrinks the underlying AIG.

theorem Std.Sat.AIG.mkGateCached.go_decl_eq {α : Type} [Hashable α] [DecidableEq α] (aig : Std.Sat.AIG α) (input : aig.GateInput) (idx : Nat) (h1 : idx < (Std.Sat.AIG.mkGateCached.go aig input).aig.decls.size) (h2 : idx < aig.decls.size) :
(Std.Sat.AIG.mkGateCached.go aig input).aig.decls[idx] = aig.decls[idx]
theorem Std.Sat.AIG.mkGateCached_decl_eq {α : Type} [Hashable α] [DecidableEq α] (aig : Std.Sat.AIG α) (input : aig.GateInput) (idx : Nat) (h1 : idx < (aig.mkGateCached input).aig.decls.size) (h2 : idx < aig.decls.size) :
(aig.mkGateCached input).aig.decls[idx] = aig.decls[idx]

The AIG produced by AIG.mkGateCached agrees with the input AIG on all indices that are valid for both.

instance Std.Sat.AIG.instLawfulOperatorGateInputMkGateCached {α : Type} [Hashable α] [DecidableEq α] :
Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.GateInput Std.Sat.AIG.mkGateCached
Equations
  • =
theorem Std.Sat.AIG.mkGateCached.go_eval_eq_mkGate_eval {α : Type} [Hashable α] [DecidableEq α] {assign : αBool} {aig : Std.Sat.AIG α} {input : aig.GateInput} :
assign, Std.Sat.AIG.mkGateCached.go aig input = assign, aig.mkGate input
@[simp]
theorem Std.Sat.AIG.mkGateCached_eval_eq_mkGate_eval {α : Type} [Hashable α] [DecidableEq α] {assign : αBool} {aig : Std.Sat.AIG α} {input : aig.GateInput} :
assign, aig.mkGateCached input = assign, aig.mkGate input

The central equality theorem between mkGateCached and mkGate.