package idd

  1. Overview
  2. Docs

Module Idd_.IddSource

Identity Suppressed Decision Diagrams (IDDs).

Types

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

Sourcetype manager
Sourceval manager : unit -> manager

Constructors

Sourceval ident : t

The identity relation.

Sourceval empty : t

The empty relation.

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

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

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.

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

Sourceval seq : manager -> t -> t -> t

Sequential composition

Sourceval union : manager -> t -> t -> t

(Relational) union

Sourceval star : manager -> t -> t

(Relational) transitive-reflexive closure

Boolean operations

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

Sourceval subseteq : manager -> t -> t -> bool

relational containment

Semantics

Sourceval 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

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

Innovation. Community. Security.