5 #include "isl_piplib.h"
6 #include "isl_map_piplib.h"
7 #include "isl_map_private.h"
8 #include "isl_equalities.h"
10 static void copy_values_from(isl_int *dst, Entier *src, unsigned n)
14 for (i = 0; i < n; ++i)
15 entier_assign(dst[i], src[i]);
18 static void add_value(isl_int *dst, Entier *src)
20 mpz_add(*dst, *dst, *src);
23 static void copy_constraint_from(isl_int *dst, PipVector *src,
24 unsigned nparam, unsigned n_in, unsigned n_out,
25 unsigned extra, int *pos)
29 copy_values_from(dst, src->the_vector+src->nb_elements-1, 1);
30 copy_values_from(dst+1, src->the_vector, nparam+n_in);
31 isl_seq_clr(dst+1+nparam+n_in, n_out);
32 isl_seq_clr(dst+1+nparam+n_in+n_out, extra);
33 for (i = 0; i + n_in + nparam < src->nb_elements-1; ++i) {
35 add_value(&dst[1+nparam+n_in+n_out+p],
36 &src->the_vector[n_in+nparam+i]);
40 static int add_inequality(struct isl_ctx *ctx,
41 struct isl_basic_map *bmap, int *pos, PipVector *vec)
43 unsigned nparam = isl_basic_map_n_param(bmap);
44 unsigned n_in = isl_basic_map_n_in(bmap);
45 unsigned n_out = isl_basic_map_n_out(bmap);
46 unsigned n_div = isl_basic_map_n_div(bmap);
47 int i = isl_basic_map_alloc_inequality(bmap);
50 copy_constraint_from(bmap->ineq[i], vec,
51 nparam, n_in, n_out, n_div, pos);
56 /* For a div d = floor(f/m), add the constraints
59 * -(f-(n-1)) + m d >= 0
61 * Note that the second constraint is the negation of
65 static int add_div_constraints(struct isl_ctx *ctx,
66 struct isl_basic_map *bmap, int *pos, PipNewparm *p, unsigned div)
69 unsigned total = isl_basic_map_total_dim(bmap);
70 unsigned div_pos = 1 + total - bmap->n_div + div;
72 i = add_inequality(ctx, bmap, pos, p->vector);
75 copy_values_from(&bmap->ineq[i][div_pos], &p->deno, 1);
76 isl_int_neg(bmap->ineq[i][div_pos], bmap->ineq[i][div_pos]);
78 j = isl_basic_map_alloc_inequality(bmap);
81 isl_seq_neg(bmap->ineq[j], bmap->ineq[i], 1 + total);
82 isl_int_add(bmap->ineq[j][0], bmap->ineq[j][0], bmap->ineq[j][div_pos]);
83 isl_int_sub_ui(bmap->ineq[j][0], bmap->ineq[j][0], 1);
87 static int add_equality(struct isl_ctx *ctx,
88 struct isl_basic_map *bmap, int *pos,
89 unsigned var, PipVector *vec)
92 unsigned nparam = isl_basic_map_n_param(bmap);
93 unsigned n_in = isl_basic_map_n_in(bmap);
94 unsigned n_out = isl_basic_map_n_out(bmap);
96 isl_assert(ctx, var < n_out, return -1);
98 i = isl_basic_map_alloc_equality(bmap);
101 copy_constraint_from(bmap->eq[i], vec,
102 nparam, n_in, n_out, bmap->extra, pos);
103 isl_int_set_si(bmap->eq[i][1+nparam+n_in+var], -1);
108 static int find_div(struct isl_ctx *ctx,
109 struct isl_basic_map *bmap, int *pos, PipNewparm *p)
112 unsigned nparam = isl_basic_map_n_param(bmap);
113 unsigned n_in = isl_basic_map_n_in(bmap);
114 unsigned n_out = isl_basic_map_n_out(bmap);
116 i = isl_basic_map_alloc_div(bmap);
120 copy_constraint_from(bmap->div[i]+1, p->vector,
121 nparam, n_in, n_out, bmap->extra, pos);
123 copy_values_from(bmap->div[i], &p->deno, 1);
124 for (j = 0; j < i; ++j)
125 if (isl_seq_eq(bmap->div[i], bmap->div[j],
126 1+1+isl_basic_map_total_dim(bmap)+j)) {
127 isl_basic_map_free_div(bmap, 1);
131 if (add_div_constraints(ctx, bmap, pos, p, i) < 0)
137 /* Count some properties of a quast
138 * - maximal number of new parameters
140 * - total number of solutions
141 * - total number of empty branches
143 static void quast_count(PipQuast *q, int *maxnew, int depth, int *maxdepth,
144 int *sol, int *nosol)
148 for (p = q->newparm; p; p = p->next)
149 if (p->rank > *maxnew)
152 if (++depth > *maxdepth)
154 quast_count(q->next_else, maxnew, depth, maxdepth, sol, nosol);
155 quast_count(q->next_then, maxnew, depth, maxdepth, sol, nosol);
165 * pos: array of length bmap->set.extra, mapping each of the existential
166 * variables PIP proposes to an existential variable in bmap
167 * bmap: collects the currently active constraints
168 * rest: collects the empty leaves of the quast (if not NULL)
172 struct isl_basic_map *bmap;
173 struct isl_set **rest;
178 * New existentially quantified variables are places after the existing ones.
180 static struct isl_map *scan_quast_r(struct scan_data *data, PipQuast *q,
184 struct isl_basic_map *bmap = data->bmap;
185 unsigned old_n_div = bmap->n_div;
186 unsigned nparam = isl_basic_map_n_param(bmap);
187 unsigned n_in = isl_basic_map_n_in(bmap);
188 unsigned n_out = isl_basic_map_n_out(bmap);
193 for (p = q->newparm; p; p = p->next) {
195 unsigned pip_param = nparam + n_in;
197 pos = find_div(data->ctx, bmap, data->pos, p);
200 data->pos[p->rank - pip_param] = pos;
204 int pos = add_inequality(data->ctx, bmap, data->pos,
208 map = scan_quast_r(data, q->next_then, map);
210 if (isl_inequality_negate(bmap, pos))
212 map = scan_quast_r(data, q->next_else, map);
214 if (isl_basic_map_free_inequality(bmap, 1))
216 } else if (q->list) {
219 /* if bmap->n_out is zero, we are only interested in the domains
220 * where a solution exists and not in the actual solution
222 for (j = 0, l = q->list; j < n_out && l; ++j, l = l->next)
223 if (add_equality(data->ctx, bmap, data->pos, j,
226 map = isl_map_add(map, isl_basic_map_copy(bmap));
227 if (isl_basic_map_free_equality(bmap, n_out))
229 } else if (data->rest) {
230 struct isl_basic_set *bset;
231 bset = isl_basic_set_from_basic_map(isl_basic_map_copy(bmap));
232 bset = isl_basic_set_drop_dims(bset, n_in, n_out);
235 *data->rest = isl_set_add(*data->rest, bset);
238 if (isl_basic_map_free_inequality(bmap, 2*(bmap->n_div - old_n_div)))
240 if (isl_basic_map_free_div(bmap, bmap->n_div - old_n_div))
249 * Returns a map of dimension "keep_dim" with "context" as domain and
250 * as range the first "isl_dim_size(keep_dim, isl_dim_out)" variables
251 * in the quast lists.
253 static struct isl_map *isl_map_from_quast(struct isl_ctx *ctx, PipQuast *q,
254 struct isl_dim *keep_dim,
255 struct isl_basic_set *context,
256 struct isl_set **rest)
262 struct scan_data data;
263 struct isl_map *map = NULL;
264 struct isl_dim *dims;
274 if (!context || !keep_dim)
277 dim = isl_basic_set_n_dim(context);
278 nparam = isl_basic_set_n_param(context);
279 keep = isl_dim_size(keep_dim, isl_dim_out);
280 pip_param = nparam + dim;
285 nexist = pip_param-1;
286 quast_count(q, &nexist, 0, &max_depth, &n_sol, &n_nosol);
287 nexist -= pip_param-1;
290 *rest = isl_set_alloc_dim(isl_dim_copy(context->dim), n_nosol,
295 map = isl_map_alloc_dim(isl_dim_copy(keep_dim), n_sol,
300 dims = isl_dim_reverse(isl_dim_copy(context->dim));
301 data.bmap = isl_basic_map_from_basic_set(context, dims);
302 data.bmap = isl_basic_map_extend_dim(data.bmap,
303 keep_dim, nexist, keep, max_depth+2*nexist);
307 if (data.bmap->extra) {
309 data.pos = isl_alloc_array(ctx, int, data.bmap->extra);
312 for (i = 0; i < data.bmap->n_div; ++i)
316 map = scan_quast_r(&data, q, map);
317 map = isl_map_finalize(map);
321 *rest = isl_set_finalize(*rest);
325 isl_basic_map_free(data.bmap);
330 isl_basic_set_free(context);
331 isl_dim_free(keep_dim);
335 isl_basic_map_free(data.bmap);
344 static void copy_values_to(Entier *dst, isl_int *src, unsigned n)
348 for (i = 0; i < n; ++i)
349 entier_assign(dst[i], src[i]);
352 static void copy_constraint_to(Entier *dst, isl_int *src,
353 unsigned pip_param, unsigned pip_var,
354 unsigned extra_front, unsigned extra_back)
356 copy_values_to(dst+1+extra_front+pip_var+pip_param+extra_back, src, 1);
357 copy_values_to(dst+1+extra_front+pip_var, src+1, pip_param);
358 copy_values_to(dst+1+extra_front, src+1+pip_param, pip_var);
361 PipMatrix *isl_basic_map_to_pip(struct isl_basic_map *bmap, unsigned pip_param,
362 unsigned extra_front, unsigned extra_back)
369 unsigned pip_var = isl_basic_map_total_dim(bmap) - pip_param;
371 nrow = extra_front + bmap->n_eq + bmap->n_ineq;
372 ncol = 1 + extra_front + pip_var + pip_param + extra_back + 1;
373 M = pip_matrix_alloc(nrow, ncol);
378 for (i = 0; i < bmap->n_eq; ++i) {
379 entier_set_si(M->p[off+i][0], 0);
380 copy_constraint_to(M->p[off+i], bmap->eq[i],
381 pip_param, pip_var, extra_front, extra_back);
384 for (i = 0; i < bmap->n_ineq; ++i) {
385 entier_set_si(M->p[off+i][0], 1);
386 copy_constraint_to(M->p[off+i], bmap->ineq[i],
387 pip_param, pip_var, extra_front, extra_back);
392 PipMatrix *isl_basic_set_to_pip(struct isl_basic_set *bset, unsigned pip_param,
393 unsigned extra_front, unsigned extra_back)
395 return isl_basic_map_to_pip((struct isl_basic_map *)bset,
396 pip_param, extra_front, extra_back);
399 static struct isl_map *extremum_on(
400 struct isl_basic_map *bmap, struct isl_basic_set *dom,
401 struct isl_set **empty, int max)
407 PipMatrix *domain = NULL, *context = NULL;
408 unsigned nparam, n_in, n_out;
414 isl_assert(ctx, isl_basic_map_compatible_domain(bmap, dom), goto error);
415 nparam = isl_basic_map_n_param(bmap);
416 n_in = isl_basic_map_n_in(bmap);
417 n_out = isl_basic_map_n_out(bmap);
419 domain = isl_basic_map_to_pip(bmap, nparam + n_in, 0, dom->n_div);
422 context = isl_basic_map_to_pip((struct isl_basic_map *)dom, 0, 0, 0);
426 options = pip_options_init();
427 options->Simplify = 1;
428 options->Maximize = max;
429 options->Urs_unknowns = -1;
430 options->Urs_parms = -1;
431 sol = pip_solve(domain, context, -1, options);
434 struct isl_basic_set *copy;
435 copy = isl_basic_set_copy(dom);
436 map = isl_map_from_quast(ctx, sol,
437 isl_dim_copy(bmap->dim), copy, empty);
439 map = isl_map_empty_like_basic_map(bmap);
445 if (map->n == 0 && empty) {
446 isl_set_free(*empty);
447 *empty = isl_set_from_basic_set(dom);
449 isl_basic_set_free(dom);
450 isl_basic_map_free(bmap);
453 pip_options_free(options);
454 pip_matrix_free(domain);
455 pip_matrix_free(context);
460 pip_matrix_free(domain);
462 pip_matrix_free(context);
463 isl_basic_map_free(bmap);
464 isl_basic_set_free(dom);
468 struct isl_map *isl_pip_basic_map_lexmax(
469 struct isl_basic_map *bmap, struct isl_basic_set *dom,
470 struct isl_set **empty)
472 return extremum_on(bmap, dom, empty, 1);
475 struct isl_map *isl_pip_basic_map_lexmin(
476 struct isl_basic_map *bmap, struct isl_basic_set *dom,
477 struct isl_set **empty)
479 return extremum_on(bmap, dom, empty, 0);
482 /* Project the given basic set onto its parameter domain, possibly introducing
483 * new, explicit, existential variables in the constraints.
484 * The input has parameters and output variables.
485 * The output has the same parameters, but no output variables, only
486 * explicit existentially quantified variables.
488 static struct isl_set *compute_divs_no_eq(struct isl_basic_set *bset)
490 PipMatrix *domain = NULL, *context = NULL;
497 struct isl_basic_set *dom;
504 nparam = isl_basic_set_n_param(bset);
506 domain = isl_basic_set_to_pip(bset, nparam, 0, 0);
509 context = pip_matrix_alloc(0, nparam + 2);
513 options = pip_options_init();
514 options->Simplify = 1;
515 options->Urs_unknowns = -1;
516 options->Urs_parms = -1;
517 sol = pip_solve(domain, context, -1, options);
519 dom = isl_basic_set_alloc(ctx, nparam, 0, 0, 0, 0);
520 map = isl_map_from_quast(ctx, sol, isl_dim_copy(dom->dim), dom, NULL);
521 set = (struct isl_set *)map;
524 pip_options_free(options);
525 pip_matrix_free(domain);
526 pip_matrix_free(context);
528 isl_basic_set_free(bset);
533 pip_matrix_free(domain);
535 pip_matrix_free(context);
536 isl_basic_set_free(dom);
537 isl_basic_set_free(bset);
541 static struct isl_map *isl_map_reset_dim(struct isl_map *map,
549 for (i = 0; i < map->n; ++i) {
550 isl_dim_free(map->p[i]->dim);
551 map->p[i]->dim = isl_dim_copy(dim);
553 isl_dim_free(map->dim);
563 static struct isl_set *isl_set_reset_dim(struct isl_set *set,
566 return (struct isl_set *) isl_map_reset_dim((struct isl_map *)set, dim);
569 /* Given a matrix M (mat) and a size n (size), replace mat
575 * where I is an n x n identity matrix.
577 static struct isl_mat *append_identity(struct isl_ctx *ctx,
578 struct isl_mat *mat, unsigned size)
581 unsigned n_row, n_col;
585 mat = isl_mat_extend(ctx, mat, n_row + size, n_col + size);
588 for (i = 0; i < n_row; ++i)
589 isl_seq_clr(mat->row[i] + n_col, size);
590 for (i = 0; i < size; ++i) {
591 isl_seq_clr(mat->row[n_row + i], n_col + size);
592 isl_int_set_si(mat->row[n_row + i][n_col + i], 1);
597 /* Apply a preimage specified by "mat" on the parameters of "bset".
599 static struct isl_basic_set *basic_set_parameter_preimage(
600 struct isl_basic_set *bset, struct isl_mat *mat)
602 unsigned nparam, n_out;
607 bset->dim = isl_dim_cow(bset->dim);
611 nparam = isl_basic_set_dim(bset, isl_dim_param);
612 n_out = isl_basic_set_dim(bset, isl_dim_set);
614 isl_assert(bset->ctx, mat->n_row == 1 + nparam, goto error);
616 mat = append_identity(bset->ctx, mat, n_out);
620 bset->dim->nparam = 0;
621 bset->dim->n_out += nparam;
622 bset = isl_basic_set_preimage(bset, mat);
624 bset->dim->nparam = bset->dim->n_out - n_out;
625 bset->dim->n_out = n_out;
629 isl_mat_free(bset ? bset->ctx : NULL, mat);
630 isl_basic_set_free(bset);
634 /* Apply a preimage specified by "mat" on the parameters of "set".
636 static struct isl_set *set_parameter_preimage(
637 struct isl_set *set, struct isl_mat *mat)
639 struct isl_dim *dim = NULL;
640 unsigned nparam, n_out;
645 dim = isl_dim_copy(set->dim);
646 dim = isl_dim_cow(dim);
650 nparam = isl_set_dim(set, isl_dim_param);
651 n_out = isl_set_dim(set, isl_dim_set);
653 isl_assert(set->ctx, mat->n_row == 1 + nparam, goto error);
655 mat = append_identity(set->ctx, mat, n_out);
660 dim->n_out += nparam;
661 isl_set_reset_dim(set, dim);
662 set = isl_set_preimage(set, mat);
665 dim = isl_dim_copy(set->dim);
666 dim = isl_dim_cow(dim);
669 dim->nparam = dim->n_out - n_out;
671 isl_set_reset_dim(set, dim);
675 isl_mat_free(set ? set->ctx : NULL, mat);
681 /* Intersect the basic set "bset" with the affine space specified by the
682 * equalities in "eq".
684 static struct isl_basic_set *basic_set_append_equalities(
685 struct isl_basic_set *bset, struct isl_mat *eq)
693 bset = isl_basic_set_extend_dim(bset, isl_dim_copy(bset->dim), 0,
698 len = 1 + isl_dim_total(bset->dim) + bset->extra;
699 for (i = 0; i < eq->n_row; ++i) {
700 k = isl_basic_set_alloc_equality(bset);
703 isl_seq_cpy(bset->eq[k], eq->row[i], eq->n_col);
704 isl_seq_clr(bset->eq[k] + eq->n_col, len - eq->n_col);
706 isl_mat_free(bset->ctx, eq);
710 isl_mat_free(bset ? bset->ctx : NULL, eq);
711 isl_basic_set_free(bset);
715 /* Intersect the set "set" with the affine space specified by the
716 * equalities in "eq".
718 static struct isl_set *set_append_equalities(struct isl_set *set,
726 for (i = 0; i < set->n; ++i) {
727 set->p[i] = basic_set_append_equalities(set->p[i],
728 isl_mat_copy(set->ctx, eq));
732 isl_mat_free(set->ctx, eq);
735 isl_mat_free(set ? set->ctx : NULL, eq);
740 /* Project the given basic set onto its parameter domain, possibly introducing
741 * new, explicit, existential variables in the constraints.
742 * The input has parameters and output variables.
743 * The output has the same parameters, but no output variables, only
744 * explicit existentially quantified variables.
746 * The actual projection is performed by pip, but pip doesn't seem
747 * to like equalities very much, so we first remove the equalities
748 * among the parameters by performing a variable compression on
749 * the parameters. Afterward, an inverse transformation is performed
750 * and the equalities among the parameters are inserted back in.
752 static struct isl_set *compute_divs(struct isl_basic_set *bset)
756 struct isl_mat *T, *T2;
758 unsigned nparam, n_out;
760 bset = isl_basic_set_cow(bset);
765 return compute_divs_no_eq(bset);
767 isl_basic_set_gauss(bset, NULL);
769 nparam = isl_basic_set_dim(bset, isl_dim_param);
770 n_out = isl_basic_set_dim(bset, isl_dim_out);
772 for (i = 0, j = n_out - 1; i < bset->n_eq && j >= 0; --j) {
773 if (!isl_int_is_zero(bset->eq[i][1 + nparam + j]))
777 return compute_divs_no_eq(bset);
779 eq = isl_mat_sub_alloc(bset->ctx, bset->eq, i, bset->n_eq - i,
781 eq = isl_mat_cow(bset->ctx, eq);
782 T = isl_mat_variable_compression(bset->ctx,
783 isl_mat_copy(bset->ctx, eq), &T2);
784 bset = basic_set_parameter_preimage(bset, T);
786 set = compute_divs_no_eq(bset);
787 set = set_parameter_preimage(set, T2);
788 set = set_append_equalities(set, eq);
792 /* Compute an explicit representation for all the existentially
793 * quantified variables.
794 * The input and output dimensions are first turned into parameters
795 * and the existential variables into output dimensions.
796 * compute_divs then returns a map with the same parameters and
797 * no input or output dimensions and the dimension specification
798 * is reset to that of the input.
800 struct isl_map *isl_pip_basic_map_compute_divs(struct isl_basic_map *bmap)
802 struct isl_basic_set *bset;
805 struct isl_dim *dim, *orig_dim = NULL;
810 bmap = isl_basic_map_cow(bmap);
814 nparam = isl_basic_map_dim(bmap, isl_dim_param);
815 n_in = isl_basic_map_dim(bmap, isl_dim_in);
816 n_out = isl_basic_map_dim(bmap, isl_dim_out);
817 dim = isl_dim_set_alloc(bmap->ctx, nparam + n_in + n_out, bmap->n_div);
821 orig_dim = bmap->dim;
823 bmap->extra -= bmap->n_div;
825 bset = (struct isl_basic_set *)bmap;
827 set = compute_divs(bset);
828 map = (struct isl_map *)set;
829 map = isl_map_reset_dim(map, orig_dim);
833 isl_basic_map_free(bmap);