Home

Integer Set Library: Manual

1. 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_type type int pos isl_int v int isl_constraint_involves_dims __isl_keep isl_constraint constraint enum isl_dim_type type unsigned first unsigned n The explicit representations of the existentially quantified variables can be inspected using the following function Note that the user is only allowed to use this func tion if the inspected set or map is the result of a call to isl_set_compute_divs or isl_map_compute_divs The existentially quantified variable is equal to the floor of the returned affine expression The affine expression itself can be inspected using the functions in 91 3 17 __isl_give isl_aff isl_constraint_get_div __isl_keep isl_constraint constraint int pos 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_type cl enum isl_dim_type c2 enum isl_dim_type c3 enum isl_dim_type c4 __isl_give isl_mat isl_basic_set_inequalities_matrix __isl_keep isl_basic_set bset enum isl_dim_type cl enum isl_dim_type c2 enum isl_dim_type c3 enum isl_dim_type c4 __isl_give isl_mat isl_basic_map
2. int isl_map_foreach_basic_map __isl_keep isl_map map int fn __isl_take isl_basic_map bmap void user void user 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 fn __isl_take isl_constraint c void user void user void isl_constraint_free __isl_take isl_constraint c Again the callback function fn should return O 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 function to find out whether a constraint represents an equality If not it represents an inequality 27 int isl_constraint_is_equality __isl_keep isl_constraint constraint
3. 2 3 5 Preprocessing In this section we describe some transformations that are or can be applied in advance to reduce the running time of the actual dual simplex method with Gomory cuts Feasibility Check and Detection of Equalities Experience with the original PipLib has shown that Gomory cuts do not perform very well on problems that are non obviously empty i e problems with rational solutions but no integer solutions In isl we therefore first perform a feasibility check on the original problem considered as a non parametric problem over the combined space of unknowns and parameters In fact we do not simply check the feasibility but we also check for implicit equalities among the integer points by computing the integer affine hull The algorithm used is the same as that described in below Computing the affine hull is fairly expensive but it can bring huge benefits if any equalities can be found or if the problem turns out to be empty Constraint Simplification If the coefficients of the unknown and parameters in a constraint have a common factor then this factor should be removed possibly rounding down the constant term For example the constraint 2x 5 gt 0 should be simplified to x 3 gt 0 isl performs such simplifications on all sets and relations Recent versions of PipLib also perform this simplification on the input Exploiting Equalities If there are any explicit equalities in the input description P
4. bset int isl_basic_set_is_empty __isl_keep isl_basic_set bset int isl_set_plain_is_empty __isl_keep isl_set set 31 int int int int int int int e Universality int int int isl_set_is_empty __isl_keep isl_set set isl_union_set_is_empty __isl_keep isl_union_set uset isl_basic_map_plain_is_empty __isl_keep isl_basic_map bmap isl_basic_map_is_empty __isl_keep isl_basic_map bmap isl_map_plain_is_empty __isl_keep isl_map map isl_map_is_empty __isl_keep isl_map map isl_union_map_is_empty __isl_keep isl_union_map umap isl_basic_set_is_universe __isl_keep isl_basic_set bset isl_basic_map_is_universe __isl_keep isl_basic_map bmap isl_set_plain_is_universe __isl_keep isl_set set e Single valuedness e Injectivity e Bijectivity e Position int int int int int int int int int int int isl_map_is_single_valued __isl_keep isl_map map isl_union_map_is_single_valued __isl_keep isl_union_map umap isl_map_plain_is_injective __isl_keep isl_map map isl_map_is_injective __isl_keep isl_map map isl_union_map_plain_is_injective __isl_keep isl_union_map umap isl_union_map_is_injective __isl_keep isl_union_map umap isl_map_is_bijective __isl_keep isl_map map isl_union_map_is_bijective __isl_keep isl_union_map umap isl_basic_map_plain_is_fixed __isl_keep isl_basic_map bmap enum isl_dim_type type unsigned pos isl_int val
5. int isl_map_find_dim_by_id __isl_keep isl_map map enum isl_dim_type type __isl_keep isl_id id int isl_set_find_dim_by_name __isl_keep isl_set set enum isl_dim_type type const char name int isl_map_find_dim_by_name __isl_keep isl_map map enum isl_dim_type type const char name const char isl_constraint_get_dim_name __isl_keep isl_constraint constraint enum isl_dim_type type unsigned pos const char isl_basic_set_get_dim_name __isl_keep isl_basic_set bset 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 pos const char isl_basic_map_get_dim_name __isl_keep isl_basic_map bmap enum isl_dim_type type unsigned pos const char isl_map_get_dim_name __isl_keep isl_map map enum isl_dim_type type unsigned pos These functions are mostly useful to obtain the identifiers positions or names of the parameters Identifiers of individual dimensions are essentially only useful for printing They are ignored by all other operations and may not be preserved across those operations 1 3 12 Properties Unary Properties e Emptiness The following functions test whether the given set or relation contains any integer points The plain 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_plain_is_empty __isl_keep isl_basic_set
6. FILE input __isl_give isl_set isl_set_read_from_str isl_ctx ctx const char str include lt isl map h gt __isl_give isl_basic_map isl_basic_map_read_from_file isl_ctx ctx FILE input __isl_give isl_basic_map isl_basic_map_read_from_str isl_ctx ctx const char str __isl_give isl_map isl_map_read_from_file isl_ctx ctx FILE input __isl_give isl_map isl_map_read_from_str isl_ctx ctx const char str include lt isl union_set h gt 18 __isl_give isl_union_set isl_union_set_read_from_file isl_ctx ctx FILE input __isl_give isl_union_set isl_union_set_read_from_str isl_ctx ctx const char str include lt isl union_map h gt __isl_give isl_union_map isl_union_map_read_from_file isl_ctx ctx FILE input __isl_give isl_union_map isl_union_map_read_from_str isl_ctx ctx const char str The input format is autodetected and may be either the PolyLib format or the isl 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 _
7. isl_set_plain_is_fixed __isl_keep isl_set set enum isl_dim_type type unsigned pos isl_int val isl_map_plain_is_fixed __isl_keep isl_map map enum isl_dim_type type unsigned pos isl_int val 32 Check if the relation obviously lies on a hyperplane where the given dimension has a fixed value and if so return that value in val e Space To check whether a set is a parameter domain use this function int isl_set_is_params __isl_keep isl_set set int isl_union_set_is_params __isl_keep isl_union_set uset e Wrapping The following functions check whether the domain of the given basic set is a wrapped relation int isl_basic_set_is_wrapping __isl_keep isl_basic_set bset int isl_set_is_wrapping __isl_keep isl_set set e Internal Product int isl_basic_map_can_zip __isl_keep isl_basic_map bmap int isl_map_can_zip __isl_keep isl_map map Check whether the product of domain and range of the given relation can be computed i e whether both domain and range are nested relations Binary Properties e Equality int isl_set_plain_is_equal __isl_keep isl_set set1 __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 bmap1 __isl_keep isl_basic_map bmap2 int isl_map_is_equal __isl_keep isl_
8. AR 0 1 y y lt 1 102 and we obtain the approximation n gt x Y gt x y n gt 2AxX gt 1l4 exay lt xt y x If we consider both AR and A R then we obtain n gt x y gt x y n z2 2Ay lt l n yAx gt 1l xAy lt x y x Note however that this is not the most accurate affine approximation that can be ob tained That would be n gt x y gt x y y lt S2 n x y x An gt z2Ax gt l x 2 5 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 overapproximation 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 Q If R is acyclic then the inductive definition of is equivalent to its completion i e R RU RoR is a defining property Since T is known to be an overapproximation we only need to check whether TCRU 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 inc
9. Polynomial approximations in the polytope model Bringing the power of quasi polynomials to the masses In J Sankaran and T Vander Aa Eds Digest of the 6th Workshop on Optimization for DSP and Embedded Systems ODES 6 91 Nelson C G 1980 Techniques for program verification Ph D thesis Stanford University Stanford CA USA 87 Schrijver A 1986 Theory of Linear and Integer Programming John Wiley amp Sons 100 Seghir R and V Loechner 2006 October Memory optimization by counting points in integer transformations of parametric polytopes In Proceedings of the International Conference on Compilers Architectures and Synthesis for Em bedded Systems CASES 2006 Seoul Korea 95 112 Tarjan R 1972 Depth first search and linear graph algorithms SIAM Journal on Computing 1 2 146 160 104 Verdoolaege S 2006 barvinok version 0 22 Available from http freshmeat net projects barvinok 87 Verdoolaege S 2009 April An integer set library for program analysis 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 Verdoolaege S K Beyls M Bruynooghe and F Catthoor 2005 Experiences with enumeration of integer projections of parametric polytopes In R Bodik Ed Proceedings of 14th International Conference on Compiler Construc tion Edinburgh Scotland Volume 3443
10. __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 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 10 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_space space __isl_give isl_basic_map isl_basic_map_empty __isl_take isl_space space __isl_give isl_set isl_set_empty __isl_take isl_space space __isl_give isl_map isl_map_empty __isl_take isl_space space __isl_give isl_union_set isl_union_set_empty 20 __isl_take isl_space space __isl_give isl_union_map isl_union_map_empty __isl_take isl_space space For isl_union_sets and isl_union_maps the space is only used to specify the parameters Universe sets and relations __isl_give isl_basic_set isl_basic_set_universe __isl_take isl_space space __isl_give isl_basic_map isl_basic_map_universe __isl_take isl_space space __isl_give isl_set isl_set_universe
11. __isl_keep isl_union_pw_qpolynomial upwaqp int fn __isl_take isl_pw_qpolynomial pwqp void user void user To extract the piecewise quasipolynomial in a given space from a union use __isl_give isl_pw_qpolynomial isl_union_pw_qpolynomial_extract_pw_qpolynomial __isl_keep isl_union_pw_qpolynomial upwaqp __isl_take isl_space space To iterate over the cells in a piecewise quasipolynomial use either of the following two functions int isl_pw_qpolynomial_foreach_piece __isl_keep isl_pw_qpolynomial pwqp int fn __isl_take isl_set set __isl_take isl_qpolynomial qp void user void user int isl_pw_qpolynomial_foreach_lifted_piece __isl_keep isl_pw_qpolynomial pwqp int fn __isl_take isl_set set __isl_take isl_qpolynomial 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_qpolynomial_foreach_piece and isl_pw_qpolynomial_foreach_lifted_piece is that isl_pw_qpolynomial_foreach_lifted_piece will first compute unique rep resentations for all existentially quantified variables and then turn these existentially quantified variables into extra set variables adapting the associated quasipolynomial accordingly This means that the set passed to fn will not have any existentially 69 quantified variables but that the dimensions of the sets may be different for different invocations of fn To iterate over all terms i
12. __isl_take isl_local_space ls enum isl_dim_type type unsigned n __isl_give isl_local_space isl_local_space_insert_dims __isl_take isl_local_space ls enum isl_dim_type type unsigned first unsigned n __isl_give isl_local_space isl_local_space_drop_dims __isl_take isl_local_space ls enum isl_dim_type type unsigned first unsigned n 1 3 9 Input and Output isl supports its own input output format which is similar to the Omega format but also supports the PolyLib format in some cases isl format The isl format is similar to that of Omega but has a different syntax for describing the parameters and allows for the definition of an existentially quantified variable as the integer division of an affine expression For example the set of integers i between 0 and n such that i 10 lt 6 can be described as n gt i exists a 1 10 09 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 17 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 represent
13. in turn means that Tay 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 z2 gt 0 w dao a k fi k gt lAy xt fAw Zzt ka Tay 24 nA5a 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 dao q 7a 2 nA 6o 2 x y A 5 o lt 1 x y The fact that we ignore some impure constraints clearly leads to a loss of accuracy In some cases some of this loss can be recovered by not considering the parameters in a special way That is instead of considering the set A AR s 6 Z Ix gt yER 6 y x we consider the set A AR 6 Z As x gt s y R 6 s s y x The first n coordinates of every element in A are zero Projecting out these zero co ordinates from A is equivalent to projecting out the parameters in A The result is obviously a superset of A but all its constraints are of type and they can therefore all be used in the construction of Qj Example 2 5 6 Consider the relation R n gt x y gt 1 x l n y n gt 2 We have AR n gt U 1l n n 2 and so by treating the parameters in a special way we obtain the following approxi mation for R n gt x y gt X y n 2aAy lt l nt yAx gt 14 x If we consider instead R n x y gt nj 1 x 1 n y n gt 2 then
14. would use the following code isl_space space isl_local_space ls isl_constraint c isl_basic_set bset space isl_space_set_alloc ctx 0 2 bset isl_basic_set_universe isl_space_copy space ls isl_local_space_from_space space c isl_equality_alloc isl_local_space_copy ls c isl_constraint_set_coefficient_si c isl_dim_set 0 1 c isl_constraint_set_coefficient_si c isl_dim_set 1 2 bset isl_basic_set_add_constraint bset c c isl_inequality_alloc isl_local_space_copy ls c isl_constraint_set_constant_si c 10 c isl_constraint_set_coefficient_si c isl_dim_set 0 1 bset isl_basic_set_add_constraint bset c c isl_inequality_alloc ls c isl_constraint_set_constant_si c 42 c isl_constraint_set_coefficient_si c isl_dim_set 0 1 bset isl_basic_set_add_constraint bset c bset isl_basic_set_project_out bset isl_dim_set 1 1 Or alternatively isl_basic_set bset bset isl_basic_set_read_from_str ctx i exists a i 2a and i gt 10 and i lt 42 24 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_space space __isl_take isl_mat eq __isl_take isl_mat ineq enum isl_dim_type cl enum isl_dim_type c2 enum isl_dim_type c3 enum isl_dim_type c4 __isl_give isl_basic_map isl_basic_map_
15. 3 2 The Dual Simplex Method Tableaus can be represented in several slightly different ways In is1 the dual simplex method uses the same representation as that used by its incremental LP solver based on the primal simplex method The implementation of this LP solver is based on that of Simplify Detlefs et al 2005 which in turn was derived from the work of 1980 In the original Nelson 1980 the tableau was implemented as a sparse matrix but neither Simplify nor the current implementation of is1 does so Given some affine constraints on the variables Ax b gt 0 the tableau represents the relationship between the variables x and non negative variables y Ax b cor responding to the constraints The initial tableau contains b A and expresses the constraints y in the rows in terms of the variables x in the columns The main op eration defined on a tableau exchanges a column and a row variable and is called a pivot During this process some coefficients may become rational As in the PipLib implementation isl maintains a shared denominator per row The sample value of a tableau is one where each column variable is assigned zero and each row variable is assigned the constant term of the row This sample value represents a valid solution if each constraint variable is assigned a non negative value i e if the constant terms of rows corresponding to constraints are all non negative The dual simplex method starts from an initial sa
16. Applications Berlin Heidelberg pp 98 109 Springer Verlag Boulet P and X Redon 1998 Communication pre evaluation in HPF In EU ROPAR 98 Volume 1470 of Lecture Notes in Computer Science pp 263 272 Springer Verlag Berlin 87 Bygde S 2010 March Static WCET analysis based on abstract interpretation and counting of elements Licentiate thesis Cook W T Rutherford H E Scarf and D F Shallcross 1991 August An imple mentation of the generalized basis reduction algorithm for integer programming Cowles Foundation Discussion Papers 990 Cowles Foundation Yale University available at http ideas repec org p cwl cwldpp 990 html 94 De Loera J A D Haws R Hemmecke P Huggins and R Yoshida 2004 Jan uary Three kinds of integer programming algorithms based on barvinok s ratio nal functions In Integer Programming and Combinatorial Optimization 10th International IPCO Conference Volume 3064 of Lecture Notes in Computer Science pp 244 255 87 De Smet S 2010 April personal communication 100 Detlefs D G Nelson and J B Saxe 2005 Simplify a theorem prover for pro gram checking J ACM 52 3 365 473 87 111 Feautrier P 1988 Parametric integer programming RAIRO Recherche Op rationnelle 22 3 243 268 Feautrier P 1991 Dataflow analysis of array and scalar references International Journal of Parallel Programming 20 1 23 53 87 Feautrier P 1992
17. December Some efficient solutions to the affine scheduling problem Part II multidimensional time International Journal of Parallel Pro gramming 21 6 389 420 Feautrier P J Collard and C Bastoul 2002 Solving systems of affine in equalities Technical report PRiSM Versailles University Galea F 2009 November personal communication 94 Karr M 1976 Affine relationships among variables of a program Acta Informat ica 6 133 151 94 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 104 Kelly W V Maslov W Pugh E Rosser T Shpeisman and D Wonnacott 1996b November The Omega library Technical report University of Maryland 110 Kelly W W Pugh E Rosser and T Shpeisman 1996c Transitive closure of in finite graphs and its applications In C H Huang P Sadayappan 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 Meister B 2004 December Stating and Manipulating Periodicity in the Polytope Model Applications to Program Analysis and Optimization Ph D thesis Uni versit Louis Pasteur 91 Meister B and S Verdoolaege 2008 April
18. Lifting Lift the input set to a space with extra dimensions corresponding to the existen tially quantified variables in the input In particular the result lives in a wrapped map where the domain is the original space and the range corresponds to the original existentially quantified variables __isl_give isl_basic_set isl_basic_set_lift __isl_take isl_basic_set bset __isl_give isl_set isl_set_lift __isl_take isl_set set __isl_give isl_union_set isl_union_set_lift __isl_take isl_union_set uset Given a local space that contains the existentially quantified variables of a set a basic relation that when applied to a basic set has essentially the same effect as isl_basic_set_lift can be constructed using the following function include lt isl local_space h gt __isl_give isl_basic_map isl_local_space_lifting __isl_take isl_local_space ls Internal Product __isl_give isl_basic_map isl_basic_map_zip __isl_take isl_basic_map bmap __isl_give isl_map isl_map_zip __isl_take isl_map map __isl_give isl_union_map isl_union_map_zip __isl_take isl_union_map umap Given a relation with nested relations for domain and range interchange the range of the domain with the domain of the range Aligning parameters __isl_give isl_set isl_set_align_params __isl_take isl_set set __isl_take isl_space model __isl_give isl_map isl_map_align_params __isl_take isl_map map __isl_take isl_spa
19. __isl_take isl_pw_aff pwaff A rational bound on a dimension can be extracted from an isl_constraint using the following function The constraint is required to have a non zero coefficient for the specified dimension include lt isl constraint h gt __isl_give isl_aff isl_constraint_get_bound __isl_keep isl_constraint constraint enum isl_dim_type type int pos The entire affine expression of the constraint can also be extracted using the fol lowing function include lt isl constraint h gt __isl_give isl_aff isl_constraint_get_aff __isl_keep isl_constraint constraint Conversely an equality constraint equating the affine expression to zero or an inequality constraint enforcing the affine expression to be non negative can be con structed using 54 __isl_give isl_constraint isl_equality_from_aff __isl_take isl_aff aff __isl_give isl_constraint isl_inequality_from_aff __isl_take isl_aff aff The expression can be inspected using include lt isl aff h gt isl_ctx isl_aff_get_ctx __isl_keep isl_aff aff int isl_aff_dim __isl_keep isl_aff aff enum isl_dim_type type __isl_give isl_local_space isl_aff_get_domain_local_space __isl_keep isl_aff aff __isl_give isl_local_space isl_aff_get_local_space __isl_keep isl_aff aff const char isl_aff_get_dim_name __isl_keep isl_aff aff enum isl_dim_type type unsigned pos const char isl_pw_aff_get_dim_name __isl_keep isl_pw_a
20. _int_is_pos i is _int_is_neg i isl_int_is_nonpos i is _int_is_nonneg i isl_int_is_divisible_by 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 is1_set and isl_map represent unions of isl_basic_sets and isl_basic_maps respectively However all isl_basic_sets or isl_basic_maps in the union need to live in the same space isl_union_sets and isl_union_maps represent unions of isl_sets or isl_maps in different spaces where spaces are con sidered different if they have a different number of dimensions and or different names see 41 3 7 The difference between sets and relations maps is that sets have one set of variables 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 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 making sure tha
21. a valid solution for the original problem we need to find a non negative value of c satisfying the constraints If b p gt 0 we can take t 0 so that c cj t cj gt 0 If b p lt 0 we can take t b p Since r b p c f 0 and f gt 0 we have c c b p 0 Note that these choices amount to plugging in t b p max b p 0 Conversely given a solution to the new problem we need to find a non negative value of cj but this is easy since cj c t and both of these are non negative Plugging in t max b p 0 can be performed as in Section 2 3 6 but as in the case of offline symmetry detection it may be better to provide a direct representation for such expressions in the internal representation of sets and relations or at least in a quast like output format 2 4 Coalescing See Verdoolaege 2009 for now More details will be added later 96 2 5 Transitive Closure 2 5 1 Introduction Definition 2 5 1 Power of a Relation Let R Z gt 22 be a relation and k Zs a positive number then power k of relation R is defined as R ifk 1 RE if 2 1 RoR ifk gt 2 Definition 2 5 2 Transitive Closure of a Relation Let R Z gt 22 be a relation then the transitive closure R of R is the union of all positive powers of R Rt e k21 Alternatively the transitive closure may be defined inductively as R RU Ro R 2 2 Since the transitiv
22. affine expression is the maximum of those of pwaff1 and pwaff2 If only one of pwaff1 or pwaff2 is defined on a given cell then the associated expres sion is the defined one An expression can be read from input using include lt isl aff h gt __isl_give isl_aff isl_aff_read_from_str isl_ctx ctx const char str __isl_give isl_pw_aff isl_pw_aff_read_from_str isl_ctx ctx const char str An expression can be printed using include lt isl aff h gt __isl_give isl_printer isl_printer_print_aff __isl_take isl_printer p __isl_keep isl_aff aff __isl_give isl_printer isl_printer_print_pw_aff __isl_take isl_printer p __isl_keep isl_pw_aff pwaff 1 3 18 Piecewise Multiple Quasi Affine Expressions An isl_multi_aff object represents a sequence of zero or more affine expressions all defined on the same domain space An isl_multi_aff can be constructed from a isl_aff_list using the following function include lt isl aff h gt __isl_give isl_multi_aff isl_multi_aff_from_aff_list __isl_take isl_space space __isl_take isl_aff_list list An empty piecewise multiple quasi affine expression one with no cells or a piece wise multiple quasi affine expression with a single cell can be created using the follow ing functions 61 include lt isl aff h gt __isl_give isl_pw_multi_aff isl_pw_multi_aff_empty __isl_take isl_space space __isl_give isl_pw_multi_aff isl_pw_multi_aff_alloc __isl
23. and multiplication on the resulting quasipolynomials __isl_give isl_qpolynomial isl_qpolynomial_zero_on_domain __isl_take isl_space domain __isl_give isl_qpolynomial isl_qpolynomial_one_on_domain __isl_take isl_space domain 67 __isl_give isl_qpolynomial isl_qpolynomial_infty_on_domain __isl_take isl_space domain __isl_give isl_qpolynomial isl_qpolynomial_neginfty_on_domain __isl_take isl_space domain __isl_give isl_qpolynomial isl_qpolynomial_nan_on_domain __isl_take isl_space domain __isl_give isl_qpolynomial isl_qpolynomial_rat_cst_on_domain __isl_take isl_space domain const isl_int n const isl_int d __isl_give isl_qpolynomial isl_qpolynomial_var_on_domain __isl_take isl_space domain enum isl_dim_type type unsigned pos __isl_give isl_qpolynomial isl_qpolynomial_from_aff __isl_take isl_aff aff Note that the space in which a quasipolynomial lives is a map space with a one dimensional range The domain argument in some of the functions above corresponds to the domain of this map space The zero piecewise quasipolynomial or a piecewise quasipolynomial with a sin gle cell can be created using the following functions Multiple of these single cell piecewise quasipolynomials can be combined to create more complicated piecewise quasipolynomials __isl_give isl_pw_qpolynomial isl_pw_qpolynomial_zero __isl_take isl_space space __isl_give isl_pw_qpolynomial isl_pw_qpolynomial_allo
24. 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 say that they use D dom R Uran R but presumably they mean that they use D domR UranR Now this expression of D contains a union so it not directly usable do not explain how they avoid this union Apparently in their implementation they are using the convex hull of domR U ranR or at least an approximation of this convex hull We use the simple hull 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 each j i either dom R C D or dom Rj N ran R 0 2 14 and similarly for each j i either ran R C Dor ran R N dom R 0 2 15 then we can refine to RFU Corjecjul J corfu J recju LR dom R CD dom R Nran R 0 dom R CD dom R jNran R 0 ranR CD ran R CD ran R dom R 0 ran R Adom R 0 If only property 2 14 holds we can use 4 dom R Nran R 0 while if only property 2 15 holds we can use rofe U aoc U consul U aj c vw dom R CD ran R CD ran RjNdom 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 co
25. 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 destroyed 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 vertex void isl_vertex_free __isl_take isl_vertex vertex 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
26. empty Given a basic map map or bmap the following functions simply 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 The following functions return their result in the form of a piecewise multi affine expression See 1 3 18 but are otherwise equivalent to the corresponding functions returning a basic set or relation __isl_give isl_pw_multi_aff isl_basic_map_lexmin_pw_multi_aff __isl_take isl_basic_map bmap 51 __isl_give isl_pw_multi_aff isl_basic_set_partial_lexmin_pw_multi_aff __isl_take isl_basic_set bset __isl_take isl_basic_set dom __isl_give isl_set empty __isl_give isl_pw_multi_aff isl_basic_set_partial_lexmax_pw_multi_aff __isl_take isl_basic_set bset __isl_take isl_basic_set dom __isl_give isl_set empty __isl_give isl_pw_multi_aff isl_basic_map_partia
27. is a row variable then the row already appears somewhere else in the tableau In case of parametric problems the sign of the constant term may depend on the parameters Each time the constant term of a constraint row changes we therefore need to check whether the new term can attain negative and or positive values over the current set of possible parameter values i e the context If all these terms can only attain non negative values the current state of the tableau represents a solution If one of the terms can only attain non positive values and is not identically zero the corresponding row can be pivoted Otherwise we pick one of the terms that can attain both positive and negative values and split the context into a part where it only attains non negative values and a part where it only attains negative values 2 3 3 Gomory Cuts The solution found by the dual simplex method may have non integral coordinates If so some rational solutions including the current sample value can be cut off by applying a parametric Gomory cut Let r b p a c be the row corresponding to the first non integral coordinate of x with b p the constant term an affine expression in the parameters p i e b p f p g Note that only row variables can attain non integral values as the sample value of the column variables is zero Consider the expression b p b p a c with the ceiling function and the fractional part This expre
28. isl_id id Note that is1_id_get_name returns a pointer to some internal data structure so the result can only be used while the corresponding is1_id is alive 1 3 7 Spaces Whenever a new set or relation is created from scratch the space in which it lives needs to be specified using an isl_space include lt isl space h gt __isl_give isl_space isl_space_alloc isl_ctx ctx unsigned nparam unsigned n_in unsigned n_out __isl_give isl_space isl_space_params_alloc isl_ctx ctx unsigned nparam __isl_give isl_space isl_space_set_alloc isl_ctx ctx 11 unsigned nparam unsigned dim __isl_give isl_space isl_space_copy __isl_keep isl_space space void isl_space_free __isl_take isl_space space unsigned isl_space_dim __isl_keep isl_space space enum isl_dim_type type The space used for creating a parameter domain needs to be created using isl_space_params_alloc For other sets the space needs to be created using isl_space_set_alloc while for a relation the space needs to be created using isl_space_alloc isl_space_dim can be used to find out the number of dimensions of each type in a space where type may be isl_dim_ param is1_dim_in only for relations is1_dim_out only for relations isl_dim_set only for sets or isl_dim_all To check whether a given space is that of a set or a map or whether it is a parameter space use these functions include lt isl space h gt int isl_space_is_params __isl
29. isl_set isl_set context isl_set_gist_params isl_set set isl_set context set __isl_give isl_union_set isl_union_set_gist __isl_take __isl_take isl_union_set uset isl_union_set context __isl_give isl_union_set isl_union_set_gist_params __isl_take __isl_take isl_union_set uset isl_set set __isl_give isl_basic_map isl_basic_map_gist __isl_take __isl_take __isl_give isl_map __isl_take __isl_give isl_map __isl_take __isl_take __isl_give isl_map __isl_take __isl_take __isl_give isl_map __isl_take __isl_take isl_basic_map bmap isl_basic_map context isl_map_gist __isl_take isl_map map isl_map context isl_map_gist_params isl_map map isl_set context isl_map_gist_domain isl_map map isl_set context isl_map_gist_range isl_map map isl_set context __isl_give isl_union_map isl_union_map_gist __isl_take __isl_take isl_union_map umap isl_union_map context __isl_give isl_union_map isl_union_map_gist_params __isl_take __isl_take isl_union_map umap isl_set set __isl_give isl_union_map isl_union_map_gist_domain __isl_take isl_union_map umap 49 __isl_take isl_union_set uset 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 inequal
30. isl_space space enum isl_dim_type type const char name The identifiers or names of entire spaces may be set or read off using the following functions include lt isl space h gt __isl_give isl_space isl_space_set_tuple_id __isl_take isl_space space enum isl_dim_type type __isl_take isl_id id __isl_give isl_space isl_space_reset_tuple_id __isl_take isl_space space enum isl_dim_type type int isl_space_has_tuple_id __isl_keep isl_space space enum isl_dim_type type __isl_give isl_id isl_space_get_tuple_id __isl_keep isl_space space enum isl_dim_type type __isl_give isl_space isl_space_set_tuple_name __isl_take isl_space space enum isl_dim_type type const char s const char isl_space_get_tuple_name __isl_keep isl_space space enum isl_dim_type type 14 The type argument needs to be one of is1_dim_in isl_dim_out or isl_dim_set As with isl_space_get_name the isl_space_get_tuple_name function returns a pointer to some internal data structure Binary 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 spaces include lt isl space h gt int isl_space_is_wrapping __isl_keep isl_space space __isl_give isl_space isl_space_wrap __isl_take isl_space space __
31. isl_union_pw_qpolynomial upwqp1 __isl_keep isl_union_pw_qpolynomial upwqp2 Operations on Piecewise Quasipolynomials __isl_give isl_qpolynomial isl_qpolynomial_scale __isl_take isl_qpolynomial qp isl_int v __isl_give isl_qpolynomial isl_qpolynomial_neg 70 __isl_take isl_qpolynomial qp __isl_give isl_qpolynomial isl_qpolynomial_add __isl_take isl_qpolynomial qp1 __isl_take isl_qpolynomial qp2 __isl_give isl_qpolynomial isl_qpolynomial_sub __isl_take isl_qpolynomial qp1 __isl_take isl_qpolynomial qp2 __isl_give isl_qpolynomial isl_qpolynomial_mul __isl_take isl_qpolynomial qp1 __isl_take isl_qpolynomial qp2 __isl_give isl_qpolynomial isl_qpolynomial_pow __isl_take isl_qpolynomial qp unsigned exponent __isl_give isl_pw_qpolynomial isl_pw_qpolynomial_add __isl_take isl_pw_qpolynomial pwqp1 __isl_take isl_pw_qpolynomial pwqp2 __isl_give isl_pw_qpolynomial isl_pw_qpolynomial_sub __isl_take isl_pw_qpolynomial pwqp1 __isl_take isl_pw_qpolynomial pwqp2 __isl_give isl_pw_qpolynomial isl_pw_qpolynomial_add_disjoint __isl_take isl_pw_qpolynomial pwqp1 __isl_take isl_pw_qpolynomial pwqp2 __isl_give isl_pw_qpolynomial isl_pw_qpolynomial_neg __isl_take isl_pw_qpolynomial pwaqp __isl_give isl_pw_qpolynomial isl_pw_qpolynomial_mul __isl_take isl_pw_qpolynomial pwqp1 __isl_take isl_pw_qpolynomial pwqp2 __isl_give isl_pw_qpolynomial isl_pw_qpolynomial_pow __i
32. mapping from the domains to the scheduled space can be obtained from an isl_schedule using the following function __isl_give isl_union_map isl_schedule_get_map __isl_keep isl_schedule sched A representation of the schedule can be printed using __isl_give isl_printer isl_printer_print_schedule __isl_take isl_printer p __isl_keep isl_schedule schedule A representation of the schedule as a forest of bands can be obtained using the following function __isl_give isl_band_list isl_schedule_get_band_forest __isl_keep isl_schedule schedule The list can be manipulated as explained in 1 3 15 The bands inside the list can be copied and freed using the following functions include lt isl band h gt __isl_give isl_band isl_band_copy __isl_keep isl_band band void isl_band_free __isl_take isl_band band Each band contains zero or more scheduling dimensions These are referred to as the members of the band The section of the schedule that corresponds to the band is referred to as the partial schedule of the band For those nodes that participate in a band the outer scheduling dimensions form the prefix schedule while the inner scheduling dimensions form the suffix schedule That is if we take a cut of the band forest then the union of the concatenations of the prefix partial and suffix schedules of each band in the cut is equal to the entire schedule modulo some possible padding at the end with zero
33. of Lecture Notes in Computer Science Berlin pp 91 105 Springer Verlag Verhaegh W F J 1995 Multidimensional Periodic Scheduling Ph D thesis Technische Universiteit Eindhoven 95 113
34. scheduling dimensions The properties of a band can be inspected using the following functions 80 include lt isl band h gt isl_ctx isl_band_get_ctx __isl_keep isl_band band int isl_band_has_children __isl_keep isl_band band __isl_give isl_band_list isl_band_get_children __isl_keep isl_band band __isl_give isl_union_map isl_band_get_prefix_schedule __isl_keep isl_band band __isl_give isl_union_map isl_band_get_partial_schedule __isl_keep isl_band band __isl_give isl_union_map isl_band_get_suffix_schedule __isl_keep isl_band band int isl_band_n_member __isl_keep isl_band band int isl_band_member_is_zero_distance __isl_keep isl_band band int pos Note that a scheduling dimension is considered to be zero distance if it does not carry any proximity dependences within its band That is if the dependence distances of the proximity dependences are all zero in that direction for fixed iterations of outer bands A representation of the band can be printed using Options include lt isl band h gt __isl_give isl_printer isl_printer_print_band __isl_take isl_printer p __isl_keep isl_band band include lt isl schedule h gt int isl_options_set_schedule_max_constant_term isl_ctx ctx int val int isl_options_get_schedule_max_constant_term isl_ctx ctx int isl_options_set_schedule_maximize_band_depth isl_ctx ctx int val int isl_options_get
35. trace Other tools that automatically pro vide stack traces on abort or that do not want to continue execution after an error was triggered may also prefer to abort on error The on error behavior of isl can be specified by calling isl_options_set_on_error or by setting the command line option isl on error Valid arguments for the func tion call are ISL_ON_ERROR_WARN ISL_ON_ERROR_CONTINUE and ISL_ON_ERROR_ABORT The choices for the command line option are warn continue and abort It is also possible to query the current error mode include lt isl options h gt int isl_options_set_on_error isl_ctx ctx int val int isl_options_get_on_error isl_ctx ctx 1 3 6 Identifiers Identifiers are used to identify both individual dimensions and tuples of dimensions They consist of a name and an optional pointer Identifiers with the same name but different pointer values are considered to be distinct Identifiers can be constructed copied freed inspected and printed using the following functions include lt isl id h gt __isl_give isl_id isl_id_alloc isl_ctx ctx __isl_keep const char name void user __isl_give isl_id isl_id_copy isl_id id void isl_id_free __isl_take isl_id id isl_ctx isl_id_get_ctx __isl_keep isl_id id void isl_id_get_user __isl_keep isl_id id __isl_keep const char isl_id_get_name __isl_keep isl_id id __isl_give isl_printer isl_printer_print_id __isl_take isl_printer p __isl_keep
36. 2 int pos2 __isl_give isl_map isl_map_equate __isl_take isl_map map enum isl_dim_type typel int posl enum isl_dim_type type2 int pos2 Intersect the set or relation with the hyperplane where the given dimensions are equal to each other __isl_give isl_map isl_map_oppose __isl_take isl_map map enum isl_dim_type typel int posl enum isl_dim_type type2 int pos2 Intersect the relation with the hyperplane where the given dimensions have op posite values Identity __isl_give isl_map isl_set_identity __isl_take isl_set set __isl_give isl_union_map isl_union_set_identity __isl_take isl_union_set uset Construct an identity relation on the given union set Deltas 37 __isl_give isl_basic_set isl_basic_map_deltas __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_map_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 __isl_give isl_basic_map isl_basic_map_deltas_map __isl_take isl_basic_map bmap __isl_give isl_map isl_map_deltas_map __isl_take isl_map map __isl_give isl_union_map isl_union_map_deltas_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 d
37. Ax Bs Dz e gt 0 with A Z 4 Be Z D e 2 and c 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 0 Definition 2 1 3 Polyhedral Relation A polyhedral relation R is a finite union of ba sic relations R R of type Z gt Qa 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 Z D Z and c Z Definition 2 1 4 Parameter Domain of a Relation Let R Z gt 27 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 85 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 and S Z 3 22 be two relations then the composition of R and S is defined as SoRt sph7 x gt x3 Z x ZB dx Z X1 gt X2 E R S A X2 gt x3 E S s Definition 2 1 8 Difference Set of a Relation Let R Z gt 22 be a relation The difference set A R of R i
38. CP CK wrap unwrap CD dom unwrap NCP CK we obtain rat c_cst c_n gt i2 i3 i3 lt c_n and 13 lt c_cst 2c_n i2 and c_n lt 9 and 2c_n lt c_cst The approximation for k A K solutions CK K is then n gt rat 10 i1 il lt i0 and i gt 1 and il lt 2 n iQ Finally the computed approximation for R T unwrap dx dy gt x y gt x dx y dy K R n gt x y gt x 1 y 1 n n gt 2 T T CCdom R gt Cran R T is n gt x y gt 00 01 ol lt x y o0 and o0 gt 1 x and ol lt 2 n x y o0 and n gt 2 Existentially quantified 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 5 5 Consider the relation R n gt x gt y dao 7a 2 n A 5a l x yAy gt 6 x The difference set of this relation is A AR n gt x dao q 79 2 n 5 1l xAx gt 6 101 The existentially quantified variables can be defined in terms of the parameters and variables as 2 n d l x ao an amp i 7 5 ay can therefore be treated as a parameter while a can be treated as a variable This
39. Integer Set Library Manual Version isl 0 09 Sven Verdoolaege December 18 2011 Contents I User Manual 3 1 1 Introduction 2 a ee 3 3 5 1 2 1 Installation from the git repository 5 1 2 2 Common installation instructions 6 be sites as cee ger se op dere ho as os Be eee als E ce oe ee 7 1 3 1 Initialization 2 2 ee ee ee 7 13 2 Integers o i sce gp ae ea ERR SS REPS SERS 7 1 3 3 Sets and Relations 0 0200004 9 1 3 4 Memory Management 9 1 3 5 Error Handling p s e paceca e E L E 10 1 3 6 __ Identifiers a s s empane ew Bete le ae a e EMA s 11 E EE E E E E 11 She od ent bebe ete Se Sie ea hae 16 1 3 9 Inputand Output 2 2 2 a 17 EA e D teenie 20 a ae a e xe A 25 SM te dete Sos A ore Se hee ee oh hee 31 es te dey genes a aes es a at aes ls os Gee 34 nthe MS oe ea Ge ce ee Oi a eee ea 45 TS TS STASIS e ae eke OR a Rb bed hee a Ba hi a E R 52 1 3 16 Matrices lt ss aed ee nd eh we Re SR EA 53 S 54 soho cree 61 13 19 Points 3 62348 eae ee oe Ge eA ee Se EAA aS 65 1 3 20 Piecewise Quasipolynomials 0 0 Vortiurt pee tr rere re ae Teegaa e Bete tne eat Ge 77 1 3 23 Scheduling seo sopce me ke OG Mh a E G 79 Lhe e Aa a A 82 a ea e op sie es Ske e erodes a E ites ne 83 1 4 1 isl_ polyhedron_sample 84 14 2 isl pip i
40. __isl_keep isl_basic_map bmap enum isl_dim_type type unsigned first unsigned n int isl_map_involves_dims __isl_keep isl_map map enum isl_dim_type type unsigned first unsigned n Similarly the following functions can be used to check whether a given dimension is involved in any lower or upper bound int isl_set_dim_has_lower_bound __isl_keep isl_set set enum isl_dim_type type unsigned pos int isl_set_dim_has_upper_bound __isl_keep isl_set set enum isl_dim_type type unsigned pos The identifiers or names of the domain and range spaces of a set or relation can be read off or set using the following functions __isl_give isl_set isl_set_set_tuple_id __isl_take isl_set set __isl_take isl_id id __isl_give isl_set isl_set_reset_tuple_id __isl_take isl_set set int isl_set_has_tuple_id __isl_keep isl_set set __isl_give isl_id isl_set_get_tuple_id 29 __isl_keep isl_set set __isl_give isl_map isl_map_set_tuple_id __isl_take isl_map map enum isl_dim_type type __isl_take isl_id id __isl_give isl_map isl_map_reset_tuple_id __isl_take isl_map map enum isl_dim_type type int isl_map_has_tuple_id __isl_keep isl_map map enum isl_dim_type type __isl_give isl_id isl_map_get_tuple_id __isl_keep isl_map map enum isl_dim_type type const char isl_basic_set_get_tuple_name __isl_keep isl_basic_set bset __isl_give isl_basic_set isl_basic_set_set_tuple_name __isl_take is
41. __isl_take isl_space space __isl_give isl_map isl_map_universe __isl_take isl_space space __isl_give isl_union_set isl_union_set_universe __isl_take isl_union_set uset __isl_give isl_union_map isl_union_map_universe __isl_take isl_union_map umap The sets and relations constructed by the functions above contain all integer val ues while those constructed by the functions below only contain non negative values __isl_give isl_basic_set isl_basic_set_nat_universe __isl_take isl_space space __isl_give isl_basic_map isl_basic_map_nat_universe __isl_take isl_space space __isl_give isl_set isl_set_nat_universe __isl_take isl_space space __isl_give isl_map isl_map_nat_universe __isl_take isl_space space Identity relations __isl_give isl_basic_map isl_basic_map_identity __isl_take isl_space space __isl_give isl_map isl_map_identity __isl_take isl_space space The number of input and output dimensions in space needs to be the same Lexicographic order 21 __isl_give isl_map isl_map_lex_1t __isl_take isl_space set_space __isl_give isl_map isl_map_lex_le __isl_take isl_space set_space __isl_give isl_map isl_map_lex_gt __isl_take isl_space set_space __isl_give isl_map isl_map_lex_ge __isl_take isl_space set_space __isl_give isl_map isl_map_lex_lt_first __isl_take isl_space space unsigned n __isl_give isl_map isl_map_lex_le_first __isl_ta
42. _equalities_matrix __isl_keep isl_basic_map bmap enum isl_dim_type cl enum isl_dim_type c2 enum isl_dim_type c3 enum isl_dim_type c4 enum isl_dim_type c5 __isl_give isl_mat isl_basic_map_inequalities_matrix __isl_keep isl_basic_map bmap enum isl_dim_type cl enum isl_dim_type c2 enum isl_dim_type c3 enum isl_dim_type c4 enum isl_dim_type c5 28 The isl_dim_type 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 number of parameters input output or set dimensions can be obtained using the following functions unsigned isl_basic_set_dim __isl_keep isl_basic_set bset enum isl_dim_type type unsigned isl_basic_map_dim __isl_keep isl_basic_map bmap enum isl_dim_type type unsigned isl_set_dim __isl_keep isl_set set enum isl_dim_type type unsigned isl_map_dim __isl_keep isl_map map enum isl_dim_type type To check whether the description of a set or relation depends on one or more given dimensions it is not necessary to iterate over all constraints Instead the following functions can be used int isl_basic_set_involves_dims __isl_keep isl_basic_set bset enum isl_dim_type type unsigned first unsigned n int isl_set_involves_dims __isl_keep isl_set set enum isl_dim_type type unsigned first unsigned n int isl_basic_map_involves_dims
43. _fold isl_pw_qpolynomial_fold_gist_params __isl_take isl_pw_qpolynomial_fold pwf __isl_take isl_set context __isl_give isl_union_pw_qpolynomial_fold isl_union_pw_qpolynomial_fold_gist __isl_take isl_union_pw_qpolynomial_fold upwf __isl_take isl_union_set context __isl_give isl_union_pw_qpolynomial_fold isl_union_pw_qpolynomial_fold_gist_params __isl_take isl_union_pw_qpolynomial_fold upwf __isl_take isl_set context 76 The gist operation applies the gist operation to each of the cells in the domain of the input piecewise quasipolynomial reduction In future the operation will also exploit the context to simplify the quasipolynomial reductions associated to each cell __isl_give isl_pw_qpolynomial_fold isl_set_apply_pw_qpolynomial_fold __isl_take isl_set set __isl_take isl_pw_qpolynomial_fold pwf int tight __isl_give isl_pw_qpolynomial_fold isl_map_apply_pw_qpolynomial_fold __isl_take isl_map map __isl_take isl_pw_qpolynomial_fold pwf int tight __isl_give isl_union_pw_qpolynomial_fold isl_union_set_apply_union_pw_qpolynomial_fold __isl_take isl_union_set uset __isl_take isl_union_pw_qpolynomial_fold upwf int tight __isl_give isl_union_pw_qpolynomial_fold isl_union_map_apply_union_pw_qpolynomial_fold __isl_take isl_union_map umap __isl_take isl_union_pw_qpolynomial_fold upwf int tight The functions taking a map compose the given map with the given piecewise quasip
44. _isl_give isl_printer isl_printer_set_indent __isl_take isl_printer p int indent __isl_give isl_printer isl_printer_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 may be either ISL_FORMAT_ISL ISL_FORMAT_OMEGA ISL_FORMAT_POLYLIB ISL_FORMAT_EXT_POLYLIB or ISL_FORMAT_LATEX and defaults to ISL_FORMAT_ISL Each line in the output is indented by indent set by isl_printer_set_indent spaces default 0 prefixed by prefix and suffixed by suffix In the PolyLib format output the coefficients of the existentially quantified variables appear between those of the set variables and those of the parameters The function isl_printer_indent increases the indentation by the specified amount which may be negative To actually print something use 19 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 __isl_take isl_printer printer __isl_keep isl_basic_map bmap __isl_give isl_printer isl_printer_print_map __isl_take isl_printer printer
45. _keep isl_space space int isl_space_is_set __isl_keep isl_space space It is often useful to create objects that live in the same space as some other object This can be accomplished by creating the new objects see Creating New Sets and Relations or Creating New Piecewise Quasipolynomials based on the space of the original object include lt isl set h gt __isl_give isl_space isl_basic_set_get_space __isl_keep isl_basic_set bset __isl_give isl_space isl_set_get_space __isl_keep isl_set include lt isl union_set h gt __isl_give isl_space isl_union_set_get_space __isl_keep isl_union_set uset include lt isl map h gt __isl_give isl_space isl_basic_map_get_space __isl_keep isl_basic_map bmap __isl_give isl_space isl_map_get_space __isl_keep isl_map include lt isl union_map h gt __isl_give isl_space isl_union_map_get_space __isl_keep isl_union_map umap include lt isl constraint h gt __isl_give isl_space isl_constraint_get_space __isl_keep isl_constraint constraint 12 set map include lt isl polynomial h gt __isl_give isl_space isl_qpolynomial_get_domain_space __isl_keep isl_qpolynomial qp __isl_give isl_space isl_qpolynomial_get_space __isl_keep isl_qpolynomial qp __isl_give isl_space isl_qpolynomial_fold_get_space __isl_keep isl_qpolynomial_fold fold __isl_give isl_space isl_pw_qpolynomial_get_domain_space __isl_keep isl_pw_qpolynomial pwaq
46. _local_space_dim __isl_keep isl_local_space ls enum isl_dim_type type const char isl_local_space_get_dim_name __isl_keep isl_local_space ls enum isl_dim_type type unsigned pos __isl_give isl_local_space isl_local_space_set_dim_name __isl_take isl_local_space ls enum isl_dim_type type unsigned pos const char s __isl_give isl_local_space isl_local_space_set_dim_id __isl_take isl_local_space ls enum isl_dim_type type unsigned pos __isl_take isl_id id __isl_give isl_space isl_local_space_get_space __isl_keep isl_local_space ls __isl_give isl_aff isl_local_space_get_div __isl_keep isl_local_space ls int pos 16 __isl_give isl_local_space isl_local_space_copy __isl_keep isl_local_space ls void isl_local_space_free __isl_take isl_local_space ls Two local spaces can be compared using int isl_local_space_is_equal __isl_keep isl_local_space ls1 __isl_keep isl_local_space 1s2 Local spaces can be created from other local spaces using the following functions __isl_give isl_local_space isl_local_space_domain __isl_take isl_local_space ls __isl_give isl_local_space isl_local_space_range __isl_take isl_local_space ls __isl_give isl_local_space isl_local_space_from_domain __isl_take isl_local_space ls __isl_give isl_local_space isl_local_space_intersect __isl_take isl_local_space ls1 __isl_take isl_local_space 1s2 __isl_give isl_local_space isl_local_space_add_dims
47. _pw_aff_align_params __isl_take isl_pw_aff pwaff __isl_take isl_space model __isl_give isl_aff isl_aff_gist_params __isl_take isl_aff aff __isl_take isl_set context __isl_give isl_aff isl_aff_gist __isl_take isl_aff aff __isl_take isl_set context __isl_give isl_pw_aff isl_pw_aff_gist_params __isl_take isl_pw_aff pwaff __isl_take isl_set context 58 __isl_give isl_pw_aff isl_pw_aff_gist __isl_take isl_pw_aff pwaff __isl_take isl_set context __isl_give isl_set isl_pw_aff_domain __isl_take isl_pw_aff pwaff __isl_give isl_pw_aff isl_pw_aff_intersect_domain __isl_take isl_pw_aff pa __isl_take isl_set set __isl_give isl_pw_aff isl_pw_aff_intersect_params __isl_take isl_pw_aff pa __isl_take isl_set set __isl_give isl_aff isl_aff_mul __isl_take isl_aff aff1 __isl_take isl_aff af 2 __isl_give isl_pw_aff isl_pw_aff_mul __isl_take isl_pw_aff pwaff1 __isl_take isl_pw_aff pwaff2 When multiplying two affine expressions at least one of the two needs to be a constant include lt isl aff h gt __isl_give isl_basic_set isl_aff_le_basic_set __isl_take isl_aff aff1 __isl_take isl_aff aff2 __isl_give isl_basic_set isl_aff_ge_basic_set __isl_take isl_aff aff1 __isl_take isl_aff aff2 __isl_give isl_set __isl_take __isl_take __isl_give isl_set __isl_take __isl_take __isl_give isl_set __isl_take isl_pw_aff_eq_set isl_pw_af
48. _read_from_str isl_ctx ctx const char str __isl_give isl_pw_multi_aff isl_pw_multi_aff_read_from_str isl_ctx ctx const char str An expression can be printed using include lt isl aff h gt __isl_give isl_printer isl_printer_print_multi_aff __isl_take isl_printer p __isl_keep isl_multi_aff maff __isl_give isl_printer isl_printer_print_pw_multi_aff 64 __isl_take isl_printer p __isl_keep isl_pw_multi_aff pma 1 3 19 Points Points are elements of a set They can be used to construct simple sets boxes or they 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 isl_space space The coordinates of a point can be inspected set and changed using int isl_point_get_coordinate __isl_keep isl_point pnt enum isl_dim_type type int pos isl_int v __isl_give isl_point isl_point_set_coordinate __isl_take isl_point pnt enum isl_dim_type type int pos isl_int v __isl_give isl_point isl_point_add_ui __isl_take isl_point pnt enum isl_dim_type type int pos unsigned val __isl_give isl_point isl_point_sub_ui __isl_take isl_point pnt enum isl_dim_type type int pos unsigned val Other properties can be obtained using isl_ctx isl_point_get_ctx __isl_keep isl_point pnt Points can be copied or freed using __isl_give isl_point isl_point_copy __isl_keep isl_point pn
49. _schedule_maximize_band_depth isl_ctx ctx int isl_options_set_schedule_outer_zero_distance isl_ctx ctx int val int isl_options_get_schedule_outer_zero_distance isl_ctx ctx int isl_options_set_schedule_split_parallel isl_ctx ctx int val int isl_options_get_schedule_split_parallel 81 isl_ctx ctx int isl_options_set_schedule_algorithm isl_ctx ctx int val int isl_options_get_schedule_algorithm isl_ctx ctx schedule_max_constant_term This option enforces that the constant coefficients in the calculated schedule are not larger than the maximal constant term This option can significantly increase the speed of the scheduling calculation and may also prevent fusing of unrelated dimensions A value of 1 means that this option does not introduce bounds on the constant coefficients schedule_maximize_band_depth If this option is set we do not split bands at the point where we detect splitting is necessary Instead we backtrack and split bands as early as possible This reduces the number of splits and maximizes the width of the bands Wider bands give more possibilities for tiling schedule_outer_zero _distance If this option is set then we try to construct schedules where the outermost scheduling dimension in each band results in a zero dependence distance over the proximity dependences schedule_split_parallel If this option is set then we try to construct schedules in which the constant term
50. _take isl_basic_map bmap1 isl_basic_map bmap2 isl_map_apply_domain isl_map map1 isl_map map2 __isl_give isl_union_map isl_union_map_apply_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 map1 isl_map map2 __isl_give isl_union_map isl_union_map_apply_range e Cartesian Product __isl_take __isl_take __isl_give isl_set __isl_take __isl_take isl_union_map umap1 isl_union_map umap2 isl_set_product isl_set setl1 isl_set set2 47 __isl_give isl_union_set isl_union_set_product __isl_take isl_union_set uset1 __isl_take isl_union_set uset2 __isl_give isl_basic_map isl_basic_map_domain_product __isl_take isl_basic_map bmap1 __isl_take isl_basic_map bmap2 __isl_give isl_basic_map isl_basic_map_range_product __isl_take isl_basic_map bmap1 __isl_take isl_basic_map bmap2 __isl_give isl_map isl_map_domain_product __isl_take isl_map map1 __isl_take isl_map map2 __isl_give isl_map isl_map_range_product __isl_take isl_map map1 __isl_take isl_map map2 __isl_give isl_union_map isl_union_map_range_product __isl_take isl_union_map umap1 __isl_take isl_union_map umap2 __isl_give isl_map isl_map_product __isl_take isl_map map1 __isl_take isl_map map2 __isl_give isl_union_map isl_union_map_product __isl_take isl_union_map u
51. _take isl_set set __isl_take isl_multi_aff maff A piecewise multiple quasi affine expression can also be initialized from an isl_set or isl_map provided the is1l_set is a singleton and the isl map is single valued __isl_give isl_pw_multi_aff isl_pw_multi_aff_from_set __isl_take isl_set set __isl_give isl_pw_multi_aff isl_pw_multi_aff_from_map __isl_take isl_map map Multiple quasi affine expressions can be copied and freed using include lt isl aff h gt __isl_give isl_multi_aff isl_multi_aff_copy __isl_keep isl_multi_aff maff void isl_multi_aff_free __isl_take isl_multi_aff maff __isl_give isl_pw_multi_aff isl_pw_multi_aff_copy __isl_keep isl_pw_multi_aff pma void isl_pw_multi_aff_free __isl_take isl_pw_multi_aff pma The expression can be inspected using include lt isl aff h gt isl_ctx isl_multi_aff_get_ctx __isl_keep isl_multi_aff maff isl_ctx isl_pw_multi_aff_get_ctx __isl_keep isl_pw_multi_aff pma unsigned isl_multi_aff_dim __isl_keep isl_multi_aff maff enum isl_dim_type type unsigned isl_pw_multi_aff_dim __isl_keep isl_pw_multi_aff pma enum isl_dim_type type __isl_give isl_aff isl_multi_aff_get_aff __isl_keep isl_multi_aff multi int pos __isl_give isl_pw_aff isl_pw_multi_aff_get_pw_aff __isl_keep isl_pw_multi_aff pma int pos const char isl_pw_multi_aff_get_dim_name __isl_keep isl_pw_multi_aff pma enum isl_dim_type type unsigned pos __isl_
52. ach relation Rp contains all indirect paths from p to q in the input graph for r 0 n 1 do R R for p 0 n 1 do for q 0 n 1 do if p r orq r then Rpg Rpq U Rig o Rpr U R Q Ry o Rpr nA a amp UN Figure 2 3 The relation solid arrows on the right of Figure of Beletska et al 2009 and its transitive closure vertices In particular let there be n parts P in the partition We construct n relations Ry U R i s t dom R CP ran R CP apply Algorithm land return the union of all resulting Rq as the transitive closure of R Each iteration of the r loop in Algorithm 1 updates all relations Rq to include paths that go from p to r possibly stay there for 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 the result of the union in Line 6 which should be done in any case The transitive closure in Line 2 is performed using a recursive call This recursive call includes the par
53. ach 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 pwap 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 73 __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_qpolynomial_fold pwf __isl_give isl_union_pw_qpolynomial_fold isl_union_pw_qpolynomial_fold_copy __isl_keep isl_union_pw_qpolynomial_fold upwf void isl_qpolynomial_fold_free __isl_take isl_qpolynomial_fold fold void isl_pw_qpolynomial_fold_free __isl_take isl_pw_qpolynomial_fold pwf void isl_union_pw_qpolynomial_fold_free __isl_take isl_union_pw_qpolynomial_fold upwf Printing Piecewise Quasipolynomial Reductions Piecewise quasipolynomial reductions can be printed using the following function __isl_give isl_printer isl_printer_print_pw_qpolynomial_fold __isl_take isl_printer p __isl_keep isl_pw_qpolynomial_fold pwf __isl_give isl_printer isl_printer_print_union_pw_qpolynomial_fold __isl_take isl_printer p __isl_
54. affine programs For bug reports feature requests and questions visit the the discussion group at http groups google com group isI 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_qpolynomial_fold_add has been renamed to isl_pw_qpolynomial_fold_fold Similarly isl_union_pw_qpolynomial_fold_add has been renamed to isl_union_pw_qpolynomial_fold_fol Changes since isl 0 04 e All header files have been renamed from isl_header h to isl header h Changes since isl 0 05 e The functions isl_printer_print_basic_set andisl_printer_print_basic_map no longer print a newline e The functions isl1_flow_get_no_source and isl_union_map_compute_flow now return the accesses for which no source could be found instead of the itera tions where those accesses occur e The functions isl_basic_map_identity and isl_map_identity now take a map space as input An old call isl_map_identity space can be rewritten to isl_map_identity isl_space_map_from_set space e The function isl_map_power no longer takes a parameter position as input In stead the exponent is now expressed as the domain
55. ake isl_set set 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 20 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 quasipoly nomial at a given point is the value of the quasipolynomial associated to the cell that contains the point Outside of the union 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 x y
56. ake isl_union_map umap1 __isl_take isl_union_map umap2 __isl_give isl_set __isl_take __isl_take __isl_give isl_map __isl_take __isl_take __isl_give isl_set e Set difference __isl_give isl_set isl_set_subtract __isl_take __isl_take __isl_give isl_map __isl_take __isl_take __isl_give isl_map __isl_take isl_set setl isl_set set2 isl_map_subtract isl_map map1 isl_map map2 isl_map_subtract_domain isl_map map 46 __isl_take isl_set dom __isl_give isl_map isl_map_subtract_range __isl_take __isl_take isl_map map isl_set dom __isl_give isl_union_set isl_union_set_subtract __isl_take __isl_take isl_union_set uset1 isl_union_set uset2 __isl_give isl_union_map isl_union_map_subtract e Application __isl_take __isl_take isl_union_map umap1 isl_union_map umap2 __isl_give isl_basic_set isl_basic_set_apply __isl_take __isl_take __isl_give isl_set __isl_take __isl_take isl_basic_set bset isl_basic_map bmap isl_set_apply isl_set set isl_map map __isl_give isl_union_set isl_union_set_apply __isl_take __isl_take isl_union_set uset isl_union_map umap __isl_give isl_basic_map isl_basic_map_apply_domain __isl_take __isl_take isl_basic_map bmap1 isl_basic_map bmap2 __isl_give isl_basic_map isl_basic_map_apply_range __isl_take __isl_take __isl_give isl_map __isl_take __isl
57. andling isl supports different ways to react in case a runtime error is triggered Runtime errors arise e g if a function such as isl_map_intersect is called with two maps that have incompatible spaces There are three possible ways to react on error to warn to continue or to abort The default behavior is to warn In this mode isl prints a warning stores the last error in the corresponding isl_ctx and the function in which the error was triggered returns NULL An error does not corrupt internal state such that isl can continue to be used isl also provides functions to read the last error and to reset the memory that stores the last error The last error is only stored for information purposes Its presence does not change the behavior of isl Hence resetting an error is not required to continue to use isl but only to observe new errors include lt isl ctx h gt enum isl_error isl_ctx_last_error isl_ctx ctx void isl_ctx_reset_error isl_ctx ctx Another option is to continue on error This is similar to warn on error mode except that isl does not print any warning This allows a program to implement its own error reporting The last option is to directly abort the execution of the program from within the isl library This makes it obviously impossible to recover from an error but it allows to directly spot the error location By aborting on error debuggers break at the location 10 the error occurred and can provide a stack
58. basic_set_lexmin __isl_take isl_basic_set bset __isl_give isl_set isl_basic_set_lexmax __isl_take isl_basic_set bset __isl_give isl_set isl_set_lexmin __isl_take isl_set set __isl_give isl_set isl_set_lexmax __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 50 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 any 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_take __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
59. c __isl_take isl_set set __isl_take isl_qpolynomial qp __isl_give isl_pw_qpolynomial isl_pw_qpolynomial_from_qpolynomial __isl_take isl_qpolynomial qp __isl_give isl_pw_qpolynomial isl_pw_qpolynomial_from_pw_aff __isl_take isl_pw_aff pwaff __isl_give isl_union_pw_qpolynomial isl_union_pw_qpolynomial_zero __isl_take isl_space space __isl_give isl_union_pw_qpolynomial isl_union_pw_qpolynomial_from_pw_qpolynomial __isl_take isl_pw_qpolynomial pwaqp __isl_give isl_union_pw_qpolynomial isl_union_pw_qpolynomial_add_pw_qpolynomial __isl_take isl_union_pw_qpolynomial upwaqp __isl_take isl_pw_qpolynomial pwaqp Quasipolynomials can be copied and freed again using the following functions __isl_give isl_qpolynomial isl_qpolynomial_copy __isl_keep isl_qpolynomial qp void isl_qpolynomial_free __isl_take isl_qpolynomial qp 68 __isl_give isl_pw_qpolynomial isl_pw_qpolynomial_copy __isl_keep isl_pw_qpolynomial pwaqp void isl_pw_qpolynomial_free __isl_take isl_pw_qpolynomial pwaqp __isl_give isl_union_pw_qpolynomial isl_union_pw_qpolynomial_copy __isl_keep isl_union_pw_qpolynomial upwaqp void isl_union_pw_qpolynomial_free __isl_take isl_union_pw_qpolynomial upwaqp Inspecting Piecewise Quasipolynomials To iterate over all piecewise quasipolynomials in a union piecewise quasipolynomial use the following function int isl_union_pw_qpolynomial_foreach_pw_qpolynomial
60. ce model 43 Change the order of the parameters of the given set or relation such that the first parameters match those of model This may involve the introduction of extra parameters All parameters need to be named Dimension manipulation __isl_give isl_set isl_set_add_dims __isl_take isl_set set enum isl_dim_type type unsigned n __isl_give isl_map isl_map_add_dims __isl_take isl_map map enum isl_dim_type type unsigned n __isl_give isl_set isl_set_insert_dims __isl_take isl_set set enum isl_dim_type type unsigned pos unsigned n __isl_give isl_map isl_map_insert_dims __isl_take isl_map map enum isl_dim_type type unsigned pos unsigned n __isl_give isl_basic_set isl_basic_set_move_dims __isl_take isl_basic_set bset enum isl_dim_type dst_type unsigned dst_pos enum isl_dim_type src_type unsigned src_pos unsigned n __isl_give isl_basic_map isl_basic_map_move_dims __isl_take isl_basic_map bmap enum isl_dim_type dst_type unsigned dst_pos enum isl_dim_type src_type unsigned src_pos unsigned n __isl_give isl_set isl_set_move_dims __isl_take isl_set set enum isl_dim_type dst_type unsigned dst_pos enum isl_dim_type src_type unsigned src_pos unsigned n __isl_give isl_map isl_map_move_dims __isl_take isl_map map enum isl_dim_type dst_type unsigned dst_pos enum isl_dim_type src_type unsigned src_pos unsigned n It is usually not advisable to directly change the inp
61. constraint of A s The approximation of k A s can therefore be obtained using three applications of Farkas lemma The first obtains the coefficients of constraints valid for A s The second obtains the coefficients of constraints valid for the projection of A s onto the parameters The opposite of the second set is then computed and intersected with the first set The result is the set of coefficients of con straints valid for k Aj s A final application of Farkas lemma is needed to obtain the approximation of k A s itself Example 2 5 4 Consider the relation n gt x y gt 1 x l n t y n gt 2 The difference set of this relation is A n gt l1 l n n22 Using our approach we would only consider the mixed constraint y 1 n gt 0 leading to the following approximation of the transitive closure n gt x y gt 09 01 n gt 2A0 lt l n y 0o2l x If instead we apply Farkas s lemma to A i e D n gt 1 1 n n gt 2 CD coefficients D CD we obtain rat coefficients c_cst c_n gt i2 i3 i3 lt c_n and i3 lt c_cst 2c_n i2 The pure parametric constraints valid for A 100 P a b gt CP coefficients P CP are rat coefficients c_cst c_n gt c_n gt 9 and 2c_n gt c_cst Negating these coefficients and intersecting with CD NCP rat coefficients a b gt gt coefficients a b gt
62. ct for mulation of the problem The original version of PipLib required the user to manually add a big param eter perform the reformulation and interpret the result Feautrier et al 2002 Recent versions allow the user to simply specify that the unknowns may be negative or that the maximum should be computed and then these transformations are performed internally Although there are some application e g that of Feautrier 1992 where it is useful to have explicit control over the big parameter negative unknowns and maximization are by far the most common applications of the big parameter and we believe that the user should not be bothered with such implementation issues The current version of isl therefore does not provide any interface for specifying big parameters Instead the user can specify whether a maximum needs to be computed and no assumptions are made on the sign of the unknowns Instead the sign of the unknowns is checked internally and a big parameter is automatically introduced when needed For compati bility with PipLib the isl_pip tool does explicitly add non negativity constraints on the unknowns unless the Urs_unknowns option is specified Currently there is also no 89 way in isl of expressing a big parameter in the output Even though isl makes the same divisibility assumption on the big parameter as recent versions of PipLib it will therefore eventually produce an error if the problem turns out to be unbounded
63. d be more complicated as the compression would have to preserve the lexicographical order Moreover due to our handling of equalities described above there should be no need for such variable compression Although parameter compression has been implemented in isl it is currently not yet used during parametric integer programming 2 3 6 Postprocessing The output of PipLib is a quast quasi affine selection tree Each internal node in this tree corresponds to a split of the context based on a parametric constant term in the main 91 tableau with indeterminate sign Each of these nodes may introduce extra variables in the context corresponding to integer divisions Each leaf of the tree prescribes the solution in that part of the context that satisfies all the conditions on the path leading to the leaf Such a quast is a very economical way of representing the solution but it would not be suitable as the only internal representation of sets and relations in isl Instead isl represents the constraints of a set or relation in disjunctive normal form The result of a parametric integer programming problem is then also converted to this internal representation Unfortunately the conversion to disjunctive normal form can lead to an explosion of the size of the representation In some cases this overhead would have to be paid anyway in subsequent operations but in other cases especially for outside users that just want to solve parametric integer p
64. d of looking for the lexicographically minimal value of x we search instead for the lexicographically minimal value of x M x The sample value x 0 of the initial tableau then corresponds to x M which is clearly not greater than any potential solution The sign of the constant term of a row is determined lexicographically with the coefficient of M considered first That is if the coefficient of M is not zero then its sign is the sign of the entire term Otherwise the sign is determined by the remaining affine expression in the parameters If the original problem has a bounded optimum then the final sample value will be of the form M v and the optimal value of the original problem is then v Maximization problems can be handled in a similar way by computing the minimum of M x When the optimum is unbounded the optimal value computed for the original prob lem will involve the big parameter In the original implementation of PipLib the big parameter could even appear in some of the extra variables q created during the ap plication of a Gomory cut The final result could then contain implicit conditions on the big parameter through conditions on such q variables This problem was resolved in later versions of PipLib by taking M to be divisible by any positive number The big parameter can then never appear in any q because aM 0 It should be noted though that an unbounded problem usually but not always indicates an incorre
65. de 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 is _int_init i is _int_clear i isl_int_set r i is _int_set_si r i isl_int_set_gmp r g isl_int_get_gmp i g is _int_abs r i isl_int_neg r i isl_int_swap i j is _int_swap_or_set i j is _int_add_ui r i j is _int_sub_ui z i j isl_int_add r i j isl int_sub r i j isl int mul r i j is _int_mul_ui 1 i j isl int_addmul r i j is _int_submul r i j is int_gcd r i j is _int_lem 1i j is _int_divexact r i j is _int_cdiv_q 1 i j is _int_fdiv_q r i j is _int_fdiv_r r i j isl_int_fdiv_q _ui 1 i j isl int_read r s isl_int_print out i width is _int_sgn i isl_int_cmp i j is _int_cmp si i si isl_int_eq i j isl_int_ne i j isl _int_It i j is _int_le i j is _int_gt i j isl_int_ge i j is _int_abs_eq i j is _int_abs_ne i j is _int_abs_It i j is _int_abs_gt i j is _int_abs_ge i j is _int_is_zero i is _int_is_one i is _int_is_negone i is
66. dimension as a function of the parameters and input dimensions but independently of the other set or output dimensions For lexicographic optimization see 1 3 14 Dual The following functions compute either the set of rational coefficient values of valid constraints for the given set or the set of rational values satisfying the 40 constraints with coefficients from the given set Internally these two sets of func tions perform essentially the same operations except that the set of coefficients is assumed to be a cone while the set of values may be any polyhedron The current implementation is based on the Farkas lemma and Fourier Motzkin elim ination but this may change or be made optional in future In particular future implementations may use different dualization algorithms or skip the elimination step __isl_give isl_basic_set isl_basic_set_coefficients __isl_take isl_basic_set bset __isl_give isl_basic_set isl_set_coefficients __isl_take isl_set set __isl_give isl_union_set isl_union_set_coefficients __isl_take isl_union_set bset __isl_give isl_basic_set isl_basic_set_solutions __isl_take isl_basic_set bset __isl_give isl_basic_set isl_set_solutions __isl_take isl_set set __isl_give isl_union_set isl_union_set_solutions __isl_take isl_union_set bset e Power __isl_give isl_map isl_map_power __isl_take isl_map map int exact __isl_give isl_union_map isl_union_map_powe
67. e 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 C T Of course 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 R for k gt 1 and then project out the parameter k from the resulting relation Example 2 5 3 As a trivial example consider the relation R x gt x 1 The kth power of this map for arbitrary k is Reakw xoxtk k gt 1 The transitive closure is then Rt a xry akeZ y x k x gt yly gt x 1 2 5 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 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
68. e iteration domains is given by the schedule The relations returned through must _no_source and may_no_source are subsets of sink Any of must_dep 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 23 Scheduling The functionality described in this section is fairly new and may be subject to change The following function can be used to compute a schedule for a union of domains By default the algorithm used to construct the schedule is similar to that of Pluto Alternatively Feautrier s multi dimensional scheduling algorithm can be selected The generated schedule respects all validity dependences That is all dependence dis tances over these dependences in the scheduled space are lexicographically positive 79 The default algorithm tries to minimize the dependence distances over proximity dependences Moreover it tries to obtain sequences bands of schedule dimensions for groups of domains where the dependence distances have only non negative val ues When using Feautrier s algorithm the proximity dependence distances are only minimized during the extension to a full dimensional schedule include lt isl schedule h gt __isl_give isl_schedule isl_union_set_compute_schedule __isl_take isl_union_set domain __isl_take isl_union_map validity __isl_take isl_union_map proximity void isl_schedule_free __isl_take isl_schedule sched A
69. e pwaff1 is greater than or equal to pwaff2 The functions operating on isl_pw_aff_list apply the corresponding isl_pw_aff function to each pair of elements in the two lists include lt isl aff h gt __isl_give isl_set isl_pw_aff_nonneg_set __isl_take isl_pw_aff pwaff __isl_give isl_set isl_pw_aff_zero_set __isl_take isl_pw_aff pwaff __isl_give isl_set isl_pw_aff_non_zero_set __isl_take isl_pw_aff pwaff The function isl_pw_aff_nonneg_set returns a set containing those elements in the domain of pwaff where pwaff is non negative include lt isl aff h gt __isl_give isl_pw_aff isl_pw_aff_cond __isl_take isl_set cond __isl_take isl_pw_aff pwaff_true __isl_take isl_pw_aff pwaff_false The function isl_pw_aff_cond performs a conditional operator and returns an ex pression that is equal to pwaff_true for elements in cond and equal to pwaff_false for elements not in cond include lt isl aff h gt 60 __isl_give isl_pw_aff isl_pw_aff_union_min __isl_take isl_pw_aff pwaff1 __isl_take isl_pw_aff pwaff2 __isl_give isl_pw_aff isl_pw_aff_union_max __isl_take isl_pw_aff pwaff1 __isl_take isl_pw_aff pwaff2 __isl_give isl_pw_aff isl_pw_aff_union_add __isl_take isl_pw_aff pwaff1 __isl_take isl_pw_aff pwaff2 The function isl_pw_aff_union_max computes a piecewise quasi affine expres sion with a domain that is the union of those of pwaff1 and pwaff2 and such that on each cell the quasi
70. e signs while on the negative side we need to perform a pivot which may affect any number of rows meaning that the effect on the signs is difficult to predict This heuristic is of course much more expensive to evaluate than the heuristic used by PipLib More extensive tests are needed to evaluate whether the heuristic is worth while Dual Simplex Gomory Cuts When a new constraint is added to the context the first steps of the dual simplex method applied to this new context will be the same or at least very similar to those taken on the original context i e before the constraint was added In isl we therefore apply the dual simplex method incrementally on the context and backtrack to a previous state when a constraint is removed again An initial implementation that was never made public would also keep the Gomory cuts but the current implementation backtracks to before the point where Gomory cuts are added before adding an extra constraint to the context Keeping the Gomory cuts has the advantage that the sample value is always an integer point and that this point may also satisfy the new constraint However due to the technique of maintaining witnesses explained above we would not perform a feasibility test in such cases and then the previously added cuts may be redundant possibly resulting in an accumulation of a large number of cuts 93 If the parameters may be negative then the same big parameter trick used in the main tableau
71. easibility tests need to be performed depending on the result of the first test When a new constraint is added to the context the points that violate the constraint are temporarily removed They are reconsidered when we backtrack over the addition of the constraint as they will satisfy the negation of the constraint It is only when we backtrack over the addition of the points that they are finally removed completely When an extra integer division is added to the context the new coordinates of the wit nesses can easily be computed by evaluating the integer division The idea of keeping track of witnesses was first used in barvinok Choice of Constant Term on which to Split Recall that if there are no rows with a non positive constant term but there are rows with an indeterminate sign then the context needs to be split along the constant term of one of these rows If there is more than one such row then we need to choose which row to split on first PipLib uses a heuristic based on the absolute sizes of the coefficients In particular it takes the largest coefficient of each row and then selects the row where this largest coefficient is smaller than those of the other rows In isl we take that row for which non negativity of its constant term implies non negativity of as many of the constant terms of the other rows as possible The intuition behind this heuristic is that on the positive side we will have fewer negative and in determinat
72. efore also A3f gt r s Note that if there are no mixed constraints and if the rational relaxation of A s i e x Q7 Aix c gt 0 has integer vertices then the approximation 99 is exact i e Q P In this case the vertices of A s generate the rational cone x c Qt Ai c x and therefore A s is a Hilbert basis of this cone Theorem 16 4 Note however that as pointed out by De Smet 2010 if there are any mixed con straints then the above procedure may not compute the most accurate affine approx imation of k A s with k gt 1 In particular we only consider the negative mixed constraints that happen to appear in the description of A s while we should instead consider all valid such constraints It is also sufficient to consider those constraints because any constraint that is valid for k A s is also valid for 1 Aj s Aj s Take therefore any constraint a x b s c gt 0 valid for A s This constraint is also valid for k A s iff k a x b s c gt 0 If b s c can attain any positive value then a x may be negative for some elements of A s We then have k a x lt a x for k gt 1 and so the constraint is not valid for k A s We therefore need to impose b s c lt 0 for all values of s such that A s is non empty i e b and c need to be such that b s c gt 0 is a valid constraint of A s That is b c are the opposites of the coefficients of a valid
73. elta set e 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 e Detecting equalities __isl_give isl_basic_set isl_basic_set_detect_equalities __isl_take isl_basic_set bset __isl_give isl_basic_map isl_basic_map_detect_equalities __isl_take isl_basic_map bmap __isl_give isl_set isl_set_detect_equalities __isl_take isl_set set __isl_give isl_map isl_map_detect_equalities __isl_take isl_map map __isl_give isl_union_set isl_union_set_detect_equalities __isl_take isl_union_set uset __isl_give isl_union_map isl_union_map_detect_equalities __isl_take isl_union_map umap Simplify the representation of a set or relation by detecting implicit equalities 38 e Removing redundant constraints __isl_give isl_basic_set isl_basic_set_remove_redundancies __isl_take isl_basic_set bset __isl_give isl_set isl_set_remove_redundancies __isl_take isl_set set __isl_give isl_basic_map isl_basic_map_remove_redundancies __isl_take isl_basic_map bmap __isl_give isl_map isl_map_remove_redundancies __
74. esm epic ee ee 1 4 3 isl polyhedron minimize 1 4 4 isl_ polytope_scan 00004 2 Implementation Details 2 1 Sets and Relations gt ee ee ees 2 2 Simple Hulls 2 ogge Go Bead ee ede es keer ce r BRS 2 3 Parametric Integer Programming 0 2 3 1 Introduction 2 3 2 The Dual Simplex Method 2 3 3 Gomory Cuts 2 3 4 Negative Unknowns and Maximization 2 3 5 Preprocessing 2 3 6 Postprocessing 2 3 7 _ Context Tableau 2 3 8 Experiments 2 3 9 Online Symmetry Detection 2 4 Coalescing 2 5 1 Introduction 2 0 neke irek References Chapter 1 User Manual 1 1 Introduction 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 is1 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
75. f pwaffl isl_pw_aff pwaff2 isl_pw_aff_ne_set isl_pw_aff pwaffl isl_pw_aff pwaff2 isl_pw_aff_le_set isl_pw_aff pwaffl __isl_take isl_pw_aff pwaff2 __isl_give isl_set isl_pw_aff_lt_set __isl_take isl_pw_aff pwaff1 __isl_take isl_pw_aff pwaff2 __isl_give isl_set isl_pw_aff_ge_set __isl_take isl_pw_aff pwaff1 __isl_take __isl_give isl_set __isl_take __isl_take __isl_give isl_set isl_pw_aff pwaff2 isl_pw_aff_gt_set isl_pw_aff pwaffl isl_pw_aff pwaff2 isl_pw_aff_list_eq_set 59 __isl_take isl_pw_aff_list list1 __isl_take isl_pw_aff_list list2 __isl_give isl_set isl_pw_aff_list_ne_set __isl_take isl_pw_aff_list listl __isl_take isl_pw_aff_list list2 __isl_give isl_set isl_pw_aff_list_le_set __isl_take isl_pw_aff_list listl __isl_take isl_pw_aff_list list2 __isl_give isl_set isl_pw_aff_list_lt_set __isl_take isl_pw_aff_list list1 __isl_take isl_pw_aff_list list2 __isl_give isl_set isl_pw_aff_list_ge_set __isl_take isl_pw_aff_list listl __isl_take isl_pw_aff_list list2 __isl_give isl_set isl_pw_aff_list_gt_set __isl_take isl_pw_aff_list listl __isl_take isl_pw_aff_list list2 The function isl_aff_ge_basic_set returns a basic set containing those elements in the shared space of aff1 and aff2 where aff1 is greater than or equal to aff2 The function isl_aff_ge_set returns a set containing those elements in the shared domain of pwaff1 and pwaff2 wher
76. f 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 Barthou 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 1996c with the transitive closure operation only being applied to relations from a given domain to itself However it is also possible to detect disjoint domains and ranges and to apply Floyd Warshall internally 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 5 2 Otherwise we apply Floyd Warshall on the graph with as vertices the parts of the partition and as edges the R attached to the appropriate pairs of 106 Algorithm 1 The modified Floyd Warshall algorithm of Kelly et al 1996c Input Relations R 0 lt p q lt n Output Updated relations Rp such that e
77. ff pa enum isl_dim_type type unsigned pos int isl_pw_aff_has_dim_id __isl_keep isl_pw_aff pa enum isl_dim_type type unsigned pos __isl_give isl_id isl_pw_aff_get_dim_id __isl_keep isl_pw_aff pa enum isl_dim_type type unsigned pos int isl_aff_get_constant __isl_keep isl_aff aff isl_int v int isl_aff_get_coefficient __isl_keep isl_aff aff enum isl_dim_type type int pos isl_int v int isl_aff_get_denominator __isl_keep isl_aff aff isl_int v __isl_give isl_aff isl_aff_get_div __isl_keep isl_aff aff int pos int isl_pw_aff_foreach_piece __isl_keep isl_pw_aff pwaff int fn __isl_take isl_set set __isl_take isl_aff aff void user void user int isl_aff_is_cst __isl_keep isl_aff aff int isl_pw_aff_is_cst __isl_keep isl_pw_aff pwaff int isl_aff_involves_dims __isl_keep isl_aff aff enum isl_dim_type type unsigned first unsigned n int isl_pw_aff_involves_dims __isl_keep isl_pw_aff pwaff enum isl_dim_type type unsigned first unsigned n 55 isl_ctx isl_pw_aff_get_ctx __isl_keep isl_pw_aff pwaff unsigned isl_pw_aff_dim __isl_keep isl_pw_aff pwaff enum isl_dim_type type int isl_pw_aff_is_empty __isl_keep isl_pw_aff pwaff It can be modified using include lt isl aff h gt __isl_give isl_pw_aff isl_pw_aff_set_tuple_id __isl_take isl_pw_aff pwaff enum isl_dim_type type __isl_take isl_id id __isl_give isl_aff isl_aff_set_dim_name __is
78. ffl __isl_take isl_multi_aff maff2 __isl_give isl_pw_multi_aff isl_pw_multi_aff_add 63 __isl_take isl_pw_multi_aff pmal __isl_take isl_pw_multi_aff pma2 __isl_give isl_pw_multi_aff isl_pw_multi_aff_union_add __isl_take isl_pw_multi_aff pmal __isl_take isl_pw_multi_aff pma2 __isl_give isl_multi_aff isl_multi_aff_scale __isl_take isl_multi_aff maff isl_int f __isl_give isl_pw_multi_aff isl_pw_multi_aff_intersect_params __isl_take isl_pw_multi_aff pma __isl_take isl_set set __isl_give isl_pw_multi_aff isl_pw_multi_aff_intersect_domain __isl_take isl_pw_multi_aff pma __isl_take isl_set set __isl_give isl_multi_aff isl_multi_aff_lift __isl_take isl_multi_aff maff __isl_give isl_local_space ls __isl_give isl_multi_aff isl_multi_aff_gist_params __isl_take isl_multi_aff maff __isl_take isl_set context __isl_give isl_multi_aff isl_multi_aff_gist __isl_take isl_multi_aff maff __isl_take isl_set context __isl_give isl_pw_multi_aff isl_pw_multi_aff_gist_params __isl_take isl_pw_multi_aff pma __isl_take isl_set set __isl_give isl_pw_multi_aff isl_pw_multi_aff_gist __isl_take isl_pw_multi_aff pma __isl_take isl_set set If the 1s argument of isl_multi_aff_lift is not NULL then it is assigned the local space that lies at the basis of the lifting applied An expression can be read from input using include lt isl aff h gt __isl_give isl_multi_aff isl_multi_aff
79. first approximations we 97 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 collection 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 Zao ki Als y x X A X 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 Z then simplifies to P x y Aki Z y x 9 k n J 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 A s 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
80. for GMP architecture dependent files with piplib Which copy of pip1lib 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 is1_ctx is moved An isl_ctxcan be allocated using is1_ctx_alloc and freed using isl_ctx_free All objects allocated within an isl_ctx should be freed before 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 insi
81. format 83 1 4 1 isl_polyhedron_sample isl_polyhedron_sampl1le takes a polyhedron as input and prints an integer element of the polyhedron if there is any The first column in the output is the denominator and is always equal to 1 If the polyhedron 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 i 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 last 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 polyhedron minimize isl polyhedron 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_polytope_scan Given a polytope isl polytope scan prints all integer points in the polytope 84 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
82. from basic sets and relations using the following functions include lt isl constraint h gt __isl_give isl_constraint isl_equality_alloc __isl_take isl_local_space ls __isl_give isl_constraint isl_inequality_alloc __isl_take isl_local_space ls __isl_give isl_constraint isl_constraint_set_constant __isl_take isl_constraint constraint isl_int v __isl_give isl_constraint isl_constraint_set_constant_si __isl_take isl_constraint constraint int v __isl_give isl_constraint isl_constraint_set_coefficient __isl_take isl_constraint constraint enum isl_dim_type type int pos isl_int v __isl_give isl_constraint isl_constraint_set_coefficient_si __isl_take isl_constraint constraint enum isl_dim_type type int pos int v __isl_give isl_basic_map isl_basic_map_add_constraint __isl_take isl_basic_map bmap 23 __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 __isl_give isl_map isl_map_add_constraint __isl_take isl_map map __isl_take isl_constraint constraint __isl_give isl_set isl_set_add_constraint __isl_take isl_set set __isl_take isl_constraint constraint __isl_give isl_basic_set isl_basic_set_drop_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 you
83. from_constraint_matrices __isl_take isl_space space __isl_take isl_mat eq __isl_take isl_mat ineq enum isl_dim_type cl enum isl_dim_type c2 enum isl_dim_type c3 enum isl_dim_type c4 enum isl_dim_type c5 The isl_dim_type arguments indicate the order in which different kinds of vari ables appear in the input matrices and should be a permutation of isl_dim_cst isl_dim_param isl_dim_set and isl_dim_div for sets and of isl_dim_cst isl_dim_param is _dim_in isl_dim_out and isl_dim_div for relations A basic set or relation can also be constructed from a piecewise multiple affine expression or a list of affine expressions See 1 3 17 and 1 3 18 __isl_give isl_basic_map isl_basic_map_from_aff __isl_take isl_aff aff __isl_give isl_set isl_set_from_pw_aff __isl_take isl_pw_aff pwaff __isl_give isl_map isl_map_from_pw_aff __isl_take isl_pw_aff pwaff __isl_give isl_basic_map isl_basic_map_from_aff_list __isl_take isl_space domain_space __isl_take isl_aff_list list __isl_give isl_basic_map isl_basic_map_from_multi_aff __isl_take isl_multi_aff maff __isl_give isl_set isl_set_from_pw_multi_aff __isl_take isl_pw_multi_aff pma __isl_give isl_map isl_map_from_pw_multi_aff __isl_take isl_pw_multi_aff pma The domain_dim argument describes the domain of the resulting basic relation It is required because the list may consist of zero affine expressions 1 3 11 Inspecting Sets and Relat
84. ge Wrapping __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 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_basic_set isl_basic_set_flatten __isl_take isl_basic_set bset __isl_give isl_set isl_set_flatten __isl_take isl_set set __isl_give isl_basic_map isl_basic_map_flatten_domain __isl_take isl_basic_map bmap __isl_give isl_basic_map isl_basic_map_flatten_range __isl_take isl_basic_map bmap __isl_give isl_map isl_map_flatten_range __isl_take isl_map map __isl_give isl_map isl_map_flatten_domain __isl_take isl_map map __isl_give isl_basic_map isl_basic_map_flatten __isl_take isl_basic_map bmap __isl_give isl_map isl_map_flatten __isl_take isl_map map 42 __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
85. give isl_basic_set isl_set_polyhedral_hul1 __isl_take isl_set set __isl_give isl_basic_map isl_map_polyhedral_hul1l __isl_take isl_map map __isl_give isl_union_set isl_union_set_polyhedral_hul1 __isl_take isl_union_set uset __isl_give isl_union_map isl_union_map_polyhedral_hul1 __isl_take isl_union_map umap These functions compute a single basic set or relation not involving any existen tially quantified variables that contains the whole input set or relation In case of union sets and relations the polyhedral hull is computed per space Optimization include lt isl ilp h gt enum isl_lp_result isl_basic_set_max __isl_keep isl_basic_set bset __isl_keep isl_aff obj isl_int opt enum isl_lp_result isl_set_min __isl_keep isl_set set __isl_keep isl_aff obj isl_int opt enum isl_lp_result isl_set_max __isl_keep isl_set set __isl_keep isl_aff obj isl_int opt Compute the minimum or maximum of the integer affine expression obj over the points in set returning the result in opt The return value may be one of isl_lp_error isl_lp_ok isl_lp_unbounded or isl_lp_empty Parametric optimization __isl_give isl_pw_aff isl_set_dim_min __isl_take isl_set set int pos __isl_give isl_pw_aff isl_set_dim_max __isl_take isl_set set int pos __isl_give isl_pw_aff isl_map_dim_max __isl_take isl_map map int pos Compute the minimum or maximum of the given set or output
86. give isl_id isl_pw_multi_aff_get_dim_id 62 __isl_keep isl_pw_multi_aff pma enum isl_dim_type type unsigned pos const char isl_multi_aff_get_tuple_name __isl_keep isl_multi_aff multi enum isl_dim_type type const char isl_pw_multi_aff_get_tuple_name __isl_keep isl_pw_multi_aff pma enum isl_dim_type type int isl_pw_multi_aff_has_tuple_id __isl_keep isl_pw_multi_aff pma enum isl_dim_type type __isl_give isl_id isl_pw_multi_aff_get_tuple_id __isl_keep isl_pw_multi_aff pma enum isl_dim_type type int isl_pw_multi_aff_foreach_piece __isl_keep isl_pw_multi_aff pma int fn __isl_take isl_set set __isl_take isl_multi_aff maff void user void user It can be modified using include lt isl aff h gt __isl_give isl_multi_aff isl_multi_aff_set_dim_name __isl_take isl_multi_aff maff enum isl_dim_type type unsigned pos const char s __isl_give isl_pw_multi_aff isl_pw_multi_aff_set_tuple_id __isl_take isl_pw_multi_aff pma enum isl_dim_type type __isl_take isl_id id To check whether two multiple affine expressions are obviously equal to each other use int isl_multi_aff_plain_is_equal __isl_keep isl_multi_aff maff1 __isl_keep isl_multi_aff maff2 int isl_pw_multi_aff_plain_is_equal __isl_keep isl_pw_multi_aff pmal __isl_keep isl_pw_multi_aff pma2 Operations include include lt isl aff h gt __isl_give isl_multi_aff isl_multi_aff_add __isl_take isl_multi_aff ma
87. gned n __isl_give isl_aff isl_aff_add_dims __isl_take isl_aff aff enum isl_dim_type type unsigned n __isl_give isl_pw_aff isl_pw_aff_add_dims __isl_take isl_pw_aff pwaff enum isl_dim_type type unsigned n __isl_give isl_aff isl_aff_drop_dims __isl_take isl_aff aff enum isl_dim_type type unsigned first unsigned n __isl_give isl_pw_aff isl_pw_aff_drop_dims __isl_take isl_pw_aff pwaff enum isl_dim_type type unsigned first unsigned n Note that the set_constant and set_coefficient functions set the numerator of the constant or coefficient while add_constant and add_coefficient add an integer value to the possibly rational constant or coefficient To check whether an affine expressions is obviously zero or obviously equal to some other affine expression use include lt isl aff h gt int isl_aff_plain_is_zero __isl_keep isl_aff aff int isl_aff_plain_is_equal __isl_keep isl_aff aff1 __isl_keep isl_aff aff2 int isl_pw_aff_plain_is_equal __isl_keep isl_pw_aff pwaff1 __isl_keep isl_pw_aff pwaff2 Operations include include lt isl aff h gt __isl_give isl_aff isl_aff_add __isl_take isl_aff aff1 __isl_take isl_aff af 2 __isl_give isl_pw_aff isl_pw_aff_add __isl_take isl_pw_aff pwaff1 __isl_take isl_pw_aff pwaff2 __isl_give isl_pw_aff isl_pw_aff_min __isl_take isl_pw_aff pwaff1 __isl_take isl_pw_aff pwaff2 __isl_give isl_pw_aff isl_pw_aff_max __isl_take isl_
88. hat happens when we do not perform offline symmetry de tection At some point one of the b p a x gt 0 constraints say the jth constraint appears as a column variable say c while the other constraints are represented as rows of the form b p bj p c The context is then split according to the relative order of b p and one of the remaining b p The offline method avoids this split by re placing all b p by a single newly introduced parameter that represents the minimum of these b p In the online method the split is similarly avoided by the introduc tion of a new parameter In particular a new parameter is introduced that represents b p bi p max b p bip 0 In general let r b p a c be a row of the tableau such that the sign of b p is indeterminate and such that exactly one of the elements of a is a 1 while all remaining elements are non positive That is r b p cj f with f Diz aici 2 0 We introduce a new parameter t with context constraints t gt b p and t gt 0 and replace the column variable cj by c t The row r is now equal to b p t c f The constant term of this row is always non negative because any negative value of b p is compensated by t gt b p while and non negative value remains non negative because t gt 0 We need to show that this transformation does not eliminate any valid solutions and that it does not introduce any spurious solutions Given
89. igned first unsigned n __isl_give isl_space isl_space_move_dims __isl_take isl_space space enum isl_dim_type dst_type unsigned dst_pos enum isl_dim_type src_type unsigned src_pos unsigned n __isl_give isl_space isl_space_map_from_set __isl_take isl_space space __isl_give isl_space isl_space_map_from_domain_and_range __isl_take isl_space domain 15 __isl_take isl_space range __isl_give isl_space isl_space_zip __isl_take isl_space space Note that if dimensions are added or removed from a space then the name and the internal structure are lost 1 3 8 Local Spaces A local space is essentially a space with zero or more existentially quantified variables The local space of a basic set or relation can be obtained using the following functions include lt isl set h gt __isl_give isl_local_space isl_basic_set_get_local_space __isl_keep isl_basic_set bset include lt isl map h gt __isl_give isl_local_space isl_basic_map_get_local_space __isl_keep isl_basic_map bmap A new local space can be created from a space using include lt isl local_space h gt __isl_give isl_local_space isl_local_space_from_space __isl_take isl_space space They can be inspected modified copied and freed using the following functions include lt isl local_space h gt isl_ctx isl_local_space_get_ctx __isl_keep isl_local_space ls int isl_local_space_is_set __isl_keep isl_local_space ls int isl
90. ing the number of rows and columns where the number of rows is 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 constraint 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 __isl_give isl_basic_set isl_basic_set_read_from_str isl_ctx ctx const char str __isl_give isl_set isl_set_read_from_file isl_ctx ctx
91. input piecewise quasipolynomial The context is also exploited to simplify the quasipolynomials associated to each cell __isl_give isl_pw_qpolynomial isl_pw_qpolynomial_to_polynomial __isl_take isl_pw_qpolynomial pwqp int sign __isl_give isl_union_pw_qpolynomial isl_union_pw_qpolynomial_to_polynomial __isl_take isl_union_pw_qpolynomial upwqp int sign Approximate each quasipolynomial by a polynomial If sign is positive the poly 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 21 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_qpolynomial pwqp enum isl_fold type int tight __isl_give isl_union_pw_qpolynomial_fold isl_union_pw_qpolynomial_bound __isl_take isl_union_pw_qpolynomial upwaqp enum isl_fold type int tight The type argument may be either isl_fold_min or isl_fold_max If tight is not NULL then tight is set to 1 is the returned bound is known be tight i e for e
92. ions 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 25 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 existentially 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 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 appear 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_
93. ipLib converts each into a pair of inequalities It is also possible to write r equalities as r 1 inequalities Feautrier et al 2002 but it is even better to exploit the equalities to reduce the di mensionality of the problem Given an equality involving at least one unknown we pivot the row corresponding to the equality with the column corresponding to the last unknown with non zero coefficient The new column variable can then be removed completely because it is identically zero thereby reducing the dimensionality of the problem by one The last unknown is chosen to ensure that the columns of the initial tableau remain lexicographically positive In particular if the equality is of the form b Nici i xi 0 with a 0 then the implicit top rows of the initial tableau are 90 changed as follows j 0h 0 l j 0 1 gt j b aj ai aj 0 h 0 h Currently isl also eliminates equalities involving only parameters in a similar way provided at least one of the coefficients is equal to one The application of parameter compression see below would obviate the need for removing parametric equalities Offline Symmetry Detection Some problems notably those of Bygde 2010 have a collection of constraints say bi p a x gt 0 that only differ in their parametric constant terms These constant terms will be non negative on different parts of the context and this context may have to be split for each of the constraints In the
94. is applied to the context This big parameter is of course unrelated to the big parameter from the main tableau Note that it is not a requirement for this parameter to be big but it does allow for some code reuse in isl In PipLib the extra parameter is not big but this may be because the big parameter of the main tableau also appears in the context tableau Finally it was reported by Galea 2009 who worked on a parametric integer pro gramming implementation in Se a that it is beneficial to add cuts for all rational coordinates in the context tableau Based on this report the initial isl implementation was adapted accordingly Generalized Basis Reduction The default algorithm used in isl for feasibility checking is generalized basis reduc tion Cook et al 1991 This algorithm is also used in the barvinok implementation The algorithm is fairly robust but it has some overhead We therefore try to avoid call ing the algorithm in easy cases In particular we incrementally keep track of points for which the entire unit hypercube positioned at that point lies in the context This set is described by translates of the constraints of the context and if rationally non empty any rational point in the set can be rounded up to yield an integer point in the context A restriction of the algorithm is that it only works on bounded sets The affine hull of the recession cone therefore needs to be projected out first As soon as the algo
95. 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 PS U Id o P UId NA x gt y yari xari k gt O 2 6 with P s xX gt y Ik Zz E kAi s y x 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 yg4 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 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 98 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 invo
96. 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 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 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 5 7 Consider the relation in example closure4 that comes with the Omega calculator Kelly et al 1996a R R U Ro with R x y gt x y 1 1 lt x y lt 10 R x y gt x Ly 1 lt x lt 2045 lt y lt 15 104 Figure 2 1 The relation from Example 2 5 7 This relation is shown graphically in Figure 2 1 We have R o R x y gt xt lyt tD 1 lt x lt 9A5 lt y lt 10 R0 Ri x y gt 4 1ly D 1 lt x lt 10A4 lt y lt 10 Clearly Ri o Ra C Rp o R and so R U R2 Rj o RF UR U R3 E
97. is split off from the linear part if the linear parts of the scheduling rows for all nodes in the graphs are the same The constant term is then placed in a separate band and the linear part is simplified schedule_algorithm Selects the scheduling algorithm to be used Available scheduling algorithms are ISL_SCHEDULE_ALGORITHM_ISL and ISL_SCHEDULE_ALGORITHM_FEAUTRIER 1 3 24 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_vertices 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 82 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 fn __isl_take isl_vertex vertex void user void user Other operations that
98. 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_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_map 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 analysis 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 identify 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 supplied tokens identifyi
99. isl_give isl_space isl_space_unwrap __isl_take isl_space space The input to is1_space_is_wrapping and isl_space_unwrap should be the space of a set while that of isl_space_wrap should be the space of a relation Con versely the output of isl_space_unwrap is the space of a relation while that of isl_space_wrap is the space of a set Spaces can be created from other spaces using the following functions __isl_give isl_space isl_space_domain __isl_take isl_space space __isl_give isl_space isl_space_from_domain __isl_take isl_space space __isl_give isl_space isl_space_range __isl_take isl_space space __isl_give isl_space isl_space_from_range __isl_take isl_space space __isl_give isl_space isl_space_params __isl_take isl_space space __isl_give isl_space isl_space_set_from_params __isl_take isl_space space __isl_give isl_space isl_space_reverse __isl_take isl_space space __isl_give isl_space isl_space_join __isl_take isl_space left __isl_take isl_space right __isl_give isl_space isl_space_align_params __isl_take isl_space spacel __isl_take isl_space space2 __isl_give isl_space isl_space_insert_dims __isl_take isl_space space enum isl_dim_type type unsigned pos unsigned n __isl_give isl_space isl_space_add_dims __isl_take isl_space space enum isl_dim_type type unsigned n __isl_give isl_space isl_space_drop_dims __isl_take isl_space space enum isl_dim_type type uns
100. isl_take isl_basic_map bmap __isl_take isl_basic_set bset __isl_give isl_basic_map isl_basic_map_intersect __isl_take __isl_take __isl_give isl_map __isl_take __isl_take __isl_give isl_map __isl_take __isl_take __isl_give isl_map isl_basic_map bmap1 isl_basic_map bmap2 isl_map_intersect_params isl_map map isl_set params isl_map_intersect_domain isl_map map isl_set set isl_map_intersect_range 45 __isl_take isl_map map __isl_take isl_set set __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 umap __isl_take isl_union_set uset __isl_give isl_union_map isl_union_map_intersect __isl_take isl_union_map umap1 __isl_take isl_union_map umap2 e Union isl_basic_set_union isl_basic_set bsetl isl_basic_set bset2 isl_basic_map_union isl_basic_map bmap1 isl_basic_map bmap2 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 uset1 __isl_take isl_union_set uset2 __isl_give isl_union_map isl_union_map_union __isl_t
101. isl_take isl_map map e Convex hull __isl_give isl_basic_set isl_set_convex_hul1 __isl_take isl_set set __isl_give isl_basic_map isl_map_convex_hul11 __isl_take isl_map map If the input set or relation has any existentially quantified variables then the result of these operations is currently undefined e Simple hull __isl_give isl_basic_set isl_set_simple_hul1 __isl_take isl_set set __isl_give isl_basic_map isl_map_simple_hul11 __isl_take isl_map map __isl_give isl_union_map isl_union_map_simple_hul1 __isl_take isl_union_map umap 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 e Affine hull __isl_give isl_basic_set isl_basic_set_affine_hull __isl_take isl_basic_set bset __isl_give isl_basic_set isl_set_affine_hull __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_hul1l __isl_take isl_basic_map bmap __isl_give isl_basic_map isl_map_affine_hull1l __isl_take isl_map map __isl_give isl_union_map isl_union_map_affine_hul1 __isl_take isl_union_map umap 39 In case of union sets and relations the affine hull is computed per space Polyhedral hull __isl_
102. ities 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 isl_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 simply 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_
103. ive isl_set isl_set_fix __isl_take isl_set set enum isl_dim_type type unsigned pos isl_int value __isl_give isl_set isl_set_fix_si __isl_take isl_set set enum isl_dim_type type unsigned pos int value __isl_give isl_basic_map isl_basic_map_fix_si __isl_take isl_basic_map bmap enum isl_dim_type type unsigned pos int value __isl_give isl_map isl_map_fix_si __isl_take isl_map map enum isl_dim_type type unsigned pos int value Intersect the set or relation with the hyperplane where the given dimension has the fixed given value 36 __isl_give isl_basic_map isl_basic_map_lower_bound_si __isl_take isl_basic_map bmap enum isl_dim_type type unsigned pos __isl_give isl_set isl_set_lower_bound_si __isl_take isl_set set enum isl_dim_type type unsigned pos __isl_give isl_map isl_map_lower_bound_si __isl_take isl_map map enum isl_dim_type type unsigned pos __isl_give isl_set isl_set_upper_bound_si __isl_take isl_set set enum isl_dim_type type unsigned pos __isl_give isl_map isl_map_upper_bound_si __isl_take isl_map map enum isl_dim_type type unsigned pos int int int int int value value value value value Intersect the set or relation with the half space where the given dimension has a value bounded the fixed given value __isl_give isl_set isl_set_equate __isl_take isl_set set enum isl_dim_type typel int posl enum isl_dim_type type
104. ke 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_type type unsigned first unsigned n __isl_give isl_basic_map isl_basic_map_project_out __isl_take isl_basic_map bmap enum isl_dim_type type unsigned first unsigned n __isl_give isl_set isl_set_project_out __isl_take isl_set set enum isl_dim_type type unsigned first unsigned n __isl_give isl_map isl_map_project_out __isl_take isl_map map enum isl_dim_type type unsigned first unsigned n __isl_give isl_basic_set isl_basic_set_params __isl_take isl_basic_set bset __isl_give isl_basic_set isl_basic_map_domain __isl_take isl_basic_map bmap __isl_give isl_basic_set isl_basic_map_range __isl_take isl_basic_map bmap __isl_give isl_set isl_set_params __isl_take isl_set set __isl_give isl_set isl_map_params __isl_take isl_map map __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_set isl_union_set_params __isl_take isl_union_set uset __isl_give isl_set isl_union_map_params __isl_take isl_union_map umap __isl_give isl_union_set isl_union_map_domain __isl_take isl_union_map umap __isl_give isl_union_set i
105. ke isl_space space unsigned n __isl_give isl_map isl_map_lex_gt_first __isl_take isl_space space unsigned n __isl_give isl_map isl_map_lex_ge_first __isl_take isl_space space unsigned n The first four functions take a space for a set and return relations that express that the elements in the domain are lexicographically less isl_map_lex_1t 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 space for a map and return relations that express that the first n dimensions in the domain are lexicographically less isl1_map_lex_1t_first less or equal isl_map_lex_le_first greater isl_map_lex_gt_first or greater or equal isl_map_lex_ge_first than the first n dimensions in the range 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_map __isl_take isl_map map __isl_give isl_union_set isl_union_set_from_set __isl_take isl_set set The inverse conversions below can only be used if the input union set or relation is known to contain elements in exactly one space __isl_gi
106. keep isl_union_pw_qpolynomial_fold upwf For isl_printer_print_pw_qpolynomial_fold output format of the printer needs to be set to either ISL_FORMAT_ISL or ISL_FORMAT_C Forisl_printer print union pw_qpolynomial 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_qpolynomial_fold_set_dim_name __isl_take isl_pw_qpolynomial_fold pwf enum isl_dim_type type unsigned pos const char s 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 74 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_qpolynomial_fold fold void user void user See Inspecting Piecewise Quasipoly
107. l_basic_set set const char s 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_type type __isl_give isl_basic_map isl_basic_map_set_tuple_name __isl_take isl_basic_map bmap enum isl_dim_type type const char s const char isl_map_get_tuple_name __isl_keep isl_map map enum isl_dim_type type As with isl_space_get_tuple_name the value returned points to an internal data structure The identifiers positions or names of individual dimensions can be read off using the following functions __isl_give isl_set isl_set_set_dim_id __isl_take isl_set set enum isl_dim_type type unsigned pos __isl_take isl_id id int isl_set_has_dim_id __isl_keep isl_set set enum isl_dim_type type unsigned pos __isl_give isl_id isl_set_get_dim_id __isl_keep isl_set set enum isl_dim_type type unsigned pos int isl_basic_map_has_dim_id __isl_keep isl_basic_map bmap enum isl_dim_type type unsigned pos __isl_give isl_map isl_map_set_dim_id __isl_take isl_map map enum isl_dim_type type unsigned pos __isl_take isl_id id int isl_map_has_dim_id __isl_keep isl_map map enum isl_dim_type type unsigned pos 30 __isl_give isl_id isl_map_get_dim_id __isl_keep isl_map map enum isl_dim_type type unsigned pos int isl_set_find_dim_by_id __isl_keep isl_set set enum isl_dim_type type __isl_keep isl_id id
108. l_lexmin_pw_multi_aff __isl_take isl_basic_map bmap __isl_take isl_basic_set dom __isl_give isl_set empty __isl_give isl_pw_multi_aff isl_basic_map_partial_lexmax_pw_multi_aff __isl_take isl_basic_map bmap __isl_take isl_basic_set dom __isl_give isl_set empty 1 3 15 Lists Lists are defined over several element types including isl_aff isl_pw_aff isl_basic_set and isl_set Here we take lists of isl_sets as an example Lists can be created copied and freed using the following functions include lt isl list h gt __isl_give isl_set_list isl_set_list_from_set __isl_take isl_set el __isl_give isl_set_list isl_set_list_alloc isl_ctx ctx int n __isl_give isl_set_list isl_set_list_copy __isl_keep isl_set_list list __isl_give isl_set_list isl_set_list_add __isl_take isl_set_list list __isl_take isl_set el __isl_give isl_set_list isl_set_list_concat __isl_take isl_set_list listl1 __isl_take isl_set_list list2 void isl_set_list_free __isl_take isl_set_list list isl_set_list_alloc creates an empty list with a capacity forn elements isl_set_list_from_set creates a list with a single element Lists can be inspected using the following functions include lt isl list h gt 52 isl_ctx isl_set_list_get_ctx __isl_keep isl_set_list list int isl_set_list_n_set __isl_keep isl_set_list list __isl_give isl_set isl_set_list_get_set __isl_keep isl_set_list list int i
109. l_take isl_aff aff enum isl_dim_type type unsigned pos const char s __isl_give isl_aff isl_aff_set_dim_id __isl_take isl_aff aff enum isl_dim_type type unsigned pos __isl_take isl_id id __isl_give isl_pw_aff isl_pw_aff_set_dim_id __isl_take isl_pw_aff pma enum isl_dim_type type unsigned pos __isl_take isl_id id __isl_give isl_aff isl_aff_set_constant __isl_take isl_aff aff isl_int v __isl_give isl_aff isl_aff_set_constant_si __isl_take isl_aff aff int v __isl_give isl_aff isl_aff_set_coefficient __isl_take isl_aff aff enum isl_dim_type type int pos isl_int v __isl_give isl_aff isl_aff_set_coefficient_si __isl_take isl_aff aff enum isl_dim_type type int pos int v __isl_give isl_aff isl_aff_set_denominator __isl_take isl_aff aff isl_int v __isl_give isl_aff isl_aff_add_constant __isl_take isl_aff aff isl_int v __isl_give isl_aff isl_aff_add_constant_si __isl_take isl_aff aff int v __isl_give isl_aff isl_aff_add_coefficient __isl_take isl_aff aff enum isl_dim_type type int pos isl_int v __isl_give isl_aff isl_aff_add_coefficient_si __isl_take isl_aff aff enum isl_dim_type type int pos int v __isl_give isl_aff isl_aff_insert_dims __isl_take isl_aff aff 56 enum isl_dim_type type unsigned first unsigned n __isl_give isl_pw_aff isl_pw_aff_insert_dims __isl_take isl_pw_aff pwaff enum isl_dim_type type unsigned first unsi
110. lated 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 5 6 In this case C R D can be obtained by allowing the value zero for k in 2 16 i e by computing i gt j da k k gt OAKL lt j i lt kUA Vp jp ip Mp p In our implementation we take as D the simple hull Section 2 2 of domR U ran R To determine whether it is safe to use C R D we check the following conditions as proposed by Kelly et al 1996c C R D R is not a union and for each j i the condition C R D R7 Rj o C R D Rv Rj holds 110 Bibliography Bagnara R P M Hill and E Zaffanella The Parma Polyhedra Library www cS unipr it ppl 94 Barthou D A Cohen and J F Collard 2000 Maximal static expansion Int J Parallel Program 28 3 213 243 106 Barvinok A and K Woods 2003 April Short rational generating functions for lattice point problems J Amer Math Soc 16 957 979 87 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
111. lt n 66 Input and Output Piecewise quasipolynomials can be read from input using __isl_give isl_union_pw_qpolynomial isl_union_pw_qpolynomial_read_from_str isl_ctx ctx const char str Quasipolynomials and piecewise quasipolynomials can be printed using the follow ing functions __isl_give isl_printer isl_printer_print_qpolynomial __isl_take isl_printer p __isl_keep isl_qpolynomial qp __isl_give isl_printer isl_printer_print_pw_qpolynomial __isl_take isl_printer p __isl_keep isl_pw_qpolynomial pwaqp __isl_give isl_printer isl_printer_print_union_pw_qpolynomial __isl_take isl_printer p __isl_keep isl_union_pw_qpolynomial upwqp The output format of the printer needs to be set to either ISL_FORMAT_ISL or ISL_FORMAT_C For isl_printer_print_union_pw_qpolynomial only ISL_FORMAT_ISL is supported In case of printing in ISL_FORMAT_C the user may want to set the names of all dimensions __isl_give isl_qpolynomial isl_qpolynomial_set_dim_name __isl_take isl_qpolynomial qp enum isl_dim_type type unsigned pos const char s __isl_give isl_pw_qpolynomial isl_pw_qpolynomial_set_dim_name __isl_take isl_pw_qpolynomial pwqp enum isl_dim_type type 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
112. lves 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 c 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 each row j and for all s Ai s N 8 B38 c3 gt 0 0 4 positive mixed constraints A4x Bas c4 gt 0 such that for each row j there is at least one s such that A s N amp B4 js c4 gt 0 0 We will use the following approximation Q for P s xX gt y Ik Z f eZl y x k gt y 2 10 Af kci gt 0 A Bas gt OA A3f B38 c3 gt 0 To prove that Q is indeed an overapproximation of P we need to show that for every s Z for every k Zs and for every f kA 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 kAj s is a sum of k elements f 1 in Aj s Each of these elements satisfies the constraints in 2 7 i e Ai c r gt 0 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 ther
113. m Ver doolaege et al 2005 and were used to drive the first Gomory cuts based implemen tation in isl The third and final group of test cases are borrowed from Bygde 2010 and inspired the offline symmetry detection of Section 2 3 5 Without symmetry de tection the running times are 11s and 5 9s All running times of barvinok and isl include a conversion to disjunctive normal form Without this conversion the final two cases can be solved in 0 07s and 0 21s The PipLib implementation has some fixed limits and will sometimes report the problem to be too complex TC while on some other problems it will run out of memory OOM The barvinok implementation does not support problems with a non trivial lineality space line nor maximization prob lems max The Gomory cuts based isl implementation was terminated after 1000 minutes on the first problem The gbr version introduces some overhead on some of the easier problems but is overall the clear winner 2 3 9 Online Symmetry Detection Manual experiments on small instances of the problems of Bygde 2010 and an anal ysis of the results by the approximate MPA method developed by Bygde 2010 have 95 revealed that these problems contain many more symmetries than can be detected us ing the offline method of In this section we present an online detection mechanism that has not been implemented yet but that has shown promising results in manual applications Let us first consider w
114. map map Alternatively the existentially 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 __isl_give isl_map isl_map_remove_divs __isl_take isl_map map 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 26 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 in a given space from a union use __isl_give isl_set isl_union_set_extract_set __isl_keep isl_union_set uset __isl_take isl_space space __isl_give isl_map isl_union_map_extract_map __isl_keep isl_union_map umap __isl_take isl_space space To 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
115. map map1 __isl_keep isl_map map2 int isl_map_plain_is_equal __isl_keep isl_map map1 __isl_keep isl_map map2 int isl_union_map_is_equal __isl_keep isl_union_map umap1 __isl_keep isl_union_map umap2 33 e Disjointness int isl_set_plain_is_disjoint __isl_keep isl_set setl __isl_keep isl_set set2 e Subset int isl_set_is_subset __isl_keep isl_set setl __isl_keep isl_set set2 int isl_set_is_strict_subset __isl_keep isl_set set1 __isl_keep isl_set set2 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_strict_subset __isl_keep isl_basic_map bmap1 __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 umap1 __isl_keep isl_union_map umap2 int isl_union_map_is_strict_subset __isl_keep isl_union_map umap1 __isl_keep isl_union_map umap2 1 3 13 Unary Operations e Complement __isl_give isl_set isl_set_complement __isl_take isl_set set e Inverse map 34 __isl_give isl_basic_map isl_basic_map_reverse __isl_ta
116. map1 __isl_take isl_union_map umap2 The above functions compute the cross product of the given sets or relations The domains and ranges of the results are wrapped maps between domains and ranges of the inputs To obtain a flat product use the following functions instead __isl_give isl_basic_set isl_basic_set_flat_product __isl_take isl_basic_set bset1 __isl_take isl_basic_set bset2 __isl_give isl_set isl_set_flat_product __isl_take isl_set setl __isl_take isl_set set2 __isl_give isl_basic_map isl_basic_map_flat_range_product __isl_take isl_basic_map bmap1 __isl_take isl_basic_map bmap2 __isl_give isl_map isl_map_flat_domain_product __isl_take isl_map map1 __isl_take isl_map map2 __isl_give isl_map isl_map_flat_range_product __isl_take isl_map map1 __isl_take isl_map map2 __isl_give isl_union_map isl_union_map_flat_range_product __isl_take isl_union_map umap1 48 __isl_take isl_union_map umap2 __isl_give isl_basic_map isl_basic_map_flat_product __isl_take __isl_take __isl_give isl_map e Simplification __isl_take __isl_take isl_basic_map bmap1 isl_basic_map bmap2 isl_map_flat_product isl_map map1 isl_map map2 __isl_give isl_basic_set isl_basic_set_gist __isl_take __isl_take __isl_give isl_set __isl_take __isl_give isl_set __isl_take __isl_take isl_basic_set bset isl_basic_set context isl_set_gist __isl_take
117. mple value that may be invalid but that is known to be lexicographically no greater than any solution and gradually increments this sample value through pivoting until a valid solution is obtained In particular each pivot exchanges a row variable r n gt a c with negative sample 87 value n with a column variable c such that a gt 0 Since cj n r Dizi Gj Ci aj the new row variable will have a positive sample value n If no such column can be found then the problem is infeasible By always choosing the column that leads to the lexicographically smallest increment in the variables x the first solution found is guaranteed to be the lexicographically minimal solution Feautrier 1988 In order to be able to determine the smallest increment the tableau is implicitly extended with extra rows defining the original variables in terms of the column variables If we assume that all variables are non negative then we know that the zero vector is no greater than the minimal solution and then the initial extended tableau looks as follows le x 07 r baA Each column in this extended tableau is lexicographically positive and will remain so because of the column choice explained above It is then clear that the value of x will increase in each step Note that there is no need to store the extra rows explicitly If a given x is a column variable then the corresponding row is the unit vector e If on the other hand it
118. mpute approximations of transitive closures of R and R sepa rately Note however that the condition R o R2 is actually too strong If R o R2 is a subset of R2 o R then we can reorder the segments in any path that moves through both R and R to first move through R and then through R2 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 R iff The components can be obtained from the graph by applying Tarjan s algorithm 1972 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 separately If the approximation turns out to be inexact for any of the components then the entire result is marked inexact and the exactness check
119. n a quasipolynomial use int isl_qpolynomial_foreach_term __isl_keep isl_qpolynomial qp int fn __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_type type 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 __isl_keep isl_term term enum isl_dim_type type unsigned pos __isl_give isl_aff 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 To check whether two union piecewise quasipolynomials are obviously equal use int isl_union_pw_qpolynomial_plain_is_equal __isl_keep
120. n_pw_qpolynomial_intersect_params __isl_take isl_union_pw_qpolynomial upwpq __isl_take isl_set set __isl_give isl_qpolynomial isl_qpolynomial_align_params __isl_take isl_qpolynomial qp __isl_take isl_space model __isl_give isl_qpolynomial isl_qpolynomial_project_domain_on_params __isl_take isl_qpolynomial qp __isl_give isl_pw_qpolynomial isl_pw_qpolynomial_project_domain_on_params __isl_take isl_pw_qpolynomial pwaqp __isl_give isl_union_pw_qpolynomial isl_union_pw_qpolynomial_coalesce __isl_take isl_union_pw_qpolynomial upwaqp __isl_give isl_qpolynomial isl_qpolynomial_gist_params __isl_take isl_qpolynomial qp __isl_take isl_set context __isl_give isl_qpolynomial isl_qpolynomial_gist __isl_take isl_qpolynomial qp __isl_take isl_set context __isl_give isl_pw_qpolynomial isl_pw_qpolynomial_gist_params __isl_take isl_pw_qpolynomial pwqp __isl_take isl_set context __isl_give isl_pw_qpolynomial isl_pw_qpolynomial_gist __isl_take isl_pw_qpolynomial pwqp __isl_take isl_set context __isl_give isl_union_pw_qpolynomial isl_union_pw_qpolynomial_gist_params 72 __isl_take isl_union_pw_qpolynomial upwaqp __isl_take isl_set context __isl_give isl_union_pw_qpolynomial isl_union_pw_qpolynomial_gist __isl_take isl_union_pw_qpolynomial upwaqp __isl_take isl_union_set context The gist operation applies the gist operation to each of the cells in the domain of the
121. ndex int isl_set_list_foreach __isl_keep isl_set_list list int fn __isl_take isl_set el void user void user Lists can be printed using include lt isl list h gt __isl_give isl_printer isl_printer_print_set_list __isl_take isl_printer p __isl_keep isl_set_list list 1 3 16 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 isl_ctx ctx unsigned n_row unsigned n_col __isl_give isl_mat isl_mat_copy __isl_keep isl_mat mat void isl_mat_free __isl_take isl_mat mat Note that the elements of a newly created matrix may have arbitrary values The elements can be changed and inspected using the following functions isl_ctx isl_mat_get_ctx __isl_keep isl_mat mat 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_give isl_mat isl_mat_set_element_si __isl_take isl_mat mat int row int col int v isl_mat_get_element will return a negative value if anything 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 multi
122. ned 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 86 2 3 Parametric Integer Programming 2 3 1 Introduction Parametric integer programming Feautrier 1988 is used to solve many problems within the context of the polyhedral model Here we are mainly interested in dependence analysis Feautrier 1991 and in computing a unique representation for existentially quantified variables The latter operation has been used for counting elements in sets involving such variables and lies at the core of the internal representation of isl Parametric integer programming was first implemented in PipLib An alternative method for parametric integer programming was later implemented in barvinok doolaege 2006 This method is not based on Feautrier s algorithm but on rational generating functions Barvinok and Woods 2003 and was inspired by the digging technique of a a Pt integer programming problems In the following sections we briefly recall the dual simplex method combined with Gomory cuts and describe some extensions and optimizations The main algorithm is applied to a matrix data structure known as a tableau In case of parametric prob lems there are two tableaus one for the main problem and one for the constraints on the parameters known as the context tableau The handling of the context tableau is described in Section 2 3 7 2
123. ng 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 J 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_source 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 78 The result of the dependence analysis is collected in an isl_flow There may be elements of the sink access for which no preceding source access could be found or for which all preceding sources are may accesses The relations containing 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 analysis with the sink a read and the sources must writes the first relation corresponds
124. nomials for an explanation of the difference between these two functions To iterate over all quasipolynomials in a reduction use int isl_qpolynomial_fold_foreach_qpolynomial __isl_keep isl_qpolynomial_fold fold int fn __isl_take isl_qpolynomial qp void user void user Properties of Piecewise Quasipolynomial Reductions To check whether two union piecewise quasipolynomial reductions are obviously equal use int isl_union_pw_qpolynomial_fold_plain_is_equal __isl_keep isl_union_pw_qpolynomial_fold upwf1 __isl_keep isl_union_pw_qpolynomial_fold upwf2 Operations on Piecewise Quasipolynomial Reductions __isl_give isl_qpolynomial_fold isl_qpolynomial_fold_scale __isl_take isl_qpolynomial_fold fold isl_int v __isl_give isl_pw_qpolynomial_fold isl_pw_qpolynomial_fold_add __isl_take isl_pw_qpolynomial_fold pwf1 __isl_take isl_pw_qpolynomial_fold pwf2 __isl_give isl_pw_qpolynomial_fold isl_pw_qpolynomial_fold_fold __isl_take isl_pw_qpolynomial_fold pwf1 __isl_take isl_pw_qpolynomial_fold pwf2 __isl_give isl_union_pw_qpolynomial_fold isl_union_pw_qpolynomial_fold_fold __isl_take isl_union_pw_qpolynomial_fold upwf1 __isl_take isl_union_pw_qpolynomial_fold upwf2 __isl_give isl_qpolynomial isl_pw_qpolynomial_fold_eval __isl_take isl_pw_qpolynomial_fold pwf __isl_take isl_point pnt 75 __isl_give isl_qpolynomial isl_union_pw_qpolynomial_fold_eval __isl_take isl_union_pw_qpol
125. ntain the composition of these extra elements with powers of Rj 109 2 5 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 where p ranges over the dimensions and L U and M are constant integer vectors The elements of U may be 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 i lt kUA Vp jp ip Mp p 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 5 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 calcu
126. of the resulting relation Changes since isl 0 06 e The format of isl_printer_print_qpolynomial s ISL_FORMAT_ISL output has changed Use ISL_FORMAT_C to obtain the old output e The _fast_ functions have been renamed to _plain_ Some of the old names have been kept for backward compatibility but they will be removed in the future Changes since isl 0 07 e The function isl_pw_aff_max has been renamed to isl_pw_aff_union_max Similarly the function isl_pw_aff_add has been renamed to isl_pw_aff_union_add e The isl_dim type has been renamed to isl_space along with the associated functions Some of the old names have been kept for backward compatibility but they will be removed in the future e Spaces of maps sets and parameter domains are now treated differently The dis tinction between map spaces and set spaces has always been made on a concep tual level but proper use of such spaces was never checked Furthermore up un til isl 0 07 there was no way of explicitly creating a parameter space These can now be created directly using isl_space_params_alloc or from other spaces using isl_space_params e The space in which isl_aff isl_pw_aff isl_qpolynomial isl_pw_qpolynomial isl_qpolynomial_fold and isl_pw_qpolynomial_fold objects live is now a map space instead of a set space This means for example that the dimensions of the domain of an isl_aff are now considered to be of type isl1_dim_in in stead of isl_dim_set Ext
127. oly nomial 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 piecewise quasipolynomial reduction as a function of an element in the domain of the map The functions taking a set compute a bound over all elements in the intersection of the set and the domain of the piecewise quasipolynomial reduction 1 3 22 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 The resulting dependence relations map source iterations to the corresponding sink iterations 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 from the last must access and from 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 77 include lt isl flow h gt typedef int
128. omplete 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 l K lyan xan 1 CR Li A K lyas xan 22 CR oK lyar xa121 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 Rt N Id 0 then since T is an overapproximation of R also T N Id This in turn means 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 103 2 5 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 U R and R o Ry 0 then we know that any path that passes through R cannot later pass through Rj i e R RI UR U R3 OR 2 11 We can therefore co
129. osure of the original relation is then equal to Rog U Ro U Rio U Rit 2 5 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 J then we can pick some R and compute the transitive closure of R as R r uUe onion 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 R U Id but 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 Rt U Idp to represent this relaxed version of R use the notation R C R D can be computed by allowing k to attain the value 0 in and by using PA D D 108 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 gt 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
130. ould only be measuring overhead such as input output and conversions and not the running time of the actual algorithm We compare the fol lowing versions piplib 1 4 0 5 g0132fd9 barvinok 9 32 1 73 gc5d7751 isl 0 05 1 82 g3a37260 and PPL version 0 11 2 94 PipLib barvinok islcut isl gbr PPL Phideo TC 793m gt 999m 2 7s 372m el 0 33s 3 5s 0 08s O 11s 0 18s e3 0 14s 0 13s 0 10s 0 10s 0 17s e4 0 24s 9 1s 0 09s 0 11s 0 70s e5 0 12s 6 0s 0 06s 0 14s 0 17s e6 0 10s 6 8s 0 17s 0 08s 0 21s e7 0 03s 0 27s 0 04s 0 04s 0 03s eg 0 03s 0 18s 0 03s 0 04s 0 01s e9 OOM 70m 2 6s 0 94s 22s vd 0 04s 0 10s 0 03s 0 03s 0 03s bouleti 0 25s line 0 06s 0 06s 0 15s difficult OOM 1 3s 1 7s 0 33s 1 4s cnt sum TC max 2 28 2 28 OOM jcomplex TC max 3 7s 3 9 OOM Table 2 1 Comparison of Execution Times The first test case is the following dependence analysis problem originating from the Phideo project that was communicated to us by Bart Kienhuis lexmax j1 j2 gt i1 12 13 14 i15 16 i17 18 19 i10 1 lt il jl lt 8 and 1 lt i2 i13 14 15 16 i17 18 i9 i10 lt 2 and 1 lt j2 lt 128 and il 1 jl 1 and i2 14 2 13 2 4 14 4 8 i5 8 16 i6 16 32 17 32 64 18 64 128 19 128 256 110 256 3 j2 3 66 This problem was the main inspiration for some of the optimizations in Section 2 3 7 The second group of test cases are projections used during counting The first nine of these come from Seghir and Loechner 2006 The remaining two come fro
131. p __isl_give isl_space isl_pw_qpolynomial_get_space __isl_keep isl_pw_qpolynomial pwaqp __isl_give isl_space isl_pw_qpolynomial_fold_get_domain_space __isl_keep isl_pw_qpolynomial_fold pwf __isl_give isl_space isl_pw_qpolynomial_fold_get_space __isl_keep isl_pw_qpolynomial_fold pwf __isl_give isl_space isl_union_pw_qpolynomial_get_space __isl_keep isl_union_pw_qpolynomial upwaqp __isl_give isl_space isl_union_pw_qpolynomial_fold_get_space __isl_keep isl_union_pw_qpolynomial_fold upwf include lt isl aff h gt __isl_give isl_space isl_aff_get_domain_space __isl_keep isl_aff aff __isl_give isl_space isl_aff_get_space __isl_keep isl_aff aff __isl_give isl_space isl_pw_aff_get_domain_space __isl_keep isl_pw_aff pwaff __isl_give isl_space isl_pw_aff_get_space __isl_keep isl_pw_aff pwaff __isl_give isl_space isl_multi_aff_get_space __isl_keep isl_multi_aff maff __isl_give isl_space isl_pw_multi_aff_get_domain_space __isl_keep isl_pw_multi_aff pma __isl_give isl_space isl_pw_multi_aff_get_space __isl_keep isl_pw_multi_aff pma include lt isl point h gt __isl_give isl_space isl_point_get_space __isl_keep isl_point pnt The identifiers or names of the individual dimensions may be set or read off using the following functions include lt isl space h gt __isl_give isl_space isl_space_set_dim_id __isl_take isl_space space enum isl_dim_type type
132. ple 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 53 1 3 17 Piecewise Quasi Affine Expressions The zero quasi affine expression on a given domain can be created using __isl_give isl_aff isl_aff_zero_on_domain __isl_take isl_local_space ls Note that the space in which the resulting object lives is a map space with the given space as domain and a one dimensional range An empty piecewise quasi affine expression one with no cells or a piecewise quasi affine expression with a single cell can be created using the following functions include lt isl aff h gt __isl_give isl_pw_aff isl_pw_aff_empty __isl_take isl_space space __isl_give isl_pw_aff isl_pw_aff_alloc __isl_take isl_set set __isl_take isl_aff aff __isl_give isl_pw_aff isl_pw_aff_from_aff __isl_take isl_aff aff Quasi affine expressions can be copied and freed using include lt isl aff h gt __isl_give isl_aff isl_aff_copy __isl_keep isl_aff aff void isl_aff_free __isl_take isl_aff aff __isl_give isl_pw_aff isl_pw_aff_copy __isl_keep isl_pw_aff pwaff void isl_pw_aff_free
133. pression to be non negative and one where the expression is negative As already mentioned by Feautrier 1988 any integer linear feasibility solver could be used but the PipLib implementation uses a recursive call to the dual simplex with Gomory cuts algorithm to determine the feasibility of a context In isl two ways of handling the context have been implemented one that performs the recursive call and one used by default that uses generalized basis reduction We start with some optimizations that are shared between the two implementations and then discuss additional details of each of them Maintaining Witnesses A common feature of both integer linear feasibility solvers is that they will not only say whether a set is empty or not but if the set is non empty they will also provide a witness for this result i e a point that belongs to the set By maintaining a list of such witnesses we can avoid many feasibility tests during the determination of the signs 92 of affine expressions In particular if the expression evaluates to a positive number on some of these points and to a negative number on some others then no feasibility test needs to be performed If all the evaluations are non negative we only need to check for the possibility of a negative value and similarly in case of all non positive evaluations Finally in the rare case that all points evaluate to zero or at the start when no points have been collected yet one or two f
134. pw_aff pwaff1 __isl_take isl_pw_aff pwaff2 __isl_give isl_aff isl_aff_sub __isl_take isl_aff aff1 __isl_take isl_aff aff2 57 __isl_give isl_pw_aff isl_pw_aff_sub __isl_take isl_pw_aff pwaff1 __isl_take isl_pw_aff pwaff2 __isl_give isl_aff isl_aff_neg __isl_take isl_aff aff __isl_give isl_pw_aff isl_pw_aff_neg __isl_take isl_pw_aff pwaff __isl_give isl_aff isl_aff_ceil __isl_take isl_aff aff __isl_give isl_pw_aff isl_pw_aff_ceil __isl_take isl_pw_aff pwaff __isl_give isl_aff isl_aff_floor __isl_take isl_aff aff __isl_give isl_pw_aff isl_pw_aff_floor __isl_take isl_pw_aff pwaff __isl_give isl_aff isl_aff_mod __isl_take isl_aff aff isl_int mod __isl_give isl_pw_aff isl_pw_aff_mod __isl_take isl_pw_aff pwaff isl_int mod __isl_give isl_aff isl_aff_scale __isl_take isl_aff aff isl_int f __isl_give isl_pw_aff isl_pw_aff_scale __isl_take isl_pw_aff pwaff isl_int f __isl_give isl_aff isl_aff_scale_down __isl_take isl_aff aff isl_int f __isl_give isl_aff isl_aff_scale_down_ui __isl_take isl_aff aff unsigned f __isl_give isl_pw_aff isl_pw_aff_scale_down __isl_take isl_pw_aff pwaff isl_int f __isl_give isl_pw_aff isl_pw_aff_list_min __isl_take isl_pw_aff_list list __isl_give isl_pw_aff isl_pw_aff_list_max __isl_take isl_pw_aff_list list __isl_give isl_pw_aff isl_pw_aff_coalesce __isl_take isl_pw_aff pwaqp __isl_give isl_pw_aff isl
135. r __isl_take isl_union_map umap int exact Compute a parametric representation for all positive powers k of map The result maps k to a nested relation corresponding to the kth power of map The result may be an overapproximation If the result is known to be exact then exact is set to 1 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 __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 e Reaching path lengths __isl_give isl_map isl_map_reaching_path_lengths __isl_take isl_map map int exact 41 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 messa
136. ra functions have been added to obtain the domain space Some of the constructors still take a domain space and have therefore been renamed e The functions isl_equality_alloc and isl_inequality_alloc now take an isl_local_space instead of an isl_space An isl_local_space can be cre ated from an isl_space using isl_local_space_from_space e The isl_div type has been removed Functions that used to return an isl_div now return an isl_aff Note that the space of an isl_aff is that of relation When replacing a call to isl_div_get_coefficient byacalltoisl_aff_get_coefficient any isl_dim_set argument needs to be replaced by isl_dim_in A call to isl_aff_from_div can be replaced by a call to isl_aff_floor A call to isl_qpolynomial_div div call be replaced by the nested call isl_qpolynomial_from_aff isl_aff_floor div The function isl_constraint_div has also been renamed to isl_constraint_get_div The nparam argument has been removed from isl_map_read_from_str and similar functions When reading input in the original PolyLib format the result will have no parameters If parameters are expected the caller may want to perform dimension manipulation on the result 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
137. rithm is invoked we then also incrementally keep track of this recession cone The reduced basis found by one call of the algorithm is also reused as initial basis for the next call Some problems lead to the introduction of many integer divisions Within a given context some of these integer divisions may be equal to each other even if the ex pressions are not identical or they may be equal to some affine combination of other variables To detect such cases we compute the affine hull of the context each time a new integer division is added The algorithm used for computing this affine hull is that of Karr 1976 while the points used in this algorithm are obtained by performing integer feasibility checks on that part of the context outside the current approximation of the affine hull The list of witnesses is used to construct an initial approximation of the hull while any extra points found during the construction of the hull is added to this list Any equality found in this way that expresses an integer division as an integer affine combination of other variables is propagated to the main tableau where it is used to eliminate that integer division 2 3 8 Experiments Table 2 1 compares the execution times of isl with both types of context tableau on some more difficult instances to those of other tools run on an Intel Xeon W3520 2 66GHz Easier problems such as the test cases distributed with PipLib can be solved so quickly that we w
138. rogramming problems we would like to avoid this overhead in future That is we are planning on introducing quasts or a related representation as one of several possible internal representations and on allowing the output of isl pip to optionally be printed as a quast Currently isl also does not have an internal representation for expressions such as min b p from the offline symmetry detection of Section 2 3 5 Assume that one of these expressions has n bounds b p If the expression does not appear in the affine expression describing the solution but only in the constraints and if moreover the expression only appears with a positive coefficient i e min b p gt f p then each of these constraints can simply be reduplicated n times once for each of the bounds Otherwise a conversion to disjunctive normal form leads to n cases each described as u b p with constraints b p lt b p for j gt i and b p lt b p for j lt i Note that even though this conversion leads to a size increase by a factor of n not detecting the symmetry could lead to an increase by a factor of n if all possible orderings end up being considered 2 3 7 Context Tableau The main operation that a context tableau needs to provide is a test on the sign of an affine expression over the elements of the context This sign can be determined by solving two integer linear feasibility problems one with a constraint added to the context that enforces the ex
139. s 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 Simple Hull of a Set The simple hull of a set S Uj lt jcy Si with S Ot 92 isn so xe Z See VV Axt Bst Dase ol l lt i lt v is the set H Z 2 sesos xez ez A Ax Bs DasasKi 20 l lt i lt v with K the component wise smallest non negative integer vectors such that S C H The K can be obtai
140. sl_take isl_pw_qpolynomial pwqp unsigned exponent __isl_give isl_union_pw_qpolynomial isl_union_pw_qpolynomial_add __isl_take isl_union_pw_qpolynomial upwaqp1 __isl_take isl_union_pw_qpolynomial upwqp2 __isl_give isl_union_pw_qpolynomial isl_union_pw_qpolynomial_sub __isl_take isl_union_pw_qpolynomial upwqp1 __isl_take isl_union_pw_qpolynomial upwqp2 __isl_give isl_union_pw_qpolynomial isl_union_pw_qpolynomial_mul __isl_take isl_union_pw_qpolynomial upwqp1 __isl_take isl_union_pw_qpolynomial upwqp2 __isl_give isl_qpolynomial isl_pw_qpolynomial_eval __isl_take isl_pw_qpolynomial pwqp __isl_take isl_point pnt __isl_give isl_qpolynomial isl_union_pw_qpolynomial_eval __isl_take isl_union_pw_qpolynomial upwaqp __isl_take isl_point pnt 71 __isl_give isl_set isl_pw_qpolynomial_domain __isl_take isl_pw_qpolynomial pwaqp __isl_give isl_pw_qpolynomial isl_pw_qpolynomial_intersect_domain __isl_take isl_pw_qpolynomial pwpq __isl_take isl_set set __isl_give isl_pw_qpolynomial isl_pw_qpolynomial_intersect_params __isl_take isl_pw_qpolynomial pwpq __isl_take isl_set set __isl_give isl_union_set isl_union_pw_qpolynomial_domain __isl_take isl_union_pw_qpolynomial upwqp __isl_give isl_union_pw_qpolynomial isl_union_pw_qpolynomial_intersect_domain __isl_take isl_union_pw_qpolynomial upwpq __isl_take isl_union_set uset __isl_give isl_union_pw_qpolynomial isl_unio
141. sl_union_map_range __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 35 __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 Elimination __isl_give isl_set isl_set_eliminate __isl_take isl_set set enum isl_dim_type type unsigned first unsigned n __isl_give isl_basic_map isl_basic_map_eliminate __isl_take isl_basic_map bmap enum isl_dim_type type unsigned first unsigned n __isl_give isl_map isl_map_eliminate __isl_take isl_map map enum isl_dim_type type unsigned first unsigned n Eliminate the coefficients for the given dimensions from the constraints without removing the dimensions Slicing __isl_give isl_basic_set isl_basic_set_fix __isl_take isl_basic_set bset enum isl_dim_type type unsigned pos isl_int value __isl_give isl_basic_set isl_basic_set_fix_si __isl_take isl_basic_set bset enum isl_dim_type type unsigned pos int value __isl_g
142. ssion is negative at the sample value since c 0 and r b p is fractional i e b p gt b p On the other hand for each integral value of r and c gt 0 the expression is non negative because b p b p gt 1 Imposing this expression to be non negative therefore does not invalidate any integral solutions while it does cut away the current fractional sample value To be able to formulate this constraint a new variable q b p b p is added to the context This integral variable 88 is uniquely defined by the constraints 0 lt db p dq lt d 1 with d the common denominator of f and g In practice the variable g f p g is used instead and the coefficients of the new constraint are adjusted accordingly The sign of the constant term of this new constraint need not be determined as it is non positive by construction When several of these extra context variables are added it is important to avoid adding duplicates Recent versions of PipLib also check for such duplicates 2 3 4 Negative Unknowns and Maximization There are two places in the above algorithm where the unknowns x are assumed to be non negative the initial tableau starts from sample value x 0 and is assumed to be non negative during the construction of Gomory cuts To deal with negative unknowns Appendix A 2 proposed to use a big parameter say M that is taken to be an arbitrarily large positive number Instea
143. t 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 pnt1 __isl_take isl_point pnt2 __isl_give isl_set isl_set_box_from_points __isl_take isl_point pnt1 __isl_take isl_point pnt2 65 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 fn __isl_take isl_point pnt void user void user int isl_union_set_foreach_point __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 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_t
144. t the original object gets used somewhere else or is explicitly freed The arguments and return values of all documented 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 its usual operation However it will still make sure that all the other __isl_take arguments are re leased _ 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 Error H
145. titioning step but the resulting partition will usually be a singleton The result of the recursive call will either be exact or an overapproximation The final result of Floyd Warshall is therefore also exact or an overapproximation Example 2 5 9 Consider the relation on the right of Figure 1 of Beletska et al 2009 107 reproduced in Figure 2 3 This relation can be described as x y gt x2 y2 By 2x A x2 xXA3y2 34 2xAxX2 gt 0AX lt 3 V 2 1LltxAy yAxzOA3y gt 24 2xAx lt 2A3y lt 34 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 domains and ranges can therefore be partitioned into two parts Po and P shown as the white and black dots in Figure 2 3 respectively Initially we have Roo 9 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 2xAx gt 20Ax lt 3 Ri 0 In the first iteration Rog remains the same 0 Ro and Rio are therefore also unaffected but R is updated to include Ro Ro i e the dashed arrow in the figure This new Rj 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 Rig Ro ie the dotted arrow in the figure The transitive cl
146. to the reads from uninitialized array elements and the second relation is empty 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 whether 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 may_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_map must_no_source __isl_give isl_union_map may_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 th
147. unsigned pos 13 __isl_take isl_id id int isl_space_has_dim_id __isl_keep isl_space space enum isl_dim_type type unsigned pos __isl_give isl_id isl_space_get_dim_id __isl_keep isl_space space enum isl_dim_type type unsigned pos __isl_give isl_space isl_space_set_dim_name __isl_take isl_space space enum isl_dim_type type unsigned pos __isl_keep const char name __isl_keep const char isl_space_get_dim_name __isl_keep isl_space space enum isl_dim_type type unsigned pos Note that isl_space_get_name returns a pointer to some internal data structure so the result can only be used while the corresponding isl_space is alive Also note that every 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_set isl_map isl_union_set and or is l_union_map arguments may have different parameters as long as they are named in which case the result will have as parameters the union of the parameters of the arguments Given the identifier or name of a dimension typically a parameter its position can be obtained from the following function include lt isl space h gt int isl_space_find_dim_by_id __isl_keep isl_space space enum isl_dim_type type __isl_keep isl_id id int isl_space_find_dim_by_name __isl_keep
148. 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 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 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
149. ut 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 assuming isl_set_align_params and isl_map_align_params are not sufficient 44 1 3 14 Binary 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_params __isl_take isl_basic_set bset1 __isl_take isl_basic_set bset2 __isl_give isl_basic_set isl_basic_set_intersect __isl_take isl_basic_set bset1 __isl_take isl_basic_set bset2 __isl_give isl_set isl_set_intersect_params __isl_take isl_set set __isl_take isl_set params __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_params __isl_take isl_union_set uset __isl_take isl_set set __isl_give isl_union_map isl_union_map_intersect_params __isl_take isl_union_map umap __isl_take isl_set set __isl_give isl_union_set isl_union_set_intersect __isl_take isl_union_set uset1 __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 __
150. ve isl_set isl_set_from_union_set __isl_take isl_union_set uset __isl_give isl_map isl_map_from_union_map __isl_take isl_union_map umap 22 A zero dimensional set can be constructed on a given parameter domain using the following function __isl_give isl_set isl_set_from_params __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_copy __isl_keep isl_basic_set bset __isl_give isl_set isl_set_copy __isl_keep isl_set set __isl_give isl_union_set isl_union_set_copy __isl_keep isl_union_set uset __isl_give isl_basic_map isl_basic_map_copy __isl_keep isl_basic_map bmap __isl_give isl_map isl_map_copy __isl_keep isl_map map __isl_give isl_union_map isl_union_map_copy __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 l_take isl_union_map umap Other sets and relations can be constructed by 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 or removed
151. worst case the basic algorithm may have to consider all possible orderings of the constant terms Instead is introduces a new parameter say u and replaces the collection of constraints by the single constraint u a x 0 along with context constraints u lt b p Any solution to the new system is also a solution to the original system since a x gt u gt b p Conversely m min b p satisfies the constraints on u and therefore extends a solution to the new system It can also be plugged into a new solution See for how this substitution is currently performed in isl The method described in this section can only detect symmetries that are explicitly available in the input See for the detection and exploitation of symmetries that appear during the course of the dual simplex method Parameter Compression It may in some cases be apparent from the equalities in the problem description that there can only be a solution for a sublattice of the parameters In such cases parameter compression can be used to replace the parameters by alternative dense parameters For example if there is a constraint 2x n then the system will only have solutions for even values of n and n can be replaced by 2n Similarly the parameters n and m in a system with the constraint 2n 3m can be replaced by a single parameter n with n 3n and m 2n It is also possible to perform a similar compression on the unknowns but it woul
152. xample 2 5 8 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 R U R3 U R3 with Ri n i j gt i 3 j i lt 2j 4Ai lt n 3Aj lt 2i l1 Aj lt n R n i j gt i j 3 i lt 2j 1 Ai lt nAj lt 2i 4Aj lt n 3 Rz n i j gt i 1 j 1 i lt 2j l Ai lt n 1 Aj lt 2i l j lt n l1 The figure shows this relation for n 1 Both R o R C R o R3 and R3 o Ra C R30 R3 which the reader can verify using the iscc calculator R1 n gt i j gt i 3 j i lt 2 j 4 and i lt n 3 and j lt 2 i 1 andj lt n R2 n gt i j gt 1i j 3 i lt 2 j 1 andi 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 R1 R3 R3 R1 R2 R3 R3 R2 105 Figure 2 2 The relation from Example 2 5 8 R3 can therefore be moved forward in any path For the other two basic relations we have both Ry o R R o R and R o Ry R o R and so R and R form a strongly connected component By computing the power of R3 and R U R3 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 5 5 Partitioning the domains and ranges o
153. ynomial_fold upwf __isl_take isl_point pnt __isl_give isl_pw_qpolynomial_fold sl_pw_qpolynomial_fold_intersect_params __isl_take isl_pw_qpolynomial_fold pwf __isl_take isl_set set __isl_give isl_union_set isl_union_pw_qpolynomial_fold_domain __isl_take isl_union_pw_qpolynomial_fold upwf __isl_give isl_union_pw_qpolynomial_fold isl_union_pw_qpolynomial_fold_intersect_dc __isl_take isl_union_pw_qpolynomial_fold upwf __isl_take isl_union_set uset __isl_give isl_union_pw_qpolynomial_fold isl_union_pw_qpolynomial_fold_intersect_params __isl_take isl_union_pw_qpolynomial_fold upwf __isl_take isl_set set __isl_give isl_pw_qpolynomial_fold isl_pw_qpolynomial_fold_project_domain_on_param __isl_take isl_pw_qpolynomial_fold pwf __isl_give isl_pw_qpolynomial_fold isl_pw_qpolynomial_fold_coalesce __isl_take isl_pw_qpolynomial_fold pwf __isl_give isl_union_pw_qpolynomial_fold isl_union_pw_qpolynomial_fold_coalesce __isl_take isl_union_pw_qpolynomial_fold upwf __isl_give isl_qpolynomial_fold isl_qpolynomial_fold_gist_params __isl_take isl_qpolynomial_fold fold __isl_take isl_set context __isl_give isl_qpolynomial_fold isl_qpolynomial_fold_gist __isl_take isl_qpolynomial_fold fold __isl_take isl_set context __isl_give isl_pw_qpolynomial_fold isl_pw_qpolynomial_fold_gist __isl_take isl_pw_qpolynomial_fold pwf __isl_take isl_set context __isl_give isl_pw_qpolynomial

Integer Set Library: Manual

Contents

Download Pdf Manuals

Related Search

Related Contents