package idd

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

Install

Dune Dependency

Authors

Maintainers

Sources

0.1.tar.gz
sha256=2242527e57c1bfbcaecc9b31553d068b34635416cd2fe7b4abd382798f675d7f
md5=ae78cf9648a3238e7336c95229e507ad

Description

Published: 24 May 2019

README

Overview

This package implements hash-consed binary decision diagrams (BDDs) and identity-suppressed decision diagrams (IDDs).

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

Dependencies (5)

  1. ppx_deriving
  2. ppx_jane
  3. base >= "v0.12.0" & < "v0.17"
  4. dune
  5. ocaml >= "4.04.0"

Dev Dependencies

None

Used by

None

Conflicts

None

OCaml

Innovation. Community. Security.