4 #include "isl_piplib.h"
5 #include "isl_map_piplib.h"
6 #include "isl_map_private.h"
8 static void copy_values_from(isl_int
*dst
, Entier
*src
, unsigned n
)
12 for (i
= 0; i
< n
; ++i
)
13 entier_assign(dst
[i
], src
[i
]);
16 static void add_value(isl_int
*dst
, Entier
*src
)
18 mpz_add(*dst
, *dst
, *src
);
21 static void copy_constraint_from(isl_int
*dst
, PipVector
*src
,
22 unsigned nparam
, unsigned n_in
, unsigned n_out
,
23 unsigned extra
, int *pos
)
27 copy_values_from(dst
, src
->the_vector
+src
->nb_elements
-1, 1);
28 copy_values_from(dst
+1, src
->the_vector
, nparam
+n_in
);
29 isl_seq_clr(dst
+1+nparam
+n_in
, n_out
);
30 isl_seq_clr(dst
+1+nparam
+n_in
+n_out
, extra
);
31 for (i
= 0; i
+ n_in
+ nparam
< src
->nb_elements
-1; ++i
) {
33 add_value(&dst
[1+nparam
+n_in
+n_out
+p
],
34 &src
->the_vector
[n_in
+nparam
+i
]);
38 static int add_inequality(struct isl_ctx
*ctx
,
39 struct isl_basic_map
*bmap
, int *pos
, PipVector
*vec
)
41 unsigned nparam
= isl_basic_map_n_param(bmap
);
42 unsigned n_in
= isl_basic_map_n_in(bmap
);
43 unsigned n_out
= isl_basic_map_n_out(bmap
);
44 unsigned n_div
= isl_basic_map_n_div(bmap
);
45 int i
= isl_basic_map_alloc_inequality(bmap
);
48 copy_constraint_from(bmap
->ineq
[i
], vec
,
49 nparam
, n_in
, n_out
, n_div
, pos
);
54 /* For a div d = floor(f/m), add the constraints
57 * -(f-(n-1)) + m d >= 0
59 * Note that the second constraint is the negation of
63 static int add_div_constraints(struct isl_ctx
*ctx
,
64 struct isl_basic_map
*bmap
, int *pos
, PipNewparm
*p
, unsigned div
)
67 unsigned total
= isl_basic_map_total_dim(bmap
);
68 unsigned div_pos
= 1 + total
- bmap
->n_div
+ div
;
70 i
= add_inequality(ctx
, bmap
, pos
, p
->vector
);
73 copy_values_from(&bmap
->ineq
[i
][div_pos
], &p
->deno
, 1);
74 isl_int_neg(bmap
->ineq
[i
][div_pos
], bmap
->ineq
[i
][div_pos
]);
76 j
= isl_basic_map_alloc_inequality(bmap
);
79 isl_seq_neg(bmap
->ineq
[j
], bmap
->ineq
[i
], 1 + total
);
80 isl_int_add(bmap
->ineq
[j
][0], bmap
->ineq
[j
][0], bmap
->ineq
[j
][div_pos
]);
81 isl_int_sub_ui(bmap
->ineq
[j
][0], bmap
->ineq
[j
][0], 1);
85 static int add_equality(struct isl_ctx
*ctx
,
86 struct isl_basic_map
*bmap
, int *pos
,
87 unsigned var
, PipVector
*vec
)
90 unsigned nparam
= isl_basic_map_n_param(bmap
);
91 unsigned n_in
= isl_basic_map_n_in(bmap
);
92 unsigned n_out
= isl_basic_map_n_out(bmap
);
94 isl_assert(ctx
, var
< n_out
, return -1);
96 i
= isl_basic_map_alloc_equality(bmap
);
99 copy_constraint_from(bmap
->eq
[i
], vec
,
100 nparam
, n_in
, n_out
, bmap
->extra
, pos
);
101 isl_int_set_si(bmap
->eq
[i
][1+nparam
+n_in
+var
], -1);
106 static int find_div(struct isl_ctx
*ctx
,
107 struct isl_basic_map
*bmap
, int *pos
, PipNewparm
*p
)
110 unsigned nparam
= isl_basic_map_n_param(bmap
);
111 unsigned n_in
= isl_basic_map_n_in(bmap
);
112 unsigned n_out
= isl_basic_map_n_out(bmap
);
114 i
= isl_basic_map_alloc_div(bmap
);
118 copy_constraint_from(bmap
->div
[i
]+1, p
->vector
,
119 nparam
, n_in
, n_out
, bmap
->extra
, pos
);
121 copy_values_from(bmap
->div
[i
], &p
->deno
, 1);
122 for (j
= 0; j
< i
; ++j
)
123 if (isl_seq_eq(bmap
->div
[i
], bmap
->div
[j
],
124 1+1+isl_basic_map_total_dim(bmap
)+j
)) {
125 isl_basic_map_free_div(bmap
, 1);
129 if (add_div_constraints(ctx
, bmap
, pos
, p
, i
) < 0)
135 /* Count some properties of a quast
136 * - maximal number of new parameters
138 * - total number of solutions
139 * - total number of empty branches
141 static void quast_count(PipQuast
*q
, int *maxnew
, int depth
, int *maxdepth
,
142 int *sol
, int *nosol
)
146 for (p
= q
->newparm
; p
; p
= p
->next
)
147 if (p
->rank
> *maxnew
)
150 if (++depth
> *maxdepth
)
152 quast_count(q
->next_else
, maxnew
, depth
, maxdepth
, sol
, nosol
);
153 quast_count(q
->next_then
, maxnew
, depth
, maxdepth
, sol
, nosol
);
163 * pos: array of length bmap->set.extra, mapping each of the existential
164 * variables PIP proposes to an existential variable in bmap
165 * bmap: collects the currently active constraints
166 * rest: collects the empty leaves of the quast (if not NULL)
170 struct isl_basic_map
*bmap
;
171 struct isl_set
**rest
;
176 * New existentially quantified variables are places after the existing ones.
178 static struct isl_map
*scan_quast_r(struct scan_data
*data
, PipQuast
*q
,
182 struct isl_basic_map
*bmap
= data
->bmap
;
183 unsigned old_n_div
= bmap
->n_div
;
184 unsigned nparam
= isl_basic_map_n_param(bmap
);
185 unsigned n_in
= isl_basic_map_n_in(bmap
);
186 unsigned n_out
= isl_basic_map_n_out(bmap
);
191 for (p
= q
->newparm
; p
; p
= p
->next
) {
193 unsigned pip_param
= nparam
+ n_in
;
195 pos
= find_div(data
->ctx
, bmap
, data
->pos
, p
);
198 data
->pos
[p
->rank
- pip_param
] = pos
;
202 int pos
= add_inequality(data
->ctx
, bmap
, data
->pos
,
206 map
= scan_quast_r(data
, q
->next_then
, map
);
208 if (isl_inequality_negate(bmap
, pos
))
210 map
= scan_quast_r(data
, q
->next_else
, map
);
212 if (isl_basic_map_free_inequality(bmap
, 1))
214 } else if (q
->list
) {
217 /* if bmap->n_out is zero, we are only interested in the domains
218 * where a solution exists and not in the actual solution
220 for (j
= 0, l
= q
->list
; j
< n_out
&& l
; ++j
, l
= l
->next
)
221 if (add_equality(data
->ctx
, bmap
, data
->pos
, j
,
224 map
= isl_map_add(map
, isl_basic_map_copy(bmap
));
225 if (isl_basic_map_free_equality(bmap
, n_out
))
227 } else if (data
->rest
) {
228 struct isl_basic_set
*bset
;
229 bset
= isl_basic_set_from_basic_map(isl_basic_map_copy(bmap
));
230 bset
= isl_basic_set_drop_dims(bset
, n_in
, n_out
);
233 *data
->rest
= isl_set_add(*data
->rest
, bset
);
236 if (isl_basic_map_free_inequality(bmap
, 2*(bmap
->n_div
- old_n_div
)))
238 if (isl_basic_map_free_div(bmap
, bmap
->n_div
- old_n_div
))
247 * Returns a map of dimension "keep_dim" with "context" as domain and
248 * as range the first "isl_dim_size(keep_dim, isl_dim_out)" variables
249 * in the quast lists.
251 static struct isl_map
*isl_map_from_quast(struct isl_ctx
*ctx
, PipQuast
*q
,
252 struct isl_dim
*keep_dim
,
253 struct isl_basic_set
*context
,
254 struct isl_set
**rest
)
260 struct scan_data data
;
261 struct isl_map
*map
= NULL
;
262 struct isl_dim
*dims
;
272 if (!context
|| !keep_dim
)
275 dim
= isl_basic_set_n_dim(context
);
276 nparam
= isl_basic_set_n_param(context
);
277 keep
= isl_dim_size(keep_dim
, isl_dim_out
);
278 pip_param
= nparam
+ dim
;
283 nexist
= pip_param
-1;
284 quast_count(q
, &nexist
, 0, &max_depth
, &n_sol
, &n_nosol
);
285 nexist
-= pip_param
-1;
288 *rest
= isl_set_alloc_dim(isl_dim_copy(context
->dim
), n_nosol
,
293 map
= isl_map_alloc_dim(isl_dim_copy(keep_dim
), n_sol
,
298 dims
= isl_dim_reverse(isl_dim_copy(context
->dim
));
299 data
.bmap
= isl_basic_map_from_basic_set(context
, dims
);
300 data
.bmap
= isl_basic_map_extend_dim(data
.bmap
,
301 keep_dim
, nexist
, keep
, max_depth
+2*nexist
);
305 if (data
.bmap
->extra
) {
307 data
.pos
= isl_alloc_array(ctx
, int, data
.bmap
->extra
);
310 for (i
= 0; i
< data
.bmap
->n_div
; ++i
)
314 map
= scan_quast_r(&data
, q
, map
);
315 map
= isl_map_finalize(map
);
319 *rest
= isl_set_finalize(*rest
);
323 isl_basic_map_free(data
.bmap
);
328 isl_basic_set_free(context
);
329 isl_dim_free(keep_dim
);
333 isl_basic_map_free(data
.bmap
);
342 static void copy_values_to(Entier
*dst
, isl_int
*src
, unsigned n
)
346 for (i
= 0; i
< n
; ++i
)
347 entier_assign(dst
[i
], src
[i
]);
350 static void copy_constraint_to(Entier
*dst
, isl_int
*src
,
351 unsigned pip_param
, unsigned pip_var
,
352 unsigned extra_front
, unsigned extra_back
)
354 copy_values_to(dst
+1+extra_front
+pip_var
+pip_param
+extra_back
, src
, 1);
355 copy_values_to(dst
+1+extra_front
+pip_var
, src
+1, pip_param
);
356 copy_values_to(dst
+1+extra_front
, src
+1+pip_param
, pip_var
);
359 PipMatrix
*isl_basic_map_to_pip(struct isl_basic_map
*bmap
, unsigned pip_param
,
360 unsigned extra_front
, unsigned extra_back
)
367 unsigned pip_var
= isl_basic_map_total_dim(bmap
) - pip_param
;
369 nrow
= extra_front
+ bmap
->n_eq
+ bmap
->n_ineq
;
370 ncol
= 1 + extra_front
+ pip_var
+ pip_param
+ extra_back
+ 1;
371 M
= pip_matrix_alloc(nrow
, ncol
);
376 for (i
= 0; i
< bmap
->n_eq
; ++i
) {
377 entier_set_si(M
->p
[off
+i
][0], 0);
378 copy_constraint_to(M
->p
[off
+i
], bmap
->eq
[i
],
379 pip_param
, pip_var
, extra_front
, extra_back
);
382 for (i
= 0; i
< bmap
->n_ineq
; ++i
) {
383 entier_set_si(M
->p
[off
+i
][0], 1);
384 copy_constraint_to(M
->p
[off
+i
], bmap
->ineq
[i
],
385 pip_param
, pip_var
, extra_front
, extra_back
);
390 PipMatrix
*isl_basic_set_to_pip(struct isl_basic_set
*bset
, unsigned pip_param
,
391 unsigned extra_front
, unsigned extra_back
)
393 return isl_basic_map_to_pip((struct isl_basic_map
*)bset
,
394 pip_param
, extra_front
, extra_back
);
397 static struct isl_map
*extremum_on(
398 struct isl_basic_map
*bmap
, struct isl_basic_set
*dom
,
399 struct isl_set
**empty
, int max
)
405 PipMatrix
*domain
= NULL
, *context
= NULL
;
406 unsigned nparam
, n_in
, n_out
;
412 isl_assert(ctx
, isl_basic_map_compatible_domain(bmap
, dom
), goto error
);
413 nparam
= isl_basic_map_n_param(bmap
);
414 n_in
= isl_basic_map_n_in(bmap
);
415 n_out
= isl_basic_map_n_out(bmap
);
417 domain
= isl_basic_map_to_pip(bmap
, nparam
+ n_in
, 0, dom
->n_div
);
420 context
= isl_basic_map_to_pip((struct isl_basic_map
*)dom
, 0, 0, 0);
424 options
= pip_options_init();
425 options
->Simplify
= 1;
426 options
->Maximize
= max
;
427 options
->Urs_unknowns
= -1;
428 options
->Urs_parms
= -1;
429 sol
= pip_solve(domain
, context
, -1, options
);
432 struct isl_basic_set
*copy
;
433 copy
= isl_basic_set_copy(dom
);
434 map
= isl_map_from_quast(ctx
, sol
,
435 isl_dim_copy(bmap
->dim
), copy
, empty
);
437 map
= isl_map_empty_like_basic_map(bmap
);
443 if (map
->n
== 0 && empty
) {
444 isl_set_free(*empty
);
445 *empty
= isl_set_from_basic_set(dom
);
447 isl_basic_set_free(dom
);
448 isl_basic_map_free(bmap
);
451 pip_options_free(options
);
452 pip_matrix_free(domain
);
453 pip_matrix_free(context
);
458 pip_matrix_free(domain
);
460 pip_matrix_free(context
);
461 isl_basic_map_free(bmap
);
462 isl_basic_set_free(dom
);
466 struct isl_map
*isl_pip_basic_map_lexmax(
467 struct isl_basic_map
*bmap
, struct isl_basic_set
*dom
,
468 struct isl_set
**empty
)
470 return extremum_on(bmap
, dom
, empty
, 1);
473 struct isl_map
*isl_pip_basic_map_lexmin(
474 struct isl_basic_map
*bmap
, struct isl_basic_set
*dom
,
475 struct isl_set
**empty
)
477 return extremum_on(bmap
, dom
, empty
, 0);
480 /* Project the given basic set onto its parameter domain, possibly introducing
481 * new, explicit, existential variables in the constraints.
482 * The input has parameters and output variables.
483 * The output has the same parameters, but no output variables, only
484 * explicit existentially quantified variables.
486 static struct isl_set
*compute_divs(struct isl_basic_set
*bset
)
488 PipMatrix
*domain
= NULL
, *context
= NULL
;
495 struct isl_basic_set
*dom
;
502 nparam
= isl_basic_set_n_param(bset
);
504 domain
= isl_basic_set_to_pip(bset
, nparam
, 0, 0);
507 context
= pip_matrix_alloc(0, nparam
+ 2);
511 options
= pip_options_init();
512 options
->Simplify
= 1;
513 options
->Urs_unknowns
= -1;
514 options
->Urs_parms
= -1;
515 sol
= pip_solve(domain
, context
, -1, options
);
517 dom
= isl_basic_set_alloc(ctx
, nparam
, 0, 0, 0, 0);
518 map
= isl_map_from_quast(ctx
, sol
, isl_dim_copy(dom
->dim
), dom
, NULL
);
519 set
= (struct isl_set
*)map
;
522 pip_options_free(options
);
523 pip_matrix_free(domain
);
524 pip_matrix_free(context
);
526 isl_basic_set_free(bset
);
531 pip_matrix_free(domain
);
533 pip_matrix_free(context
);
534 isl_basic_set_free(dom
);
535 isl_basic_set_free(bset
);
539 static struct isl_map
*isl_map_reset_dim(struct isl_map
*map
,
547 for (i
= 0; i
< map
->n
; ++i
) {
548 isl_dim_free(map
->p
[i
]->dim
);
549 map
->p
[i
]->dim
= isl_dim_copy(dim
);
551 isl_dim_free(map
->dim
);
561 /* Compute an explicit representation for all the existentially
562 * quantified variables.
563 * The input and output dimensions are first turned into parameters
564 * and the existential variables into output dimensions.
565 * compute_divs then returns a map with the same parameters and
566 * no input or output dimensions and the dimension specification
567 * is reset to that of the input.
569 struct isl_map
*isl_pip_basic_map_compute_divs(struct isl_basic_map
*bmap
)
571 struct isl_basic_set
*bset
;
574 struct isl_dim
*dim
, *orig_dim
= NULL
;
579 bmap
= isl_basic_map_cow(bmap
);
583 nparam
= isl_basic_map_dim(bmap
, isl_dim_param
);
584 n_in
= isl_basic_map_dim(bmap
, isl_dim_in
);
585 n_out
= isl_basic_map_dim(bmap
, isl_dim_out
);
586 dim
= isl_dim_set_alloc(bmap
->ctx
, nparam
+ n_in
+ n_out
, bmap
->n_div
);
590 orig_dim
= bmap
->dim
;
592 bmap
->extra
-= bmap
->n_div
;
594 bset
= (struct isl_basic_set
*)bmap
;
596 set
= compute_divs(bset
);
597 map
= (struct isl_map
*)set
;
598 map
= isl_map_reset_dim(map
, orig_dim
);
602 isl_basic_map_free(bmap
);