# Module Ppl

    module Ppl: sig .. end

Convex Polyhedra and Linear Congruences abstract domains (PPL wrapper)

This module is a wrapper around the Parma Polyhedra Library.

    type loose

    type strict

Two flavors for convex polyhedra: loose or strict.

Loose polyhedra cannot have strict inequality constraints like `x>0`. They are algorithmically more efficient (less generators, simpler normalization). Convex polyhedra are defined by the conjunction of a set of linear constraints of the form `a_0*x_0 + ... + a_n*x_n + b >= 0` or `a_0*x_0 + ... + a_n*x_n + b > 0` where `a_0, ..., a_n, b, c` are constants and `x_0, ..., x_n` variables.

    type grid

Linear congruences.

Linear congruences are defined by the conjunction of equality constraints modulo a rational number, of the form `a_0*x_0 + ... + a_n*x_n = b mod c`, where `a_0, ..., a_n, b, c` are constants and `x_0, ..., x_n` variables.

    type 'a t

Type of convex polyhedra/linear congruences, where `'a` is `loose`, `strict` or `grid`.

Abstract values which are convex polyhedra have the type `loose t Apron.AbstractX.t` or `strict t Apron.AbstractX.t`. Abstract values which are conjunction of linear congruences equalities have the type `grid t Apron.AbstractX.t`. Managers allocated by PPL have the type `'a t Apron.Manager.t`.

    val manager_alloc_loose : unit -> loose t Apron.Manager.t

Allocate a PPL manager for loose convex polyhedra.

    val manager_alloc_strict : unit -> strict t Apron.Manager.t

Allocate a PPL manager for strict convex polyhedra.

    val manager_alloc_grid : unit -> grid t Apron.Manager.t

Allocate a new manager for linear congruences (grids)

    val manager_is_ppl : 'a Apron.Manager.t -> bool

### Type conversions

    val manager_is_ppl_loose : 'a Apron.Manager.t -> bool

    val manager_is_ppl_strict : 'a Apron.Manager.t -> bool

    val manager_is_ppl_grid : 'a Apron.Manager.t -> bool

Return `true` iff the argument manager is a ppl manager

    val manager_of_ppl : 'a t Apron.Manager.t -> 'b Apron.Manager.t

    val manager_of_ppl_loose : loose t Apron.Manager.t -> 'a Apron.Manager.t

    val manager_of_ppl_strict : strict t Apron.Manager.t -> 'a Apron.Manager.t

    val manager_of_ppl_grid : grid t Apron.Manager.t -> 'a Apron.Manager.t

Make a ppl manager generic

    val manager_to_ppl : 'a Apron.Manager.t -> 'b t Apron.Manager.t

    val manager_to_ppl_loose : 'a Apron.Manager.t -> loose t Apron.Manager.t

    val manager_to_ppl_strict : 'a Apron.Manager.t -> strict t Apron.Manager.t

    val manager_to_ppl_grid : 'a Apron.Manager.t -> grid t Apron.Manager.t

Instanciate the type of a ppl manager. Raises `Failure` if the argument manager is not a ppl manager

    module Abstract0: sig .. end

    module Abstract1: sig .. end

### Compilation information

See Compiling and linking client programs against APRON for complete explanations. We just show examples with the file `mlexample.ml`.

Do not forget the `-cc "g++"` option: PPL is a C++ library which requires a C++ linker.

#### Bytecode compilation

    ocamlc -cc "g++"-I $MLGMPIDL_PREFIX/lib -I $APRON_PREFIX/lib -o mlexample.byte \
      bigarray.cma gmp.cma apron.cma ppl.cma mlexample.ml

    ocamlc -cc "g++" -I $MLGMPIDL_PREFIX/lib -I $APRON_PREFIX/lib -make-runtime -o myrun \
      bigarray.cma gmp.cma apron.cma ppl.cma

    ocamlc -cc "g++" -I $MLGMPIDL_PREFIX/lib -I $APRON_PREFIX/lib -use-runtime myrun -o mlexample.byte \
      bigarray.cma gmp.cma apron.cma ppl.cma mlexample.ml

#### Native-code compilation

    ocamlopt -cc "g++" -I $MLGMPIDL_PREFIX/lib -I $APRON_PREFIX/lib -o mlexample.opt \
      bigarray.cmxa gmp.cmxa apron.cmxa ppl.cmxa mlexample.ml

#### Without auto-linking feature

    ocamlopt -cc "g++" -I $MLGMPIDL_PREFIX/lib -I $APRON_PREFIX/lib -noautolink -o mlexample.opt \
      bigarray.cmxa gmp.cmxa apron.cmxa ppl.cmxa mlexample.ml \
      -cclib "-L$MLGMPIDL_PREFIX/lib -L$APRON_PREFIX/lib -L$PPL_PREFIX/lib\
    	  -lap_ppl_caml_debug -lap_ppl_debug -lppl -lgmpxx \
    	  -lapron_caml_debug -lapron_debug \
    	  -lgmp_caml -L$MPFR_PREFIX/lib -lmpfr -L$GMP_PREFIX/lib -lgmp \
    	  -L$CAMLIDL_PREFIX/lib/ocaml -lcamlidl \
    	  -lbigarray"