2 * Copyright 2010-2011 INRIA Saclay
3 * Copyright 2014 Ecole Normale Superieure
5 * Use of this software is governed by the MIT license
7 * Written by Sven Verdoolaege, INRIA Saclay - Ile-de-France,
8 * Parc Club Orsay Universite, ZAC des vignes, 4 rue Jacques Monod,
10 * and Ecole Normale Superieure, 45 rue d'Ulm, 75230 Paris, France
13 #include <isl_map_private.h>
14 #include <isl_aff_private.h>
15 #include <isl_morph.h>
17 #include <isl_mat_private.h>
18 #include <isl_space_private.h>
19 #include <isl_equalities.h>
20 #include <isl_id_private.h>
21 #include <isl_aff_private.h>
22 #include <isl_vec_private.h>
24 isl_ctx
*isl_morph_get_ctx(__isl_keep isl_morph
*morph
)
28 return isl_basic_set_get_ctx(morph
->dom
);
31 __isl_give isl_morph
*isl_morph_alloc(
32 __isl_take isl_basic_set
*dom
, __isl_take isl_basic_set
*ran
,
33 __isl_take isl_mat
*map
, __isl_take isl_mat
*inv
)
37 if (!dom
|| !ran
|| !map
|| !inv
)
40 morph
= isl_alloc_type(dom
->ctx
, struct isl_morph
);
52 isl_basic_set_free(dom
);
53 isl_basic_set_free(ran
);
59 __isl_give isl_morph
*isl_morph_copy(__isl_keep isl_morph
*morph
)
68 __isl_give isl_morph
*isl_morph_dup(__isl_keep isl_morph
*morph
)
73 return isl_morph_alloc(isl_basic_set_copy(morph
->dom
),
74 isl_basic_set_copy(morph
->ran
),
75 isl_mat_copy(morph
->map
), isl_mat_copy(morph
->inv
));
78 __isl_give isl_morph
*isl_morph_cow(__isl_take isl_morph
*morph
)
86 return isl_morph_dup(morph
);
89 __isl_null isl_morph
*isl_morph_free(__isl_take isl_morph
*morph
)
97 isl_basic_set_free(morph
->dom
);
98 isl_basic_set_free(morph
->ran
);
99 isl_mat_free(morph
->map
);
100 isl_mat_free(morph
->inv
);
106 /* Is "morph" an identity on the parameters?
108 static isl_bool
identity_on_parameters(__isl_keep isl_morph
*morph
)
110 isl_bool is_identity
;
111 isl_size nparam
, nparam_ran
;
114 nparam
= isl_morph_dom_dim(morph
, isl_dim_param
);
115 nparam_ran
= isl_morph_ran_dim(morph
, isl_dim_param
);
116 if (nparam
< 0 || nparam_ran
< 0)
117 return isl_bool_error
;
118 if (nparam
!= nparam_ran
)
119 return isl_bool_false
;
121 return isl_bool_true
;
122 sub
= isl_mat_sub_alloc(morph
->map
, 0, 1 + nparam
, 0, 1 + nparam
);
123 is_identity
= isl_mat_is_scaled_identity(sub
);
129 /* Return an affine expression of the variables of the range of "morph"
130 * in terms of the parameters and the variables of the domain on "morph".
132 * In order for the space manipulations to make sense, we require
133 * that the parameters are not modified by "morph".
135 __isl_give isl_multi_aff
*isl_morph_get_var_multi_aff(
136 __isl_keep isl_morph
*morph
)
138 isl_space
*dom
, *ran
, *space
;
141 isl_size nparam
, nvar
;
143 isl_bool is_identity
;
148 is_identity
= identity_on_parameters(morph
);
152 isl_die(isl_morph_get_ctx(morph
), isl_error_invalid
,
153 "cannot handle parameter compression", return NULL
);
155 dom
= isl_morph_get_dom_space(morph
);
156 ls
= isl_local_space_from_space(isl_space_copy(dom
));
157 ran
= isl_morph_get_ran_space(morph
);
158 space
= isl_space_map_from_domain_and_range(dom
, ran
);
159 ma
= isl_multi_aff_zero(space
);
161 nparam
= isl_multi_aff_dim(ma
, isl_dim_param
);
162 nvar
= isl_multi_aff_dim(ma
, isl_dim_out
);
163 if (nparam
< 0 || nvar
< 0)
164 ma
= isl_multi_aff_free(ma
);
165 for (i
= 0; i
< nvar
; ++i
) {
170 v
= isl_mat_get_row(morph
->map
, 1 + nparam
+ i
);
171 v
= isl_vec_insert_els(v
, 0, 1);
172 val
= isl_mat_get_element_val(morph
->map
, 0, 0);
173 v
= isl_vec_set_element_val(v
, 0, val
);
174 aff
= isl_aff_alloc_vec(isl_local_space_copy(ls
), v
);
175 ma
= isl_multi_aff_set_aff(ma
, i
, aff
);
178 isl_local_space_free(ls
);
182 /* Return the domain space of "morph".
184 static __isl_keep isl_space
*isl_morph_peek_dom_space(
185 __isl_keep isl_morph
*morph
)
190 return isl_basic_set_peek_space(morph
->dom
);
193 /* Return a copy of the domain space of "morph".
195 __isl_give isl_space
*isl_morph_get_dom_space(__isl_keep isl_morph
*morph
)
197 return isl_space_copy(isl_morph_peek_dom_space(morph
));
200 /* Check that the match against "space" with result "match" was successful.
202 static isl_stat
check_space_match(__isl_keep isl_space
*space
, isl_bool match
)
205 return isl_stat_error
;
207 isl_die(isl_space_get_ctx(space
), isl_error_invalid
,
208 "spaces don't match", return isl_stat_error
);
213 /* Check that "morph" can be applied to the "space".
215 isl_stat
isl_morph_check_applies(__isl_keep isl_morph
*morph
,
216 __isl_keep isl_space
*space
)
218 isl_space
*dom_space
;
221 dom_space
= isl_morph_peek_dom_space(morph
);
222 applies
= isl_space_is_equal(dom_space
, space
);
223 return check_space_match(space
, applies
);
226 __isl_give isl_space
*isl_morph_get_ran_space(__isl_keep isl_morph
*morph
)
231 return isl_space_copy(morph
->ran
->dim
);
234 isl_size
isl_morph_dom_dim(__isl_keep isl_morph
*morph
, enum isl_dim_type type
)
237 return isl_size_error
;
239 return isl_basic_set_dim(morph
->dom
, type
);
242 isl_size
isl_morph_ran_dim(__isl_keep isl_morph
*morph
, enum isl_dim_type type
)
245 return isl_size_error
;
247 return isl_basic_set_dim(morph
->ran
, type
);
250 __isl_give isl_morph
*isl_morph_remove_dom_dims(__isl_take isl_morph
*morph
,
251 enum isl_dim_type type
, unsigned first
, unsigned n
)
258 morph
= isl_morph_cow(morph
);
262 dom_offset
= isl_space_offset(morph
->dom
->dim
, type
);
264 return isl_morph_free(morph
);
266 morph
->dom
= isl_basic_set_remove_dims(morph
->dom
, type
, first
, n
);
268 morph
->map
= isl_mat_drop_cols(morph
->map
, 1 + dom_offset
+ first
, n
);
270 morph
->inv
= isl_mat_drop_rows(morph
->inv
, 1 + dom_offset
+ first
, n
);
272 if (morph
->dom
&& morph
->ran
&& morph
->map
&& morph
->inv
)
275 isl_morph_free(morph
);
279 __isl_give isl_morph
*isl_morph_remove_ran_dims(__isl_take isl_morph
*morph
,
280 enum isl_dim_type type
, unsigned first
, unsigned n
)
287 morph
= isl_morph_cow(morph
);
291 ran_offset
= isl_space_offset(morph
->ran
->dim
, type
);
293 return isl_morph_free(morph
);
295 morph
->ran
= isl_basic_set_remove_dims(morph
->ran
, type
, first
, n
);
297 morph
->map
= isl_mat_drop_rows(morph
->map
, 1 + ran_offset
+ first
, n
);
299 morph
->inv
= isl_mat_drop_cols(morph
->inv
, 1 + ran_offset
+ first
, n
);
301 if (morph
->dom
&& morph
->ran
&& morph
->map
&& morph
->inv
)
304 isl_morph_free(morph
);
308 /* Project domain of morph onto its parameter domain.
310 __isl_give isl_morph
*isl_morph_dom_params(__isl_take isl_morph
*morph
)
314 morph
= isl_morph_cow(morph
);
317 n
= isl_basic_set_dim(morph
->dom
, isl_dim_set
);
319 return isl_morph_free(morph
);
320 morph
= isl_morph_remove_dom_dims(morph
, isl_dim_set
, 0, n
);
323 morph
->dom
= isl_basic_set_params(morph
->dom
);
327 isl_morph_free(morph
);
331 /* Project range of morph onto its parameter domain.
333 __isl_give isl_morph
*isl_morph_ran_params(__isl_take isl_morph
*morph
)
337 morph
= isl_morph_cow(morph
);
340 n
= isl_basic_set_dim(morph
->ran
, isl_dim_set
);
342 return isl_morph_free(morph
);
343 morph
= isl_morph_remove_ran_dims(morph
, isl_dim_set
, 0, n
);
346 morph
->ran
= isl_basic_set_params(morph
->ran
);
350 isl_morph_free(morph
);
354 /* Replace the identifier of the tuple of the range of the morph by "id".
356 static __isl_give isl_morph
*isl_morph_set_ran_tuple_id(
357 __isl_take isl_morph
*morph
, __isl_keep isl_id
*id
)
359 morph
= isl_morph_cow(morph
);
362 morph
->ran
= isl_basic_set_set_tuple_id(morph
->ran
, isl_id_copy(id
));
364 return isl_morph_free(morph
);
368 void isl_morph_print_internal(__isl_take isl_morph
*morph
, FILE *out
)
373 isl_basic_set_dump(morph
->dom
);
374 isl_basic_set_dump(morph
->ran
);
375 isl_mat_print_internal(morph
->map
, out
, 4);
376 isl_mat_print_internal(morph
->inv
, out
, 4);
379 void isl_morph_dump(__isl_take isl_morph
*morph
)
381 isl_morph_print_internal(morph
, stderr
);
384 __isl_give isl_morph
*isl_morph_identity(__isl_keep isl_basic_set
*bset
)
387 isl_basic_set
*universe
;
390 total
= isl_basic_set_dim(bset
, isl_dim_all
);
394 id
= isl_mat_identity(bset
->ctx
, 1 + total
);
395 universe
= isl_basic_set_universe(isl_space_copy(bset
->dim
));
397 return isl_morph_alloc(universe
, isl_basic_set_copy(universe
),
398 id
, isl_mat_copy(id
));
401 /* Create a(n identity) morphism between empty sets of the same dimension
404 __isl_give isl_morph
*isl_morph_empty(__isl_keep isl_basic_set
*bset
)
407 isl_basic_set
*empty
;
410 total
= isl_basic_set_dim(bset
, isl_dim_all
);
414 id
= isl_mat_identity(bset
->ctx
, 1 + total
);
415 empty
= isl_basic_set_empty(isl_space_copy(bset
->dim
));
417 return isl_morph_alloc(empty
, isl_basic_set_copy(empty
),
418 id
, isl_mat_copy(id
));
421 /* Construct a basic set described by the "n" equalities of "bset" starting
424 static __isl_give isl_basic_set
*copy_equalities(__isl_keep isl_basic_set
*bset
,
425 unsigned first
, unsigned n
)
431 total
= isl_basic_set_dim(bset
, isl_dim_all
);
432 if (total
< 0 || isl_basic_set_check_no_locals(bset
) < 0)
435 eq
= isl_basic_set_alloc_space(isl_basic_set_get_space(bset
), 0, n
, 0);
438 for (i
= 0; i
< n
; ++i
) {
439 k
= isl_basic_set_alloc_equality(eq
);
442 isl_seq_cpy(eq
->eq
[k
], bset
->eq
[first
+ i
], 1 + total
);
447 isl_basic_set_free(eq
);
451 /* Given a basic set, exploit the equalities in the basic set to construct
452 * a morphism that maps the basic set to a lower-dimensional space.
453 * Specifically, the morphism reduces the number of dimensions of type "type".
455 * We first select the equalities of interest, that is those that involve
456 * variables of type "type" and no later variables.
457 * Denote those equalities as
461 * where C(p) depends on the parameters if type == isl_dim_set and
462 * is a constant if type == isl_dim_param.
464 * Use isl_mat_final_variable_compression to construct a compression
470 * If T is a zero-column matrix, then the set of equality constraints
471 * do not admit a solution. In this case, an empty morphism is returned.
473 * Both matrices are extended to map the full original space to the full
476 __isl_give isl_morph
*isl_basic_set_variable_compression(
477 __isl_keep isl_basic_set
*bset
, enum isl_dim_type type
)
487 isl_basic_set
*dom
, *ran
;
492 if (isl_basic_set_plain_is_empty(bset
))
493 return isl_morph_empty(bset
);
495 if (isl_basic_set_check_no_locals(bset
) < 0)
498 ntype
= isl_basic_set_dim(bset
, type
);
499 total
= isl_basic_set_dim(bset
, isl_dim_all
);
500 if (ntype
< 0 || total
< 0)
502 otype
= isl_basic_set_offset(bset
, type
);
503 orest
= otype
+ ntype
;
504 nrest
= total
- (orest
- 1);
506 for (f_eq
= 0; f_eq
< bset
->n_eq
; ++f_eq
)
507 if (isl_seq_first_non_zero(bset
->eq
[f_eq
] + orest
, nrest
) == -1)
509 for (n_eq
= 0; f_eq
+ n_eq
< bset
->n_eq
; ++n_eq
)
510 if (isl_seq_first_non_zero(bset
->eq
[f_eq
+ n_eq
] + otype
, ntype
) == -1)
513 return isl_morph_identity(bset
);
515 E
= isl_mat_sub_alloc6(bset
->ctx
, bset
->eq
, f_eq
, n_eq
, 0, orest
);
516 C
= isl_mat_final_variable_compression(E
, otype
- 1, &Q
);
519 if (C
&& C
->n_col
== 0) {
522 return isl_morph_empty(bset
);
525 Q
= isl_mat_diagonal(Q
, isl_mat_identity(bset
->ctx
, nrest
));
526 C
= isl_mat_diagonal(C
, isl_mat_identity(bset
->ctx
, nrest
));
528 space
= isl_space_copy(bset
->dim
);
529 space
= isl_space_drop_dims(space
, type
, 0, ntype
);
530 space
= isl_space_add_dims(space
, type
, ntype
- n_eq
);
531 ran
= isl_basic_set_universe(space
);
532 dom
= copy_equalities(bset
, f_eq
, n_eq
);
534 return isl_morph_alloc(dom
, ran
, Q
, C
);
537 /* Given a basic set, exploit the equalities in the basic set to construct
538 * a morphism that maps the basic set to a lower-dimensional space
539 * with identifier "id".
540 * Specifically, the morphism reduces the number of set dimensions.
542 __isl_give isl_morph
*isl_basic_set_variable_compression_with_id(
543 __isl_keep isl_basic_set
*bset
, __isl_keep isl_id
*id
)
547 morph
= isl_basic_set_variable_compression(bset
, isl_dim_set
);
548 morph
= isl_morph_set_ran_tuple_id(morph
, id
);
552 /* Construct a parameter compression for "bset".
553 * We basically just call isl_mat_parameter_compression with the right input
554 * and then extend the resulting matrix to include the variables.
556 * The implementation assumes that "bset" does not have any equalities
557 * that only involve the parameters and that isl_basic_set_gauss has
558 * been applied to "bset".
560 * Let the equalities be given as
564 * We use isl_mat_parameter_compression_ext to compute the compression
568 __isl_give isl_morph
*isl_basic_set_parameter_compression(
569 __isl_keep isl_basic_set
*bset
)
577 isl_basic_set
*dom
, *ran
;
582 if (isl_basic_set_plain_is_empty(bset
))
583 return isl_morph_empty(bset
);
585 return isl_morph_identity(bset
);
588 nparam
= isl_basic_set_dim(bset
, isl_dim_param
);
589 nvar
= isl_basic_set_dim(bset
, isl_dim_set
);
590 n_div
= isl_basic_set_dim(bset
, isl_dim_div
);
591 if (nparam
< 0 || nvar
< 0 || n_div
< 0)
594 if (isl_seq_first_non_zero(bset
->eq
[bset
->n_eq
- 1] + 1 + nparam
,
596 isl_die(isl_basic_set_get_ctx(bset
), isl_error_invalid
,
597 "input not allowed to have parameter equalities",
599 if (n_eq
> nvar
+ n_div
)
600 isl_die(isl_basic_set_get_ctx(bset
), isl_error_invalid
,
601 "input not gaussed", return NULL
);
603 B
= isl_mat_sub_alloc6(bset
->ctx
, bset
->eq
, 0, n_eq
, 0, 1 + nparam
);
604 H
= isl_mat_sub_alloc6(bset
->ctx
, bset
->eq
,
605 0, n_eq
, 1 + nparam
, nvar
+ n_div
);
606 inv
= isl_mat_parameter_compression_ext(B
, H
);
607 inv
= isl_mat_diagonal(inv
, isl_mat_identity(bset
->ctx
, nvar
));
608 map
= isl_mat_right_inverse(isl_mat_copy(inv
));
610 dom
= isl_basic_set_universe(isl_space_copy(bset
->dim
));
611 ran
= isl_basic_set_universe(isl_space_copy(bset
->dim
));
613 return isl_morph_alloc(dom
, ran
, map
, inv
);
616 /* Construct an isl_multi_aff that corresponds
617 * to the affine transformation matrix "mat" and
618 * that lives in an anonymous space.
620 static __isl_give isl_multi_aff
*isl_multi_aff_from_aff_mat_anonymous(
621 __isl_take isl_mat
*mat
)
623 isl_size n_row
, n_col
;
627 ctx
= isl_mat_get_ctx(mat
);
628 n_row
= isl_mat_rows(mat
);
629 n_col
= isl_mat_cols(mat
);
630 if (n_row
< 0 || n_col
< 0)
633 space
= isl_space_alloc(ctx
, 0, n_col
- 1, n_row
- 1);
635 return isl_multi_aff_from_aff_mat(space
, mat
);
638 /* Apply the morphism to the basic set.
639 * In particular, compute the preimage of "bset" under the inverse mapping
640 * in morph and intersect with the range of the morphism.
641 * Note that the mapping in morph applies to both parameters and set dimensions,
642 * so the parameters need to be treated as set dimensions during the call
643 * to isl_basic_set_preimage_multi_aff.
645 __isl_give isl_basic_set
*isl_morph_basic_set(__isl_take isl_morph
*morph
,
646 __isl_take isl_basic_set
*bset
)
652 if (!morph
|| isl_basic_set_check_equal_space(bset
, morph
->dom
) < 0)
654 n_param
= isl_basic_set_dim(morph
->dom
, isl_dim_param
);
658 ma
= isl_multi_aff_from_aff_mat_anonymous(isl_mat_copy(morph
->inv
));
660 bset
= isl_basic_set_move_dims(bset
, isl_dim_set
, 0,
661 isl_dim_param
, 0, n_param
);
662 bset
= isl_basic_set_preimage_multi_aff(bset
, ma
);
663 space
= isl_basic_set_get_space(morph
->ran
);
664 bset
= isl_basic_set_reset_space(bset
, space
);
665 bset
= isl_basic_set_intersect(bset
, isl_basic_set_copy(morph
->ran
));
667 isl_morph_free(morph
);
670 isl_morph_free(morph
);
671 isl_basic_set_free(bset
);
675 /* Apply the morphism to the set.
676 * In particular, compute the preimage of "set" under the inverse mapping
677 * in morph and intersect with the range of the morphism.
678 * Note that the mapping in morph applies to both parameters and set dimensions,
679 * so the parameters need to be treated as set dimensions during the call
680 * to isl_set_preimage_multi_aff.
682 __isl_give isl_set
*isl_morph_set(__isl_take isl_morph
*morph
,
683 __isl_take isl_set
*set
)
690 if (!morph
|| isl_set_basic_set_check_equal_space(set
, morph
->dom
) < 0)
692 n_param
= isl_basic_set_dim(morph
->dom
, isl_dim_param
);
696 ma
= isl_multi_aff_from_aff_mat_anonymous(isl_mat_copy(morph
->inv
));
698 set
= isl_set_move_dims(set
, isl_dim_set
, 0, isl_dim_param
, 0, n_param
);
699 set
= isl_set_preimage_multi_aff(set
, ma
);
700 space
= isl_basic_set_get_space(morph
->ran
);
701 set
= isl_set_reset_space(set
, space
);
702 ran
= isl_basic_set_copy(morph
->ran
);
703 set
= isl_set_intersect(set
, isl_set_from_basic_set(ran
));
705 isl_morph_free(morph
);
709 isl_morph_free(morph
);
713 /* Construct a morphism that first does morph2 and then morph1.
715 __isl_give isl_morph
*isl_morph_compose(__isl_take isl_morph
*morph1
,
716 __isl_take isl_morph
*morph2
)
719 isl_basic_set
*dom
, *ran
;
721 if (!morph1
|| !morph2
)
724 map
= isl_mat_product(isl_mat_copy(morph1
->map
), isl_mat_copy(morph2
->map
));
725 inv
= isl_mat_product(isl_mat_copy(morph2
->inv
), isl_mat_copy(morph1
->inv
));
726 dom
= isl_morph_basic_set(isl_morph_inverse(isl_morph_copy(morph2
)),
727 isl_basic_set_copy(morph1
->dom
));
728 dom
= isl_basic_set_intersect(dom
, isl_basic_set_copy(morph2
->dom
));
729 ran
= isl_morph_basic_set(isl_morph_copy(morph1
),
730 isl_basic_set_copy(morph2
->ran
));
731 ran
= isl_basic_set_intersect(ran
, isl_basic_set_copy(morph1
->ran
));
733 isl_morph_free(morph1
);
734 isl_morph_free(morph2
);
736 return isl_morph_alloc(dom
, ran
, map
, inv
);
738 isl_morph_free(morph1
);
739 isl_morph_free(morph2
);
743 __isl_give isl_morph
*isl_morph_inverse(__isl_take isl_morph
*morph
)
748 morph
= isl_morph_cow(morph
);
753 morph
->dom
= morph
->ran
;
757 morph
->map
= morph
->inv
;
763 /* We detect all the equalities first to avoid implicit equalities
764 * being discovered during the computations. In particular,
765 * the compression on the variables could expose additional stride
766 * constraints on the parameters. This would result in existentially
767 * quantified variables after applying the resulting morph, which
768 * in turn could break invariants of the calling functions.
770 __isl_give isl_morph
*isl_basic_set_full_compression(
771 __isl_keep isl_basic_set
*bset
)
773 isl_morph
*morph
, *morph2
;
775 bset
= isl_basic_set_copy(bset
);
776 bset
= isl_basic_set_detect_equalities(bset
);
778 morph
= isl_basic_set_variable_compression(bset
, isl_dim_param
);
779 bset
= isl_morph_basic_set(isl_morph_copy(morph
), bset
);
781 morph2
= isl_basic_set_parameter_compression(bset
);
782 bset
= isl_morph_basic_set(isl_morph_copy(morph2
), bset
);
784 morph
= isl_morph_compose(morph2
, morph
);
786 morph2
= isl_basic_set_variable_compression(bset
, isl_dim_set
);
787 isl_basic_set_free(bset
);
789 morph
= isl_morph_compose(morph2
, morph
);
794 __isl_give isl_vec
*isl_morph_vec(__isl_take isl_morph
*morph
,
795 __isl_take isl_vec
*vec
)
800 vec
= isl_mat_vec_product(isl_mat_copy(morph
->map
), vec
);
802 isl_morph_free(morph
);
805 isl_morph_free(morph
);