Propositional simplification of HOL terms via binary decision diagrams.

Uses a self-contained ROBDD implementation with no dependency on Elixir internals. BDD nodes: :bdd_top, :bdd_bot, or {var, high, low} where var is a term ID integer and the variable ordering is ascending integer.

bdd_to_term/1 reads a BDD back as a minimal HOL formula using Shannon expansion with short-circuit identities, so the result is always at least as simple as the input and often simpler.

Modes

• :shallow — simplify only the term's top-level propositional structure. Sub-formulas under quantifiers, abstractions or non-logical heads are opaque atoms.

• :deep — bottom-up over the DAG: simplify every type-o sub-formula, including the bodies of quantifiers and other abstractions whose ultimate goal type is o.