Abstract values and operations of level 1 (ap_abstract1.h)

datatype: ap_abstract1_t

Datatype for abstract values at level 1.

For information:

typedef struct ap_abstract1_t {
  ap_abstract0_t* abstract0;
  ap_environment_t* env;
} ap_abstract1_t;
  /* data structure invariant:
     ap_abstract0_integer_dimension(man,abstract0)== env->intdim &&
     ap_abstract0_real_dimension(man,abstract0)== env->realdim */

datatype: ap_box1_t

typedef struct ap_box1_t {
  ap_interval_t** p;
  ap_environment_t* env;
} ap_box1_t;
void ap_box1_fprint(FILE* stream, ap_box1_t* box);
void ap_box1_clear(ap_box1_t* box);

Most operations are offered in 2 versions: functional or destructive See Abstract values and operations of level 0.

We remind the policy for redimensioning (see Level 1 of the interface):

• For functions taking one abstract value and one expression (or constraint or generator, or array of ...), the environment of the expression should be a sub-environment of the environment of the abstract value. The environment of the result is the environment of the argument abstract value.
• For functions taking several abstract values, their environments should be the same. Otherwise, it is up to the user to move them to a common super-environment (see Environments).

Constructors, Accessors, Tests and Extraction of properties

Operations

Additional functions

Allocating abstract values of level 1

Function: ap_abstract1_t ap_abstract1_copy (ap_manager_t* man, ap_abstract1_t* a)

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

Function: void ap_abstract1_clear (ap_manager_t* man, ap_abstract1_t* a)

Free all the memory used by a.

Function: size_t ap_abstract1_size (ap_manager_t* man, ap_abstract1_t* a)

Return the abstract size of a.

Control of internal representation of abstract values of level 1

Function: void ap_abstract1_minimize (ap_manager_t* man, ap_abstract1_t* a)

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

Function: void ap_abstract1_canonicalize (ap_manager_t* man, ap_abstract1_t* a)

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

Function: int ap_abstract1_hash (ap_manager_t* man, ap_abstract1_t* a)

Return an hash value for a. Two abstract values in canonical from (according to ap_abstract1_canonicalize) and considered as equal by the function ap_abstract1_is_eq are given the same hash value.

Function: void ap_abstract1_approximate (ap_manager_t* man, ap_abstract1_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_abstract1_approximate.

Printing abstract values of level 1

Function: void ap_abstract1_fprint (FILE* stream, ap_manager_t* man, ap_abstract1_t* a)

Print a in a pretty way on the stream.

Function: void ap_abstract1_fprintdiff (FILE* stream, ap_manager_t* man, ap_abstract1_t* a1, ap_abstract1_t* a2)

Print the difference between a1 (old value) and a2 (new value). The meaning of difference is library dependent.

Function: void ap_abstract1_fdump (FILE* stream, ap_manager_t* man, ap_abstract1_t* a)

Dump the internal representation of a for debugging purposes.

Serialization of abstract values of level 1

Function: ap_membuf_t ap_abstract1_serialize_raw (ap_manager_t* man, ap_abstract1_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_abstract1_t ap_abstract1_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 1

Function: ap_abstract1_t ap_abstract1_bottom (ap_manager_t* man, ap_environment_t* env)

Function: ap_abstract1_t ap_abstract1_top (ap_manager_t* man, ap_environment_t* env)

Create resp. a bottom (empty) value and a top (universe) value defined on the environment env.

Function: ap_abstract1_t ap_abstract1_of_box (ap_manager_t* man, ap_environment_t* env, ap_var_t* tvar, ap_interval_t** tinterval, size_t size)

Abstract an hypercube defined by the arrays tvar and tintnerval of size size.

If no inclusion is specified for a variable in the environment, its value is no constrained in the resulting abstract value.

Accessors for abstract values of level 1

Function: ap_dimension_t ap_abstract1_environment (ap_manager_t* man, ap_abstract1_t* a)

Get a reference to the environment of a. Do not free it.

Function: ap_manager_t* ap_abstract1_manager (ap_abstract1_t* a)

Get a reference to the manager contained in a. Do not free it.

Function: ap_dimension_t ap_abstract1_abstract0 (ap_manager_t* man, ap_abstract1_t* a)

Get a reference to the underlying abstract value of level 0 in a. Do not free it.

Tests on abstract values of level 1

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_abstract1_is_bottom (ap_manager_t* man, ap_abstract1_t* a)

Function: bool ap_abstract1_is_top (ap_manager_t* man, ap_abstract1_t* a)

Emtpiness and universality tests.

Function: bool ap_abstract1_is_leq (ap_manager_t* man, ap_abstract1_t* a1, ap_abstract1_t* a2)

Function: bool ap_abstract1_is_eq (ap_manager_t* man, ap_abstract1_t* a1, ap_abstract1_t* a2)

Inclusion and equality tests.

Function: bool ap_abstract1_sat_interval (ap_manager_t* man, ap_abstract1_t* a, ap_var_t var, ap_interval_t* interval)

Is the variable var included in the interval interval in the abstract value a ?

Function: bool ap_abstract1_sat_lincons (ap_manager_t* man, ap_abstract1_t* a, ap_lincons1_t* cons)

Function: bool ap_abstract1_sat_tcons (ap_manager_t* man, ap_abstract1_t* a, ap_tcons1_t* cons)

Does the abstract value a satisfy the constraint cons ?

Function: bool ap_abstract1_is_variable_unconstrained (ap_manager_t* man, ap_abstract1_t* a, ap_var_t var)

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 1

Function: ap_interval_t* ap_abstract1_bound_variable (ap_manager_t* man, ap_abstract1_t* a, ap_var_t var)

Return the interval taken by the variable var over the abstract value a.

Function: ap_interval_t* ap_abstract1_bound_linexpr (ap_manager_t* man, ap_abstract1_t* a, ap_linexpr1_t* expr)

Function: ap_interval_t* ap_abstract1_bound_texpr (ap_manager_t* man, ap_abstract1_t* a, ap_texpr1_t* expr)

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

In the case of truly linear expression, this function allows to solve a Linear Programming (LP) problem, but depending on the underlying domain the solution may be not optimal.

Function: ap_box1_t ap_abstract1_to_box (ap_manager_t* man, ap_abstract1_t* a)

Convert a to an interval/hypercube.

Function: ap_lincons1_array_t ap_abstract1_to_lincons_array (ap_manager_t* man, ap_abstract1_t* a)

Function: ap_tcons1_array_t ap_abstract1_to_tcons_array (ap_manager_t* man, ap_abstract1_t* a)

Convert a to a conjunction of linear (resp. tree) constraints.

The constraints are normally guaranteed to be without intervals.

Function: ap_generator1_array_t ap_abstract1_to_generator_array (ap_manager_t* man, ap_abstract1_t* a)

Convert a to an array of generators.

Meet and Join of abstract values of level 1

Function: ap_abstract1_t ap_abstract1_meet (ap_manager_t* man, bool destructive, ap_abstract1_t* a1, ap_abstract1_t* a2)

Function: ap_abstract1_t ap_abstract1_join (ap_manager_t* man, bool destructive, ap_abstract1_t* a1, ap_abstract1_t* a2)

Meet and Join of 2 abstract values

Function: ap_abstract1_t ap_abstract1_meet_array (ap_manager_t* man, ap_abstract1_t* array, size_t size)

Function: ap_abstract1_t ap_abstract1_join_array (ap_manager_t* man, ap_abstract1_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==1 (no way to define the environment of the result in such a case).

Function: ap_abstract1_t ap_abstract1_meet_lincons_array (ap_manager_t* man, bool destructive, ap_abstract1_t* a, ap_lincons1_array_t* array)

Function: ap_abstract1_t ap_abstract1_meet_tcons_array (ap_manager_t* man, bool destructive, ap_abstract1_t* a, ap_tcons1_array_t* array)

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

Function: ap_abstract1_t ap_abstract1_add_ray_array (ap_manager_t* man, bool destructive, ap_abstract1_t* a, ap_generator1_array_t* array)

Generalized time elapse operator.

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

Assignements and Substitutions of abstract values of level 1

Function: ap_abstract1_t ap_abstract1_assign_linexpr_array (ap_manager_t* man, bool destructive, ap_abstract1_t* org, ap_var_t* tvar, ap_linexpr1_t* texpr, size_t size, ap_abstract1_t* dest)

Function: ap_abstract1_t ap_abstract1_substitute_linexpr_array (ap_manager_t* man, bool destructive, ap_abstract1_t* org, ap_var_t* tvar, ap_linexpr1_t* texpr, size_t size, ap_abstract1_t* dest)

Function: ap_abstract1_t ap_abstract1_assign_texpr_array (ap_manager_t* man, bool destructive, ap_abstract1_t* org, ap_var_t* tvar, ap_texpr1_t* texpr, size_t size, ap_abstract1_t* dest)

Function: ap_abstract1_t ap_abstract1_substitute_texpr_array (ap_manager_t* man, bool destructive, ap_abstract1_t* org, ap_var_t* tvar, ap_texpr1_t* texpr, size_t size, ap_abstract1_t* dest)

Parallel Assignement and Substitution of several variables 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 1

Function: ap_abstract1_t ap_abstract1_forget_array (ap_manager_t* man, bool destructive, ap_abstract1_t* a, ap_var_t* tvar, size_t size, bool project)

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

Change of environments of abstract values of level 1

Function: ap_abstract1_t ap_abstract1_change_environment (ap_manager_t* man, bool destructive, ap_abstract1_t* a, ap_environment_t* nenv, bool project)

Change the environment of the abstract values. Variables that are removed are first existentially quantified, and variables that are introduced are either unconstrained (project==false) or initialized to 0 (project==false).

Function: ap_abstract1_t ap_abstract1_minimize_environment (ap_manager_t* man, bool destructive, ap_abstract1_t* a)

Remove from the environment of the abstract value and from the abstract value itself variables that are unconstrained in it.

Function: ap_abstract1_t ap_abstract1_rename_array (ap_manager_t* man, bool destructive, ap_abstract1_t* a, ap_var_t* tvar, ap_var_t* ntvar, size_t size)

Parallel renaming of the environment of the abstract value. The new variables should not interfere with the variables that are not renamed.

Expansion and Folding of dimensions of abstract values of level 1

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_abstract1_t ap_abstract1_expand (ap_manager_t* man, bool destructive, ap_abstract1_t* a, ap_var_t var, ap_var_t* tvar, size_t size)

Expand the variable var into itself + the size additional variables of the array tvar, which are given the same type as var. The additional variables are added to the environment of the argument for making the environment of the result, so they should not belong to the initial environment.

It results in size+1 unrelated variables having same relations with other dimensions.

Function: ap_abstract1_t ap_abstract1_fold (ap_manager_t* man, bool destructive, ap_abstract1_t* a, ap_var_t* tvar, size_t size)

Fold the variables in the array tvar of size size>=1 and put the result in the first variable in the array. The other variables of the array are then forgot and removed from the environment.

Widening of abstract values of level 1

Function: ap_abstract1_t ap_abstract1_widening (ap_manager_t* man, ap_abstract1_t* a1, ap_abstract1_t* a2)

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

Function: ap_abstract1_t ap_abstract1_widening_threshold (ap_manager_t* man, ap_abstract1_t* a1, ap_abstract1_t* a2, ap_lincons1_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.

Topological closure of abstract values of level 1

Function: ap_abstract1_t* ap_abstract1_closure (ap_manager_t* man, bool destructive, ap_abstract1_t* a)

Relax strict constraints into non strict constraints.

Additional functions on abstract values of level 1

Function: ap_abstract1_t ap_abstract1_of_lincons_array (ap_manager_t* man, ap_environment_t* env, ap_lincons1_array_t* array)

Function: ap_abstract1_t ap_abstract1_of_tcons_array (ap_manager_t* man, ap_environment_t* env, ap_tcons1_array_t* array)

Abstract a conjunction of constraints. The environment of the array should be a subset of the environment env.

Function: ap_abstract1_t ap_abstract1_assign_linexpr (ap_manager_t* man, bool destructive, ap_abstract1_t* org, ap_var_t var, ap_linexpr1_t* expr, ap_abstract1_t* dest)

Function: ap_abstract1_t ap_abstract1_substitute_linexpr (ap_manager_t* man, bool destructive, ap_abstract1_t* org, ap_var_t var, ap_linexpr1_t* expr, ap_abstract1_t* dest)

Function: ap_abstract1_t ap_abstract1_assign_texpr (ap_manager_t* man, bool destructive, ap_abstract1_t* org, ap_var_t var, ap_texpr1_t* expr, ap_abstract1_t* dest)

Function: ap_abstract1_t ap_abstract1_substitute_texpr (ap_manager_t* man, bool destructive, ap_abstract1_t* org, ap_var_t var, ap_texpr1_t* expr, ap_abstract1_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_abstract1_t ap_abstract1_unify (ap_manager_t* man, bool destructive, ap_abstract1_t* a1, ap_abstract1_t* a2)

Unify two abstract values on their common variables, that is, embed them on the least common environment and then compute their meet. The result is defined on the least common environment.

For instance, the unification of 1<=x<=3 and x=y defined on { x, y } and 2<=z<=4 and z=y defined on {y,z } results in 2<=x<=3 and x=y=z defined on {x,y,z}.

Function: ap_linexpr1_t ap_abstract1_quasilinear_of_intlinear (ap_manager_t* man, ap_abstract1_t* a, ap_linexpr1_t* expr)

Evaluate the interval linear expression expr on the abstract value a and approximate it by a quasilinear expression.

This implies calls to ap_abstract0_bound_dimension.

Function: ap_linexpr1_t ap_abstract1_intlinear_of_tree (ap_manager_t* man, ap_abstract1_t* a, ap_texpr1_t* expr, bool quasilinear)

Evaluate the tree expression expr on the abstract value a and approximate it by an interval linear (resp. quasilinear if quasilinear is true) expression.

This implies calls to ap_abstract0_bound_dimension.