Documentation

Bdd.Evaluate

source
@[irreducible]
def Evaluate.evaluate {n m : ℕ} (O : OBdd n m) :
Vector Bool n → Bool
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Evaluate.evaluate_evaluate {n✝ m✝ : ℕ} {O : OBdd n✝ m✝} :
    evaluate O = O.evaluate
    source
    theorem Evaluate.evaluate_terminal {n m : ℕ} {b : Bool} {O : OBdd n m} :
    (↑O).root = Pointer.terminal b → evaluate O = Function.const (Vector Bool n) b
    source
    theorem Evaluate.evaluate_node {n m : ℕ} {j : Fin m} {O : OBdd n m} (h : (↑O).root = Pointer.node j) :
    evaluate O = fun (I : Vector Bool n) => if I[(↑O).heap[j].var] = true then evaluate (O.high h) I else evaluate (O.low h) I
    source
    def Evaluate.Parser.Attr.bdd_nvars :
    Lean.ParserDescr

    A simp attribute that is used in BDD.lean to infer the size of BDDs when during evaluation.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Evaluate.Parser.Attr.bdd_nvars_proc :
      Lean.ParserDescr

      Simplification procedure

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Evaluate.tacticBdd_bounds :
        Lean.ParserDescr
        Equations
        Instances For