Documentation

Std.Sat.AIG.RefVecOperator.Fold

source
@[specialize #[]]
def Std.Sat.AIG.RefVec.fold {α : Type} [Hashable α] [DecidableEq α] {len : Nat} (aig : AIG α) (vec : aig.RefVec len) (func : (aig : AIG α) → aig.BinaryInput → Entrypoint α) [LawfulOperator α BinaryInput func] :
Entrypoint α
Equations
Instances For
    source
    @[irreducible, specialize #[]]
    def Std.Sat.AIG.RefVec.fold.go {α : Type} [Hashable α] [DecidableEq α] (aig : AIG α) (acc : aig.Ref) (idx len : Nat) (input : aig.RefVec len) (f : (aig : AIG α) → aig.BinaryInput → Entrypoint α) [LawfulOperator α BinaryInput f] :
    Entrypoint α
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem Std.Sat.AIG.RefVec.fold.go_le_size {α : Type} [Hashable α] [DecidableEq α] {len : Nat} {aig : AIG α} (acc : aig.Ref) (idx : Nat) (s : aig.RefVec len) (f : (aig : AIG α) → aig.BinaryInput → Entrypoint α) [LawfulOperator α BinaryInput f] :
      aig.decls.size ≤ (go aig acc idx len s f).aig.decls.size
      source
      theorem Std.Sat.AIG.RefVec.fold_le_size {α : Type} [Hashable α] [DecidableEq α] {len : Nat} {aig : AIG α} (vec : aig.RefVec len) (func : (aig : AIG α) → aig.BinaryInput → Entrypoint α) [LawfulOperator α BinaryInput func] :
      aig.decls.size ≤ (fold aig vec func).aig.decls.size
      source
      theorem Std.Sat.AIG.RefVec.fold.go_decl_eq {α : Type} [Hashable α] [DecidableEq α] {len : Nat} {aig : AIG α} (acc : aig.Ref) (i : Nat) (s : aig.RefVec len) (f : (aig : AIG α) → aig.BinaryInput → Entrypoint α) [LawfulOperator α BinaryInput f] (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < (go aig acc i len s f).aig.decls.size) :
      (go aig acc i len s f).aig.decls[idx] = aig.decls[idx]
      source
      theorem Std.Sat.AIG.RefVec.fold_decl_eq {α : Type} [Hashable α] [DecidableEq α] {len : Nat} {aig : AIG α} (vec : aig.RefVec len) (func : (aig : AIG α) → aig.BinaryInput → Entrypoint α) [LawfulOperator α BinaryInput func] (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < (fold aig vec func).aig.decls.size) :
      (fold aig vec func).aig.decls[idx] = aig.decls[idx]
      source
      theorem Std.Sat.AIG.RefVec.fold_lt_size_of_lt_aig_size {α : Type} [Hashable α] [DecidableEq α] {len x : Nat} (aig : AIG α) (vec : aig.RefVec len) (func : (aig : AIG α) → aig.BinaryInput → Entrypoint α) [LawfulOperator α BinaryInput func] (h : x < aig.decls.size) :
      x < (fold aig vec func).aig.decls.size
      source
      theorem Std.Sat.AIG.RefVec.fold_le_size_of_le_aig_size {α : Type} [Hashable α] [DecidableEq α] {len x : Nat} (aig : AIG α) (vec : aig.RefVec len) (func : (aig : AIG α) → aig.BinaryInput → Entrypoint α) [LawfulOperator α BinaryInput func] (h : x ≤ aig.decls.size) :
      x ≤ (fold aig vec func).aig.decls.size
      source
      theorem Std.Sat.AIG.RefVec.fold.denote_go_and {α : Type} [Hashable α] [DecidableEq α] {len : Nat} {assign : α → Bool} {aig : AIG α} (acc : aig.Ref) (curr : Nat) (hcurr : curr ≤ len) (input : aig.RefVec len) :
      (⟦assign, { aig := (go aig acc curr len input mkAndCached).aig, ref := (go aig acc curr len input mkAndCached).ref }⟧ = true) = (⟦assign, { aig := aig, ref := acc }⟧ = true ∧ ∀ (idx : Nat) (hidx1 : idx < len), curr ≤ idx → ⟦assign, { aig := aig, ref := input.get idx hidx1 }⟧ = true)
      source
      @[simp]
      theorem Std.Sat.AIG.RefVec.denote_fold_and {α : Type} [Hashable α] [DecidableEq α] {len : Nat} {assign : α → Bool} {aig : AIG α} (s : aig.RefVec len) :
      ⟦assign, fold aig s mkAndCached⟧ = true ↔ ∀ (idx : Nat) (hidx : idx < len), ⟦assign, { aig := aig, ref := s.get idx hidx }⟧ = true