Home

Integer Set Library: Manual

Contents

1. __isl_give isl basic set isl_basic_map_wrap isl take isl basic map bmap isl give isl set isl map wrap isl take isl map map isl give isl union set isl union map wrap isl take isl union map umap isl give isl basic map isl basic set unwrap isl take isl basic set bset isl give isl map isl set unwrap isl take isl set set isl give isl union map isl union set unwrap isl take isl union set uset e Flattening Remove any internal structure of domain and range of the given set or relation If there is any such internal structure in the input then the name of the space is also removed __isl_give isl set isl set flatten isl take isl set set isl give isl map isl map flatten isl take isl map map isl give isl map isl set flatten map isl take isl set set The function above constructs a relation that maps the input set to a flattened version of the set 28 e Dimension manipulation __isl_give isl_set isl_set_add_dims __isl_take isl set set enum isl dim tvpe tvpe unsigned n isl give isl map isl map add dims isl take isl map map enum isl dim tvpe tvpe unsigned n It is usually not advisable to directly change the input or output space of a set or a relation as this removes the name and the internal structure of the space However the above functions can be useful to add new parameters 1 3 11 Binary
2. i lt 2 j 1 and i lt n and j lt 2i 4 and j lt n 3 R3 n gt i j gt i 1 j 1 i lt 2 j 1 and i lt n 1 and j lt 21 1 andj lt n 1 RI R3 R3 RI R2 R3 R3 R2 R can therefore be moved forward in any path For the other two basic relations we have both R o Ri Rio R and R o R R o Ri and so Ri and R form a strongly connected component By computing the power of R3 and Ri U Ro separately and composing the results the power of R can be computed exactly using 2 5 As explained by Beletska et al 2009 applying the same formula to R directly without a decomposition would result in an overapproximation of the power 2 4 5 Partitioning the domains and ranges of R The algorithm of assumes that the input relation R can be treated as a union of translations This is a reasonable assumption if R maps elements of a given abstract domain to the same domain However if R is a union of relations that map between different domains then this assumption no longer holds In particular when an entire dependence graph is encoded in a single relation as is done by e g Section 6 1 then it does not make sense to look at differences between iterations of different domains Now arguably a modified Floyd Warshall algorithm should be applied to the dependence graph as advocated by Kelly et al 19960 with the transitive closure operation only being applied to relations from
3. 31 __isl_give isl_map isl_map_gist __isl_take isl_map map __isl_take isl_map context isl give isl union map isl union map gist isl take isl union map umap isl take isl union map context The gist operation returns a set or relation that has the same intersection with the context as the input set or relation Any implicit equality in the intersection is made explicit in the result while all inequalities that are redundant with respect to the intersection are removed In case of union sets and relations the gist operation is performed per space Lexicographic Optimization Given a basic set set or bset and a zero dimensional domain dom the following functions compute a set that contains the lexicographic minimum or maximum of the elements in set or bset for those values of the parameters that satisfy dom If empty is not NULL then empty is assigned a set that contains the parameter values in dom for which set or bset has no elements In other words the union of the parameter values for which the result is non empty and of empty is equal to dom __isl_give isl_set isl_basic_set_partial_lexmin __isl_take isl basic set bset isl take isl basic set dom isl give isl set empty isl give isl set isl basic set partial lexmax isl take isl basic set bset isl take isl basic set dom isl give isl set empty isl give isl set isl set partial lexmin isl take i
4. function to find out whether a constraint represents an equality If not it represents an inequality int isl_constraint_is_equality __isl_keep isl_constraint constraint The coefficients of the constraints can be inspected using the following functions void isl_constraint_get_constant isl keep isl_constraint constraint isl_int v void isl constraint get coefficient isl keep isl constraint constraint enum isl dim tvpe type int pos isl int v The explicit representations of the existentiallv quantified variables can be inspected using the following functions Note that the user is only allowed to use these func tions if the inspected set or map is the result of a call to isl_set_compute_divs or isl_map_compute_divs 20 __isl_give isl_div isl_constraint_div __isl_keep isl_constraint constraint int pos void isl div get constant isl keep isl_div div isl int v void isl div get denominator isl keep isl div div isl int v void isl div get coefficient isl keep isl div div enum isl dim tvpe type int pos isl int v To obtain the constraints of a basic set or map in matrix form use the following functions isl give isl mat isl basic set equalities matrix isl keep isl basic set bset enum isl dim tvpe cl enum isl dim tvpe c2 enum isl dim tvpe c3 enum isl dim tvpe c4 isl give isl mat isl basic set inequalities matrix isl keep isl basic set bset enum isl d
5. is _int_fdiv_q_ui 1i j isl int read r s isl int print out i width isl int sgn i isl_int_cmp i j isl int cmp si i si isl int eq i j isl int ne i j isl int It i j isl int le i j isl int gt i j isl int ge ijj isl int abs eq i j isl int abs ne i j is _int_abs_It i j is _int_abs_gt i j is _int_abs_ge i j isl int is zero i isl int is one i isl int is negone i isl int is pos i isl int is neg i isl int is nonpos i isl int is nonneg i isl int is divisible bv i j 1 3 3 Sets and Relations isl uses six types of objects for representing sets and relations isl_basic_set isl basic map isl set isl map isl union set and isl_union_map isl basic set and isl basic map represent sets and relations that can be described as a conjunction of affine constraints while isl set and isl map represent unions of isl basic sets and isl basic maps respectivelv However allisl basic setsorisl basic maps in the union need to have the same dimension isl union sets and isl union maps represent unions of isl sets or isl maps of different dimensions where dimensions with different space names see Dimension Specifications are considered different as well The difference between sets and relations maps is that sets have one set of vari ables while relations have two sets of variables input variables and output variables 1 3 4 Memory Management Since a high level operation on sets and or relations usually
6. of all dimensions 36 isl give isl qpolvnomial isl qpolvnomial set dim name isl take isl qpolvnomial qp enum isl dim tvpe tvpe unsigned pos const char s isl give isl pw qpolvnomial isl pw qpolvnomial set dim name isl take isl pw qpolvnomial pwqp enum isl dim tvpe tvpe unsigned pos const char s Creating New Piecewise Quasipolynomials Some simple quasipolynomials can be created using the following functions More complicated quasipolynomials can be created by applying operations such as addition and multiplication on the resulting quasipolynomials isl give isl qpolvnomial isl_qpolynomial_zero isl take isl_dim dim isl give isl qpolvnomial isl qpolvnomial one C isl take isl dim dim isl give isl qpolvnomial isl qpolvnomial inftv isl take isl dim dim isl give isl qpolvnomial isl qpolvnomial neginftv isl take isl_dim dim isl give isl qpolvnomial isl qpolvnomial nan isl take isl_dim dim isl give isl qpolvnomial isl qpolvnomial rat cst isl take isl dim dim const isl int n const isl int d isl give isl qpolvnomial isl_qpolynomial_div isl take isl div div isl give isl qpolvnomial isl qpolvnomial varc isl take isl_dim dim enum isl dim tvpe tvpe unsigned pos The zero piecewise quasipolvnomial or a piecewise quasipolvnomial with a sin gle cell can be created using the following functions Multiple of t
7. proposed by Kelly et al 1996c C R D Ri is not a union and for each j i the condition C R D Ri o R o C R D Ri R holds 63 Bibliography Barthou D A Cohen and J F Collard 2000 Maximal static expansion Int J Parallel Program 28 3 213 243 59 Beletska A D Barthou W Bielecki and A Cohen 2009 Computing the transi tive closure of a union of affine integer tuple relations In COCOA 09 Proceed ings of the 3rd International Conference on Combinatorial Optimization and Applications Berlin Heidelberg pp 98 109 Springer Verlag 6253 58 50 Kelly W V Maslov W Pugh E Rosser T Shpeisman and D Wonnacott 1996a November The Omega calculator and library Technical report University of Maryland 581 Kellv W V Maslov W Pugh E Rosser T Shpeisman and D Wonnacott 1996b November The Omega librarv Technical report Universitv of Marvland Kellv W W Pugh E Rosser and T Shpeisman 1996c Transitive closure of in finite graphs and its applications In C H Huang P Sadavappan U Banerjee D Gelernter A Nicolau and D A Padua Eds Languages and Compilers for Parallel Computing 8th International Workshop LCPC 95 Columbus Ohio USA August 10 12 1995 Proceedings Volume 1033 of Lecture Notes in Com puter Science pp 126 140 Springer Schrijver A 1986 Theory of Linear and Integer Programming John Wiley amp Sons 55
8. umap isl take isl union set uset isl give isl union map isl union map intersect isl take isl union map umapl isl take isl union map umap2 e Union isl give isl set isl basic set union isl take isl basic set bseti isl take isl basic set bset2 isl give isl map isl basic map union isl take isl basic map bmapl isl take isl basic map bmap2 isl give isl set isl set union isl take isl set setl isl take isl set set2 isl give isl map isl map union isl take isl map map1 isl take isl map map2 isl give isl union set isl union set union isl take isl union set useti isl take isl union set uset2 isl give isl union map isl union map union isl take isl union map umapl isl take isl union map umap2 e Set difference isl give isl set isl set subtract isl take isl set setl isl take isl set set2 isl give isl map isl map subtract isl take isl map map1 isl take isl map map2 isl give isl union set isl union set subtract isl take isl union set useti isl take isl union set uset2 isl give isl union map isl union map subtract 30 e Application __isl_take __isl_take isl union map umap1 isl union map umap2 isl give isl basic set isl basic set applv isl take isl take isl give isl set isl take isl take
9. vertex void isl vertex free isl take isl vertex vertex 47 isl_vertex_get_expr returns a singleton parametric set describing the vertex while isl_vertex_get_domain returns the activity domain of the vertex Note that isl_vertex_get_domain and isl vertex get expr return rational basic sets so they should mainly be used for inspection and should not be mixed with integer sets Chambers can be inspected and destroyed using the following functions isl_ctx isl_cell_get_ctx __isl_keep isl cell cell isl give isl basic set isl cell get domain isl keep isl cell cell void isl cell free isl take isl cell cell 1 4 Applications Although isl is mainly meant to be used as a library it also contains some basic applications that use some of the functionality of isl The input may be specified in either the isl format or the PolyLib format 1 4 1 isl polvhedron sample isl polvhedron sample takes a polvhedron as input and prints an integer element of the polvhedron if there is anv The first column in the output is the denominator and is alwavs equal to 1 If the polvhedron contains no integer points then a vector of length zero is printed 1 4 2 isl pip isl_pip takes the same input as the example program from the piplib distribution 1 e a set of constraints on the parameters a line containing only 1 and finally a set of constraints on a parametric polyhedron The coefficients of the parameters appear in the las
10. where p ranges over the dimensions and L U and M are constant integer vectors The elements of U may be co meaning that there is no upper bound corresponding to that element and similarly for L Such an overapproximation can be obtained by computing strides lower and upper bounds on the difference set AR The transitive closure of such a d form relation is i gt j da k k gt 1AkKL lt j iskUA Vp jp ip MpQp 2 16 The domain and range of this transitive closure are then intersected with those of the input relation This is a special case of the algorithm in Section 2 4 2 In their algorithm for computing lower bounds the authors use the above algorithm as a substep on the disjuncts in the relation At the end they say If an upper bound is required it can be calculated in a manner similar to that of a single conjunct sic relation Presumably the authors mean that a d form approximation of the whole input rela tion should be used However the accuracy can be improved by also trying to apply the incremental technique from the same paper which is explained in more detail in Section 2 4 6 In this case C R D can be obtained by allowing the value zero for kin 2 16 i e by computing i gt j da k k gt OAKL lt j i lt kUA Vp jp ip Mpap In our implementation we take as D the simple hull Section 2 2 of domR U ranR To determine whether it is safe to use C R D we check the following conditions as
11. Operations The two arguments of a binary operation not only need to live in the same isl_ctx they currently also need to have the same number of parameters Basic Operations e Intersection __isl_give isl basic set isl basic set intersect isl take isl basic set bseti isl take isl basic set bset2 isl give isl set isl set intersect isl take isl set setl isl take isl set set2 isl give isl union set isl union set intersect isl take isl union set useti isl take isl union set uset2 isl give isl basic map isl basic map intersect domain isl take isl basic map bmap isl take isl basic set bset isl give isl basic map isl basic map intersect range isl take isl basic map bmap isl take isl basic set bset isl give isl basic map isl basic map intersect isl take isl basic map bmap1 isl take isl basic map bmap2 isl give isl map isl map intersect domain isl take isl map map isl take isl set set isl give isl map isl map intersect range isl take isl map map isl take isl set set 29 isl give isl map isl map intersect isl take isl map map1 isl take isl map map2 isl give isl union map isl union map intersect domain isl take isl union map umap isl take isl union set uset isl give isl union map isl union map intersect range isl take isl union map
12. and S Z gt 22 be two relations then the composition of R and S is defined as SoR sbp xi gt x3 E Z x ZB dx Z X1 gt X2 E R S A X2 gt x3 S s Definition 2 1 8 Difference Set of a Relation Let R Z gt 2777 be a relation The difference set A R of R is the set of differences between image elements and the cor responding domain elements AR s 6 Z 4x gt yeR 5 y x 2 2 Simple Hull It is sometimes useful to have a single basic set or basic relation that contains a given set or relation For rational sets the obvious choice would be to compute the rational convex hull For integer sets the obvious choice would be the integer hull However isl currently does not support an integer hull operation and even if it did it would be fairly expensive to compute The convex hull operation is supported but it is also fairly expensive to compute given only an implicit representation Usually it is not required to compute the exact integer hull and an overapproxima tion of this hull is sufficient The simple hull of a set is such an overapproximation and it is defined as the inclusion wise smallest basic set that is described by con straints that are translates of the constraints in the input set This means that the simple hull is relatively cheap to compute and that the number of constraints in the simple hull is no larger than the number of constraints in the input Definition 2 2 1
13. bset isl give isl basic set isl set affine hull 26 __isl_take isl set set isl give isl union set isl union set affine hull isl take isl union set uset isl give isl basic map isl basic map affine hull isl take isl basic map bmap isl give isl basic map isl map affine hull isl take isl map map isl give isl union map isl union map affine hull isl take isl union map umap In case of union sets and relations the affine hull is computed per space e Polyhedral hull isl give isl_basic_set isl set polvhedral hull isl take isl set set isl give isl basic map isl map polvhedral hull isl take isl map map isl give isl union set isl union set polvhedral hull isl take isl union set uset isl give isl union map isl union map polvhedral hull isl take isl union map umap These functions compute a single basic set or relation not involving anv existen tiallv quantified variables that contains the whole input set or relation In case of union sets and relations the polvhedral hull is computed per space e Power isl give isl map isl map power isl take isl map map unsigned param int exact Compute a parametric representation for all positive powers k of map The power k is equated to the parameter at position param The result may be an overap proximation If the result is exact then exact is set to 1 The cur
14. bv starting from a universe set or re lation adding equality and or inequality constraints and then projecting out the exis tentially quantified variables if any Constraints can be constructed manipulated and added to basic sets and relations using the following functions include lt isl constraint h gt isl give isl_constraint isl_equality_alloc isl take isl dim dim isl give isl constraint isl_inequality_alloc isl take isl dim dim void isl constraint set constant isl keep isl constraint constraint isl int v 16 void isl constraint set coefficient isl keep isl constraint constraint enum isl dim tvpe type int pos isl int v isl give isl basic map isl basic map add constraint isl take isl basic map bmap isl take isl constraint constraint isl give isl basic set isl basic set add constraint isl take isl basic set bset isl take isl constraint constraint For example to create a set containing the even integers between 10 and 42 vou would use the following code isl int v struct isl dim dim struct isl constraint c struct isl basic set bset isl int init v dim isl dim set alloc ctx 0 2 bset isl basic set universe isl dim copv dim c isl equalitv alloc isl dim copv dim isl int set si Cv 1 isl constraint set coefficient c isl dim set 0 v isl int set si v 2 isl constraint set coefficient c isl dim se
15. fold upwf isl take isl union set uset isl give isl pw qpolvnomial fold isl pw qpolvnomial fold coalesce C isl take isl pw qpolvnomial fold pwf isl give isl union pw qpolvnomial fold isl union pw qpolvnomial fold coalesce C isl take isl union pw qpolvnomial fold upwf isl give isl pw qpolvnomial fold isl pw qpolvnomial fold gist isl take isl pw qpolvnomial fold pwf isl take isl set context isl give isl union pw qpolvnomial fold isl union pw qpolvnomial fold gist isl take isl union pw qpolvnomial fold upwf isl take isl union set context The gist operation applies the gist operation to each of the cells in the domain of the input piecewise quasipolvnomial reduction In future the operation will also exploit the context to simplifv the quasipolvnomial reductions associated to each cell isl give isl pw qpolvnomial fold isl map applv pw qpolvnomial fold isl take isl map map isl take isl pw qpolvnomial fold pwf int tight isl give isl union pw qpolvnomial fold isl union map applv union pw qpolvnomial fold isl take isl union map umap isl take isl union pw qpolvnomial fold upwf int tight These functions compose the given map with the given piecewise quasipolvnomial reduction That is compute a bound of the same type as pwf or upwf itself over all elements in the intersection of the range of the map and the domain of the
16. in some cases it is possible to relax the constraints of R to include part of the identity relation say on domain D We will use the notation C R D Ri U Idp to represent this relaxed version of R use the notation RI C R D can be computed by allowing k to attain the value 0 in and by using PN D gt D instead of 2 3 Typically D will be a strict superset of both dom R and ran R We therefore need to check that domain and range of the transitive closure are part of C R D i e the part that results from the paths of positive length k 2 1 are equal to the domain and range of R If not then the incremental approach cannot be applied for the given choice of R and D In order to be able to replace R by C R D in 2 13 D should be chosen to include both dom R and ran R i e such that Idp oR o Idp R for all j i et al 1996c say that they use D dom R Uran R but presumably they mean that they 61 use D domR U ran R Now this expression of D contains a union so it not directly usable Kelly et al 1996c do not explain how they avoid this union Apparently in their implementation they are using the convex hull of domR U ran R or at least an approximation of this convex hull We use the simple hull Section 2 2 of dom R U ran R It is also possible to use a domain D that does not include dom R U ran R but then we have to compose with C R D more selectively In particular if we have for ea
17. involves several substeps and since the user is usually not interested in the intermediate results most functions that return a new object will also release all the objects passed as arguments If the user still wants to use one or more of these arguments after the function call she should pass along a copy of the object rather than the object itself The user is then responsible for make sure that the original object gets used somewhere else or is explicitly freed The arguments and return values of all documents functions are annotated to make clear which arguments are released and which arguments are preserved In particular the following annotations are used _isl_give isl give means that a new object is returned The user should make sure that the returned pointer is used exactly once as a value for an isl take argument In between it can be used as a value for as many __isl_keep arguments as the user likes There is one exception and that is the case where the pointer returned is NULL Is this case the user is free to use it as an __isl_take argument or not _isl_take isl take means that the object the argument points to is taken over by the function and may no longer be used by the user as an argument to any other function The pointer value must be one returned by a function returning an isl give pointer If the user passes in a NULL value then this will be treated as an error in the sense that the function will not perform
18. isl basic set bset isl basic map bmap isl set applv isl set set isl map map isl give isl union set isl union set applv isl take isl take isl union set uset isl union map umap isl give isl basic map isl basic map applv domain isl take isl take isl basic map bmap1 isl basic map bmap2 isl give isl basic map isl basic map applv range isl take isl take isl give isl map isl take isl take isl basic map bmap1 isl basic map bmap2 isl map applv domain isl map mapi isl map map2 isl give isl union map isl union map applv domain isl take isl take isl give isl map isl take isl take isl union map umap1 isl union map umap2 isl_map_apply_range isl map mapl isl map map2 isl give isl union map isl union map applv range e Simplification isl take isl take isl union map umap1 isl union map umap2 isl give isl basic set isl basic set gist isl take isl basic set bset isl take isl basic set context isl give isl set isl set gist isl take isl set isl take isl set context isl give isl union set isl union set gist isl take isl union set uset isl take isl union set context isl give isl basic map isl basic map gist isl take isl basic map bmap isl take isl basic map context set
19. isl keep isl union set uset int fn isl take isl point pnt void user void user The function fn is called for each integer point in set with as second argument the last argument of the isl set foreach point call The function fn should return 0 on success and 1 on failure In the latter case isl set foreach point will stop enumerating and return 1 as well If the enumeration is performed successfully and to completion then isl set foreach point returns 0 To obtain a single point of a basic set use isl give isl point isl basic set sample point isl take isl basic set bset isl give isl point isl set sample point isl take isl set set 35 If set does not contain any integer points then the resulting point will be void a property that can be tested using int isl point is void isl keep isl point pnt 1 3 14 Piecewise Quasipolynomials A piecewise quasipolynomial is a particular kind of function that maps a parametric point to a rational value More specifically a quasipolynomial is a polynomial expres sion in greatest integer parts of affine expressions of parameters and variables A piece wise quasipolynomial is a subdivision of a given parametric domain into disjoint cells with a quasipolynomial associated to each cell The value of the piecewise quasipolv nomial at a given point is the value of the quasipolynomial associated to the cell that contains the point Outside of the u
20. its usual operation However it will still make sure that all the the other isl take arguments are released _isl_keep isl keep means that the function will only use the object temporarily After the function has finished the user can still use it as an argument to other func tions A NULL value will be treated in the same way as a NULL value for an isl take argument 1 3 5 Dimension Specifications Whenever a new set or relation is created from scratch its dimension needs to be spec ified using an isl dim include lt isl dim h gt __isl_give isl dim isl dim alloc isl ctx ctx unsigned nparam unsigned n in unsigned n out isl give isl dim isl dim set alloc isl ctx ctx unsigned nparam unsigned dim isl give isl dim isl dim copv isl keep isl dim dim void isl dim free isl take isl dim dim unsigned isl dim size isl keep isl dim dim enum isl dim tvpe tvpe The dimension specification used for creating a set needs to be created using isl dim set alloc while that for creating a relation needs to be created using isl dim alloc isl_dim_size can be used to find out the number of dimensions of each type in a dimension specifica tion where type may be isl dim param isl dim in only for relations isl dim out only for relations isl dim set only for sets or isl dim all It is often useful to create objects that live in the same space as some other object This can be accomplished bv creating the
21. piecewise quasipolynomial reduction as a function of an element in the domain of the map 44 1 3 16 Dependence Analysis isl contains specialized functionality for performing array dataflow analysis That is given a sink access relation and a collection of possible source access relations isl can compute relations that describe for each iteration of the sink access which iteration of which of the source access relations was the last to access the same data element before the given iteration of the sink access To compute standard flow dependences the sink should be a read while the sources should be writes If any of the source accesses are marked as being may accesses then there will be a dependence to the last must access and to any may access that follows this last must access In particular if all sources are may accesses then memory based dependence analysis is performed If on the other hand all sources are must accesses then value based dependence analysis is performed include lt isl flow h gt typedef int C isl access level before void first void second isl give isl access info isl access info alloc isl take isl map sink void sink user isl access level before fn int max source isl give isl access info isl access info add source isl take isl access info acc isl take isl map source int must void source user void isl access info free isl take isl access info acc isl
22. qpolvnomial fold fold void user void user See Inspecting Piecewise Quasipolvnomials for an explanation of the difference between these two functions To iterate over all quasipolvnomials in a reduction use int isl qpolvnomial fold foreach qpolvnomial isl keep isl qpolvnomial fold fold int fn isl take isl qpolvnomial qp void user void user Operations on Piecewise Quasipolvnomial Reductions isl give isl pw qpolvnomial fold isl pw qpolvnomial fold add isl take isl pw qpolvnomial fold pwf1 isl take isl pw qpolvnomial fold pwf2 isl give isl pw qpolvnomial fold isl pw qpolvnomial fold fold isl take isl pw qpolvnomial fold pwf1 isl take isl pw qpolvnomial fold pwf2 isl give isl union pw qpolvnomial fold isl union pw qpolvnomial fold fold isl take isl union pw qpolvnomial fold upwf1 isl take isl union pw qpolvnomial fold upwf2 43 isl give isl_qpolynomial isl_pw_qpolynomial_fold_eval isl take isl pw qpolvnomial fold pwf isl take isl point pnt isl give isl qpolvnomial isl union pw qpolvnomial fold eval isl take isl union pw qpolvnomial fold upwf isl take isl point pnt isl give isl union set isl union pw qpolvnomial fold domain isl take isl union pw qpolvnomial fold upwf isl give isl union pw qpolvnomial fold isl union pw qpolvnomial fold intersect dc isl take isl union pw qpolvnomial
23. s y x 0 Note that each P contains paths of length at least one We therefore need to take the union with the identity relation when composing the P s to allow for paths that do not contain any offsets from one or more A The path that consists of only identity relations is removed by imposing the constraint Vari Xa 1 gt 0 Taking the union with the identity relation means that that the relations we compose in 2 6 each consist of two 53 basic relations If there are m disjuncts in the input relation then a direct application of the composition operation may therefore result in a relation with 2 disjuncts which is prohibitively expensive It is therefore crucial to apply coalescing after each composition Let us now consider how to compute an overapproximation of P Those that cor respond to singleton A s are grouped together and handled as in 2 5 Note that this is just an optimization The procedure described below would produce results that are at least as accurate For simplicity we first assume that no constraint in A involves any existentially quantified variables We will return to existentially quantified variables at the end of this section Without existentially quantified variables we can classify the constraints of A as follows 1 non parametric constraints Aix c1 gt 0 2 7 2 purely parametric constraints Bos 0 gt 0 2 8 3 negative mixed constraints A3X B3s 63 gt 0 2 9 such that for
24. strict subset isl keep isl basic map bmapl isl keep isl basic map bmap2 int isl map is subset isl keep isl map map1 isl keep isl map map2 int isl map is strict subset isl keep isl map map1 isl keep isl map map2 int isl union map is subset isl keep isl union map umapl isl keep isl union map umap2 int isl union map is strict subset isl keep isl union map umapl isl keep isl union map umap2 1 3 10 Unarv Operations e Complement __isl_give isl set isl_set_complement __isl_take isl set set e Inverse map isl give isl basic map isl basic map reverse isl take isl basic map bmap isl give isl map isl map reverse isl take isl map map isl give isl union map isl union map reverse isl take isl union map umap e Projection isl give isl basic set isl basic set project out isl take isl basic set bset enum isl dim tvpe tvpe unsigned first unsigned n 24 isl give isl basic map isl_basic_map_project_out isl take isl basic map bmap enum isl dim tvpe tvpe unsigned first unsigned n isl give isl set isl set project out isl take isl set set enum isl dim tvpe tvpe unsigned first unsigned n isl give isl map isl map project out isl take isl map map enum isl dim tvpe tvpe unsigned first unsigned n isl give isl basic set isl basic map domain isl take isl basic map bma
25. that A K contains a point whose first d coordinates are zero and whose final coordinate is positive In the implementation we currently perform this test on P instead of K Note that if R is acyclic and T is not then the approximation is clearly not exact and the approximation of the power K will not be exact either 2 4 4 Decomposing R into strongly connected components If the input relation R is a union of several basic relations that can be partially ordered then the accuracy of the approximation may be improved by computing an approxima tion of each strongly connected components separately For example if R R UR and Ri o R2 0 then we know that any path that passes through Rz cannot later pass through Ri i e R RiUR U Ri oRj 2 11 We can therefore compute approximations of transitive closures of Ri and R2 sepa rately Note however that the condition Ri o Ra is actually too strong If Ri o R2 is a subset of Ra o Ri then we can reorder the segments in any path that moves through both R and R to first move through R and then through R3 This idea can be generalized to relations that are unions of more than two basic relations by constructing the strongly connected components in the graph with as ver tices the basic relations and an edge between two basic relations R and R if R needs to follow R in some paths That is there is an edge from R to Rj iff The components can be obtained from the graph by ap
26. 1 Tarjan R 1972 Depth first search and linear graph algorithms SIAM Journal on Computing 1 2 146 160 56 Verdoolaege S 2009 April An integer set librarv for program analvsis Ad vances in the Theory of Integer Linear Optimization and its Extensions AMS 2009 Spring Western Section Meeting San Francisco California 25 26 April 2009 52 64
27. Integer Set Library Manual Version isl 0 05 1 Sven Verdoolaege January 5 2011 Contents 1 User Manual 3 1 1 Introductionj 00000 3 3 4 1 2 1 Installation from the git repositorvj 000000 4 1 2 2 Common installation instructions 4 Lape b ph da Cee ee bis a o bes 5 1 3 1 Initialization 000000 3 13 2 Integers s ronsar nie eh aa E A EERE SERS 6 1 3 3 Sets and Relations ooa 8 1 3 4 Memory Management L oaoa 8 semie do 9 1 3 6 Input and Output 11 Toe ereer errs 14 1 3 8 Inspecting Sets and Relations 18 1 3 9 Properties sosa ye ee a a A ee Be es 22 1 3 10 Unarv Operations 1 3 11 Binary Operations 6 29 1 3 12 Matrices e se e be eee wa b bnin ea be eee be ba 34 1 3 16 Dependence Analysis 1 3 17 Parametric Vertex Enumeration 47 Lae AD di AREA AA eee ek a ee ad 48 1 4 1 isl polyhedron_sample 48 14 2 Uslpip s kk ike be ewe eh eS Rea a eA 48 1 4 3 isl_polyhedron_minimize 48 1 4 4 isl_ polytope_scan 04 48 13 isl polvlibju se p sose e ib a Sebo ARES Bak doe BE so 49 2 Implementation Details 2 1 Sets and Relations 2 2 Simple Hull 2 3 Coalescing 2 4 1 Introduction 0 0 0 0 00 eee ee ee References Chapter 1 User Manual 1 1 I
28. LL then tight is set to 1 is the returned bound is known be tight i e for each value of the parameters there is at least one element in the domain that reaches the bound If the domain of pwqp is not wrapping then the bound is computed over all elements in that domain and the result has a purely parametric domain If the domain of pwqp is wrapping then the bound is computed over the range of the wrapped relation The domain of the wrapped relation becomes the domain of the result A piecewise quasipolynomial reduction can be copied or freed using the following functions __isl_give isl_qpolynomial_fold isl_qpolynomial_fold_copy __isl_keep isl_qpolynomial_fold fold isl give isl_pw_qpolynomial_fold isl_pw_qpolynomial_fold_copy isl keep isl pw qpolvnomial fold pwf isl give isl union pw qpolvnomial fold isl union pw qpolvnomial fold copv isl keep isl union pw qpolvnomial fold upwf void isl qpolvnomial fold free isl take isl qpolvnomial fold fold void isl pw qpolvnomial fold free isl take isl pw qpolvnomial fold pwf void isl union pw qpolvnomial fold free isl take isl union pw qpolvnomial fold upwf Printing Piecewise Quasipolvnomial Reductions Piecewise quasipolvnomial reductions can be printed using the following function isl give isl printer isl printer print pw qpolvnomial fold isl take isl printer p isl keep isl pw qpolvnomial fold pwf isl give isl pr
29. Simple Hull of a Set The simple hull of a set S Uj lt jcy Si with S E xe Z See VV Axe Bar Da o20 1 lt i lt v is the set H Z 34 ipso xezimez A Axe Bar Dare K 20 l lt i lt v with K the component wise smallest non negative integer vectors such that S H The K can be obtained by solving a number of LP problems one for each element of each K If any LP problem is unbounded then the corresponding constraint is dropped 51 2 3 Coalescing See Verdoolaege 2009 for now More details will be added later 2 4 Transitive Closure 2 4 1 Introduction Definition 2 4 1 Power of a Relation Let R Z gt 2777 be a relation and k Zs a positive number then power k of relation R is defined as r IR ifk 1 Re TA 2 1 RoR ifk gt 2 Definition 2 4 2 Transitive Closure of a Relation Let R Z gt 277 be a relation then the transitive closure R of R is the union of all positive powers of R Rt JR k21 Alternatively the transitive closure may be defined inductively as R RU Ro R 2 2 Since the transitive closure of a polyhedral relation may no longer be a polyhedral relation Kelly et al 1996c we can in the general case only compute an approxima tion of the transitive closure Whereas Kelly et al 1996c compute underapproxima tions we like Beletska et al 2009 compute overapproximations That is given a relation R we will compute a relation T such that Rt T Of c
30. __isl_give isl qpolvnomial isl_qpolynomial_neg isl take isl qpolvnomial qp isl give isl qpolvnomial isl qpolvnomial add isl take isl qpolvnomial qpi isl take isl qpolvnomial qp2 isl give isl qpolvnomial isl qpolvnomial sub isl take isl qpolvnomial qpi isl take isl qpolvnomial qp2 isl give isl_qpolynomial isl qpolvnomial mul isl take isl qpolvnomial qp1 isl take isl qpolvnomial qp2 isl give isl qpolvnomial isl_qpolynomial_pow isl take isl qpolvnomial qp unsigned exponent isl give isl pw qpolvnomial isl pw qpolvnomial add isl take isl pw qpolvnomial pwqpl isl take isl pw qpolvnomial pwqp2 isl give isl pw qpolvnomial isl pw qpolvnomial sub isl take isl pw qpolvnomial pwqpl isl take isl pw qpolvnomial pwqp2 isl give isl pw qpolvnomial isl pw qpolvnomial add disjoint isl take isl pw qpolvnomial pwqpl isl take isl pw qpolvnomial pwqp2 isl give isl pw qpolvnomial isl pw qpolvnomial neg isl take isl pw qpolvnomial pwqp isl give isl pw qpolvnomial isl pw qpolvnomial mul isl take isl pw qpolvnomial pwqpl isl take isl pw qpolvnomial pwqp2 isl give isl union pw qpolvnomial isl union pw qpolvnomial add isl take isl union pw qpolvnomial upwqpl isl take isl union pw qpolvnomial upwqp2 isl give isl union pw qpolvnomial isl union pw qpolvnomial sub is
31. a given domain to itself However it is also possible to detect disjoint domains and ranges and to apply Floyd Warshall internally Algorithm 1 The modified Flovd Warshall algorithm of Kellv et al 1996c Input Relations Rp4 0 lt p q lt n Output Updated relations R such that each relation R contains all indirect paths from p to q in the input graph for r e 0 n 1 do R R for p 0 n 1 do for q 0 n 1 do if p r orq r then aA uk UN 4 l Rig Reg Rigo Ri U Ry oR GR Let the input relation R be a union of m basic relations R Let D2 be the domains of R and D the ranges of R The first step is to group overlapping D until a partition is obtained If the resulting partition consists of a single part then we continue with the algorithm of Section 2 4 2 Otherwise we apply Floyd Warshall on the graph with as 59 Figure 2 3 The relation solid arrows on the right of Figure 1 of Beletska et al 2009 and its transitive closure vertices the parts of the partition and as edges the R attached to the appropriate pairs of vertices In particular let there be n parts P in the partition We construct n relations Rog U Ri is t dom R CP Aran R CP apply Algorithm 1jand return the union of all resulting R q as the transitive closure of R Each iteration of the r loop infAlgorithm Tlupdates all relations R q to include paths that go from p to r possibly stay there for
32. a while and then go from r to q Note that paths that stay in r include all paths that pass through earlier vertices since R itself has been updated accordingly in previous iterations of the outer loop In principle it would be sufficient to use the R and R computed in the previous iteration of the r loop in Line 6 However from an implementation perspective it is easier to allow either or both of these to have been updated in the same iteration of the r loop This may result in duplicate paths but these can usually be removed by coalescing Section 2 3 the result of the union in Line 6 which should be done in any case The transitive closure in Linef jis performed using a recursive call This recursive call includes the partitioning step but the resulting partition will usuallv be a singleton The result of the recursive call will either be exact or an overapproximation The final result of Flovd Warshall is therefore also exact or an overapproximation Example 2 4 7 Consider the relation on the right of Figure 1 of Beletska et al 2009 reproduced injFigure 2 3 This relation can be described as x y gt x2 y2 Gy 2x A x2 XA 3y2 3 4 2XAXZOAX 83 V La 1 xAy yAx gt 0A3y gt 2 2xAx lt 203y lt 3 2x Note that the domain of the upward relation overlaps with the range of the rightward relation and vice versa but that the domain of neither relation overlaps with its own range or the domain of the other relation The d
33. antified variables can be handled by classifying them into variables that are uniquely determined by the parameters variables that are independent of the parameters and others The first set can be treated as parameters and the second as vari ables Constraints involving the other existentially quantified variables are removed Example 2 4 4 Consider the relation R n gt x gt y dao 7a9 2 n A 5a 1 x yAy gt 6 x The difference set of this relation is A AR n gt 1 x J00 01 7 o 2 n A 5a l xAx26 The existentially quantified variables can be defined in terms of the parameters and variables as 2 n d 1 x Aa an a l 7 5 ay can therefore be treated as a parameter while a can be treated as a variable This in turn means that lay 2 n can be treated as a purely parametric constraint while the other two constraints are non parametric The corresponding Q 2 10 is therefore n gt x z gt 0 w dao ak4fi k gt lAy x fAw zt ka Tap 2 n A 5a k xAx gt 6k Projecting out the final coordinates encoding the length of the paths results in the exact transitive closure R n gt x gt y Jao 7a 2 n A 6o gt x y 500 lt 1 x y 2 4 3 Checking Exactness The approximation T for the transitive closure R can be obtained by projecting out the parameter k from the approximation K of the power R Since K is an over approximation of R T will also be an overapp
34. ap deltas isl take isl union map umap These functions return a basic set containing the differences between image elements and corresponding domain elements in the input Coalescing Simplify the representation of a set or relation by trying to combine pairs of basic sets or relations into a single basic set or relation isl give isl set isl set coalesce isl take isl_set set isl give isl map isl map coalesce isl take isl map map isl give isl union set isl union set coalesce isl take isl union set uset isl give isl union map isl union map coalesce isl take isl union map umap Convex hull isl give isl basic set isl set convex hull isl take isl set set isl give isl basic map isl_map_convex_hull isl take isl map map If the input set or relation has anv existentiallv quantified variables then the result of these operations is currently undefined Simple hull isl give isl_basic_set isl set simple hull isl take isl set set isl give isl basic map isl map simple hull isl take isl map map These functions compute a single basic set or relation that contains the whole input set or relation In particular the output is described by translates of the constraints describing the basic sets or relations in the input See Section 2 2 Affine hull __isl_give isl_basic_set isl basic set affine hull isl take isl basic set
35. at_copy __isl_keep isl mat mat void isl mat free isl take isl mat mat Note that the elements of a newlv created matrix mav have arbitrarv values The elements can be changed and inspected using the following functions int isl mat rows isl keep isl mat mat int isl mat cols isl keep isl mat mat int isl mat get element isl keep isl mat mat int row int col isl int v isl give isl mat isl mat set element isl take isl mat mat int row int col isl int v isl mat get element will return a negative value if anvthing went wrong In that case the value of v is undefined The following function can be used to compute the right inverse of a matrix i e a matrix such that the product of the original and the inverse in that order is a multiple of the identity matrix The input matrix is assumed to be of full row rank isl give isl_mat isl_mat_right_inverse __isl_take isl mat mat The following function can be used to compute the right kernel or null space of a matrix i e a matrix such that the product of the original and the kernel in that order is the zero matrix isl give isl mat isl mat right kernel isl take isl mat mat 1 3 13 Points Points are elements of a set Thev can be used to construct simple sets boxes or thev can be used to represent the individual elements of a set The zero point the origin can be created using __isl_give isl_point isl_point_zero __isl_take is
36. ch j i either dom R C Dor dom Rj N ran R 0 2 14 and similarly for each j i either ran R C D or ran Rj N dom R 0 2 15 then we can refine to RFU cenjecjuj U corjju U recju r dom R CD dom R Nran R 0 dom R CD dom R Nran R 0 ranR CD ran R CD ran R Adom R 0 ran R Adom R 0 If only property 2 14 holds we can use dom R Nran R 0 while if only property 2 15 holds we can use RON U solu aro U consul U a c dom R ED ran RjED ran R Adom R 0 It should be noted that if we want the result of the incremental approach to be transitively closed then we can only apply it if all of the transitive closure operations involved are exact If say the second transitive closure in contains extra el ements then the result does not necessarily contain the composition of these extra elements with powers of Rj 2 4 7 An Omega like implementation While the main algorithm of Kelly et al 1996c is designed to compute and underap proximation of the transitive closure the authors mention that they could also compute overapproximations In this section we describe our implementation of an algorithm that is based on their ideas Note that the Omega library computes underapproximations Kelly et al 1996b Section 6 4 The main tool is Equation 2 of Kelly et al 1996c The input relation R is first overapproximated by a d form relation i j da L lt j i lt UA Vp jp ip Mp p 62
37. dim set dim isl give isl map isl map identitv isl take isl dim set dim These functions take a dimension specification for a set and return an identitv relation between two such sets e Lexicographic order isl give isl map isl map lex It isl take isl dim set dim isl give isl map isl map lex le isl take isl dim set dim isl give isl map isl map lex gt isl take isl dim set dim isl give isl map isl map lex ge C isl take isl dim set dim isl give isl map isl map lex It first isl take isl dim dim unsigned n isl give isl map isl map lex le first isl take isl dim dim unsigned n isl give isl map isl map lex gt first isl take isl dim dim unsigned n isl give isl map isl map lex ge first isl take isl dim dim unsigned n The first four functions take a dimension specification for a set and return re lations that express that the elements in the domain are lexicographicallv less isl map lex lt less or equal isl map lex le greater isl map lex gt or greater or equal isl map lex ge than the elements in the range The last four functions take a dimension specification for a map and return relations that express that the first n dimensions in the domain are lexicographicallv less isl map lex lt first less or equal isl map lex 1e first greater isl map lex gt first or greater or equal isl map lex ge first
38. e __isl_give __isl_give isl_map __isl_take __isl_give __isl_give isl_map __isl_take __isl_give isl_basic_map_partial_lexmax isl_basic_map bmap isl_basic_set dom isl set empty isl basic map partial lexmin isl basic map bmap isl basic set dom isl set empty isl map partial lexmax isl map map isl take isl set dom isl set empty isl_map_partial_lexmin isl_map map __isl_take isl_set dom isl set empty Given a basic map map or bmap the following functions simplv return a map mapping each element in the domain of map or bmap to the lexicographic minimum or maximum of all elements associated to that element In case of union relations the optimum is computed per space __isl_give isl_map __isl_take __isl_give isl_map __isl_take __isl_give isl_map __isl_take __isl_give isl_map __isl_take isl_basic_map_lexmin isl_basic_map bmap isl_basic_map_lexmax isl_basic_map bmap isl_map_lexmin isl map map isl map lexmax isl map map isl give isl union map isl union map lexmin isl take isl union map umap isl give isl union map isl union map lexmax isl take isl union map umap 33 1 3 12 Matrices Matrices can be created copied and freed using the following functions include lt isl mat h gt __isl_give isl_mat isl_mat_alloc struct isl_ctx ctx unsigned n_row unsigned n_col __isl_give isl mat isl_m
39. e isl printer isl printer set indent isl take isl printer p int indent isl give isl printer isl printer set prefix isl take isl printer p const char prefix isl give isl printer isl printer set suffix isl take isl printer p const char suffix The output format mav be either ISL FORMAT ISL ISL FORMAT OMEGA ISL FORMAT POLVLIB ISL FORMAT EXT POLVLIB or ISL FORMAT LATEX and defaults to ISL FORMAT ISL Each line in the output is indented by indent spaces default 0 prefixed by prefix and suffixed by suffix In the PolyLib format output the coefficients of the exis tentially quantified variables appear between those of the set variables and those of the parameters To actually print something use include lt isl set h gt __isl_give isl_printer isl_printer_print_basic_set __isl_take isl printer printer __isl_keep isl basic set bset isl give isl printer isl printer print set isl take isl printer printer isl keep isl set set include lt isl map h gt isl give isl_printer isl_printer_print_basic_map 13 __isl_take isl printer printer isl keep isl_basic_map bmap isl give isl printer isl printer print mapC isl take isl printer printer isl keep isl map map include lt isl union_set h gt isl give isl_printer isl_printer_print_union_set isl take isl printer p isl keep isl union set uset include lt
40. each row j and for all s Ai s N 6 B3 S C3 j gt 0 0 4 positive mixed constraints A4x Bas c 2 0 such that for each row j there is at least one s such that A s N 6 Ba js 4 gt 0 0 We will use the following approximation Q for P s xX gt y ake Zs feZ y x LA y 2 10 Af kci gt OA Bos c gt 0 A Asf B3s c3 gt 0 To prove that O is indeed an overapproximation of P we need to show that for every s Z for every k Zs and for every f kAj s we have that f k satisfies the constraints in 2 10 If A s is non empty then s must satisfy the constraints in 2 8 Each element f k kA s is a sum of k elements f 1 in Aj s Each of these elements satisfies the constraints in 2 7 i e fj 120 jai e 54 The sum of these elements therefore satisfies the same set of inequalities i e A f ke gt 0 Finally the constraints in are such that for any s in the parameter domain of A we have r s B38 3 lt 0 i e A3f gt r s gt 0 and therefore also A3f gt r s Note that if there are no mixed constraints and if the rational relaxation of A s i e x Q Aix 0 gt 0 has integer vertices then the approximation is exact i e Q P In this case the vertices of A s generate the rational cone x e Q Ai c x and therefore A s is a Hilbert basis of this cone Schrijver 1986 Theorem 16 4 Existentially qu
41. ear in the same order in each of the disjuncts of a set or map then the user should call either of the following functions __isl_give isl set isl_set_align_divs __isl_take isl_set set __isl_give isl map isl_map_align_divs __isl_take isl map map Alternativelv the existentiallv quantified variables can be removed using the fol lowing functions which compute an overapproximation isl give isl basic set isl basic set remove divs isl take isl basic set bset isl give isl basic map isl basic map remove divs isl take isl basic map bmap isl give isl set isl set remove divs isl take isl set set To iterate over all the sets or maps in a union set or map use int isl union set foreach set isl keep isl union set uset int fn __isl_take isl set set void user void user int isl union map foreach map isl keep isl union map umap int fn isl take isl map map void user void user The number of sets or maps in a union set or map can be obtained from int isl union set n set isl keep isl union set uset int isl union map n map isl keep isl union map umap To extract the set or map from a union with a given dimension specification use isl give isl set isl union set extract set isl keep isl union set uset isl take isl_dim dim isl give isl map isl union map extract mapC isl keep isl union map umap isl take isl dim dim T
42. ension specifications include lt isl dim h gt int isl_dim_is_wrapping __isl_keep isl_dim dim __isl_give isl_dim isl dim wrapC isl take isl dim dim isl give isl dim isl dim unwrap isl take isl dim dim The input to isl dim is wrapping and isl dim unwrap should be the dimen sion specification of a set while that of isl dim wrap should be the dimension spec ification of a relation Conversely the output of is1_dim_unwrap is the dimension 10 specification of a relation while that of isl dim wrap is the dimension specification of a set Dimension specifications can be created from other dimension specifications using the following functions __isl_give isl_dim __isl_give isl_dim __isl_give isl_dim __isl_give isl_dim __isl_give isl_dim isl_dim_domain __isl_take isl_dim dim isl_dim_from_domain __isl_take isl_dim dim isl_dim_range __isl_take isl_dim dim isl_dim_from_range __isl_take isl_dim dim isl_dim_reverse __isl_take isl_dim dim isl give isl dim isl_dim_join __isl_take isl dim left isl take isl dim right isl give isl dim isl dim insert isl take isl dim dim enum isl dim tvpe tvpe unsigned pos unsigned n isl give isl dim isl dim add isl take isl dim dim enum isl dim tvpe tvpe unsigned n isl give isl dim isl dim dropC isl take isl dim dim enum isl dim tvpe tvpe unsigned first unsigned n Note that if dimensions are added or removed fro
43. es isl_basic_set_compute_vertices isl keep isl basic set bset The function isl basic set compute vertices performs the actual computa tion of the parametric vertices and the chamber decomposition and store the result in an isl_vertices object This information can be queried by either iterating over all the vertices or iterating over all the chambers or cells and then iterating over all vertices that are active on the chamber int isl_vertices_foreach_vertex __isl_keep isl_vertices vertices int fn __isl_take isl_vertex vertex void user void user int isl vertices foreach cell isl keep isl vertices vertices int fn __isl_take isl cell cell void user void user int isl cell foreach vertex isl keep isl cell cell int C fn isl take isl vertex vertex void user void user Other operations that can be performed on an isl vertices object are the follow ing isl ctx isl vertices get ctx isl keep isl vertices vertices int isl vertices get n vertices isl keep isl vertices vertices void isl vertices free isl take isl vertices vertices Vertices can be inspected and destroved using the following functions isl ctx isl vertex get ctx isl keep isl vertex vertex int isl vertex get id isl keep isl vertex vertex isl give isl basic set isl vertex get domain isl keep isl vertex vertex isl give isl basic set isl vertex get expr isl keep isl vertex
44. fore the isl ctx itself is freed isl_ctx isl_ctx_allocQ void isl_ctx_free isl_ctx ctx 1 3 2 Integers All operations on integers mainly the coefficients of the constraints describing the sets and relations are performed in exact integer arithmetic using GMP However to allow future versions of isl to optionally support fixed integer arithmetic all calls to GMP are wrapped inside isl specific macros The basic type is isl int and the operations below are available on this type The meanings of these operations are essentially the same as their GMP mpz counterparts As always with GMP types isl ints need to be initialized with isl_int_init before they can be used and they need to be released with isl_int_clear after the last use The user should not assume that an isl_int is represented as a mpz_t but should instead explicitly convert between mpz_ts and isl_ints using isl int set gmp and isl int get gmp whenever a mpz_t is re quired isl int init i isl int clear i isl int set r i isl int set si r i isl int set gmp r g isl int get gmp i g isl int abs r i isl_int_neg r i isl int swap i j isl int swap or set i j isl int add _ui ni j isl int sub ui r ij isl int add r i j isl int sub r i j isl int mul r i j isl int mul ui r i j is _int_addmul r i j isl int submul r i j isl int ged ri j isl int lem r i j isl_int_divexact r i j is _int_cdiv_q i j isl_int fdiv_q ri j is _int_fdiv_r 1 i j
45. give isl flow isl access info compute flow isl take isl access info acc int isl flow foreach isl keep isl flow deps int fn isl take isl map dep int must void dep user void user void user isl give isl set isl flow get no source isl keep isl flow deps int must void isl flow free isl take isl flow deps The function isl access info compute flow performs the actual dependence analvsis The other functions are used to construct the input for this function or to read off the output The input is collected in an isl access info which can be created through a call to isl access info alloc The arguments to this functions are the sink ac cess relation sink a token sink user used to identifv the sink access to the user a callback function for specifying the relative order of source and sink accesses and the number of source access relations that will be added The callback function has type int void first void second The function is called with two user 45 supplied tokens identifying either a source or the sink and it should return the shared nesting level and the relative order of the two accesses In particular let n be the num ber of loops shared by the two accesses If first precedes second textually then the function should return 2 n 1 otherwise it should return 2 n The sources can be added to the isl_access_info by performing at most max_source calls to isl_access_info_add_s
46. he sets mav be different for different invocations of fn To iterate over all terms in a quasipolynomial use int isl_qpolynomial_foreach_term __isl_keep isl qpolvnomial qp int fn C isl take isl term term void user void user The terms themselves can be inspected and freed using these functions unsigned isl term dim isl keep isl term term enum isl dim tvpe tvpe void isl term get num isl keep isl term term isl int n void isl term get den isl keep isl term term isl int d int isl term get exp C isl keep isl term term enum isl dim tvpe tvpe unsigned pos isl give isl div isl term get div isl keep isl term term unsigned pos void isl term free isl take isl term term Each term is a product of parameters set variables and integer divisions The func tion isl term get exp returns the exponent of a given dimensions in the given term The isl ints in the arguments of isl term get num and isl term get den need to have been initialized using isl int init before calling these functions Properties of Piecewise Quasipolynomials To check whether a quasipolynomial is actually a constant use the following function int isl_qpolynomial_is_cst __isl_keep isl_qpolynomial qp isl int n isl int d If qp is a constant and if n and d are not NULL then the numerator and denominator of the constant are returned in n and d respectively 39 Operations on Piecewise Quasipolynomials
47. hese single cell piecewise quasipolvnomials can be combined to create more complicated piecewise quasipolvnomials isl give isl pw qpolvnomial isl pw qpolvnomial zero isl take isl_dim dim isl give isl pw qpolvnomial isl pw qpolvnomial alloc isl take isl set set isl take isl qpolvnomial qp isl give isl union pw qpolvnomial isl union pw qpolvnomial zero 37 __isl_take isl_dim dim isl give isl_union_pw_qpolynomial isl_union_pw_qpolynomial_from_pw_qpolynomial __isl_take isl_pw_qpolynomial pwqp isl give isl_union_pw_qpolynomial isl_union_pw_qpolynomial_add_pw_qpolynomial __isl_take isl_union_pw_qpolynomial upwqp __isl_take isl_pw_qpolynomial pwqp Quasipolynomials can be copied and freed again using the following functions isl give isl qpolvnomial isl_qpolynomial_copy isl keep isl qpolvnomial qp void isl qpolvnomial free isl take isl qpolvnomial qp isl give isl pw qpolvnomial isl_pw_qpolynomial_copy isl keep isl pw qpolvnomial pwqp void isl pw qpolvnomial free isl take isl pw qpolvnomial pwqp isl give isl union pw qpolvnomial isl union pw qpolvnomial copv isl keep isl union pw qpolvnomial upwqp void isl union pw qpolvnomial free isl take isl union pw qpolvnomial upwqp Inspecting Piecewise Quasipolvnomials To iterate over all piecewise quasipolvnomials in a union piecewise quasipolvnomial use the follow
48. im tvpe cl enum isl dim tvpe c2 enum isl dim tvpe c3 enum isl dim tvpe c4 isl give isl mat isl basic map equalities matrix isl keep isl basic map bmap enum isl dim tvpe cl enum isl dim tvpe c2 enum isl dim tvpe c3 enum isl dim tvpe cA enum isl dim tvpe c5 isl give isl mat isl basic map inequalities matrix isl keep isl basic map bmap enum isl dim tvpe cl enum isl dim tvpe c2 enum isl dim tvpe c3 enum isl dim tvpe cA enum isl dim tvpe c5 The isl dim tvpe arguments dictate the order in which different kinds of vari ables appear in the resulting matrix and should be a permutation of isl_dim_cst isl dim param isl dim in isl dim out and isl_dim_div The names of the domain and range spaces of a set or relation can be read off using the following functions const char isl set get tuple name isl keep isl set set const char isl basic map get tuple name isl keep isl basic map bmap enum isl dim tvpe tvpe const char isl map get tuple name isl keep isl map map enum isl dim tvpe tvpe 21 As with isl_dim_get_tuple_name the value returned points to an internal data structure The names of individual dimensions can be read off using the following functions const char isl_constraint_get_dim_name __isl_keep isl_constraint constraint enum isl_dim_type type unsigned pos const char isl_set_get_dim_name __isl_keep isl_set set enum isl_dim_type type unsigned
49. ing function int isl union pw qpolvnomial foreach pw qpolvnomial isl keep isl union pw qpolvnomial upwqp int fn isl take isl pw qpolvnomial pwqp void user void user To extract the piecewise quasipolvnomial from a union with a given dimension specification use isl give isl pw qpolvnomial isl union pw qpolvnomial extract pw qpolvnomial isl keep isl union pw qpolvnomial upwqp isl take isl_dim dim To iterate over the cells in a piecewise quasipolvnomial use either of the following two functions int isl pw qpolvnomial foreach piece C isl keep isl pw qpolvnomial pwqp int fn isl take isl set set isl take isl qpolvnomial qp 38 void user void user int isl pw qpolvnomial foreach lifted piece isl keep isl pw qpolvnomial pwqp int C fn isl take isl set set isl take isl qpolvnomial qp void user void user As usual the function fn should return 0 on success and 1 on failure The differ ence between isl pw qpolvnomial foreach piece and isl pw qpolvnomial foreach lifted piece is that isl pw qpolvnomial foreach lifted piece will first compute unique rep resentations for all existentiallv quantified variables and then turn these existentiallv quantified variables into extra set variables adapting the associated quasipolvnomial accordingly This means that the set passed to fn will not have any existentially quantified variables but that the dimensions of t
50. inter isl printer print union pw qpolvnomial fold isl take isl printer p isl keep isl union pw qpolvnomial fold upwf Forisl printer print pw qpolvnomial fold output format of the printer needs to be set to either ISL FORMAT ISL or ISL FORMAT C For isl printer print union pw qpolvnomial fold output format of the printer needs to be set to ISL FORMAT ISL In case of printing in ISL FORMAT C the user may want to set the names of all dimensions isl give isl_pw_qpolynomial_fold isl pw qpolvnomial fold set dim name C isl take isl pw qpolvnomial fold pwf enum isl dim tvpe tvpe unsigned pos const char s 42 Inspecting Piecewise Quasipolynomial Reductions To iterate over all piecewise quasipolynomial reductions in a union piecewise quasipoly nomial reduction use the following function int isl_union_pw_qpolynomial_fold_foreach_pw_qpolynomial_fold __isl_keep isl_union_pw_qpolynomial_fold upwf int fn __isl_take isl_pw_qpolynomial_fold pwf void user void user To iterate over the cells in a piecewise quasipolynomial reduction use either of the following two functions int isl_pw_qpolynomial_fold_foreach_piece __isl_keep isl_pw_qpolynomial_fold pwf int fn __isl_take isl_set set __isl_take isl_qpolynomial_fold fold void user void user int isl_pw_qpolynomial_fold_foreach_lifted_piece __isl_keep isl_pw_qpolynomial_fold pwf int fn __isl_take isl set set isl take isl
51. isl union_map h gt __isl_give isl_printer isl_printer_print_union_map __isl_take isl_printer p __isl_keep isl_union_map umap When called on a file printer the following function flushes the file When called on a string printer the buffer is cleared __isl_give isl printer isl printer flush isl take isl printer p 1 3 7 Creating New Sets and Relations isl has functions for creating some standard sets and relations e Empty sets and relations isl give isl basic set isl_basic_set_empty isl take isl dim dim isl give isl basic map isl basic map emptv isl take isl dim dim isl give isl set isl set emptv isl take isl dim dim isl give isl map isl map emptv isl take isl dim dim isl give isl union set isl union set emptv isl take isl dim dim isl give isl union map isl union map emptv isl take isl_dim dim For isl union sets and isl union maps the dimensions specification is only used to specifv the parameters e Universe sets and relations 14 __isl_give isl_basic_set isl_basic_set_universe __isl_take isl_dim dim isl give isl basic map isl_basic_map_universe isl take isl dim dim isl give isl set isl set universe isl take isl dim dim isl give isl map isl map universe isl take isl dim dim e Identitv relations isl give isl basic map isl basic map identitv isl take isl
52. l fold fol Changes since isl 0 04 e All header files have been renamed from isl header h to isl header h 1 2 Installation The source of isl can be obtained either as a tarball or from the git repository Both are available from http freshmeat net projects isl The installation process depends on how you obtained the source 1 2 1 Installation from the git repository 1 Clone or update the repository The first time the source is obtained you need to clone the repository git clone git repo or cz isl git To obtain updates you need to pull in the latest changes git pull 2 Generate configure autogen sh After performing the above steps continue with the Common installation instruc tions 1 2 2 Common installation instructions 1 Obtain GMP Building isl requires GMP including its headers files Your distribution may not provide these header files by default and you may need to install a package called gmp devel or something similar Alternatively GMP can be built from source available from http gmplib org 2 Configure isl uses the standard autoconf configure script To run it just type configure optionally followed by some configure options A complete list of options can be obtained by running configure help Below we discuss some of the more common options isl can optionally use piplib but no piplib functionality is currently used by default The with piplib option can be used to specify
53. l take isl union pw qpolvnomial upwqpl isl take isl union pw qpolvnomial upwqp2 isl give isl union pw qpolvnomial isl union pw qpolvnomial mul isl take isl union pw qpolvnomial upwqpl isl take isl union pw qpolvnomial upwqp2 isl give isl qpolvnomial isl pw qpolvnomial eval isl take isl pw qpolvnomial pwqp isl take isl point pnt isl give isl qpolvnomial isl union pw qpolvnomial eval isl take isl union pw qpolvnomial upwqp isl take isl point pnt 40 __isl_give isl set isl_pw_qpolynomial_domain isl take isl_pw_qpolynomial pwqp isl give isl pw qpolvnomial isl pw qpolvnomial intersect domain isl take isl pw qpolvnomial pwpq isl take isl set set isl give isl union set isl union pw qpolvnomial domain isl take isl union pw qpolvnomial upwqp isl give isl union pw qpolvnomial isl union pw qpolvnomial intersect domain isl take isl union pw qpolvnomial upwpq isl take isl union set uset isl give isl union pw qpolvnomial isl union pw qpolvnomial coalesce C isl take isl union pw qpolvnomial upwqp isl give isl pw qpolvnomial isl pw qpolvnomial gist isl take isl pw qpolvnomial pwqp isl take isl set context isl give isl union pw qpolvnomial isl union pw qpolvnomial gist isl take isl union pw qpolvnomial upwqp isl take isl union set context The gist operation applies
54. l_dim dim The coordinates of a point can be inspected set and changed using void isl_point_get_coordinate __isl_keep isl point pnt enum isl dim tvpe type int pos isl int v isl give isl point isl point set coordinate C isl take isl point pnt enum isl dim tvpe type int pos isl int v 34 isl give isl point isl point add ui isl take isl point pnt enum isl dim tvpe tvpe int pos unsigned val isl give isl point isl point sub ui isl take isl point pnt enum isl dim tvpe tvpe int pos unsigned val Points can be copied or freed using isl give isl point isl point copv isl keep isl point pnt void isl point free isl take isl point pnt A singleton set can be created from a point using isl give isl basic set isl basic set from point isl take isl point pnt isl give isl set isl set from point isl take isl point pnt and a box can be created from two opposite extremal points using isl give isl basic set isl basic set box from points isl take isl point pnti isl take isl point pnt2 isl give isl set isl set box from points isl take isl point pnti isl take isl point pnt2 All elements of a bounded union set can be enumerated using the following func tions int isl set foreach point isl keep isl set set int C fn isl take isl point pnt void user void user int isl union set foreach point
55. m dim enum isl_dim_type type unsigned pos Note that isl dim get name returns a pointer to some internal data structure so the result can only be used while the corresponding isl dim is alive Also note that ev ery function that operates on two sets or relations requires that both arguments have the same parameters This also means that if one of the arguments has named parameters then the other needs to have named parameters too and the names need to match Pairs of isl union set and or isl union map arguments may have different parameters as long as thev are named in which case the result will have as parameters the union of the parameters of the arguments The names of entire spaces mav be set or read off using the following functions include lt isl dim h gt isl give isl_dim isl_dim_set_tuple_name isl take isl_dim dim enum isl dim tvpe type const char s const char isl dim get tuple name isl keep isl dim dim enum isl dim tvpe tvpe The dim argument needs to be one of isl dim in isl dim out or isl dim set As with isl dim get name the isl dim get tuple name function returns a pointer to some internal data structure Binarv operations require the corresponding spaces of their arguments to have the same name Spaces can be nested In particular the domain of a set or the domain or range of a relation can be a nested relation The following functions can be used to construct and deconstruct such nested dim
56. m a space then the name and the internal structure are lost 1 3 6 Input and Output isl supports its own input output format which is similar to the Omega format but also supports the PolvLib format in some cases isl format The isl format is similar to that of Omega but has a different svntax for describing the parameters and allows for the definition of an existentiallv quantified variable as the integer division of an affine expression For example the set of integers i between 0 and n such thati 10 lt 6can be described as n gt i exists a 1 10 0 lt i andi lt n and i 10 a lt 6 A set or relation can have several disjuncts separated by the keyword or Each disjunct is either a conjunction of constraints or a projection exists of a conjunction of constraints The constraints are separated by the keyword and PolyLib format If the represented set is a union then the first line contains a single number representing the number of disjuncts Otherwise a line containing the number 1 is optional Each disjunct is represented by a matrix of constraints The first line contains two numbers representing the number of rows and columns where the number of rows is 11 equal to the number of constraints and the number of columns is equal to two plus the number of variables The following lines contain the actual rows of the constraint matrix In each row the first column indicates whether the constrai
57. new objects see Creating New Sets and Relations or Creating New Piecewise Quasipolvnomials based on the dimension specification of the original object include lt isl set h gt __isl_give isl_dim isl_basic_set_get_dim __isl_keep isl basic set bset isl give isl dim isl set get dim isl keep isl set set include lt isl union_set h gt __isl_give isl_dim isl_union_set_get_dim __isl_keep isl union set uset include lt isl map h gt __isl_give isl_dim isl_basic_map_get_dim isl keep isl basic map bmap isl give isl dim isl map get dim isl keep isl map map include lt isl union_map h gt __isl_give isl_dim isl union map get dim isl keep isl union map umap include lt isl polynomial h gt isl give isl dim isl_qpolynomial_get_dim isl keep isl qpolvnomial qp isl give isl dim isl pw qpolvnomial get dim isl keep isl pw qpolvnomial pwqp isl give isl_dim isl_union_pw_qpolynomial_get_dim isl keep isl union pw qpolvnomial upwqp isl give isl dim isl union pw qpolvnomial fold get dim isl keep isl union pw qpolvnomial fold upwf The names of the individual dimensions mav be set or read off using the following functions include lt isl dim h gt __isl_give isl dim isl_dim_set_name __isl_take isl_dim dim enum isl_dim_type type unsigned pos __isl_keep const char name isl keep const char isl_dim_get_name __isl_keep isl_di
58. ng functions check whether the domain of the given basic setis a wrapped relation int isl basic set is wrapping isl keep isl basic set bset int isl set is wrappingC isl keep isl set set Binarv Properties e Equality int isl set fast is eqgual isl keep isl set seti isl keep isl set set2 int isl set is equal isl keep isl set setl isl keep isl set set2 int isl union set is equal isl keep isl union set usetl isl keep isl union set uset2 int isl basic map is equal isl keep isl basic map bmapl isl keep isl basic map bmap2 int isl map is equal isl keep isl map mapl isl keep isl map map2 int isl map fast is equal isl keep isl map mapl isl keep isl map map2 int isl union map is equal isl keep isl union map umap1 isl keep isl union map umap2 e Disjointness int isl set fast is disjoint isl keep isl set seti isl keep isl set set2 e Subset int isl set is subset isl keep isl set seti isl keep isl set set2 int isl set is strict subset isl keep isl set set1 isl keep isl set set2 23 int isl_union_set_is_subset __isl_keep isl union set usetl isl keep isl union set uset2 int isl union set is strict subset isl keep isl union set usetl isl keep isl union set uset2 int isl basic map is subset isl keep isl basic map bmap1 isl keep isl basic map bmap2 int isl basic map is
59. nion of cells the value is assumed to be zero For example the piecewise quasipolynomial In gt x gt 1 n x x lt n and x gt 0 maps xto1 n x for values of x between 0 and n A given piecewise quasipoly nomial has a fixed domain dimension Union piecewise quasipolynomials are used to contain piecewise quasipolynomials defined over different domains Piecewise quasipoly nomials are mainly used by the barvinok library for representing the number of ele ments in a parametric set or map For example the piecewise quasipolynomial above represents the number of points in the map n gt x gt y x y gt 0 and 0 lt gt x y lt n Printing Piecewise Quasipolynomials Quasipolynomials and piecewise quasipolynomials can be printed using the following functions isl give isl printer isl printer print qpolvnomial isl take isl printer p isl keep isl qpolvnomial qp isl give isl printer isl printer print pw qpolvnomial isl take isl printer p isl keep isl pw qpolvnomial pwqp isl give isl printer isl printer print union pw qpolvnomial isl take isl printer p isl keep isl union pw qpolvnomial upwqp The output format of the printer needs to be set to either ISL FORMAT ISL or ISL FORMAT C Forisl printer print union pw qpolvnomial only ISL FORMAT ISL is supported In case of printing in ISL FORMAT C the user mav want to set the names
60. nt is an equality 0 or inequality 1 The final column corresponds to the constant term If the set is parametric then the coefficients of the parameters appear in the last columns before the constant column The coefficients of any existentially quantified variables appear between those of the set variables and those of the parameters Extended PolyLib format The extended PolyLib format is nearly identical to the PolyLib format The only difference is that the line containing the number of rows and columns of a constraint matrix also contains four additional numbers the number of output dimensions the number of input dimensions the number of local dimensions i e the number of ex istentially quantified variables and the number of parameters For sets the number of output dimensions is equal to the number of set dimensions while the number of input dimensions is zero Input include lt isl set h gt __isl_give isl basic set isl_basic_set_read_from_file isl ctx ctx FILE input int nparam isl give isl basic set isl basic set read from str isl ctx ctx const char str int nparam isl give isl set isl set read from file isl ctx ctx FILE input int nparam isl give isl set isl set read from str isl ctx ctx const char str int nparam include lt isl map h gt __isl_give isl_basic_map isl_basic_map_read_from_file isl ctx ctx FILE input int nparam isl give isl_basic_ma
61. ntroduction isl is a thread safe C library for manipulating sets and relations of integer points bounded by affine constraints The descriptions of the sets and relations may involve both parameters and existentially quantified variables All computations are performed in exact integer arithmetic using GMP The isl library offers functionality that is similar to that offered by the Omega and Omega libraries but the underlying algorithms are in most cases completely different The library is by no means complete and some fairly basic functionality is still missing Still even in its current form the library has been successfully used as a backend polyhedral library for the polyhedral scanner CLooG and as part of an equiva lence checker of static affine programs For bug reports feature requests and questions visit the the discussion group at http groups google com group isl development 1 1 1 Backward Incompatible Changes Changes since isl 0 02 e The old printing functions have been deprecated and replaced by isl printer functions see Input and Output e Most functions related to dependence analysis have acquired an extra must ar gument To obtain the old behavior this argument should be given the value 1 See Dependence Analysis Changes since isl 0 03 e The function isl pw qpolvnomial fold add has been renamed to isl_pw_qpolynomial_fold_fold Similarly isl union pw qpolvnomial fold add has been renamed to isl union pw qpolvnomia
62. o iterate over all the basic sets or maps in a set or map use int isl set foreach basic set isl keep isl set set int fn __isl_take isl basic set bset void user void user int isl map foreach basic map isl keep isl map map int fn isl take isl basic map bmap void user void user 19 The callback function fn should return 0 if successful and 1 if an error occurs In the latter case or if any other error occurs the above functions will return 1 It should be noted that isl does not guarantee that the basic sets or maps passed to fn are disjoint If this is required then the user should call one of the following functions first __isl_give isl set isl set make disjoint isl take isl set set isl give isl map isl map make disjoint isl take isl map map The number of basic sets in a set can be obtained from int isl set n basic set isl keep isl set set To iterate over the constraints of a basic set or map use include lt isl constraint h gt int isl_basic_map_foreach_constraint isl keep isl basic map bmap int C fn C isl take isl constraint c void user void user void isl constraint free struct isl constraint c Again the callback function fn should return 0 if successful and 1 if an error occurs In the latter case or if any other error occurs the above functions will return 1 The constraint c represents either an equality or an inequality Use the following
63. omains and ranges can therefore be partitioned into two parts Po and Py shown as the white and black dots in Figure 2 3 60 respectively Initially we have Roo 0 Roi x y gt x 1 y x gt 0A3y gt 2 2xAx lt 2A3y lt 3 2x Rio x y gt x2 y2 By 2x A x2 xA 3y 3 2xAx20Ax lt 3 Ri 0 In the first iteration Rog remains the same 0 0 Ro and Rio are therefore also unaffected but Ri is updated to include Ro o Rio i e the dashed arrow in the figure This new Ri is obviously transitively closed so it is not changed in the second iteration and it does not have an effect on Ro and Rio However Roo is updated to include Rio Ro ie the dotted arrow in the figure The transitive closure of the original relation is then equal to Roy U Ro U Rio U Ri 2 4 6 Incremental Computation In some cases it is possible and useful to compute the transitive closure of union of basic relations incrementally In particular if R is a union of m basic maps R JR j then we can pick some R and compute the transitive closure of R as M r a o er 2 13 j i For this approach to be successful it is crucial that each of the disjuncts in the argument of the second transitive closure in be representable as a single basic relation i e without a union If this condition holds then by using 2 13 the number of disjuncts in the argument of the transitive closure can be reduced by one Now R Rf U Id but
64. on P of paths that move through a total of k offsets and then intersect domain and range of this collection with those of R That is K PAN domR gt rank 2 3 with P s x gt y Ak EZz0 6 ki Als y x 0 y ki k gt 0 2 4 and with A the basic sets that compose the difference set A R Note that the number of basic sets A need not be the same as the number of basic relations in R Also note that since addition is commutative it does not matter in which order we add the offsets and so we are allowed to group them as we did in 2 4 If all the A s are singleton sets A with 6 Z then simplifies to P xy Akie Zo y xt k n y ki k gt 0 2 5 and then the approximation computed in is essentially the same as that of Beletska et al 2009 If some of the Ajs are not singleton sets or if some of 6 s are parametric then we need to resort to further approximations To ease both the exposition and the implementation we will for the remainder of this section work with extended offsets A A x 1 That is each offset is extended with an extra coordinate that is set equal to one The paths constructed by summing such extended offsets have the length encoded as the difference of their final coordi nates The path P can then be decomposed into paths P one for each Aj P P U Id o o P5U Id o P UId N x gt y yari Xari k gt 0 2 6 with P s xX gt y Ik Zz E kA
65. ource must indicates whether the source is a must access or a may access Note that a multi valued access relation should only be marked must if every iteration in the domain of the relation accesses all elements in its image The source user token is again used to identify the source access The range of the source access relation source should have the same dimension as the range of the sink access relation The isl_access_info_free function should usually not be called explicitly because it is called implicitly by isl_access_info_compute_flow The result of the dependence analysis is collected in an isl flow There may be elements in the domain of the sink access for which no preceding source access could be found or for which all preceding sources are may accesses The sets of these elements can be obtained through calls to isl flow get no source the first with must set and the second with must unset In the case of standard flow dependence analvsis with the sink a read and the sources must writes the first set corresponds to the reads from uninitialized arrav elements and the second set is emptv The actual flow dependences can be extracted using isl flow foreach This function will call the user specified callback function fn for each non empty dependence between a source and the sink The callback function is called with four arguments the actual flow dependence relation mapping source iterations to sink iterations a boolean that indicates whe
66. ourse we want this approximation to be as close as possible to the actual transitive closure R and we want to detect the cases where the approximation is exact i e where T R For computing an approximation of the transitive closure of R we follow the same general strategy as Beletska et al 2009 and first compute an approximation of Rl for k gt 1 and then project out the parameter k from the resulting relation Example 2 4 3 As a trivial example consider the relation R x gt x 1 The kth power of this map for arbitrary k is Rt k x gt x k k21 The transitive closure is then Rt a xry akeZy y x k xr gt yly gt x 1 52 2 4 2 Computing an Approximation of R There are some special cases where the computation of R is very easy One such case is that where R does not compose with itself i e Ro R 0 or dom R N ran R 0 In this case R is only non empty for k 1 where it is equal to R itself In general it is impossible to construct a closed form of R as a polyhedral relation We will therefore need to make some approximations As a first approximations we will consider each of the basic relations in R as simply adding one or more offsets to a domain element to arrive at an image element and ignore the fact that some of these offsets may only be applied to some of the domain elements That is we will only consider the difference set AR of the relation In particular we will first construct a collecti
67. p isl give isl basic set isl basic map range C isl take isl basic map bmap isl give isl set isl map domain isl take isl map bmap isl give isl set isl map range isl take isl map map isl give isl union set isl union map domain isl take isl union map umap isl give isl union set isl union map range C isl take isl union map umap isl give isl basic map isl basic map domain map isl take isl basic map bmap isl give isl basic map isl basic map range map isl take isl basic map bmap isl give isl map isl map domain map isl take isl map map isl give isl map isl map range map isl take isl map map isl give isl union map isl union map domain map isl take isl union map umap isl give isl union map isl union map range map isl take isl union map umap The functions above construct a basic regular or union relation that maps a wrapped version of the input relation to its domain or range Identitv isl give isl map isl set identitv isl take isl set set isl give isl union map isl union set identitv isl take isl union set uset Construct an identitv relation on the given union set Deltas isl give isl basic set isl basic map deltas 25 isl take isl basic map bmap isl give isl set isl map deltas isl take isl map map isl give isl union set isl union m
68. p isl_basic_map_read_from_str isl ctx ctx const char str int nparam isl give isl map isl map read from file struct isl ctx ctx FILE input int nparam isl give isl map isl map read from str isl ctx ctx const char str int nparam include lt isl union_set h gt __isl_give isl union set isl_union_set_read_from_str struct isl ctx ctx const char str include lt isl union_map h gt __isl_give isl union map isl union map read from str struct isl ctx ctx const char str 12 The input format is autodetected and may be either the PolyLib format or the isl format nparam specifies how many of the final columns in the PolyLib format correspond to parameters If input is given in the isl format then the number of parameters needs to be equal to nparam If nparam is negative then any number of parameters is accepted in the isl format and zero parameters are assumed in the PolyLib format Output Before anything can be printed an isl printer needs to be created __isl_give isl_printer isl_printer_to_file isl_ctx ctx FILE file __isl_give isl_printer isl_printer_to_str isl_ctx ctx void isl_printer_free __isl_take isl printer printer isl give char isl printer get str isl keep isl printer printer The behavior of the printer can be modified in various ways isl give isl printer isl printer set output format isl take isl printer p int output format isl giv
69. pear in the input matrices and should be a permutation of isl dim cst isl dim param isl dim set and is1_dim_ div for sets and of isl dim cst isl dim param isl dim in isl dim out and isl dim div for relations 1 3 8 Inspecting Sets and Relations Usually the user should not have to care about the actual constraints of the sets and maps but should instead apply the abstract operations explained in the following sec tions Occasionally however it may be required to inspect the individual coefficients of the constraints This section explains how to do so In these cases it may also be useful to have isl compute an explicit representation of the existentially quantified variables isl give isl set isl_set_compute_divs isl take isl set set isl give isl map isl map compute divs isl take isl map map isl give isl union set isl union set compute divs isl take isl union set uset isl give isl union map isl union map compute divs isl take isl union map umap This explicit representation defines the existentiallv quantified variables as integer divisions of the other variables possibly including earlier existentially quantified vari ables An explicitly represented existentially quantified variable therefore has a unique 18 value when the values of the other variables are known If furthermore the same ex istentials i e existentials with the same explicit representations should app
70. plying Tarjan s algorithm 1972 56 Figure 2 1 The relation from Example 2 4 5 In practice we compute the extended powers K of each component separately and then compose them as in 2 6 Note however that in this case the order in which we apply them is important and should correspond to a topological ordering of the strongly connected components Simply applying Tarjan s algorithm will produce topologically sorted strongly connected components The graph on which Tarjan s al gorithm is applied is constructed on the fly That is whenever the algorithm checks if there is an edge between two vertices we evaluate 2 12 The exactness check is performed on each component separatelv If the approximation turns out to be inexact for anv of the components then the entire result is marked inexact and the exactness check is skipped on the components that still need to be handled It should be noted that is only valid for exact transitive closures If over approximations are computed in the right hand side then the result will still be an overapproximation of the left hand side but this result may not be transitively closed If we only separate components based on the condition R o R 0 then there is no problem as this condition will still hold on the computed approximations of the tran sitive closures If however we have exploited during the decomposition and if the
71. pos const char isl basic map get dim name isl keep isl basic map bmap enum isl dim tvpe tvpe unsigned pos const char isl map get dim name isl keep isl map map enum isl dim tvpe tvpe unsigned pos These functions are mostly useful to obtain the names of the parameters 1 3 9 Properties Unary Properties e Emptiness The following functions test whether the given set or relation contains any integer points The fast variants do not perform any computations but simply check if the given set or relation is already known to be empty int isl_basic_set_fast_is_empty __isl_keep isl basic set bset int isl basic set is emptvC isl keep isl basic set bset int isl set is emptv isl keep isl set set int isl union set is emptvC isl keep isl union set uset int isl basic map fast is emptv isl keep isl basic map bmap int isl basic map is emptv isl keep isl basic map bmap int isl map fast is emptvC isl keep isl map map int isl map is emptv isl keep isl map map int isl union map is emptv isl keep isl union map umap e Universality int isl_basic_set_is_universe __isl_keep isl basic set bset int isl basic map is universe isl keep isl basic map bmap int isl set fast is universe isl keep isl set set e Single valuedness int isl map is single valued isl keep isl map map 22 e Bijectivity int isl_map_is_bijective __isl_keep isl map map e Wrapping The followni
72. rent imple mentation only produces exact results for particular cases of piecewise transla tions i e piecewise uniform dependences e Transitive closure __isl_give isl_map isl_map_transitive_closure __isl_take isl map map int exact isl give isl union map isl union map transitive closure C isl take isl union map umap int exact Compute the transitive closure of map The result may be an overapproximation If the result is known to be exact then exact is set to 1 The current implemen tation only produces exact results for particular cases of piecewise translations i e piecewise uniform dependences 27 e Reaching path lengths isl give isl_map isl_map_reaching_path_lengths isl take isl map map int exact Compute a relation that maps each element in the range of map to the lengths of all paths composed of edges in map that end up in the given element The result may be an overapproximation If the result is known to be exact then exact is set to 1 To compute the maximal path length the resulting relation should be postprocessed by isl_map_lexmax In particular if the input relation is a dependence relation mapping sources to sinks then the maximal path length corresponds to the free schedule Note however that isl map lexmax expects the maximum to be finite so if the path lengths are unbounded possibly due to the overapproximation then you will get an error message e Wrapping
73. result turns out not to be exact then we check whether the result is transitively closed If not we recompute the transitive closure skipping the decomposition Note that testing for transitive closedness on the result may be fairly expensive so we may want to make this check configurable Example 2 4 5 Consider the relation in example closure4 that comes with the Omega 57 Figure 2 2 The relation from Example 2 4 6 calculator Kelly et al 1996a R Ri U Ro with Ri y gt yt 1 lt x y lt 10 R x y 9 4 1 y 1 lt x lt 20A5 lt y lt 15 This relation is shown graphically in Figure 2 1 We have Ri o R x y gt xt lyt D 1 lt x lt 9A5 lt y lt 10 R0 Ri x y gt 4 ly D 1 lt x lt 10A4 lt y lt IO Clearly Rio Ry C R o R and so Ri U R2 Rj ORT UR UR Example 2 4 6 Consider the relation on the right of Beletska et al 2009 Figure 2 reproduced in Figure 2 2 The relation can be described as R Ri U RU R3 with Ri ane G edt 3 pli lt s2j 4aAi lt sn 3Aj lt 2i 1Aj lt n Ry n i j gt i j 3 i lt 2j 1 i lt nAj lt 2i 4Aj lt n 3 R3 ne Gp eG hLyj Dlis2j lLaAisn 1Aj lt 2i 1l1Aj lt n 1 The figure shows this relation forn 7 Both R o Ri C Rio R3 and R3 o Rp C R30 R3 which the reader can verify using the iscc calculator Ri n gt i j gt 1 3 i lt 2 j 4 and i lt n 3 and j lt 2 i 1 andj lt n 58 R2 n gt i j gt i j 3
74. roximation of R To check whether the results are exact we need to consider two cases depending on whether R is cyclic where R is defined to be cyclic if Rt maps any element to itself i e Rt N Id 0 If R is acyclic then the inductive definition of is equivalent to its completion i e R RU RoR 55 is a defining property Since T is known to be an overapproximation we only need to check whether TERU RoT This is essentially Theorem 5 of Kelly et al 1996c The only difference is that they only consider lexicographically forward relations a special case of acyclic relations If on the other hand R is cyclic then we have to resort to checking whether the approximation K of the power is exact Note that T may be exact even if K is not exact so the check is sound but incomplete To check exactness of the power we simply need to check 2 1 Since again K is known to be an overapproximation we only need to check whether K Iyae Xan CR K lyar xas122 CR oK lyasi aaei21 gt where R x gt y x gt y RA yay Xa 1 1 i e R extended with path lengths equal to 1 All that remains is to explain how to check the cyclicity of R Note that the ex actness on the power is always sound even in the acyclic case so we only need to be careful that we find all cyclic cases Now if R is cyclic i e R N Id 0 then since T is an overapproximation of R also T N Id 0 This in turn means
75. sl set set isl take isl set dom isl give isl set empty isl give isl set isl set partial lexmax isl take isl set set isl take isl set dom isl give isl set empty Given a basic set set or bset the following functions simplv return a set con taining the lexicographic minimum or maximum of the elements in set or bset In case of union sets the optimum is computed per space isl give isl set isl take isl give isl set isl take isl give isl set isl take isl give isl set isl basic set lexmin isl basic set bset isl basic set lexmax isl basic set bset isl set lexmin isl set set isl set lexmax 32 __isl_take isl_set set __isl_give isl_union_set isl_union_set_lexmin __isl_take isl union set uset isl give isl union set isl union set lexmax isl take isl union set uset Given a basic relation map or bmap and a domain dom the following functions compute a relation that maps each element of dom to the single lexicographic minimum or maximum of the elements that are associated to that same element in map or bmap If empty is not NULL then empty is assigned a set that contains the elements in dom that do not map to anv elements in map or bmap In other words the union of the domain of the result and of empty is equal to dom __isl_give isl_map __isl_take __isl_take __isl_give __isl_give isl_map __isl_take __isl_tak
76. t 1 v bset isl basic set add constraint bset c c isl inequalitv alloc isl dim copv dim isl int set si Cv 10 isl constraint set constant c v isl int set siCv 1 isl constraint set coefficient c isl dim set 0 v bset isl basic set add constraint bset c c isl inequalitv alloc dim isl int set si v 42 isl constraint set constant c v isl int set si Cv 1 isl constraint set coefficient c isl dim set 0 v bset isl basic set add constraint bset c bset isl basic set project out bset isl dim set 1 1 isl int clear v Or alternativelv 17 struct isl_basic_set bset bset isl_basic_set_read_from_str ctx flil exists a i 2a and i gt 10 and i lt 42 1 A basic set or relation can also be constructed from two matrices describing the equalities and the inequalities __isl_give isl basic set isl basic set from constraint matrices isl take isl_dim dim isl take isl mat eq isl take isl mat ineq enum isl dim tvpe cl enum isl dim tvpe c2 enum isl dim tvpe c3 enum isl dim tvpe c4 isl give isl basic map isl basic map from constraint matrices isl take isl_dim dim isl take isl mat eq isl take isl mat ineq enum isl dim tvpe cl enum isl dim tvpe c2 enum isl dim tvpe c3 enum isl dim tvpe cA enum isl dim tvpe c5 The isl dim tvpe arguments indicate the order in which different kinds of vari ables ap
77. t columns but before the final constant column The output is the lexicographic minimum of the parametric polyhedron As isl currently does not have its own output format the output is just a dump of the internal state 1 4 3 isl polvhedron minimize isl polvhedron minimize computes the minimum of some linear or affine objective function over the integer points in a polyhedron If an affine objective function is given then the constant should appear in the last column 1 4 4 isl polvtope scan Given a polvtope isl polvtope scan prints all integer points in the polvtope 48 1 5 isl polvlib The isl polvlib librarv provides the following functions for converting between isl objects and PolvLib objects The librarv is distributed separatelv for licensing reasons include lt isl_set_polylib h gt __isl_give isl_basic_set isl_basic_set_new_from_polylib Polyhedron P __isl_take isl_dim dim Polyhedron isl_basic_set_to_polylib __isl_keep isl basic set bset isl give isl set isl set new from polvlib Polvhedron D isl take isl dim dim Polyhedron isl set to polvlib C isl keep isl set set include lt isl_map_polylib h gt __isl_give isl basic map isl_basic_map_new_from_polylib Polyhedron P isl take isl_dim dim isl give isl map isl map new from polvlib Polvhedron D isl take isl_dim dim Polyhedron isl basic map to polvlib isl keep isl basic map bmap Polyhedron isl map
78. than the first n dimensions in the range 15 A basic set or relation can be converted to a set or relation using the following functions __isl_give isl_set isl_set_from_basic_set __isl_take isl basic set bset isl give isl map isl map from basic map isl take isl basic map bmap Sets and relations can be converted to union sets and relations using the following functions isl give isl union map isl union map from mapC isl take isl map map isl give isl union set isl union set from set isl take isl set set Sets and relations can be copied and freed again using the following functions isl give isl basic set isl basic set copv isl keep isl basic set bset isl give isl set isl set copv isl keep isl set set isl give isl union set isl union set copv isl keep isl union set uset isl give isl basic map isl basic map copvC isl keep isl basic map bmap isl give isl map isl map copvC isl keep isl map map isl give isl union map isl union map copv C isl keep isl union map umap void isl basic set free isl take isl basic set bset void isl set free isl take isl set set void isl union set free isl take isl union set uset void isl basic map free isl take isl basic map bmap void isl map free isl take isl map map void isl union map free isl take isl union map umap Other sets and relations can be constructed
79. the gist operation to each of the cells in the domain of the input piecewise quasipolvnomial The context is also exploited to simplifv the quasipolvnomials associated to each cell isl give isl pw qpolvnomial isl pw qpolvnomial to polvnomial isl take isl pw qpolvnomial pwqp int sign isl give isl union pw qpolvnomial isl union pw qpolvnomial to polvnomial isl take isl union pw qpolvnomial upwqp int sign Approximate each quasipolvnomial bv a polvnomial If sign is positive the polv nomial will be an overapproximation If sign is negative it will be an underapproxi mation If sign is zero the approximation will lie somewhere in between 1 3 15 Bounds on Piecewise Quasipolynomials and Piecewise Quasipoly nomial Reductions A piecewise quasipolynomial reduction is a piecewise reduction or fold of quasipoly nomials In particular the reduction can be maximum or a minimum The objects are mainly used to represent the result of an upper or lower bound on a quasipolynomial over its domain i e as the result of the following function isl give isl_pw_qpolynomial_fold isl_pw_qpolynomial_bound isl take isl pw qpolvnomial pwqp enum isl fold tvpe int tight 41 isl give isl_union_pw_qpolynomial_fold isl_union_pw_qpolynomial_bound isl take isl union pw qpolvnomial upwqp enum isl fold tvpe int tight The type argument may be either isl fold min or isl fold max If tight is not NU
80. ther it is a must or may dependence a token identifying the source and an additional void with value equal to the third argument of the isl flow foreach call A dependence is marked must if it originates from a must source and if it is not followed by any may sources After finishing with an isl flow the user should call isl flow free to free all associated memory A higher level interface to dependence analysis is provided by the following func tion include lt isl flow h gt int isl_union_map_compute_flow __isl_take isl union map sink isl take isl union map must source isl take isl union map mav source isl take isl union map schedule isl give isl union map must_dep isl give isl union map may_dep isl give isl union set must no source isl give isl union set mav no source The arrays are identified by the tuple names of the ranges of the accesses The iteration domains by the tuple names of the domains of the accesses and of the schedule The relative order of the iteration domains is given by the schedule Any of must_dep 46 may_dep must_no_source or may_no_source may be NULL but a NULL value for any of the other arguments is treated as an error 1 3 17 Parametric Vertex Enumeration The parametric vertex enumeration described in this section is mainly intended to be used internally and by the barvinok library include lt isl vertices h gt isl give isl vertic
81. to polvlibC isl keep isl map map 49 Chapter 2 Implementation Details 2 1 Sets and Relations Definition 2 1 1 Polyhedral Set A polyhedral set S is a finite union of basic sets S Si each of which can be represented using affine constraints S Z gt 2 s1 Ss x eZ Iz Zf Ax Bs Dz c gt 0 with A Z 4 Be Z D e ZP ande e Z Definition 2 1 2 Parameter Domain of a Set Let S Z gt 2 be a set The pa rameter domain of S is the set pdomS s Z S s 4 0 Definition 2 1 3 Polyhedral Relation A polyhedral relation R is a finite union of ba sic relations R Ui R of type Z gt 22 each of which can be represented using affine constraints R s gt RAs x gt x Z x Z Jz Zf Aix A2X2 Bs DZ c gt 0 with A Z 4 B e zm D e Z ande Z Definition 2 1 4 Parameter Domain of a Relation Let R Z gt 21777 be a rela tion The parameter domain of R is the set pdomR s Z R s 0 Definition 2 1 5 Domain of a Relation Let R Z gt 22 be a relation The do main of R is the polyhedral set domR s gt x1 Z dx Z x1 X2 R s 50 Definition 2 1 6 Range of a Relation Let R Z gt 22 be a relation The range of R is the polyhedral set ranR s x Z Ax Z x1 x2 R s Definition 2 1 7 Composition of Relations Let R Z gt 22
82. which piplib library to use either an installed version system an externally built version build or no version no The option build is mostly useful in configure scripts of larger projects that bundle both isl and piplib prefix Installation prefix for isl with gmp prefix Installation prefix for GMP architecture independent files with gmp exec prefix Installation prefix for GMP architecture dependent files with piplib Which copy of piplib to use either no default system or build with piplib prefix Installation prefix for system piplib architecture independent files with piplib exec prefix Installation prefix for system piplib architecture dependent files with piplib builddir Location where build piplib was built 3 Compile make 4 Install optional make install 1 3 Library 1 3 1 Initialization All manipulations of integer sets and relations occur within the context of an isl_ctx A given isl ctx can only be used within a single thread All arguments of a function are required to have been allocated within the same context There are currently no functions available for moving an object from one isl_ctx to another isl ctx This means that there is currently no way of safely moving an object from one thread to another unless the whole isl ctx is moved An isl ctx can be allocated using isl ctx alloc and freed using isl ctx free All objects allocated within an isl ctx should be freed be

Download Pdf Manuals

Related Search

Related Contents

Bryan Boilers RV350 User's Manual  Benutzerhandbuch  Forces commnes n°20 - Communauté de Communes Bourganeuf    Wormhole Switch JUC100 －New Version  Samsung LN22C350 manual do usuário  Can Humans Think?  800AJ - Jofemesa  Arcam fmj DV139 User's Manual  BETRIEBSANLEITUNG MX32, MX32FU  

Copyright © All rights reserved. Failed to retrieve file