theo

Tech stack & purpose

Theo is a Binary Decision Diagram (BDD) library for OCaml that provides efficient boolean logic manipulation with support for theory reasoning over linear orders and equality, applicable to domains like booleans, strings, integers, and semantic versions. The library is built in OCaml using Dune and includes core BDD operations (AND, OR, NOT, IMPLIES, EQUIV, XOR, quantifiers), optimization techniques like hash-consing and negative edge optimizations, and comprehensive introspection capabilities. The project features a generic architecture based on functors—`Make` for the core BDD engine, `Theory` for domain-specific values, and `Combine` for merging theories—and is verified through an extensive test suite including property-based testing with QCheck and an optional Monolith fuzzing harness for catching cache-interaction bugs across arbitrary API call sequences.

Languages

Contributors

• 
  Jérôme Vouillon20 commits · 117 followers