/usr/include/pk.h is in libapron-dev 0.9.10-5.2ubuntu3.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 | /* ********************************************************************** */
/* pk.h: Interface of the polka linear relation library */
/* ********************************************************************** */
/* This file is part of the APRON Library, released under LGPL license. Please
read the COPYING file packaged in the distribution */
#ifndef __PK_H__
#define __PK_H__
#ifdef __cplusplus
extern "C" {
#endif
#include "ap_global0.h"
/* The invariant of the representation of a polyhedron is the following: if the
polyhedron is empty, then C==F==satC==satF==0. Otherwise, we have
(C || F) && (satC || satF || !(C && F)).
This means that a non-empty polyhedron has a minimal representation minimal
if and only if C && F if and only if satC || satF. */
typedef enum pk_status_t {
pk_status_conseps=0x1,
pk_status_consgauss=0x2,
pk_status_gengauss=0x4,
pk_status_minimaleps=0x8
} pk_status_t;
struct pk_t {
/* private data: do not use directly ! */
struct matrix_t* C;
struct matrix_t* F;
struct satmat_t* satC;
struct satmat_t* satF;
size_t intdim;
size_t realdim;
size_t nbeq;
size_t nbline;
pk_status_t status;
};
typedef struct pk_t pk_t;
typedef struct pk_internal_t pk_internal_t;
/*
Important remark: the newpolka library is normally intended to be accessed
through the APRON interface, i.e., through abstract0_XX and abstract1_XX
functions. If it is accessed directly with pk_XXX functions, many checks on
arguments will not be performed.
*/
/* ============================================================ */
/* A. Constructor for APRON manager (to be freed with ap_manager_free). */
/* ============================================================ */
ap_manager_t* pk_manager_alloc(bool strict);
/* Allocate a NewPolka manager for convex polyhedra.
If the Boolean parameter is true, abstract values generated with the
manager can have strict constraints (like x>0). Otherwise they are defined
using only loose constraints. Managers and abstract values in strict or
loose mode are incompatible.
*/
/* ============================================================ */
/* B. Options */
/* ============================================================ */
pk_internal_t* pk_manager_get_internal(ap_manager_t* man);
/* For setting options when one has a ap_manager_t object, one can use the
APRON function ap_manager_get_internal with a cast. */
void pk_set_max_coeff_size(pk_internal_t* pk, size_t size);
void pk_set_approximate_max_coeff_size(pk_internal_t* pk, size_t size);
size_t pk_get_max_coeff_size(pk_internal_t* pk);
size_t pk_get_approximate_max_coeff_size(pk_internal_t* pk);
/* ============================================================ */
/* D. Conversions */
/* ============================================================ */
pk_t* pk_of_abstract0(ap_abstract0_t* abstract);
/* Extract from an abstract value the underlying NewPolka polyhedron. There
is no copy, and only the argument should be freed. */
ap_abstract0_t* pk_to_abstract0(ap_manager_t* man, pk_t* poly);
/* Create an abstract value from the manager and the underlying NewPolka
polyhedron. There is no copy, and only the result should be freed
*/
/* ============================================================ */
/* D. Constructor and destructor for internal manager */
/* ============================================================ */
/* Allocates pk and initializes it with a default size */
struct pk_internal_t* pk_internal_alloc(bool strict);
/* Clear and free pk */
void pk_internal_free(pk_internal_t* pk);
/* ********************************************************************** */
/* I. General management */
/* ********************************************************************** */
/* ============================================================ */
/* I.1 Memory */
/* ============================================================ */
pk_t* pk_copy(ap_manager_t* man, pk_t* a);
/* Return a copy of an abstract value, on
which destructive update does not affect the initial value. */
void pk_free(ap_manager_t* man, pk_t* a);
/* Free all the memory used by the abstract value */
size_t pk_size(ap_manager_t* man, pk_t* a);
/* Return the abstract size of a polyhedron, which is the number of
coefficients of its current representation, possibly redundant. */
/* ============================================================ */
/* I.2 Control of internal representation */
/* ============================================================ */
void pk_minimize(ap_manager_t* man, pk_t* a);
/* Minimize the size of the representation of a.
This may result in a later recomputation of internal information.
*/
void pk_canonicalize(ap_manager_t* man, pk_t* a);
/* Put the polyhedron with minimized constraints and frames. If in addition
the integer man->option->canonicalize.algorithm is strictly positive,
normalize equalities and lines, and also strict constraints */
int pk_hash(ap_manager_t* man, pk_t* a);
/* Return an hash value for the abstract value. Two abstract values in
canonical from (according to @code{ap_abstract1_canonicalize}) and
considered as equal by the function ap_abstract0_is_eq are given the
same hash value (this implies more or less a canonical form).
*/
void pk_approximate(ap_manager_t* man, pk_t* a, int algorithm);
/* Perform some transformation on the abstract value, guided by the
field algorithm.
Approximation:
- algorithm==0: do nothing
- algorithm==-1: normalize integer minimal constraints (induces a smaller
polyhedron)
- algorithm==1: remove constraints with coefficients of size greater than
max_coeff_size, if max_coeff_size > 0
- algorithm==2: in addition, keep same bounding box (more precise)
- algorithm==3: in addition, keep same bounding octagon (even more
precise)
- algorithm==10: round constraints with too big coefficients, of size
greater than approximate_max_coeff_size, if
approximate_max_coeff_size>0
*/
/* ============================================================ */
/* I.3 Printing */
/* ============================================================ */
void pk_fprint(FILE* stream,
ap_manager_t* man,
pk_t* a,
char** name_of_dim);
/* Print the abstract value in a pretty way, using function
name_of_dim to name dimensions */
void pk_fprintdiff(FILE* stream,
ap_manager_t* man,
pk_t* a1, pk_t* a2,
char** name_of_dim);
/* Print the difference between a1 (old value) and a2 (new value),
using function name_of_dim to name dimensions.
The meaning of difference is library dependent.
Not implemented */
void pk_fdump(FILE* stream, ap_manager_t* man, pk_t* a);
/* Dump the internal representation of an abstract value,
for debugging purposes */
/* ============================================================ */
/* I.4 Serialization */
/* ============================================================ */
ap_membuf_t pk_serialize_raw(ap_manager_t* man, pk_t* a);
/* Allocate a memory buffer (with malloc), output the abstract value in raw
binary format to it and return a pointer on the memory buffer and the size
of bytes written. It is the user responsability to free the memory
afterwards (with free).
Not implemented */
pk_t* pk_deserialize_raw(ap_manager_t* man, void* ptr, size_t* size);
/* Return the abstract value read in raw binary format from the input stream
and store in size the number of bytes read
Not implemented */
/* ********************************************************************** */
/* II. Constructor, accessors, tests and property extraction */
/* ********************************************************************** */
/* ============================================================ */
/* II.1 Basic constructors */
/* ============================================================ */
/* We assume that dimensions [0..intdim-1] correspond to integer variables, and
dimensions [intdim..intdim+realdim-1] to real variables */
pk_t* pk_bottom(ap_manager_t* man, size_t intdim, size_t realdim);
/* Create a bottom (empty) value */
pk_t* pk_top(ap_manager_t* man, size_t intdim, size_t realdim);
/* Create a top (universe) value */
pk_t* pk_of_box(ap_manager_t* man,
size_t intdim, size_t realdim,
ap_interval_t** tinterval);
/* Abstract an hypercube defined by the array of intervals
of size intdim+realdim */
/* ============================================================ */
/* II.2 Accessors */
/* ============================================================ */
ap_dimension_t pk_dimension(ap_manager_t* man, pk_t* a);
/* Return the total number of dimensions of the abstract values */
/* ============================================================ */
/* II.3 Tests */
/* ============================================================ */
bool pk_is_bottom(ap_manager_t* man, pk_t* a);
/* Emptiness test
algorithm >= 0: strict behaviour, compute canonical form if necessary
algorithm < 0: lazy behaviour, always cheap
*/
bool pk_is_top(ap_manager_t* man, pk_t* a);
/* Universe test
algorithm >= 0: strict behaviour, compute canonical form if necessary
algorithm < 0: lazy behaviour, always cheap
*/
bool pk_is_leq(ap_manager_t* man, pk_t* a1, pk_t* a2);
/* Inclusion test:
Is always strict
algorithm > 0: (nearly always) compute canonical forms
algorithm <= 0: compute dual representations only if necessary
*/
bool pk_is_eq(ap_manager_t* man, pk_t* a1, pk_t* a2);
/* Equality test:
Is always strict
Use algorithm field of is_leq.
*/
bool pk_sat_lincons(ap_manager_t* man, pk_t* a, ap_lincons0_t* lincons);
/* Satisfiability of a linear constraint
Is always strict
algorithm > 0: (nearly always) compute canonical form
algorithm <= 0: compute dual representation only if necessary
*/
bool pk_sat_tcons(ap_manager_t* man, pk_t* a, ap_tcons0_t* cons);
/* Satisfiability of a tree expression constraint. */
bool pk_sat_interval(ap_manager_t* man, pk_t* a,
ap_dim_t dim, ap_interval_t* interval);
/* Inclusion of a dimension in an interval
Is always strict
algorithm > 0: (nearly always) compute canonical form
algorithm <= 0: compute dual representation only if necessary
*/
bool pk_is_dimension_unconstrained(ap_manager_t* man, pk_t* po,
ap_dim_t dim);
/* Is a dimension unconstrained ?
Is always strict
algorithm > 0: compute canonical form
algorithm <= 0: compute dual representation only if necessary
*/
/* ============================================================ */
/* II.4 Extraction of properties */
/* ============================================================ */
ap_interval_t* pk_bound_linexpr(ap_manager_t* man,
pk_t* a, ap_linexpr0_t* expr);
/* Returns the interval taken by a linear expression
over the abstract value.
algorithm > 0: compute canonical form
algorithm <= 0: compute dual representation only if necessary
*/
ap_interval_t* pk_bound_texpr(ap_manager_t* man,
pk_t* a, ap_texpr0_t* expr);
/* Returns the interval taken by a tree expression
over the abstract value. */
ap_interval_t* pk_bound_dimension(ap_manager_t* man,
pk_t* a, ap_dim_t dim);
/* Returns the interval taken by the dimension
over the abstract value
algorithm > 0: compute canonical form
algorithm <= 0: compute dual representation only if necessary
*/
ap_lincons0_array_t pk_to_lincons_array(ap_manager_t* man, pk_t* a);
/* Converts an abstract value to a polyhedra
(conjunction of linear constraints).
Always consider canonical form */
ap_tcons0_array_t pk_to_tcons_array(ap_manager_t* man, pk_t* a);
/* Converts an abstract value to a
conjunction of tree expressions constraints. */
ap_interval_t** pk_to_box(ap_manager_t* man, pk_t* a);
/* Converts an abstract value to an interval/hypercube.
The size of the resulting array is pk_dimension(man,a). This
function can be reimplemented by using pk_bound_linexpr
algorithm >= 0: compute canonical form
algorithm < 0: compute dual representation only if necessary
*/
ap_generator0_array_t pk_to_generator_array(ap_manager_t* man, pk_t* a);
/* Converts an abstract value to a system of generators.
Always consider canonical form. */
/* ********************************************************************** */
/* III. Operations */
/* ********************************************************************** */
/* ============================================================ */
/* III.1 Meet and Join */
/* ============================================================ */
pk_t* pk_meet(ap_manager_t* man, bool destructive, pk_t* a1, pk_t* a2);
pk_t* pk_join(ap_manager_t* man, bool destructive, pk_t* a1, pk_t* a2);
/* Meet and Join of 2 abstract values */
pk_t* pk_meet_array(ap_manager_t* man, pk_t** tab, size_t size);
pk_t* pk_join_array(ap_manager_t* man, pk_t** tab, size_t size);
/* Meet and Join of a non empty array of abstract values. */
pk_t* pk_meet_lincons_array(ap_manager_t* man,
bool destructive, pk_t* a,
ap_lincons0_array_t* array);
pk_t* pk_meet_tcons_array(ap_manager_t* man,
bool destructive, pk_t* a,
ap_tcons0_array_t* array);
/* Meet of an abstract value with a set of constraints. */
pk_t* pk_add_ray_array(ap_manager_t* man,
bool destructive, pk_t* a,
ap_generator0_array_t* array);
/* Generalized time elapse operator */
/* ============================================================ */
/* III.2 Assignement and Substitutions */
/* ============================================================ */
pk_t* pk_assign_linexpr_array(ap_manager_t* man,
bool destructive, pk_t* a,
ap_dim_t* tdim,
ap_linexpr0_t** texpr,
size_t size,
pk_t* dest);
pk_t* pk_substitute_linexpr_array(ap_manager_t* man,
bool destructive, pk_t* a,
ap_dim_t* tdim,
ap_linexpr0_t** texpr,
size_t size,
pk_t* dest);
pk_t* pk_assign_texpr_array(ap_manager_t* man,
bool destructive, pk_t* a,
ap_dim_t* tdim,
ap_texpr0_t** texpr,
size_t size,
pk_t* dest);
pk_t* pk_substitute_texpr_array(ap_manager_t* man,
bool destructive, pk_t* a,
ap_dim_t* tdim,
ap_texpr0_t** texpr,
size_t size,
pk_t* dest);
/* Parallel Assignement and Substitution of several dimensions by interval
expressons. */
/* ============================================================ */
/* III.3 Projections */
/* ============================================================ */
pk_t* pk_forget_array(ap_manager_t* man,
bool destructive, pk_t* a,
ap_dim_t* tdim, size_t size,
bool project);
/* ============================================================ */
/* III.4 Change and permutation of dimensions */
/* ============================================================ */
pk_t* pk_add_dimensions(ap_manager_t* man,
bool destructive, pk_t* a,
ap_dimchange_t* dimchange,
bool project);
pk_t* pk_remove_dimensions(ap_manager_t* man,
bool destructive, pk_t* a,
ap_dimchange_t* dimchange);
pk_t* pk_permute_dimensions(ap_manager_t* man,
bool destructive,
pk_t* a,
ap_dimperm_t* permutation);
/* ============================================================ */
/* III.5 Expansion and folding of dimensions */
/* ============================================================ */
pk_t* pk_expand(ap_manager_t* man,
bool destructive, pk_t* a,
ap_dim_t dim,
size_t n);
/* Expand the dimension dim into itself + n additional dimensions.
It results in (n+1) unrelated dimensions having same
relations with other dimensions. The (n+1) dimensions are put as follows:
- original dimension dim
- if the dimension is integer, the n additional dimensions are put at the
end of integer dimensions; if it is real, at the end of the real
dimensions.
*/
pk_t* pk_fold(ap_manager_t* man,
bool destructive, pk_t* a,
ap_dim_t* tdim,
size_t size);
/* Fold the dimensions in the array tdim of size n>=1 and put the result
in the first dimension in the array. The other dimensions of the array
are then removed (using pk_permute_remove_dimensions). */
/* ============================================================ */
/* III.6 Widening */
/* ============================================================ */
/* Widening */
pk_t* pk_widening(ap_manager_t* man, pk_t* a1, pk_t* a2);
/* ============================================================ */
/* III.7 Closure operation */
/* ============================================================ */
/* Returns the topological closure of a possibly opened abstract value */
pk_t* pk_closure(ap_manager_t* man, bool destructive, pk_t* a);
#ifdef __cplusplus
}
#endif
#endif
|