Documentation

Std.Sat.AIG.RefVecOperator.Fold

Instances For
    theorem Std.Sat.AIG.RefVec.FoldTarget.lawful {α : Type} [Hashable α] [DecidableEq α] {aig : Std.Sat.AIG α} (self : Std.Sat.AIG.RefVec.FoldTarget aig) :
    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) :
    Equations
    Instances For
      @[specialize #[]]
      Equations
      Instances For
        @[irreducible, specialize #[]]
        def Std.Sat.AIG.RefVec.fold.go {α : Type} [Hashable α] [DecidableEq α] (aig : Std.Sat.AIG α) (acc : aig.Ref) (idx : Nat) (len : Nat) (input : aig.RefVec len) (f : (aig : Std.Sat.AIG α) → aig.BinaryInputStd.Sat.AIG.Entrypoint α) [Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.BinaryInput f] :
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[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.BinaryInputStd.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.BinaryInputStd.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 idxassign, { 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