bdd.mlpacki

(** Finite-type expressions/properties on top of CUDD *)

(**
Higher-level interface relying on {!Cudd} interface for manipulating
BDDs/MTBDDs:
- {!Reg}: manipulating arrays of BDDs as CPU register, including
  most ALU (Arithmetic and Logical Unit) operations;
- {!Int}: signed/unsigned integers encoded as arrays of BDDs;
- {!Enum}: enumerated types, with management of labels and types (requires {!Env});

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

Exploits
{{:http://pop-art.inrialpes.fr/~bjeannet/mlxxxidl-forge/mlcuddidl/html/index.html}MLCuddIDL}
(ultimately {{:http://vlsi.colorado.edu/~fabio/CUDD/cuddIntro.html}CUDD}) and
{{:http://pop-art.inrialpes.fr/~bjeannet/bjeannet-forge/camllib/html/index.html}Camllib}
libraries.

*)

(* *)