Module Bdd

module Bdd: sig .. end

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

• Bdd.Reg: manipulating arrays of BDDs as CPU register, including most ALU (Arithmetic and Logical Unit) operations;
• Bdd.Int: signed/unsigned integers encoded as arrays of BDDs;
• Bdd.Enum: enumerated types, with management of labels and types (requires Bdd.Env);
• Bdd.Output: outputing BDDs/MTBDDs (low-level)

• Bdd.Env: environment defining finite-type variables and user-defined enumerated types, and mapping them to BDDs indices;
• Bdd.Expr0: general finite-type expressions;
• Bdd.Domain0: Boolean formula seen as an (abstract) domain
• Bdd.Expr1, Bdd.Domain1: extends Bdd.Expr0 and Bdd.Domain0 by incorporating normalized environments.

module Output: sig .. end

module Normalform: sig .. end

module Reg: sig .. end

module Env: sig .. end

module Int: sig .. end

module Enum: sig .. end

module Cond: sig .. end

module Decompose: sig .. end

module Expr0: sig .. end

module Expr1: sig .. end

module Domain0: sig .. end

module Domain1: sig .. end