Std.Sat.AIG.RefVec

source

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

aig.RefVec 0

Equations

Std.Sat.AIG.RefVec.empty = { refs := { toArray := #[], size_toArray := Std.Sat.AIG.RefVec.empty._proof_1 }, hrefs := ⋯ }

Instances For

source

def Std.Sat.AIG.RefVec.emptyWithCapacity {α : Type} [Hashable α] [DecidableEq α] {aig : AIG α} (c : Nat) :

aig.RefVec 0

Equations

Std.Sat.AIG.RefVec.emptyWithCapacity c = { refs := Vector.emptyWithCapacity c, hrefs := ⋯ }

Instances For

source

@[simp]

theorem Std.Sat.AIG.RefVec.emptyWithCapacity_eq {α : Type} [Hashable α] [DecidableEq α] {aig : AIG α} {c : Nat} :

emptyWithCapacity c = empty

source

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

s.cast' h = { refs := s.refs, hrefs := ⋯ }

Instances For

source

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

Instances For

source

@[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, hrefs := hrefs }.get idx hidx = { gate := refs[idx].gate, invert := refs[idx].invert, hgate := ⋯ }

Instances For

source

@[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, hrefs := hrefs }.push ref = { refs := refs.push (Std.Sat.AIG.Fanin.mk ref.gate ref.invert), hrefs := ⋯ }

Instances For

source

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

source

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

source

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

source

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

source

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

source

@[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, hrefs := hrefs }.append { refs := refs_1, hrefs := hrefs_1 } = { refs := refs ++ refs_1, hrefs := ⋯ }

Instances For

source

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) ⋯

source

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

Instances For

source

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

source

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

source

def Std.Sat.AIG.RefVec.countKnown {α : Type} [Hashable α] [DecidableEq α] {len : Nat} (aig : AIG α) (s : aig.RefVec len) :

Nat

Equations

Std.Sat.AIG.RefVec.countKnown aig s = Std.Sat.AIG.RefVec.countKnown.go aig s 0 0

Instances For

source

@[irreducible]

def Std.Sat.AIG.RefVec.countKnown.go {α : Type} [Hashable α] [DecidableEq α] {len : Nat} (aig : AIG α) (s : aig.RefVec len) (idx acc : Nat) :

Nat

Equations

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

Instances For

source

structure Std.Sat.AIG.BinaryRefVec {α : Type} [Hashable α] [DecidableEq α] (aig : 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 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 }

Instances For

source

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

source

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