This package implements hash-consed binary decision diagrams (BDDs) and identity-suppressed decision diagrams (IDDs). The API is documented here.

An IDD, like a BBD, can be seen as representing a transition relation R on a state space of boolean vectors. I.e. boolean vector pair (v1, v2) belongs to R if and only if evaluating the IDD-representation of R in the environment given by (v1, v2) yields true.

The main motivation for IDDs is that they represent the identity relation in a constant amount of space instead of in an amount of space that is linear in the size of the boolean vectors.

• Constructors: true, false, if-then-else
• Operations: equality, negation, disjunction, conjunction

• Constructors: identity relation, empty relation, test, set, branch
• Operations: equality, subset test, apply algorithm, union, sequential composition, transitive-reflexive closure

Assuming you have utop installed like so,

opam install utop

you can start an interactive session by executing the following from the root directory of the project:

dune utop .

You can then experiment with the library in utop and render decision diagrams to inspect them, provided you have graphviz installed.

open Idd_;;

(* DDs *)
let mgr = Dd.manager ();;
let d0 = Dd.branch mgr (Var.out 1) Dd.ctrue Dd.cfalse;;
Dd.render d0;;
let d1 = Dd.branch mgr (Var.inp 1) d0 d0;;
Dd.render d1;;

(* IDDs *)
let mgr = Idd.manager();;
Dd.render (Idd.test mgr 3 true :> Dd.t);;
Dd.render (Idd.set mgr 3 true :> Dd.t);;
let flip = Idd.(union mgr (seq mgr (test mgr 3 true) (set mgr 3 false))
                          (seq mgr (test mgr 3 false) (set mgr 3 true)));;
Dd.render (flip :> Dd.t)

To build from source execute

dune build

To run all tests execute

dune runtest