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 Compiling and linking client programs against APRON 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"