Documentation

Std.Sat.AIG.RefVecOperator.Zip

class Std.Sat.AIG.RefVec.LawfulZipOperator (α : Type) [Hashable α] [DecidableEq α] (f : (aig : Std.Sat.AIG α) → aig.BinaryInputStd.Sat.AIG.Entrypoint α) [Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.BinaryInput f] :
  • chainable : ∀ (aig : Std.Sat.AIG α) (input1 input2 : aig.BinaryInput) (h : aig.decls.size (f aig input1).aig.decls.size) (assign : αBool), assign, f (f aig input1).aig (input2.cast h) = assign, f aig input2
Instances
    theorem Std.Sat.AIG.RefVec.LawfulZipOperator.chainable {α : Type} :
    ∀ {inst : Hashable α} {inst_1 : DecidableEq α} {f : (aig : Std.Sat.AIG α) → aig.BinaryInputStd.Sat.AIG.Entrypoint α} {inst_2 : Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.BinaryInput f} [self : Std.Sat.AIG.RefVec.LawfulZipOperator α f] (aig : Std.Sat.AIG α) (input1 input2 : aig.BinaryInput) (h : aig.decls.size (f aig input1).aig.decls.size) (assign : αBool), assign, f (f aig input1).aig (input2.cast h) = assign, f aig input2
    theorem Std.Sat.AIG.RefVec.LawfulZipOperator.denote_prefix_cast_ref {α : Type} [Hashable α] [DecidableEq α] {assign : αBool} {aig : Std.Sat.AIG α} {input1 : aig.BinaryInput} {input2 : aig.BinaryInput} {f : (aig : Std.Sat.AIG α) → aig.BinaryInputStd.Sat.AIG.Entrypoint α} [Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.BinaryInput f] [Std.Sat.AIG.RefVec.LawfulZipOperator α f] {h : aig.decls.size (f aig input1).aig.decls.size} :
    assign, f (f aig input1).aig (input2.cast h) = assign, f aig input2
    structure Std.Sat.AIG.RefVec.ZipTarget {α : Type} [Hashable α] [DecidableEq α] (aig : Std.Sat.AIG α) (len : Nat) :
    Instances For
      theorem Std.Sat.AIG.RefVec.ZipTarget.lawful {α : Type} [Hashable α] [DecidableEq α] {aig : Std.Sat.AIG α} {len : Nat} (self : Std.Sat.AIG.RefVec.ZipTarget aig len) :
      Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.BinaryInput self.func
      @[specialize #[]]
      def Std.Sat.AIG.RefVec.zip {α : Type} [Hashable α] [DecidableEq α] {len : Nat} (aig : Std.Sat.AIG α) (target : Std.Sat.AIG.RefVec.ZipTarget aig len) :
      Equations
      Instances For
        @[irreducible, specialize #[]]
        def Std.Sat.AIG.RefVec.zip.go {α : Type} [Hashable α] [DecidableEq α] {len : Nat} (aig : Std.Sat.AIG α) (idx : Nat) (s : aig.RefVec idx) (hidx : idx len) (lhs : aig.RefVec len) (rhs : aig.RefVec len) (f : (aig : Std.Sat.AIG α) → aig.BinaryInputStd.Sat.AIG.Entrypoint α) [Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.BinaryInput f] [Std.Sat.AIG.RefVec.LawfulZipOperator α f] :
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[irreducible]
          theorem Std.Sat.AIG.RefVec.zip.go_le_size {α : Type} [Hashable α] [DecidableEq α] {len : Nat} {aig : Std.Sat.AIG α} (idx : Nat) (hidx : idx len) (s : aig.RefVec idx) (lhs : aig.RefVec len) (rhs : aig.RefVec len) (f : (aig : Std.Sat.AIG α) → aig.BinaryInputStd.Sat.AIG.Entrypoint α) [Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.BinaryInput f] [chainable : Std.Sat.AIG.RefVec.LawfulZipOperator α f] :
          aig.decls.size (Std.Sat.AIG.RefVec.zip.go aig idx s hidx lhs rhs f).aig.decls.size
          theorem Std.Sat.AIG.RefVec.zip_le_size {α : Type} [Hashable α] [DecidableEq α] {len : Nat} {aig : Std.Sat.AIG α} (target : Std.Sat.AIG.RefVec.ZipTarget aig len) :
          aig.decls.size (Std.Sat.AIG.RefVec.zip aig target).aig.decls.size
          @[irreducible]
          theorem Std.Sat.AIG.RefVec.zip.go_decl_eq {α : Type} [Hashable α] [DecidableEq α] {len : Nat} {aig : Std.Sat.AIG α} (i : Nat) (hi : i len) (lhs : aig.RefVec len) (rhs : aig.RefVec len) (s : aig.RefVec i) (f : (aig : Std.Sat.AIG α) → aig.BinaryInputStd.Sat.AIG.Entrypoint α) [Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.BinaryInput f] [chainable : Std.Sat.AIG.RefVec.LawfulZipOperator α f] (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < (Std.Sat.AIG.RefVec.zip.go aig i s hi lhs rhs f).aig.decls.size) :
          (Std.Sat.AIG.RefVec.zip.go aig i s hi lhs rhs f).aig.decls[idx] = aig.decls[idx]
          theorem Std.Sat.AIG.RefVec.zip_decl_eq {α : Type} [Hashable α] [DecidableEq α] {len : Nat} {aig : Std.Sat.AIG α} (target : Std.Sat.AIG.RefVec.ZipTarget aig len) (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < (Std.Sat.AIG.RefVec.zip aig target).aig.decls.size) :
          (Std.Sat.AIG.RefVec.zip aig target).aig.decls[idx] = aig.decls[idx]
          instance Std.Sat.AIG.RefVec.instLawfulVecOperatorZipTargetZip {α : Type} [Hashable α] [DecidableEq α] :
          Std.Sat.AIG.LawfulVecOperator α Std.Sat.AIG.RefVec.ZipTarget fun {len : Nat} => Std.Sat.AIG.RefVec.zip
          Equations
          • =
          @[irreducible]
          theorem Std.Sat.AIG.RefVec.zip.go_get_aux {α : Type} [Hashable α] [DecidableEq α] {len : Nat} {aig : Std.Sat.AIG α} (curr : Nat) (hcurr : curr len) (s : aig.RefVec curr) (lhs : aig.RefVec len) (rhs : aig.RefVec len) (f : (aig : Std.Sat.AIG α) → aig.BinaryInputStd.Sat.AIG.Entrypoint α) [Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.BinaryInput f] [chainable : Std.Sat.AIG.RefVec.LawfulZipOperator α f] (idx : Nat) (hidx : idx < curr) (hfoo : aig.decls.size (Std.Sat.AIG.RefVec.zip.go aig curr s hcurr lhs rhs f).aig.decls.size) :
          (Std.Sat.AIG.RefVec.zip.go aig curr s hcurr lhs rhs f).vec.get idx = (s.get idx hidx).cast hfoo
          theorem Std.Sat.AIG.RefVec.zip.go_get {α : Type} [Hashable α] [DecidableEq α] {len : Nat} {aig : Std.Sat.AIG α} (curr : Nat) (hcurr : curr len) (s : aig.RefVec curr) (lhs : aig.RefVec len) (rhs : aig.RefVec len) (f : (aig : Std.Sat.AIG α) → aig.BinaryInputStd.Sat.AIG.Entrypoint α) [Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.BinaryInput f] [chainable : Std.Sat.AIG.RefVec.LawfulZipOperator α f] (idx : Nat) (hidx : idx < curr) :
          (Std.Sat.AIG.RefVec.zip.go aig curr s hcurr lhs rhs f).vec.get idx = (s.get idx hidx).cast
          theorem Std.Sat.AIG.RefVec.zip.go_denote_mem_prefix {α : Type} [Hashable α] [DecidableEq α] {len : Nat} {assign : αBool} {aig : Std.Sat.AIG α} (curr : Nat) (hcurr : curr len) (s : aig.RefVec curr) (lhs : aig.RefVec len) (rhs : aig.RefVec len) (f : (aig : Std.Sat.AIG α) → aig.BinaryInputStd.Sat.AIG.Entrypoint α) [Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.BinaryInput f] [chainable : Std.Sat.AIG.RefVec.LawfulZipOperator α f] (start : Nat) (hstart : start < aig.decls.size) :
          assign, { aig := (Std.Sat.AIG.RefVec.zip.go aig curr s hcurr lhs rhs f).aig, ref := { gate := start, hgate := } } = assign, { aig := aig, ref := { gate := start, hgate := hstart } }
          @[irreducible]
          theorem Std.Sat.AIG.RefVec.zip.denote_go {α : Type} [Hashable α] [DecidableEq α] {len : Nat} {assign : αBool} {aig : Std.Sat.AIG α} (curr : Nat) (hcurr : curr len) (s : aig.RefVec curr) (lhs : aig.RefVec len) (rhs : aig.RefVec len) (f : (aig : Std.Sat.AIG α) → aig.BinaryInputStd.Sat.AIG.Entrypoint α) [Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.BinaryInput f] [chainable : Std.Sat.AIG.RefVec.LawfulZipOperator α f] (idx : Nat) (hidx1 : idx < len) :
          curr idxassign, { aig := (Std.Sat.AIG.RefVec.zip.go aig curr s hcurr lhs rhs f).aig, ref := (Std.Sat.AIG.RefVec.zip.go aig curr s hcurr lhs rhs f).vec.get idx hidx1 } = assign, f aig { lhs := lhs.get idx hidx1, rhs := rhs.get idx hidx1 }
          @[simp]
          theorem Std.Sat.AIG.RefVec.denote_zip {α : Type} [Hashable α] [DecidableEq α] {len : Nat} {assign : αBool} {aig : Std.Sat.AIG α} (target : Std.Sat.AIG.RefVec.ZipTarget aig len) (idx : Nat) (hidx : idx < len) :
          assign, { aig := (Std.Sat.AIG.RefVec.zip aig target).aig, ref := (Std.Sat.AIG.RefVec.zip aig target).vec.get idx hidx } = assign, target.func aig { lhs := target.input.lhs.get idx hidx, rhs := target.input.rhs.get idx hidx }