/* * Copyright 2008-2009 Katholieke Universiteit Leuven * Copyright 2013 Ecole Normale Superieure * Copyright 2014 INRIA Rocquencourt * Copyright 2016 Sven Verdoolaege * * 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 * and Ecole Normale Superieure, 45 rue d'Ulm, 75230 Paris, France * and Inria Paris - Rocquencourt, Domaine de Voluceau - Rocquencourt, * B.P. 105 - 78153 Le Chesnay, France */ #include <isl_ctx_private.h> #include <isl_mat_private.h> #include <isl_vec_private.h> #include "isl_map_private.h" #include "isl_tab.h" #include <isl_seq.h> #include <isl_config.h> #include <bset_to_bmap.c> #include <bset_from_bmap.c> /* * The implementation of tableaus in this file was inspired by Section 8 * of David Detlefs, Greg Nelson and James B. Saxe, "Simplify: a theorem * prover for program checking". */ struct isl_tab *isl_tab_alloc(struct isl_ctx *ctx, unsigned n_row, unsigned n_var, unsigned M) { … } isl_ctx *isl_tab_get_ctx(struct isl_tab *tab) { … } int isl_tab_extend_cons(struct isl_tab *tab, unsigned n_new) { … } /* Make room for at least n_new extra variables. * Return -1 if anything went wrong. */ int isl_tab_extend_vars(struct isl_tab *tab, unsigned n_new) { … } static void free_undo_record(struct isl_tab_undo *undo) { … } static void free_undo(struct isl_tab *tab) { … } void isl_tab_free(struct isl_tab *tab) { … } struct isl_tab *isl_tab_dup(struct isl_tab *tab) { … } /* Construct the coefficient matrix of the product tableau * of two tableaus. * mat{1,2} is the coefficient matrix of tableau {1,2} * row{1,2} is the number of rows in tableau {1,2} * col{1,2} is the number of columns in tableau {1,2} * off is the offset to the coefficient column (skipping the * denominator, the constant term and the big parameter if any) * r{1,2} is the number of redundant rows in tableau {1,2} * d{1,2} is the number of dead columns in tableau {1,2} * * The order of the rows and columns in the result is as explained * in isl_tab_product. */ static __isl_give isl_mat *tab_mat_product(__isl_keep isl_mat *mat1, __isl_keep isl_mat *mat2, unsigned row1, unsigned row2, unsigned col1, unsigned col2, unsigned off, unsigned r1, unsigned r2, unsigned d1, unsigned d2) { … } /* Update the row or column index of a variable that corresponds * to a variable in the first input tableau. */ static void update_index1(struct isl_tab_var *var, unsigned r1, unsigned r2, unsigned d1, unsigned d2) { … } /* Update the row or column index of a variable that corresponds * to a variable in the second input tableau. */ static void update_index2(struct isl_tab_var *var, unsigned row1, unsigned col1, unsigned r1, unsigned r2, unsigned d1, unsigned d2) { … } /* Create a tableau that represents the Cartesian product of the sets * represented by tableaus tab1 and tab2. * The order of the rows in the product is * - redundant rows of tab1 * - redundant rows of tab2 * - non-redundant rows of tab1 * - non-redundant rows of tab2 * The order of the columns is * - denominator * - constant term * - coefficient of big parameter, if any * - dead columns of tab1 * - dead columns of tab2 * - live columns of tab1 * - live columns of tab2 * The order of the variables and the constraints is a concatenation * of order in the two input tableaus. */ struct isl_tab *isl_tab_product(struct isl_tab *tab1, struct isl_tab *tab2) { … } static struct isl_tab_var *var_from_index(struct isl_tab *tab, int i) { … } struct isl_tab_var *isl_tab_var_from_row(struct isl_tab *tab, int i) { … } static struct isl_tab_var *var_from_col(struct isl_tab *tab, int i) { … } /* Check if there are any upper bounds on column variable "var", * i.e., non-negative rows where var appears with a negative coefficient. * Return 1 if there are no such bounds. */ static int max_is_manifestly_unbounded(struct isl_tab *tab, struct isl_tab_var *var) { … } /* Check if there are any lower bounds on column variable "var", * i.e., non-negative rows where var appears with a positive coefficient. * Return 1 if there are no such bounds. */ static int min_is_manifestly_unbounded(struct isl_tab *tab, struct isl_tab_var *var) { … } static int row_cmp(struct isl_tab *tab, int r1, int r2, int c, isl_int *t) { … } /* Given the index of a column "c", return the index of a row * that can be used to pivot the column in, with either an increase * (sgn > 0) or a decrease (sgn < 0) of the corresponding variable. * If "var" is not NULL, then the row returned will be different from * the one associated with "var". * * Each row in the tableau is of the form * * x_r = a_r0 + \sum_i a_ri x_i * * Only rows with x_r >= 0 and with the sign of a_ri opposite to "sgn" * impose any limit on the increase or decrease in the value of x_c * and this bound is equal to a_r0 / |a_rc|. We are therefore looking * for the row with the smallest (most stringent) such bound. * Note that the common denominator of each row drops out of the fraction. * To check if row j has a smaller bound than row r, i.e., * a_j0 / |a_jc| < a_r0 / |a_rc| or a_j0 |a_rc| < a_r0 |a_jc|, * we check if -sign(a_jc) (a_j0 a_rc - a_r0 a_jc) < 0, * where -sign(a_jc) is equal to "sgn". */ static int pivot_row(struct isl_tab *tab, struct isl_tab_var *var, int sgn, int c) { … } /* Find a pivot (row and col) that will increase (sgn > 0) or decrease * (sgn < 0) the value of row variable var. * If not NULL, then skip_var is a row variable that should be ignored * while looking for a pivot row. It is usually equal to var. * * As the given row in the tableau is of the form * * x_r = a_r0 + \sum_i a_ri x_i * * we need to find a column such that the sign of a_ri is equal to "sgn" * (such that an increase in x_i will have the desired effect) or a * column with a variable that may attain negative values. * If a_ri is positive, then we need to move x_i in the same direction * to obtain the desired effect. Otherwise, x_i has to move in the * opposite direction. */ static void find_pivot(struct isl_tab *tab, struct isl_tab_var *var, struct isl_tab_var *skip_var, int sgn, int *row, int *col) { … } /* Return 1 if row "row" represents an obviously redundant inequality. * This means * - it represents an inequality or a variable * - that is the sum of a non-negative sample value and a positive * combination of zero or more non-negative constraints. */ int isl_tab_row_is_redundant(struct isl_tab *tab, int row) { … } static void swap_rows(struct isl_tab *tab, int row1, int row2) { … } static isl_stat push_union(struct isl_tab *tab, enum isl_tab_undo_type type, union isl_tab_undo_val u) WARN_UNUSED; /* Push record "u" onto the undo stack of "tab", provided "tab" * keeps track of undo information. * * If the record cannot be pushed, then mark the undo stack as invalid * such that a later rollback attempt will not try to undo earlier * records without having been able to undo the current record. */ static isl_stat push_union(struct isl_tab *tab, enum isl_tab_undo_type type, union isl_tab_undo_val u) { … } isl_stat isl_tab_push_var(struct isl_tab *tab, enum isl_tab_undo_type type, struct isl_tab_var *var) { … } isl_stat isl_tab_push(struct isl_tab *tab, enum isl_tab_undo_type type) { … } /* Push a record on the undo stack describing the current basic * variables, so that the this state can be restored during rollback. */ isl_stat isl_tab_push_basis(struct isl_tab *tab) { … } isl_stat isl_tab_push_callback(struct isl_tab *tab, struct isl_tab_callback *callback) { … } struct isl_tab *isl_tab_init_samples(struct isl_tab *tab) { … } int isl_tab_add_sample(struct isl_tab *tab, __isl_take isl_vec *sample) { … } struct isl_tab *isl_tab_drop_sample(struct isl_tab *tab, int s) { … } /* Record the current number of samples so that we can remove newer * samples during a rollback. */ isl_stat isl_tab_save_samples(struct isl_tab *tab) { … } /* Mark row with index "row" as being redundant. * If we may need to undo the operation or if the row represents * a variable of the original problem, the row is kept, * but no longer considered when looking for a pivot row. * Otherwise, the row is simply removed. * * The row may be interchanged with some other row. If it * is interchanged with a later row, return 1. Otherwise return 0. * If the rows are checked in order in the calling function, * then a return value of 1 means that the row with the given * row number may now contain a different row that hasn't been checked yet. */ int isl_tab_mark_redundant(struct isl_tab *tab, int row) { … } /* Mark "tab" as a rational tableau. * If it wasn't marked as a rational tableau already and if we may * need to undo changes, then arrange for the marking to be undone * during the undo. */ int isl_tab_mark_rational(struct isl_tab *tab) { … } isl_stat isl_tab_mark_empty(struct isl_tab *tab) { … } int isl_tab_freeze_constraint(struct isl_tab *tab, int con) { … } /* Update the rows signs after a pivot of "row" and "col", with "row_sgn" * the original sign of the pivot element. * We only keep track of row signs during PILP solving and in this case * we only pivot a row with negative sign (meaning the value is always * non-positive) using a positive pivot element. * * For each row j, the new value of the parametric constant is equal to * * a_j0 - a_jc a_r0/a_rc * * where a_j0 is the original parametric constant, a_rc is the pivot element, * a_r0 is the parametric constant of the pivot row and a_jc is the * pivot column entry of the row j. * Since a_r0 is non-positive and a_rc is positive, the sign of row j * remains the same if a_jc has the same sign as the row j or if * a_jc is zero. In all other cases, we reset the sign to "unknown". */ static void update_row_sign(struct isl_tab *tab, int row, int col, int row_sgn) { … } /* Given a row number "row" and a column number "col", pivot the tableau * such that the associated variables are interchanged. * The given row in the tableau expresses * * x_r = a_r0 + \sum_i a_ri x_i * * or * * x_c = 1/a_rc x_r - a_r0/a_rc + sum_{i \ne r} -a_ri/a_rc * * Substituting this equality into the other rows * * x_j = a_j0 + \sum_i a_ji x_i * * with a_jc \ne 0, we obtain * * x_j = a_jc/a_rc x_r + a_j0 - a_jc a_r0/a_rc + sum a_ji - a_jc a_ri/a_rc * * The tableau * * n_rc/d_r n_ri/d_r * n_jc/d_j n_ji/d_j * * where i is any other column and j is any other row, * is therefore transformed into * * s(n_rc)d_r/|n_rc| -s(n_rc)n_ri/|n_rc| * s(n_rc)d_r n_jc/(|n_rc| d_j) (n_ji |n_rc| - s(n_rc)n_jc n_ri)/(|n_rc| d_j) * * The transformation is performed along the following steps * * d_r/n_rc n_ri/n_rc * n_jc/d_j n_ji/d_j * * s(n_rc)d_r/|n_rc| -s(n_rc)n_ri/|n_rc| * n_jc/d_j n_ji/d_j * * s(n_rc)d_r/|n_rc| -s(n_rc)n_ri/|n_rc| * n_jc/(|n_rc| d_j) n_ji/(|n_rc| d_j) * * s(n_rc)d_r/|n_rc| -s(n_rc)n_ri/|n_rc| * n_jc/(|n_rc| d_j) (n_ji |n_rc|)/(|n_rc| d_j) * * s(n_rc)d_r/|n_rc| -s(n_rc)n_ri/|n_rc| * n_jc/(|n_rc| d_j) (n_ji |n_rc| - s(n_rc)n_jc n_ri)/(|n_rc| d_j) * * s(n_rc)d_r/|n_rc| -s(n_rc)n_ri/|n_rc| * s(n_rc)d_r n_jc/(|n_rc| d_j) (n_ji |n_rc| - s(n_rc)n_jc n_ri)/(|n_rc| d_j) * */ int isl_tab_pivot(struct isl_tab *tab, int row, int col) { … } /* If "var" represents a column variable, then pivot is up (sgn > 0) * or down (sgn < 0) to a row. The variable is assumed not to be * unbounded in the specified direction. * If sgn = 0, then the variable is unbounded in both directions, * and we pivot with any row we can find. */ static int to_row(struct isl_tab *tab, struct isl_tab_var *var, int sign) WARN_UNUSED; static int to_row(struct isl_tab *tab, struct isl_tab_var *var, int sign) { … } /* Check whether all variables that are marked as non-negative * also have a non-negative sample value. This function is not * called from the current code but is useful during debugging. */ static void check_table(struct isl_tab *tab) __attribute__ ((unused)); static void check_table(struct isl_tab *tab) { … } /* Return the sign of the maximal value of "var". * If the sign is not negative, then on return from this function, * the sample value will also be non-negative. * * If "var" is manifestly unbounded wrt positive values, we are done. * Otherwise, we pivot the variable up to a row if needed. * Then we continue pivoting up until either * - no more up pivots can be performed * - the sample value is positive * - the variable is pivoted into a manifestly unbounded column */ static int sign_of_max(struct isl_tab *tab, struct isl_tab_var *var) { … } int isl_tab_sign_of_max(struct isl_tab *tab, int con) { … } static int row_is_neg(struct isl_tab *tab, int row) { … } static int row_sgn(struct isl_tab *tab, int row) { … } /* Perform pivots until the row variable "var" has a non-negative * sample value or until no more upward pivots can be performed. * Return the sign of the sample value after the pivots have been * performed. */ static int restore_row(struct isl_tab *tab, struct isl_tab_var *var) { … } /* Perform pivots until we are sure that the row variable "var" * can attain non-negative values. After return from this * function, "var" is still a row variable, but its sample * value may not be non-negative, even if the function returns 1. */ static int at_least_zero(struct isl_tab *tab, struct isl_tab_var *var) { … } /* Return a negative value if "var" can attain negative values. * Return a non-negative value otherwise. * * If "var" is manifestly unbounded wrt negative values, we are done. * Otherwise, if var is in a column, we can pivot it down to a row. * Then we continue pivoting down until either * - the pivot would result in a manifestly unbounded column * => we don't perform the pivot, but simply return -1 * - no more down pivots can be performed * - the sample value is negative * If the sample value becomes negative and the variable is supposed * to be nonnegative, then we undo the last pivot. * However, if the last pivot has made the pivoting variable * obviously redundant, then it may have moved to another row. * In that case we look for upward pivots until we reach a non-negative * value again. */ static int sign_of_min(struct isl_tab *tab, struct isl_tab_var *var) { … } static int row_at_most_neg_one(struct isl_tab *tab, int row) { … } /* Return 1 if "var" can attain values <= -1. * Return 0 otherwise. * * If the variable "var" is supposed to be non-negative (is_nonneg is set), * then the sample value of "var" is assumed to be non-negative when the * the function is called. If 1 is returned then the constraint * is not redundant and the sample value is made non-negative again before * the function returns. */ int isl_tab_min_at_most_neg_one(struct isl_tab *tab, struct isl_tab_var *var) { … } /* Return 1 if "var" can attain values >= 1. * Return 0 otherwise. */ static int at_least_one(struct isl_tab *tab, struct isl_tab_var *var) { … } static void swap_cols(struct isl_tab *tab, int col1, int col2) { … } /* Mark column with index "col" as representing a zero variable. * If we may need to undo the operation the column is kept, * but no longer considered. * Otherwise, the column is simply removed. * * The column may be interchanged with some other column. If it * is interchanged with a later column, return 1. Otherwise return 0. * If the columns are checked in order in the calling function, * then a return value of 1 means that the column with the given * column number may now contain a different column that * hasn't been checked yet. */ int isl_tab_kill_col(struct isl_tab *tab, int col) { … } static int row_is_manifestly_non_integral(struct isl_tab *tab, int row) { … } /* For integer tableaus, check if any of the coordinates are stuck * at a non-integral value. */ static int tab_is_manifestly_empty(struct isl_tab *tab) { … } /* Row variable "var" is non-negative and cannot attain any values * larger than zero. This means that the coefficients of the unrestricted * column variables are zero and that the coefficients of the non-negative * column variables are zero or negative. * Each of the non-negative variables with a negative coefficient can * then also be written as the negative sum of non-negative variables * and must therefore also be zero. * * If "temp_var" is set, then "var" is a temporary variable that * will be removed after this function returns and for which * no information is recorded on the undo stack. * Do not add any undo records involving this variable in this case * since the variable will have been removed before any future undo * operations. Also avoid marking the variable as redundant, * since that either adds an undo record or needlessly removes the row * (the caller will take care of removing the row). */ static isl_stat close_row(struct isl_tab *tab, struct isl_tab_var *var, int temp_var) WARN_UNUSED; static isl_stat close_row(struct isl_tab *tab, struct isl_tab_var *var, int temp_var) { … } /* Add a constraint to the tableau and allocate a row for it. * Return the index into the constraint array "con". * * This function assumes that at least one more row and at least * one more element in the constraint array are available in the tableau. */ int isl_tab_allocate_con(struct isl_tab *tab) { … } /* Move the entries in tab->var up one position, starting at "first", * creating room for an extra entry at position "first". * Since some of the entries of tab->row_var and tab->col_var contain * indices into this array, they have to be updated accordingly. */ static int var_insert_entry(struct isl_tab *tab, int first) { … } /* Drop the entry at position "first" in tab->var, moving all * subsequent entries down. * Since some of the entries of tab->row_var and tab->col_var contain * indices into this array, they have to be updated accordingly. */ static int var_drop_entry(struct isl_tab *tab, int first) { … } /* Add a variable to the tableau at position "r" and allocate a column for it. * Return the index into the variable array "var", i.e., "r", * or -1 on error. */ int isl_tab_insert_var(struct isl_tab *tab, int r) { … } /* Add a row to the tableau. The row is given as an affine combination * of the original variables and needs to be expressed in terms of the * column variables. * * This function assumes that at least one more row and at least * one more element in the constraint array are available in the tableau. * * We add each term in turn. * If r = n/d_r is the current sum and we need to add k x, then * if x is a column variable, we increase the numerator of * this column by k d_r * if x = f/d_x is a row variable, then the new representation of r is * * n k f d_x/g n + d_r/g k f m/d_r n + m/d_g k f * --- + --- = ------------------- = ------------------- * d_r d_r d_r d_x/g m * * with g the gcd of d_r and d_x and m the lcm of d_r and d_x. * * If tab->M is set, then, internally, each variable x is represented * as x' - M. We then also need no subtract k d_r from the coefficient of M. */ int isl_tab_add_row(struct isl_tab *tab, isl_int *line) { … } static isl_stat drop_row(struct isl_tab *tab, int row) { … } /* Drop the variable in column "col" along with the column. * The column is removed first because it may need to be moved * into the last position and this process requires * the contents of the col_var array in a state * before the removal of the variable. */ static isl_stat drop_col(struct isl_tab *tab, int col) { … } /* Add inequality "ineq" and check if it conflicts with the * previously added constraints or if it is obviously redundant. * * This function assumes that at least one more row and at least * one more element in the constraint array are available in the tableau. */ isl_stat isl_tab_add_ineq(struct isl_tab *tab, isl_int *ineq) { … } /* Pivot a non-negative variable down until it reaches the value zero * and then pivot the variable into a column position. */ static int to_col(struct isl_tab *tab, struct isl_tab_var *var) WARN_UNUSED; static int to_col(struct isl_tab *tab, struct isl_tab_var *var) { … } /* We assume Gaussian elimination has been performed on the equalities. * The equalities can therefore never conflict. * Adding the equalities is currently only really useful for a later call * to isl_tab_ineq_type. * * This function assumes that at least one more row and at least * one more element in the constraint array are available in the tableau. */ static struct isl_tab *add_eq(struct isl_tab *tab, isl_int *eq) { … } /* Does the sample value of row "row" of "tab" involve the big parameter, * if any? */ static int row_is_big(struct isl_tab *tab, int row) { … } static int row_is_manifestly_zero(struct isl_tab *tab, int row) { … } /* Add an equality that is known to be valid for the given tableau. * * This function assumes that at least one more row and at least * one more element in the constraint array are available in the tableau. */ int isl_tab_add_valid_eq(struct isl_tab *tab, isl_int *eq) { … } /* Add a zero row to "tab" and return the corresponding index * in the constraint array. * * This function assumes that at least one more row and at least * one more element in the constraint array are available in the tableau. */ static int add_zero_row(struct isl_tab *tab) { … } /* Add equality "eq" and check if it conflicts with the * previously added constraints or if it is obviously redundant. * * This function assumes that at least one more row and at least * one more element in the constraint array are available in the tableau. * If tab->bmap is set, then two rows are needed instead of one. */ isl_stat isl_tab_add_eq(struct isl_tab *tab, isl_int *eq) { … } /* Construct and return an inequality that expresses an upper bound * on the given div. * In particular, if the div is given by * * d = floor(e/m) * * then the inequality expresses * * m d <= e */ static __isl_give isl_vec *ineq_for_div(__isl_keep isl_basic_map *bmap, unsigned div) { … } /* For a div d = floor(f/m), add the constraints * * f - m d >= 0 * -(f-(m-1)) + m d >= 0 * * Note that the second constraint is the negation of * * f - m d >= m * * If add_ineq is not NULL, then this function is used * instead of isl_tab_add_ineq to effectively add the inequalities. * * This function assumes that at least two more rows and at least * two more elements in the constraint array are available in the tableau. */ static isl_stat add_div_constraints(struct isl_tab *tab, unsigned div, isl_stat (*add_ineq)(void *user, isl_int *), void *user) { … } /* Check whether the div described by "div" is obviously non-negative. * If we are using a big parameter, then we will encode the div * as div' = M + div, which is always non-negative. * Otherwise, we check whether div is a non-negative affine combination * of non-negative variables. */ static int div_is_nonneg(struct isl_tab *tab, __isl_keep isl_vec *div) { … } /* Insert an extra div, prescribed by "div", to the tableau and * the associated bmap (which is assumed to be non-NULL). * The extra integer division is inserted at (tableau) position "pos". * Return "pos" or -1 if an error occurred. * * If add_ineq is not NULL, then this function is used instead * of isl_tab_add_ineq to add the div constraints. * This complication is needed because the code in isl_tab_pip * wants to perform some extra processing when an inequality * is added to the tableau. */ int isl_tab_insert_div(struct isl_tab *tab, int pos, __isl_keep isl_vec *div, isl_stat (*add_ineq)(void *user, isl_int *), void *user) { … } /* Add an extra div, prescribed by "div", to the tableau and * the associated bmap (which is assumed to be non-NULL). */ int isl_tab_add_div(struct isl_tab *tab, __isl_keep isl_vec *div) { … } /* If "track" is set, then we want to keep track of all constraints in tab * in its bmap field. This field is initialized from a copy of "bmap", * so we need to make sure that all constraints in "bmap" also appear * in the constructed tab. */ __isl_give struct isl_tab *isl_tab_from_basic_map( __isl_keep isl_basic_map *bmap, int track) { … } __isl_give struct isl_tab *isl_tab_from_basic_set( __isl_keep isl_basic_set *bset, int track) { … } /* Construct a tableau corresponding to the recession cone of "bset". */ struct isl_tab *isl_tab_from_recession_cone(__isl_keep isl_basic_set *bset, int parametric) { … } /* Assuming "tab" is the tableau of a cone, check if the cone is * bounded, i.e., if it is empty or only contains the origin. */ isl_bool isl_tab_cone_is_bounded(struct isl_tab *tab) { … } int isl_tab_sample_is_integer(struct isl_tab *tab) { … } static struct isl_vec *extract_integer_sample(struct isl_tab *tab) { … } __isl_give isl_vec *isl_tab_get_sample_value(struct isl_tab *tab) { … } /* Store the sample value of "var" of "tab" rounded up (if sgn > 0) * or down (if sgn < 0) to the nearest integer in *v. */ static void get_rounded_sample_value(struct isl_tab *tab, struct isl_tab_var *var, int sgn, isl_int *v) { … } /* Update "bmap" based on the results of the tableau "tab". * In particular, implicit equalities are made explicit, redundant constraints * are removed and if the sample value happens to be integer, it is stored * in "bmap" (unless "bmap" already had an integer sample). * * The tableau is assumed to have been created from "bmap" using * isl_tab_from_basic_map. */ __isl_give isl_basic_map *isl_basic_map_update_from_tab( __isl_take isl_basic_map *bmap, struct isl_tab *tab) { … } __isl_give isl_basic_set *isl_basic_set_update_from_tab( __isl_take isl_basic_set *bset, struct isl_tab *tab) { … } /* Drop the last constraint added to "tab" in position "r". * The constraint is expected to have remained in a row. */ static isl_stat drop_last_con_in_row(struct isl_tab *tab, int r) { … } /* Given a non-negative variable "var", temporarily add a new non-negative * variable that is the opposite of "var", ensuring that "var" can only attain * the value zero. The new variable is removed again before this function * returns. However, the effect of forcing "var" to be zero remains. * If var = n/d is a row variable, then the new variable = -n/d. * If var is a column variables, then the new variable = -var. * If the new variable cannot attain non-negative values, then * the resulting tableau is empty. * Otherwise, we know the value will be zero and we close the row. */ static isl_stat cut_to_hyperplane(struct isl_tab *tab, struct isl_tab_var *var) { … } /* Check that "con" is a valid constraint position for "tab". */ static isl_stat isl_tab_check_con(struct isl_tab *tab, int con) { … } /* Given a tableau "tab" and an inequality constraint "con" of the tableau, * relax the inequality by one. That is, the inequality r >= 0 is replaced * by r' = r + 1 >= 0. * If r is a row variable, we simply increase the constant term by one * (taking into account the denominator). * If r is a column variable, then we need to modify each row that * refers to r = r' - 1 by substituting this equality, effectively * subtracting the coefficient of the column from the constant. * We should only do this if the minimum is manifestly unbounded, * however. Otherwise, we may end up with negative sample values * for non-negative variables. * So, if r is a column variable with a minimum that is not * manifestly unbounded, then we need to move it to a row. * However, the sample value of this row may be negative, * even after the relaxation, so we need to restore it. * We therefore prefer to pivot a column up to a row, if possible. */ int isl_tab_relax(struct isl_tab *tab, int con) { … } /* Replace the variable v at position "pos" in the tableau "tab" * by v' = v + shift. * * If the variable is in a column, then we first check if we can * simply plug in v = v' - shift. The effect on a row with * coefficient f/d for variable v is that the constant term c/d * is replaced by (c - f * shift)/d. If shift is positive and * f is negative for each row that needs to remain non-negative, * then this is clearly safe. In other words, if the minimum of v * is manifestly unbounded, then we can keep v in a column position. * Otherwise, we can pivot it down to a row. * Similarly, if shift is negative, we need to check if the maximum * of is manifestly unbounded. * * If the variable is in a row (from the start or after pivoting), * then the constant term c/d is replaced by (c + d * shift)/d. */ int isl_tab_shift_var(struct isl_tab *tab, int pos, isl_int shift) { … } /* Remove the sign constraint from constraint "con". * * If the constraint variable was originally marked non-negative, * then we make sure we mark it non-negative again during rollback. */ int isl_tab_unrestrict(struct isl_tab *tab, int con) { … } int isl_tab_select_facet(struct isl_tab *tab, int con) { … } static int may_be_equality(struct isl_tab *tab, int row) { … } /* Return an isl_tab_var that has been marked or NULL if no such * variable can be found. * The marked field has only been set for variables that * appear in non-redundant rows or non-dead columns. * * Pick the last constraint variable that is marked and * that appears in either a non-redundant row or a non-dead columns. * Since the returned variable is tested for being a redundant constraint or * an implicit equality, there is no need to return any tab variable that * corresponds to a variable. */ static struct isl_tab_var *select_marked(struct isl_tab *tab) { … } /* Check for (near) equalities among the constraints. * A constraint is an equality if it is non-negative and if * its maximal value is either * - zero (in case of rational tableaus), or * - strictly less than 1 (in case of integer tableaus) * * We first mark all non-redundant and non-dead variables that * are not frozen and not obviously not an equality. * Then we iterate over all marked variables if they can attain * any values larger than zero or at least one. * If the maximal value is zero, we mark any column variables * that appear in the row as being zero and mark the row as being redundant. * Otherwise, if the maximal value is strictly less than one (and the * tableau is integer), then we restrict the value to being zero * by adding an opposite non-negative variable. * The order in which the variables are considered is not important. */ int isl_tab_detect_implicit_equalities(struct isl_tab *tab) { … } /* Update the element of row_var or col_var that corresponds to * constraint tab->con[i] to a move from position "old" to position "i". */ static int update_con_after_move(struct isl_tab *tab, int i, int old) { … } /* Interchange constraints "con1" and "con2" in "tab". * In particular, interchange the contents of these entries in tab->con. * Since tab->col_var and tab->row_var point back into this array, * they need to be updated accordingly. */ isl_stat isl_tab_swap_constraints(struct isl_tab *tab, int con1, int con2) { … } /* Rotate the "n" constraints starting at "first" to the right, * putting the last constraint in the position of the first constraint. */ static int rotate_constraints(struct isl_tab *tab, int first, int n) { … } /* Drop the "n" entries starting at position "first" in tab->con, moving all * subsequent entries down. * Since some of the entries of tab->row_var and tab->col_var contain * indices into this array, they have to be updated accordingly. */ static isl_stat con_drop_entries(struct isl_tab *tab, unsigned first, unsigned n) { … } /* isl_basic_map_gauss5 callback that gets called when * two (equality) constraints "a" and "b" get interchanged * in the basic map. Perform the same interchange in "tab". */ static isl_stat swap_eq(unsigned a, unsigned b, void *user) { … } /* isl_basic_map_gauss5 callback that gets called when * the final "n" equality constraints get removed. * As a special case, if "n" is equal to the total number * of equality constraints, then this means the basic map * turned out to be empty. * Drop the same number of equality constraints from "tab" or * mark it empty in the special case. */ static isl_stat drop_eq(unsigned n, void *user) { … } /* If "bmap" has more than a single reference, then call * isl_basic_map_gauss on it, updating "tab" accordingly. */ static __isl_give isl_basic_map *gauss_if_shared(__isl_take isl_basic_map *bmap, struct isl_tab *tab) { … } /* Make the equalities that are implicit in "bmap" but that have been * detected in the corresponding "tab" explicit in "bmap" and update * "tab" to reflect the new order of the constraints. * * In particular, if inequality i is an implicit equality then * isl_basic_map_inequality_to_equality will move the inequality * in front of the other equality and it will move the last inequality * in the position of inequality i. * In the tableau, the inequalities of "bmap" are stored after the equalities * and so the original order * * E E E E E A A A I B B B B L * * is changed into * * I E E E E E A A A L B B B B * * where I is the implicit equality, the E are equalities, * the A inequalities before I, the B inequalities after I and * L the last inequality. * We therefore need to rotate to the right two sets of constraints, * those up to and including I and those after I. * * If "tab" contains any constraints that are not in "bmap" then they * appear after those in "bmap" and they should be left untouched. * * Note that this function only calls isl_basic_map_gauss * (in case some equality constraints got detected) * if "bmap" has more than one reference. * If it only has a single reference, then it is left in a temporary state, * because the caller may require this state. * Calling isl_basic_map_gauss is then the responsibility of the caller. */ __isl_give isl_basic_map *isl_tab_make_equalities_explicit(struct isl_tab *tab, __isl_take isl_basic_map *bmap) { … } static int con_is_redundant(struct isl_tab *tab, struct isl_tab_var *var) { … } /* Check for (near) redundant constraints. * A constraint is redundant if it is non-negative and if * its minimal value (temporarily ignoring the non-negativity) is either * - zero (in case of rational tableaus), or * - strictly larger than -1 (in case of integer tableaus) * * We first mark all non-redundant and non-dead variables that * are not frozen and not obviously negatively unbounded. * Then we iterate over all marked variables if they can attain * any values smaller than zero or at most negative one. * If not, we mark the row as being redundant (assuming it hasn't * been detected as being obviously redundant in the mean time). */ int isl_tab_detect_redundant(struct isl_tab *tab) { … } int isl_tab_is_equality(struct isl_tab *tab, int con) { … } /* Return the minimal value of the affine expression "f" with denominator * "denom" in *opt, *opt_denom, assuming the tableau is not empty and * the expression cannot attain arbitrarily small values. * If opt_denom is NULL, then *opt is rounded up to the nearest integer. * The return value reflects the nature of the result (empty, unbounded, * minimal value returned in *opt). * * This function assumes that at least one more row and at least * one more element in the constraint array are available in the tableau. */ enum isl_lp_result isl_tab_min(struct isl_tab *tab, isl_int *f, isl_int denom, isl_int *opt, isl_int *opt_denom, unsigned flags) { … } /* Is the constraint at position "con" marked as being redundant? * If it is marked as representing an equality, then it is not * considered to be redundant. * Note that isl_tab_mark_redundant marks both the isl_tab_var as * redundant and moves the corresponding row into the first * tab->n_redundant positions (or removes the row, assigning it index -1), * so the final test is actually redundant itself. */ int isl_tab_is_redundant(struct isl_tab *tab, int con) { … } /* Is variable "var" of "tab" fixed to a constant value by its row * in the tableau? * If so and if "value" is not NULL, then store this constant value * in "value". * * That is, is it a row variable that only has non-zero coefficients * for dead columns? */ static isl_bool is_constant(struct isl_tab *tab, struct isl_tab_var *var, isl_int *value) { … } /* Has the variable "var' of "tab" reached a value that is greater than * or equal (if sgn > 0) or smaller than or equal (if sgn < 0) to "target"? * "tmp" has been initialized by the caller and can be used * to perform local computations. * * If the sample value involves the big parameter, then any value * is reached. * Otherwise check if n/d >= t, i.e., n >= d * t (if sgn > 0) * or n/d <= t, i.e., n <= d * t (if sgn < 0). */ static int reached(struct isl_tab *tab, struct isl_tab_var *var, int sgn, isl_int target, isl_int *tmp) { … } /* Can variable "var" of "tab" attain the value "target" by * pivoting up (if sgn > 0) or down (if sgn < 0)? * If not, then pivot up [down] to the greatest [smallest] * rational value. * "tmp" has been initialized by the caller and can be used * to perform local computations. * * If the variable is manifestly unbounded in the desired direction, * then it can attain any value. * Otherwise, it can be moved to a row. * Continue pivoting until the target is reached. * If no more pivoting can be performed, the maximal [minimal] * rational value has been reached and the target cannot be reached. * If the variable would be pivoted into a manifestly unbounded column, * then the target can be reached. */ static isl_bool var_reaches(struct isl_tab *tab, struct isl_tab_var *var, int sgn, isl_int target, isl_int *tmp) { … } /* Check if variable "var" of "tab" can only attain a single (integer) * value, and, if so, add an equality constraint to fix the variable * to this single value and store the result in "target". * "target" and "tmp" have been initialized by the caller. * * Given the current sample value, round it down and check * whether it is possible to attain a strictly smaller integer value. * If so, the variable is not restricted to a single integer value. * Otherwise, the search stops at the smallest rational value. * Round up this value and check whether it is possible to attain * a strictly greater integer value. * If so, the variable is not restricted to a single integer value. * Otherwise, the search stops at the greatest rational value. * If rounding down this value yields a value that is different * from rounding up the smallest rational value, then the variable * cannot attain any integer value. Mark the tableau empty. * Otherwise, add an equality constraint that fixes the variable * to the single integer value found. */ static isl_bool detect_constant_with_tmp(struct isl_tab *tab, struct isl_tab_var *var, isl_int *target, isl_int *tmp) { … } /* Check if variable "var" of "tab" can only attain a single (integer) * value, and, if so, add an equality constraint to fix the variable * to this single value and store the result in "value" (if "value" * is not NULL). * * If the current sample value involves the big parameter, * then the variable cannot have a fixed integer value. * If the variable is already fixed to a single value by its row, then * there is no need to add another equality constraint. * * Otherwise, allocate some temporary variables and continue * with detect_constant_with_tmp. */ static isl_bool get_constant(struct isl_tab *tab, struct isl_tab_var *var, isl_int *value) { … } /* Check if variable "var" of "tab" can only attain a single (integer) * value, and, if so, add an equality constraint to fix the variable * to this single value and store the result in "value" (if "value" * is not NULL). * * For rational tableaus, nothing needs to be done. */ isl_bool isl_tab_is_constant(struct isl_tab *tab, int var, isl_int *value) { … } /* Check if any of the variables of "tab" can only attain a single (integer) * value, and, if so, add equality constraints to fix those variables * to these single values. * * For rational tableaus, nothing needs to be done. */ isl_stat isl_tab_detect_constants(struct isl_tab *tab) { … } /* Take a snapshot of the tableau that can be restored by a call to * isl_tab_rollback. */ struct isl_tab_undo *isl_tab_snap(struct isl_tab *tab) { … } /* Does "tab" need to keep track of undo information? * That is, was a snapshot taken that may need to be restored? */ isl_bool isl_tab_need_undo(struct isl_tab *tab) { … } /* Remove all tracking of undo information from "tab", invalidating * any snapshots that may have been taken of the tableau. * Since all snapshots have been invalidated, there is also * no need to start keeping track of undo information again. */ void isl_tab_clear_undo(struct isl_tab *tab) { … } /* Undo the operation performed by isl_tab_relax. */ static isl_stat unrelax(struct isl_tab *tab, struct isl_tab_var *var) WARN_UNUSED; static isl_stat unrelax(struct isl_tab *tab, struct isl_tab_var *var) { … } /* Undo the operation performed by isl_tab_unrestrict. * * In particular, mark the variable as being non-negative and make * sure the sample value respects this constraint. */ static isl_stat ununrestrict(struct isl_tab *tab, struct isl_tab_var *var) { … } /* Unmark the last redundant row in "tab" as being redundant. * This undoes part of the modifications performed by isl_tab_mark_redundant. * In particular, remove the redundant mark and make * sure the sample value respects the constraint again. * A variable that is marked non-negative by isl_tab_mark_redundant * is covered by a separate undo record. */ static isl_stat restore_last_redundant(struct isl_tab *tab) { … } static isl_stat perform_undo_var(struct isl_tab *tab, struct isl_tab_undo *undo) WARN_UNUSED; static isl_stat perform_undo_var(struct isl_tab *tab, struct isl_tab_undo *undo) { … } /* Restore all rows that have been marked redundant by isl_tab_mark_redundant * and that have been preserved in the tableau. * Note that isl_tab_mark_redundant may also have marked some variables * as being non-negative before marking them redundant. These need * to be removed as well as otherwise some constraints could end up * getting marked redundant with respect to the variable. */ isl_stat isl_tab_restore_redundant(struct isl_tab *tab) { … } /* Undo the addition of an integer division to the basic map representation * of "tab" in position "pos". */ static isl_stat drop_bmap_div(struct isl_tab *tab, int pos) { … } /* Restore the tableau to the state where the basic variables * are those in "col_var". * We first construct a list of variables that are currently in * the basis, but shouldn't. Then we iterate over all variables * that should be in the basis and for each one that is currently * not in the basis, we exchange it with one of the elements of the * list constructed before. * We can always find an appropriate variable to pivot with because * the current basis is mapped to the old basis by a non-singular * matrix and so we can never end up with a zero row. */ static int restore_basis(struct isl_tab *tab, int *col_var) { … } /* Remove all samples with index n or greater, i.e., those samples * that were added since we saved this number of samples in * isl_tab_save_samples. */ static void drop_samples_since(struct isl_tab *tab, int n) { … } static isl_stat perform_undo(struct isl_tab *tab, struct isl_tab_undo *undo) WARN_UNUSED; static isl_stat perform_undo(struct isl_tab *tab, struct isl_tab_undo *undo) { … } /* Return the tableau to the state it was in when the snapshot "snap" * was taken. */ isl_stat isl_tab_rollback(struct isl_tab *tab, struct isl_tab_undo *snap) { … } /* The given row "row" represents an inequality violated by all * points in the tableau. Check for some special cases of such * separating constraints. * In particular, if the row has been reduced to the constant -1, * then we know the inequality is adjacent (but opposite) to * an equality in the tableau. * If the row has been reduced to r = c*(-1 -r'), with r' an inequality * of the tableau and c a positive constant, then the inequality * is adjacent (but opposite) to the inequality r'. */ static enum isl_ineq_type separation_type(struct isl_tab *tab, unsigned row) { … } /* Check the effect of inequality "ineq" on the tableau "tab". * The result may be * isl_ineq_redundant: satisfied by all points in the tableau * isl_ineq_separate: satisfied by no point in the tableau * isl_ineq_cut: satisfied by some by not all points * isl_ineq_adj_eq: adjacent to an equality * isl_ineq_adj_ineq: adjacent to an inequality. */ enum isl_ineq_type isl_tab_ineq_type(struct isl_tab *tab, isl_int *ineq) { … } isl_stat isl_tab_track_bmap(struct isl_tab *tab, __isl_take isl_basic_map *bmap) { … } isl_stat isl_tab_track_bset(struct isl_tab *tab, __isl_take isl_basic_set *bset) { … } __isl_keep isl_basic_set *isl_tab_peek_bset(struct isl_tab *tab) { … } static void isl_tab_print_internal(__isl_keep struct isl_tab *tab, FILE *out, int indent) { … } void isl_tab_dump(__isl_keep struct isl_tab *tab) { … }
Codebase Browser
llvm