package idd

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module `Idd_.Bdd`Source

Reduced Ordered Binary Decision Diagrams (BDDs).

Sourcetype t = private Dd.t

A BDD is just a DD with two additional structural constraints:

Ordered: the variables along any root-leaf path of a BDD increase strictly monotonically.
Reduced: The hi and lo subtrees of any branch are distinct.

Sourceval equal : t -> t -> bool

Sourcetype manager

Sourceval manager : unit -> manager

Sourceval ctrue : t

Sourceval cfalse : t

Sourceval conj : manager -> t -> t -> t

boolean conjunction (logical and)

Sourceval disj : manager -> t -> t -> t

boolean disjunction (logical or)

Sourceval neg : manager -> t -> t

boolean negation (logical not)

Sourceval ite : manager -> Var.t -> t -> t -> t

ite mgr i u v behaves like u when variable i is true, and like v otherwise.

Sourcemodule Make () : Boolean.Algebra with type t = t

BDDs form a boolean algebra.

Sourceval eval : t -> env:(Var.t -> bool) -> bool