Module Polka

`module Polka: `sig` .. `end``
Convex Polyhedra and Linear Equalities abstract domains

`type internal `

Convex Polyhedra and Linear Equalities abstract domains
`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 equalities `
Linear equalities.

Linear equalities are conjunctions of linear equalities of the form `a_0*x_0 + ... + a_n*x_n + b = 0`.

`type `'a` t `
Type of convex polyhedra/linear equalities, where `'a` is `loose`, `strict` or `equalities`.

Abstract values which are convex polyhedra have the type `(loose t) Apron.Abstract0.t` or `(loose t) Apron.Abstract1.t` or `(strict t) Apron.Abstract0.t` or `(strict t) Apron.Abstract1.t`.

Abstract values which are conjunction of linear equalities have the type `(equalities t) Apron.Abstract0.t` or `(equalities t) Apron.Abstract1.t`.

Managers allocated by NewPolka have the type `'a t Apron.Manager.t`.

`val manager_alloc_loose : `unit -> loose t Apron.Manager.t``
Create a NewPolka manager for loose convex polyhedra.
`val manager_alloc_strict : `unit -> strict t Apron.Manager.t``
Create a NewPolka manager for strict convex polyhedra.
`val manager_alloc_equalities : `unit -> equalities t Apron.Manager.t``
Create a NewPolka manager for conjunctions of linear equalities.
`val manager_get_internal : `'a t Apron.Manager.t -> internal``
Get the internal submanager of a NewPolka manager.

Various options. See the C documentation
`val set_max_coeff_size : `internal -> int -> unit``
`val set_approximate_max_coeff_size : `internal -> int -> unit``
`val get_max_coeff_size : `internal -> int``
`val get_approximate_max_coeff_size : `internal -> int``

Type conversions

`val manager_is_polka : `'a Apron.Manager.t -> bool``
`val manager_is_polka_loose : `'a Apron.Manager.t -> bool``
`val manager_is_polka_strict : `'a Apron.Manager.t -> bool``
`val manager_is_polka_equalities : `'a Apron.Manager.t -> bool``
Return `true` iff the argument manager is a polka manager
`val manager_of_polka : `'a t Apron.Manager.t -> 'b Apron.Manager.t``
`val manager_of_polka_loose : `loose t Apron.Manager.t -> 'a Apron.Manager.t``
`val manager_of_polka_strict : `strict t Apron.Manager.t -> 'a Apron.Manager.t``
`val manager_of_polka_equalities : `equalities t Apron.Manager.t -> 'a Apron.Manager.t``
Makes a polka manager generic
`val manager_to_polka : `'a Apron.Manager.t -> 'b t Apron.Manager.t``
`val manager_to_polka_loose : `'a Apron.Manager.t -> loose t Apron.Manager.t``
`val manager_to_polka_strict : `'a Apron.Manager.t -> strict t Apron.Manager.t``
`val manager_to_polka_equalities : `'a Apron.Manager.t -> equalities t Apron.Manager.t``
Instanciate the type of a polka manager. Raises `Failure` if the argument manager is not a polka manager
`module Abstract0: `sig` .. `end``
`module Abstract1: `sig` .. `end``

Compilation information

See `Introduction.compilation` for complete explanations. We just show examples with the file `mlexample.ml`.

Bytecode compilation

```ocamlc -I \$MLGMPIDL_PREFIX/lib -I \$APRON_PREFIX/lib -o mlexample.byte \ bigarray.cma gmp.cma apron.cma polkaMPQ.cma mlexample.ml```

```ocamlc -I \$MLGMPIDL_PREFIX/lib -I \$APRON_PREFIX/lib -make-runtime -o myrun \ bigarray.cma gmp.cma apron.cma polkaMPQ.cma ocamlc -I \$MLGMPIDL_PREFIX/lib -I \$APRON_PREFIX/lib -use-runtime myrun -o mlexample.byte \ bigarray.cma gmp.cma apron.cma polkaMPQ.cma mlexample.ml ```

Native-code compilation

```ocamlopt -I \$MLGMPIDL_PREFIX/lib -I \$APRON_PREFIX/lib -o mlexample.opt \ bigarray.cmxa gmp.cmxa apron.cmxa polkaMPQ.cmxa mlexample.ml ```

```ocamlopt -I \$MLGMPIDL_PREFIX/lib -I \$APRON_PREFIX/lib -noautolink -o mlexample.opt \ bigarray.cmxa gmp.cmxa apron.cmxa polkaMPQ.cmxa mlexample.ml \ -cclib "-L\$MLGMPIDL_PREFIX/lib -L\$APRON_PREFIX/lib \ -lpolkaMPQ_caml_debug -lpolkaMPQ_debug \ -lapron_caml_debug -lapron_debug \ -lgmp_caml -L\$MPFR_PREFIX/lib -lmpfr -L\$GMP_PREFIX/lib -lgmp \ -L\$CAMLIDL_PREFIX/lib/ocaml -lcamlidl \ -lbigarray" ```