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
Instances For
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}
(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}
{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}
{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}
{idx lhs rhs : Nat}
{linv 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 α)
:
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 := ⋯ }
Instances For
@[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 lhs rhs : Nat}
{linv 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 α)
:
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 := ⋯ } }
Instances For
@[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