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

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

- empty {α : Type} [DecidableEq α] [Hashable α] : Inv1 0 ∅
- insert {α : Type} [DecidableEq α] [Hashable α] {n : Nat} {map : HashMap α Nat} {x : α} (hinv : Inv1 n map) (hfind : map[x]? = none) : Inv1 (n + 1) (map.insert x n)

Instances For

source
theorem Std.Sat.AIG.RelabelNat.State.Inv1.lt_of_get?_eq_some {α : Type} [DecidableEq α] [Hashable α] [EquivBEq α] {n m : Nat} (map : HashMap α Nat) (x : α) (hinv : Inv1 n map) :
map[x]? = some m → m < n
source
theorem Std.Sat.AIG.RelabelNat.State.Inv1.property {α : Type} [DecidableEq α] [Hashable α] [EquivBEq α] {n m : Nat} (x y : α) (map : HashMap α Nat) (hinv : 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.

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

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

- empty {α : Type} [DecidableEq α] [Hashable α] {decls : Array (Decl α)} : Inv2 decls 0 ∅
- newAtom {α : Type} [DecidableEq α] [Hashable α] {decls : Array (Decl α)} {idx : Nat} {map : HashMap α Nat} {a : α} {val : Nat} (hinv : Inv2 decls idx map) (hlt : idx < decls.size) (hatom : decls[idx] = Decl.atom a) (hmap : map[a]? = none) : Inv2 decls (idx + 1) (map.insert a val)
- oldAtom {α : Type} [DecidableEq α] [Hashable α] {decls : Array (Decl α)} {idx : Nat} {map : HashMap α Nat} {a : α} {n : Nat} (hinv : Inv2 decls idx map) (hlt : idx < decls.size) (hatom : decls[idx] = Decl.atom a) (hmap : map[a]? = some n) : Inv2 decls (idx + 1) map
- false {α : Type} [DecidableEq α] [Hashable α] {decls : Array (Decl α)} {idx : Nat} {map : HashMap α Nat} (hinv : Inv2 decls idx map) (hlt : idx < decls.size) (hatom : decls[idx] = Decl.false) : Inv2 decls (idx + 1) map
- gate {α : Type} [DecidableEq α] [Hashable α] {decls : Array (Decl α)} {idx : Nat} {map : HashMap α Nat} {l r : Fanin} (hinv : Inv2 decls idx map) (hlt : idx < decls.size) (hatom : decls[idx] = Decl.gate l r) : Inv2 decls (idx + 1) map

Instances For

source
theorem Std.Sat.AIG.RelabelNat.State.Inv2.upper_lt_size {α : Type} [DecidableEq α] [Hashable α] {upper : Nat} {map : HashMap α Nat} {decls : Array (Decl α)} (hinv : Inv2 decls upper map) :
upper ≤ decls.size
source
theorem Std.Sat.AIG.RelabelNat.State.Inv2.property {α : Type} [DecidableEq α] [Hashable α] (decls : Array (Decl α)) (idx upper : Nat) (map : HashMap α Nat) (hidx : idx < upper) (a : α) (hinv : Inv2 decls upper map) (heq : decls[idx] = 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`.

source
structure Std.Sat.AIG.RelabelNat.State (α : Type) [DecidableEq α] [Hashable α] (decls : Array (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 : HashMap α Nat

  The translation `HashMap`

- inv1 : Inv1 self.max self.map

  Proof that we never reuse a number.

- inv2 : Inv2 decls idx self.map

  Proof that we inserted all atoms until `idx`.

Instances For

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

The basic initial state.

Equations

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

Instances For

source
def Std.Sat.AIG.RelabelNat.State.addAtom {α : Type} [DecidableEq α] [Hashable α] {idx : Nat} {decls : Array (Decl α)} {hidx : idx < decls.size} (state : State α decls idx) (a : α) (h : decls[idx] = Decl.atom a) :
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.

Instances For

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

Insert a `Decl.false` into the `State` structure.

Equations

- state.addFalse h = { max := state.max, map := state.map, inv1 := ⋯, inv2 := ⋯ }

Instances For

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

Insert a `Decl.gate` into the `State` structure.

Equations

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

Instances For

source
def Std.Sat.AIG.RelabelNat.State.ofAIGAux {α : Type} [DecidableEq α] [Hashable α] (aig : AIG α) :
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

Instances For

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

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

Instances For

source
def Std.Sat.AIG.RelabelNat.State.ofAIG {α : Type} [DecidableEq α] [Hashable α] (aig : AIG α) :
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

Instances For

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

The map returned by `ofAIG` fulfills the `Inv1` property.

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

The map returned by `ofAIG` fulfills the `Inv2` property.

source
theorem Std.Sat.AIG.RelabelNat.State.ofAIG_find_unique {α : Type} [DecidableEq α] [Hashable α] {n : Nat} {aig : AIG α} (a : α) (ha : (ofAIG aig)[a]? = some n) (a' : α) :
(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.

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

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

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

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

Instances For

source
def Std.Sat.AIG.relabelNat {α : Type} [DecidableEq α] [Hashable α] (aig : AIG α) :
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

Instances For

source
@[simp]
theorem Std.Sat.AIG.relabelNat'_fst_eq_relabelNat {α : Type} [DecidableEq α] [Hashable α] {aig : AIG α} :
aig.relabelNat'.fst = aig.relabelNat
source
@[simp]
theorem Std.Sat.AIG.relabelNat_size_eq_size {α : Type} [DecidableEq α] [Hashable α] {aig : AIG α} :
aig.relabelNat.decls.size = aig.decls.size
source
theorem Std.Sat.AIG.relabelNat_unsat_iff_of_NonEmpty {α : Type} [DecidableEq α] [Hashable α] {idx : Nat} {invert : Bool} [Nonempty α] {aig : AIG α} {hidx1 : idx < aig.relabelNat.decls.size} {hidx2 : idx < aig.decls.size} :
aig.relabelNat.UnsatAt idx invert hidx1 ↔ aig.UnsatAt idx invert hidx2
source
theorem Std.Sat.AIG.relabelNat_unsat_iff {α : Type} [DecidableEq α] [Hashable α] {idx : Nat} {invert : Bool} {aig : AIG α} {hidx1 : idx < aig.relabelNat.decls.size} {hidx2 : idx < aig.decls.size} :
aig.relabelNat.UnsatAt idx invert hidx1 ↔ aig.UnsatAt idx invert hidx2

`relabelNat` preserves unsatisfiablility.

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

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

Instances For

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

Instances For

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

`relabelNat` preserves unsatisfiablility.