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

- Std.Sat.AIG.Decl.relabel r Std.Sat.AIG.Decl.false = Std.Sat.AIG.Decl.false
- 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) = Std.Sat.AIG.Decl.gate lhs rhs

Instances For

source
theorem Std.Sat.AIG.Decl.relabel_id_map {α : Type} (decl : Decl α) :
relabel id decl = decl
source
theorem Std.Sat.AIG.Decl.relabel_comp {α β γ : Type} (decl : Decl α) (g : α → β) (h : β → γ) :
relabel (h ∘ g) decl = relabel h (relabel g decl)
source
theorem Std.Sat.AIG.Decl.relabel_false {α β : Type} {idx : Nat} {decls : Array (Decl α)} {r : α → β} {hidx : idx < decls.size} (h : relabel r decls[idx] = false) :
decls[idx] = false
source
theorem Std.Sat.AIG.Decl.relabel_atom {α β : Type} {idx : Nat} {a : β} {decls : Array (Decl α)} {r : α → β} {hidx : idx < decls.size} (h : relabel r decls[idx] = atom a) :
∃ (x : α), decls[idx] = atom x ∧ a = r x
source
theorem Std.Sat.AIG.Decl.relabel_gate {α β : Type} {idx : Nat} {lhs rhs : Fanin} {decls : Array (Decl α)} {r : α → β} {hidx : idx < decls.size} (h : relabel r decls[idx] = gate lhs rhs) :
decls[idx] = gate lhs rhs
source
def Std.Sat.AIG.relabel {α : Type} [Hashable α] [DecidableEq α] {β : Type} [Hashable β] [DecidableEq β] (r : α → β) (aig : AIG α) :
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, hdag := ⋯, hzero := ⋯, hconst := ⋯ }

Instances For

source
@[simp]
theorem Std.Sat.AIG.relabel_size_eq_size {α : Type} [Hashable α] [DecidableEq α] {β : Type} [Hashable β] [DecidableEq β] {aig : AIG α} {r : α → β} :
(relabel r aig).decls.size = aig.decls.size
source
theorem Std.Sat.AIG.relabel_false {α : Type} [Hashable α] [DecidableEq α] {β : Type} [Hashable β] [DecidableEq β] {idx : Nat} {aig : AIG α} {r : α → β} {hidx : idx < (relabel r aig).decls.size} (h : (relabel r aig).decls[idx] = Decl.false) :
aig.decls[idx] = Decl.false
source
theorem Std.Sat.AIG.relabel_atom {α : Type} [Hashable α] [DecidableEq α] {β : Type} [Hashable β] [DecidableEq β] {idx : Nat} {a : β} {aig : AIG α} {r : α → β} {hidx : idx < (relabel r aig).decls.size} (h : (relabel r aig).decls[idx] = Decl.atom a) :
∃ (x : α), aig.decls[idx] = Decl.atom x ∧ a = r x
source
theorem Std.Sat.AIG.relabel_gate {α : Type} [Hashable α] [DecidableEq α] {β : Type} [Hashable β] [DecidableEq β] {idx : Nat} {lhs rhs : Fanin} {aig : AIG α} {r : α → β} {hidx : idx < (relabel r aig).decls.size} (h : (relabel r aig).decls[idx] = Decl.gate lhs rhs) :
aig.decls[idx] = Decl.gate lhs rhs
source
@[simp, irreducible]
theorem Std.Sat.AIG.denote_relabel {α : Type} [Hashable α] [DecidableEq α] {β : Type} [Hashable β] [DecidableEq β] {invert : Bool} (aig : AIG α) (r : α → β) (start : Nat) {hidx : start < (relabel r aig).decls.size} (assign : β → Bool) :
⟦assign, { aig := relabel r aig, ref := { gate := start, invert := invert, hgate := hidx } }⟧ = ⟦assign ∘ r, { aig := aig, ref := { gate := start, invert := invert, hgate := ⋯ } }⟧
source
theorem Std.Sat.AIG.unsat_relabel {α : Type} [Hashable α] [DecidableEq α] {β : Type} [Hashable β] [DecidableEq β] {idx : Nat} {invert : Bool} {aig : AIG α} (r : α → β) {hidx : idx < aig.decls.size} :
aig.UnsatAt idx invert hidx → (relabel r aig).UnsatAt idx invert ⋯
source
theorem Std.Sat.AIG.relabel_unsat_iff_of_not_Nonempty {α : Type} [Hashable α] [DecidableEq α] {β : Type} [Hashable β] [DecidableEq β] {idx : Nat} {invert : Bool} {aig : AIG α} {r : α → β} {hidx1 : idx < (relabel r aig).decls.size} {hidx2 : idx < aig.decls.size} (hNonempty : ¬Nonempty α) :
(relabel r aig).UnsatAt idx invert hidx1 ↔ aig.UnsatAt idx invert hidx2
source
theorem Std.Sat.AIG.relabel_unsat_iff_of_Nonempty {α : Type} [Hashable α] [DecidableEq α] {β : Type} [Hashable β] [DecidableEq β] {idx : Nat} {invert : Bool} [Nonempty α] {aig : AIG α} {r : α → β} {hidx1 : idx < (relabel r aig).decls.size} {hidx2 : idx < aig.decls.size} (hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → r x = r y → x = y) :
(relabel r aig).UnsatAt idx invert hidx1 ↔ aig.UnsatAt idx invert hidx2
source
theorem Std.Sat.AIG.relabel_unsat_iff {α : Type} [Hashable α] [DecidableEq α] {β : Type} [Hashable β] [DecidableEq β] {idx : Nat} {invert : Bool} {aig : AIG α} {r : α → β} {hidx1 : idx < (relabel r aig).decls.size} {hidx2 : idx < aig.decls.size} (hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → r x = r y → x = y) :
(relabel r aig).UnsatAt idx invert hidx1 ↔ aig.UnsatAt idx invert hidx2

`relabel` preserves unsatisfiablility.

source
def Std.Sat.AIG.Entrypoint.relabel {α : Type} [Hashable α] [DecidableEq α] {β : Type} [Hashable β] [DecidableEq β] (r : α → β) (entry : Entrypoint α) :
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, invert := __src.invert, hgate := ⋯ } }

Instances For

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