Std.Sat.AIG.Relabel

source

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

Decl β

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 β

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 β

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