class
Std.Sat.AIG.LawfulVecOperator
(α : Type)
[Hashable α]
[DecidableEq α]
(β : Std.Sat.AIG α → Nat → Type)
(f : {len : Nat} → (aig : Std.Sat.AIG α) → β aig len → Std.Sat.AIG.RefVecEntry α len)
:
- le_size : ∀ {len : Nat} (aig : Std.Sat.AIG α) (input : β aig len), aig.decls.size ≤ (f aig input).aig.decls.size
Instances
theorem
Std.Sat.AIG.LawfulVecOperator.le_size
{α : Type}
[Hashable α]
[DecidableEq α]
{β : Std.Sat.AIG α → Nat → Type}
{f : {len : Nat} → (aig : Std.Sat.AIG α) → β aig len → Std.Sat.AIG.RefVecEntry α len}
[self : Std.Sat.AIG.LawfulVecOperator α β f]
{len : Nat}
(aig : Std.Sat.AIG α)
(input : β aig len)
:
aig.decls.size ≤ (f aig input).aig.decls.size
theorem
Std.Sat.AIG.LawfulVecOperator.decl_eq
{α : Type}
[Hashable α]
[DecidableEq α]
{β : Std.Sat.AIG α → Nat → Type}
{f : {len : Nat} → (aig : Std.Sat.AIG α) → β aig len → Std.Sat.AIG.RefVecEntry α len}
[self : Std.Sat.AIG.LawfulVecOperator α β f]
{len : Nat}
(aig : Std.Sat.AIG α)
(input : β aig len)
(idx : Nat)
(h1 : idx < aig.decls.size)
(h2 : idx < (f aig input).aig.decls.size)
:
(f aig input).aig.decls[idx] = aig.decls[idx]
theorem
Std.Sat.AIG.LawfulVecOperator.isPrefix_aig
{α : Type}
[Hashable α]
[DecidableEq α]
{β : Std.Sat.AIG α → Nat → Type}
{f : {len : Nat} → (aig : Std.Sat.AIG α) → β aig len → Std.Sat.AIG.RefVecEntry α len}
[Std.Sat.AIG.LawfulVecOperator α β fun {len : Nat} => f]
{len : Nat}
(aig : Std.Sat.AIG α)
(input : β aig len)
:
Std.Sat.AIG.IsPrefix aig.decls (f aig input).aig.decls
theorem
Std.Sat.AIG.LawfulVecOperator.lt_size
{α : Type}
[Hashable α]
[DecidableEq α]
{β : Std.Sat.AIG α → Nat → Type}
{f : {len : Nat} → (aig : Std.Sat.AIG α) → β aig len → Std.Sat.AIG.RefVecEntry α len}
[Std.Sat.AIG.LawfulVecOperator α β fun {len : Nat} => f]
{len : Nat}
(entry : Std.Sat.AIG.Entrypoint α)
(input : β entry.aig len)
:
entry.ref.gate < (f entry.aig input).aig.decls.size
theorem
Std.Sat.AIG.LawfulVecOperator.lt_size_of_lt_aig_size
{α : Type}
[Hashable α]
[DecidableEq α]
{β : Std.Sat.AIG α → Nat → Type}
{f : {len : Nat} → (aig : Std.Sat.AIG α) → β aig len → Std.Sat.AIG.RefVecEntry α len}
[Std.Sat.AIG.LawfulVecOperator α β fun {len : Nat} => f]
{len : Nat}
{x : Nat}
(aig : Std.Sat.AIG α)
(input : β aig len)
(h : x < aig.decls.size)
:
x < (f aig input).aig.decls.size
theorem
Std.Sat.AIG.LawfulVecOperator.le_size_of_le_aig_size
{α : Type}
[Hashable α]
[DecidableEq α]
{β : Std.Sat.AIG α → Nat → Type}
{f : {len : Nat} → (aig : Std.Sat.AIG α) → β aig len → Std.Sat.AIG.RefVecEntry α len}
[Std.Sat.AIG.LawfulVecOperator α β fun {len : Nat} => f]
{len : Nat}
{x : Nat}
(aig : Std.Sat.AIG α)
(input : β aig len)
(h : x ≤ aig.decls.size)
:
x ≤ (f aig input).aig.decls.size
@[simp]
theorem
Std.Sat.AIG.LawfulVecOperator.denote_input_entry
{α : Type}
[Hashable α]
[DecidableEq α]
{β : Std.Sat.AIG α → Nat → Type}
{f : {len : Nat} → (aig : Std.Sat.AIG α) → β aig len → Std.Sat.AIG.RefVecEntry α len}
[Std.Sat.AIG.LawfulVecOperator α β fun {len : Nat} => f]
{len : Nat}
{assign : α → Bool}
(entry : Std.Sat.AIG.Entrypoint α)
{input : β entry.aig len}
{h : entry.ref.gate < (f entry.aig input).aig.decls.size}
:
⟦assign, { aig := (f entry.aig input).aig, ref := { gate := entry.ref.gate, hgate := h } }⟧ = ⟦assign, entry⟧
@[simp]
theorem
Std.Sat.AIG.LawfulVecOperator.denote_cast_entry
{α : Type}
[Hashable α]
[DecidableEq α]
{β : Std.Sat.AIG α → Nat → Type}
{f : {len : Nat} → (aig : Std.Sat.AIG α) → β aig len → Std.Sat.AIG.RefVecEntry α len}
[Std.Sat.AIG.LawfulVecOperator α β fun {len : Nat} => f]
{len : Nat}
{assign : α → Bool}
(entry : Std.Sat.AIG.Entrypoint α)
{input : β entry.aig len}
{h : entry.aig.decls.size ≤ (f entry.aig input).aig.decls.size}
:
⟦assign, { aig := (f entry.aig input).aig, ref := entry.ref.cast h }⟧ = ⟦assign, entry⟧
theorem
Std.Sat.AIG.LawfulVecOperator.denote_mem_prefix
{α : Type}
[Hashable α]
[DecidableEq α]
{β : Std.Sat.AIG α → Nat → Type}
{f : {len : Nat} → (aig : Std.Sat.AIG α) → β aig len → Std.Sat.AIG.RefVecEntry α len}
[Std.Sat.AIG.LawfulVecOperator α β fun {len : Nat} => f]
{len : Nat}
{assign : α → Bool}
{start : Nat}
{aig : Std.Sat.AIG α}
{input : β aig len}
(h : start < aig.decls.size)
:
⟦assign, { aig := (f aig input).aig, ref := { gate := start, hgate := ⋯ } }⟧ = ⟦assign, { aig := aig, ref := { gate := start, hgate := h } }⟧
@[simp]
theorem
Std.Sat.AIG.LawfulVecOperator.denote_input_vec
{α : Type}
[Hashable α]
[DecidableEq α]
{β : Std.Sat.AIG α → Nat → Type}
{f : {len : Nat} → (aig : Std.Sat.AIG α) → β aig len → Std.Sat.AIG.RefVecEntry α len}
[Std.Sat.AIG.LawfulVecOperator α β fun {len : Nat} => f]
{len : Nat}
{assign : α → Bool}
{idx : Nat}
{hidx : idx < len}
(s : Std.Sat.AIG.RefVecEntry α len)
{input : β s.aig len}
{hcast : s.aig.decls.size ≤ (f s.aig input).aig.decls.size}
:
⟦assign, { aig := (f s.aig input).aig, ref := (s.vec.get idx hidx).cast hcast }⟧ = ⟦assign, { aig := s.aig, ref := s.vec.get idx hidx }⟧