nexmon – Rev 1
?pathlinks?
/*
* Copyright 2008-2009 Katholieke Universiteit Leuven
*
* Use of this software is governed by the GNU LGPLv2.1 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/set.h>
#include <isl/map.h>
#include <isl/mat.h>
#include <isl/seq.h>
#include "isl_piplib.h"
#include "isl_map_piplib.h"
static void copy_values_from(isl_int *dst, Entier *src, unsigned n)
{
int i;
for (i = 0; i < n; ++i)
entier_assign(dst[i], src[i]);
}
static void add_value(isl_int *dst, Entier *src)
{
mpz_add(*dst, *dst, *src);
}
static void copy_constraint_from(isl_int *dst, PipVector *src,
unsigned nparam, unsigned n_in, unsigned n_out,
unsigned extra, int *pos)
{
int i;
copy_values_from(dst, src->the_vector+src->nb_elements-1, 1);
copy_values_from(dst+1, src->the_vector, nparam+n_in);
isl_seq_clr(dst+1+nparam+n_in, n_out);
isl_seq_clr(dst+1+nparam+n_in+n_out, extra);
for (i = 0; i + n_in + nparam < src->nb_elements-1; ++i) {
int p = pos[i];
add_value(&dst[1+nparam+n_in+n_out+p],
&src->the_vector[n_in+nparam+i]);
}
}
static int add_inequality(struct isl_ctx *ctx,
struct isl_basic_map *bmap, int *pos, PipVector *vec)
{
unsigned nparam = isl_basic_map_n_param(bmap);
unsigned n_in = isl_basic_map_n_in(bmap);
unsigned n_out = isl_basic_map_n_out(bmap);
unsigned n_div = isl_basic_map_n_div(bmap);
int i = isl_basic_map_alloc_inequality(bmap);
if (i < 0)
return -1;
copy_constraint_from(bmap->ineq[i], vec,
nparam, n_in, n_out, n_div, pos);
return i;
}
/* For a div d = floor(f/m), add the constraints
*
* f - m d >= 0
* -(f-(n-1)) + m d >= 0
*
* Note that the second constraint is the negation of
*
* f - m d >= n
*/
static int add_div_constraints(struct isl_ctx *ctx,
struct isl_basic_map *bmap, int *pos, PipNewparm *p, unsigned div)
{
int i, j;
unsigned total = isl_basic_map_total_dim(bmap);
unsigned div_pos = 1 + total - bmap->n_div + div;
i = add_inequality(ctx, bmap, pos, p->vector);
if (i < 0)
return -1;
copy_values_from(&bmap->ineq[i][div_pos], &p->deno, 1);
isl_int_neg(bmap->ineq[i][div_pos], bmap->ineq[i][div_pos]);
j = isl_basic_map_alloc_inequality(bmap);
if (j < 0)
return -1;
isl_seq_neg(bmap->ineq[j], bmap->ineq[i], 1 + total);
isl_int_add(bmap->ineq[j][0], bmap->ineq[j][0], bmap->ineq[j][div_pos]);
isl_int_sub_ui(bmap->ineq[j][0], bmap->ineq[j][0], 1);
return j;
}
static int add_equality(struct isl_ctx *ctx,
struct isl_basic_map *bmap, int *pos,
unsigned var, PipVector *vec)
{
int i;
unsigned nparam = isl_basic_map_n_param(bmap);
unsigned n_in = isl_basic_map_n_in(bmap);
unsigned n_out = isl_basic_map_n_out(bmap);
isl_assert(ctx, var < n_out, return -1);
i = isl_basic_map_alloc_equality(bmap);
if (i < 0)
return -1;
copy_constraint_from(bmap->eq[i], vec,
nparam, n_in, n_out, bmap->extra, pos);
isl_int_set_si(bmap->eq[i][1+nparam+n_in+var], -1);
return i;
}
static int find_div(struct isl_ctx *ctx,
struct isl_basic_map *bmap, int *pos, PipNewparm *p)
{
int i, j;
unsigned nparam = isl_basic_map_n_param(bmap);
unsigned n_in = isl_basic_map_n_in(bmap);
unsigned n_out = isl_basic_map_n_out(bmap);
i = isl_basic_map_alloc_div(bmap);
if (i < 0)
return -1;
copy_constraint_from(bmap->div[i]+1, p->vector,
nparam, n_in, n_out, bmap->extra, pos);
copy_values_from(bmap->div[i], &p->deno, 1);
for (j = 0; j < i; ++j)
if (isl_seq_eq(bmap->div[i], bmap->div[j],
1+1+isl_basic_map_total_dim(bmap)+j)) {
isl_basic_map_free_div(bmap, 1);
return j;
}
if (add_div_constraints(ctx, bmap, pos, p, i) < 0)
return -1;
return i;
}
/* Count some properties of a quast
* - maximal number of new parameters
* - maximal depth
* - total number of solutions
* - total number of empty branches
*/
static void quast_count(PipQuast *q, int *maxnew, int depth, int *maxdepth,
int *sol, int *nosol)
{
PipNewparm *p;
for (p = q->newparm; p; p = p->next)
if (p->rank > *maxnew)
*maxnew = p->rank;
if (q->condition) {
if (++depth > *maxdepth)
*maxdepth = depth;
quast_count(q->next_else, maxnew, depth, maxdepth, sol, nosol);
quast_count(q->next_then, maxnew, depth, maxdepth, sol, nosol);
} else {
if (q->list)
++(*sol);
else
++(*nosol);
}
}
/*
* pos: array of length bmap->set.extra, mapping each of the existential
* variables PIP proposes to an existential variable in bmap
* bmap: collects the currently active constraints
* rest: collects the empty leaves of the quast (if not NULL)
*/
struct scan_data {
struct isl_ctx *ctx;
struct isl_basic_map *bmap;
struct isl_set **rest;
int *pos;
};
/*
* New existentially quantified variables are places after the existing ones.
*/
static struct isl_map *scan_quast_r(struct scan_data *data, PipQuast *q,
struct isl_map *map)
{
PipNewparm *p;
struct isl_basic_map *bmap = data->bmap;
unsigned old_n_div = bmap->n_div;
unsigned nparam = isl_basic_map_n_param(bmap);
unsigned n_in = isl_basic_map_n_in(bmap);
unsigned n_out = isl_basic_map_n_out(bmap);
if (!map)
goto error;
for (p = q->newparm; p; p = p->next) {
int pos;
unsigned pip_param = nparam + n_in;
pos = find_div(data->ctx, bmap, data->pos, p);
if (pos < 0)
goto error;
data->pos[p->rank - pip_param] = pos;
}
if (q->condition) {
int pos = add_inequality(data->ctx, bmap, data->pos,
q->condition);
if (pos < 0)
goto error;
map = scan_quast_r(data, q->next_then, map);
if (isl_inequality_negate(bmap, pos))
goto error;
map = scan_quast_r(data, q->next_else, map);
if (isl_basic_map_free_inequality(bmap, 1))
goto error;
} else if (q->list) {
PipList *l;
int j;
/* if bmap->n_out is zero, we are only interested in the domains
* where a solution exists and not in the actual solution
*/
for (j = 0, l = q->list; j < n_out && l; ++j, l = l->next)
if (add_equality(data->ctx, bmap, data->pos, j,
l->vector) < 0)
goto error;
map = isl_map_add_basic_map(map, isl_basic_map_copy(bmap));
if (isl_basic_map_free_equality(bmap, n_out))
goto error;
} else if (data->rest) {
struct isl_basic_set *bset;
bset = isl_basic_set_from_basic_map(isl_basic_map_copy(bmap));
bset = isl_basic_set_drop_dims(bset, n_in, n_out);
if (!bset)
goto error;
*data->rest = isl_set_add_basic_set(*data->rest, bset);
}
if (isl_basic_map_free_inequality(bmap, 2*(bmap->n_div - old_n_div)))
goto error;
if (isl_basic_map_free_div(bmap, bmap->n_div - old_n_div))
goto error;
return map;
error:
isl_map_free(map);
return NULL;
}
/*
* Returns a map of dimension "keep_dim" with "context" as domain and
* as range the first "isl_space_dim(keep_dim, isl_dim_out)" variables
* in the quast lists.
*/
static struct isl_map *isl_map_from_quast(struct isl_ctx *ctx, PipQuast *q,
isl_space *keep_dim,
struct isl_basic_set *context,
struct isl_set **rest)
{
int pip_param;
int nexist;
int max_depth;
int n_sol, n_nosol;
struct scan_data data;
struct isl_map *map = NULL;
isl_space *dims;
unsigned nparam;
unsigned dim;
unsigned keep;
data.ctx = ctx;
data.rest = rest;
data.bmap = NULL;
data.pos = NULL;
if (!context || !keep_dim)
goto error;
dim = isl_basic_set_n_dim(context);
nparam = isl_basic_set_n_param(context);
keep = isl_space_dim(keep_dim, isl_dim_out);
pip_param = nparam + dim;
max_depth = 0;
n_sol = 0;
n_nosol = 0;
nexist = pip_param-1;
quast_count(q, &nexist, 0, &max_depth, &n_sol, &n_nosol);
nexist -= pip_param-1;
if (rest) {
*rest = isl_set_alloc_space(isl_space_copy(context->dim), n_nosol,
ISL_MAP_DISJOINT);
if (!*rest)
goto error;
}
map = isl_map_alloc_space(isl_space_copy(keep_dim), n_sol,
ISL_MAP_DISJOINT);
if (!map)
goto error;
dims = isl_space_reverse(isl_space_copy(context->dim));
data.bmap = isl_basic_map_from_basic_set(context, dims);
data.bmap = isl_basic_map_extend_space(data.bmap,
keep_dim, nexist, keep, max_depth+2*nexist);
if (!data.bmap)
goto error2;
if (data.bmap->extra) {
int i;
data.pos = isl_alloc_array(ctx, int, data.bmap->extra);
if (!data.pos)
goto error;
for (i = 0; i < data.bmap->n_div; ++i)
data.pos[i] = i;
}
map = scan_quast_r(&data, q, map);
map = isl_map_finalize(map);
if (!map)
goto error2;
if (rest) {
*rest = isl_set_finalize(*rest);
if (!*rest)
goto error2;
}
isl_basic_map_free(data.bmap);
if (data.pos)
free(data.pos);
return map;
error:
isl_basic_set_free(context);
isl_space_free(keep_dim);
error2:
if (data.pos)
free(data.pos);
isl_basic_map_free(data.bmap);
isl_map_free(map);
if (rest) {
isl_set_free(*rest);
*rest = NULL;
}
return NULL;
}
static void copy_values_to(Entier *dst, isl_int *src, unsigned n)
{
int i;
for (i = 0; i < n; ++i)
entier_assign(dst[i], src[i]);
}
static void copy_constraint_to(Entier *dst, isl_int *src,
unsigned pip_param, unsigned pip_var,
unsigned extra_front, unsigned extra_back)
{
copy_values_to(dst+1+extra_front+pip_var+pip_param+extra_back, src, 1);
copy_values_to(dst+1+extra_front+pip_var, src+1, pip_param);
copy_values_to(dst+1+extra_front, src+1+pip_param, pip_var);
}
PipMatrix *isl_basic_map_to_pip(struct isl_basic_map *bmap, unsigned pip_param,
unsigned extra_front, unsigned extra_back)
{
int i;
unsigned nrow;
unsigned ncol;
PipMatrix *M;
unsigned off;
unsigned pip_var = isl_basic_map_total_dim(bmap) - pip_param;
nrow = extra_front + bmap->n_eq + bmap->n_ineq;
ncol = 1 + extra_front + pip_var + pip_param + extra_back + 1;
M = pip_matrix_alloc(nrow, ncol);
if (!M)
return NULL;
off = extra_front;
for (i = 0; i < bmap->n_eq; ++i) {
entier_set_si(M->p[off+i][0], 0);
copy_constraint_to(M->p[off+i], bmap->eq[i],
pip_param, pip_var, extra_front, extra_back);
}
off += bmap->n_eq;
for (i = 0; i < bmap->n_ineq; ++i) {
entier_set_si(M->p[off+i][0], 1);
copy_constraint_to(M->p[off+i], bmap->ineq[i],
pip_param, pip_var, extra_front, extra_back);
}
return M;
}
PipMatrix *isl_basic_set_to_pip(struct isl_basic_set *bset, unsigned pip_param,
unsigned extra_front, unsigned extra_back)
{
return isl_basic_map_to_pip((struct isl_basic_map *)bset,
pip_param, extra_front, extra_back);
}
struct isl_map *isl_pip_basic_map_lexopt(
struct isl_basic_map *bmap, struct isl_basic_set *dom,
struct isl_set **empty, int max)
{
PipOptions *options;
PipQuast *sol;
struct isl_map *map;
struct isl_ctx *ctx;
PipMatrix *domain = NULL, *context = NULL;
unsigned nparam, n_in, n_out;
bmap = isl_basic_map_detect_equalities(bmap);
if (!bmap || !dom)
goto error;
ctx = bmap->ctx;
isl_assert(ctx, isl_basic_map_compatible_domain(bmap, dom), goto error);
nparam = isl_basic_map_n_param(bmap);
n_in = isl_basic_map_n_in(bmap);
n_out = isl_basic_map_n_out(bmap);
domain = isl_basic_map_to_pip(bmap, nparam + n_in, 0, dom->n_div);
if (!domain)
goto error;
context = isl_basic_map_to_pip((struct isl_basic_map *)dom, 0, 0, 0);
if (!context)
goto error;
options = pip_options_init();
options->Simplify = 1;
options->Maximize = max;
options->Urs_unknowns = -1;
options->Urs_parms = -1;
sol = pip_solve(domain, context, -1, options);
if (sol) {
struct isl_basic_set *copy;
copy = isl_basic_set_copy(dom);
map = isl_map_from_quast(ctx, sol,
isl_space_copy(bmap->dim), copy, empty);
} else {
map = isl_map_empty_like_basic_map(bmap);
if (empty)
*empty = NULL;
}
if (!map)
goto error;
if (map->n == 0 && empty) {
isl_set_free(*empty);
*empty = isl_set_from_basic_set(dom);
} else
isl_basic_set_free(dom);
isl_basic_map_free(bmap);
pip_quast_free(sol);
pip_options_free(options);
pip_matrix_free(domain);
pip_matrix_free(context);
return map;
error:
if (domain)
pip_matrix_free(domain);
if (context)
pip_matrix_free(context);
isl_basic_map_free(bmap);
isl_basic_set_free(dom);
return NULL;
}