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 with "context" as domain and as range the first
248 * "keep" variables in the quast lists.
250 static struct isl_map
*isl_map_from_quast(struct isl_ctx
*ctx
, PipQuast
*q
,
252 struct isl_basic_set
*context
,
253 struct isl_set
**rest
)
259 struct scan_data data
;
261 struct isl_dim
*dims
;
273 dim
= isl_basic_set_n_dim(context
);
274 nparam
= isl_basic_set_n_param(context
);
275 pip_param
= nparam
+ dim
;
280 nexist
= pip_param
-1;
281 quast_count(q
, &nexist
, 0, &max_depth
, &n_sol
, &n_nosol
);
282 nexist
-= pip_param
-1;
285 *rest
= isl_set_alloc(data
.ctx
, nparam
, dim
, n_nosol
,
290 map
= isl_map_alloc(data
.ctx
, nparam
, dim
, keep
, n_sol
,
295 dims
= isl_dim_reverse(isl_dim_copy(context
->dim
));
296 data
.bmap
= isl_basic_map_from_basic_set(context
, dims
);
297 data
.bmap
= isl_basic_map_extend(data
.bmap
,
298 nparam
, dim
, keep
, nexist
, keep
, max_depth
+2*nexist
);
302 if (data
.bmap
->extra
) {
304 data
.pos
= isl_alloc_array(ctx
, int, data
.bmap
->extra
);
307 for (i
= 0; i
< data
.bmap
->n_div
; ++i
)
311 map
= scan_quast_r(&data
, q
, map
);
312 map
= isl_map_finalize(map
);
316 *rest
= isl_set_finalize(*rest
);
320 isl_basic_map_free(data
.bmap
);
327 isl_basic_map_free(data
.bmap
);
336 static void copy_values_to(Entier
*dst
, isl_int
*src
, unsigned n
)
340 for (i
= 0; i
< n
; ++i
)
341 entier_assign(dst
[i
], src
[i
]);
344 static void copy_constraint_to(Entier
*dst
, isl_int
*src
,
345 unsigned pip_param
, unsigned pip_var
,
346 unsigned extra_front
, unsigned extra_back
)
348 copy_values_to(dst
+1+extra_front
+pip_var
+pip_param
+extra_back
, src
, 1);
349 copy_values_to(dst
+1+extra_front
+pip_var
, src
+1, pip_param
);
350 copy_values_to(dst
+1+extra_front
, src
+1+pip_param
, pip_var
);
353 PipMatrix
*isl_basic_map_to_pip(struct isl_basic_map
*bmap
, unsigned pip_param
,
354 unsigned extra_front
, unsigned extra_back
)
361 unsigned pip_var
= isl_basic_map_total_dim(bmap
) - pip_param
;
363 nrow
= extra_front
+ bmap
->n_eq
+ bmap
->n_ineq
;
364 ncol
= 1 + extra_front
+ pip_var
+ pip_param
+ extra_back
+ 1;
365 M
= pip_matrix_alloc(nrow
, ncol
);
370 for (i
= 0; i
< bmap
->n_eq
; ++i
) {
371 entier_set_si(M
->p
[off
+i
][0], 0);
372 copy_constraint_to(M
->p
[off
+i
], bmap
->eq
[i
],
373 pip_param
, pip_var
, extra_front
, extra_back
);
376 for (i
= 0; i
< bmap
->n_ineq
; ++i
) {
377 entier_set_si(M
->p
[off
+i
][0], 1);
378 copy_constraint_to(M
->p
[off
+i
], bmap
->ineq
[i
],
379 pip_param
, pip_var
, extra_front
, extra_back
);
384 static struct isl_map
*extremum_on(
385 struct isl_basic_map
*bmap
, struct isl_basic_set
*dom
,
386 struct isl_set
**empty
, int max
)
392 PipMatrix
*domain
= NULL
, *context
= NULL
;
393 unsigned nparam
, n_in
, n_out
;
399 isl_assert(ctx
, isl_basic_map_compatible_domain(bmap
, dom
), goto error
);
400 nparam
= isl_basic_map_n_param(bmap
);
401 n_in
= isl_basic_map_n_in(bmap
);
402 n_out
= isl_basic_map_n_out(bmap
);
404 domain
= isl_basic_map_to_pip(bmap
, nparam
+ n_in
, 0, dom
->n_div
);
407 context
= isl_basic_map_to_pip((struct isl_basic_map
*)dom
, 0, 0, 0);
411 options
= pip_options_init();
412 options
->Simplify
= 1;
413 options
->Maximize
= max
;
414 options
->Urs_unknowns
= -1;
415 options
->Urs_parms
= -1;
416 sol
= pip_solve(domain
, context
, -1, options
);
419 struct isl_basic_set
*copy
;
420 copy
= isl_basic_set_copy(dom
);
421 map
= isl_map_from_quast(ctx
, sol
, n_out
, copy
, empty
);
423 map
= isl_map_empty_like_basic_map(bmap
);
429 if (map
->n
== 0 && empty
) {
430 isl_set_free(*empty
);
431 *empty
= isl_set_from_basic_set(dom
);
433 isl_basic_set_free(dom
);
434 isl_basic_map_free(bmap
);
437 pip_options_free(options
);
438 pip_matrix_free(domain
);
439 pip_matrix_free(context
);
444 pip_matrix_free(domain
);
446 pip_matrix_free(context
);
447 isl_basic_map_free(bmap
);
448 isl_basic_set_free(dom
);
452 struct isl_map
*isl_pip_basic_map_lexmax(
453 struct isl_basic_map
*bmap
, struct isl_basic_set
*dom
,
454 struct isl_set
**empty
)
456 return extremum_on(bmap
, dom
, empty
, 1);
459 struct isl_map
*isl_pip_basic_map_lexmin(
460 struct isl_basic_map
*bmap
, struct isl_basic_set
*dom
,
461 struct isl_set
**empty
)
463 return extremum_on(bmap
, dom
, empty
, 0);
466 struct isl_map
*isl_pip_basic_map_compute_divs(struct isl_basic_map
*bmap
)
468 PipMatrix
*domain
= NULL
, *context
= NULL
;
475 struct isl_basic_set
*dom
;
484 nparam
= isl_basic_map_n_param(bmap
);
485 n_in
= isl_basic_map_n_in(bmap
);
486 n_out
= isl_basic_map_n_out(bmap
);
488 domain
= isl_basic_map_to_pip(bmap
, nparam
+ n_in
+ n_out
, 0, 0);
491 context
= pip_matrix_alloc(0, nparam
+ n_in
+ n_out
+ 2);
495 options
= pip_options_init();
496 options
->Simplify
= 1;
497 options
->Urs_unknowns
= -1;
498 options
->Urs_parms
= -1;
499 sol
= pip_solve(domain
, context
, -1, options
);
501 dom
= isl_basic_set_alloc(ctx
, nparam
, n_in
+ n_out
, 0, 0, 0);
502 map
= isl_map_from_quast(ctx
, sol
, 0, dom
, NULL
);
505 pip_options_free(options
);
506 pip_matrix_free(domain
);
507 pip_matrix_free(context
);
509 dim
= isl_dim_copy(bmap
->dim
);
510 isl_basic_map_free(bmap
);
512 set
= isl_map_domain(map
);
514 return isl_map_from_set(set
, dim
);
517 pip_matrix_free(domain
);
519 pip_matrix_free(context
);
520 isl_basic_set_free(dom
);
521 isl_basic_map_free(bmap
);