Documentation

Bdd.Reduce

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
Instances For
    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.

    def Reduce.oreduce {n m : } (O : OBdd n m) :
    (s : ) × OBdd n s
    Equations
    Instances For
      theorem Reduce.oreduce_reduced {n m : } {O : OBdd n m} :
      @[simp]
      theorem Reduce.oreduce_evaluate {n m : } {O : OBdd n m} :