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.

This is a subroutine of reduce.

Equations

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

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

discover is correct.

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

discover is correct.

def Reduce.oreduce {n m : ℕ} (O : OBdd n m) : (k : ℕ) × OBdd n k

Equations

• Reduce.oreduce O_2 = ⟨0, ⟨{ heap := Vector.emptyWithCapacity 0, root := Pointer.terminal (Reduce.zero_vars_to_bool✝ ↑O_2) }, ⋯⟩⟩
• Reduce.oreduce O_3 = ⟨0, O_3⟩
• Reduce.oreduce O_3 = match h : Reduce.reduce''✝ O_3 with | (B, k) => ⟨↑k, ⟨Trim.trim B ⋯ ⋯, ⋯⟩⟩

theorem Reduce.oreduce_reduced {n m : ℕ} {O : OBdd n m} : (oreduce O).snd.Reduced

@[simp]

theorem Reduce.oreduce_evaluate {n m : ℕ} {O : OBdd n m} : (oreduce O).snd.evaluate = O.evaluate