Module Bdd

module Bdd: sig .. end
Finite-type expressions/properties on top of CUDD


Higher-level interface relying on Cudd interface for manipulating BDDs/MTBDDs:

Finite-type expressions and properties: Exploits MLCuddIDL (ultimately CUDD) and Camllib libraries.

Module Output: Output of BDDs/MTBDDs

module Output: sig .. end

Module Normalform: Utility types and functions for normalization

module Normalform: sig .. end

Module Reg: Bounded unsigned integer expressions with BDDs

module Reg: sig .. end

Module Env: Normalized managers/environments

module Env: sig .. end

Module Int: Bounded integer expressions with BDDs

module Int: sig .. end

Module Enum: Enumerated expressions with BDDs

module Enum: sig .. end

Module Cond: Normalized condition environments (base module)

module Cond: sig .. end

Module Decompose: Separation of Boolean formula in purely Boolean/conditional parts

module Decompose: sig .. end

Module Expr0: Finite-type expressions with BDDs

module Expr0: sig .. end

Module Expr1: Finite-type expressions with normalized environments

module Expr1: sig .. end

Module Domain0: Boolean (abstract) domain

module Domain0: sig .. end

Module Domain1: Boolean (abstract) domain with normalized environment

module Domain1: sig .. end