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

Without auto-linking feature

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"