def Std.Sat.AIG.Decl.relabel {α : Type} {β : Type} (r : α → β) (decl : Std.Sat.AIG.Decl α) : Std.Sat.AIG.Decl β

Equations

• Std.Sat.AIG.Decl.relabel r (Std.Sat.AIG.Decl.const b) = Std.Sat.AIG.Decl.const b
• Std.Sat.AIG.Decl.relabel r (Std.Sat.AIG.Decl.atom a) = Std.Sat.AIG.Decl.atom (r a)
• Std.Sat.AIG.Decl.relabel r (Std.Sat.AIG.Decl.gate lhs rhs linv rinv) = Std.Sat.AIG.Decl.gate lhs rhs linv rinv

theorem Std.Sat.AIG.Decl.relabel_id_map {α : Type} (decl : Std.Sat.AIG.Decl α) : Std.Sat.AIG.Decl.relabel id decl = decl

theorem Std.Sat.AIG.Decl.relabel_comp {α : Type} {β : Type} {γ : Type} (decl : Std.Sat.AIG.Decl α) (g : α → β) (h : β → γ) : Std.Sat.AIG.Decl.relabel (h ∘ g) decl = Std.Sat.AIG.Decl.relabel h (Std.Sat.AIG.Decl.relabel g decl)

theorem Std.Sat.AIG.Decl.relabel_const {α : Type} {β : Type} {idx : Nat} {b : Bool} {decls : Array (Std.Sat.AIG.Decl α)} {r : α → β} {hidx : idx < decls.size} (h : Std.Sat.AIG.Decl.relabel r decls[idx] = Std.Sat.AIG.Decl.const b) : decls[idx] = Std.Sat.AIG.Decl.const b

theorem Std.Sat.AIG.Decl.relabel_atom {α : Type} {β : Type} {idx : Nat} {a : β} {decls : Array (Std.Sat.AIG.Decl α)} {r : α → β} {hidx : idx < decls.size} (h : Std.Sat.AIG.Decl.relabel r decls[idx] = Std.Sat.AIG.Decl.atom a) : ∃ (x : α), decls[idx] = Std.Sat.AIG.Decl.atom x ∧ a = r x

theorem Std.Sat.AIG.Decl.relabel_gate {α : Type} {β : Type} {idx : Nat} {lhs : Nat} {rhs : Nat} {linv : Bool} {rinv : Bool} {decls : Array (Std.Sat.AIG.Decl α)} {r : α → β} {hidx : idx < decls.size} (h : Std.Sat.AIG.Decl.relabel r decls[idx] = Std.Sat.AIG.Decl.gate lhs rhs linv rinv) : decls[idx] = Std.Sat.AIG.Decl.gate lhs rhs linv rinv

def Std.Sat.AIG.relabel {α : Type} [Hashable α] [DecidableEq α] {β : Type} [Hashable β] [DecidableEq β] (r : α → β) (aig : Std.Sat.AIG α) : Std.Sat.AIG β

Equations

• Std.Sat.AIG.relabel r aig = { decls := Array.map (Std.Sat.AIG.Decl.relabel r) aig.decls, cache := Std.Sat.AIG.Cache.empty (Array.map (Std.Sat.AIG.Decl.relabel r) aig.decls), invariant := ⋯ }

@[simp]

theorem Std.Sat.AIG.relabel_size_eq_size {α : Type} [Hashable α] [DecidableEq α] {β : Type} [Hashable β] [DecidableEq β] {aig : Std.Sat.AIG α} {r : α → β} : (Std.Sat.AIG.relabel r aig).decls.size = aig.decls.size

theorem Std.Sat.AIG.relabel_const {α : Type} [Hashable α] [DecidableEq α] {β : Type} [Hashable β] [DecidableEq β] {idx : Nat} {b : Bool} {aig : Std.Sat.AIG α} {r : α → β} {hidx : idx < (Std.Sat.AIG.relabel r aig).decls.size} (h : (Std.Sat.AIG.relabel r aig).decls[idx] = Std.Sat.AIG.Decl.const b) : aig.decls[idx] = Std.Sat.AIG.Decl.const b

theorem Std.Sat.AIG.relabel_atom {α : Type} [Hashable α] [DecidableEq α] {β : Type} [Hashable β] [DecidableEq β] {idx : Nat} {a : β} {aig : Std.Sat.AIG α} {r : α → β} {hidx : idx < (Std.Sat.AIG.relabel r aig).decls.size} (h : (Std.Sat.AIG.relabel r aig).decls[idx] = Std.Sat.AIG.Decl.atom a) : ∃ (x : α), aig.decls[idx] = Std.Sat.AIG.Decl.atom x ∧ a = r x

theorem Std.Sat.AIG.relabel_gate {α : Type} [Hashable α] [DecidableEq α] {β : Type} [Hashable β] [DecidableEq β] {idx : Nat} {lhs : Nat} {rhs : Nat} {linv : Bool} {rinv : Bool} {aig : Std.Sat.AIG α} {r : α → β} {hidx : idx < (Std.Sat.AIG.relabel r aig).decls.size} (h : (Std.Sat.AIG.relabel r aig).decls[idx] = Std.Sat.AIG.Decl.gate lhs rhs linv rinv) : aig.decls[idx] = Std.Sat.AIG.Decl.gate lhs rhs linv rinv

@[simp, irreducible]

theorem Std.Sat.AIG.denote_relabel {α : Type} [Hashable α] [DecidableEq α] {β : Type} [Hashable β] [DecidableEq β] (aig : Std.Sat.AIG α) (r : α → β) (start : Nat) {hidx : start < (Std.Sat.AIG.relabel r aig).decls.size} (assign : β → Bool) : ⟦assign, { aig := Std.Sat.AIG.relabel r aig, ref := { gate := start, hgate := hidx } }⟧ = ⟦assign ∘ r, { aig := aig, ref := { gate := start, hgate := ⋯ } }⟧

theorem Std.Sat.AIG.unsat_relabel {α : Type} [Hashable α] [DecidableEq α] {β : Type} [Hashable β] [DecidableEq β] {idx : Nat} {aig : Std.Sat.AIG α} (r : α → β) {hidx : idx < aig.decls.size} : aig.UnsatAt idx hidx → (Std.Sat.AIG.relabel r aig).UnsatAt idx ⋯

theorem Std.Sat.AIG.relabel_unsat_iff {α : Type} [Hashable α] [DecidableEq α] {β : Type} [Hashable β] [DecidableEq β] {idx : Nat} [Nonempty α] {aig : Std.Sat.AIG α} {r : α → β} {hidx1 : idx < (Std.Sat.AIG.relabel r aig).decls.size} {hidx2 : idx < aig.decls.size} (hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → r x = r y → x = y) : (Std.Sat.AIG.relabel r aig).UnsatAt idx hidx1 ↔ aig.UnsatAt idx hidx2

def Std.Sat.AIG.Entrypoint.relabel {α : Type} [Hashable α] [DecidableEq α] {β : Type} [Hashable β] [DecidableEq β] (r : α → β) (entry : Std.Sat.AIG.Entrypoint α) : Std.Sat.AIG.Entrypoint β

Equations

• Std.Sat.AIG.Entrypoint.relabel r entry = { aig := Std.Sat.AIG.relabel r entry.aig, ref := let __src := entry.ref; { gate := __src.gate, hgate := ⋯ } }

@[simp]

theorem Std.Sat.AIG.Entrypoint.relabel_size_eq {α : Type} [Hashable α] [DecidableEq α] {β : Type} [Hashable β] [DecidableEq β] {entry : Std.Sat.AIG.Entrypoint α} {r : α → β} : (Std.Sat.AIG.Entrypoint.relabel r entry).aig.decls.size = entry.aig.decls.size

theorem Std.Sat.AIG.Entrypoint.relabel_unsat_iff {α : Type} [Hashable α] [DecidableEq α] {β : Type} [Hashable β] [DecidableEq β] [Nonempty α] {entry : Std.Sat.AIG.Entrypoint α} {r : α → β} (hinj : ∀ (x y : α), x ∈ entry.aig → y ∈ entry.aig → r x = r y → x = y) : (Std.Sat.AIG.Entrypoint.relabel r entry).Unsat ↔ entry.Unsat