NewPolka (pk.h): convex polyhedra and linear equalities abstract domains

The NEWPOLKA convex polyhedra and linear equalities library is aimed to be used through the APRON interface. However some specific points should be precised. First, NEWPOLKA can use several underlying representations for numbers, which lead to several library variants. Second, some specific functions are needed, typically to allocate managers, and to specify special options.

Use of NewPolka

To use NEWPOLKA in C, add

#include "pk.h"
#include "pkeq.h"
  /* if you want linear equalities */

in your source file(s) and add ‘-I$(APRON_PREFIX)/include’ in the command line in your Makefile.

You should also link your object files with the NEWPOLKA library to produce an executable, by adding something like ‘-L$(APRON_PREFIX)/lib -lpolkag’ in the command line in your Makefile (followed by the standard ‘-lapron -litvmpq -litvdbl -L$(MPFR_PREFIX)/lib -lmpfr -L$(GMP_PREFIX)/lib -lgmp’).

There are actually several variants of the library:

libpolkai.a

The underlying representation for integers is long int. This may easily cause overflows, especially with many dimensions or variables. Overflows are not detected but usually result in infinite looping. The underlying representation for integers is long long int. This may (less) easily cause overflows.

libpolkag.a

The underlying representation for integers is mpz_t, the multi-precision integers from the GNU GMP library. Overflows are not possible any more, but huge numbers may appear.

All scalars of type double are converted to scalars of type mpq_t inside NewPolka, as NewPolka works internally with exact rational arithmetics. So when possible it is better for the user (in term of efficiency) to convert already double scalars to mpq_t scalars.

There is a way to prevent overflow and/or huge numbers, which is to position the options max_coeff_size and approximate_max_coeff_size, see Allocating NewPolka managers and setting specific options.

Also, all library are available in debug mode (‘libpolkai_debug.a’, ....

Allocating NewPolka managers and setting specific options

datatype: pk_internal_t

NewPolka type for internal managers (specific to NewPolka, and specific to each execution thread in multithreaded programs).

Allocating managers

Function: ap_manager_t* pk_manager_alloc (bool strict)

Allocate an APRON manager for convex polyhedra, linked to the NewPolka library.

The strict option, when true, enables strict constraints in polyhedra (like x>0). Managers in strict mode or in loose mode (strict constraints disabled) are not compatible, and so are corresponding abstract values.

Function: ap_manager_t* pkeq_manager_alloc ()

Allocate an APRON manager for linear equalities, linked to the NewPolka library.

Most options which makes sense for convex polyhedra are meaningless for linear equalities. It is better to set the standard options associated to functions so that abstract values are in canonical form (see NewPolka standard options). This is the default anyway.

Setting options

Options specific to NEWPOLKA are set directly on the internal manager. It can be extracted with the pk_manager_get_internal function.

Function: pk_internal_t* pk_manager_get_internal (ap_manager_t* man)

Return the internal submanager. If man has not been created by pk_manager_alloc or pkeq_manager_alloc, return NULL.

Function: void pk_set_max_coeff_size (pk_internal_t* pk, size_t size)

If size is not 0, try to raise an AP_EXC_OVERFLOW exception as soon as the size of an integer exceed size.

Very incomplete implementation. Currently, used only in libpolkag variant, where the size is the number of limbs as returned by the function mpz_size of the GMP library. This allows to detect huge numbers.

Function: void pk_set_approximate_max_coeff_size (pk_internal_t* pk, size_t size)

This is the parameter to the poly_approximate/ap_abstractX_approximate functions.

Function: size_t pk_get_max_coeff_size (pk_internal_t* pk)

Function: size_t pk_get_approximate_max_coeff_size (pk_internal_t* pk)

Reading the previous parameters.

NewPolka standard options

This section describes the NewPolka options which are selected using the standard mechanism offered by APRON (see Manager options).

Modes

Most functions of NewPolka has two modes. In the lazy mode the canonicalization (computation of the dual representation and minimisation of both representations) of the argument polyhedra is performed only when the needed representation is not available. The resulting polyhedra is in general not in the canonical representation. In the strict mode, argument polyhedra are canonicalized (if they are not yet in canonical form) and the result is (in general) in canonical form.

The strict mode exploits the incremental propery of the Chernikova algorithm and maintain in parallel the constraints and the generators representations. The lazy mode delays computations as much as possible.

Be cautious, in the following table, canonical means minimized constraints and generators representation, but nothing more. In particular, the function canonicalize performs further normalization by normalizing strict constraints (when they exist) and ordering constraints and generators.