[ANN] Theo 0.1.0: a BDD library with theory support

Ecosystem
1

I’m pleased to announce the first release of Theo, an OCaml library for Binary Decision Diagrams (BDDs).

BDDs give you a canonical representation of boolean functions: two logically equivalent formulas always produce the exact same structure, so checking equivalence becomes a pointer comparison, O(1). Theo’s key extension is theory support: atoms aren’t just boolean variables but constraints like ocaml >= 4.14 or name = "foo", and the engine understands their semantics. This makes it practical for real-world constraint problems.

For example, a package manager can ask whether (ocaml >= 4.14 AND dune >= 3.0) OR (ocaml >= 5.0) is compatible with ocaml < 5.0. Theo reasons about the version constraints directly: it knows ocaml >= 4.14 is redundant when ocaml >= 5.0 holds, detects that the second disjunct contradicts ocaml < 5.0, and can extract the simplest satisfying assignment (ocaml >= 4.14, dune >= 3.0).

Highlights of the 0.1.0 release:

  • Core BDD engine with hash-consing (via weak tables) and a canonical negative-edge form
  • Boolean operations: AND, OR, NOT, IMPLIES, EQUIV, XOR, plus exists/forall quantifiers
  • Pluggable theory support over linear orders and equality (booleans, strings, integers, semantic versions), with a Combine functor to mix theories in the same BDD
  • restrict for partial evaluation under a set of external constraints, and constraint introspection via pattern matching
  • Minimal-witness extraction (shortest satisfying assignment) and zero-allocation entailment checks (implication, disjointness, exhaustiveness)
  • Irredundant sum-of-products (Minato–Morreale) computation
  • A property-based test suite

Some implementation details that may be of interest: memoization caches are built on ephemerons, so cache entries are reclaimed automatically once the BDD nodes they depend on become unreachable, with no manual cache invalidation and no leaks. Theory-aware simplification happens during BDD construction, using atom ordering to prune redundant bounds. The theory interface is a small functor-based API, and the same Syntax functor produces both BDD formulas and constraint lists.

I’ve written a companion blog post that walks through the main ideas: hash-consing and ephemeron caches, theory-aware simplification, and the algorithmic techniques behind restrict, minimal witnesses, and zero-allocation queries.

Feedback and contributions welcome!

2

Looks very interesting, thanks!

Out of curiosity: what was the motivation for this development?

Cheers,
Nicolas

3

The wasm_of_ocaml runtime is about 23k lines of handwritten Wasm text files, which is not very maintainable. To address this, I’m working on an improved Rust-like syntax for WebAssembly. Now, we use a preprocessor with conditionals, and I wanted to be able to translate and typecheck files back and forth between the two syntaxes while preserving preprocessor directives. For that, I needed a robust way to keep track of the boolean guard conditions, and BDDs seemed like a perfect fit. And things got a bit out of hand…

4

I see that you use QCheck in test/test_properties.ml. I would encourage you to give “model-based testing” a try, using Monolith or qcheck-stm. Whenever I have used this approach (for specific domains where it works well) I have been blown away by how effective it is, and I think that it would work very well to check a BDD implementation – it would find all the bugs.