return aff;
}
+/* Return a piecewise affine expression defined on the specified domain
+ * that is equal to zero.
+ */
+__isl_give isl_pw_aff *isl_pw_aff_zero_on_domain(__isl_take isl_local_space *ls)
+{
+ return isl_pw_aff_from_aff(isl_aff_zero_on_domain(ls));
+}
+
+/* Return an affine expression that is equal to the specified dimension
+ * in "ls".
+ */
+__isl_give isl_aff *isl_aff_var_on_domain(__isl_take isl_local_space *ls,
+ enum isl_dim_type type, unsigned pos)
+{
+ isl_space *space;
+ isl_aff *aff;
+
+ if (!ls)
+ return NULL;
+
+ space = isl_local_space_get_space(ls);
+ if (!space)
+ goto error;
+ if (isl_space_is_map(space))
+ isl_die(isl_space_get_ctx(space), isl_error_invalid,
+ "expecting (parameter) set space", goto error);
+ if (pos >= isl_local_space_dim(ls, type))
+ isl_die(isl_space_get_ctx(space), isl_error_invalid,
+ "position out of bounds", goto error);
+
+ isl_space_free(space);
+ aff = isl_aff_alloc(ls);
+ if (!aff)
+ return NULL;
+
+ pos += isl_local_space_offset(aff->ls, type);
+
+ isl_int_set_si(aff->v->el[0], 1);
+ isl_seq_clr(aff->v->el + 1, aff->v->size - 1);
+ isl_int_set_si(aff->v->el[1 + pos], 1);
+
+ return aff;
+error:
+ isl_local_space_free(ls);
+ isl_space_free(space);
+ return NULL;
+}
+
+/* Return a piecewise affine expression that is equal to
+ * the specified dimension in "ls".
+ */
+__isl_give isl_pw_aff *isl_pw_aff_var_on_domain(__isl_take isl_local_space *ls,
+ enum isl_dim_type type, unsigned pos)
+{
+ return isl_pw_aff_from_aff(isl_aff_var_on_domain(ls, type, pos));
+}
+
__isl_give isl_aff *isl_aff_copy(__isl_keep isl_aff *aff)
{
if (!aff)
/* Return a basic set containing those elements in the space
* of aff where it is non-negative.
+ * If "rational" is set, then return a rational basic set.
*/
-__isl_give isl_basic_set *isl_aff_nonneg_basic_set(__isl_take isl_aff *aff)
+static __isl_give isl_basic_set *aff_nonneg_basic_set(
+ __isl_take isl_aff *aff, int rational)
{
isl_constraint *ineq;
isl_basic_set *bset;
ineq = isl_inequality_from_aff(aff);
bset = isl_basic_set_from_constraint(ineq);
+ if (rational)
+ bset = isl_basic_set_set_rational(bset);
bset = isl_basic_set_simplify(bset);
return bset;
}
+/* Return a basic set containing those elements in the space
+ * of aff where it is non-negative.
+ */
+__isl_give isl_basic_set *isl_aff_nonneg_basic_set(__isl_take isl_aff *aff)
+{
+ return aff_nonneg_basic_set(aff, 0);
+}
+
/* Return a basic set containing those elements in the domain space
* of aff where it is negative.
*/
/* Return a basic set containing those elements in the space
* of aff where it is zero.
+ * If "rational" is set, then return a rational basic set.
*/
-__isl_give isl_basic_set *isl_aff_zero_basic_set(__isl_take isl_aff *aff)
+static __isl_give isl_basic_set *aff_zero_basic_set(__isl_take isl_aff *aff,
+ int rational)
{
isl_constraint *ineq;
isl_basic_set *bset;
ineq = isl_equality_from_aff(aff);
bset = isl_basic_set_from_constraint(ineq);
+ if (rational)
+ bset = isl_basic_set_set_rational(bset);
bset = isl_basic_set_simplify(bset);
return bset;
}
+/* Return a basic set containing those elements in the space
+ * of aff where it is zero.
+ */
+__isl_give isl_basic_set *isl_aff_zero_basic_set(__isl_take isl_aff *aff)
+{
+ return aff_zero_basic_set(aff, 0);
+}
+
/* Return a basic set containing those elements in the shared space
* of aff1 and aff2 where aff1 is greater than or equal to aff2.
*/
for (i = 0; i < pwaff->n; ++i) {
isl_basic_set *bset;
isl_set *set_i;
+ int rational;
- bset = isl_aff_nonneg_basic_set(isl_aff_copy(pwaff->p[i].aff));
+ rational = isl_set_has_rational(pwaff->p[i].set);
+ bset = aff_nonneg_basic_set(isl_aff_copy(pwaff->p[i].aff),
+ rational);
set_i = isl_set_from_basic_set(bset);
set_i = isl_set_intersect(set_i, isl_set_copy(pwaff->p[i].set));
set = isl_set_union_disjoint(set, set_i);
for (i = 0; i < pwaff->n; ++i) {
isl_basic_set *bset;
isl_set *set_i, *zero;
+ int rational;
- bset = isl_aff_zero_basic_set(isl_aff_copy(pwaff->p[i].aff));
+ rational = isl_set_has_rational(pwaff->p[i].set);
+ bset = aff_zero_basic_set(isl_aff_copy(pwaff->p[i].aff),
+ rational);
zero = isl_set_from_basic_set(bset);
set_i = isl_set_copy(pwaff->p[i].set);
if (complement)
return NULL;
}
+/* Compute the quotient of the integer division of "pa1" by "pa2"
+ * with rounding towards zero.
+ * "pa2" is assumed to be a piecewise constant.
+ *
+ * In particular, return
+ *
+ * pa1 >= 0 ? floor(pa1/pa2) : ceil(pa1/pa2)
+ *
+ */
+__isl_give isl_pw_aff *isl_pw_aff_tdiv_q(__isl_take isl_pw_aff *pa1,
+ __isl_take isl_pw_aff *pa2)
+{
+ int is_cst;
+ isl_set *cond;
+ isl_pw_aff *f, *c;
+
+ is_cst = isl_pw_aff_is_cst(pa2);
+ if (is_cst < 0)
+ goto error;
+ if (!is_cst)
+ isl_die(isl_pw_aff_get_ctx(pa2), isl_error_invalid,
+ "second argument should be a piecewise constant",
+ goto error);
+
+ pa1 = isl_pw_aff_div(pa1, pa2);
+
+ cond = isl_pw_aff_nonneg_set(isl_pw_aff_copy(pa1));
+ f = isl_pw_aff_floor(isl_pw_aff_copy(pa1));
+ c = isl_pw_aff_ceil(pa1);
+ return isl_pw_aff_cond(isl_set_indicator_function(cond), f, c);
+error:
+ isl_pw_aff_free(pa1);
+ isl_pw_aff_free(pa2);
+ return NULL;
+}
+
+/* Compute the remainder of the integer division of "pa1" by "pa2"
+ * with rounding towards zero.
+ * "pa2" is assumed to be a piecewise constant.
+ *
+ * In particular, return
+ *
+ * pa1 - pa2 * (pa1 >= 0 ? floor(pa1/pa2) : ceil(pa1/pa2))
+ *
+ */
+__isl_give isl_pw_aff *isl_pw_aff_tdiv_r(__isl_take isl_pw_aff *pa1,
+ __isl_take isl_pw_aff *pa2)
+{
+ int is_cst;
+ isl_pw_aff *res;
+
+ is_cst = isl_pw_aff_is_cst(pa2);
+ if (is_cst < 0)
+ goto error;
+ if (!is_cst)
+ isl_die(isl_pw_aff_get_ctx(pa2), isl_error_invalid,
+ "second argument should be a piecewise constant",
+ goto error);
+ res = isl_pw_aff_tdiv_q(isl_pw_aff_copy(pa1), isl_pw_aff_copy(pa2));
+ res = isl_pw_aff_mul(pa2, res);
+ res = isl_pw_aff_sub(pa1, res);
+ return res;
+error:
+ isl_pw_aff_free(pa1);
+ isl_pw_aff_free(pa2);
+ return NULL;
+}
+
static __isl_give isl_pw_aff *pw_aff_min(__isl_take isl_pw_aff *pwaff1,
__isl_take isl_pw_aff *pwaff2)
{
return pw_aff_list_reduce(list, &isl_pw_aff_max);
}
-#undef BASE
-#define BASE aff
-
-#include <isl_multi_templ.c>
-
-/* Construct an isl_multi_aff in the given space with value zero in
- * each of the output dimensions.
+/* Mark the domains of "pwaff" as rational.
*/
-__isl_give isl_multi_aff *isl_multi_aff_zero(__isl_take isl_space *space)
+__isl_give isl_pw_aff *isl_pw_aff_set_rational(__isl_take isl_pw_aff *pwaff)
{
- int n;
- isl_multi_aff *ma;
+ int i;
- if (!space)
+ pwaff = isl_pw_aff_cow(pwaff);
+ if (!pwaff)
return NULL;
+ if (pwaff->n == 0)
+ return pwaff;
- n = isl_space_dim(space , isl_dim_out);
- ma = isl_multi_aff_alloc(isl_space_copy(space));
-
- if (!n)
- isl_space_free(space);
- else {
- int i;
- isl_local_space *ls;
- isl_aff *aff;
-
- space = isl_space_domain(space);
- ls = isl_local_space_from_space(space);
- aff = isl_aff_zero_on_domain(ls);
-
- for (i = 0; i < n; ++i)
- ma = isl_multi_aff_set_aff(ma, i, isl_aff_copy(aff));
-
- isl_aff_free(aff);
+ for (i = 0; i < pwaff->n; ++i) {
+ pwaff->p[i].set = isl_set_set_rational(pwaff->p[i].set);
+ if (!pwaff->p[i].set)
+ return isl_pw_aff_free(pwaff);
}
- return ma;
+ return pwaff;
}
-/* Create an isl_multi_aff in the given space that maps each
- * input dimension to the corresponding output dimension.
+/* Mark the domains of the elements of "list" as rational.
*/
-__isl_give isl_multi_aff *isl_multi_aff_identity(__isl_take isl_space *space)
+__isl_give isl_pw_aff_list *isl_pw_aff_list_set_rational(
+ __isl_take isl_pw_aff_list *list)
{
- int n;
- isl_multi_aff *ma;
+ int i;
- if (!space)
+ if (!list)
return NULL;
+ if (list->n == 0)
+ return list;
- if (isl_space_is_set(space))
- isl_die(isl_space_get_ctx(space), isl_error_invalid,
- "expecting map space", goto error);
-
- n = isl_space_dim(space, isl_dim_out);
- if (n != isl_space_dim(space, isl_dim_in))
- isl_die(isl_space_get_ctx(space), isl_error_invalid,
- "number of input and output dimensions needs to be "
- "the same", goto error);
-
- ma = isl_multi_aff_alloc(isl_space_copy(space));
-
- if (!n)
- isl_space_free(space);
- else {
- int i;
- isl_local_space *ls;
- isl_aff *aff;
-
- space = isl_space_domain(space);
- ls = isl_local_space_from_space(space);
- aff = isl_aff_zero_on_domain(ls);
-
- for (i = 0; i < n; ++i) {
- isl_aff *aff_i;
- aff_i = isl_aff_copy(aff);
- aff_i = isl_aff_add_coefficient_si(aff_i,
- isl_dim_in, i, 1);
- ma = isl_multi_aff_set_aff(ma, i, aff_i);
- }
+ for (i = 0; i < list->n; ++i) {
+ isl_pw_aff *pa;
- isl_aff_free(aff);
+ pa = isl_pw_aff_list_get_pw_aff(list, i);
+ pa = isl_pw_aff_set_rational(pa);
+ list = isl_pw_aff_list_set_pw_aff(list, i, pa);
}
- return ma;
-error:
- isl_space_free(space);
- return NULL;
+ return list;
}
+#undef BASE
+#define BASE aff
+
+#include <isl_multi_templ.c>
+
/* Create an isl_pw_multi_aff with the given isl_multi_aff on a universe
* domain.
*/
return 1;
}
-__isl_give isl_multi_aff *isl_multi_aff_set_dim_name(
- __isl_take isl_multi_aff *maff,
- enum isl_dim_type type, unsigned pos, const char *s)
-{
- int i;
-
- maff = isl_multi_aff_cow(maff);
- if (!maff)
- return NULL;
-
- maff->space = isl_space_set_dim_name(maff->space, type, pos, s);
- if (!maff->space)
- return isl_multi_aff_free(maff);
-
- if (type == isl_dim_out)
- return maff;
- for (i = 0; i < maff->n; ++i) {
- maff->p[i] = isl_aff_set_dim_name(maff->p[i], type, pos, s);
- if (!maff->p[i])
- return isl_multi_aff_free(maff);
- }
-
- return maff;
-}
-
-__isl_give isl_multi_aff *isl_multi_aff_drop_dims(__isl_take isl_multi_aff *maff,
- enum isl_dim_type type, unsigned first, unsigned n)
-{
- int i;
-
- maff = isl_multi_aff_cow(maff);
- if (!maff)
- return NULL;
-
- maff->space = isl_space_drop_dims(maff->space, type, first, n);
- if (!maff->space)
- return isl_multi_aff_free(maff);
-
- if (type == isl_dim_out) {
- for (i = 0; i < n; ++i)
- isl_aff_free(maff->p[first + i]);
- for (i = first; i + n < maff->n; ++i)
- maff->p[i] = maff->p[i + n];
- maff->n -= n;
- return maff;
- }
-
- for (i = 0; i < maff->n; ++i) {
- maff->p[i] = isl_aff_drop_dims(maff->p[i], type, first, n);
- if (!maff->p[i])
- return isl_multi_aff_free(maff);
- }
-
- return maff;
-}
-
/* Return the set of domain elements where "ma1" is lexicographically
* smaller than or equal to "ma2".
*/
__isl_give isl_set *isl_set_from_pw_multi_aff(__isl_take isl_pw_multi_aff *pma)
{
+ if (!pma)
+ return NULL;
+
if (!isl_space_is_set(pma->dim))
isl_die(isl_pw_multi_aff_get_ctx(pma), isl_error_invalid,
"isl_pw_multi_aff cannot be converted into an isl_set",
return res;
}
+/* Compute the preimage of the affine expression "src" under "ma"
+ * and put the result in "dst". If "has_denom" is set (to one),
+ * then "src" and "dst" have an extra initial denominator.
+ * "n_div_ma" is the number of existentials in "ma"
+ * "n_div_bset" is the number of existentials in "src"
+ * The resulting "dst" (which is assumed to have been allocated by
+ * the caller) contains coefficients for both sets of existentials,
+ * first those in "ma" and then those in "src".
+ * f, c1, c2 and g are temporary objects that have been initialized
+ * by the caller.
+ *
+ * Let src represent the expression
+ *
+ * (a(p) + b x + c(divs))/d
+ *
+ * and let ma represent the expressions
+ *
+ * x_i = (r_i(p) + s_i(y) + t_i(divs'))/m_i
+ *
+ * We start out with the following expression for dst:
+ *
+ * (a(p) + 0 y + 0 divs' + f \sum_i b_i x_i + c(divs))/d
+ *
+ * with the multiplication factor f initially equal to 1.
+ * For each x_i that we substitute, we multiply the numerator
+ * (and denominator) of dst by c_1 = m_i and add the numerator
+ * of the x_i expression multiplied by c_2 = f b_i,
+ * after removing the common factors of c_1 and c_2.
+ * The multiplication factor f also needs to be multiplied by c_1
+ * for the next x_j, j > i.
+ */
+void isl_seq_preimage(isl_int *dst, isl_int *src,
+ __isl_keep isl_multi_aff *ma, int n_div_ma, int n_div_bset,
+ isl_int f, isl_int c1, isl_int c2, isl_int g, int has_denom)
+{
+ int i;
+ int n_param, n_in, n_out;
+ int o_div_bset;
+
+ n_param = isl_multi_aff_dim(ma, isl_dim_param);
+ n_in = isl_multi_aff_dim(ma, isl_dim_in);
+ n_out = isl_multi_aff_dim(ma, isl_dim_out);
+
+ o_div_bset = has_denom + 1 + n_param + n_in + n_div_ma;
+
+ isl_seq_cpy(dst, src, has_denom + 1 + n_param);
+ isl_seq_clr(dst + has_denom + 1 + n_param, n_in + n_div_ma);
+ isl_seq_cpy(dst + o_div_bset,
+ src + has_denom + 1 + n_param + n_out, n_div_bset);
+
+ isl_int_set_si(f, 1);
+
+ for (i = 0; i < n_out; ++i) {
+ if (isl_int_is_zero(src[has_denom + 1 + n_param + i]))
+ continue;
+ isl_int_set(c1, ma->p[i]->v->el[0]);
+ isl_int_mul(c2, f, src[has_denom + 1 + n_param + i]);
+ isl_int_gcd(g, c1, c2);
+ isl_int_divexact(c1, c1, g);
+ isl_int_divexact(c2, c2, g);
+
+ isl_int_mul(f, f, c1);
+ isl_seq_combine(dst + has_denom, c1, dst + has_denom,
+ c2, ma->p[i]->v->el + 1, ma->p[i]->v->size - 1);
+ isl_seq_scale(dst + o_div_bset,
+ dst + o_div_bset, c1, n_div_bset);
+ if (has_denom)
+ isl_int_mul(dst[0], dst[0], c1);
+ }
+}
+
/* Extend the local space of "dst" to include the divs
* in the local space of "src".
*/
return NULL;
}
-/* Given two isl_multi_affs A -> B and C -> D,
- * construct an isl_multi_aff (A * C) -> (B, D).
+/* Given two aligned isl_pw_multi_affs A -> B and C -> D,
+ * construct an isl_pw_multi_aff (A * C) -> [B -> D].
*/
-__isl_give isl_multi_aff *isl_multi_aff_flat_range_product(
- __isl_take isl_multi_aff *ma1, __isl_take isl_multi_aff *ma2)
+static __isl_give isl_pw_multi_aff *pw_multi_aff_range_product(
+ __isl_take isl_pw_multi_aff *pma1, __isl_take isl_pw_multi_aff *pma2)
{
- int i, n1, n2;
- isl_aff *aff;
isl_space *space;
- isl_multi_aff *res;
- if (!ma1 || !ma2)
- goto error;
-
- space = isl_space_range_product(isl_multi_aff_get_space(ma1),
- isl_multi_aff_get_space(ma2));
- space = isl_space_flatten_range(space);
- res = isl_multi_aff_alloc(space);
-
- n1 = isl_multi_aff_dim(ma1, isl_dim_out);
- n2 = isl_multi_aff_dim(ma2, isl_dim_out);
-
- for (i = 0; i < n1; ++i) {
- aff = isl_multi_aff_get_aff(ma1, i);
- res = isl_multi_aff_set_aff(res, i, aff);
- }
-
- for (i = 0; i < n2; ++i) {
- aff = isl_multi_aff_get_aff(ma2, i);
- res = isl_multi_aff_set_aff(res, n1 + i, aff);
- }
+ space = isl_space_range_product(isl_pw_multi_aff_get_space(pma1),
+ isl_pw_multi_aff_get_space(pma2));
+ return isl_pw_multi_aff_on_shared_domain_in(pma1, pma2, space,
+ &isl_multi_aff_range_product);
+}
- isl_multi_aff_free(ma1);
- isl_multi_aff_free(ma2);
- return res;
-error:
- isl_multi_aff_free(ma1);
- isl_multi_aff_free(ma2);
- return NULL;
+/* Given two isl_pw_multi_affs A -> B and C -> D,
+ * construct an isl_pw_multi_aff (A * C) -> [B -> D].
+ */
+__isl_give isl_pw_multi_aff *isl_pw_multi_aff_range_product(
+ __isl_take isl_pw_multi_aff *pma1, __isl_take isl_pw_multi_aff *pma2)
+{
+ return isl_pw_multi_aff_align_params_pw_pw_and(pma1, pma2,
+ &pw_multi_aff_range_product);
}
/* Given two aligned isl_pw_multi_affs A -> B and C -> D,
isl_pw_aff_free(pa);
return NULL;
}
+
+#undef BASE
+#define BASE pw_aff
+
+#include <isl_multi_templ.c>