Documentation

Std.Sat.AIG.RefVec

def Std.Sat.AIG.RefVec.empty {α : Type} [Hashable α] [DecidableEq α] {aig : Std.Sat.AIG α} :
aig.RefVec 0
Equations
Instances For
    @[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
      @[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
        @[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
          @[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
            @[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
            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
            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
            @[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
            @[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
              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)
              @[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
                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
                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
                def Std.Sat.AIG.RefVec.countKnown {α : Type} [Hashable α] [DecidableEq α] {len : Nat} [Inhabited α] (aig : Std.Sat.AIG α) (s : aig.RefVec len) :
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  structure Std.Sat.AIG.BinaryRefVec {α : Type} [Hashable α] [DecidableEq α] (aig : Std.Sat.AIG α) (len : Nat) :
                  • lhs : aig.RefVec len
                  • rhs : aig.RefVec len
                  Instances For
                    @[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
                      @[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
                      @[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