isl_tab_lexopt_templ.c

   1 /*
   2  * Copyright 2008-2009 Katholieke Universiteit Leuven
   3  * Copyright 2010      INRIA Saclay
   4  * Copyright 2011      Sven Verdoolaege
   5  *
   6  * Use of this software is governed by the MIT license
   7  *
   8  * Written by Sven Verdoolaege, K.U.Leuven, Departement
   9  * Computerwetenschappen, Celestijnenlaan 200A, B-3001 Leuven, Belgium
  10  * and INRIA Saclay - Ile-de-France, Parc Club Orsay Universite,
  11  * ZAC des vignes, 4 rue Jacques Monod, 91893 Orsay, France
  12  */
  13
  14 #define xSF(TYPE,SUFFIX) TYPE ## SUFFIX
  15 #define SF(TYPE,SUFFIX) xSF(TYPE,SUFFIX)
  16
  17 /* Given a basic map with at least two parallel constraints (as found
  18  * by the function parallel_constraints), first look for more constraints
  19  * parallel to the two constraint and replace the found list of parallel
  20  * constraints by a single constraint with as "input" part the minimum
  21  * of the input parts of the list of constraints.  Then, recursively call
  22  * basic_map_partial_lexopt (possibly finding more parallel constraints)
  23  * and plug in the definition of the minimum in the result.
  24  *
  25  * As in parallel_constraints, only inequality constraints that only
  26  * involve input variables that do not occur in any other inequality
  27  * constraints are considered.
  28  *
  29  * More specifically, given a set of constraints
  30  *
  31  *      a x + b_i(p) >= 0
  32  *
  33  * Replace this set by a single constraint
  34  *
  35  *      a x + u >= 0
  36  *
  37  * with u a new parameter with constraints
  38  *
  39  *      u <= b_i(p)
  40  *
  41  * Any solution to the new system is also a solution for the original system
  42  * since
  43  *
  44  *      a x >= -u >= -b_i(p)
  45  *
  46  * Moreover, m = min_i(b_i(p)) satisfies the constraints on u and can
  47  * therefore be plugged into the solution.
  48  */
  49 static TYPE *SF(basic_map_partial_lexopt_symm,SUFFIX)(
  50         __isl_take isl_basic_map *bmap, __isl_take isl_basic_set *dom,
  51         __isl_give isl_set **empty, int max, int first, int second)
  52 {
  53         int i, n, k;
  54         int *list = NULL;
  55         unsigned n_in, n_out, n_div;
  56         isl_ctx *ctx;
  57         isl_vec *var = NULL;
  58         isl_mat *cst = NULL;
  59         isl_space *map_space, *set_space;
  60
  61         map_space = isl_basic_map_get_space(bmap);
  62         set_space = empty ? isl_basic_set_get_space(dom) : NULL;
  63
  64         n_in = isl_basic_map_dim(bmap, isl_dim_param) +
  65                isl_basic_map_dim(bmap, isl_dim_in);
  66         n_out = isl_basic_map_dim(bmap, isl_dim_all) - n_in;
  67
  68         ctx = isl_basic_map_get_ctx(bmap);
  69         list = isl_alloc_array(ctx, int, bmap->n_ineq);
  70         var = isl_vec_alloc(ctx, n_out);
  71         if ((bmap->n_ineq && !list) || (n_out && !var))
  72                 goto error;
  73
  74         list[0] = first;
  75         list[1] = second;
  76         isl_seq_cpy(var->el, bmap->ineq[first] + 1 + n_in, n_out);
  77         for (i = second + 1, n = 2; i < bmap->n_ineq; ++i) {
  78                 if (isl_seq_eq(var->el, bmap->ineq[i] + 1 + n_in, n_out) &&
  79                     all_single_occurrence(bmap, i, n_in))
  80                         list[n++] = i;
  81         }
  82
  83         cst = isl_mat_alloc(ctx, n, 1 + n_in);
  84         if (!cst)
  85                 goto error;
  86
  87         for (i = 0; i < n; ++i)
  88                 isl_seq_cpy(cst->row[i], bmap->ineq[list[i]], 1 + n_in);
  89
  90         bmap = isl_basic_map_cow(bmap);
  91         if (!bmap)
  92                 goto error;
  93         for (i = n - 1; i >= 0; --i)
  94                 if (isl_basic_map_drop_inequality(bmap, list[i]) < 0)
  95                         goto error;
  96
  97         bmap = isl_basic_map_add_dims(bmap, isl_dim_in, 1);
  98         bmap = isl_basic_map_extend_constraints(bmap, 0, 1);
  99         k = isl_basic_map_alloc_inequality(bmap);
 100         if (k < 0)
 101                 goto error;
 102         isl_seq_clr(bmap->ineq[k], 1 + n_in);
 103         isl_int_set_si(bmap->ineq[k][1 + n_in], 1);
 104         isl_seq_cpy(bmap->ineq[k] + 1 + n_in + 1, var->el, n_out);
 105         bmap = isl_basic_map_finalize(bmap);
 106
 107         n_div = isl_basic_set_dim(dom, isl_dim_div);
 108         dom = isl_basic_set_add_dims(dom, isl_dim_set, 1);
 109         dom = isl_basic_set_extend_constraints(dom, 0, n);
 110         for (i = 0; i < n; ++i) {
 111                 k = isl_basic_set_alloc_inequality(dom);
 112                 if (k < 0)
 113                         goto error;
 114                 isl_seq_cpy(dom->ineq[k], cst->row[i], 1 + n_in);
 115                 isl_int_set_si(dom->ineq[k][1 + n_in], -1);
 116                 isl_seq_clr(dom->ineq[k] + 1 + n_in + 1, n_div);
 117         }
 118
 119         isl_vec_free(var);
 120         free(list);
 121
 122         return SF(basic_map_partial_lexopt_symm_core,SUFFIX)(bmap, dom, empty,
 123                                                 max, cst, map_space, set_space);
 124 error:
 125         isl_space_free(map_space);
 126         isl_space_free(set_space);
 127         isl_mat_free(cst);
 128         isl_vec_free(var);
 129         free(list);
 130         isl_basic_set_free(dom);
 131         isl_basic_map_free(bmap);
 132         return NULL;
 133 }
 134
 135 /* Recursive part of isl_tab_basic_map_partial_lexopt*, after detecting
 136  * equalities and removing redundant constraints.
 137  *
 138  * We first check if there are any parallel constraints (left).
 139  * If not, we are in the base case.
 140  * If there are parallel constraints, we replace them by a single
 141  * constraint in basic_map_partial_lexopt_symm_pma and then call
 142  * this function recursively to look for more parallel constraints.
 143  */
 144 static __isl_give TYPE *SF(basic_map_partial_lexopt,SUFFIX)(
 145         __isl_take isl_basic_map *bmap, __isl_take isl_basic_set *dom,
 146         __isl_give isl_set **empty, int max)
 147 {
 148         int par = 0;
 149         int first, second;
 150
 151         if (!bmap)
 152                 goto error;
 153
 154         if (bmap->ctx->opt->pip_symmetry)
 155                 par = parallel_constraints(bmap, &first, &second);
 156         if (par < 0)
 157                 goto error;
 158         if (!par)
 159                 return SF(basic_map_partial_lexopt_base,SUFFIX)(bmap, dom,
 160                                                                 empty, max);
 161
 162         return SF(basic_map_partial_lexopt_symm,SUFFIX)(bmap, dom, empty, max,
 163                                                          first, second);
 164 error:
 165         isl_basic_set_free(dom);
 166         isl_basic_map_free(bmap);
 167         return NULL;
 168 }
 169
 170 /* Compute the lexicographic minimum (or maximum if "max" is set)
 171  * of "bmap" over the domain "dom" and return the result as
 172  * either a map or a piecewise multi-affine expression depending on TYPE.
 173  * If "empty" is not NULL, then *empty is assigned a set that
 174  * contains those parts of the domain where there is no solution.
 175  * If "bmap" is marked as rational (ISL_BASIC_MAP_RATIONAL),
 176  * then we compute the rational optimum.  Otherwise, we compute
 177  * the integral optimum.
 178  *
 179  * We perform some preprocessing.  As the PILP solver does not
 180  * handle implicit equalities very well, we first make sure all
 181  * the equalities are explicitly available.
 182  *
 183  * We also add context constraints to the basic map and remove
 184  * redundant constraints.  This is only needed because of the
 185  * way we handle simple symmetries.  In particular, we currently look
 186  * for symmetries on the constraints, before we set up the main tableau.
 187  * It is then no good to look for symmetries on possibly redundant constraints.
 188  */
 189 __isl_give TYPE *SF(isl_tab_basic_map_partial_lexopt,SUFFIX)(
 190         __isl_take isl_basic_map *bmap, __isl_take isl_basic_set *dom,
 191         __isl_give isl_set **empty, int max)
 192 {
 193         if (empty)
 194                 *empty = NULL;
 195         if (!bmap || !dom)
 196                 goto error;
 197
 198         isl_assert(bmap->ctx,
 199             isl_basic_map_compatible_domain(bmap, dom), goto error);
 200
 201         if (isl_basic_set_dim(dom, isl_dim_all) == 0)
 202                 return SF(basic_map_partial_lexopt,SUFFIX)(bmap, dom, empty,
 203                                                             max);
 204
 205         bmap = isl_basic_map_intersect_domain(bmap, isl_basic_set_copy(dom));
 206         bmap = isl_basic_map_detect_equalities(bmap);
 207         bmap = isl_basic_map_remove_redundancies(bmap);
 208
 209         return SF(basic_map_partial_lexopt,SUFFIX)(bmap, dom, empty, max);
 210 error:
 211         isl_basic_set_free(dom);
 212         isl_basic_map_free(bmap);
 213         return NULL;
 214 }