Documentation

Std.Sat.AIG.RefVec

def Std.Sat.AIG.RefVec.empty {α : Type} [Hashable α] [DecidableEq α] {aig : AIG α} :
aig.RefVec 0
Equations
    Instances For
      def Std.Sat.AIG.RefVec.emptyWithCapacity {α : Type} [Hashable α] [DecidableEq α] {aig : AIG α} (c : Nat) :
      aig.RefVec 0
      Equations
        Instances For
          @[inline]
          def Std.Sat.AIG.RefVec.cast' {α : Type} [Hashable α] [DecidableEq α] {len : Nat} {aig1 aig2 : AIG α} (s : aig1.RefVec len) (h : (∀ {i : Nat} (h : i < len), s.refs[i].gate < aig1.decls.size)∀ {i : Nat} (h : i < len), s.refs[i].gate < aig2.decls.size) :
          aig2.RefVec len
          Equations
            Instances For
              @[inline]
              def Std.Sat.AIG.RefVec.cast {α : Type} [Hashable α] [DecidableEq α] {len : Nat} {aig1 aig2 : AIG α} (s : aig1.RefVec len) (h : aig1.decls.size aig2.decls.size) :
              aig2.RefVec len
              Equations
                Instances For
                  @[inline]
                  def Std.Sat.AIG.RefVec.get {α : Type} [Hashable α] [DecidableEq α] {aig : AIG α} {len : Nat} (s : aig.RefVec len) (idx : Nat) (hidx : idx < len) :
                  aig.Ref
                  Equations
                    Instances For
                      @[inline]
                      def Std.Sat.AIG.RefVec.push {α : Type} [Hashable α] [DecidableEq α] {aig : AIG α} {len : Nat} (s : aig.RefVec len) (ref : aig.Ref) :
                      aig.RefVec (len + 1)
                      Equations
                        Instances For
                          @[simp]
                          theorem Std.Sat.AIG.RefVec.cast_cast {α : Type} [Hashable α] [DecidableEq α] {len : Nat} {aig1 aig2 aig3 : AIG α} (s : aig1.RefVec len) (h1 : aig1.decls.size aig2.decls.size) (h2 : aig2.decls.size aig3.decls.size) :
                          (s.cast h1).cast h2 = s.cast
                          @[simp]
                          theorem Std.Sat.AIG.RefVec.get_push_ref_eq {α : Type} [Hashable α] [DecidableEq α] {aig : 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 : 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 : 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 aig2 : 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 : AIG α} {lw rw : Nat} (lhs : aig.RefVec lw) (rhs : aig.RefVec rw) :
                          aig.RefVec (lw + rw)
                          Equations
                            Instances For
                              theorem Std.Sat.AIG.RefVec.get_append {α : Type} [Hashable α] [DecidableEq α] {aig : AIG α} {lw 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 : AIG α} {len : Nat} (s : aig.RefVec len) (idx : Nat) (alt : aig.Ref) :
                              aig.Ref
                              Equations
                                Instances For
                                  theorem Std.Sat.AIG.RefVec.get_in_bound {α : Type} [Hashable α] [DecidableEq α] {aig : 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 : 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} (aig : AIG α) (s : aig.RefVec len) :
                                  Equations
                                    Instances For
                                      @[irreducible]
                                      def Std.Sat.AIG.RefVec.countKnown.go {α : Type} [Hashable α] [DecidableEq α] {len : Nat} (aig : AIG α) (s : aig.RefVec len) (idx acc : Nat) :
                                      Equations
                                        Instances For
                                          structure Std.Sat.AIG.BinaryRefVec {α : Type} [Hashable α] [DecidableEq α] (aig : AIG α) (len : Nat) :
                                          Instances For
                                            @[inline]
                                            def Std.Sat.AIG.BinaryRefVec.cast {α : Type} [Hashable α] [DecidableEq α] {len : Nat} {aig1 aig2 : AIG α} (s : aig1.BinaryRefVec len) (h : aig1.decls.size aig2.decls.size) :
                                            aig2.BinaryRefVec len
                                            Equations
                                              Instances For
                                                @[simp]
                                                theorem Std.Sat.AIG.BinaryRefVec.lhs_get_cast {α : Type} [Hashable α] [DecidableEq α] {len : Nat} {aig1 aig2 : 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 aig2 : 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