#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"
#include "isl_map_private.h"
+#include "isl_equalities.h"
static void copy_values_from(isl_int *dst, Entier *src, unsigned n)
{
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,
- bmap->nparam, bmap->n_in, bmap->n_out, bmap->extra, pos);
+ nparam, n_in, n_out, n_div, pos);
return i;
}
struct isl_basic_map *bmap, int *pos, PipNewparm *p, unsigned div)
{
int i, j;
- unsigned div_pos = 1 + bmap->nparam + bmap->n_in + bmap->n_out + div;
- unsigned total = bmap->nparam + bmap->n_in + bmap->n_out + bmap->extra;
+ 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)
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 < bmap->n_out, return -1);
+ 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,
- bmap->nparam, bmap->n_in, bmap->n_out, bmap->extra, pos);
- isl_int_set_si(bmap->eq[i][1+bmap->nparam+bmap->n_in+var], -1);
+ nparam, n_in, n_out, bmap->extra, pos);
+ isl_int_set_si(bmap->eq[i][1+nparam+n_in+var], -1);
return i;
}
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,
- bmap->nparam, bmap->n_in, bmap->n_out, bmap->extra, pos);
+ 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+bmap->nparam+bmap->n_in+bmap->n_out+j)) {
+ 1+1+isl_basic_map_total_dim(bmap)+j)) {
isl_basic_map_free_div(bmap, 1);
return j;
}
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 = bmap->nparam + bmap->n_in;
+ unsigned pip_param = nparam + n_in;
pos = find_div(data->ctx, bmap, data->pos, p);
if (pos < 0)
/* 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 < bmap->n_out && l; ++j, l = l->next)
+ 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(map, isl_basic_map_copy(bmap));
- if (isl_basic_map_free_equality(bmap, bmap->n_out))
+ if (isl_basic_map_free_equality(bmap, n_out))
goto error;
- } else if (map->n && data->rest) {
- /* not interested in rest if no sol */
+ } 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_vars(bset, bmap->n_in, bmap->n_out);
+ bset = isl_basic_set_drop_dims(bset, n_in, n_out);
if (!bset)
goto error;
*data->rest = isl_set_add(*data->rest, bset);
}
/*
- * Returns a map with "context" as domain and as range the first
- * "keep" variables in the quast lists.
+ * Returns a map of dimension "keep_dim" with "context" as domain and
+ * as range the first "isl_dim_size(keep_dim, isl_dim_out)" variables
+ * in the quast lists.
*/
static struct isl_map *isl_map_from_quast(struct isl_ctx *ctx, PipQuast *q,
- unsigned keep,
+ struct isl_dim *keep_dim,
struct isl_basic_set *context,
struct isl_set **rest)
{
int max_depth;
int n_sol, n_nosol;
struct scan_data data;
- struct isl_map *map;
+ struct isl_map *map = NULL;
+ struct isl_dim *dims;
unsigned nparam;
+ unsigned dim;
+ unsigned keep;
data.ctx = ctx;
data.rest = rest;
data.bmap = NULL;
data.pos = NULL;
- if (!context)
+ if (!context || !keep_dim)
goto error;
- nparam = context->nparam;
- pip_param = nparam + context->dim;
+ dim = isl_basic_set_n_dim(context);
+ nparam = isl_basic_set_n_param(context);
+ keep = isl_dim_size(keep_dim, isl_dim_out);
+ pip_param = nparam + dim;
max_depth = 0;
n_sol = 0;
nexist -= pip_param-1;
if (rest) {
- *rest = isl_set_alloc(data.ctx, nparam, context->dim, n_nosol,
+ *rest = isl_set_alloc_dim(isl_dim_copy(context->dim), n_nosol,
ISL_MAP_DISJOINT);
if (!*rest)
goto error;
}
- map = isl_map_alloc(data.ctx, nparam, context->dim, keep, n_sol,
+ map = isl_map_alloc_dim(isl_dim_copy(keep_dim), n_sol,
ISL_MAP_DISJOINT);
if (!map)
goto error;
- data.bmap = isl_basic_map_from_basic_set(context,
- context->dim, 0);
- data.bmap = isl_basic_map_extend(data.bmap,
- nparam, data.bmap->n_in, keep, nexist, keep, max_depth+2*nexist);
+ dims = isl_dim_reverse(isl_dim_copy(context->dim));
+ data.bmap = isl_basic_map_from_basic_set(context, dims);
+ data.bmap = isl_basic_map_extend_dim(data.bmap,
+ keep_dim, nexist, keep, max_depth+2*nexist);
if (!data.bmap)
- goto error;
+ goto error2;
if (data.bmap->extra) {
int i;
map = scan_quast_r(&data, q, map);
map = isl_map_finalize(map);
if (!map)
- goto error;
+ goto error2;
if (rest) {
*rest = isl_set_finalize(*rest);
if (!*rest)
- goto error;
+ goto error2;
}
isl_basic_map_free(data.bmap);
if (data.pos)
free(data.pos);
return map;
error:
+ isl_basic_set_free(context);
+ isl_dim_free(keep_dim);
+error2:
if (data.pos)
free(data.pos);
isl_basic_map_free(data.bmap);
unsigned ncol;
PipMatrix *M;
unsigned off;
- unsigned pip_var = bmap->nparam + bmap->n_in + bmap->n_out
- + bmap->n_div - pip_param;
+ 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;
return M;
}
-static struct isl_map *extremum_on(
+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)
{
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, bmap->nparam == dom->nparam, goto error);
- isl_assert(ctx, bmap->n_in == dom->dim, goto error);
+ 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, bmap->nparam + bmap->n_in,
- 0, dom->n_div);
+ 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 (sol) {
struct isl_basic_set *copy;
copy = isl_basic_set_copy(dom);
- map = isl_map_from_quast(ctx, sol, bmap->n_out, copy, empty);
+ map = isl_map_from_quast(ctx, sol,
+ isl_dim_copy(bmap->dim), copy, empty);
} else {
- map = isl_map_empty(ctx, bmap->nparam, bmap->n_in, bmap->n_out);
+ map = isl_map_empty_like_basic_map(bmap);
if (empty)
*empty = NULL;
}
return NULL;
}
-struct isl_map *isl_pip_basic_map_lexmax(
- struct isl_basic_map *bmap, struct isl_basic_set *dom,
- struct isl_set **empty)
-{
- return extremum_on(bmap, dom, empty, 1);
-}
-
-struct isl_map *isl_pip_basic_map_lexmin(
- struct isl_basic_map *bmap, struct isl_basic_set *dom,
- struct isl_set **empty)
-{
- return extremum_on(bmap, dom, empty, 0);
-}
-
-struct isl_map *isl_pip_basic_map_compute_divs(struct isl_basic_map *bmap)
+/* Project the given basic set onto its parameter domain, possibly introducing
+ * new, explicit, existential variables in the constraints.
+ * The input has parameters and output variables.
+ * The output has the same parameters, but no output variables, only
+ * explicit existentially quantified variables.
+ */
+static struct isl_set *compute_divs_no_eq(struct isl_basic_set *bset)
{
PipMatrix *domain = NULL, *context = NULL;
PipOptions *options;
PipQuast *sol;
struct isl_ctx *ctx;
+ struct isl_dim *dim;
struct isl_map *map;
struct isl_set *set;
struct isl_basic_set *dom;
- unsigned n_in;
- unsigned n_out;
+ unsigned nparam;
- if (!bmap)
+ if (!bset)
goto error;
- ctx = bmap->ctx;
- n_in = bmap->n_in;
- n_out = bmap->n_out;
+ ctx = bset->ctx;
+ nparam = isl_basic_set_n_param(bset);
- domain = isl_basic_map_to_pip(bmap, bmap->nparam + n_in + n_out, 0, 0);
+ domain = isl_basic_set_to_pip(bset, nparam, 0, 0);
if (!domain)
goto error;
- context = pip_matrix_alloc(0, bmap->nparam + n_in + n_out + 2);
+ context = pip_matrix_alloc(0, nparam + 2);
if (!context)
goto error;
options->Urs_parms = -1;
sol = pip_solve(domain, context, -1, options);
- dom = isl_basic_set_alloc(ctx, bmap->nparam, n_in + n_out, 0, 0, 0);
- map = isl_map_from_quast(ctx, sol, 0, dom, NULL);
+ dom = isl_basic_set_alloc(ctx, nparam, 0, 0, 0, 0);
+ map = isl_map_from_quast(ctx, sol, isl_dim_copy(dom->dim), dom, NULL);
+ set = (struct isl_set *)map;
pip_quast_free(sol);
pip_options_free(options);
pip_matrix_free(domain);
pip_matrix_free(context);
- isl_basic_map_free(bmap);
-
- set = isl_map_domain(map);
+ isl_basic_set_free(bset);
- return isl_map_from_set(set, n_in, n_out);
+ return set;
error:
if (domain)
pip_matrix_free(domain);
if (context)
pip_matrix_free(context);
isl_basic_set_free(dom);
+ isl_basic_set_free(bset);
+ return NULL;
+}
+
+static struct isl_map *isl_map_reset_dim(struct isl_map *map,
+ struct isl_dim *dim)
+{
+ int i;
+
+ if (!map || !dim)
+ goto error;
+
+ for (i = 0; i < map->n; ++i) {
+ isl_dim_free(map->p[i]->dim);
+ map->p[i]->dim = isl_dim_copy(dim);
+ }
+ isl_dim_free(map->dim);
+ map->dim = dim;
+
+ return map;
+error:
+ isl_map_free(map);
+ isl_dim_free(dim);
+ return NULL;
+}
+
+static struct isl_set *isl_set_reset_dim(struct isl_set *set,
+ struct isl_dim *dim)
+{
+ return (struct isl_set *) isl_map_reset_dim((struct isl_map *)set, dim);
+}
+
+/* Apply a preimage specified by "mat" on the parameters of "bset".
+ * bset is assumed to have only parameters and divs.
+ */
+static struct isl_basic_set *basic_set_parameter_preimage(
+ struct isl_basic_set *bset, struct isl_mat *mat)
+{
+ unsigned nparam;
+
+ if (!bset || !mat)
+ goto error;
+
+ bset->dim = isl_dim_cow(bset->dim);
+ if (!bset->dim)
+ goto error;
+
+ nparam = isl_basic_set_dim(bset, isl_dim_param);
+
+ isl_assert(bset->ctx, mat->n_row == 1 + nparam, goto error);
+
+ bset->dim->nparam = 0;
+ bset->dim->n_out = nparam;
+ bset = isl_basic_set_preimage(bset, mat);
+ if (bset) {
+ bset->dim->nparam = bset->dim->n_out;
+ bset->dim->n_out = 0;
+ }
+ return bset;
+error:
+ isl_mat_free(mat);
+ isl_basic_set_free(bset);
+ return NULL;
+}
+
+/* Apply a preimage specified by "mat" on the parameters of "set".
+ * set is assumed to have only parameters and divs.
+ */
+static struct isl_set *set_parameter_preimage(
+ struct isl_set *set, struct isl_mat *mat)
+{
+ struct isl_dim *dim = NULL;
+ unsigned nparam;
+
+ if (!set || !mat)
+ goto error;
+
+ dim = isl_dim_copy(set->dim);
+ dim = isl_dim_cow(dim);
+ if (!dim)
+ goto error;
+
+ nparam = isl_set_dim(set, isl_dim_param);
+
+ isl_assert(set->ctx, mat->n_row == 1 + nparam, goto error);
+
+ dim->nparam = 0;
+ dim->n_out = nparam;
+ isl_set_reset_dim(set, dim);
+ set = isl_set_preimage(set, mat);
+ if (!set)
+ goto error2;
+ dim = isl_dim_copy(set->dim);
+ dim = isl_dim_cow(dim);
+ if (!dim)
+ goto error2;
+ dim->nparam = dim->n_out;
+ dim->n_out = 0;
+ isl_set_reset_dim(set, dim);
+ return set;
+error:
+ isl_dim_free(dim);
+ isl_mat_free(mat);
+error2:
+ isl_set_free(set);
+ return NULL;
+}
+
+/* Intersect the basic set "bset" with the affine space specified by the
+ * equalities in "eq".
+ */
+static struct isl_basic_set *basic_set_append_equalities(
+ struct isl_basic_set *bset, struct isl_mat *eq)
+{
+ int i, k;
+ unsigned len;
+
+ if (!bset || !eq)
+ goto error;
+
+ bset = isl_basic_set_extend_dim(bset, isl_dim_copy(bset->dim), 0,
+ eq->n_row, 0);
+ if (!bset)
+ goto error;
+
+ len = 1 + isl_dim_total(bset->dim) + bset->extra;
+ for (i = 0; i < eq->n_row; ++i) {
+ k = isl_basic_set_alloc_equality(bset);
+ if (k < 0)
+ goto error;
+ isl_seq_cpy(bset->eq[k], eq->row[i], eq->n_col);
+ isl_seq_clr(bset->eq[k] + eq->n_col, len - eq->n_col);
+ }
+ isl_mat_free(eq);
+
+ return bset;
+error:
+ isl_mat_free(eq);
+ isl_basic_set_free(bset);
+ return NULL;
+}
+
+/* Intersect the set "set" with the affine space specified by the
+ * equalities in "eq".
+ */
+static struct isl_set *set_append_equalities(struct isl_set *set,
+ struct isl_mat *eq)
+{
+ int i;
+
+ if (!set || !eq)
+ goto error;
+
+ for (i = 0; i < set->n; ++i) {
+ set->p[i] = basic_set_append_equalities(set->p[i],
+ isl_mat_copy(eq));
+ if (!set->p[i])
+ goto error;
+ }
+ isl_mat_free(eq);
+ return set;
+error:
+ isl_mat_free(eq);
+ isl_set_free(set);
+ return NULL;
+}
+
+/* Project the given basic set onto its parameter domain, possibly introducing
+ * new, explicit, existential variables in the constraints.
+ * The input has parameters and (possibly implicit) existential variables.
+ * The output has the same parameters, but only
+ * explicit existentially quantified variables.
+ *
+ * The actual projection is performed by pip, but pip doesn't seem
+ * to like equalities very much, so we first remove the equalities
+ * among the parameters by performing a variable compression on
+ * the parameters. Afterward, an inverse transformation is performed
+ * and the equalities among the parameters are inserted back in.
+ */
+static struct isl_set *compute_divs(struct isl_basic_set *bset)
+{
+ int i, j;
+ struct isl_mat *eq;
+ struct isl_mat *T, *T2;
+ struct isl_set *set;
+ unsigned nparam, n_div;
+
+ bset = isl_basic_set_cow(bset);
+ if (!bset)
+ return NULL;
+
+ if (bset->n_eq == 0)
+ return compute_divs_no_eq(bset);
+
+ isl_basic_set_gauss(bset, NULL);
+
+ nparam = isl_basic_set_dim(bset, isl_dim_param);
+ n_div = isl_basic_set_dim(bset, isl_dim_div);
+
+ for (i = 0, j = n_div - 1; i < bset->n_eq && j >= 0; --j) {
+ if (!isl_int_is_zero(bset->eq[i][1 + nparam + j]))
+ ++i;
+ }
+ if (i == bset->n_eq)
+ return compute_divs_no_eq(bset);
+
+ eq = isl_mat_sub_alloc(bset->ctx, bset->eq, i, bset->n_eq - i,
+ 0, 1 + nparam);
+ eq = isl_mat_cow(eq);
+ T = isl_mat_variable_compression(isl_mat_copy(eq), &T2);
+ bset = basic_set_parameter_preimage(bset, T);
+
+ set = compute_divs_no_eq(bset);
+ set = set_parameter_preimage(set, T2);
+ set = set_append_equalities(set, eq);
+ return set;
+}
+
+/* Compute an explicit representation for all the existentially
+ * quantified variables.
+ * The input and output dimensions are first turned into parameters.
+ * compute_divs then returns a map with the same parameters and
+ * no input or output dimensions and the dimension specification
+ * is reset to that of the input.
+ */
+struct isl_map *isl_pip_basic_map_compute_divs(struct isl_basic_map *bmap)
+{
+ struct isl_basic_set *bset;
+ struct isl_set *set;
+ struct isl_map *map;
+ struct isl_dim *dim, *orig_dim = NULL;
+ unsigned nparam;
+ unsigned n_in;
+ unsigned n_out;
+
+ bmap = isl_basic_map_cow(bmap);
+ if (!bmap)
+ return NULL;
+
+ nparam = isl_basic_map_dim(bmap, isl_dim_param);
+ n_in = isl_basic_map_dim(bmap, isl_dim_in);
+ n_out = isl_basic_map_dim(bmap, isl_dim_out);
+ dim = isl_dim_set_alloc(bmap->ctx, nparam + n_in + n_out, 0);
+ if (!dim)
+ goto error;
+
+ orig_dim = bmap->dim;
+ bmap->dim = dim;
+ bset = (struct isl_basic_set *)bmap;
+
+ set = compute_divs(bset);
+ map = (struct isl_map *)set;
+ map = isl_map_reset_dim(map, orig_dim);
+
+ return map;
+error:
isl_basic_map_free(bmap);
return NULL;
}
projects / platform / upstream / isl.git / blobdiff