inductive Std.Sat.AIG.RelabelNat.State.Inv1 {α : Type} [DecidableEq α] [Hashable α] : Nat → Std.HashMap α Nat → Prop

This invariant ensures that we only insert an atom at most once and with a monotonically increasing index.

• empty: ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Hashable α], Std.Sat.AIG.RelabelNat.State.Inv1 0 ∅
• insert: ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Hashable α] {n : Nat} {map : Std.HashMap α Nat} {x : α}, Std.Sat.AIG.RelabelNat.State.Inv1 n map → map[x]? = none → Std.Sat.AIG.RelabelNat.State.Inv1 (n + 1) (map.insert x n)

theorem Std.Sat.AIG.RelabelNat.State.Inv1.lt_of_get?_eq_some {α : Type} [DecidableEq α] [Hashable α] [EquivBEq α] {n m : Nat} (map : Std.HashMap α Nat) (x : α) (hinv : Std.Sat.AIG.RelabelNat.State.Inv1 n map) : map[x]? = some m → m < n

theorem Std.Sat.AIG.RelabelNat.State.Inv1.property {α : Type} [DecidableEq α] [Hashable α] [EquivBEq α] {n m : Nat} (x y : α) (map : Std.HashMap α Nat) (hinv : Std.Sat.AIG.RelabelNat.State.Inv1 n map) (hfound1 : map[x]? = some m) (hfound2 : map[y]? = some m) : x = y

If a HashMap fulfills Inv1 it is in an injection.

inductive Std.Sat.AIG.RelabelNat.State.Inv2 {α : Type} [DecidableEq α] [Hashable α] (decls : Array (Std.Sat.AIG.Decl α)) : Nat → Std.HashMap α Nat → Prop

This invariant says that we have already visited and inserted all nodes up to a certain index.

• empty: ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Hashable α] {decls : Array (Std.Sat.AIG.Decl α)}, Std.Sat.AIG.RelabelNat.State.Inv2 decls 0 ∅
• newAtom: ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Hashable α] {decls : Array (Std.Sat.AIG.Decl α)} {idx : Nat} {map : Std.HashMap α Nat} {a : α} {val : Nat}, Std.Sat.AIG.RelabelNat.State.Inv2 decls idx map → ∀ (hlt : idx < decls.size), decls[idx] = Std.Sat.AIG.Decl.atom a → map[a]? = none → Std.Sat.AIG.RelabelNat.State.Inv2 decls (idx + 1) (map.insert a val)
• oldAtom: ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Hashable α] {decls : Array (Std.Sat.AIG.Decl α)} {idx : Nat} {map : Std.HashMap α Nat} {a : α} {n : Nat}, Std.Sat.AIG.RelabelNat.State.Inv2 decls idx map → ∀ (hlt : idx < decls.size), decls[idx] = Std.Sat.AIG.Decl.atom a → map[a]? = some n → Std.Sat.AIG.RelabelNat.State.Inv2 decls (idx + 1) map
• const: ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Hashable α] {decls : Array (Std.Sat.AIG.Decl α)} {idx : Nat} {map : Std.HashMap α Nat} {b : Bool}, Std.Sat.AIG.RelabelNat.State.Inv2 decls idx map → ∀ (hlt : idx < decls.size), decls[idx] = Std.Sat.AIG.Decl.const b → Std.Sat.AIG.RelabelNat.State.Inv2 decls (idx + 1) map
• gate: ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Hashable α] {decls : Array (Std.Sat.AIG.Decl α)} {idx : Nat} {map : Std.HashMap α Nat} {l r : Nat} {li ri : Bool}, Std.Sat.AIG.RelabelNat.State.Inv2 decls idx map → ∀ (hlt : idx < decls.size), decls[idx] = Std.Sat.AIG.Decl.gate l r li ri → Std.Sat.AIG.RelabelNat.State.Inv2 decls (idx + 1) map

theorem Std.Sat.AIG.RelabelNat.State.Inv2.upper_lt_size {α : Type} [DecidableEq α] [Hashable α] {upper : Nat} {map : Std.HashMap α Nat} {decls : Array (Std.Sat.AIG.Decl α)} (hinv : Std.Sat.AIG.RelabelNat.State.Inv2 decls upper map) : upper ≤ decls.size

theorem Std.Sat.AIG.RelabelNat.State.Inv2.property {α : Type} [DecidableEq α] [Hashable α] (decls : Array (Std.Sat.AIG.Decl α)) (idx upper : Nat) (map : Std.HashMap α Nat) (hidx : idx < upper) (a : α) (hinv : Std.Sat.AIG.RelabelNat.State.Inv2 decls upper map) (heq : decls[idx] = Std.Sat.AIG.Decl.atom a) : ∃ (n : Nat), map[a]? = some n

The key property provided by Inv2, if we have Inv2 at a certain index, then all atoms below that index have been inserted into the HashMap.

structure Std.Sat.AIG.RelabelNat.State (α : Type) [DecidableEq α] [Hashable α] (decls : Array (Std.Sat.AIG.Decl α)) (idx : Nat) : Type

The invariant carrying state structure for building the HashMap that translates from arbitrary atom identifiers to Nat.

• max : Nat

  The next number to use for identifying an atom.

• map : Std.HashMap α Nat

  The translation HashMap

• inv1 : Std.Sat.AIG.RelabelNat.State.Inv1 self.max self.map

  Proof that we never reuse a number.

• inv2 : Std.Sat.AIG.RelabelNat.State.Inv2 decls idx self.map

  Proof that we inserted all atoms until idx.

def Std.Sat.AIG.RelabelNat.State.empty {α : Type} [DecidableEq α] [Hashable α] {decls : Array (Std.Sat.AIG.Decl α)} : Std.Sat.AIG.RelabelNat.State α decls 0

The basic initial state.

Equations

• Std.Sat.AIG.RelabelNat.State.empty = { max := 0, map := ∅, inv1 := ⋯, inv2 := ⋯ }

def Std.Sat.AIG.RelabelNat.State.addAtom {α : Type} [DecidableEq α] [Hashable α] {idx : Nat} {decls : Array (Std.Sat.AIG.Decl α)} {hidx : idx < decls.size} (state : Std.Sat.AIG.RelabelNat.State α decls idx) (a : α) (h : decls[idx] = Std.Sat.AIG.Decl.atom a) : Std.Sat.AIG.RelabelNat.State α decls (idx + 1)

Insert a Decl.atom into the State structure.

Equations

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

def Std.Sat.AIG.RelabelNat.State.addConst {α : Type} [DecidableEq α] [Hashable α] {idx : Nat} {decls : Array (Std.Sat.AIG.Decl α)} {hidx : idx < decls.size} (state : Std.Sat.AIG.RelabelNat.State α decls idx) (b : Bool) (h : decls[idx] = Std.Sat.AIG.Decl.const b) : Std.Sat.AIG.RelabelNat.State α decls (idx + 1)

Insert a Decl.const into the State structure.

Equations

• state.addConst b h = { max := state.max, map := state.map, inv1 := ⋯, inv2 := ⋯ }

def Std.Sat.AIG.RelabelNat.State.addGate {α : Type} [DecidableEq α] [Hashable α] {idx : Nat} {decls : Array (Std.Sat.AIG.Decl α)} {hidx : idx < decls.size} (state : Std.Sat.AIG.RelabelNat.State α decls idx) (lhs rhs : Nat) (linv rinv : Bool) (h : decls[idx] = Std.Sat.AIG.Decl.gate lhs rhs linv rinv) : Std.Sat.AIG.RelabelNat.State α decls (idx + 1)

Insert a Decl.gate into the State structure.

Equations

• state.addGate lhs rhs linv rinv h = { max := state.max, map := state.map, inv1 := ⋯, inv2 := ⋯ }

def Std.Sat.AIG.RelabelNat.State.ofAIGAux {α : Type} [DecidableEq α] [Hashable α] (aig : Std.Sat.AIG α) : Std.Sat.AIG.RelabelNat.State α aig.decls aig.decls.size

Build up a State that has all atoms of an AIG inserted.

Equations

• Std.Sat.AIG.RelabelNat.State.ofAIGAux aig = Std.Sat.AIG.RelabelNat.State.ofAIGAux.go aig.decls 0 Std.Sat.AIG.RelabelNat.State.empty

@[irreducible]

def Std.Sat.AIG.RelabelNat.State.ofAIGAux.go {α : Type} [DecidableEq α] [Hashable α] (decls : Array (Std.Sat.AIG.Decl α)) (idx : Nat) (state : Std.Sat.AIG.RelabelNat.State α decls idx) : Std.Sat.AIG.RelabelNat.State α decls decls.size

Equations

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

def Std.Sat.AIG.RelabelNat.State.ofAIG {α : Type} [DecidableEq α] [Hashable α] (aig : Std.Sat.AIG α) : Std.HashMap α Nat

Obtain the atom mapping from α to Nat for a given AIG.

Equations

• Std.Sat.AIG.RelabelNat.State.ofAIG aig = (Std.Sat.AIG.RelabelNat.State.ofAIGAux aig).map

theorem Std.Sat.AIG.RelabelNat.State.ofAIG.Inv1 {α : Type} [DecidableEq α] [Hashable α] (aig : Std.Sat.AIG α) : ∃ (n : Nat), Std.Sat.AIG.RelabelNat.State.Inv1 n (Std.Sat.AIG.RelabelNat.State.ofAIG aig)

The map returned by ofAIG fulfills the Inv1 property.

theorem Std.Sat.AIG.RelabelNat.State.ofAIG.Inv2 {α : Type} [DecidableEq α] [Hashable α] (aig : Std.Sat.AIG α) : Std.Sat.AIG.RelabelNat.State.Inv2 aig.decls aig.decls.size (Std.Sat.AIG.RelabelNat.State.ofAIG aig)

The map returned by ofAIG fulfills the Inv2 property.

theorem Std.Sat.AIG.RelabelNat.State.ofAIG_find_unique {α : Type} [DecidableEq α] [Hashable α] {n : Nat} {aig : Std.Sat.AIG α} (a : α) (ha : (Std.Sat.AIG.RelabelNat.State.ofAIG aig)[a]? = some n) (a' : α) : (Std.Sat.AIG.RelabelNat.State.ofAIG aig)[a']? = some n → a = a'

Assuming that we find a Nat for an atom in the ofAIG map, that Nat is unique in the map.

theorem Std.Sat.AIG.RelabelNat.State.ofAIG_find_some {α : Type} [DecidableEq α] [Hashable α] {aig : Std.Sat.AIG α} (a : α) : a ∈ aig → ∃ (n : Nat), (Std.Sat.AIG.RelabelNat.State.ofAIG aig)[a]? = some n

We will find a Nat for every atom in the AIG that the ofAIG map was built from.

def Std.Sat.AIG.relabelNat' {α : Type} [DecidableEq α] [Hashable α] (aig : Std.Sat.AIG α) : Std.Sat.AIG Nat × Std.HashMap α Nat

Equations

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

def Std.Sat.AIG.relabelNat {α : Type} [DecidableEq α] [Hashable α] (aig : Std.Sat.AIG α) : Std.Sat.AIG Nat

Map an AIG with arbitrary atom identifiers to one that uses Nat as atom identifiers. This is useful for preparing an AIG for CNF translation if it doesn't already use Nat identifiers.

Equations

• aig.relabelNat = aig.relabelNat'.fst

@[simp]

theorem Std.Sat.AIG.relabelNat'_fst_eq_relabelNat {α : Type} [DecidableEq α] [Hashable α] {aig : Std.Sat.AIG α} : aig.relabelNat'.fst = aig.relabelNat

@[simp]

theorem Std.Sat.AIG.relabelNat_size_eq_size {α : Type} [DecidableEq α] [Hashable α] {aig : Std.Sat.AIG α} : aig.relabelNat.decls.size = aig.decls.size

theorem Std.Sat.AIG.relabelNat_unsat_iff {α : Type} [DecidableEq α] [Hashable α] {idx : Nat} [Nonempty α] {aig : Std.Sat.AIG α} {hidx1 : idx < aig.relabelNat.decls.size} {hidx2 : idx < aig.decls.size} : aig.relabelNat.UnsatAt idx hidx1 ↔ aig.UnsatAt idx hidx2

relabelNat preserves unsatisfiablility.

def Std.Sat.AIG.Entrypoint.relabelNat' {α : Type} [DecidableEq α] [Hashable α] (entry : Std.Sat.AIG.Entrypoint α) : Std.Sat.AIG.Entrypoint Nat × Std.HashMap α Nat

Equations

• entry.relabelNat' = ({ aig := entry.aig.relabelNat'.fst, ref := let __src := entry.ref; { gate := __src.gate, hgate := ⋯ } }, entry.aig.relabelNat'.snd)

def Std.Sat.AIG.Entrypoint.relabelNat {α : Type} [DecidableEq α] [Hashable α] (entry : Std.Sat.AIG.Entrypoint α) : Std.Sat.AIG.Entrypoint Nat

Map an Entrypoint with arbitrary atom identifiers to one that uses Nat as atom identifiers. This is useful for preparing an AIG for CNF translation if it doesn't already use Nat identifiers.

Equations

• entry.relabelNat = { aig := entry.aig.relabelNat, ref := let __src := entry.ref; { gate := __src.gate, hgate := ⋯ } }

theorem Std.Sat.AIG.Entrypoint.relabelNat_unsat_iff {α : Type} [DecidableEq α] [Hashable α] {entry : Std.Sat.AIG.Entrypoint α} [Nonempty α] : entry.relabelNat.Unsat ↔ entry.Unsat

relabelNat preserves unsatisfiablility.