def Std.Sat.AIG.RefVec.empty {α : Type} [Hashable α] [DecidableEq α] {aig : AIG α} : aig.RefVec 0

Equations

• Std.Sat.AIG.RefVec.empty = { refs := #[], hlen := Std.Sat.AIG.RefVec.empty.proof_1, hrefs := ⋯ }

@[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] < 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 := ⋯ }

@[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

• s.cast h = s.cast' ⋯

@[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

• { refs := refs, hlen := hlen, hrefs := hrefs }.get idx hidx = { gate := refs[idx], hgate := ⋯ }

@[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

• { refs := refs, hlen := hlen, hrefs := hrefs }.push ref = { refs := refs.push ref.gate, hlen := ⋯, hrefs := ⋯ }

@[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

• { refs := refs, hlen := hlen, hrefs := hrefs }.append { refs := refs_1, hlen := hlen_1, hrefs := hrefs_1 } = { refs := refs ++ refs_1, hlen := ⋯, hrefs := ⋯ }

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

• s.getD idx alt = if hidx : idx < len then s.get idx hidx else alt

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} [Inhabited α] (aig : AIG α) (s : aig.RefVec len) : Nat

Equations

• One or more equations did not get rendered due to their size.

structure Std.Sat.AIG.BinaryRefVec {α : Type} [Hashable α] [DecidableEq α] (aig : AIG α) (len : Nat) : Type

• lhs : aig.RefVec len
• rhs : aig.RefVec len

Instances For

• Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd.instLawfulVecOperatorBinaryRefVec
• Std.Tactic.BVDecide.BVExpr.bitblast.blastMul.instLawfulVecOperatorBVBitBinaryRefVecBlast
• Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorBVBitBinaryRefVecBlastMul
• Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorBinaryRefVecBlastSub
• Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorBinaryRefVecBlastUdiv
• Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorBinaryRefVecBlastUmod

@[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

• { lhs := lhs, rhs := rhs }.cast h = { lhs := lhs.cast h, rhs := rhs.cast h }

@[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