package idds

  1. Overview
  2. Docs

Module Idds.DdSource

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

Sourcetype t = private
  1. | True
  2. | False
  3. | 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

Sourcetype 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.

Sourceval manager : Base.unit -> manager

Initialize a fresh manager

Constructors

Sourceval cfalse : t

The constant false.

Sourceval ctrue : t

The constant true.

Sourceval 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

Sourceval 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.

Sourceval to_string : ?var_name:(Var.t -> Base.string) -> t -> Base.string
Sourceval render : ?var_name:(Var.t -> Base.string) -> ?format:Base.string -> ?title:Base.string -> t -> Base.unit

Low-level API

Sourceval 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.

Sourceval 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.