Next: , Previous: , Up: Managers and Abstract Domains  

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.


Next: , Up: NewPolka  

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’, ....


Next: , Previous: , Up: NewPolka  

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.


Previous: , Up: NewPolka  

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.

FunctionalgoComments
copyIdentical representation
free
sizeReturn the number of coefficients.
Their size (when using multi-precision integers) is not taken into account.
minimizeRequire canonicalization.

Keep only the smallest representation among the constraints and the generators representation.

canonicalize
approximateRequire constraints.
algo here refers to the explicit parameter of the function. A negative number indicates a possibly smaller result, a positive one a possibly greater one. The effects of the function may be different for 2 identical polyhedra defined by different systems of (non minimal) constraints.
Equalities are never modified.
-1Normalize integer minimal constraints. This results in a smaller polyhedra.
1Remove constraints with coefficients of size (in bits) greater than the approximate_max_coeff_size parameter.
2Idem, but preserve interval constraints.
3Idem, but preserve octagonal constraints (+/- xi +/- xj >= cst).
10Simplify constraints such that the coefficients size (in bits) are less or equal than the approximate_max_coeff_size parameter. The constant coefficients are recomputed by linear programming and are not involved in the reduction process.
Do nothing
fprintRequire canonicalization.
fprintdiffnot implemented
fdumpPrint raw representations of any of the constraints, generators and saturation matrices that are available.
serialize_raw, deserialize_rawnot implemented
bottom,topReturn canonical form.
of_boxReturn constraints.
of_lincons_arrayReturn constraints.
>=0Take into account interval-linear constraints, after having minimized the quasi-linear constraints
<0Ignore interval-linear constraints
dimension
is_bottom<0If generators not available, return tbool_top
>=0If generators not available, canonicalize and return tbool_false or tbool_true.
is_top<0If not in canonical form, return tbool_top
>=0Require canonical form.
is_leq<=0Require generators of first argument and constraints of second argument.
>0Require canonical form for both arguments.
is_eqRequire canonical form for both arguments.
is_dimension_unconstrainedRequire canonical form
sat_interval, sat_lincons, bound_dimension, bound_linexpr<=0Require generators.
>0Require canonical form.
to_box<0Require generators.
>=0Require canonical form.
to_lincons_array, to_generator_arrayRequire canonical form.
meet, meet_array, meet_lincons_array<0Require constraints.
Return non-minimized constraints.
>=0Require canonical form.
Return canonical form.
join, join_array, add_ray_array<0Require generators.
Return non-minimized generators.
>=0Require canonical form.
Return canonical form.
assign_linexpr1. If the optional argument is NULL,
<=0If the expr. is deterministic and invertible, require any representation and return the transformed one. If in canonical form, return canonical form.
If the expr. is deterministic and non-invertible, require generators and return generators
If the expr. is non-deterministic, require constraints and return generators.
>0Require canonical form, return canonical form.
If the expr. is deterministic,(and even more, invertible), the operation is more efficient.
2. If the optional argument is not NULL, first the assignement is performed, and then the meet function is applied with its corresponding option.
substitute_linexpr1. If the optional argument is NULL,
<=0If the expr. is deterministic and invertible, require any representation and return the transformed one. If in canonical form, return canonical form.
If the expr. is deterministic and non-invertible, require constraints and return constraints
If the expr. is non-deterministic, require constraints and return generators.
>0Require canonical form, return canonical form.
If the expr. is deterministic (and even more, invertible), the operation is more efficient.
2. If the optional argument is not NULL, first the substitution is performed, and then the meet function is applied with its corresponding option.
assign_linexpr_array1. If the optional argument is NULL,
<=0If the expr. are deterministic, require generators and return generators
Otherwise, require canonical form and return generators.
>0Require canonical form, return canonical form.
2. If the optional argument is not NULL, first the assignement is performed, and then the meet function is applied with its corresponding option.
substitute_linexpr_array1. If the optional argument is NULL,
<=0If the expr. are deterministic, require constraints and return constraints
Otherwise, require canonical form and return generators.
>0Require canonical form, return canonical form.
2. If the optional argument is not NULL, first the substitution is performed, and then the meet function is applied with its corresponding option.
forget_array<=0Require generators and return generators.
>0Require canonical form and return canonical form.
add_dimensions, permute_dimensions<=0Require any representation and return the updated one.
If in canonical form, return canonical form.
>0Require canonical form, return canonical form.
remove_dimensions<=0Require generators, return generators.
>0Require canonical form, return canonical form.
expand<0Require constraints, return constraints.
>=0Require canonical form, return canonical form.
fold<0Require generators, return generators.
>=0Require canonical form, return canonical form.
wideningRequire canonical form.
closure1. If pk_manager_alloc() has been given a false Boolean (no strict constraints), same as copy.
2. Otherwise,
<0Require constraints, return constraints.
>=0Require canonical form, return constraints.

Previous: , Up: NewPolka