Abstract values and operations of level 0 (ap_abstract0.h)

datatype: ap_abstract0_t

Datatype for abstract values at level 0.

Most operations are offered in 2 versions: functional or destructive. In such a case, the Boolean argument destructive controls the behaviour of the functionn:

• In the destructive semantics, after the call the first abstract value in the arguments of the function is destroyed and should not be referenced any more. Although the returned value might actually be equal to the (destroyed) argument, the user just manipulates the returned value and never refers directly to the (destroyed) argument.
• In the functional semantics, the first abstract value in the arguments is neither (semantically) modified nor deallocated.

Constructors, Accessors, Tests and Extraction of properties

Operations

Additional functions

Allocating abstract values of level 0

Function: ap_abstract0_t* ap_abstract0_copy (ap_manager_t* man, ap_abstract0_t* a)

Return a copy of a, on which destructive update does not affect a.

Function: void ap_abstract0_free (ap_manager_t* man, ap_abstract0_t* a)

Free all the memory used by a.

Function: size_t ap_abstract0_size (ap_manager_t* man, ap_abstract0_t* a)

Return the abstract size of a.

Control of internal representation of level 0

Function: void ap_abstract0_minimize (ap_manager_t* man, ap_abstract0_t* a)

Minimize the size of the representation of a. This may result in a later recomputation of internal information.

Function: void ap_abstract0_canonicalize (ap_manager_t* man, ap_abstract0_t* a)

Put a in canonical form. (not yet clear definition)

Function: int ap_abstract0_hash (ap_manager_t* man, ap_abstract0_t* a)

Return an hash value for a. Two abstract values in canonical from (according to ap_abstract0_canonicalize) and considered as equal by the function ap_abstract0_is_eq should be given the same hash value (this implies more or less a canonical form).

Function: void ap_abstract0_approximate (ap_manager_t* man, ap_abstract0_t* a, int algorithm)

Perform some transformation on a, guided by the field algorithm.

The transformation may lose information. The argument algorithm overrides the field algorithm of the structure of type ap_funopt_t associated to ap_abstract0_approximate.

Printing abstract values of level 0

Function: void ap_abstract0_fprint (FILE* stream, ap_manager_t* man, ap_abstract0_t* a, char** name_of_dim)

Print a in a pretty way, using array name_of_dim to name dimensions.. If name_of_dim is NULL, use the default names x0, x1, ....

Function: void ap_abstract0_fprintdiff (FILE* stream, ap_manager_t* man, ap_abstract0_t* a1, ap_abstract0_t* a2, char** name_of_dim)

Print the difference between a1 (old value) and a2 (new value), using array name_of_dim to name dimensions. The meaning of difference is library dependent.

Function: void ap_abstract0_fdump (FILE* stream, ap_manager_t* man, ap_abstract0_t* a)

Dump the internal representation of a for debugging purposes.

Serialization of abstract values of level 0

Function: ap_membuf_t ap_abstract0_serialize_raw (ap_manager_t* man, ap_abstract0_t* a)

Allocate a memory buffer (with malloc), output a in raw binary format to it and return a pointer on the memory buffer and the number of bytes written. It is the user responsability to free the memory afterwards (with free).

Function: ap_abstract0_t* ap_abstract0_deserialize_raw (ap_manager_t* man, void* ptr, size_t* size)

Return the abstract value read in raw binary format from the buffer pointed by ptr and store in size the number of bytes read.

Constructors for abstract values of level 0

Function: ap_abstract0_t* ap_abstract0_bottom (ap_manager_t* man, size_t intdim, size_t realdim)

Function: ap_abstract0_t* ap_abstract0_top (ap_manager_t* man, size_t intdim, size_t realdim)

Create resp. a bottom (empty) value and a top (universe) value with intdim integer dimensions and realdim real dimensions.

Function: ap_abstract0_t* ap_abstract0_of_box (ap_manager_t* man, size_t intdim, size_t realdim, ap_interval_t** array)

Abstract an hypercube defined by the array of intervals array of size intdim+realdim.

Accessors for abstract values of level 0

Function: ap_dimension_t ap_abstract0_dimension (ap_manager_t* man, ap_abstract0_t* a)

Return the dimensionality of a.

Tests on abstract values of level 0

In abstract tests,

• true means that the predicate is certainly true;
• false means false or don’t know (an exception has occurred, or the exact computation was considered too expensive to be performed, according to the options).

Function: bool ap_abstract0_is_bottom (ap_manager_t* man, ap_abstract0_t* a)

Function: bool ap_abstract0_is_top (ap_manager_t* man, ap_abstract0_t* a)

Emtpiness and universality tests.

Function: bool ap_abstract0_is_leq (ap_manager_t* man, ap_abstract0_t* a1, ap_abstract0_t* a2)

Function: bool ap_abstract0_is_eq (ap_manager_t* man, ap_abstract0_t* a1, ap_abstract0_t* a2)

Inclusion and equality tests.

Function: bool ap_abstract0_sat_interval (ap_manager_t* man, ap_abstract0_t* a, ap_dim_t dim, ap_interval_t* interval)

Is the dimension dim included in the interval interval in the abstract value a ?

Function: bool ap_abstract0_sat_lincons (ap_manager_t* man, ap_abstract0_t* a, ap_lincons0_t* cons)

Function: bool ap_abstract0_sat_tcons (ap_manager_t* man, ap_abstract0_t* a, ap_tcons0_t* cons)

Does the abstract value a satisfy the constraint cons ?

Function: bool ap_abstract0_is_dimension_unconstrained (ap_manager_t* man, ap_abstract0_t* a, ap_dim_t dim)

Is the dimension dim unconstrained in the abstract value a ? If it is the case, we have forget(man,a,dim) == a.

Extraction of properties of abstract values of level 0

Function: ap_interval_t* ap_abstract0_bound_dimension (ap_manager_t* man, ap_abstract0_t* a, ap_dim_t dim)

Return the interval taken by the dimension dim over the abstract valuea

Function: ap_interval_t* ap_abstract0_bound_linexpr (ap_manager_t* man, ap_abstract0_t* a, ap_linexpr0_t* expr)

Function: ap_interval_t* ap_abstract0_bound_texpr (ap_manager_t* man, ap_abstract0_t* a, ap_texpr0_t* expr)

Return the interval taken by a linear expression expr over the abstract value a.

This function allows to solve a Linear Programming (LP) problem, but depending on the underlying domain the solution may be not optimal.

Function: ap_interval_t** ap_abstract0_to_box (ap_manager_t* man, ap_abstract0_t* a)

Convert a to an interval/hypercube. The size of the resulting array is ap_abstract0_dimension(man,a).

Function: ap_lincons0_array_t ap_abstract0_to_lincons_array (ap_manager_t* man, ap_abstract0_t* a)

Function: ap_tcons0_array_t ap_abstract0_to_tcons_array (ap_manager_t* man, ap_abstract0_t* a)

Convert a to a conjunction of constraints.

The constraints are normally guaranteed to be scalar (without intervals)

Function: ap_generator0_array_t ap_abstract0_to_generator_array (ap_manager_t* man, ap_abstract0_t* a)

Convert a to an array of generators.

Meet and Join of abstract values of level 0

Function: ap_abstract0_t* ap_abstract0_meet (ap_manager_t* man, bool destructive, ap_abstract0_t* a1, ap_abstract0_t* a2)

Function: ap_abstract0_t* ap_abstract0_join (ap_manager_t* man, bool destructive, ap_abstract0_t* a1, ap_abstract0_t* a2)

Meet and Join of 2 abstract values

Function: ap_abstract0_t* ap_abstract0_meet_array (ap_manager_t* man, ap_abstract0_t** array, size_t size)

Function: ap_abstract0_t* ap_abstract0_join_array (ap_manager_t* man, ap_abstract0_t** array, size_t size)

Meet and Join of the array array of abstract values of size size.

Raise an AP_EXC_INVALID_ARGUMENT exception if size==0 (no way to define the dimensionality of the result in such a case).

Function: ap_abstract0_t* ap_abstract0_meet_lincons_array (ap_manager_t* man, bool destructive, ap_abstract0_t* a, ap_lincons0_array_t* array)

Function: ap_abstract0_t* ap_abstract0_meet_tcons_array (ap_manager_t* man, bool destructive, ap_abstract0_t* a, ap_tcons0_array_t* array)

Meet of the abstract value a with the set of constraints array.

array should have exactly the same dimensionality as a.

Function: ap_abstract0_t* ap_abstract0_add_ray_array (ap_manager_t* man, bool destructive, ap_abstract0_t* a, ap_generator0_array_t* array)

Generalized time elapse operator.

array is supposed to contain only rays or lines, no vertices.

array should have exactly the same dimensionality as a.

Assignements and Substitutions of abstract values of level 0

Function: ap_abstract0_t* ap_abstract0_assign_linexpr_array (ap_manager_t* man, bool destructive, ap_abstract0_t* org, ap_dim_t* tdim, ap_linexpr0_t** texpr, size_t size, ap_abstract0_t* dest)

Function: ap_abstract0_t* ap_abstract0_substitute_linexpr_array (ap_manager_t* man, bool destructive, ap_abstract0_t* org, ap_dim_t* tdim, ap_linexpr0_t** texpr, size_t size, ap_abstract0_t* dest)

Function: ap_abstract0_t* ap_abstract0_assign_texpr_array (ap_manager_t* man, bool destructive, ap_abstract0_t* org, ap_dim_t* tdim, ap_texpr0_t** texpr, size_t size, ap_abstract0_t* dest)

Function: ap_abstract0_t* ap_abstract0_substitute_texpr_array (ap_manager_t* man, bool destructive, ap_abstract0_t* org, ap_dim_t* tdim, ap_texpr0_t** texpr, size_t size, ap_abstract0_t* dest)

Parallel Assignement and Substitution of several dimensions by expressions in abstract value org.

dest is an optional argument. If not NULL, semantically speaking, the result of the transformation is intersected with dest. This is useful for precise backward transformations in lattices like intervals or octagons.

Existential quantification of abstract values of level 0

Function: ap_abstract0_t* ap_abstract0_forget_array (ap_manager_t* man, bool destructive, ap_abstract0_t* a, ap_dim_t* tdim, size_t size, bool project)

Forget (project=false) or Project (project=true) the array of dimensions tdim of size size in the abstract value a.

Change and permutation of dimensions of abstract values of level 0

Function: ap_abstract0_t* ap_abstract0_add_dimensions (ap_manager_t* man, bool destructive, ap_abstract0_t* a, ap_dimchange_t* dimchange, bool project)

Function: ap_abstract0_t* ap_abstract0_remove_dimensions (ap_manager_t* man, bool destructive, ap_abstract0_t* a, ap_dimchange_t* dimchange)

Addition and Removal of dimensions in a according to dimchange. In the case of addition, new dimensions are either unconstrained (project==false) or initialized to 0 ((project==true).

Function: ap_abstract0_t* ap_abstract0_apply_dimchange2 (ap_manager_t* man, bool destructive, ap_abstract0_t* a, ap_dimchange2_t* dimchange2, bool project)

Apply the transformation specified by dimchange2. New dimensions are either unconstrained (project==false) or initialized to 0 ((project==true).

Function: ap_abstract0_t* ap_abstract0_permute_dimensions (ap_manager_t* man, bool destructive, ap_abstract0_t* a, ap_dimperm_t* perm)

Permute the dimensions of a according to the permutation perm.

The size of the permutation is supposed to be large enough w.r.t. a.

Expansion and Folding of dimensions of abstract values of level 0

Formally, expanding z into z and w in abstract value (predicate) P is defined by expand(P(x,y,z),z,w) = P(x,y,z) and P(x,y,w).

Conversely, folding z and w into z in abstract value (predicate) Q is defined by fold(Q(x,y,z,w),z,w) = (exists w: Q(x,y,z,w)) or (exists z:Q(x,y,z,w)[z<-w]).

Function: ap_abstract0_t* ap_abstract0_expand (ap_manager_t* man, bool destructive, ap_abstract0_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 dim 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.

Function: ap_abstract0_t* ap_abstract0_fold (ap_manager_t* man, bool destructive, ap_abstract0_t* a, ap_dim_t* tdim, size_t size)

Fold the dimensions in the array tdim of size size>=1 and put the result in the first dimension in the array assumed to be sorted. The other dimensions of the array are then removed.

Widening of abstract values of level 0

Function: ap_abstract0_t* ap_abstract0_widening (ap_manager_t* man, ap_abstract0_t* a1, ap_abstract0_t* a2)

Widening of a1 with a2. a1 is supposed to be included in a2.

Topological closure of abstract values of level 0

Function: ap_abstract0_t* ap_abstract0_closure (ap_manager_t* man, bool destructive, ap_abstract0_t* a)

Relax strict constraints into non strict constraints.

Additional functions on abstract values of level 0

These functions do not have corresponding functions into underlying libraries.

Function: ap_manager_t* ap_abstract0_manager (ap_abstract0_t* a)

Return a reference to the manager contained in a.

The reference should not be freed.

Function: ap_abstract0_t* ap_abstract0_of_lincons_array (ap_manager_t* man, size_t intdim, size_t realdim, ap_lincons0_array_t* array)

Function: ap_abstract0_t* ap_abstract0_of_tcons_array (ap_manager_t* man, size_t intdim, size_t realdim, ap_tcons0_array_t* array)

Abstract a conjunction of constraints. The constraints in the array should have exactly the dimensions (intdim,realdim).

Function: ap_abstract0_t* ap_abstract0_assign_linexpr (ap_manager_t* man, bool destructive, ap_abstract0_t* org, ap_dim_t dim, ap_linexpr0_t* expr, ap_abstract0_t* dest)

Function: ap_abstract0_t* ap_abstract0_substitute_linexpr (ap_manager_t* man, bool destructive, ap_abstract0_t* org, ap_dim_t dim, ap_linexpr0_t* expr, ap_abstract0_t* dest)

Function: ap_abstract0_t* ap_abstract0_assign_texpr (ap_manager_t* man, bool destructive, ap_abstract0_t* org, ap_dim_t dim, ap_texpr0_t* expr, ap_abstract0_t* dest)

Function: ap_abstract0_t* ap_abstract0_substitute_texpr (ap_manager_t* man, bool destructive, ap_abstract0_t* org, ap_dim_t dim, ap_texpr0_t* expr, ap_abstract0_t* dest)

Assignement and Substitution of the dimension dim by the expression expr in abstract value org.

dest is an optional argument. If not NULL, semantically speaking, the result of the transformation is intersected with dest. This is useful for precise backward transformations in lattices like intervals or octagons.

Function: ap_abstract0_t* ap_abstract0_widening_threshold (ap_manager_t* man, ap_abstract0_t* a1, ap_abstract0_t* a2, ap_lincons0_array_t* array)

Widening with threshold.

Intersect the result of the standard widening with all the constraints in array that are satisfied by both a1 and a2.