Teaching Booleans About Versions: A Theory-Augmented BDD Library in OCaml
A tour of Theo, an OCaml BDD library with complement edges for O(1) negation, ephemeron-based caching, and theory support for reasoning about version constraints and equality, turning logical equivalence into a pointer…