package idd

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Legend:
Library
Module
Module type
Parameter
Class
Class type

Identity Suppressed Decision Diagrams (IDDs).

type t = private Dd.t

An IDD is just a DD with two additional structural constraints that ensure canonicity: two IDDs encode the same function iff they are the same IDD.

type manager

val manager : unit -> manager

val ident : t

The identity relation.

val empty : t

The empty relation.

val test : manager -> int -> bool -> t

For i < n, eval (test i b) env n = env (Var.inp i) = b && eval ident env n rel n (test i b) = { (x,x) | x \in B^n, x_i = b }

val set : manager -> int -> bool -> t

For i < n, eval (set i b) env n = eval ident env' n, where env' x = if x = Var.inp i then b else env x rel n (set i b) = { (x,xi:=b) | x \in B^n }

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.

val apply : manager -> (bool -> bool -> bool) -> t -> t -> t

apply mgr op t0 t1 is t such that Bool.equal (op (eval t0 env n) (eval t1 env n)) (eval t env n)

val seq : manager -> t -> t -> t

Sequential composition

val union : manager -> t -> t -> t

(Relational) union

val star : manager -> t -> t

(Relational) transitive-reflexive closure

val equal : t -> t -> 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 subseteq : manager -> t -> t -> bool

relational containment

val eval : t -> (Var.t -> bool) -> int -> bool

eval tree env n evaluates idd tree in environment env where the variable indices are 0,...,n-1

module Rel : Algebra.KAT with type b := Bdd.t and type t := t