Viewing file:  isl_tab_lexopt_templ.c (7.49 KB) -rw-r--r--
Select action/file-type:
 (+) |  (+) |  (+) | Code (+) | Session (+) |  (+) | SDB (+) |  (+) |  (+) |  (+) |  (+) |  (+) |
/*
* Copyright 2008-2009 Katholieke Universiteit Leuven
* Copyright 2010 INRIA Saclay
* Copyright 2011 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 INRIA Saclay - Ile-de-France, Parc Club Orsay Universite,
* ZAC des vignes, 4 rue Jacques Monod, 91893 Orsay, France
*/
#define xSF(TYPE,SUFFIX) TYPE ## SUFFIX
#define SF(TYPE,SUFFIX) xSF(TYPE,SUFFIX)
/* Given a basic map with at least two parallel constraints (as found
* by the function parallel_constraints), first look for more constraints
* parallel to the two constraint and replace the found list of parallel
* constraints by a single constraint with as "input" part the minimum
* of the input parts of the list of constraints. Then, recursively call
* basic_map_partial_lexopt (possibly finding more parallel constraints)
* and plug in the definition of the minimum in the result.
*
* As in parallel_constraints, only inequality constraints that only
* involve input variables that do not occur in any other inequality
* constraints are considered.
*
* More specifically, given a set of constraints
*
* a x + b_i(p) >= 0
*
* Replace this set by a single constraint
*
* a x + u >= 0
*
* with u a new parameter with constraints
*
* u <= b_i(p)
*
* Any solution to the new system is also a solution for the original system
* since
*
* a x >= -u >= -b_i(p)
*
* Moreover, m = min_i(b_i(p)) satisfies the constraints on u and can
* therefore be plugged into the solution.
*/
static TYPE *SF(basic_map_partial_lexopt_symm,SUFFIX)(
__isl_take isl_basic_map *bmap, __isl_take isl_basic_set *dom,
__isl_give isl_set **empty, int max, int first, int second)
{
int i, n, k;
int *list = NULL;
isl_size bmap_in, bmap_param, bmap_all;
unsigned n_in, n_out, n_div;
isl_ctx *ctx;
isl_vec *var = NULL;
isl_mat *cst = NULL;
isl_space *map_space, *set_space;
map_space = isl_basic_map_get_space(bmap);
set_space = empty ? isl_basic_set_get_space(dom) : NULL;
bmap_in = isl_basic_map_dim(bmap, isl_dim_in);
bmap_param = isl_basic_map_dim(bmap, isl_dim_param);
bmap_all = isl_basic_map_dim(bmap, isl_dim_all);
if (bmap_in < 0 || bmap_param < 0 || bmap_all < 0)
goto error;
n_in = bmap_param + bmap_in;
n_out = bmap_all - n_in;
ctx = isl_basic_map_get_ctx(bmap);
list = isl_alloc_array(ctx, int, bmap->n_ineq);
var = isl_vec_alloc(ctx, n_out);
if ((bmap->n_ineq && !list) || (n_out && !var))
goto error;
list[0] = first;
list[1] = second;
isl_seq_cpy(var->el, bmap->ineq[first] + 1 + n_in, n_out);
for (i = second + 1, n = 2; i < bmap->n_ineq; ++i) {
if (isl_seq_eq(var->el, bmap->ineq[i] + 1 + n_in, n_out) &&
all_single_occurrence(bmap, i, n_in))
list[n++] = i;
}
cst = isl_mat_alloc(ctx, n, 1 + n_in);
if (!cst)
goto error;
for (i = 0; i < n; ++i)
isl_seq_cpy(cst->row[i], bmap->ineq[list[i]], 1 + n_in);
bmap = isl_basic_map_cow(bmap);
if (!bmap)
goto error;
for (i = n - 1; i >= 0; --i)
if (isl_basic_map_drop_inequality(bmap, list[i]) < 0)
goto error;
bmap = isl_basic_map_add_dims(bmap, isl_dim_in, 1);
bmap = isl_basic_map_extend_constraints(bmap, 0, 1);
k = isl_basic_map_alloc_inequality(bmap);
if (k < 0)
goto error;
isl_seq_clr(bmap->ineq[k], 1 + n_in);
isl_int_set_si(bmap->ineq[k][1 + n_in], 1);
isl_seq_cpy(bmap->ineq[k] + 1 + n_in + 1, var->el, n_out);
bmap = isl_basic_map_finalize(bmap);
n_div = isl_basic_set_dim(dom, isl_dim_div);
dom = isl_basic_set_add_dims(dom, isl_dim_set, 1);
dom = isl_basic_set_extend_constraints(dom, 0, n);
for (i = 0; i < n; ++i) {
k = isl_basic_set_alloc_inequality(dom);
if (k < 0)
goto error;
isl_seq_cpy(dom->ineq[k], cst->row[i], 1 + n_in);
isl_int_set_si(dom->ineq[k][1 + n_in], -1);
isl_seq_clr(dom->ineq[k] + 1 + n_in + 1, n_div);
}
isl_vec_free(var);
free(list);
return SF(basic_map_partial_lexopt_symm_core,SUFFIX)(bmap, dom, empty,
max, cst, map_space, set_space);
error:
isl_space_free(map_space);
isl_space_free(set_space);
isl_mat_free(cst);
isl_vec_free(var);
free(list);
isl_basic_set_free(dom);
isl_basic_map_free(bmap);
return NULL;
}
/* Recursive part of isl_tab_basic_map_partial_lexopt*, after detecting
* equalities and removing redundant constraints.
*
* We first check if there are any parallel constraints (left).
* If not, we are in the base case.
* If there are parallel constraints, we replace them by a single
* constraint in basic_map_partial_lexopt_symm_pma and then call
* this function recursively to look for more parallel constraints.
*/
static __isl_give TYPE *SF(basic_map_partial_lexopt,SUFFIX)(
__isl_take isl_basic_map *bmap, __isl_take isl_basic_set *dom,
__isl_give isl_set **empty, int max)
{
isl_bool par = isl_bool_false;
int first, second;
if (!bmap)
goto error;
if (bmap->ctx->opt->pip_symmetry)
par = parallel_constraints(bmap, &first, &second);
if (par < 0)
goto error;
if (!par)
return SF(basic_map_partial_lexopt_base,SUFFIX)(bmap, dom,
empty, max);
return SF(basic_map_partial_lexopt_symm,SUFFIX)(bmap, dom, empty, max,
first, second);
error:
isl_basic_set_free(dom);
isl_basic_map_free(bmap);
return NULL;
}
/* Compute the lexicographic minimum (or maximum if "flags" includes
* ISL_OPT_MAX) of "bmap" over the domain "dom" and return the result as
* either a map or a piecewise multi-affine expression depending on TYPE.
* If "empty" is not NULL, then *empty is assigned a set that
* contains those parts of the domain where there is no solution.
* If "flags" includes ISL_OPT_FULL, then "dom" is NULL and the optimum
* should be computed over the domain of "bmap". "empty" is also NULL
* in this case.
* If "bmap" is marked as rational (ISL_BASIC_MAP_RATIONAL),
* then we compute the rational optimum. Otherwise, we compute
* the integral optimum.
*
* We perform some preprocessing. As the PILP solver does not
* handle implicit equalities very well, we first make sure all
* the equalities are explicitly available.
*
* We also add context constraints to the basic map and remove
* redundant constraints. This is only needed because of the
* way we handle simple symmetries. In particular, we currently look
* for symmetries on the constraints, before we set up the main tableau.
* It is then no good to look for symmetries on possibly redundant constraints.
* If the domain was extracted from the basic map, then there is
* no need to add back those constraints again.
*/
__isl_give TYPE *SF(isl_tab_basic_map_partial_lexopt,SUFFIX)(
__isl_take isl_basic_map *bmap, __isl_take isl_basic_set *dom,
__isl_give isl_set **empty, unsigned flags)
{
int max, full;
isl_bool compatible;
if (empty)
*empty = NULL;
full = ISL_FL_ISSET(flags, ISL_OPT_FULL);
if (full)
dom = extract_domain(bmap, flags);
compatible = isl_basic_map_compatible_domain(bmap, dom);
if (compatible < 0)
goto error;
if (!compatible)
isl_die(isl_basic_map_get_ctx(bmap), isl_error_invalid,
"domain does not match input", goto error);
max = ISL_FL_ISSET(flags, ISL_OPT_MAX);
if (isl_basic_set_dim(dom, isl_dim_all) == 0)
return SF(basic_map_partial_lexopt,SUFFIX)(bmap, dom, empty,
max);
if (!full)
bmap = isl_basic_map_intersect_domain(bmap,
isl_basic_set_copy(dom));
bmap = isl_basic_map_detect_equalities(bmap);
bmap = isl_basic_map_remove_redundancies(bmap);
return SF(basic_map_partial_lexopt,SUFFIX)(bmap, dom, empty, max);
error:
isl_basic_set_free(dom);
isl_basic_map_free(bmap);
return NULL;
}
|
