Polka

This modules defines datatypes, some global read-only variables, and library initialization and finalization functions.

Exceptions and Datatypes

Exception: Overflow of string

Exception raised when an overflow occurs when converting from internal type pkint_t in the C library to OCAML native integer. The exception carries the string representation of the number in base 10.

Datatype: dimsup

type dimsup = { pos: int; nbdims: int; }

Data-type for insertion and deletion of columns in vectors, matrices, and polyhedra.

Initialization and finalization funtions

Function: initialize : bool -> int -> int -> unit

initialize strict maxdims maxrows initializes internal data-structures and global variables of the library:

• strict indicates wether strict inequalities are enabled or not;
• maxdims is the maximum number of dimensions allowed in polyhedra; the maximum number of columns allowed in vectors and matrices is thus equal to this number plus polka_dec (see below);
• maxrows is the maximum number of rows or vectors allowed in matrices.

Set variables strict and dec (see below).

Function: set_gc : int -> unit

Sets the ratio used/max of the OCAML garbage collector for all the abstract objects allocated by POLKA. The default is 2^26, which means that there is at most 64MB of unreclaimed memory.

Function: finalize : unit -> unit

Free internal data-structure used in the libary.

Function: set_widening_affine : unit -> unit

Function: set_widening_linear : unit -> unit

Select respectively the `affine mode" or the "linear mode" for the widening operation on polyhedra (see Widening mode).

Variables

Variable: strict : bool ref

Indicate if strict inequalities are enabled or not.

Variable: dec : int ref

Index of the first "real" dimension in vectors and matrices.