Documentation

Std.Sat.AIG.RefVec

source
def Std.Sat.AIG.RefVec.empty {α : Type} [Hashable α] [DecidableEq α] {aig : Std.Sat.AIG α} :
aig.RefVec 0
Equations
Instances For
    source
    @[inline]
    def Std.Sat.AIG.RefVec.cast' {α : Type} [Hashable α] [DecidableEq α] {len : Nat} {aig1 : Std.Sat.AIG α} {aig2 : Std.Sat.AIG α} (s : aig1.RefVec len) (h : (∀ {i : Nat} (h : i < len), s.refs[i] < aig1.decls.size) → ∀ {i : Nat} (h : i < len), s.refs[i] < aig2.decls.size) :
    aig2.RefVec len
    Equations
    • s.cast' h = { refs := s.refs, hlen := ⋯, hrefs := ⋯ }
    Instances For
      source
      @[inline]
      def Std.Sat.AIG.RefVec.cast {α : Type} [Hashable α] [DecidableEq α] {len : Nat} {aig1 : Std.Sat.AIG α} {aig2 : Std.Sat.AIG α} (s : aig1.RefVec len) (h : aig1.decls.size ≤ aig2.decls.size) :
      aig2.RefVec len
      Equations
      • s.cast h = s.cast' ⋯
      Instances For
        source
        @[inline]
        def Std.Sat.AIG.RefVec.get {α : Type} [Hashable α] [DecidableEq α] {aig : Std.Sat.AIG α} {len : Nat} (s : aig.RefVec len) (idx : Nat) (hidx : idx < len) :
        aig.Ref
        Equations
        • { refs := refs, hlen := hlen, hrefs := hrefs }.get idx hidx = { gate := refs[idx], hgate := ⋯ }
        Instances For
          source
          @[inline]
          def Std.Sat.AIG.RefVec.push {α : Type} [Hashable α] [DecidableEq α] {aig : Std.Sat.AIG α} {len : Nat} (s : aig.RefVec len) (ref : aig.Ref) :
          aig.RefVec (len + 1)
          Equations
          • { refs := refs, hlen := hlen, hrefs := hrefs }.push ref = { refs := refs.push ref.gate, hlen := ⋯, hrefs := ⋯ }
          Instances For
            source
            @[simp]
            theorem Std.Sat.AIG.RefVec.get_push_ref_eq {α : Type} [Hashable α] [DecidableEq α] {aig : Std.Sat.AIG α} {len : Nat} (s : aig.RefVec len) (ref : aig.Ref) :
            (s.push ref).get len ⋯ = ref
            source
            theorem Std.Sat.AIG.RefVec.get_push_ref_eq' {α : Type} [Hashable α] [DecidableEq α] {aig : Std.Sat.AIG α} {len : Nat} (s : aig.RefVec len) (ref : aig.Ref) (idx : Nat) (hidx : idx = len) :
            (s.push ref).get idx ⋯ = ref
            source
            theorem Std.Sat.AIG.RefVec.get_push_ref_lt {α : Type} [Hashable α] [DecidableEq α] {aig : Std.Sat.AIG α} {len : Nat} (s : aig.RefVec len) (ref : aig.Ref) (idx : Nat) (hidx : idx < len) :
            (s.push ref).get idx ⋯ = s.get idx hidx
            source
            @[simp]
            theorem Std.Sat.AIG.RefVec.get_cast {α : Type} [Hashable α] [DecidableEq α] {len : Nat} {aig1 : Std.Sat.AIG α} {aig2 : Std.Sat.AIG α} (s : aig1.RefVec len) (idx : Nat) (hidx : idx < len) (hcast : aig1.decls.size ≤ aig2.decls.size) :
            (s.cast hcast).get idx hidx = (s.get idx hidx).cast hcast
            source
            @[inline]
            def Std.Sat.AIG.RefVec.append {α : Type} [Hashable α] [DecidableEq α] {aig : Std.Sat.AIG α} {lw : Nat} {rw : Nat} (lhs : aig.RefVec lw) (rhs : aig.RefVec rw) :
            aig.RefVec (lw + rw)
            Equations
            • { refs := refs, hlen := hlen, hrefs := hrefs }.append { refs := refs_1, hlen := hlen_1, hrefs := hrefs_1 } = { refs := refs ++ refs_1, hlen := ⋯, hrefs := ⋯ }
            Instances For
              source
              theorem Std.Sat.AIG.RefVec.get_append {α : Type} [Hashable α] [DecidableEq α] {aig : Std.Sat.AIG α} {lw : Nat} {rw : Nat} (lhs : aig.RefVec lw) (rhs : aig.RefVec rw) (idx : Nat) (hidx : idx < lw + rw) :
              (lhs.append rhs).get idx hidx = if h : idx < lw then lhs.get idx h else rhs.get (idx - lw) ⋯
              source
              @[inline]
              def Std.Sat.AIG.RefVec.getD {α : Type} [Hashable α] [DecidableEq α] {aig : Std.Sat.AIG α} {len : Nat} (s : aig.RefVec len) (idx : Nat) (alt : aig.Ref) :
              aig.Ref
              Equations
              • s.getD idx alt = if hidx : idx < len then s.get idx hidx else alt
              Instances For
                source
                theorem Std.Sat.AIG.RefVec.get_in_bound {α : Type} [Hashable α] [DecidableEq α] {aig : Std.Sat.AIG α} {len : Nat} (s : aig.RefVec len) (idx : Nat) (alt : aig.Ref) (hidx : idx < len) :
                s.getD idx alt = s.get idx hidx
                source
                theorem Std.Sat.AIG.RefVec.get_out_bound {α : Type} [Hashable α] [DecidableEq α] {aig : Std.Sat.AIG α} {len : Nat} (s : aig.RefVec len) (idx : Nat) (alt : aig.Ref) (hidx : len ≤ idx) :
                s.getD idx alt = alt
                source
                structure Std.Sat.AIG.BinaryRefVec {α : Type} [Hashable α] [DecidableEq α] (aig : Std.Sat.AIG α) (len : Nat) :
                Type
                • lhs : aig.RefVec len
                • rhs : aig.RefVec len
                Instances For
                  source
                  @[inline]
                  def Std.Sat.AIG.BinaryRefVec.cast {α : Type} [Hashable α] [DecidableEq α] {len : Nat} {aig1 : Std.Sat.AIG α} {aig2 : Std.Sat.AIG α} (s : aig1.BinaryRefVec len) (h : aig1.decls.size ≤ aig2.decls.size) :
                  aig2.BinaryRefVec len
                  Equations
                  • { lhs := lhs, rhs := rhs }.cast h = { lhs := lhs.cast h, rhs := rhs.cast h }
                  Instances For
                    source
                    @[simp]
                    theorem Std.Sat.AIG.BinaryRefVec.lhs_get_cast {α : Type} [Hashable α] [DecidableEq α] {len : Nat} {aig1 : Std.Sat.AIG α} {aig2 : Std.Sat.AIG α} (s : aig1.BinaryRefVec len) (idx : Nat) (hidx : idx < len) (hcast : aig1.decls.size ≤ aig2.decls.size) :
                    (s.cast hcast).lhs.get idx hidx = (s.lhs.get idx hidx).cast hcast
                    source
                    @[simp]
                    theorem Std.Sat.AIG.BinaryRefVec.rhs_get_cast {α : Type} [Hashable α] [DecidableEq α] {len : Nat} {aig1 : Std.Sat.AIG α} {aig2 : Std.Sat.AIG α} (s : aig1.BinaryRefVec len) (idx : Nat) (hidx : idx < len) (hcast : aig1.decls.size ≤ aig2.decls.size) :
                    (s.cast hcast).rhs.get idx hidx = (s.rhs.get idx hidx).cast hcast