Module 3 — Combine BDDs with Apply and ITE · Binary Decision Diagrams with CUDD

formal.org
Binary Decision Diagrams with CUDD

Module 3 — Combine BDDs with Apply and ITEApply by Shannon expansion, the unique and computed tables, terminal cases and controlling values, ITE, and quantification by cofactors.Katas in this module (4)

Kata 3.1 — Build operators from ITE alone

Kata 3.2 — Decide which call stops early

Kata 3.3 — Quantify without the quantifier

Kata 3.4 — Make an AND bigger than its operands

Part of Binary Decision Diagrams with CUDD on formal.org.