structure Std.Sat.AIG.RefVec.FoldTarget {α : Type} [Hashable α] [DecidableEq α] (aig : Std.Sat.AIG α) : Type

• len : Nat
• vec : aig.RefVec self.len
• func : (aig : Std.Sat.AIG α) → aig.BinaryInput → Std.Sat.AIG.Entrypoint α
• lawful : Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.BinaryInput self.func

@[inline]

def Std.Sat.AIG.RefVec.FoldTarget.mkAnd {α : Type} [Hashable α] [DecidableEq α] {w : Nat} {aig : Std.Sat.AIG α} (vec : aig.RefVec w) : Std.Sat.AIG.RefVec.FoldTarget aig

Equations

• Std.Sat.AIG.RefVec.FoldTarget.mkAnd vec = Std.Sat.AIG.RefVec.FoldTarget.mk vec Std.Sat.AIG.mkAndCached

@[specialize #[]]

def Std.Sat.AIG.RefVec.fold {α : Type} [Hashable α] [DecidableEq α] (aig : Std.Sat.AIG α) (target : Std.Sat.AIG.RefVec.FoldTarget aig) : Std.Sat.AIG.Entrypoint α

Equations

• Std.Sat.AIG.RefVec.fold aig target = Std.Sat.AIG.RefVec.fold.go (aig.mkConstCached true).aig (aig.mkConstCached true).ref 0 target.len (target.vec.cast ⋯) target.func

@[irreducible, specialize #[]]

def Std.Sat.AIG.RefVec.fold.go {α : Type} [Hashable α] [DecidableEq α] (aig : Std.Sat.AIG α) (acc : aig.Ref) (idx len : Nat) (input : aig.RefVec len) (f : (aig : Std.Sat.AIG α) → aig.BinaryInput → Std.Sat.AIG.Entrypoint α) [Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.BinaryInput f] : Std.Sat.AIG.Entrypoint α

Equations

• One or more equations did not get rendered due to their size.

@[irreducible]

theorem Std.Sat.AIG.RefVec.fold.go_le_size {α : Type} [Hashable α] [DecidableEq α] {len : Nat} {aig : Std.Sat.AIG α} (acc : aig.Ref) (idx : Nat) (s : aig.RefVec len) (f : (aig : Std.Sat.AIG α) → aig.BinaryInput → Std.Sat.AIG.Entrypoint α) [Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.BinaryInput f] : aig.decls.size ≤ (Std.Sat.AIG.RefVec.fold.go aig acc idx len s f).aig.decls.size

theorem Std.Sat.AIG.RefVec.fold_le_size {α : Type} [Hashable α] [DecidableEq α] {aig : Std.Sat.AIG α} (target : Std.Sat.AIG.RefVec.FoldTarget aig) : aig.decls.size ≤ (Std.Sat.AIG.RefVec.fold aig target).aig.decls.size

@[irreducible]

theorem Std.Sat.AIG.RefVec.fold.go_decl_eq {α : Type} [Hashable α] [DecidableEq α] {len : Nat} {aig : Std.Sat.AIG α} (acc : aig.Ref) (i : Nat) (s : aig.RefVec len) (f : (aig : Std.Sat.AIG α) → aig.BinaryInput → Std.Sat.AIG.Entrypoint α) [Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.BinaryInput f] (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < (Std.Sat.AIG.RefVec.fold.go aig acc i len s f).aig.decls.size) : (Std.Sat.AIG.RefVec.fold.go aig acc i len s f).aig.decls[idx] = aig.decls[idx]

theorem Std.Sat.AIG.RefVec.fold_decl_eq {α : Type} [Hashable α] [DecidableEq α] {aig : Std.Sat.AIG α} (target : Std.Sat.AIG.RefVec.FoldTarget aig) (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < (Std.Sat.AIG.RefVec.fold aig target).aig.decls.size) : (Std.Sat.AIG.RefVec.fold aig target).aig.decls[idx] = aig.decls[idx]

instance Std.Sat.AIG.RefVec.instLawfulOperatorFoldTargetFold {α : Type} [Hashable α] [DecidableEq α] : Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.RefVec.FoldTarget Std.Sat.AIG.RefVec.fold

Equations

• ⋯ = ⋯

@[irreducible]

theorem Std.Sat.AIG.RefVec.fold.denote_go_and {α : Type} [Hashable α] [DecidableEq α] {len : Nat} {assign : α → Bool} {aig : Std.Sat.AIG α} (acc : aig.Ref) (curr : Nat) (hcurr : curr ≤ len) (input : aig.RefVec len) : (⟦assign, { aig := (Std.Sat.AIG.RefVec.fold.go aig acc curr len input Std.Sat.AIG.mkAndCached).aig, ref := (Std.Sat.AIG.RefVec.fold.go aig acc curr len input Std.Sat.AIG.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)

@[simp]

theorem Std.Sat.AIG.RefVec.denote_fold_and {α : Type} [Hashable α] [DecidableEq α] {len : Nat} {assign : α → Bool} {aig : Std.Sat.AIG α} (s : aig.RefVec len) : ⟦assign, Std.Sat.AIG.RefVec.fold aig (Std.Sat.AIG.RefVec.FoldTarget.mkAnd s)⟧ = true ↔ ∀ (idx : Nat) (hidx : idx < len), ⟦assign, { aig := aig, ref := s.get idx hidx }⟧ = true