Module Theo

Theory-Augmented Binary Decision Diagrams (BDDs)

This module provides an efficient implementation of Binary Decision Diagrams with support for theory reasoning over linear orders and equality (including booleans, strings, integers, semantic versions).

BDDs are canonical representations of boolean functions that enable efficient logical operations and satisfiability checking through hash-consing and memoization.

Features:

• Automatic node sharing via hash-consing
• Memoized operations for performance
• Theory atoms: boolean tests, string equality, version comparisons
• Type-safe variable system using GADTs

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

Example usage:

module Bdd = Theo.Make (Theo.Void)

let b1 = Bdd.Var.fresh ()
let b2 = Bdd.Var.fresh ()
let expr = Bdd.Syntax.(bool b1 && not (bool b2))

let () =
  if Bdd.is_tautology expr then Printf.printf "Always true\n"
  else Printf.printf "Depends on variables\n"

Architecture: The library is built around a few core concepts:

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

Example: Combining Theories To use multiple theories (e.g., String equality and Version comparisons) in the same BDD:

  (* 1. Define your atomic types *)
  module StringAtom = struct ... end (* implements Comparable *)
  module VersionAtom = struct ... end (* implements Comparable *)

  (* 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 *)
  (* Notice we pass parts of the sum theory to the helpers *)
  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 expr = MyBDD.and_ V.(v_var < v) S.(s_var = s)

Example: Working with Constraints You can also use the syntax modules to build restrict constraints, and pattern match on constraints using view_constraint.

(* 1. Build constraint syntax helpers *)
(* Instead of MyBDD, we pass MyBDD.Constraint to the syntax functors *)
module V_cstr = VersionLeq.Syntax (MyTheory.Left (MyBDD.Constraint))
module S_cstr = StringEq.Syntax (MyTheory.Right (MyBDD.Constraint))

(* 2. Create constraints *)
(* Note: These return atomic_constraint list, NOT a BDD *)
let c1 = V_cstr.(v_var < v)
let c2 = S_cstr.(s_var = s)

(* 3. Combine constraints *)
let constraints = MyBDD.Constraint.and_ c1 c2

(* 4. Restrict a BDD *)
let restricted_expr = MyBDD.restrict expr constraints

(* 5. Introspection (Pattern Matching) *)
let match_constraint (c : MyBDD.atomic_constraint) =
  match MyBDD.view_constraint c with
  | MyBDD.Constraint { payload = Bool; value; _ } ->
      Printf.printf "Boolean variable is %b" value
  | MyBDD.Constraint { payload = Theory desc; value; _ } -> (
      (* 'desc' is a 'kind MyTheory.t' (the sum type) *)
      match desc with
      | MyTheory.Left (VersionLeq.Bound { limit; inclusive = _ }) ->
          Printf.printf "Version <= %s is %b"
            (VersionAtom.to_string limit)
            value
      | MyTheory.Right (StringEq.Const s) ->
          Printf.printf "String = %s is %b" (StringAtom.to_string s) value)