package idds

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Legend:
Library
Module
Module type
Parameter
Class
Class type

Reduced Ordered Binary Decision Diagrams (BDDs).

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

val ctrue : t

val cfalse : t

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.

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