Theo

Theo is a Binary Decision Diagram (BDD) library for OCaml. It provides efficient boolean logic manipulation with support for theory reasoning over linear orders and equality (including booleans, strings, integers, and semantic versions).

Documentation

The API documentation is available online at: https://vouillon.github.io/theo/theo/Theo/

Features

• Generic Theory Support: Create BDDs for any domain by implementing the Theory interface.
• Combinators: Easily combine multiple theories (e.g., String + Version) using the Combine functor.
• Core BDD Operations: AND, OR, NOT, IMPLIES, EQUIV, XOR, quantifiers (exists/forall).
• Optimization:
  • Hash-consing for structural sharing.
  • Efficient restrict operations for partial evaluation.
  • Negative edge optimizations (canonical form).
• Introspection: Inspect and pattern match on constraints.
• Verification: Comprehensive test suite including property-based fuzzing.

Installation

Prerequisites

• OCaml >= 4.14
• Dune >= 3.17

Building from Source

git clone https://github.com/vouillon/theo.git
cd theo
dune build

Installing via Opam

To install the latest release from the opam repository:

opam install theo

Alternatively, to install from a local checkout:

opam install .

Running Tests

dune runtest

In addition to the QCheck suite, fuzz/ contains an optional Monolith harness that tests Theo against a reference model over arbitrary sequences of API calls (optionally with afl-fuzz). It is a dev-only tool and is not part of dune runtest; see fuzz/README.md.

Architecture

The library is built around a few core concepts:

• Make: The core BDD engine functor. It takes a Theory as input and produces a BDD module.
• Theory: An interface for values that can be part of the BDD.
• Combine: A functor to combine two theories into one sum theory.
• Primitive_theory: Standard theories builders like Leq (linear order) and Eq (equality).

Usage

The examples below are compiled and checked by test/doc_examples.ml; keep them in sync.

1. Simple Boolean Logic

Use Theo.Void for standard BDDs without extra theories.

module BDD = Theo.Make (Theo.Void)

let () =
  let x = BDD.Var.fresh () in
  let y = BDD.Var.fresh () in

  (* Construct expressions *)
  let open BDD.Syntax in
  let expr = bool x && not (bool y) in

  (* Check tautology/satisfiability *)
  let is_sat = BDD.is_satisfiable expr in (* true *)
  let is_taut = BDD.is_tautology expr in (* false *)
  Printf.printf "Sat: %b, Taut: %b\n" is_sat is_taut

2. Combining Theories

You can combine multiple theories (e.g., String equality and Version comparisons) in the same BDD.

(* 1. Define your atomic types *)
module StringAtom = struct 
  include String 
  let to_string s = s 
  let hash = Hashtbl.hash 
end
module VersionAtom = struct 
  type t = { major: int; minor: int; patch: int }
  let compare = compare
  let equal = (=)
  let hash = Hashtbl.hash
  let to_string v = Printf.sprintf "%d.%d.%d" v.major v.minor v.patch
end

(* 2. Instantiate primitive theories *)
module StringEq = Theo.Eq(StringAtom)
module VersionLeq = Theo.Leq(VersionAtom)

(* 3. Combine them into a single theory *)
module MyTheory = Theo.Combine(VersionLeq)(StringEq)

(* 4. Create the BDD module *)
module MyBDD = Theo.Make(MyTheory)

(* 5. Instantiate syntax helpers for convenient construction *)
module V = VersionLeq.Syntax(MyTheory.Left(MyBDD))
module S = StringEq.Syntax(MyTheory.Right(MyBDD))

(* 6. Now you can mix them! *)
let v_var = MyBDD.Var.fresh ()
let s_var = MyBDD.Var.fresh ()
let v = { VersionAtom.major = 1; minor = 0; patch = 0 }
let s = "production"

(* Use infix operators: V.(...) and S.(...) *)
let expr = MyBDD.and_ V.(v_var < v) S.(s_var = s)
(* "Version < 1.0.0 AND String = 'production'" *)

3. Working with Constraints

You can build constraints for restrict or inspect them using pattern matching.

(* 1. Build constraint syntax helpers *)
(* Pass MyBDD.Constraint instead of MyBDD *)
module V_cstr = VersionLeq.Syntax(MyTheory.Left(MyBDD.Constraint))
module S_cstr = StringEq.Syntax(MyTheory.Right(MyBDD.Constraint))

let () =
  (* 2. Create constraints *)
  let c1 = V_cstr.(v_var < v) in

  (* 3. Restrict a BDD *)
  (* assume that v_var < 1.0.0 *)
  let restricted_expr = MyBDD.restrict expr c1 in
  Printf.printf "Restricted: %s\n" (MyBDD.to_string restricted_expr);

  (* 4. Introspection *)
  let describe (c : MyBDD.atomic_constraint) =
    match MyBDD.view_constraint c with
    | MyBDD.Constraint { payload = Bool; value; _ } ->
        Printf.printf "boolean variable is %b\n" value
    | MyBDD.Constraint { payload = Theory desc; value; _ } -> (
        match desc with
        | MyTheory.Left (VersionLeq.Bound { limit; inclusive }) ->
            Printf.printf "version %s %s is %b\n"
              (if inclusive then "<=" else "<")
              (VersionAtom.to_string limit) value
        | MyTheory.Right (StringEq.Const s) ->
            Printf.printf "string = %s is %b\n" s value)
  in
  List.iter describe c1

Thread Safety

Theo is not thread-safe (nor domain-safe): fresh variable generation, the hash-consing tables, and the operation caches are shared mutable state.

Project Structure

• src/lib-theo/: Core library implementation.
  • theo.ml: Main BDD engine and theory functors.
  • theo.mli: Public API documentation.
• test/: Unit tests, properties, and benchmarks.
  • test/support/: Shared private library (theo_test_support): the monomorphised BDD instance and the reference model used for fuzzing.
• fuzz/: Optional Monolith fuzzing harness (see fuzz/README.md).

License

MIT License.