Home

Integer Set Library: Manual

1. 1 5 Polyhedral Compilation Library This section collects functionality in isl that has been specifically designed for use during polyhedral compilation 1 5 1 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 106 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 include lt isl flow h gt typedef int 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
2. __isl_give isl_basic_set isl_set_unshifted_simple_hul11 __isl_take isl_set set __isl_give isl_basic_map isl_map_unshifted_simple_hul1 __isl_take isl_map map __isl_give isl_basic_set isl_set_simple_hul11 __isl_take isl_set set __isl_give isl_basic_map isl_map_simple_hu11 __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 con straints describing the basic sets or relations in the input In case of isl_set_unshifted_simple_hul1 only the original constraints are used without any translation 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_hul1l __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_hul1 __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 In case of union sets and relations the affine hull is computed per space 51 e Polyhedral hull __isl_give isl_basic_set isl_set_polyhedral_hul1l __isl_take i
3. int isl_val_get_den_gmp __isl_keep isl_val v mpz_t z Conversion from isl_int The following functions are only temporarily available to ease the transition from isl_int to isl_val They will be removed in the next release include lt isl val_int h gt __isl_give isl_val isl_val_int_from_isl_int isl_ctx ctx isl_int n int isl_val_get_num_isl_int __isl_keep isl_val v isl_int n 1 4 3 Integers obsolescent In previous versions of isl integers were represented in the external interface using the isl_int type This type has now been superseded by isl val The isl_int type will be removed from the external interface in future releases New code should not use is _int The operations below are currently available on isl_ints 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 required is _int_init i is _int_clear i is _int_set 1 i is _int_set_si r i isl_int_set_gmp r g isl_int_get_gmp i g is _int_abs r i 12 isl_int_neg r i isl_int_swap i j isl_int_swap_or set i j is _int_add_ui r i j is _int_sub_ui z i
4. 1 4 13 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 bset int isl_basic_set_is_empty __isl_keep isl_basic_set bset int isl_set_plain_is_empty __isl_keep isl_set set int isl_set_is_empty __isl_keep isl_set set int isl_union_set_is_empty __isl_keep isl_union_set uset int isl_basic_map_plain_is_empty __isl_keep isl_basic_map bmap int isl_basic_map_is_empty __isl_keep isl_basic_map bmap int isl_map_plain_is_empty __isl_keep isl_map map int isl_map_is_empty __isl_keep isl_map map int isl_union_map_is_empty __isl_keep isl_union_map umap e Universality int isl_basic_set_is_universe __isl_keep isl_basic_set bset int isl_basic_map_is_universe __isl_keep isl_basic_map bmap int isl_set_plain_is_universe __isl_keep isl_set set 40 e Single valuedness int int int int e Injectivity int int int int e Bijectivity int int e Position int int int isl_basic_map_is_single_valued __isl_keep isl_basic_map bmap isl_map_plain_is_single_valued __isl_keep isl_map map isl_map_is_single_valued __isl_keep isl_map map isl_union_map_is_single_valued __isl_keep isl_union_map umap isl_map
5. S Z gt 2 s1 Ss x eZ Iz Zf 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 132 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 g
6. __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_constant_val __isl_take isl_aff aff __isl_take isl_val 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_coefficient_val __isl_take isl_aff aff enum isl_dim_type type int pos __isl_take isl_val 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_constant_val __isl_take isl_aff aff __isl_take isl_val v __isl_give isl_aff isl_aff_add_constant_num __isl_take isl_aff aff isl_int v __isl_give isl_aff isl_aff_add_constant_num_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
7. exists b 0 lt 10a 10b and 10a 9 10b 9 lt 100 a b c d gt separation_class 1 gt 0 lt 10a 10b and 10a 9 10b 9 lt 100 which simplifies to a b c d gt separation_class 1 gt 0 a gt 0 and b gt 0 and b lt 8 a a b c d gt separation_class 0 gt 0 a gt 0 and a lt 8 With this option the generated AST is as follows for int cO 0 cO lt 8 c 1 for int cl 0 cl lt c0 8 c1 1 for int c2 10 cQ c2 lt 10 cO 9 c2 1 for int c3 10 cl c3 lt 10 cl 9 c3 1 A c2 c3 for int cl c0 9 cl lt c0 10 c1 1 for int c2 10 cQ c2 lt min 10 c1 100 10 c 9 c2 1 126 for int c3 10 cl c3 lt min c2 100 10 cl 9 c3 1 ACc2 c3 for int c 9 cO lt 10 cO 1 for int cl 0 cl lt c0 10 c1 1 for int c2 10 cQ c2 lt min 10 c1 100 10 cO 9 c2 1 for int c3 10 cl c3 lt min 10 cl 9 c2 100 c3 1 ACc2 c3 separate This is a single dimensional space representing the schedule dimension s to which separation should be applied Separation tries to split a loop into sev eral pieces if this can avoid the generation of guards inside the loop See also the atomic option atomic This is a single dimensional space representing the schedule dimension s for which the domains s
8. isl_options_get_ast_build_atomic_upper_bound isl_ctx ctx isl_options_set_ast_build_prefer_pdiv isl_ctx ctx int val isl_options_get_ast_build_prefer_pdiv isl_ctx ctx isl_options_set_ast_build_exploit_nested_bounds isl_ctx ctx int val isl_options_get_ast_build_exploit_nested_bounds isl_ctx ctx isl_options_set_ast_build_group_coscheduled isl_ctx ctx int val isl_options_get_ast_build_group_coscheduled isl_ctx ctx isl_options_set_ast_build_scale_strides 122 isl_ctx ctx int val int isl_options_get_ast_build_scale_strides isl_ctx ctx int isl_options_set_ast_build_allow_else isl_ctx ctx int val int isl_options_get_ast_build_allow_else isl_ctx ctx int isl_options_set_ast_build_allow_or isl_ctx ctx int val int isl_options_get_ast_build_allow_or isl_ctx ctx ast_build_atomic_upper_bound Generate loop upper bounds that consist of the current loop iterator an operator and an expression not involving the iterator If this option is not set then the current loop iterator may appear several times in the upper bound For example when this option is turned off AST generation for the schedule n gt ALi gt i 0 lt i lt 100 n produces for int c 0 cO lt 100 amp amp n gt cO cO 1 ACcO When the option is turned on the following AST is generated for int c 0 cO lt min 100 n cO 1 ACcO ast_build_prefer_pdiv If this option is tur
9. isl_union_set_is_strict_subset __isl_keep isl_union_set usetl __isl_keep isl_union_set uset2 isl_basic_map_is_subset __isl_keep isl_basic_map bmap1 __isl_keep isl_basic_map bmap2 isl_basic_map_is_strict_subset __isl_keep isl_basic_map bmap1 __isl_keep isl_basic_map bmap2 isl_map_is_subset __isl_keep isl_map map1 __isl_keep isl_map map2 isl_map_is_strict_subset __isl_keep isl_map map1 __isl_keep isl_map map2 isl_union_map_is_subset __isl_keep isl_union_map umap1 __isl_keep isl_union_map umap2 isl_union_map_is_strict_subset __isl_keep isl_union_map umap1 __isl_keep isl_union_map umap2 isl_set_plain_cmp __isl_keep isl_set setl __isl_keep isl_set set2 This function is useful for sorting isl_sets The order depends on the internal representation of the inputs The order is fixed over different calls to the function assuming the internal representation of the inputs has not changed but may change over different versions of isl 44 1 4 14 Unary Operations e Complement __isl_give isl_set isl_set_complement __isl_take isl_set set __isl_give isl_map isl_map_complement e Inverse map __isl_take isl_map map __isl_give isl_basic_map isl_basic_map_reverse __isl_take isl_basic_map bmap __isl_give isl_map isl_map_reverse __isl_take isl_map map __isl_give isl_union_map isl_union_map_reverse e Projection __isl_take isl_u
10. 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 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_constant_val __isl_take isl_constraint constraint __isl_take isl_val 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 30 __isl_give isl_constraint isl_constraint_set_coefficient_val __isl_take isl_constraint constraint enum isl_dim_type type int pos isl_val v __isl_give isl_basic_map isl_basic_map_add_constraint __isl_take isl_basic_map bmap __isl_take isl_constraint constraint __isl_give isl_basic_set isl_basic_set_add_constraint __isl_take isl_basic_set bset __i
11. At the end they say If an upper bound is required it can be calculated in a manner similar to that of a single conjunct sic relation Presumably the authors mean that a d form approximation of the whole input rela tion should be used However the accuracy can be improved by also trying to apply the incremental technique from the same paper which is explained in more detail in Section 2 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 157 Bibliography Bagnara R P M Hill and E Zaffanella The Parma Polyhedra Library www cs unipr it ppl 141 Barthou D A Cohen and J F Collard 2000 Maximal static expansion Int J Parallel Program 28 3 213 243 153 Barvinok A and K Woods 2003 April Short rational generating functions for lattice point problems J Amer Math Soc 16 957 979 134 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 ing
12. __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 __isl_keep isl_union_pw_qpolynomial upwap 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 upwap __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 96 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 com
13. __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 delta set 49 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 One of the methods for combining pairs of basic sets or relations can result in coefficients that are much larger than those that appear in the constraints of the input By default the coefficients are not allowed to grow larger but this can be changed by unsetting the following option int isl_
14. 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_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 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 104 __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
15. enum isl_dim_type type int pos int v __isl_give isl_aff isl_aff_add_coefficient_val __isl_take isl_aff aff 76 enum isl_dim_type type int pos __isl_take isl_val v __isl_give isl_aff isl_aff_insert_dims __isl_take isl_aff aff 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 unsigned 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 isl_aff_set_constant isl_aff_set_constant_si isl_aff_set_coefficient and isl_aff_set_coefficient_si set the numerator of the constant or coefficient while isl_aff_set_constant_val and isl_aff_set_coefficient_val set the con stant or coefficient as a whole The add_constant and add_coefficient functions add an integer or rational value to the possibly rational constant or coefficient The add_constant_num functions add an integer value to the numerator To check whether an affine expressions is obviously zero or obviously equal to
16. int isl_val_is_nonneg __isl_keep isl_val v int isl_val_is_nonpos __isl_keep isl_val v int isl_val_is_pos __isl_keep isl_val v int isl_val_is_neg __isl_keep isl_val v int isl_val_is_int __isl_keep isl_val v int isl_val_is_rat __isl_keep isl_val v int isl_val_is_nan __isl_keep isl_val v int isl_val_is_infty __isl_keep isl_val v int isl_val_is_neginfty __isl_keep isl_val v Note that the sign of NaN is undefined The following binary properties are defined on pairs of isl_vals include lt isl val h gt int isl_val_lt __isl_keep isl_val v1 __isl_keep isl_val v2 int isl_val_le __isl_keep isl_val v1 __isl_keep isl_val v2 int isl_val_gt __isl_keep isl_val v1 __isl_keep isl_val v2 int isl_val_ge __isl_keep isl_val v1 __isl_keep isl_val v2 int isl_val_eq __isl_keep isl_val v1 __isl_keep isl_val v2 int isl_val_ne __isl_keep isl_val v1 __isl_keep isl_val v2 For integer isl_vals we additionally have the following binary property include lt isl val h gt int isl_val_is_divisible_by __isl_keep isl_val v1 __isl_keep isl_val v2 An isl_val can also be compared to an integer using the following function The result is undefined for NaN include lt isl val h gt int isl_val_cmp_si __isl_keep isl_val v long i The following unary operations are available on isl_vals include lt isl val h gt __isl_give isl_val isl_val_abs __isl_t
17. 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 Compute a relation that maps each element in the range of map to the lengths of all paths composed of edges in map that end up in the given element The result may be an overapproximation If the result is known to be exact then exact is set to 1 To compute the maximal path length the resulting relation should be postprocessed by isl_map_lexmax In particular if the input relation is a dependence relation mapping sources to sinks then the maximal path length corresponds to the free schedule Note however that isl_map_lexmax expects the maximum to be finite so if the path lengths are unbounded possibly due to the overapproximation then you will get an error message e Wrapping __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 55 e Flattening Remove any i
18. vec isl_int m isl_vec_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 concatenate two vectors __isl_give isl_vec isl_vec_concat __isl_take isl_vec vecl __isl_take isl_vec vec2 1 4 19 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_val isl_mat_get_element_val __isl_keep isl_mat mat int row int col __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_give isl_mat isl_mat_set_element_val __isl_take isl_mat mat int row int col __isl_take isl_val v isl mat_get_element will return a negative value if anything went wrong In that case the v
19. 8 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 4 5 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 that the original object gets used somewhere else or is explicitly freed 14 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
20. International Journal of Parallel Programming 20 1 23 53 1341 136 Feautrier P 1992 December Some efficient solutions to the affine scheduling problem Part II multidimensional time International Journal of Parallel Pro gramming 21 6 389 420 136 Feautrier P J Collard and C Bastoul 2002 Solving systems of affine inequalities Technical report PRISM Versailles University 136 Galea F 2009 November personal communication 141 Karr M 1976 Affine relationships among variables of a program Acta Informat ica 6 133 151 141 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 151 Kelly W V Maslov W Pugh E Rosser T Shpeisman and D Wonnacott 1996b November The Omega library Technical report University of Maryland 157 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 O
21. Logical and of two arguments Both arguments can be evaluated isl_ast_op_and_then Logical and of two arguments The second argument can only be evaluated if the first evaluates to true isl_ast_op_or Logical or of two arguments Both arguments can be evaluated isl_ast_op_or_else Logical or of two arguments The second argument can only be evaluated if the first evaluates to false isl_ast_op_max Maximum of two or more arguments isl_ast_op_min Minimum of two or more arguments isl_ast_op_minus Change sign isl_ast_op_add Sum of two arguments 117 isl_ast_op_sub Difference of two arguments isl_ast_op_mul Product of two arguments isl_ast_op_div Exact division That is the result is known to be an integer isl_ast_op_fdiv_q Result of integer division rounded towards negative infinity isl_ast_op_pdiv_q Result of integer division where dividend is known to be non negative isl_ast_op_pdiv_r Remainder of integer division where dividend is known to be non negative isl_ast_op_cond Conditional operator defined on three arguments If the first argument evaluates to true then the result is equal to the second argument Otherwise the result is equal to the third argument The second and third argument may only be eval uated if the first argument evaluates to true and false respectively Corresponds toa b cinC isl_ast_op_select Conditional operator defined on three arguments If
22. T may be exact even if K is not exact so the check is sound but incomplete To check exactness of the power we simply need to check 2 1 Since again K is known to be an overapproximation we only need to check whether 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 150 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 th
23. __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 __isl_take isl_printer p __isl_keep isl_pw_multi_aff pma __isl_give isl_printer isl_printer_print_union_pw_multi_aff __isl_take isl_printer p __isl_keep isl_union_pw_multi_aff upma __isl_give isl_printer isl_printer_print_multi_pw_aff __isl_take isl_printer p __isl_keep isl_multi_pw_aff mpa 91 1 4 22 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_val isl_point_get_coordinate_val __isl_keep isl_point pnt enum isl_dim_type type int pos __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_set_coordinate_val __isl_take isl_point pnt enum isl_dim_type type int pos __isl_take isl_val 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_p
24. __isl_give isl_pw_multi_aff isl_set_lexmax_pw_multi_aff __isl_take isl_set set __isl_give isl_pw_multi_aff isl_map_lexmin_pw_multi_aff __isl_take isl_map map __isl_give isl_pw_multi_aff isl_map_lexmax_pw_multi_aff __isl_take isl_map map 1 4 16 Lists Lists are defined over several element types including isl_val isl_id isl_aff isl_pw_aff isl_constraint isl_basic_set isl_set isl_ast_expr and isl_ast_node 67 Here we take lists of isl_sets as an example Lists can be created copied modified 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_insert __isl_take isl_set_list list unsigned pos __isl_take isl_set el __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_drop __isl_take isl_set_list list unsigned first unsigned n __isl_give isl_set_list isl_set_list_set_set __isl_take isl_set_list list int index __isl_take isl_set set __isl_give isl_set_list isl_set_list_concat __isl_take isl_set_list listl __isl_take isl_set_list list2 __isl_give isl_set_list isl_set_list_sort __isl_take isl_set_list list int cmp __i
25. be treated as a parameter while a can be treated as a variable This 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 c
26. ceiling function and the fractional part This expression 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 135 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 i
27. come from Seghir and Loechner 2006 The remaining two come from 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 142 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 p
28. e e eS A OR A s 92 1 4 23 Piecewise Quasipolynomials ooo a 1 5 Polyhedral Compilation Library 1 5 1 Dependence Analysis 000 1 5 2 Scheduling e e sos e OS oh ESS Be RS a RS 1 6 2 US1 pip erase ess krena HOR eo ae ee eS 1 6 3 isl polyhedron minimize 1 6 4 isl_ polytope scan oaoa 1 6 5 isl codegen aaa aa 20 200 05 000 Implementation Details 2 1 Setsand Relations oaaae 2 2 Simple Hull 22s 4 be oh moni EEE per A ESAS 2 3 Parametric Integer Programming 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 DAs Coalescingji 4 6 are dow A See linge x aoe rs BB S 2 5 Transitive Closure 2 5 1 Introduction o ea scs erresa sed ee ee 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 co
29. integer vectors such that S C H The K can be obtained by solving a number of LP problems one for each element of each K If any LP problem is unbounded then the corresponding constraint is dropped 133 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 o
30. is a wrapped relation 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_map mapl1 __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 e Disjointness int isl_set_plain_is_disjoint __isl_keep isl_set setl __isl_keep isl_set set2 int isl_set_is_disjoint __isl_keep isl_set set1 __isl_keep isl_set set2 int isl_map_is_disjoint __isl_keep isl_map map1 __isl_keep isl_map map2 e Subset 43 int int int int int int int int int int int Check whether the first argument is a strict subset of the second argument Order int isl_basic_set_is_subset __isl_keep isl_basic_set bsetl __isl_keep isl_basic_set bset2 isl_set_is_subset __isl_keep isl_set setl __isl_keep isl_set set2 isl_set_is_strict_subset __isl_keep isl_set set1 __isl_keep isl_set set2 isl_union_set_is_subset __isl_keep isl_union_set usetl __isl_keep isl_union_set uset2
31. isl_aff_project_domain_on_params __isl_take isl_aff aff __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 __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 affl __isl_take isl_aff aff2 __isl_give isl_aff isl_aff_div __isl_take isl_aff affl __isl_take isl_aff af 2 __isl_give isl_pw_aff isl_pw_aff_mul 79 __isl_take isl_pw_aff pwaff1 __isl_take isl_pw_aff pwaff2 __isl_give isl_pw_aff isl_pw_aff_div __isl_take isl_pw_aff pal __isl_take isl_pw_aff pa2 __isl_give isl_pw_aff isl_pw_aff_tdiv_q __isl_take isl_pw_aff pal __isl_take isl_pw_aff pa2 __isl_give isl_pw_aff isl_pw_aff_tdiv_r __isl_take isl_pw_aff pal __isl_take isl_pw_aff pa2 When multiplying two affine expressions at least one of the two needs to be a con stant Similarly when dividing a
32. 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 __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 Note that isl_local_space_get_div can only be used on local spaces of sets 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 __isl_take isl_local_space ls enum isl_dim_type type unsigned n 23 __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 4 10 Input and Output isl supports i
33. isl_pw_multi_aff pma 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 85 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 int isl_union_pw_multi_aff_foreach_pw_multi_aff __isl_keep isl_union_pw_multi_aff upma int fn __isl_take isl_pw_multi_aff pma void user void user It can be modified using include lt isl aff h gt __isl_give isl_multi_aff isl_multi_aff_set_aff __isl_take isl_multi_aff multi int pos __isl_take isl_aff aff __isl_give isl_pw_multi_aff isl_pw_multi_aff_set_pw_aff __isl_take isl_pw_multi_aff pma unsigned pos __isl_take isl_pw_aff pa __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_multi_aff isl_multi_aff_set_tuple_name __isl_take isl_multi_aff maff enum isl_dim_type type const char s __isl_give isl_multi_aff isl_multi_aff_set_tuple_id __isl_take isl_multi_aff maff enum isl_dim_type type __isl_take isl_id id __isl_give isl_pw_multi_aff isl_pw_multi_aff_s
34. 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 38 int isl_map_has_tuple_name __isl_keep isl_map map enum isl_dim_type type 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_id isl_basic_set_get_dim_id __isl_keep isl_basic_set bset enum isl_dim_type type unsigned pos __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 __isl_give isl_id isl_map_get_dim_id __isl_keep
35. 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 __isl_take __isl_take Preimage isl_union_map umap1 isl_union_map umap2 __isl_give isl_basic_set isl_basic_set_preimage_multi_aff __isl_take __isl_take __isl_give isl_set __isl_take __isl_take __isl_give isl_set __isl_take __isl_take __isl_give isl_map __isl_take __isl_take isl_basic_set bset isl_multi_aff ma isl_set_preimage_multi_aff isl_set set isl_multi_aff ma isl_set_preimage_pw_multi_aff isl_set set isl_pw_multi_aff pma isl_map_preimage_domain_multi_aff isl_map map isl_multi_aff ma __isl_give isl_union_map isl_union_map_preimage_domain_multi_aff __isl_take __isl_take isl_union_map umap isl_multi_aff ma These functions compute the preimage of the given set or map domain under the given function In other words the expression is plugged into the set de scription or into the domain of the map Objects of types isl_multi_aff and isl_pw multi_aff are described in Cartesian Product __isl_give isl_set isl_set_product 62 __isl_take isl_set setl __isl_take isl_set set2 __isl_give isl_union_set isl_union_set_product __isl_take isl_union_set uset1 __isl_take isl_union_s
36. j isl_int_add r i j isl int_sub r i j isl int mul r i j is _int_mul_ui r i j is _int_addmul r i j isl int_submul 1i j is int_gcd r i j is _int_lem 1i j isl_int_divexact r i j is _int_cdiv_q i j is _int_fdiv_q r i j is _int_fdiv_r r i j isl_int_fdiv_q_ui r 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 is _int_ne i j is _int_It i j is _int_le i j isl_int_gt i j 13 isl_int_ge i j is _int_abs_eq i j is _int_abs_ne i j is _int_abs_It i j isl_int_abs_gt i j isl_int_abs_ge i j is _int_is_zero i is _int_is_one i is _int_is_negone i is _int_is_pos i is _int_is_neg i is _int_is_nonpos i is _int_is_nonneg i isl_int_is_divisible_by i j 1 4 4 Sets and Relations isl uses six types of objects for representing sets and relations isl_basic_set isl_basic_map isl_set isl_map isl_union_set and isl_union_map isl_basic_set and isl_basic_map represent sets and relations that can be described as a conjunction of affine constraints while isl_set and is1_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 1 4
37. 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_local_space_dim __isl_keep isl_local_space ls enum isl_dim_type type 22 int isl_local_space_has_dim_id __isl_keep isl_local_space ls enum isl_dim_type type unsigned pos __isl_give isl_id isl_local_space_get_dim_id __isl_keep isl_local_space ls enum isl_dim_type type unsigned pos int isl_local_space_has_dim_name __isl_keep isl_local_space ls enum isl_dim_type type unsigned pos 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
38. 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 _ is _take argument 1 4 6 Error Handling 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 requir
39. optional name and an optional user pointer The name and the user pointer cannot both be NULL however Identifiers with the same name but dif ferent pointer values are considered to be distinct Similarly identifiers with different names but the same pointer value are also considered to be distinct Equal identifiers are represented using the same object Pairs of identifiers can therefore be tested for equality using the operator 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_set_free_user __isl_take isl_id id __isl_give void free_user 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 isl_id id The callback set by isl_id_set_free_user is called on the user pointer when the last reference to the isl_id is freed Note that is1_id_get_name returns a pointer to some internal data structure so the result can only be used while the corresponding isl_id is alive 16 1 4 8 Spaces Whenever a new set relation or similiar object is created from s
40. performed using a recursive call This recursive call includes the partitioning 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 154 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 inc
41. positive side we will have fewer negative and in determinate 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 140 If the parameters may be negati
42. 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 Like isl1_schedule_foreach_band the function isl_band_list_foreach_band calls fn on the bands in depth first post order A band can be tiled using the following function include lt isl band h gt int isl_band_tile __isl_keep isl_band band __isl_take isl_vec sizes int isl_options_set_tile_scale_tile_loops isl_ctx ctx int val int isl_options_get_tile_scale_tile_loops isl_ctx ctx int isl_options_set_tile_shift_point_loops isl_ctx ctx int val int isl_options_get_tile_shift_point_loops isl_ctx ctx The isl_band_tile function tiles the band using the given tile sizes inside its schedule A new child band is created to represent the point loops and it is inserted between the modified band and its children The tile_scale_tile_loops option specifies whether the tile loops iterators should be scaled by the tile sizes If the tile_shift_point_loops option is set then the point loops are shifted to start at Zero A band can be split into two nested bands using the following function int isl_band_split __isl_keep isl_band band int pos The resulting outer band contains the first pos dimensions of band while the inner band contains the remaining dimensions A representation of the band can be printed using 112 include lt isl band h gt _
43. s That is b c are the opposites of the coefficients of a valid 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 147 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
44. 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 affl __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 77 __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_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 __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_aff isl_aff_mod_val __isl_take isl_aff aff __isl
45. 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 the 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 argument
46. the first argument evaluates to true then the result is equal to the second argument Otherwise the result is equal to the third argument The second and third argument may be evaluated independently of the value of the first argument Corresponds toa b 1 a cinC isl_ast_op_eq Equality relation isl_ast_op_le Less than or equal relation isl_ast_op_1t Less than relation isl_ast_op_ge Greater than or equal relation isl_ast_op_gt Greater than relation 118 isl_ast_op_call A function call The number of arguments of the isl_ast_expr is one more than the number of arguments in the function call the first argument representing the function being called include lt isl ast h gt __isl_give isl_id isl_ast_expr_get_id __isl_keep isl_ast_expr expr Return the identifier represented by the AST expression include lt isl ast h gt int isl_ast_expr_get_int __isl_keep isl_ast_expr expr isl_int v __isl_give isl_val isl_ast_expr_get_val __isl_keep isl_ast_expr expr Return the integer represented by the AST expression Note that the integer is returned by isl_ast_expr_get_int through the v argument The return value of this function itself indicates whether the operation was performed successfully Manipulating and printing the AST AST nodes can be copied and freed using the following functions include lt isl ast h gt __isl_give isl_ast_node isl_ast_node_copy __isl_kee
47. 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 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
48. Check if the values of the given set dimension are equal to a fixed value modulo some integer value If so assign the modulo to modulo and the fixed value to residue If the given dimension attains only a single value then assign 0 to modulo and the fixed value to residue If the dimension does not attain only a single value and if no modulo can be found then assign 1 to modulo and 1 to residue 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 e Currying 42 int isl_basic_map_can_curry __isl_keep isl_basic_map bmap int isl_map_can_curry __isl_keep isl_map map Check whether the domain of the basic relation is a wrapped relation int isl_basic_map_can_uncurry __isl_keep isl_basic_map bmap int isl_map_can_uncurry __isl_keep isl_map map Check whether the range of the basic relation
49. Clearly Ri o Ra C Rp o R and so R U R2 Rj o RF UR U R3 Example 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 i j 3 i lt 2 j 1 and i lt n and j lt 2i 4 and j lt n 3 R3 n gt i j gt i 1 j 1 i lt 2 j 1 and i lt n 1 and j lt 21 1 andj lt n 1 R1 R3 R3 R1 R2 R3 R3 R2 152 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 overa
50. Integer Set Library Manual Version isl 0 12 2 Sven Verdoolaege January 12 2014 Contents I User Manual 3 1 1 Introduction 2 2 2 2 0 0 00 ee eee 3 1 1 1 Backward Incompatible Changes 3 Oe Ae wee a Se eng bw aM aap a Ue oA Beige S 5 1 3 Installation sien a ee ee eR RE SOR PS 6 1 3 1 Installation from the git repository 6 1 3 2 Common installation instructions 7 1 4 Integer Set Library 2 02 2 2 2 000 8 1 4 1 Initialization ooa 2 2 2 2 0040 8 L42 Values 2 3 ee a ba we ee E e ea be ee be ba 8 1 4 3 Integers obsolescent 2 0004 12 1 4 4 Sets and Relations 00 14 1 4 5 Memory Management 0 14 1 4 6 ErrorHandling 2 2 2 002 000 15 1 4 7 Identifiers 2 2 ee ee ee ee 16 seh Maina es es ie Bape a ete pe Se Ro ents ee eae SF Bh has 17 Se ee ee a ek e fot ee he ee 22 1 4 10 Inputand Output 2 2 2 2 ee 24 TERRERO 27 E E EE 33 a a een ee aD eee a a E a 40 Bytes es Mee seeps Settee she BE ees ts asa I eS 45 Fane ete Mepity doh Gp E E 1 te 59 1 4 16 Lists asa csaka eh Rae eek eo SES ee N 67 oh ae Avie E eae ee Seo mantle Amman a Ae ea 69 1 4 18 Vectors o econ t 2 eS Re Ee OA ee Ree RAS 71 1 4 19 Mattic s s s 24 4 ss de ee oe da ee a ree amp 72 Peer res eters 73 ih paired 83 422 Ports
51. ORS OR COPY RIGHT HOLDERS BE LIABLE FOR ANY CLAIM DAMAGES OR OTHER LI ABILITY WHETHER IN AN ACTION OF CONTRACT TORT OR OTHERWISE ARISING FROM OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE Note that isl currently requires GMP which is released under the GNU Lesser General Public License LGPL This means that code linked against is is also linked against LGPL code 1 3 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 3 1 Installation from the git repository 1 Clone or update the repository The first time the source is obtained you need to clone the repository git clone git repo or cz isl git To obtain updates you need to pull in the latest changes git pull 2 Generate configure autogen sh After performing the above steps continue with the Common installation instruc tions 1 3 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 op
52. Relations R 0 lt p q lt n Output Updated relations Rp such that each 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 i Rpg Rpq U Rig o Rpr U Ry o Ry o Rpr Aa un e WwW NY 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 Rog U R i s t dom R CP ran RjCP apply algorithm IJand return the union of all resulting R as the transitive closure of R Each iteration of the r loop injalgorithm Ijupdates 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 lis
53. __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 identifying either a source or the sink and it should return the shared nesting level and the relative order of the two accesses In particular let n be the num ber of loops shared by the two accesses If first precedes second textually then 107 the functi
54. _add_pw_multi_aff __isl_take isl_union_pw_multi_aff upma __isl_take isl_pw_multi_aff pma __isl_give isl_union_pw_multi_aff isl_union_pw_multi_aff_from_domain __isl_take isl_union_set uset A piecewise multiple quasi affine expression can also be initialized from an isl_set or isl_map provided the isl_set is a singleton and the isl_map is single valued In case of a conversion from an isl_union_set or an isl_union_map to an isl_union_pw_multi_aff these properties need to hold in each space __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 __isl_give isl_union_pw_multi_aff isl_union_pw_multi_aff_from_union_set __isl_take isl_union_set uset __isl_give isl_union_pw_multi_aff isl_union_pw_multi_aff_from_union_map __isl_take isl_union_map umap 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 __isl_give isl_union_pw_multi_aff isl_union_pw_multi_aff_copy __isl_keep isl_union_pw_multi_aff upma void isl_union_pw_multi_aff_free __isl_take isl_union_pw_mult
55. _basic_map bmap __isl_give isl_basic_map isl_basic_map_range_map __isl_take isl_basic_map bmap __isl_give isl_map isl_map_domain_map __isl_take isl_map map __isl_give isl_map isl_map_range_map __isl_take isl_map map __isl_give isl_union_map isl_union_map_domain_map __isl_take isl_union_map umap __isl_give isl_union_map isl_union_map_range_map __isl_take isl_union_map umap The functions above construct a basic regular or union relation that maps a wrapped version of the input relation to its domain or range Elimination __isl_give isl_basic_set isl_basic_set_eliminate __isl_take isl_basic_set bset enum isl_dim_type type unsigned first unsigned n __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 46 __isl_take isl_basic_set bset enum isl_dim_type type unsigned pos in
56. _children __isl_keep isl_ast_node node __isl_give isl_ast_expr isl_ast_node_user_get_expr __isl_keep isl_ast_node node Each of the returned isl_ast_exprs can in turn be inspected using the following functions include lt isl ast h gt isl_ctx isl_ast_expr_get_ctx __isl_keep isl_ast_expr expr enum isl_ast_expr_type isl_ast_expr_get_type __isl_keep isl_ast_expr expr 116 The type of an AST expression is one of isl_ast_expr_op isl_ast_expr_id or isl_ast_expr_int An isl_ast_expr_op represents the result of an operation An isl_ast_expr _id represents an identifier An isl_ast_expr_int represents an integer value Each type of expression has its own additional properties include lt isl ast h gt enum isl_ast_op_type isl_ast_expr_get_op_type __isl_keep isl_ast_expr expr int isl_ast_expr_get_op_n_arg __isl_keep isl_ast_expr expr __isl_give isl_ast_expr isl_ast_expr_get_op_arg __isl_keep isl_ast_expr expr int pos int isl_ast_node_foreach_ast_op_type __isl_keep isl_ast_node node int fn enum isl_ast_op_type type void user void user isl_ast_expr_get_op_type returns the type of the operation performed isl_ast_expr_get_op_n_arg returns the number of arguments isl_ast_expr_get_op_arg returns the specified ar gument isl_ast_node_foreach_ast_op_type calls fn for each distinct isl_ast_op_type that appears in node The operation type is one of the following isl_ast_op_and
57. _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 __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 37 int isl_set_dim_has_any_lower_bound __isl_keep isl_set set enum isl_dim_type type unsigned pos int isl_set_dim_has_any_upper_bound __isl_keep isl_set set enum isl_dim_type type unsigned
58. _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 quasipoly 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 4 25 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 int isl_vertices_foreach_vertex __isl_keep isl_vertices vertices int fn __isl_take isl_vertex vertex void user void user 105 int isl_vertices_foreach_cell __isl_keep isl_vertices
59. _get_coefficient_val __isl_keep isl_aff aff enum isl_dim_type type int pos int isl_aff_get_denominator __isl_keep isl_aff aff isl_int v __isl_give isl_val isl_aff_get_denominator_val __isl_keep isl_aff aff __isl_give isl_aff isl_aff_get_div __isl_keep isl_aff aff int pos int isl_pw_aff_n_piece __isl_keep isl_pw_aff pwaff 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 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 75 __isl_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
60. _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_map isl_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 32 __isl_take isl_pw_multi_aff pma __isl_give isl_union_map isl_union_map_from_union_pw_multi_aff __isl_take isl_union_pw_multi_aff upma 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 4 12 Inspecting Sets and Relations Usually the user should not have to care about the actual constraints of the sets and maps but should instead apply the abstract operations explained in the following sec tions Occasionally however it may be required to inspect the individual coefficients of the constraints This section explains how to do so In these cases it may also be useful to have isl compute an explicit representation of the existentially quantified variables __isl_give isl_set isl_set_compute_divs __isl_take isl_set set __isl_give isl_map isl_map_compute_divs __isl_take isl_map map __isl_give isl_union_set isl_union_set_compute_divs __isl_take isl_union_set uset __isl_give isl_union_map isl_
61. _give isl_map __isl_take __isl_take isl_set set2 isl_map_subtract isl_map map1 isl_map map2 isl_map_subtract_domain isl_map map isl_set dom isl_map_subtract_range isl_map map isl_set dom __isl_give isl_union_set isl_union_set_subtract __isl_take isl_union_set usetl __isl_take isl_union_set uset2 __isl_give isl_union_map isl_union_map_subtract __isl_take isl_union_map umap1 __isl_take isl_union_map umap2 __isl_give isl_union_map isl_union_map_subtract_domain __isl_take __isl_take isl_union_map umap isl_union_set dom __isl_give isl_union_map isl_union_map_subtract_range e Application __isl_take __isl_take isl_union_map umap isl_union_set dom __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 61 __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_take isl_basic_map bmap1 isl_basic_map bmap2 isl_map_apply_domain isl_map map1 isl_map map2 __isl_give
62. _give isl_multi_val isl_multi_val_scale_multi_val __isl_take isl_multi_val mv1 __isl_take isl_multi_val mv2 1 4 18 Vectors Vectors can be created copied and freed using the following functions include lt isl vec h gt __isl_give isl_vec isl_vec_alloc isl_ctx ctx unsigned size __isl_give isl_vec isl_vec_copy __isl_keep isl_vec vec void isl_vec_free __isl_take isl_vec vec Note that the elements of a newly created vector may have arbitrary values The elements can be changed and inspected using the following functions isl_ctx isl_vec_get_ctx __isl_keep isl_vec vec int isl_vec_size __isl_keep isl_vec vec int isl_vec_get_element __isl_keep isl_vec vec int pos isl_int v __isl_give isl_val isl_vec_get_element_val __isl_keep isl_vec vec int pos __isl_give isl_vec isl_vec_set_element __isl_take isl_vec vec int pos isl_int v __isl_give isl_vec isl_vec_set_element_si __isl_take isl_vec vec int pos int v __isl_give isl_vec isl_vec_set_element_val __isl_take isl_vec vec int pos __isl_take isl_val v __isl_give isl_vec isl_vec_set __isl_take isl_vec vec isl_int v __isl_give isl_vec isl_vec_set_si __isl_take isl_vec vec int v __isl_give isl_vec isl_vec_set_val __isl_take isl_vec vec __isl_take isl_val v int isl_vec_cmp_element __isl_keep isl_vec vecl 71 __isl_keep isl_vec vec2 int pos __isl_give isl_vec isl_vec_fdiv_r __isl_take isl_vec
63. _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 97 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 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_scale_val __isl_take isl_qpolynomial qp __isl_take isl_val v __isl_give isl_qpolynomial isl_qpolynomial_neg __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_
64. _isl_give isl_printer isl_printer_print_band __isl_take isl_printer p __isl_keep isl_band band Options include lt isl schedule h gt int isl_options_set_schedule_max_coefficient isl_ctx ctx int val int isl_options_get_schedule_max_coefficient isl_ctx ctx 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_fuse isl_ctx ctx int val int isl_options_get_schedule_fuse isl_ctx ctx int isl_options_set_schedule_maximize_band_depth isl_ctx ctx int val int isl_options_get_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_scaled isl_ctx ctx int val int isl_options_get_schedule_split_scaled isl_ctx ctx int isl_options_set_schedule_algorithm isl_ctx ctx int val int isl_options_get_schedule_algorithm isl_ctx ctx int isl_options_set_schedule_separate_components isl_ctx ctx int val int isl_options_get_schedule_separate_components isl_ctx ctx e schedule_max_coefficient This option enforces that the coefficients for variable and parameter dimensions in the calculated schedule are not larger than the specified value This option can significantly increase the speed of the scheduling calculati
65. _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 59 __isl_give isl_basic_map isl_basic_map_intersect_range __isl_take isl_basic_map bmap __isl_take isl_basic_set bset __isl_give isl_basic_map isl_basic_map_intersect __isl_take isl_basic_map bmap1 __isl_take isl_basic_map bmap2 __isl_give isl_map isl_map_intersect_params __isl_take isl_map map __isl_take isl_set params __isl_give isl_map isl_map_intersect_domain __isl_take isl_map map __isl_take isl_set set __isl_give isl_map isl_map_intersect_range __isl_take isl_map map __isl_take isl_set set __isl_give isl_map isl_map_intersect __isl_take isl_map map1 __isl_take isl_
66. _multi_aff ma2 __isl_give isl_multi_aff isl_multi_aff_flat_range_product __isl_take isl_multi_aff mal 89 __isl_take isl_multi_aff ma2 __isl_give isl_multi_aff isl_multi_aff_product __isl_take isl_multi_aff mal __isl_take isl_multi_aff ma2 __isl_give isl_pw_multi_aff isl_pw_multi_aff_range_product __isl_take isl_pw_multi_aff pmal __isl_take isl_pw_multi_aff pma2 __isl_give isl_pw_multi_aff isl_pw_multi_aff_flat_range_product __isl_take isl_pw_multi_aff pmal __isl_take isl_pw_multi_aff pma2 __isl_give isl_pw_multi_aff isl_pw_multi_aff_product __isl_take isl_pw_multi_aff pmal __isl_take isl_pw_multi_aff pma2 __isl_give isl_union_pw_multi_aff isl_union_pw_multi_aff_flat_range_product __isl_take isl_union_pw_multi_aff upmal __isl_take isl_union_pw_multi_aff upma2 __isl_give isl_multi_pw_aff isl_multi_pw_aff_range_splice __isl_take isl_multi_pw_aff mpal unsigned pos __isl_take isl_multi_pw_aff mpa2 __isl_give isl_multi_pw_aff isl_multi_pw_aff_splice __isl_take isl_multi_pw_aff mpal unsigned in_pos unsigned out_pos __isl_take isl_multi_pw_aff mpa2 __isl_give isl_multi_pw_aff isl_multi_pw_aff_range_product __isl_take isl_multi_pw_aff mpal __isl_take isl_multi_pw_aff mpa2 __isl_give isl_multi_pw_aff isl_multi_pw_aff_flat_range_product __isl_take isl_multi_pw_aff mpal __isl_take isl_multi_pw_aff mpa2 If the 1s argument of isl_multi_aff_li
67. _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 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 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 __isl_give isl_val isl_basic_map_plain_get_val_if_fixed __isl_keep isl_basic_map bmap enum isl_dim_type type unsigned pos __isl_give isl_val isl_set_plain_get_val_if_fixed __isl_keep isl_set set enum isl_dim_type type unsigned pos 41 __isl_give isl_val isl_map_plain_get_val_if_fixed __isl_keep isl_map map enum isl_dim_type type unsigned pos If the set or relation obviously lies on a hyperplane where the given dimension has a fixed value then return that value Otherwise return NaN e Stride int isl_set_dim_residue_class_val __isl_keep isl_set set int pos __isl_give isl_val modulo __isl_give isl_val residue
68. _pw_aff pa __isl_give isl_ast_expr isl_ast_build_call_from_pw_multi_aff __isl_keep isl_ast_build build __isl_take isl_pw_multi_aff pma The domains of pa and pma should correspond to the schedule space of build The tuple id of pma is used as the function being called User specified data can be attached to an isl_ast_node and obtained from the same isl_ast_node using the following functions include lt isl ast h gt __isl_give isl_ast_node isl_ast_node_set_annotation __isl_take isl_ast_node node __isl_take isl_id annotation __isl_give isl_id isl_ast_node_get_annotation __isl_keep isl_ast_node node Basic printing can be performed using the following functions include lt isl ast h gt __isl_give isl_printer isl_printer_print_ast_expr __isl_take isl_printer p __isl_keep isl_ast_expr expr __isl_give isl_printer isl_printer_print_ast_node __isl_take isl_printer p __isl_keep isl_ast_node node 120 More advanced printing can be performed using the following functions include lt isl ast h gt __isl_give isl_printer isl_ast_op_type_print_macro enum isl_ast_op_type type __isl_take isl_printer p __isl_give isl_printer isl_ast_node_print_macros __isl_keep isl_ast_node node __isl_take isl_printer p __isl_give isl_printer isl_ast_node_print __isl_keep isl_ast_node node __isl_take isl_printer p __isl_take isl_ast_print_options options __isl_give isl_pri
69. _read_from_str ctx i exists a i 2a and i gt 10 and i lt 42 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_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 or union set or relation can also be constructed from a union piecewise multiple affine expression or a list of affine expressions See 1 4 20 and 1 4 21 __isl_give isl_basic_map isl_basic_map_from_aff __isl_take isl_aff aff __isl_give isl_map isl_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
70. _read_from_str isl_ctx ctx const char str include lt isl union_set h gt __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 25 void isl_printer_free __isl_take isl_printer printer __isl_give char isl_printer_get_str __isl_keep isl_printer printer The printer can be inspected using the following functions FILE isl_printer_get_file __isl_keep isl_printer printer int isl_printer_get_output_format __isl_keep isl_printer p The behavior of the printer can be modified in various ways __isl_give isl_printer isl_printer_set_output_format __isl_take isl_printer p int output_format __isl_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_prin
71. _restrict __isl_take isl_ast_build build __isl_take isl_set set The isl_ast_build_get_schedule function returns a partial schedule for the domains elements for which part of the AST still needs to be generated in the current build In particular the domain elements are mapped to those iterations of the loops enclosing the current point of the AST generation inside which the domain elements are executed No direct correspondence between the input schedule and this schedule should be assumed The space obtained from isl_ast_build_get_schedule_space can be used to create a set for isl_ast_build_restrict to intersect with the current build In particular the set passed to isl_ast_build_restrict can have additional parameters The ids of the set dimensions in the space returned by isl_ast_build_get_schedule_space correspond to the iterators of the already generated loops The user should not rely on the ids of the output dimensions of the relations in the union relation returned by isl_ast_build_get_schedule having any particular value 1 6 Applications Although isl is mainly meant to be used as a library it also contains some basic applications that use some of the functionality of isl The input may be specified in either the isl format or the PolyLib format 130 1 6 1 isl_polyhedron_sample isl_polyhedron_samp1le takes a polyhedron as input and prints an integer element of the polyhedron if there is any The first column in the ou
72. _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 64 __isl_give isl_union_map isl_union_map_gist __isl_take isl_union_map umap __isl_take isl_union_map context __isl_give isl_union_map isl_union_map_gist_params __isl_take isl_union_map umap __isl_take isl_set set __isl_give isl_union_map isl_union_map_gist_domain __isl_take isl_union_map umap __isl_take isl_union_set uset __isl_give isl_union_map isl_union_map_gist_range __isl_take isl_union_map umap __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 inequalities that are redundant with respect to the intersection are removed In case of union sets and relations the gist operation is performed per space Lexicographic Optimization Given a basic set set or bset and a zero dimensional domain dom the following functions compute a set that contains the lexicographic minimum or maximum of the el
73. _take isl_pw_qpolynomial pwqp enum isl_dim_type type unsigned pos const char s 94 Creating New Piecewise Quasipolynomials Some simple quasipolynomials can be created using the following functions More complicated quasipolynomials can be created by applying operations such as addition and multiplication on the resulting quasipolynomials __isl_give isl_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 __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_val_on_domain __isl_take isl_space domain __isl_take isl_val val __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 ma
74. _take isl_val mod __isl_give isl_pw_aff isl_pw_aff_mod __isl_take isl_pw_aff pwaff isl_int mod __isl_give isl_pw_aff isl_pw_aff_mod_val __isl_take isl_pw_aff pa __isl_take isl_val mod __isl_give isl_aff isl_aff_scale __isl_take isl_aff aff isl_int f __isl_give isl_aff isl_aff_scale_val __isl_take isl_aff aff __isl_take isl_val v __isl_give isl_pw_aff isl_pw_aff_scale __isl_take isl_pw_aff pwaff isl_int f __isl_give isl_pw_aff isl_pw_aff_scale_val __isl_take isl_pw_aff pa __isl_take isl_val v __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_aff isl_aff_scale_down_val __isl_take isl_aff aff __isl_take isl_val v __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_scale_down_val 78 __isl_take isl_pw_aff pa __isl_take isl_val 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_aff isl_aff_align_params __isl_take isl_aff aff __isl_take isl_space model __isl_give isl_pw_aff isl_pw_aff_align_params __isl_take isl_pw_aff pwaff __isl_take isl_space model __isl_give isl_aff
75. _type type2 int pos2 set __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 48 __isl_give isl_basic_map isl_basic_map_order_ge __isl_take isl_basic_map bmap enum isl_dim_type typel int posl enum isl_dim_type type2 int pos2 __isl_give isl_map isl_map_order_1lt __isl_take isl_map map enum isl_dim_type typel int posl enum isl_dim_type type2 int pos2 __isl_give isl_basic_map isl_basic_map_order_gt __isl_take isl_basic_map bmap enum isl_dim_type typel int posl enum isl_dim_type type2 int pos2 __isl_give isl_map isl_map_order_gt __isl_take isl_map map enum isl_dim_type typel int posl enum isl_dim_type type2 int pos2 Intersect the relation with the half space where the given dimensions satisfy the given ordering 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 __isl_give isl_basic_set isl_basic_map_deltas
76. _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 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_set_n_constraint __isl_keep isl_basic_set bset int isl_basic_set_foreach_constraint __isl_keep isl_basic_set bset int fn __isl_take isl_constraint c void user void user int isl_basic_map_foreach_constraint __isl_keep isl_basic_map bmap int fn __isl_take isl_constraint c void user void user voi
77. a set space An isl_multi_val can be constructed from an isl_val_list using the following function include lt isl val h gt __isl_give isl_multi_val isl_multi_val_from_val_list __isl_take isl_space space __isl_take isl_val_list list The zero multiple value with value zero for each set dimension can be created using the following function include lt isl val h gt __isl_give isl_multi_val isl_multi_val_zero __isl_take isl_space space Multiple values can be copied and freed using include lt isl val h gt __isl_give isl_multi_val isl_multi_val_copy __isl_keep isl_multi_val mv void isl_multi_val_free __isl_take isl_multi_val mv They can be inspected using include lt isl val h gt isl_ctx isl_multi_val_get_ctx __isl_keep isl_multi_val mv unsigned isl_multi_val_dim __isl_keep isl_multi_val mv enum isl_dim_type type 69 __isl_give isl_val isl_multi_val_get_val __isl_keep isl_multi_val mv int pos const char isl_multi_val_get_tuple_name __isl_keep isl_multi_val mv enum isl_dim_type type They can be modified using include lt isl val h gt __isl_give isl_multi_val isl_multi_val_set_val __isl_take isl_multi_val mv int pos __isl_take isl_val val __isl_give isl_multi_val isl_multi_val_set_dim_name __isl_take isl_multi_val mv enum isl_dim_type type unsigned pos const char s __isl_give isl_multi_val isl_multi_val_set_tuple_name __isl_take isl_multi_
78. aces 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 __isl_give isl_space isl_space_unwrap __isl_take isl_space space The input to isl_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_
79. ake isl_val v __isl_give isl_val isl_val_neg __isl_take isl_val v __isl_give isl_val isl_val_floor __isl_take isl_val v __isl_give isl_val isl_val_ceil __isl_take isl_val v __isl_give isl_val isl_val_trunc __isl_take isl_val v The following binary operations are available on isl_vals include lt isl val h gt __isl_give isl_val isl_val_abs __isl_take isl_val v __isl_give isl_val isl_val_neg __isl_take isl_val v __isl_give isl_val isl_val_floor __isl_take isl_val v __isl_give isl_val isl_val_ceil __isl_take isl_val v __isl_give isl_val isl_val_trunc __isl_take isl_val v __isl_give isl_val isl_val_2exp __isl_take isl_val v __isl_give isl_val isl_val_min __isl_take isl_val v1 __isl_take isl_val v2 __isl_give isl_val isl_val_max __isl_take isl_val vl __isl_take isl_val v2 __isl_give isl_val isl_val_add __isl_take isl_val v1 __isl_take isl_val v2 10 __isl_give isl_val isl_val_add_ui __isl_take isl_val v1 unsigned long v2 __isl_give isl_val isl_val_sub __isl_take isl_val vl __isl_take isl_val v2 __isl_give isl_val isl_val_sub_ui __isl_take isl_val v1 unsigned long v2 __isl_give isl_val isl_val_mul __isl_take isl_val v1 __isl_take isl_val v2 __isl_give isl_val isl_val_mul_ui __isl_take isl_val v1 unsigned long v2 __isl_give isl_val isl_val_div __isl_take isl_val vl __isl_take isl_val v2 On integer values we a
80. al __isl_keep isl_pw_multi_aff pma2 Operations include include lt isl aff h gt __isl_give isl_pw_multi_aff isl_pw_multi_aff_union_lexmin __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_lexmax __isl_take isl_pw_multi_aff pmal __isl_take isl_pw_multi_aff pma2 __isl_give isl_multi_aff isl_multi_aff_add __isl_take isl_multi_aff maff1l __isl_take isl_multi_aff maff2 __isl_give isl_pw_multi_aff isl_pw_multi_aff_add __isl_take isl_pw_multi_aff pmal __isl_take isl_pw_multi_aff pma2 __isl_give isl_union_pw_multi_aff isl_union_pw_multi_aff_add __isl_take isl_union_pw_multi_aff upmal __isl_take isl_union_pw_multi_aff upma2 __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_sub __isl_take isl_multi_aff mal 87 __isl_take isl_multi_aff ma2 __isl_give isl_pw_multi_aff isl_pw_multi_aff_sub __isl_take isl_pw_multi_aff pmal __isl_take isl_pw_multi_aff pma2 __isl_give isl_union_pw_multi_aff isl_union_pw_multi_aff_sub __isl_take isl_union_pw_multi_aff upmal __isl_take isl_union_pw_multi_aff upma2 islmulti_aff_sub subtracts the second argument from the first __isl_give isl_multi_aff isl_multi_aff_scale __isl_take isl_multi_aff maff isl_int f __isl_give isl_multi_aff isl_multi_aff_scal
81. alue of v is undefined The following function can be used to compute the right inverse of a matrix i e a matrix such that the product of the original and the inverse in that order is a multiple of the identity matrix The input matrix is assumed to be of full row rank __isl_give isl_mat isl_mat_right_inverse __isl_take isl_mat mat 72 The following function can be used to compute the right kernel or null space of a matrix i e a matrix such that the product of the original and the kernel in that order is the zero matrix __isl_give isl_mat isl_mat_right_kernel __isl_take isl_mat mat 1 4 20 Piecewise Quasi Affine Expressions The zero quasi affine expression or the quasi affine expression that is equal to a specified dimension on a given domain can be created using __isl_give isl_aff isl_aff_zero_on_domain __isl_take isl_local_space ls __isl_give isl_pw_aff isl_pw_aff_zero_on_domain __isl_take isl_local_space ls __isl_give isl_aff isl_aff_var_on_domain __isl_take isl_local_space ls enum isl_dim_type type unsigned pos __isl_give isl_pw_aff isl_pw_aff_var_on_domain __isl_take isl_local_space ls enum isl_dim_type type unsigned pos Note that the space in which the resulting objects live 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 cre
82. ams_alloc For other sets the space needs to be created using isl1_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 is 1_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_keep isl_space space int isl_space_is_set __isl_keep isl_space space int isl_space_is_map __isl_keep isl_space space Spaces can be compared using the following functions include lt isl space h gt int isl_space_is_equal __isl_keep isl_space spacel __isl_keep isl_space space2 int isl_space_is_domain __isl_keep isl_space spacel 17 __isl_keep isl_space space2 int isl_space_is_range __isl_keep isl_space spacel __isl_keep isl_space space2 isl_space_is_domain checks whether the first argument is equal to the domain of the second argument This requires in particular that the first argument is a set space and that the second argument is a map 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 Quasipo
83. an be set using the following function include lt isl ast_build h gt __isl_give isl_ast_build isl_ast_build_set_options __isl_take isl_ast_build control __isl_take isl_union_map options The options are encoded in an lt is _union_map gt The domain of this union relation refers to the schedule domain i e the range of the schedule passed to isl_ast_build_ast_from_schedule In the case of nested AST generation see 1 5 3 the domain of options should re fer to the extra piece of the schedule That is it should be equal to the range of the wrapped relation in the range of the schedule The range of the options can consist of elements in one or more spaces the names of which determine the effect of the op tion The values of the range typically also refer to the schedule dimension to which the option applies In case of nested AST generation see 1 5 3 these values refer to the position of the schedule dimension within the innermost AST generation The constraints on the domain elements of the option should only refer to this dimension and earlier dimensions We consider the following spaces separation_class This space is a wrapped relation between two one dimensional spaces The in put space represents the schedule dimension to which the option applies and the output space represents the separation class While constructing a loop corre sponding to the specified schedule dimension s the AST generator will try to gene
84. arately in an arbitrary order It should be noted that the image elements only specify the order in which the corresponding domain elements should be visited No direct relation between the image elements and the loop iterators in the generated AST should be assumed Each AST is generated within a build The initial build simply specifies the con straints on the parameters if any and can be created inspected copied and freed using the following functions include lt isl ast_build h gt __isl_give isl_ast_build isl_ast_build_from_context __isl_take isl_set set isl_ctx isl_ast_build_get_ctx __isl_keep isl_ast_build build __isl_give isl_ast_build isl_ast_build_copy __isl_keep isl_ast_build build void isl_ast_build_free __isl_take isl_ast_build build The set argument is usually a parameter set with zero or more parameters More isl_ast_build functions are described in 1 5 3 and 91 5 3 Finally the AST itself can be constructed using the following function include lt isl ast_build h gt __isl_give isl_ast_node isl_ast_build_ast_from_schedule __isl_keep isl_ast_build build __isl_take isl_union_map schedule Inspecting the AST The basic properties of an AST node can be obtained as follows include lt isl ast h gt isl_ctx isl_ast_node_get_ctx __isl_keep isl_ast_node node enum isl_ast_node_type isl_ast_node_get_type __isl_keep isl_ast_node node The type of an AST node is one of is
85. ases distributed with PipLib can be solved so quickly that we would 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 141 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
86. asic_set bset enum isl_dim_type type unsigned first unsigned n __isl_give isl_basic_map isl_basic_map_remove_divs_involving_dims __isl_take isl_basic_map bmap enum isl_dim_type type unsigned first unsigned n __isl_give isl_set isl_set_remove_divs_involving_dims __isl_take isl_set set enum isl_dim_type type unsigned first unsigned n __isl_give isl_map isl_map_remove_divs_involving_dims __isl_take isl_map map enum isl_dim_type type unsigned first unsigned n __isl_give isl_basic_set isl_basic_set_remove_unknown_divs __isl_take isl_basic_set bset __isl_give isl_set isl_set_remove_unknown_divs __isl_take isl_set set __isl_give isl_map isl_map_remove_unknown_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 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 34 __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
87. ated 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 A piecewise quasi affine expression that is equal to 1 on a set and 0 outside the set can be created using the following function include lt isl aff h gt __isl_give isl_pw_aff isl_set_indicator_function __isl_take isl_set set 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 73 __isl_give isl_pw_aff isl_pw_aff_copy __isl_keep isl_pw_aff pwaff void isl_pw_aff_free __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 c
88. ccurate For simplicity we first assume that no constraint in A involves any existentially quantified variables We will return to existentially quantified variables at the end of this section Without existentially quantified variables we can classify the constraints of A as follows 1 non parametric constraints Aix 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 w
89. coefficients a b gt gt coefficients a b gt 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 3ao 79 2 n 5 1l xAx gt 6 148 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
90. cratch the space in which it lives needs to be specified using an isl_space Each space involves zero or more parameters and zero one or two tuples of set or input output dimensions The parameters and dimensions are identified by an isl_dim_type and a position The type isl_dim_param refers to parameters the type isl_dim_set refers to set dimen sions for spaces with a single tuple of dimensions and the types isl_dim_in and isl_dim_out refer to input and output dimensions for spaces with two tuples of di mensions Local spaces see also contain dimensions of type isl_dim_div Note that parameters are only identified by their position within a given object Across different objects parameters are usually identified by their names or identifiers Only unnamed parameters are identified by their positions across objects The use of un named parameters is discouraged 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 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_par
91. ction work with extended offsets A A x 1 That is each offset is extended with an extra coordinate that is set equal to one The paths constructed by summing such extended offsets have the length encoded as the difference of their final coordi nates The path P can then be decomposed into paths P one for each Aj P P U Id o o 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 145 just an optimization The procedure described below would produce results that are at least as a
92. d Proceedings of 14th International Conference on Compiler Construc tion Edinburgh Scotland Volume 3443 of Lecture Notes in Computer Science Berlin pp 91 105 Springer Verlag 134 Verhaegh W F J 1995 Multidimensional Periodic Scheduling Ph D thesis Technische Universiteit Eindhoven 142 160
93. d for the given choice of R and D In order to be able to replace R by C R D in 2 13 D should be chosen to include both dom R and ran R i e such that Idp oR o Idp R for all j i 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 closur
94. d isl_constraint_free __isl_take isl_constraint c 35 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 int isl_constraint_is_equality __isl_keep isl_constraint constraint The coefficients of the constraints can be inspected using the following functions int isl_constraint_is_lower_bound __isl_keep isl_constraint constraint enum isl_dim_type type unsigned pos int isl_constraint_is_upper_bound __isl_keep isl_constraint constraint enum isl_dim_type type unsigned pos void isl_constraint_get_constant __isl_keep isl_constraint constraint isl_int v __isl_give isl_val isl_constraint_get_constant_val __isl_keep isl_constraint constraint void isl_constraint_get_coefficient __isl_keep isl_constraint constraint enum isl_dim_type type int pos isl_int v __isl_give isl_val isl_constraint_get_coefficient_val __isl_keep isl_constraint constraint enum isl_dim_type type int pos 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 f
95. dditionally have the following operations include lt isl val h gt __isl_give isl_val isl_val_2exp __isl_take isl_val v __isl_give isl_val isl_val_mod __isl_take isl_val v1 __isl_take isl_val v2 __isl_give isl_val isl_val_gcd __isl_take isl_val vl __isl_take isl_val v2 __isl_give isl_val isl_val_gcdext __isl_take isl_val v1 __isl_take isl_val v2 __isl_give isl_val x __isl_give isl_val y The function isl_val_gcdext returns the greatest common divisor g of v1 and v2 as well as two integers x and y such that x v1 y v2 g A value can be read from input using include lt isl val h gt __isl_give isl_val isl_val_read_from_str isl_ctx ctx const char str A value can be printed using include lt isl val h gt __isl_give isl_printer isl_printer_print_val __isl_take isl_printer p __isl_keep isl_val v GMP specific functions These functions are only available if isl has been compiled with GMP support Specific integer and rational values can be created from GMP values using the fol lowing functions include lt isl val_gmp h gt __isl_give isl_val isl_val_int_from_gmp isl_ctx ctx 11 mpz_t Z __isl_give isl_val isl_val_from_gmp isl_ctx ctx const mpz_t n const mpz_t d The numerator and denominator of a rational value can be extracted as GMP values using the following functions include lt isl val_gmp h gt int isl_val_get_num_gmp __isl_keep isl_val v mpz_t z
96. ding row is the unit vector e If on the other hand it 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
97. e 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 4 2 Values An isl_val represents an integer value a rational value or one of three special values infinity negative infinity and NaN Some predefined values can be created using the following functions include lt isl val h gt __isl_give isl_val isl_val_zero isl_ctx ctx __isl_give isl_val isl_val_one isl_ctx ctx __isl_give isl_val isl_val_nan isl_ctx ctx __isl_give isl_val isl_val_infty isl_ctx ctx __isl_give isl_val isl_val_neginfty isl_ctx ctx Specific integer values can be created using the following functions include lt isl val h gt __isl_give isl_val isl_val_int_from_si isl_ctx ctx long i __isl_give isl_val isl_val_int_from_ui isl_ctx ctx unsigned long u __isl_give isl_val isl_val_int_from_chunks isl_ctx ctx size_t n size_t size const void chunks The function isl_val_int_from_chunks constructs an isl_val from the n digits each consisting of size bytes stored at chunks The least significant digit is assumed to be stored first Value objects can be copied and fr
98. e have r s B38 3 lt 0 i e A3f gt r s gt 0 and therefore also A3f gt r s Note that if there are no mixed constraints and if the rational relaxation of A s i e x Q7 Aix c gt 0 has integer vertices then the approximation 146 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
99. e in contains extra el ements then the result does not necessarily contain the composition of these extra elements with powers of Rj 156 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
100. e infinity or infinity if the problem is unbounded and NaN if the problem is 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 53 Compute the minimum or maximum of the given set or output dimension as a function of the parameters and input dimensions but independently of the other set or output dimensions For lexicographic optimization see 1 4 15 e 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 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_ta
101. e therefore needs to be projected out first As soon as the algorithm 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 c
102. e with a constraint added to the context that enforces the expression 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 139 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 t
103. e_val __isl_take isl_multi_aff ma __isl_take isl_val v __isl_give isl_pw_multi_aff isl_pw_multi_aff_scale_val __isl_take isl_pw_multi_aff pma __isl_take isl_val v __isl_give isl_multi_pw_aff isl_multi_pw_aff_scale_val __isl_take isl_multi_pw_aff mpa __isl_take isl_val v __isl_give isl_multi_aff isl_multi_aff_scale_multi_val __isl_take isl_multi_aff ma __isl_take isl_multi_val mv __isl_give isl_pw_multi_aff isl_pw_multi_aff_scale_multi_val __isl_take isl_pw_multi_aff pma __isl_take isl_multi_val mv __isl_give isl_multi_pw_aff isl_multi_pw_aff_scale_multi_val __isl_take isl_multi_pw_aff mpa __isl_take isl_multi_val mv __isl_give isl_union_pw_multi_aff isl_union_pw_multi_aff_scale_multi_val __isl_take isl_union_pw_multi_aff upma __isl_take isl_multi_val mv isl_multi_aff_scale_multi_val scales the elements of ma by the corresponding elements of mv __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 88 __isl_give isl_union_pw_multi_aff isl_union_pw_multi_aff_intersect_domain __isl_take isl_union_pw_multi_aff upma __isl_take isl_union_set uset __isl_give isl_multi_aff isl_multi_aff_lift __isl_take isl_multi_aff maff __isl_give isl_local_space ls __isl_give i
104. ed 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 15 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 the error occurred and can provide a stack 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 4 7 Identifiers Identifiers are used to identify both individual dimensions and tuples of dimensions They consist of an
105. ed if the input union set or relation is known to contain elements in exactly one space __isl_give 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 A zero dimensional basic set can be constructed on a given parameter domain using the following function 29 __isl_give isl_basic_set isl_basic_set_from_params __isl_take isl_basic_set bset __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 __is l_take isl_union_map umap Other sets and relations can be constructed by starting from a universe set or re
106. edule and the inner AST generation should handle the domains that are coscheduled by this initial part of the schedule together For example if an AST is generated for a schedule ALi gt 0 B i gt 0 then the isl_ast_build_set_create_leaf callback described below may get called twice once for each domain Setting this option ensures that the callback is only called once on both domains together ast_build_separation_bounds This option specifies which bounds to use during separation If this option is set to ISL_AST_BUILD_SEPARATION_BOUNDS_IMPLICIT then all possibly implicit bounds on the current dimension will be used during separation If this option is set to ISL_AST_BUILD_SEPARATION_BOUNDS_EXPLICIT then only those bounds that are explicitly available will be used during separation ast_build_scale_strides This option specifies whether the AST generator is allowed to scale down itera tors of strided loops ast_build_allow_else This option specifies whether the AST generator is allowed to construct if state ments with else branches ast_build_allow_or This option specifies whether the AST generator is allowed to construct if con ditions with disjunctions 124 Fine grained Control over AST Generation Besides specifying the constraints on the parameters an isl_ast_build object can be used to control various aspects of the AST generation process The most prominent way of control is through options which c
107. eed using the following functions include lt isl val h gt __isl_give isl_val isl_val_copy __isl_keep isl_val v void isl_val_free __isl_take isl_val v They can be inspected using the following functions include lt isl val h gt isl_ctx isl_val_get_ctx __isl_keep isl_val val long isl_val_get_num_si __isl_keep isl_val v long isl_val_get_den_si __isl_keep isl_val v double isl_val_get_d __isl_keep isl_val v size_t isl_val_n_abs_num_chunks __isl_keep isl_val v size_t size int isl_val_get_abs_num_chunks __isl_keep isl_val v size_t size void chunks isl_val_n_abs_num_chunks returns the number of digits of size bytes needed to store the absolute value of the numerator of v isl_val_get_abs_num_chunks stores these digits at chunks which is assumed to have been preallocated by the caller The least significant digit is stored first Note that isl_val_get_num_si isl_val_get_den_si isl_val_get_d isl_val_n_abs_num_chunks and isl_val_get_abs_num_chunks can only be applied to rational values An isl_val can be modified using the following function include lt isl val h gt __isl_give isl_val isl_val_set_si __isl_take isl_val v long i The following unary properties are defined on isl_vals include lt isl val h gt int isl_val_sgn __isl_keep isl_val v int isl_val_is_zero __isl_keep isl_val v int isl_val_is_one __isl_keep isl_val v int isl_val_is_negone __isl_keep isl_val v
108. ell If the enumeration is performed successfully and to completion then isl_set_foreach_point returns 90 To obtain a single point of a basic set use __isl_give isl_point isl_basic_set_sample_point __isl_take isl_basic_set bset __isl_give isl_point isl_set_sample_point __isl_take isl_set set 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 4 23 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 93 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 differen
109. ements 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 65 __isl_give isl_set isl_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
110. es where the outermost scheduling dimension in each band results in a zero dependence distance over the proximity dependences e schedule split_scaled If this option is set then we try to construct schedules in which the constant term is split off from the linear part if the linear parts of the scheduling rows for all nodes in the graphs have a common non trivial divisor The constant term is then placed in a separate band and the linear part is reduced e schedule_algorithm Selects the scheduling algorithm to be used Available scheduling algorithms are ISL_SCHEDULE_ALGORITHM_ISL and ISL_SCHEDULE_ALGORITHM_FEAUTRIER e schedule_separate_components If at any point the dependence graph contains any weakly connected compo nents then these components are scheduled separately If this option is not set then some iterations of the domains in these components may be scheduled to gether If this option is set then the components are given consecutive schedules 114 1 5 3 AST Generation This section describes the isl functionality for generating ASTs that visit all the ele ments in a domain in an order specified by a schedule In particular given a is1_union_map an AST is generated that visits all the elements in the domain of the isl_union_map according to the lexicographic order of the corresponding image element s If the range of the isl_union_map consists of elements in more than one space then each of these spaces is handled sep
111. estr isl_restriction_none and isl_restriction_empty are special cases of isl_restriction_input isl_restriction_none is essentially equivalent to isl_restriction_input isl_set_universe isl_space_range isl_map_get_space source_map isl_set_universe isl_space_domain isl_map_get_space source_map whereas isl_restriction_empty is essentially equivalent to isl_restriction_input isl_set_empty isl_space_range isl_map_get_space source_map isl_set_universe isl_space_domain isl_map_get_space source_map 1 5 2 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 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 sc
112. et 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_basic_map isl_basic_map_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_domain_product __isl_take isl_union_map umap1 __isl_take isl_union_map umap2 __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 umap1 __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 i
113. et_tuple_id __isl_take isl_pw_multi_aff pma enum isl_dim_type type __isl_take isl_id id __isl_give isl_multi_pw_aff isl_multi_pw_aff_set_dim_name __isl_take isl_multi_pw_aff mpa enum isl_dim_type type unsigned pos const char s __isl_give isl_multi_pw_aff isl_multi_pw_aff_set_tuple_name __isl_take isl_multi_pw_aff mpa enum isl_dim_type type const char s __isl_give isl_multi_aff isl_multi_aff_insert_dims __isl_take isl_multi_aff ma enum isl_dim_type type unsigned first unsigned n __isl_give isl_multi_aff isl_multi_aff_add_dims __isl_take isl_multi_aff ma 86 enum isl_dim_type type unsigned n __isl_give isl_multi_aff isl_multi_aff_drop_dims __isl_take isl_multi_aff maff enum isl_dim_type type unsigned first unsigned n __isl_give isl_pw_multi_aff isl_pw_multi_aff_drop_dims __isl_take isl_pw_multi_aff pma enum isl_dim_type type unsigned first unsigned n __isl_give isl_multi_pw_aff isl_multi_pw_aff_insert_dims __isl_take isl_multi_pw_aff mpa enum isl_dim_type type unsigned first unsigned n __isl_give isl_multi_pw_aff isl_multi_pw_aff_add_dims __isl_take isl_multi_pw_aff mpa enum isl_dim_type type unsigned n 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 maffl __isl_keep isl_multi_aff maff2 int isl_pw_multi_aff_plain_is_equal __isl_keep isl_pw_multi_aff pm
114. f the context tableau is described in Section 2 3 7 2 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 nega
115. fined inductively as R RU Ro R 2 2 Since the transitive closure of a polyhedral relation may no longer be a polyhedral relation Kelly et al 1996c we can in the general case only compute an approxima tion of the transitive closure Whereas Kelly et al 1996c compute underapproxima tions we like Beletska et al 2009 compute overapproximations That is given a relation R we will compute a relation T such that Rt 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
116. for outside users that just want to solve parametric integer programming 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 on
117. ft is not NULL then it is assigned the local space that lies at the basis of the lifting applied include lt isl aff h gt __isl_give isl_multi_aff isl_multi_aff_pullback_multi_aff __isl_take isl_multi_aff mal __isl_take isl_multi_aff ma2 __isl_give isl_pw_multi_aff isl_pw_multi_aff_pullback_multi_aff __isl_take isl_pw_multi_aff pma 90 __isl_take isl_multi_aff ma __isl_give isl_pw_multi_aff isl_pw_multi_aff_pullback_pw_multi_aff __isl_take isl_pw_multi_aff pmal __isl_take isl_pw_multi_aff pma2 The function isl_multi_aff_pullback_multi_aff precomposes mal by ma2 In other words ma2 is plugged into mal __isl_give isl_set isl_multi_aff_lex_le_set __isl_take isl_multi_aff mal __isl_take isl_multi_aff ma2 __isl_give isl_set isl_multi_aff_lex_ge_set __isl_take isl_multi_aff mal __isl_take isl_multi_aff ma2 The function isl_multi_aff_lex_le_set returns a set containing those elements in the shared domain space where mal is lexicographically smaller than or equal to ma2 An expression can be read from input using include lt isl aff h gt __isl_give isl_multi_aff isl_multi_aff_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 __isl_give isl_union_pw_multi_aff isl_union_pw_multi_aff_read_from_str isl_ctx ctx const char str An expression can be printed using include lt isl aff h gt
118. he result Changes since isl 0 09 e The schedule_split_parallel option has been replaced by the schedule_split_scaled option e The first argument of isl_pw_aff_cond is now an isl_pw_aff instead of an isl_set A call isl_pw_aff_cond a b c can be replaced by isl_pw_aff_cond isl_set_indicator_function a b c Changes since is 0 10 e The functions isl_set_dim_has_lower_bound and isl_set_dim_has_upper_bound have been renamed to isl_set_dim_has_any_lower_bound and is l_set_dim_has_any_upper_bound The new isl_set_dim_has_lower_bound and isl_set_dim_has_upper_bound have slightly different meanings 1 2 License isl is released under the MIT license Permission is hereby granted free of charge to any person obtaining a copy of this software and associated documentation files the Software to deal in the Software without restriction including without limitation the rights to use copy modify merge publish distribute sublicense and or sell copies of the Software and to permit persons to whom the Software is furnished to do so subject to the following conditions The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software THE SOFTWARE IS PROVIDED AS IS WITHOUT WARRANTY OF ANY KIND EXPRESS OR IMPLIED INCLUDING BUT NOT LIMITED TO THE WAR RANTIES OF MERCHANTABILITY FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT IN NO EVENT SHALL THE AUTH
119. he start when no points have been collected yet one or two feasibility 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
120. hedule 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 mapping from the domains to the scheduled space can be obtained from an isl_schedule using the following function 110 __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 individual bands can be visited in depth first post order using the following function include lt isl schedule h gt int isl_schedule_foreach_band __isl_keep isl_schedule sched int fn __isl_keep isl_band band void user void user The list can be manipulated as explained in 1 4 16 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
121. hould be considered atomic That is the AST generator will make sure that any given domain space will only appear in a single loop at the specified level Consider the following schedule a i gt i 0 lt i lt 10 bli gt i 1 0 lt i lt 10 If the following option is specified i gt separate x then the following AST will be generated a0 for int c 1 c lt 9 cO 1 f a cO b cO 1 b 9 127 If on the other hand the following option is specified i gt atomic x then the following AST will be generated for int c 0 cO lt 10 c 1 if c0 lt 9 a cQ if c0 gt 1 b cO 1 If neither atomic nor separate is specified then the AST generator may pro duce either of these two results or some intermediate form unroll This is a single dimensional space representing the schedule dimension s that should be completely unrolled To obtain a partial unrolling the user should apply an additional strip mining to the schedule and fully unroll the inner loop Additional control is available through the following functions include lt isl ast_build h gt __isl_give isl_ast_build isl_ast_build_set_iterators __isl_take isl_ast_build control __isl_take isl_id_list iterators The function isl_ast_build_set_iterators allows the user to specify a list of iterator isl_ids to be used as iterators If the input schedule is i
122. i_aff upma __isl_give isl_multi_pw_aff isl_multi_pw_aff_copy __isl_keep isl_multi_pw_aff mpa void isl_multi_pw_aff_free __isl_take isl_multi_pw_aff mpa 84 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 isl_ctx isl_union_pw_multi_aff_get_ctx __isl_keep isl_union_pw_multi_aff upma isl_ctx isl_multi_pw_aff_get_ctx __isl_keep isl_multi_pw_aff mpa 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 unsigned isl_multi_pw_aff_dim __isl_keep isl_multi_pw_aff mpa 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 __isl_give isl_pw_aff isl_multi_pw_aff_get_pw_aff __isl_keep isl_multi_pw_aff mpa 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_give isl_id isl_pw_multi_aff_get_dim_id __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 int isl_pw_multi_aff_has_tuple_name __isl_keep
123. igned 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 58 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 input or output space of a set or a relation as this removes the name and the internal structure of the space However the above functions can be useful to add new parameters assuming isl_set_align_params and isl_map_align_params are not sufficient 1 4 15 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 _
124. ion with a domain that is the union of those of pwaff1 and pwaff2 and such that on each cell the quasi 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 82 1 4 21 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 Similarly an is1_multi_pw_aff object represents a sequence of zero or more piecewise affine expressions An isl_multi_aff can be constructed from a single isl_aff oranisl_aff_list using the following functions Similarly for is _multi_pw_aff include lt isl aff h gt __isl_give isl_multi_aff isl_multi_aff_from_aff __isl_take isl_aff aff __isl_give isl_multi_pw_aff isl_multi_pw_aff_from_pw_aff __isl_take isl_pw_aff pa __isl_give isl_multi_aff isl_multi_aff_from_aff_list __i
125. isl_dim_type type unsigned pos int value __isl_give isl_set isl_set_lower_bound __isl_take isl_set set enum isl_dim_type type unsigned pos isl_int value __isl_give isl_set isl_set_lower_bound_si 47 __isl_take isl_set set enum isl_dim_type type unsigned pos int value __isl_give isl_set isl_set_lower_bound_val __isl_take isl_set set enum isl_dim_type type unsigned pos __isl_take isl_val value __isl_give isl_map isl_map_lower_bound_si __isl_take isl_map map enum isl_dim_type type unsigned pos int value __isl_give isl_set isl_set_upper_bound __isl_take isl_set set enum isl_dim_type type unsigned pos isl_int value __isl_give isl_set isl_set_upper_bound_si __isl_take isl_set set enum isl_dim_type type unsigned pos int value __isl_give isl_set isl_set_upper_bound_val __isl_take isl_set set enum isl_dim_type type unsigned pos __isl_take isl_val value __isl_give isl_map isl_map_upper_bound_si __isl_take isl_map map enum isl_dim_type type unsigned pos int value Intersect the set or relation with the half space where the given dimension has a value bounded by the fixed given integer value __isl_give isl_set isl_set_equate __isl_take isl_set enum isl_dim_type typel int posl enum isl_dim_type type2 int pos2 __isl_give isl_basic_map isl_basic_map_equate __isl_take isl_basic_map bmap enum isl_dim_type typel int posl enum isl_dim
126. 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 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 39 enum isl_dim_type type unsigned pos int isl_set_has_dim_name __isl_keep isl_set set 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 int isl_map_has_dim_name __isl_keep isl_map map 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
127. ke 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_fixed_power __isl_take isl_map map isl_int exp __isl_give isl_map isl_map_fixed_power_val __isl_take isl_map map __isl_take isl_val exp __isl_give isl_union_map isl_union_map_fixed_power __isl_take isl_union_map umap isl_int exp __isl_give isl_union_map isl_union_map_fixed_power_val __isl_take isl_union_map umap __isl_take isl_val exp Compute the given power of map where exp is assumed to be non zero If the exponent exp is negative then the exp th power of the inverse of map is computed 54 __isl_give isl_map isl_map_power __isl_take isl_map map int exact __isl_give isl_union_map isl_union_map_power __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
128. l 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_qpolynomial_fold isl_qpolynomial_fold_scale_val __isl_take isl_qpolynomial_fold fold __isl_take isl_val v __isl_give isl_pw_qpolynomial_fold isl_pw_qpolynomial_fold_scale_val __isl_take isl_pw_qpolynomial_fold pwf __isl_take isl_val v __isl_give isl_union_pw_qpolynomial_fold isl_union_pw_qpolynomial_fold_scale_val __isl_take isl_union_pw_qpolynomial_fold upwf __isl_take isl_val 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_fo
129. l_ast_node_for isl_ast_node_if isl_ast_node_block or isl_ast_node_user An isl_ast_node_for represents a for node An isl_ast_node_if represents an if node An isl_ast_node_block represents a compound node An 115 isl_ast_node_user represents an expression statement An expression statement typ ically corresponds to a domain element i e one of the elements that is visited by the AST Each type of node has its own additional properties include lt isl ast h gt __isl_give isl_ast_expr isl_ast_node_for_get_iterator __isl_keep isl_ast_node node __isl_give isl_ast_expr isl_ast_node_for_get_init __isl_keep isl_ast_node node __isl_give isl_ast_expr isl_ast_node_for_get_cond __isl_keep isl_ast_node node __isl_give isl_ast_expr isl_ast_node_for_get_inc __isl_keep isl_ast_node node __isl_give isl_ast_node isl_ast_node_for_get_body __isl_keep isl_ast_node node int isl_ast_node_for_is_degenerate __isl_keep isl_ast_node node An isl_ast_for is considered degenerate if it is known to execute exactly once include lt isl ast h gt __isl_give isl_ast_expr isl_ast_node_if_get_cond __isl_keep isl_ast_node node __isl_give isl_ast_node isl_ast_node_if_get_then __isl_keep isl_ast_node node int isl_ast_node_if_has_else __isl_keep isl_ast_node node __isl_give isl_ast_node isl_ast_node_if_get_else __isl_keep isl_ast_node node __isl_give isl_ast_node_list isl_ast_node_block_get
130. l_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 4 11 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 __isl_take isl_space space __isl_give isl_union_map isl_union_map_empty __isl_take isl_space space For isl_union_sets and is l_union_maps the space is only used to specify the parameters e Universe sets and relations 27 __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 __isl_take isl_space space __isl_give isl_map isl_map_universe __isl_take is
131. l_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 __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 28 __isl_take isl_space space unsigned n __isl_give isl_map isl_map_lex_le_first __isl_take isl_space space unsigned n __isl_give isl_map isl_map_lex_gt_first __i
132. ld 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 val h gt __isl_give isl_space isl_multi_val_get_space __isl_keep isl_multi_val mv 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_domain_space __isl_keep isl_multi_aff maff __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 __isl_give isl_space isl_union_pw_multi_aff_get_space __isl_keep isl_union_pw_multi_aff upma __isl_give isl_space isl_multi_pw_aff_get_domain_space __isl_keep isl_multi_pw_aff mpa __isl_give isl_space isl_multi_pw_aff_get_space __isl_keep isl_multi_pw_aff mpa 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
133. ld_eval __isl_take isl_pw_qpolynomial_fold pwf __isl_take isl_point pnt __isl_give isl_qpolynomial isl_union_pw_qpolynomial_fold_eval __isl_take isl_union_pw_qpolynomial_fold upwf __isl_take isl_point pnt 103 __isl_give isl_pw_qpolynomial_fold isl_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
134. lude Rig Ro ie the dotted arrow in the figure The transitive closure 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 155 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 applie
135. lynomial_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 __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 upwaqp 99 __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_union_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_qpoly
136. lynomials 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 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 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 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 pwaqp __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 18 __isl_give isl_space isl_pw_qpolynomial_fold_get_space __isl_keep isl_pw_qpolynomial_fo
137. 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 The second argument to the params functions needs to be a parametric basic set For the other functions a parametric set for either argument is only allowed if the other argument is a parametric set as well Union __isl_give isl_set isl_basic_set_union __isl_take isl_basic_set bset1 __isl_take isl_basic_set bset2 __isl_give isl_map isl_basic_map_union __isl_take isl_basic_map bmap1 __isl_take isl_basic_map bmap2 __isl_give isl_set isl_set_union __isl_take isl_set setl __isl_take isl_set set2 __isl_give isl_map isl_map_union __isl_take isl_map map1 __isl_take isl_map map2 60 __isl_give isl_union_set isl_union_set_union __isl_take isl_union_set usetl __isl_take isl_union_set uset2 __isl_give isl_union_map isl_union_map_union e Set difference __isl_take isl_union_map umap1 __isl_take isl_union_map umap2 __isl_give isl_set isl_set_subtract __isl_take isl_set setl __isl_take __isl_give isl_map __isl_take __isl_take __isl_give isl_map __isl_take __isl_take __isl
138. mpletely different The library is by no means complete and some fairly basic functionality is still missing Still even in its current form the library has been successfully used as a backend polyhedral library for the polyhedral scanner CLooG and as part of an equiva lence checker of static affine programs For bug reports feature requests and questions visit the the discussion group at http groups google com group 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_ide
139. n affine expression by another the second expression needs to be a constant isl_pw_aff_tdiv_q computes the quotient of an integer di vision with rounding towards zero isl_pw_aff_tdiv_r computes the corresponding remainder include lt isl aff h gt __isl_give isl_aff isl_aff_pullback_multi_aff __isl_take isl_aff aff __isl_take isl_multi_aff ma __isl_give isl_pw_aff isl_pw_aff_pullback_multi_aff __isl_take isl_pw_aff pa __isl_take isl_multi_aff ma __isl_give isl_pw_aff isl_pw_aff_pullback_pw_multi_aff __isl_take isl_pw_aff pa __isl_take isl_pw_multi_aff pma These functions precompose the input expression by the given isl_multi_aff or isl_pw_multi_aff In other words the isl_multi_aff or isl_pw_multi_aff is plugged into the piecewise affine expression Objects of type isl_multi_aff are described in 1 4 21 include lt isl aff h gt __isl_give isl_basic_set isl_aff_zero_basic_set __isl_take isl_aff aff __isl_give isl_basic_set isl_aff_neg_basic_set __isl_take isl_aff aff __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_pw_aff_eq_set __isl_take isl_pw_aff pwaff1 __isl_take isl_pw_aff pwaff2 __isl_give isl_set isl_pw_aff_ne_set 80 __isl_take __isl_take __isl_give isl_set __isl_take __isl_take __isl_give i
140. ned off then the AST generation will produce ASTs that may only contain isl_ast_op_fdiv_q operators but no isl_ast_op_pdiv_q or isl_ast_op_pdiv_r operators If this options is turned on then is1 will try to convert some of the isl_ast_op_fdiv_q operators to expressions containing isl_ast_op_pdiv_q or isl_ast_op_pdiv_r operators ast_build_exploit_nested_bounds Simplify conditions based on bounds of nested for loops In particular remove conditions that are implied by the fact that one or more nested loops have at least one iteration meaning that the upper bound is at least as large as the lower bound For example when this option is turned off AST generation for the schedule N M gt ALi j gt i j lt i lt N and 0 lt j lt M produces 123 if gt 0 for int c 0 cO lt N c0 1 for int cl 0 cl lt M c1 1 ACcO c1 When the option is turned on the following AST is generated for int c 0 cO lt N cO 1 for int cl 0 cl lt M c1 1 ACcO c1 ast_build_group coscheduled If two domain elements are assigned the same schedule point then they may be executed in any order and they may even appear in different loops If this options is set then the AST generator will make sure that coscheduled domain elements do not appear in separate parts of the AST This is useful in case of nested AST generation if the outer AST generation is given only part of a sch
141. nion_map umap __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 45 __isl_give isl_union_set isl_union_map_domain __isl_take isl_union_map umap __isl_give isl_union_set isl_union_map_range __isl_take isl_union_map umap __isl_give isl_basic_map isl_basic_map_domain_map __isl_take isl
142. nion_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 56 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 Currying __isl_give isl_basic_map isl_basic_map_curry __isl_take isl_basic_map bmap __isl_give isl_basic_map isl_basic_map_uncurry __isl_take isl_basic_map bmap __isl_give isl_map isl_map_curry __isl_take isl_map map __isl_give isl_map isl_map_uncurry __isl_take isl_map map __isl_give isl_union_map isl_union_map_curry __isl_take isl_union_map umap __isl_give isl_union_map isl_union_map_uncurry __isl_take isl_union_map umap Given a relation with a nested relation for domain the curry functions move the range of the nested relation out of the domain and use it as the domain of a nested relation in the range with the original range as range of this nes
143. njective then the num ber of elements in this list should be as large as the dimension of the schedule space but no direct correspondence should be assumed between dimensions and elements If the input schedule is not injective then an additional number of isl_ids equal to the largest dimension of the input domains may be required If the number of provided isl_ids is insufficient then additional names are automatically generated include lt isl ast_build h gt __isl_give isl_ast_build isl_ast_build_set_create_leaf __isl_take isl_ast_build control __isl_give isl_ast_node fn __isl_take isl_ast_build build void user void user 128 The isl_ast_build_set_create_leaf function allows for the specification of a callback that should be called whenever the AST generator arrives at an element of the schedule domain The callback should return an AST node that should be inserted at the corresponding position of the AST The default action when the callback is not set is to continue generating parts of the AST to scan all the domain elements associated to the schedule domain element and to insert user nodes calling the domain element for each of them The build argument contains the current state of the isl_ast_build To ease nested AST generation see 1 5 3 all control information that is specific to the current AST generation such as the options and the callbacks has been removed from this isl_ast_build The callback w
144. nomial_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 __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 upwap __isl_take isl_union_set context The gist operation applies the gist operation to each of the cells in the domain of the input piecewise quasipolynomial The context is also exploited to simplify the quasipolynomials associated to each cell __isl_give isl_pw_qpolynomial isl_pw_qpolynomial_to_polynomial 100 __isl_take isl_pw_qpolynomial pwqp int sign __isl_give isl_union_p
145. nter isl_ast_node_for_print __isl_keep isl_ast_node node __isl_take isl_printer p __isl_take isl_ast_print_options options __isl_give isl_printer isl_ast_node_if_print __isl_keep isl_ast_node node __isl_take isl_printer p __isl_take isl_ast_print_options options While printing an is _ast_node in ISL_FORMAT_C isl may print out an AST that makes use of macros such as floord min and max isl_ast_op_type_print_macro prints out the macro corresponding to a specific isl_ast_op_type isl_ast_node_print_macros scans the isl_ast_node for expressions where these macros would be used and prints out the required macro definitions Essentially isl_ast_ node_print_macros calls isl_ast_node_foreach_ast_op_type with isl_ast_op_type_print_macro as func tion argument isl_ast_node_print isl_ast_node_for_print and isl_ast node_if_print print an isl_ast_node in ISL_FORMAT_C but allow for some extra control through an isl_ast_print_options object This object can be created using the following func tions include lt isl ast h gt __isl_give isl_ast_print_options isl_ast_print_options_alloc isl_ctx ctx __isl_give isl_ast_print_options isl_ast_print_options_copy __isl_keep isl_ast_print_options options void isl_ast_print_options_free __isl_take isl_ast_print_options options __isl_give isl_ast_print_options isl_ast_print_options_set_print_user __isl_take isl_ast_print_options options __isl_give i
146. nternal 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 __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 e 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_u
147. ntity 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 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_p
148. nts then the entire result is marked inexact and the exactness check is skipped on the components that still need to be handled It should be noted that is only valid for exact transitive closures If over approximations are computed in the right hand side then the result will still be an overapproximation of the left hand side but this result may not be transitively closed If we only separate components based on the condition R o R 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 151 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
149. o 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 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 Quasipolynomials for an explanation of the difference between these two functions To iterate over all quasipolynomials in a reduction use 102 int isl_qpolynomial_fold_foreach_qpolynomial __isl_keep isl_qpolynomial_fold fold int fn __isl_take isl_qpolynomia
150. oint 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 pnt void isl_point_free __isl_take isl_point pnt A singleton set can be created from a point using __isl_give isl_basic_set isl_basic_set_from_point __isl_take isl_point pnt __isl_give isl_set isl_set_from_point __isl_take isl_point pnt and a box can be created from two opposite extremal points using 92 __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 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 w
151. ollowing 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 1 4 20 __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 36 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_equalities_matrix __isl_keep isl_basic_map bmap enum isl_dim_type c1 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 c1 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 dictate the order in which different kinds of vari ables appear in the resulting matrix and should be a permutation of isl_dim
152. on and may also prevent fusing of unrelated dimensions A value of 1 means that this option does not introduce bounds on the variable or parameter coefficients 113 e 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 e schedule_fuse This option controls the level of fusion If this option is set to ISL_SCHEDULE_FUSE_MIN then loops in the resulting schedule will be distributed as much as possible If this option is set to ISL_SCHEDULE_FUSE_MAX then isl will try to fuse loops in the resulting schedule e 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 Note that if the schedule_fuse option is set to ISL_SCHEDULE_FUSE_MIN then bands will be split as early as possible even if there is no need The schedule_maximize_band_depth option therefore has no effect in this case e schedule_outer_zero_distance If this option is set then we try to construct schedul
153. on 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 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 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
154. onsider instead R n x y gt nj 1 x 1 n y n gt 2 then AR 0 1 y y lt 1 149 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
155. onstraint equating the affine expression to zero or an inequality constraint enforcing the affine expression to be non negative can be con structed using __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_aff 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 74 __isl_keep isl_pw_aff pa enum isl_dim_type type unsigned pos __isl_give isl_id isl_pw_aff_get_tuple_id __isl_keep isl_pw_aff pa enum isl_dim_type type int isl_aff_get_constant __isl_keep isl_aff aff isl_int v __isl_give isl_val isl_aff_get_constant_val __isl_keep isl_aff aff int isl_aff_get_coefficient __isl_keep isl_aff aff enum isl_dim_type type int pos isl_int v __isl_give isl_val isl_aff
156. options_set_coalesce_bounded_wrapping isl_ctx ctx int val int isl_options_get_coalesce_bounded_wrapping isl_ctx ctx 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 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 __isl_take isl_map map 50 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
157. ould typically return the result of a nested AST generation or a user defined node created using the following function include lt isl ast h gt __isl_give isl_ast_node isl_ast_node_alloc_user __isl_take isl_ast_expr expr include lt isl ast_build h gt __isl_give isl_ast_build isl_ast_build_set_at_each_domain __isl_take isl_ast_build build __isl_give isl_ast_node fn __isl_take isl_ast_node node __isl_keep isl_ast_build build void user void user __isl_give isl_ast_build isl_ast_build_set_before_each_for __isl_take isl_ast_build build __isl_give isl_id fn __isl_keep isl_ast_build build void user void user __isl_give isl_ast_build isl_ast_build_set_after_each_for __isl_take isl_ast_build build __isl_give isl_ast_node fn __isl_take isl_ast_node node __isl_keep isl_ast_build build void user void user The callback set by isl_ast_build_set_at_each_domain will be called for each domain AST node The callbacks set by isl_ast_build_set_before_each_for and isl_ast_build_set_after_each_for will be called for each for AST node The first will be called in depth first pre order while the second will be called in depth first post order Since isl_ast_build_set_before_each_for is called before the for node is actually constructed it is only passed an isl_ast_build The returned isl_id will be added as an annotation using isl_ast_node_set_annotation to the construc
158. p is wrapping then the bound is computed over the range of the wrapped relation The domain of the wrapped relation becomes the domain of the result A piecewise quasipolynomial reduction can be copied or freed using the following functions __isl_give isl_qpolynomial_fold isl_qpolynomial_fold_copy __isl_keep isl_qpolynomial_fold fold __isl_give isl_pw_qpolynomial_fold isl_pw_qpolynomial_fold_copy __isl_keep isl_pw_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 101 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_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 For isl_printer_print_union_pw_qpolynomial_fold output format of the printer needs t
159. p isl_ast_node node void isl_ast_node_free __isl_take isl_ast_node node AST expressions can be copied and freed using the following functions include lt isl ast h gt __isl_give isl_ast_expr isl_ast_expr_copy __isl_keep isl_ast_expr expr void isl_ast_expr_free __isl_take isl_ast_expr expr New AST expressions can be created either directly or within the context of an isl_ast_build include lt isl ast h gt __isl_give isl_ast_expr isl_ast_expr_from_val __isl_take isl_val v __isl_give isl_ast_expr isl_ast_expr_from_id __isl_take isl_id id __isl_give isl_ast_expr isl_ast_expr_neg __isl_take isl_ast_expr expr __isl_give isl_ast_expr isl_ast_expr_add 119 __isl_take isl_ast_expr expr1 __isl_take isl_ast_expr expr2 __isl_give isl_ast_expr isl_ast_expr_sub __isl_take isl_ast_expr expr1 __isl_take isl_ast_expr expr2 __isl_give isl_ast_expr isl_ast_expr_mul __isl_take isl_ast_expr expr1 __isl_take isl_ast_expr expr2 __isl_give isl_ast_expr isl_ast_expr_div __isl_take isl_ast_expr expr1 __isl_take isl_ast_expr expr2 __isl_give isl_ast_expr isl_ast_expr_and __isl_take isl_ast_expr expr1 __isl_take isl_ast_expr expr2 __isl_give isl_ast_expr isl_ast_expr_or __isl_take isl_ast_expr expr1 __isl_take isl_ast_expr expr2 include lt isl ast_build h gt __isl_give isl_ast_expr isl_ast_build_expr_from_pw_aff __isl_keep isl_ast_build build __isl_take isl
160. p 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_alloc __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 95 __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 __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 pwqp
161. 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 24 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 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
162. pos Note that these functions return true even if there is a bound on the dimension on only some of the basic sets of set To check if they have a bound for all of the basic sets in set use the following functions instead 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 __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 isl_basic_set set const char s int isl_set_has_tuple_name __isl_keep isl_set set const char
163. pow __isl_take isl_qpolynomial qp unsigned exponent __isl_give isl_pw_qpolynomial isl_pw_qpolynomial_fix_val __isl_take isl_pw_qpolynomial pwqp enum isl_dim_type type unsigned n __isl_take isl_val v __isl_give isl_pw_qpolynomial isl_pw_qpolynomial_scale_val __isl_take isl_pw_qpolynomial pwqp __isl_take isl_val v __isl_give isl_pw_qpolynomial isl_pw_qpolynomial_add __isl_take isl_pw_qpolynomial pwqp1 __isl_take isl_pw_qpolynomial pwqp2 98 __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 __isl_take isl_pw_qpolynomial pwqp unsigned exponent __isl_give isl_union_pw_qpolynomial isl_union_pw_qpolynomial_scale_val __isl_take isl_union_pw_qpolynomial upwap __isl_take isl_val v __isl_give isl_union_pw_qpolynomial isl_union_pw_qpolynomial_add __isl_take isl_union_pw_qpolynomial upwqp1 __isl_take isl_union_pw_qpolynomial upwqp2 __isl_give isl_union_pw_qpolynomial isl_union_pw_qpo
164. pproximation of the power 2 5 5 Partitioning the domains and ranges of R The algorithm of assumes that the input relation R can be treated as a union of translations This is a reasonable assumption if R maps elements of a given abstract domain to the same domain However if R is a union of relations that map between different domains then this assumption no longer holds In particular when an entire dependence graph is encoded in a single relation as is done by e g 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 153 Algorithm 1 The modified Floyd Warshall algorithm of Kelly et al 1996c Input
165. ptimization Ph D thesis Uni versit Louis Pasteur 138 Meister B and S Verdoolaege 2008 April 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 138 Nelson C G 1980 Techniques for program verification Ph D thesis Stanford University Stanford CA USA 134 Schrijver A 1986 Theory of Linear and Integer Programming John Wiley amp Sons 147 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 142 159 Tarjan R 1972 Depth first search and linear graph algorithms SIAM Journal on Computing 1 2 146 160 151 Verdoolaege S 2006 barvinok version 0 22 Available from http freshmeat net projects barvinok 134 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 143 Verdoolaege S K Beyls M Bruynooghe and F Catthoor 2005 Experiences with enumeration of integer projections of parametric polytopes In R Bodik E
166. put e Feasibility 52 __isl_give isl_basic_set isl_basic_set_sample __isl_take isl_basic_set bset __isl_give isl_basic_set isl_set_sample __isl_take isl_set set __isl_give isl_basic_map isl_basic_map_sample __isl_take isl_basic_map bmap __isl_give isl_basic_map isl_map_sample __isl_take isl_map map If the input basic set or relation is non empty then return a singleton subset of the input Otherwise return an empty set 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 __isl_give isl_val isl_basic_set_max_val __isl_keep isl_basic_set bset __isl_keep isl_aff obj enum isl_lp_result isl_set_min __isl_keep isl_set set __isl_keep isl_aff obj isl_int opt __isl_give isl_val isl_set_min_val __isl_keep isl_set set __isl_keep isl_aff obj enum isl_lp_result isl_set_max __isl_keep isl_set set __isl_keep isl_aff obj isl_int opt __isl_give isl_val isl_set_max_val __isl_keep isl_set set __isl_keep isl_aff obj 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 in case of an isl_lp_result If the result is an isl_val then the result is NULL in case of an error the optimal value in case there is one negativ
167. pute 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 quantified variables but that the dimensions of the sets may be different for different invocations of fn The constant term of a quasipolynomial can be extracted using __isl_give isl_val isl_qpolynomial_get_constant_val __isl_keep isl_qpolynomial qp To iterate over all terms in 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 __isl_give isl_val isl_term_get_coefficient_val __isl_keep isl_term term 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
168. rate separate loops for domain elements that are assigned different classes If only some of the elements are assigned a class then those elements that are not assigned any class will be treated as belonging to a class that is separate from the explicitly assigned classes The typical use case for this option is to separate full tiles from partial tiles The other options described below are applied after the separation into classes As an example consider the separation into full and partial tiles of a tiling of a triangular domain Take for example the domain ALi j 0 lt i j and i j lt 100 and a tiling into tiles of 10 by 10 The input to the AST generator is then the schedule ALi j gt CLi 10 j 10 i j 0 lt i j and i j lt 100 125 Without any options the following AST is generated for int c 0 cO lt 10 cO 1 for int cl 0 cl lt c0 10 c1 1 for int c2 10 cQ c2 lt min 10 c1 100 10 cO 9 c2 1 for int c3 10 cl c3 lt min 10 c1 9 c2 100 c3 1 ACc2 c3 Separation into full and partial tiles can be obtained by assigning a class say O to the full tiles The full tiles are represented by those values of the first and second schedule dimensions for which there are values of the third and fourth dimensions to cover an entire tile That is we need to specify the following option a b c d gt separation_class 0 gt 0
169. re are any explicit equalities in the input description PipLib 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 137 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 conte
170. relation We will therefore need to make some approximations As a first approximations we 144 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 se
171. romising results in manual applications Let us first consider what 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 solu
172. rough Rj i e R RI UR U R3 OR 2 11 We can therefore compute 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 compone
173. s is treated as an error 108 Interaction with Dependence Analysis During the dependence analysis we frequently need to perform the following opera tion Given a relation between sink iterations and potential source iterations from a particular source domain what is the last potential source iteration corresponding to each sink iteration It can sometimes be convenient to adjust the set of potential source iterations before or after each such operation The prototypical example is fuzzy array dataflow analysis where we need to analyze if based on data dependent constraints the sink iteration can ever be executed without one or more of the corresponding po tential source iterations being executed If so we can introduce extra parameters and select an unknown but fixed source iteration from the potential source iterations To be able to perform such manipulations isl provides the following function include lt isl flow h gt typedef __isl_give isl_restriction isl_access_restrict __isl_keep isl_map source_map __isl_keep isl_set sink void source_user void user __isl_give isl_access_info isl_access_info_set_restrict __isl_take isl_access_info acc isl_access_restrict fn void user The function isl_access_info_set_restrict should be called before calling isl_access_info_compute_flow and registers a callback function that will be called any time isl is about to compute the last potential source The first arg
174. s of the 3rd International Conference on Combinatorial Optimization and Applications Berlin Heidelberg pp 98 109 Springer Verlag Boulet P and X Redon 1998 Communication pre evaluation in HPF In EU ROPAR 9S Volume 1470 of Lecture Notes in Computer Science pp 263 272 Springer Verlag Berlin 134 Bygde S 2010 March Static WCET analysis based on abstract interpretation and counting of elements Licentiate thesis 138 142 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 141 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 134 De Smet S 2010 April personal communication 147 Detlefs D G Nelson and J B Saxe 2005 Simplify a theorem prover for pro gram checking J ACM 52 3 365 473 134 158 Feautrier P 1988 Parametric integer programming RAIRO Recherche Op rationnelle 22 3 243 268 134 Feautrier P 1991 Dataflow analysis of array and scalar references
175. s taken to be an arbitrarily large positive number Instead 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 unbo
176. 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 unsigned pos __isl_take isl_id id 19 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 int isl_space_has_dim_name __isl_keep isl_space space enum isl_dim_type type unsigned pos __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 isl_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 dimen
177. sion 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 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 20 enum isl_dim_type type const char s int isl_space_has_tuple_name __isl_keep isl_space space enum isl_dim_type type const char isl_space_get_tuple_name __isl_keep isl_space space enum isl_dim_type type 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 Sp
178. sl_keep isl_set a __isl_keep isl_set b void user void user 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 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 index int isl_set_list_foreach __isl_keep isl_set_list list int fn __isl_take isl_set el void user void user int isl_set_list_foreach_scc __isl_keep isl_set_list list int follows __isl_keep isl_set a __isl_keep isl_set b void user 68 void follows_user int fn __isl_take isl_set el void user void fn_user The function isl_set_list_foreach _scc calls fn on each of the strongly con nected components of the graph with as vertices the elements of list and a directed edge from vertex b to vertex a iff follows a b returns 1 The callbacks follows and fn should return 1 on error 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 4 17 Multiple Values An isl_multi_val object represents a sequence of zero or more values living in
179. sl_printer print_user __isl_take isl_printer p 121 __isl_take isl_ast_print_options options __isl_keep isl_ast_node node void user void user __isl_give isl_ast_print_options isl_ ast_print_options_set_print_for __isl_take isl_ast_print_options options __isl_give isl_printer print_for __isl_take isl_printer p __isl_take isl_ast_print_options options __isl_keep isl_ast_node node void user void user The callback set by isl_ast_print_options_set_print_user is called when ever a node of type isl_ast_node_user needs to be printed The callback set by isl_ast_print_options_set_print_for is called whenever a node of type isl_ast_node_for needs to be printed Note that isl_ast_node_for_print will not call the callback set by isl_ast_print_options_set_print_for on the node on which isl_ast_node_for print is called but only on nested nodes of type isl_ast_node_for It is therefore safe to call isl_ast_node_for_print from within the callback set by isl_ast_print_options_set_print_for The following option determines the type to be used for iterators while printing the AST int isl_options_set_ast_iterator_type isl_ctx ctx const char val const char isl_options_get_ast_iterator_type Options isl_ctx ctx include lt isl ast_build h gt int int int int int int int int int isl_options_set_ast_build_atomic_upper_bound isl_ctx ctx int val
180. sl_pw_aff_list list2 isl_pw_aff_list_lt_set isl_pw_aff_list listl isl_pw_aff_list list2 isl_pw_aff_list_ge_set isl_pw_aff_list listl isl_pw_aff_list list2 isl_pw_aff_list_gt_set isl_pw_aff_list listl isl_pw_aff_list list2 include lt isl aff h gt __isl_give isl_set __isl_take __isl_give isl_set __isl_take isl_pw_aff_nonneg_set isl_pw_aff pwaff isl_pw_aff_zero_set isl_pw_aff pwaff 81 __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_pw_aff 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 where cond is non zero and equal to pwaff_false for elements where cond is zero include lt isl aff h gt __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 s
181. sl_pw_multi_aff isl_pw_multi_aff_coalesce __isl_take isl_pw_multi_aff pma __isl_give isl_multi_aff isl_multi_aff_align_params __isl_take isl_multi_aff multi __isl_take isl_space model __isl_give isl_pw_multi_aff isl_pw_multi_aff_align_params __isl_take isl_pw_multi_aff pma __isl_take isl_space model __isl_give isl_pw_multi_aff isl_pw_multi_aff_project_domain_on_params __isl_take isl_pw_multi_aff pma __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 __isl_give isl_set isl_pw_multi_aff_domain __isl_take isl_pw_multi_aff pma __isl_give isl_union_set isl_union_pw_multi_aff_domain __isl_take isl_union_pw_multi_aff upma __isl_give isl_multi_aff isl_multi_aff_range_splice __isl_take isl_multi_aff mal unsigned pos __isl_take isl_multi_aff ma2 __isl_give isl_multi_aff isl_multi_aff_splice __isl_take isl_multi_aff mal unsigned in_pos unsigned out_pos __isl_take isl_multi_aff ma2 __isl_give isl_multi_aff isl_multi_aff_range_product __isl_take isl_multi_aff mal __isl_take isl
182. sl_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 63 __isl_give isl_map __isl_take __isl_take __isl_give isl_map __isl_take __isl_take isl_map_flat_domain_product isl_map map1 isl_map map2 isl_map_flat_range_product isl_map map1 isl_map map2 __isl_give isl_union_map isl_union_map_flat_range_product __isl_take __isl_take isl_union_map umap1 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 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
183. sl_set __isl_take __isl_take __isl_give isl_set __isl_take __isl_take __isl_give isl_set __isl_take __isl_take __isl_give isl_set __isl_take __isl_take __isl_give isl_set __isl_take __isl_take __isl_give isl_set __isl_take __isl_take __isl_give isl_set __isl_take __isl_take __isl_give isl_set __isl_take __isl_take __isl_give isl_set __isl_take __isl_take The function isl_affmneg_basic_set returns a basic set containing those ele ments in the domain space of aff where aff is negative 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 af 2 The function isl_pw_aff_ge_set returns a set containing those elements in the shared domain of pwaff1 and pwaff2 where 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 isl_pw_aff pwaffl isl_pw_aff pwaff2 isl_pw_aff_le_set isl_pw_aff pwaffl isl_pw_aff pwaff2 isl_pw_aff_lt_set isl_pw_aff pwaffl isl_pw_aff pwaff2 isl_pw_aff_ge_set isl_pw_aff pwaffl isl_pw_aff pwaff2 isl_pw_aff_gt_set isl_pw_aff pwaffl isl_pw_aff pwaff2 isl_pw_aff_list_eq_set isl_pw_aff_list listl isl_pw_aff_list list2 isl_pw_aff_list_ne_set isl_pw_aff_list listl isl_pw_aff_list list2 isl_pw_aff_list_le_set isl_pw_aff_list listl i
184. sl_set set __isl_give isl_basic_map isl_map_polyhedral_hul1 __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 e Other approximations __isl_give isl_basic_set isl_basic_set_drop_constraints_involving_dims __isl_take isl_basic_set bset enum isl_dim_type type unsigned first unsigned n __isl_give isl_basic_map isl_basic_map_drop_constraints_involving_dims __isl_take isl_basic_map bmap enum isl_dim_type type unsigned first unsigned n __isl_give isl_basic_set isl_basic_set_drop_constraints_not_involving_dims __isl_take isl_basic_set bset enum isl_dim_type type unsigned first unsigned n __isl_give isl_set isl_set_drop_constraints_involving_dims __isl_take isl_set set enum isl_dim_type type unsigned first unsigned n __isl_give isl_map isl_map_drop_constraints_involving_dims __isl_take isl_map map enum isl_dim_type type unsigned first unsigned n These functions drop any constraints not involving the specified dimensions Note that the result depends on the representation of the in
185. sl_take __isl_give isl_map __isl_take __isl_give isl_map 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 66 __isl_take 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 4 21 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 __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_partial_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 __isl_give isl_pw_multi_aff isl_set_lexmin_pw_multi_aff __isl_take isl_set set
186. sl_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 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 90 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 9 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 31 Or alternatively isl_basic_set bset bset isl_basic_set
187. sl_take isl_space space __isl_take isl_aff_list list An empty piecewise multiple quasi affine expression one with no cells the zero piecewise multiple quasi affine expression with value zero for each output dimension a piecewise multiple quasi affine expression with a single cell with either a universe or a specified domain or a zero dimensional piecewise multiple quasi affine expression on a given domain can be created using the following functions 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_multi_aff isl_multi_aff_zero __isl_take isl_space space __isl_give isl_multi_pw_aff isl_multi_pw_aff_zero __isl_take isl_space space __isl_give isl_multi_aff isl_multi_aff_identity __isl_take isl_space space __isl_give isl_pw_multi_aff isl_pw_multi_aff_identity __isl_take isl_space space __isl_give isl_multi_pw_aff isl_multi_pw_aff_identity __isl_take isl_space space __isl_give isl_pw_multi_aff isl_pw_multi_aff_from_multi_aff __isl_take isl_multi_aff ma __isl_give isl_pw_multi_aff isl_pw_multi_aff_alloc __isl_take isl_set set __isl_take isl_multi_aff maff __isl_give isl_pw_multi_aff isl_pw_multi_aff_from_domain __isl_take isl_set set __isl_give isl_union_pw_multi_aff isl_union_pw_multi_aff_empty 83 __isl_take isl_space space __isl_give isl_union_pw_multi_aff isl_union_pw_multi_aff
188. sl_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_lt less or equal isl_map_lex_le greater isl_map_lex_gt or greater or equal isl_map_lex_ge than the elements in the range The last four functions take a space for a map and return relations that express that the first n dimensions in the domain are lexicographically less isl_map_lex_lt_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_set isl_union_set_from_basic_set __isl_take isl_basic_set bset __isl_give isl_union_map isl_union_map_from_basic_map __isl_take isl_basic_map bmap __isl_give isl_union_set isl_union_set_from_set __isl_take isl_set set __isl_give isl_union_map is l_union_map_from_map __isl_take isl_map map The inverse conversions below can only be us
189. t 22 be a relation The difference set A R of R is the set of differences between image elements and the cor responding domain elements AR s 6 Z 4x gt yeR 5 y x 2 2 Simple Hull It is sometimes useful to have a single basic set or basic relation that contains a given set or relation For rational sets the obvious choice would be to compute the rational convex hull For integer sets the obvious choice would be the integer hull However isl currently does not support an integer hull operation and even if it did it would be fairly expensive to compute The convex hull operation is supported but it is also fairly expensive to compute given only an implicit representation Usually it is not required to compute the exact integer hull and an overapproxima tion of this hull is sufficient The simple hull of a set is such an overapproximation and it is defined as the inclusion wise smallest basic set that is described by con straints that are translates of the constraints in the input set This means that the simple hull is relatively cheap to compute and that the number of constraints in the simple hull is no larger than the number of constraints in the input Definition 2 2 1 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
190. t domains Piecewise quasipoly nomials are mainly used by the barvinok library for representing the number of ele ments in a parametric set or map For example the piecewise quasipolynomial above represents the number of points in the map n gt x gt y x y gt 0 and 0 lt gt x y lt n 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 upwaqp 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
191. t value __isl_give isl_basic_set isl_basic_set_fix_val __isl_take isl_basic_set bset enum isl_dim_type type unsigned pos __isl_take isl_val v __isl_give 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_set isl_set_fix_val __isl_take isl_set set enum isl_dim_type type unsigned pos __isl_take isl_val v __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_basic_map isl_basic_map_fix_val __isl_take isl_basic_map bmap enum isl_dim_type type unsigned pos __isl_take isl_val v __isl_give isl_map isl_map_fix __isl_take isl_map map enum isl_dim_type type unsigned pos isl_int value __isl_give isl_map isl_map_fix_si __isl_take isl_map map enum isl_dim_type type unsigned pos int value __isl_give isl_map isl_map_fix_val __isl_take isl_map map enum isl_dim_type type unsigned pos __isl_take isl_val v Intersect the set or relation with the hyperplane where the given dimension has the fixed given value __isl_give isl_basic_map isl_basic_map_lower_bound_si __isl_take isl_basic_map bmap enum isl_dim_type type unsigned pos int value __isl_give isl_basic_map isl_basic_map_upper_bound_si __isl_take isl_basic_map bmap enum
192. 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 unsigned 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 21 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 __isl_take isl_space range __isl_give isl_space isl_space_zip __isl_take isl_space space __isl_give isl_space isl_space_curry __isl_take isl_space space __isl_give isl_space isl_space_uncurry __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 4 9 Local Spaces A local space is essentially a space with zero or more existentially quantified variables The local space of a constraint of a basic set or relation can be obtained using the following functions include lt isl constraint h gt __isl_give isl_local_space isl_constraint_get_local_space __isl_keep isl_constraint constraint include
193. ted for node In particular if the user has also specified an after_each_for 129 callback then the annotation can be retrieved from the node passed to that callback us ing isl_ast_node_get_annotation All callbacks should NULL on failure The given isl_ast_buildcan be used to create new isl_ast_expr objects using isl_ast_build_expr_from_pw_aff or isl_ast_build_call_from_pw_multi_aff Nested AST Generation is allows the user to create an AST within the context of another AST These nested ASTs are created using the same isl_ast_build_ast_from_schedule function that is used to create the outer AST The build argument should be an isl_ast_build passed to a callback set by isl_ast_build_set_create_leaf The space of the range of the schedule argument should refer to this build In particular the space should be a wrapped relation and the domain of this wrapped relation should be the same as that of the range of the schedule returned by isl_ast_build_get_schedule below In prac tice the new schedule is typically created by calling isl_ union_map_range_product on the old schedule and some extra piece of the schedule The space of the schedule domain is also available from the isl_ast_build include lt isl ast_build h gt __isl_give isl_union_map isl_ast_build_get_schedule __isl_keep isl_ast_build build __isl_give isl_space isl_ast_build_get_schedule_space __isl_keep isl_ast_build build __isl_give isl_ast_build isl_ast_build
194. ted relation The uncurry functions perform the inverse operation Aligning parameters __isl_give isl_basic_set isl_basic_set_align_params __isl_take isl_basic_set bset __isl_take isl_space model __isl_give isl_set isl_set_align_params __isl_take isl_set set __isl_take isl_space model __isl_give isl_basic_map isl_basic_map_align_params __isl_take isl_basic_map bmap __isl_take isl_space model 57 __isl_give isl_map isl_map_align_params __isl_take isl_map map __isl_take isl_space model 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_basic_set isl_basic_set_add_dims __isl_take isl_basic_set bset enum isl_dim_type type unsigned n __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_basic_set isl_basic_set_insert_dims __isl_take isl_basic_set bset enum isl_dim_type type unsigned pos unsigned n __isl_give isl_basic_map isl_basic_map_insert_dims __isl_take isl_basic_map bmap enum isl_dim_type type unsigned pos unsigned n __isl_give isl_set isl_set_insert_dims __isl_take isl_set set enum isl_dim_type type unsigned pos uns
195. ter_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 include lt isl printer h gt __isl_give isl_printer isl_printer_print_double __isl_take isl_printer p double d 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 26 __isl_take isl_printer printer __isl_keep isl_basic_map bmap __isl_give isl_printer isl_printer_print_map __isl_take isl_printer printer __isl_keep isl_map map include lt isl union_set h gt __isl_give is
196. 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 scheduling dimensions The properties of a band can be inspected using the following functions 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 111 __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 int isl_band_list_foreach_band __isl_keep isl_band_list list int fn __isl_keep isl_band band void user void user Note that a scheduling dimension is considered to be zero distance if it does not carry any
197. tionally 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 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 4 Integer Set Library 1 4 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 availabl
198. tions and that it does not introduce any spurious solutions Given 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 143 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 de
199. tive The dual simplex method starts from an initial sample 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 134 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 correspon
200. to perform a similar compression on the unknowns but it would 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 138 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
201. tput 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 6 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 6 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 6 4 isl_polytope_scan Given a polytope isl polytope scan prints all integer points in the polytope 1 6 5 isl_codegen Given a schedule a context set and an options relation isl codegen prints out an AST that scans the domain elements of the schedule in the order of their image s taking into account the constraints in the context set 131 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
202. ts 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 PolyLib format If the represented set is a union then the first line contains a single number representing the number of disjuncts Otherwise a line containing the number 1 is optional Each disjunct is represented by a matrix of constraints The first line contains two numbers representing the number of rows and columns where the number of rows is 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
203. ument is the reverse proto dependence mapping sink iterations to potential source iterations The second argument represents the sink iterations for which we want to compute the last source iteration The third argument is the token corresponding to the source and the final argument is the token passed to isl_access_info_set_restrict The callback is expected to return a restriction on either the input or the output of the operation computing the last potential source If the input needs to be restricted then restrictions are needed for both the source and the sink iterations The sink iterations and the potential source iterations will be intersected with these sets If the output needs to be restricted then only a restriction on the source iterations is required If any error occurs the callback should return NULL An isl_restriction object can be created freed and inspected using the following functions include lt isl flow h gt __isl_give isl_restriction isl_restriction_input __isl_take isl_set source_restr __isl_take isl_set sink_restr __isl_give isl_restriction isl_restriction_output __isl_take isl_set source_restr __isl_give isl_restriction isl_restriction_none __isl_take isl_map source_map 109 __isl_give isl_restriction isl_restriction_empty __isl_take isl_map source_map void isl_restriction_free __isl_take isl_restriction restr isl_ctx isl_restriction_get_ctx __isl_keep isl_restriction r
204. unded problem usually but not always indicates an incorrect 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 136 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 eventuall
205. 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_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 33 __isl_take isl_set set __isl_give isl_map isl_map_remove_divs __isl_take isl_map map It is also possible to only remove those divs that are defined in terms of a given range of dimensions or only those for which no explicit representation is known __isl_give isl_basic_set isl_basic_set_remove_divs_involving_dims __isl_take isl_b
206. uset __isl_give isl_union_set isl_union_set_lexmax __isl_take isl_union_set uset Given a basic relation map or bmap and a domain dom the following functions compute a relation that maps each element of dom to the single lexicographic minimum or maximum of the elements that are associated to that same element in map or bmap If empty is not NULL then empty is assigned a set that contains the elements in dom that do not map to 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_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_give isl_set empty __isl_give isl_map isl_map_partial_lexmin __isl_take isl_map map __isl_take isl_set dom __isl_give isl_set 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 __i
207. val mv enum isl_dim_type type const char s __isl_give isl_multi_val isl_multi_val_set_tuple_id __isl_take isl_multi_val mv enum isl_dim_type type __isl_take isl_id id __isl_give isl_multi_val isl_multi_val_insert_dims __isl_take isl_multi_val mv enum isl_dim_type type unsigned first unsigned n __isl_give isl_multi_val isl_multi_val_add_dims __isl_take isl_multi_val mv enum isl_dim_type type unsigned n __isl_give isl_multi_val isl_multi_val_drop_dims __isl_take isl_multi_val mv enum isl_dim_type type unsigned first unsigned n Operations include include lt isl val h gt __isl_give isl_multi_val isl_multi_val_align_params __isl_take isl_multi_val mv __isl_take isl_space model __isl_give isl_multi_val isl_multi_val_range_splice __isl_take isl_multi_val mv1 unsigned pos __isl_take isl_multi_val mv2 __isl_give isl_multi_val isl_multi_val_range_product __isl_take isl_multi_val mv1 __isl_take isl_multi_val mv2 __isl_give isl_multi_val isl_multi_val_flat_range_product __isl_take isl_multi_val mv1 __isl_take isl_multi_aff mv2 70 __isl_give isl_multi_val isl_multi_val_add_val __isl_take isl_multi_val mv __isl_take isl_val v __isl_give isl_multi_val isl_multi_val_mod_val __isl_take isl_multi_val mv __isl_take isl_val v __isl_give isl_multi_val isl_multi_val_scale_val __isl_take isl_multi_val mv __isl_take isl_val v __isl
208. ve then the same big parameter trick used in the main tableau 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 con
209. w_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 Extra 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 e 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 t
210. w_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 4 24 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 each value of the parameters there is at least one element in the domain that reaches the bound If the domain of pwqp is not wrapping then the bound is computed over all elements in that domain and the result has a purely parametric domain If the domain of pwa
211. xt may have to be split for each of the constraints In the 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
212. y produce an error if the problem turns out to be unbounded 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 the

Integer Set Library: Manual

Contents

Download Pdf Manuals

Related Search

Related Contents