Theo.MakeSourceFunctor to create a BDD implementation for a specific theory.
Make(T) produces a module containing all BDD operations (logical connectives, quantifiers, etc.) specialized for the theory T.
Make(Void) for standard boolean BDDs.Make(Combine(A)(B)) for multi-theory BDDs.Abstract type representing a BDD expression.
equal a b checks if a and b are physically equal. Since hash-consing guarantees unique representation, this is equivalent to logical equality. Same as equivalent.
Complexity: O(1)
compare a b compares the unique identifiers of a and b. defines a total ordering suitable for Set and Map.
Complexity: O(1)
hash a returns the unique identifier of a. Suitable for Hashtbl.
Complexity: O(1)
size expr returns the number of unique nodes in the BDD. Useful for analyzing BDD complexity.
Complexity: O(|expr|)
bool v creates an expression that is true when boolean variable v is true.
and_ a b computes the conjunction (AND) of two expressions.
Complexity: O(|a| × |b|) where |·| is the number of nodes
or_ a b computes the disjunction (OR) of two expressions.
Complexity: O(|a| × |b|)
xor a b computes the exclusive or of two expressions. True when exactly one of a or b is true.
Complexity: O(|a| × |b|)
iff a b computes the biconditional (if and only if) of two expressions. True when a and b have the same truth value. Equivalent to not (xor a b).
Complexity: O(|a| × |b|)
implies a b constructs the implication a => b (equivalent to not a || b). Returns a BDD representing the logical implication.
To check if a logically implies b (i.e., is a tautology), use is_tautology (implies a b).
Complexity: O(|a| × |b|)
ite cond then_ else_ computes the If-Then-Else operation. Equivalent to (cond && then_) || (not cond && else_).
Complexity: O(|cond| × |then_| × |else_|)
Syntax for convenient infix operators. Open locally with let open Theo.Syntax in ...
is_tautology expr returns true if expr is the constant true.
Complexity: O(1)
is_satisfiable expr returns true if expr has at least one satisfying assignment. Equivalent to sat expr <> None but more efficient.
Complexity: O(1)
equivalent a b checks if a and b are structurally identical. Due to hash-consing, structurally identical BDDs represent the same logical function.
Complexity: O(1)
logical_implies a b checks if a logically implies b (i.e., a => b is valid/tautology) without fully constructing the result.
is_disjoint a b checks if a and b are disjoint (i.e., a /\ b is unsatisfiable) without fully constructing the result.
is_exhaustive a b checks if a and b cover the entire space (i.e., a \/ b is a tautology) without fully constructing the result.
Represents an atomic constraint on a variable that contributes to satisfying the formula.
type constraint_view = | Constraint : {var : 'kind Var.t;The variable involved in the constraint.
*)payload : 'kind payload;The nature of the constraint: Bool for boolean variables, or Theory desc for theory atoms.
value : bool;The truth value asserted for this constraint.
value is true, the constraint is var (or atom).value is false, the constraint is not var (or not atom).} -> constraint_viewPattern-matchable view of the atomic constraint
The payload of an atomic constraint.
view_constraint c returns a pattern-matchable view of the atomic constraint c.
restrict expr constraints simplifies expr by assuming the specified constraints hold.
Complexity: O(|expr|)
ite_constant f g h evaluates if the result of ite f g h is a constant boolean without fully constructing the BDD. Returns Constant b if the result corresponds to b, or NonConstant otherwise.
exists v expr eliminates variable v from expr by computing the disjunction over all possible values. For a boolean variable, this is equivalent to restrict expr [Boolean(v, true)] || restrict expr [Boolean(v, false)]. For theory variables, it quantifies over all atoms mentioning v.
Example: let expr' = exists b (and_ (atom b) (atom c)) (* Result: atom c *)
Complexity: O(|expr|²)
forall v expr eliminates variable v from expr by computing the conjunction over all possible values. For a boolean variable, this is equivalent to restrict expr [Boolean(v, true)] && restrict expr [Boolean(v, false)].
Example: let expr' = forall b (or_ (atom b) (atom c)) (* Result: atom c *)
Complexity: O(|expr|²)
sat expr finds a satisfying set of constraints for expr, if one exists. Returns Some constraints where constraints is a list of atomic constraints that make the expression true. Returns None if the expression is unsatisfiable (equivalent to false_).
shortest_sat expr finds a satisfying set of constraints with the minimum number of atomic constraints (shortest path in the BDD DAG). Returns None if unsatisfiable.
irredundant_sop expr computes an irredundant sum-of-products (ISOP) cover of expr using the Minato-Morreale algorithm.
The result is a disjunction (outer list) of cubes (inner lists), where each cube is a conjunction of atomic constraints (literals). The disjunction of all cubes is logically equivalent to expr: sop_to_bdd (irredundant_sop expr) equals expr.
An empty outer list denotes false_; a single empty cube [[]] denotes true_.
The cover is irredundant modulo the theory: impossible combinations of atoms (e.g. v < 1 and v >= 3 can never hold together) are exploited as don't-cares. Concretely, no cube can be dropped while staying equivalent to expr, and each cube is a prime implicant modulo theory -- no literal can be removed even accounting for theory implications between atoms. For instance the cover of ¬(v<1) ∧ ((v<2) ∨ ¬(v<3)) contains the single literal cube ¬(v<3) rather than ¬(v<1) ∧ ¬(v<3), since ¬(v<3) already entails ¬(v<1).
Implementation note: the raw Minato-Morreale recursion yields a cover that is irredundant only over the atoms treated as independent Booleans; this function additionally post-processes it with theory-aware implication and equivalence checks to reach theory-level irredundancy. The post-processing is skipped when no variable carries two related atoms (in particular for purely Boolean expressions), since it cannot change the cover then.
Complexity: the Minato-Morreale recursion is memoized on the (lower, upper) interval. Producing k cubes then costs O(k²) theory-aware BDD operations for the post-processing when it runs. Note k, the size of an irredundant cover, can itself be exponential in the number of atoms in the worst case.
of_cube cube builds the conjunction (product) of the literals in cube. Returns true_ for the empty cube. This is the inverse of a single cube produced by irredundant_sop or sat.
sop_to_bdd cubes builds the disjunction of the cubes, i.e. the BDD of the sum-of-products cubes. Inverse of irredundant_sop.
and_list exprs computes the conjunction of all expressions in exprs. Returns true_ for an empty list. Uses a divide-and-conquer strategy to minimize intermediate BDD sizes and maximize cache reuse.
Example: let expr = and_list [e1; e2; e3]
Complexity: In the worst case, combining N BDDs of size S can result in exponential growth O(S^N). However, for many practical constraint problems, the divide-and-conquer approach yields typically O(S log N) performance.
or_list exprs computes the disjunction of all expressions in exprs. Returns false_ for an empty list.
Example: let expr = or_list [e1; e2; e3]
Complexity: Worst case O(S^N), typically O(S log N).
to_string expr returns a human-readable representation of the BDD structure. Shows the decision tree with atoms and branches.
print_dot chan expr prints the BDD in Graphviz DOT format to the given channel.
print_stats () prints statistics for all internal caches (atom table, node table, operation caches) to stdout. Useful for debugging and performance analysis.