Module Idds.Bdd

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 : ?dd_mgr:Dd.manager -> unit -> manager
val get_dd_manager : manager -> Dd.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.

val test : manager -> Var.t -> bool -> t

test mgr var b is the diagram that behaves like b when var = true and like not b when var = false

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

BDDs form a boolean algebra.

Semantics

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