Bddapron

About

This library is actually composed of two sub-libraries:

• Bdd: higher-level interface to CUDD (compared to MLCuddIDL):
  • Manipulation of formulas and expressions of various finite types: Boolean, bounded integers, enumerated types;
  • BDDs as an abstract domain for such datatypes.
• Bddapron:
  • Formulas and expressions mixing finite types and numerical types, represented as BDDs/MTBDDs (e.g., if x>=y-3 and b then x-y else x-2*y*y), with
  • Abstract domains combining finite-type and numerical variables, by combining BDDs/MTBDDs (for finite-type variables) and APRON domains (for numerical variables)

A short presentation in french

You will need CamlIDL and FINDLIB.

Both sublibraries require the Camllib utility library and the MLCuddIDL BDD library/binding. The Bddapron sublibrary requires in addition the APRON library and its dependencies (GMP, MPFR, MLGMPIDL).

License

Bddapron is released under the LGPL license.

Download

Current version: 2.2.0

• Subversion repository: BDDAPRON alone (see Up for the organisation of the repository)
• Subversion repository: BDDAPRON together with dependencies camllib, mlcuddidl, mlgmpidl, apron (see Up for the organisation of the repository)

Documentation

• On-line
• PDF