package idd

  1. Overview
  2. Docs

Reduced Ordered Binary Decision Diagrams (BDDs).

Types

type t = private Dd.t

A BDD is just a DD with two additional structural constraints:

  • Ordered: the variables along any root-leaf path of a BDD increase strictly monotonically.
  • Reduced: The hi and lo subtrees of any branch are distinct.
val equal : t -> t -> bool
type manager
val manager : unit -> manager

Constructors

val ctrue : t
val cfalse : t

Boolean operations

val conj : manager -> t -> t -> t

boolean conjunction (logical and)

val disj : manager -> t -> t -> t

boolean disjunction (logical or)

val neg : manager -> t -> t

boolean negation (logical not)

val ite : manager -> Var.t -> t -> t -> t

ite mgr i u v behaves like u when variable i is true, and like v otherwise.

module Make () : Boolean.Algebra with type t = t

BDDs form a boolean algebra.

Semantics

val eval : t -> env:(Var.t -> bool) -> bool