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

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

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

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

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

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

def Std.Sat.AIG.relabel {α : Type} [Hashable α] [DecidableEq α] {β : Type} [Hashable β] [DecidableEq β] (r : α → β) (aig : AIG α) (hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → r x = r y → x = y) : AIG β

Relabel the atoms of aig with r. To enforce sharing of the atoms r must be injective.

Equations

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

@[simp]

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

theorem Std.Sat.AIG.relabel_false {α : Type} [Hashable α] [DecidableEq α] {β : Type} [Hashable β] [DecidableEq β] {idx : Nat} {aig : AIG α} {r : α → β} {hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → r x = r y → x = y} {hidx : idx < (relabel r aig hinj).decls.size} (h : (relabel r aig hinj).decls[idx] = Decl.false) : aig.decls[idx] = Decl.false

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

theorem Std.Sat.AIG.relabel_gate {α : Type} [Hashable α] [DecidableEq α] {β : Type} [Hashable β] [DecidableEq β] {idx : Nat} {lhs rhs : Fanin} {aig : AIG α} {r : α → β} {hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → r x = r y → x = y} {hidx : idx < (relabel r aig hinj).decls.size} (h : (relabel r aig hinj).decls[idx] = Decl.gate lhs rhs) : aig.decls[idx] = Decl.gate lhs rhs

@[simp]

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

theorem Std.Sat.AIG.unsat_relabel {α : Type} [Hashable α] [DecidableEq α] {β : Type} [Hashable β] [DecidableEq β] {idx : Nat} {invert : Bool} {aig : AIG α} (r : α → β) {hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → r x = r y → x = y} {hidx : idx < aig.decls.size} : aig.UnsatAt idx invert hidx → (relabel r aig hinj).UnsatAt idx invert ⋯

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

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

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

relabel preserves unsatisfiablility.

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

Equations

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

@[simp]

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

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