def OBdd.discover {n m : ℕ} (O : OBdd n m) : Vector (List (Fin m)) n

Return a vector whose vth entry is a list of node indices with variable index v.

Equations

• O.discover = OBdd.discover_helper✝ (Collect.collect O) O.bdd.heap (Vector.replicate n [])

theorem OBdd.discover_spec {n m : ℕ} {O : OBdd n m} {j : Fin m} : Pointer.Reachable O.bdd.heap O.bdd.root (Pointer.node j) → j ∈ O.discover[O.bdd.heap[j].var]

discover is correct (forward direction).

theorem OBdd.discover_spec_inv {n m : ℕ} {O : OBdd n m} {j : Fin m} {i : Fin n} : j ∈ O.discover[i] → ↑O.bdd.heap[j].var = ↑i ∧ Pointer.Reachable O.bdd.heap O.bdd.root (Pointer.node j)

discover is correct (backward direction): membership implies var = i and reachability.