package idd

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Types
Manager
Constructors
Generic operations on DDs
Low-level API

idd
- Idd_
  - Algebra
    
    BA
    
    GKAT
    
    KA
    
    KAT
  - Bdd
    
    Make
  - Boolean
    
    Algebra
  - Dd
  - Idd
    
    Rel
  - Var

Legend:
Library
Module
Module type
Parameter
Class
Class type

Decision Diagrams (DDs).

This module serves as the base for the BDD and IDD modules. It provides hash-consed decision trees, but does not enforce any structural invariants on these trees beyond guranteeing that structural equality coincides with physical equality.

A decision diagram (DD) is a finite binary tree whose leaves are labeled with the constants true or false, and whose branches are labeled with boolean variables. Each branch has two subtrees hi and lo for the cases that the variable is true or false, respectively.

Given an assignment of booleans to the variables, one can evaluate such a tree in the following way:

If the tree is a leaf, return its boolean label.
If the tree is a branch labeled with the variable x, recursively evaluate
- the subtree hi if x = true, or
- the subtree lo if x = false.

The module enforces a key invariant: If u : t and v : t were constructed using the same manager, then id u = id v if and only if u and v are structurally equal (ignoring IDs). In other words, all DDs built using the same manager are hash consed.

Types

type t = private

| True
| False
| Branch of {
1. var : Var.t;
  (*
  the variable on which to branch
  *)
2. hi : t;
  (*
  subdiagram for case var = true
  *)
3. lo : t;
  (*
  subdiagramm for case var = false
  *)
4. id : Base.int;
  (*
  unique identifier for this diagram
  *)
}

The type of a decision diagram (DD).

Manager

type manager

A DD manager mgr : manager encapsulates all state required for DD construction. In particular, it is required by the branch function to allocate unique identifiers for each DD.

val manager : Base.unit -> manager

Initialize a fresh manager

Constructors

val cfalse : t

The constant false.

val ctrue : t

The constant true.

val branch : manager -> Var.t -> t -> t -> t

branch mgr var hi lo is the diagram that behaves like hi when var = true, and like lo when var = false.

Generic operations on DDs

val equal : t -> t -> Base.bool

O(1) structural equality.

PRECONDITION: The result of equal u v is only defined when u and v were built using the same manager. Otherwise, the result is arbitrary.

val to_string : t -> Base.string

Low-level API

val id : t -> Base.int

id u is an integer that is guranteed to be unique to the the diagram u. In particular, the following invariant holds whenever u and v were constructed using the same manager: id u = id v iff the trees u and v are structurally equal (ignoring IDs). Thus, one can use the IDs to test for equality in O(1). IDs are also useful for memoizing functions on DDs.

val index : t -> Base.int

The index of a diagram is the index of its top-most variable, or -1 if the diagram is a leaf.