package idds

  1. Overview
  2. Docs
Identity-suppressed decision diagrams (IDDs)

Install

Dune Dependency

Authors

Maintainers

Sources

idds-0.2.tbz
sha256=0cb7c160cb45957dfd2603ca6d10dab80fef51d60e47b9d7a5a8b7970d30ac39
sha512=eddfd447f4ddac7873f762efd3cffb4987d06a44e21f765982673549da4a5771a101d98294267fb3fec458e0eccafc9ba05d9a715034307fc23b199a4c783deb

Description

BDD and IDD implementation with hash-consing

Published: 07 Dec 2019

README

IDDs: Identity-suppressed Decision Diagrams

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

Overview

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.

Provided operations

BDDs

  • Constructors: true, false, if-then-else

  • Operations: equality, negation, disjunction, conjunction

IDDs

  • Constructors: identity relation, empty relation, test, set, branch

  • Operations: equality, subset test, apply algorithm, union, sequential composition, transitive-reflexive closure

Example session

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)

Build and test

To build from source execute

dune build

To run all tests execute

dune runtest

Dependencies (6)

  1. ppx_jane >= "v0.12.0"
  2. ppx_deriving >= "4.3"
  3. open > "0"
  4. base >= "v0.12.0"
  5. dune >= "1.10"
  6. ocaml >= "4.04.0"

Dev Dependencies (2)

  1. ppx_inline_test with-test & >= "v0.12.0"
  2. odoc with-doc

Used by (1)

  1. netkat

Conflicts

None