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
;
410 bmap
= isl_basic_map_detect_equalities(bmap
);
415 isl_assert(ctx
, isl_basic_map_compatible_domain(bmap
, dom
), goto error
);
416 nparam
= isl_basic_map_n_param(bmap
);
417 n_in
= isl_basic_map_n_in(bmap
);
418 n_out
= isl_basic_map_n_out(bmap
);
420 domain
= isl_basic_map_to_pip(bmap
, nparam
+ n_in
, 0, dom
->n_div
);
423 context
= isl_basic_map_to_pip((struct isl_basic_map
*)dom
, 0, 0, 0);
427 options
= pip_options_init();
428 options
->Simplify
= 1;
429 options
->Maximize
= max
;
430 options
->Urs_unknowns
= -1;
431 options
->Urs_parms
= -1;
432 sol
= pip_solve(domain
, context
, -1, options
);
435 struct isl_basic_set
*copy
;
436 copy
= isl_basic_set_copy(dom
);
437 map
= isl_map_from_quast(ctx
, sol
,
438 isl_dim_copy(bmap
->dim
), copy
, empty
);
440 map
= isl_map_empty_like_basic_map(bmap
);
446 if (map
->n
== 0 && empty
) {
447 isl_set_free(*empty
);
448 *empty
= isl_set_from_basic_set(dom
);
450 isl_basic_set_free(dom
);
451 isl_basic_map_free(bmap
);
454 pip_options_free(options
);
455 pip_matrix_free(domain
);
456 pip_matrix_free(context
);
461 pip_matrix_free(domain
);
463 pip_matrix_free(context
);
464 isl_basic_map_free(bmap
);
465 isl_basic_set_free(dom
);
469 struct isl_map
*isl_pip_basic_map_lexmax(
470 struct isl_basic_map
*bmap
, struct isl_basic_set
*dom
,
471 struct isl_set
**empty
)
473 return extremum_on(bmap
, dom
, empty
, 1);
476 struct isl_map
*isl_pip_basic_map_lexmin(
477 struct isl_basic_map
*bmap
, struct isl_basic_set
*dom
,
478 struct isl_set
**empty
)
480 return extremum_on(bmap
, dom
, empty
, 0);
483 /* Project the given basic set onto its parameter domain, possibly introducing
484 * new, explicit, existential variables in the constraints.
485 * The input has parameters and output variables.
486 * The output has the same parameters, but no output variables, only
487 * explicit existentially quantified variables.
489 static struct isl_set
*compute_divs_no_eq(struct isl_basic_set
*bset
)
491 PipMatrix
*domain
= NULL
, *context
= NULL
;
498 struct isl_basic_set
*dom
;
505 nparam
= isl_basic_set_n_param(bset
);
507 domain
= isl_basic_set_to_pip(bset
, nparam
, 0, 0);
510 context
= pip_matrix_alloc(0, nparam
+ 2);
514 options
= pip_options_init();
515 options
->Simplify
= 1;
516 options
->Urs_unknowns
= -1;
517 options
->Urs_parms
= -1;
518 sol
= pip_solve(domain
, context
, -1, options
);
520 dom
= isl_basic_set_alloc(ctx
, nparam
, 0, 0, 0, 0);
521 map
= isl_map_from_quast(ctx
, sol
, isl_dim_copy(dom
->dim
), dom
, NULL
);
522 set
= (struct isl_set
*)map
;
525 pip_options_free(options
);
526 pip_matrix_free(domain
);
527 pip_matrix_free(context
);
529 isl_basic_set_free(bset
);
534 pip_matrix_free(domain
);
536 pip_matrix_free(context
);
537 isl_basic_set_free(dom
);
538 isl_basic_set_free(bset
);
542 static struct isl_map
*isl_map_reset_dim(struct isl_map
*map
,
550 for (i
= 0; i
< map
->n
; ++i
) {
551 isl_dim_free(map
->p
[i
]->dim
);
552 map
->p
[i
]->dim
= isl_dim_copy(dim
);
554 isl_dim_free(map
->dim
);
564 static struct isl_set
*isl_set_reset_dim(struct isl_set
*set
,
567 return (struct isl_set
*) isl_map_reset_dim((struct isl_map
*)set
, dim
);
570 /* Given a matrix M (mat) and a size n (size), replace mat
576 * where I is an n x n identity matrix.
578 static struct isl_mat
*append_identity(struct isl_mat
*mat
, unsigned size
)
581 unsigned n_row
, n_col
;
585 mat
= isl_mat_extend(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(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
;
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(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
);
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
);
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
],
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(eq
);
782 T
= isl_mat_variable_compression(isl_mat_copy(eq
), &T2
);
783 bset
= basic_set_parameter_preimage(bset
, T
);
785 set
= compute_divs_no_eq(bset
);
786 set
= set_parameter_preimage(set
, T2
);
787 set
= set_append_equalities(set
, eq
);
791 /* Compute an explicit representation for all the existentially
792 * quantified variables.
793 * The input and output dimensions are first turned into parameters
794 * and the existential variables into output dimensions.
795 * compute_divs then returns a map with the same parameters and
796 * no input or output dimensions and the dimension specification
797 * is reset to that of the input.
799 struct isl_map
*isl_pip_basic_map_compute_divs(struct isl_basic_map
*bmap
)
801 struct isl_basic_set
*bset
;
804 struct isl_dim
*dim
, *orig_dim
= NULL
;
809 bmap
= isl_basic_map_cow(bmap
);
813 nparam
= isl_basic_map_dim(bmap
, isl_dim_param
);
814 n_in
= isl_basic_map_dim(bmap
, isl_dim_in
);
815 n_out
= isl_basic_map_dim(bmap
, isl_dim_out
);
816 dim
= isl_dim_set_alloc(bmap
->ctx
, nparam
+ n_in
+ n_out
, bmap
->n_div
);
820 orig_dim
= bmap
->dim
;
822 bmap
->extra
-= bmap
->n_div
;
824 bset
= (struct isl_basic_set
*)bmap
;
826 set
= compute_divs(bset
);
827 map
= (struct isl_map
*)set
;
828 map
= isl_map_reset_dim(map
, orig_dim
);
832 isl_basic_map_free(bmap
);