__isl_take isl_union_map *umap1,
__isl_take isl_union_map *umap2);
+=item * Preimage
+
+ __isl_give isl_basic_set *
+ isl_basic_set_preimage_multi_aff(
+ __isl_take isl_basic_set *bset,
+ __isl_take isl_multi_aff *ma);
+
+This function computes the preimage of the given set under
+the given function. In other words, the expression is plugged
+into the set description.
+Objects of type C<isl_multi_aff> are described in
+L</"Piecewise Multiple Quasi Affine Expressions">.
+
=item * Cartesian Product
__isl_give isl_set *isl_set_product(
__isl_give isl_basic_set *isl_basic_set_apply(
__isl_take isl_basic_set *bset,
__isl_take isl_basic_map *bmap);
+__isl_give isl_basic_set *isl_basic_set_preimage_multi_aff(
+ __isl_take isl_basic_set *bset, __isl_take isl_multi_aff *ma);
__isl_export
__isl_give isl_basic_set *isl_basic_set_affine_hull(
__isl_take isl_basic_set *bset);
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".
*/
void isl_seq_substitute(isl_int *p, int pos, isl_int *subs,
int p_len, int subs_len, isl_int v);
+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);
__isl_give isl_pw_multi_aff *isl_pw_multi_aff_substitute(
__isl_take isl_pw_multi_aff *pma, enum isl_dim_type type, unsigned pos,
isl_set_free(set);
return NULL;
}
+
+/* Check if the range of "ma" is compatible with "space".
+ * Return -1 if anything is wrong.
+ */
+static int check_space_compatible_range_multi_aff(
+ __isl_keep isl_space *space, __isl_keep isl_multi_aff *ma)
+{
+ int m;
+ isl_space *ma_space;
+
+ ma_space = isl_multi_aff_get_space(ma);
+ m = isl_space_is_range_internal(space, ma_space);
+ isl_space_free(ma_space);
+ if (m >= 0 && !m)
+ isl_die(isl_space_get_ctx(space), isl_error_invalid,
+ "spaces don't match", return -1);
+ return m;
+}
+
+/* Check if the range of "ma" is compatible with "bset".
+ * Return -1 if anything is wrong.
+ */
+static int check_basic_set_compatible_range_multi_aff(
+ __isl_keep isl_basic_set *bset, __isl_keep isl_multi_aff *ma)
+{
+ return check_space_compatible_range_multi_aff(bset->dim, ma);
+}
+
+/* Copy the divs from "ma" to "bset", adding zeros for the coefficients
+ * of the other divs in "bset".
+ */
+static int set_ma_divs(__isl_keep isl_basic_set *bset,
+ __isl_keep isl_multi_aff *ma, int n_div)
+{
+ int i;
+ isl_local_space *ls;
+
+ if (n_div == 0)
+ return 0;
+
+ ls = isl_aff_get_domain_local_space(ma->p[0]);
+ if (!ls)
+ return -1;
+
+ for (i = 0; i < n_div; ++i) {
+ isl_seq_cpy(bset->div[i], ls->div->row[i], ls->div->n_col);
+ isl_seq_clr(bset->div[i] + ls->div->n_col, bset->n_div - n_div);
+ if (isl_basic_set_add_div_constraints(bset, i) < 0)
+ goto error;
+ }
+
+ isl_local_space_free(ls);
+ return 0;
+error:
+ isl_local_space_free(ls);
+ return -1;
+}
+
+/* How many stride constraints does "ma" enforce?
+ * That is, how many of the affine expressions have a denominator
+ * different from one?
+ */
+static int multi_aff_strides(__isl_keep isl_multi_aff *ma)
+{
+ int i;
+ int strides = 0;
+
+ for (i = 0; i < ma->n; ++i)
+ if (!isl_int_is_one(ma->p[i]->v->el[0]))
+ strides++;
+
+ return strides;
+}
+
+/* For each affine expression in ma of the form
+ *
+ * x_i = (f_i y + h_i)/m_i
+ *
+ * with m_i different from one, add a constraint to "bset"
+ * of the form
+ *
+ * f_i y + h_i = m_i alpha_i
+ *
+ * with alpha_i an additional existentially quantified variable.
+ */
+static __isl_give isl_basic_set *add_ma_strides(
+ __isl_take isl_basic_set *bset, __isl_keep isl_multi_aff *ma)
+{
+ int i, k;
+ int div;
+ int total;
+
+ total = isl_basic_set_total_dim(bset);
+ for (i = 0; i < ma->n; ++i) {
+ int len;
+
+ if (isl_int_is_one(ma->p[i]->v->el[0]))
+ continue;
+ div = isl_basic_set_alloc_div(bset);
+ k = isl_basic_set_alloc_equality(bset);
+ if (div < 0 || k < 0)
+ goto error;
+ isl_int_set_si(bset->div[div][0], 0);
+ len = ma->p[i]->v->size;
+ isl_seq_cpy(bset->eq[k], ma->p[i]->v->el + 1, len - 1);
+ isl_seq_clr(bset->eq[k] + len - 1, 1 + total - (len - 1));
+ isl_int_neg(bset->eq[k][1 + total], ma->p[i]->v->el[0]);
+ total++;
+ }
+
+ return bset;
+error:
+ isl_basic_set_free(bset);
+ return NULL;
+}
+
+/* Compute the preimage of "bset" under the function represented by "ma".
+ * In other words, plug in "ma" in "bset". The result is a basic set
+ * that lives in the domain space of "ma".
+ *
+ * If bset is represented by
+ *
+ * A(p) + B x + C(divs) >= 0
+ *
+ * and ma is represented by
+ *
+ * x = D(p) + F(y) + G(divs')
+ *
+ * then the result is
+ *
+ * A(p) + B D(p) + B F(y) + B G(divs') + C(divs) >= 0
+ *
+ * The divs in the input set are similarly adjusted.
+ * In particular
+ *
+ * floor((a_i(p) + b_i x + c_i(divs))/n_i)
+ *
+ * becomes
+ *
+ * floor((a_i(p) + b_i D(p) + b_i F(y) + B_i G(divs') + c_i(divs))/n_i)
+ *
+ * If bset is not a rational set and if F(y) involves any denominators
+ *
+ * x_i = (f_i y + h_i)/m_i
+ *
+ * the additional constraints are added to ensure that we only
+ * map back integer points. That is we enforce
+ *
+ * f_i y + h_i = m_i alpha_i
+ *
+ * with alpha_i an additional existentially quantified variable.
+ *
+ * We first copy over the divs from "ma".
+ * Then we add the modified constraints and divs from "bset".
+ * Finally, we add the stride constraints, if needed.
+ */
+__isl_give isl_basic_set *isl_basic_set_preimage_multi_aff(
+ __isl_take isl_basic_set *bset, __isl_take isl_multi_aff *ma)
+{
+ int i, k;
+ isl_space *space;
+ isl_basic_set *res = NULL;
+ int n_div_bset, n_div_ma;
+ isl_int f, c1, c2, g;
+ int rational, strides;
+
+ isl_int_init(f);
+ isl_int_init(c1);
+ isl_int_init(c2);
+ isl_int_init(g);
+
+ ma = isl_multi_aff_align_divs(ma);
+ if (!bset || !ma)
+ goto error;
+ if (check_basic_set_compatible_range_multi_aff(bset, ma) < 0)
+ goto error;
+
+ n_div_bset = isl_basic_set_dim(bset, isl_dim_div);
+ n_div_ma = ma->n ? isl_aff_dim(ma->p[0], isl_dim_div) : 0;
+
+ space = isl_space_domain(isl_multi_aff_get_space(ma));
+ rational = isl_basic_set_is_rational(bset);
+ strides = rational ? 0 : multi_aff_strides(ma);
+ res = isl_basic_set_alloc_space(space, n_div_ma + n_div_bset + strides,
+ bset->n_eq + strides, bset->n_ineq + 2 * n_div_ma);
+ if (rational)
+ res = isl_basic_set_set_rational(res);
+
+ for (i = 0; i < n_div_ma + n_div_bset; ++i)
+ if (isl_basic_set_alloc_div(res) < 0)
+ goto error;
+
+ if (set_ma_divs(res, ma, n_div_ma) < 0)
+ goto error;
+
+ for (i = 0; i < bset->n_eq; ++i) {
+ k = isl_basic_set_alloc_equality(res);
+ if (k < 0)
+ goto error;
+ isl_seq_preimage(res->eq[k], bset->eq[i], ma, n_div_ma,
+ n_div_bset, f, c1, c2, g, 0);
+ }
+
+ for (i = 0; i < bset->n_ineq; ++i) {
+ k = isl_basic_set_alloc_inequality(res);
+ if (k < 0)
+ goto error;
+ isl_seq_preimage(res->ineq[k], bset->ineq[i], ma, n_div_ma,
+ n_div_bset, f, c1, c2, g, 0);
+ }
+
+ for (i = 0; i < bset->n_div; ++i) {
+ if (isl_int_is_zero(bset->div[i][0])) {
+ isl_int_set_si(res->div[n_div_ma + i][0], 0);
+ continue;
+ }
+ isl_seq_preimage(res->div[n_div_ma + i], bset->div[i],
+ ma, n_div_ma, n_div_bset, f, c1, c2, g, 1);
+ }
+
+ if (strides)
+ res = add_ma_strides(res, ma);
+
+ isl_int_clear(f);
+ isl_int_clear(c1);
+ isl_int_clear(c2);
+ isl_int_clear(g);
+ isl_basic_set_free(bset);
+ isl_multi_aff_free(ma);
+ res = isl_basic_set_simplify(res);
+ return isl_basic_set_finalize(res);
+error:
+ isl_int_clear(f);
+ isl_int_clear(c1);
+ isl_int_clear(c2);
+ isl_int_clear(g);
+ isl_basic_set_free(bset);
+ isl_multi_aff_free(ma);
+ isl_basic_set_free(res);
+ return NULL;
+}
}
struct {
+ const char *set;
+ const char *ma;
+ const char *res;
+} preimage_tests[] = {
+ { "{ B[i,j] : 0 <= i < 10 and 0 <= j < 100 }",
+ "{ A[j,i] -> B[i,j] }",
+ "{ A[j,i] : 0 <= i < 10 and 0 <= j < 100 }" },
+ { "{ rat: B[i,j] : 0 <= i, j and 3 i + 5 j <= 100 }",
+ "{ A[a,b] -> B[a/2,b/6] }",
+ "{ rat: A[a,b] : 0 <= a, b and 9 a + 5 b <= 600 }" },
+ { "{ B[i,j] : 0 <= i, j and 3 i + 5 j <= 100 }",
+ "{ A[a,b] -> B[a/2,b/6] }",
+ "{ A[a,b] : 0 <= a, b and 9 a + 5 b <= 600 and "
+ "exists i,j : a = 2 i and b = 6 j }" },
+ { "[n] -> { S[i] : 0 <= i <= 100 }", "[n] -> { S[n] }",
+ "[n] -> { : 0 <= n <= 100 }" },
+ { "{ B[i] : 0 <= i < 100 and exists a : i = 4 a }",
+ "{ A[a] -> B[2a] }",
+ "{ A[a] : 0 <= a < 50 and exists b : a = 2 b }" },
+ { "{ B[i] : 0 <= i < 100 and exists a : i = 4 a }",
+ "{ A[a] -> B[([a/2])] }",
+ "{ A[a] : 0 <= a < 200 and exists b : [a/2] = 4 b }" },
+ { "{ B[i,j,k] : 0 <= i,j,k <= 100 }",
+ "{ A[a] -> B[a,a,a/3] }",
+ "{ A[a] : 0 <= a <= 100 and exists b : a = 3 b }" },
+ { "{ B[i,j] : j = [(i)/2] } ", "{ A[i,j] -> B[i/3,j] }",
+ "{ A[i,j] : j = [(i)/6] and exists a : i = 3 a }" },
+};
+
+int test_preimage(isl_ctx *ctx)
+{
+ int i;
+ isl_basic_set *bset1, *bset2;
+ isl_multi_aff *ma;
+ int equal;
+
+ for (i = 0; i < ARRAY_SIZE(preimage_tests); ++i) {
+ bset1 = isl_basic_set_read_from_str(ctx, preimage_tests[i].set);
+ ma = isl_multi_aff_read_from_str(ctx, preimage_tests[i].ma);
+ bset2 = isl_basic_set_read_from_str(ctx, preimage_tests[i].res);
+ bset1 = isl_basic_set_preimage_multi_aff(bset1, ma);
+ equal = isl_basic_set_is_equal(bset1, bset2);
+ isl_basic_set_free(bset1);
+ isl_basic_set_free(bset2);
+ if (equal < 0)
+ return -1;
+ if (!equal)
+ isl_die(ctx, isl_error_unknown, "bad preimage",
+ return -1);
+ }
+
+ return 0;
+}
+
+struct {
const char *name;
int (*fn)(isl_ctx *ctx);
} tests [] = {
{ "list", &test_list },
{ "align parameters", &test_align_parameters },
+ { "preimage", &test_preimage },
{ "eliminate", &test_eliminate },
{ "reisdue class", &test_residue_class },
{ "div", &test_div },
projects / platform / upstream / isl.git / commitdiff