[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
This section describes the NewPolka options which are selected using the standard mechanism offered by APRON (see Manager options).
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.
Function | algo | Comments |
copy | Identical representation | |
free | ||
size | Return the number of coefficients. Their size (when using multi-precision integers) is not taken into account. | |
minimize | Require canonicalization. Keep only the smallest representation among the constraints and the generators representation. | |
canonicalize | ||
approximate | Require 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. | |
-1 | Normalize integer minimal constraints. This results in a smaller polyhedra. | |
1 | Remove constraints with coefficients of size (in bits) greater than the approximate_max_coeff_size parameter. | |
2 | Idem, but preserve interval constraints. | |
3 | Idem, but preserve octagonal constraints (+/- xi +/- xj >= cst). | |
10 | Simplify 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 | |
fprint | Require canonicalization. | |
fprintdiff | not implemented | |
fdump | Print raw representations of any of the constraints, generators and saturation matrices that are available. | |
serialize_raw, deserialize_raw | not implemented | |
bottom,top | Return canonical form. | |
of_box | Return constraints. | |
of_lincons_array | Return constraints. | |
>=0 | Take into account interval-linear constraints, after having minimized the quasi-linear constraints | |
<0 | Ignore interval-linear constraints | |
dimension | ||
is_bottom | <0 | If generators not available, return tbool_top |
>=0 | If generators not available, canonicalize and return tbool_false or tbool_true . |
|
is_top | <0 | If not in canonical form, return tbool_top |
>=0 | Require canonical form. | |
is_leq | <=0 | Require generators of first argument and constraints of second argument. |
>0 | Require canonical form for both arguments. | |
is_eq | Require canonical form for both arguments. | |
is_dimension_unconstrained | Require canonical form | |
sat_interval, sat_lincons, bound_dimension, bound_linexpr | <=0 | Require generators. |
>0 | Require canonical form. | |
to_box | <0 | Require generators. |
>=0 | Require canonical form. | |
to_lincons_array, | to_generator_arrayRequire canonical form. | |
meet, meet_array, meet_lincons_array | <0 | Require constraints. Return non-minimized constraints. |
>=0 | Require canonical form. Return canonical form. | |
join, join_array, add_ray_array | <0 | Require generators. Return non-minimized generators. |
>=0 | Require canonical form. Return canonical form. | |
assign_linexpr | 1. If the optional argument is NULL, | |
<=0 | If 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. | |
>0 | Require 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_linexpr | 1. If the optional argument is NULL, | |
<=0 | If 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. | |
>0 | Require 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_array | 1. If the optional argument is NULL, | |
<=0 | If the expr. are deterministic, require generators and return generators Otherwise, require canonical form and return generators. | |
>0 | Require 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_array | 1. If the optional argument is NULL, | |
<=0 | If the expr. are deterministic, require constraints and return constraints Otherwise, require canonical form and return generators. | |
>0 | Require 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 | <=0 | Require generators and return generators. |
>0 | Require canonical form and return canonical form. | |
add_dimensions, permute_dimensions | <=0 | Require any representation and return the updated one. If in canonical form, return canonical form. |
>0 | Require canonical form, return canonical form. | |
remove_dimensions | <=0 | Require generators, return generators. |
>0 | Require canonical form, return canonical form. | |
expand | <0 | Require constraints, return constraints. |
>=0 | Require canonical form, return canonical form. | |
fold | <0 | Require generators, return generators. |
>=0 | Require canonical form, return canonical form. | |
widening | Require canonical form. | |
closure | 1. If pk_manager_alloc() has been given a false Boolean (no strict constraints), same as copy. | |
2. Otherwise, | ||
<0 | Require constraints, return constraints. | |
>=0 | Require canonical form, return constraints. |
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |