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
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)
Build and test
To build from source execute
To run all tests execute
with-test & >= "v0.12.0"