# Module Bddapron

`module Bddapron: `sig` .. `end``
Finite \& numerical expressions/properties on top of CUDD \& APRON

## Introduction

Expressions and abstract domains combining finite-type and numerical types.

`Bddapron` extends `Bdd` (manipulation of finite-type formula using BDDs) and `Apron` (numerical abstract domain library). It enables formula of numerical type, and it allows decisions on numerical constraints in formula.

It can be seen as an extension of the APRON abstract domain for dealing with Boolean and finite-type variables, in addition to numerical variables.

## Module `Apronexpr`: Purely arithmetic expressions (internal)

`module Apronexpr: `sig` .. `end``

## Module `Env`: Normalized variable managers/environments

`module Env: `sig` .. `end``

## Module `Cond`: Normalized condition environments

`module Cond: `sig` .. `end``

## Module `ApronexprDD`: DDs on top of arithmetic expressions (internal)

`module ApronexprDD: `sig` .. `end``

## Module `Common`: Functions common to the two implementations of Combined Boolean/Numerical domain

`module Common: `sig` .. `end``

## Module `ApronDD`: DDs on top of Apron abstract values (internal)

`module ApronDD: `sig` .. `end``

## Module `Expr0`: Finite-type and arithmetical expressions

`module Expr0: `sig` .. `end``

## Module `Expr1`: Finite-type and arithmetical expressions with normalized environments

`module Expr1: `sig` .. `end``

## Module `Expr2`: Finite-type and arithmetical expressions with variable and condition environments

`module Expr2: `sig` .. `end``

## Module `Descend`: Recursive descend on sets of diagrams (internal)

`module Descend: `sig` .. `end``

## Module `Mtbdddomain0`: Boolean/Numerical domain, with MTBDDs over APRON values

`module Mtbdddomain0: `sig` .. `end``

## Module `Bddleaf`: Manipulation of lists of guards and leafs (internal)

`module Bddleaf: `sig` .. `end``

## Module `Bdddomain0`: Combined Boolean/Numerical domain, with lists of BDDs and APRON values

`module Bdddomain0: `sig` .. `end``

## Module `Domain0`: Boolean/Numerical domain: generic interface

`module Domain0: `sig` .. `end``

## Module `Domainlevel1`: Functor to transform an abstract domain interface from level 0 to level 1 (internal)

`module Domainlevel1: `sig` .. `end``

## Module `Mtbdddomain1`: Boolean/Numerical domain with normalized environment

`module Mtbdddomain1: `sig` .. `end``

## Module `Bdddomain1`: Boolean/Numerical domain with normalized environment

`module Bdddomain1: `sig` .. `end``

## Module `Domain1`: Boolean/Numerical domain with normalized environment

`module Domain1: `sig` .. `end``

## Module `Formula`: Extra-operations on formula

`module Formula: `sig` .. `end``

## Module `Policy`: Policies for BDDAPRON abstract values

`module Policy: `sig` .. `end``

## Module `Syntax`: Building BDDAPRON expressions from Abstract Syntax Trees

`module Syntax: `sig` .. `end``

## Module `Yacc`

`module Yacc: `sig` .. `end``

## Module `Lex`

`module Lex: `sig` .. `end``

## Module `Parser`: Parsing BDDAPRON expressions from strings (or lexing buffers)

`module Parser: `sig` .. `end``