/* * Copyright 2008-2009 Katholieke Universiteit Leuven * * Use of this software is governed by the MIT license * * Written by Sven Verdoolaege, K.U.Leuven, Departement * Computerwetenschappen, Celestijnenlaan 200A, B-3001 Leuven, Belgium */ #include <isl_ctx_private.h> #include <isl_map_private.h> #include <isl/ilp.h> #include <isl/union_set.h> #include "isl_sample.h" #include <isl_seq.h> #include "isl_equalities.h" #include <isl_aff_private.h> #include <isl_local_space_private.h> #include <isl_mat_private.h> #include <isl_val_private.h> #include <isl_vec_private.h> #include <isl_lp_private.h> #include <isl_ilp_private.h> /* Given a basic set "bset", construct a basic set U such that for * each element x in U, the whole unit box positioned at x is inside * the given basic set. * Note that U may not contain all points that satisfy this property. * * We simply add the sum of all negative coefficients to the constant * term. This ensures that if x satisfies the resulting constraints, * then x plus any sum of unit vectors satisfies the original constraints. */ static __isl_give isl_basic_set *unit_box_base_points( __isl_take isl_basic_set *bset) { … } /* Find an integer point in "bset", preferably one that is * close to minimizing "f". * * We first check if we can easily put unit boxes inside bset. * If so, we take the best base point of any of the unit boxes we can find * and round it up to the nearest integer. * If not, we simply pick any integer point in "bset". */ static __isl_give isl_vec *initial_solution(__isl_keep isl_basic_set *bset, isl_int *f) { … } /* Restrict "bset" to those points with values for f in the interval [l, u]. */ static __isl_give isl_basic_set *add_bounds(__isl_take isl_basic_set *bset, isl_int *f, isl_int l, isl_int u) { … } /* Find an integer point in "bset" that minimizes f (in any) such that * the value of f lies inside the interval [l, u]. * Return this integer point if it can be found. * Otherwise, return sol. * * We perform a number of steps until l > u. * In each step, we look for an integer point with value in either * the whole interval [l, u] or half of the interval [l, l+floor(u-l-1/2)]. * The choice depends on whether we have found an integer point in the * previous step. If so, we look for the next point in half of the remaining * interval. * If we find a point, the current solution is updated and u is set * to its value minus 1. * If no point can be found, we update l to the upper bound of the interval * we checked (u or l+floor(u-l-1/2)) plus 1. */ static __isl_give isl_vec *solve_ilp_search(__isl_keep isl_basic_set *bset, isl_int *f, isl_int *opt, __isl_take isl_vec *sol, isl_int l, isl_int u) { … } /* Find an integer point in "bset" that minimizes f (if any). * If sol_p is not NULL then the integer point is returned in *sol_p. * The optimal value of f is returned in *opt. * * The algorithm maintains a currently best solution and an interval [l, u] * of values of f for which integer solutions could potentially still be found. * The initial value of the best solution so far is any solution. * The initial value of l is minimal value of f over the rationals * (rounded up to the nearest integer). * The initial value of u is the value of f at the initial solution minus 1. * * We then call solve_ilp_search to perform a binary search on the interval. */ static enum isl_lp_result solve_ilp(__isl_keep isl_basic_set *bset, isl_int *f, isl_int *opt, __isl_give isl_vec **sol_p) { … } static enum isl_lp_result solve_ilp_with_eq(__isl_keep isl_basic_set *bset, int max, isl_int *f, isl_int *opt, __isl_give isl_vec **sol_p) { … } /* Find an integer point in "bset" that minimizes (or maximizes if max is set) * f (if any). * If sol_p is not NULL then the integer point is returned in *sol_p. * The optimal value of f is returned in *opt. * * If there is any equality among the points in "bset", then we first * project it out. Otherwise, we continue with solve_ilp above. */ enum isl_lp_result isl_basic_set_solve_ilp(__isl_keep isl_basic_set *bset, int max, isl_int *f, isl_int *opt, __isl_give isl_vec **sol_p) { … } static enum isl_lp_result basic_set_opt(__isl_keep isl_basic_set *bset, int max, __isl_keep isl_aff *obj, isl_int *opt) { … } enum isl_lp_result isl_basic_set_opt(__isl_keep isl_basic_set *bset, int max, __isl_keep isl_aff *obj, isl_int *opt) { … } /* Compute the minimum (maximum if max is set) of the integer affine * expression obj over the points in set and put the result in *opt. * * The parameters are assumed to have been aligned. */ static enum isl_lp_result isl_set_opt_aligned(__isl_keep isl_set *set, int max, __isl_keep isl_aff *obj, isl_int *opt) { … } /* Compute the minimum (maximum if max is set) of the integer affine * expression obj over the points in set and put the result in *opt. */ enum isl_lp_result isl_set_opt(__isl_keep isl_set *set, int max, __isl_keep isl_aff *obj, isl_int *opt) { … } /* Convert the result of a function that returns an isl_lp_result * to an isl_val. The numerator of "v" is set to the optimal value * if lp_res is isl_lp_ok. "max" is set if a maximum was computed. * * Return "v" with denominator set to 1 if lp_res is isl_lp_ok. * Return NULL on error. * Return a NaN if lp_res is isl_lp_empty. * Return infinity or negative infinity if lp_res is isl_lp_unbounded, * depending on "max". */ static __isl_give isl_val *convert_lp_result(enum isl_lp_result lp_res, __isl_take isl_val *v, int max) { … } /* Return the minimum (maximum if max is set) of the integer affine * expression "obj" over the points in "bset". * * Return infinity or negative infinity if the optimal value is unbounded and * NaN if "bset" is empty. * * Call isl_basic_set_opt and translate the results. */ __isl_give isl_val *isl_basic_set_opt_val(__isl_keep isl_basic_set *bset, int max, __isl_keep isl_aff *obj) { … } /* Return the maximum of the integer affine * expression "obj" over the points in "bset". * * Return infinity or negative infinity if the optimal value is unbounded and * NaN if "bset" is empty. */ __isl_give isl_val *isl_basic_set_max_val(__isl_keep isl_basic_set *bset, __isl_keep isl_aff *obj) { … } /* Return the minimum (maximum if max is set) of the integer affine * expression "obj" over the points in "set". * * Return infinity or negative infinity if the optimal value is unbounded and * NaN if "set" is empty. * * Call isl_set_opt and translate the results. */ __isl_give isl_val *isl_set_opt_val(__isl_keep isl_set *set, int max, __isl_keep isl_aff *obj) { … } /* Return the minimum of the integer affine * expression "obj" over the points in "set". * * Return infinity or negative infinity if the optimal value is unbounded and * NaN if "set" is empty. */ __isl_give isl_val *isl_set_min_val(__isl_keep isl_set *set, __isl_keep isl_aff *obj) { … } /* Return the maximum of the integer affine * expression "obj" over the points in "set". * * Return infinity or negative infinity if the optimal value is unbounded and * NaN if "set" is empty. */ __isl_give isl_val *isl_set_max_val(__isl_keep isl_set *set, __isl_keep isl_aff *obj) { … } /* Return the optimum (min or max depending on "max") of "v1" and "v2", * where either may be NaN, signifying an uninitialized value. * That is, if either is NaN, then return the other one. */ static __isl_give isl_val *val_opt(__isl_take isl_val *v1, __isl_take isl_val *v2, int max) { … } /* Internal data structure for isl_pw_aff_opt_val. * * "max" is set if the maximum should be computed. * "res" contains the current optimum and is initialized to NaN. */ struct isl_pw_aff_opt_data { … }; /* Update the optimum in data->res with respect to the affine function * "aff" defined over "set". */ static isl_stat piece_opt(__isl_take isl_set *set, __isl_take isl_aff *aff, void *user) { … } /* Return the minimum (maximum if "max" is set) of the integer piecewise affine * expression "pa" over its definition domain. * * Return infinity or negative infinity if the optimal value is unbounded and * NaN if the domain of "pa" is empty. * * Initialize the result to NaN and then update it for each of the pieces * in "pa". */ static __isl_give isl_val *isl_pw_aff_opt_val(__isl_take isl_pw_aff *pa, int max) { … } #undef TYPE #define TYPE … #include "isl_ilp_opt_fn_val_templ.c" #undef TYPE #define TYPE … #include "isl_ilp_opt_multi_val_templ.c" #undef TYPE #define TYPE … #include "isl_ilp_opt_multi_val_templ.c" /* Internal data structure for isl_union_pw_aff_opt_val. * * "max" is set if the maximum should be computed. * "res" contains the current optimum and is initialized to NaN. */ struct isl_union_pw_aff_opt_data { … }; /* Update the optimum in data->res with the optimum of "pa". */ static isl_stat pw_aff_opt(__isl_take isl_pw_aff *pa, void *user) { … } /* Return the minimum (maximum if "max" is set) of the integer piecewise affine * expression "upa" over its definition domain. * * Return infinity or negative infinity if the optimal value is unbounded and * NaN if the domain of the expression is empty. * * Initialize the result to NaN and then update it * for each of the piecewise affine expressions in "upa". */ static __isl_give isl_val *isl_union_pw_aff_opt_val( __isl_take isl_union_pw_aff *upa, int max) { … } #undef TYPE #define TYPE … #include "isl_ilp_opt_fn_val_templ.c" /* Return a list of minima (maxima if "max" is set) * for each of the expressions in "mupa" over their domains. * * An element in the list is infinity or negative infinity if the optimal * value of the corresponding expression is unbounded and * NaN if the domain of the expression is empty. * * Iterate over all the expressions in "mupa" and collect the results. */ static __isl_give isl_multi_val *isl_multi_union_pw_aff_opt_multi_val( __isl_take isl_multi_union_pw_aff *mupa, int max) { … } /* Return a list of minima (maxima if "max" is set) over the points in "uset" * for each of the expressions in "obj". * * An element in the list is infinity or negative infinity if the optimal * value of the corresponding expression is unbounded and * NaN if the intersection of "uset" with the domain of the expression * is empty. */ static __isl_give isl_multi_val *isl_union_set_opt_multi_union_pw_aff( __isl_keep isl_union_set *uset, int max, __isl_keep isl_multi_union_pw_aff *obj) { … } /* Return a list of minima over the points in "uset" * for each of the expressions in "obj". * * An element in the list is infinity or negative infinity if the optimal * value of the corresponding expression is unbounded and * NaN if the intersection of "uset" with the domain of the expression * is empty. */ __isl_give isl_multi_val *isl_union_set_min_multi_union_pw_aff( __isl_keep isl_union_set *uset, __isl_keep isl_multi_union_pw_aff *obj) { … } /* Return a list of minima * for each of the expressions in "mupa" over their domains. * * An element in the list is negative infinity if the optimal * value of the corresponding expression is unbounded and * NaN if the domain of the expression is empty. */ __isl_give isl_multi_val *isl_multi_union_pw_aff_min_multi_val( __isl_take isl_multi_union_pw_aff *mupa) { … } /* Return a list of maxima * for each of the expressions in "mupa" over their domains. * * An element in the list is infinity if the optimal * value of the corresponding expression is unbounded and * NaN if the domain of the expression is empty. */ __isl_give isl_multi_val *isl_multi_union_pw_aff_max_multi_val( __isl_take isl_multi_union_pw_aff *mupa) { … } #undef BASE #define BASE … #include "isl_ilp_opt_val_templ.c" /* Return the maximal value attained by the given set dimension, * independently of the parameter values and of any other dimensions. * * Return infinity if the optimal value is unbounded and * NaN if "bset" is empty. */ __isl_give isl_val *isl_basic_set_dim_max_val(__isl_take isl_basic_set *bset, int pos) { … } #undef BASE #define BASE … #include "isl_ilp_opt_val_templ.c" /* Return the minimal value attained by the given set dimension, * independently of the parameter values and of any other dimensions. * * Return negative infinity if the optimal value is unbounded and * NaN if "set" is empty. */ __isl_give isl_val *isl_set_dim_min_val(__isl_take isl_set *set, int pos) { … } /* Return the maximal value attained by the given set dimension, * independently of the parameter values and of any other dimensions. * * Return infinity if the optimal value is unbounded and * NaN if "set" is empty. */ __isl_give isl_val *isl_set_dim_max_val(__isl_take isl_set *set, int pos) { … }