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.
This document was generated
by Bertrand Jeannet on December, 22 2009
using texi2html