+/*
+ * Copyright 2008-2009 Katholieke Universiteit Leuven
+ *
+ * Use of this software is governed by the GNU LGPLv2.1 license
+ *
+ * Written by Sven Verdoolaege, K.U.Leuven, Departement
+ * Computerwetenschappen, Celestijnenlaan 200A, B-3001 Leuven, Belgium
+ */
+
#include <assert.h>
#include <stdio.h>
#include <limits.h>
#include <isl_ctx.h>
#include <isl_set.h>
+#include <isl_constraint.h>
static char *srcdir;
+void test_read(struct isl_ctx *ctx)
+{
+ char filename[PATH_MAX];
+ FILE *input;
+ int n;
+ struct isl_basic_set *bset1, *bset2;
+ const char *str = "{[y]: Exists ( alpha : 2alpha = y)}";
+
+ n = snprintf(filename, sizeof(filename),
+ "%s/test_inputs/set.omega", srcdir);
+ assert(n < sizeof(filename));
+ input = fopen(filename, "r");
+ assert(input);
+
+ bset1 = isl_basic_set_read_from_file(ctx, input, 0);
+ bset2 = isl_basic_set_read_from_str(ctx, str, 0);
+
+ assert(isl_basic_set_is_equal(bset1, bset2) == 1);
+
+ isl_basic_set_free(bset1);
+ isl_basic_set_free(bset2);
+
+ fclose(input);
+}
+
+/* Construct the basic set { [i] : 5 <= i <= N } */
+void test_construction(struct isl_ctx *ctx)
+{
+ isl_int v;
+ struct isl_dim *dim;
+ struct isl_basic_set *bset;
+ struct isl_constraint *c;
+
+ isl_int_init(v);
+
+ dim = isl_dim_set_alloc(ctx, 1, 1);
+ bset = isl_basic_set_universe(dim);
+
+ c = isl_inequality_alloc(isl_dim_copy(bset->dim));
+ isl_int_set_si(v, -1);
+ isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
+ isl_int_set_si(v, 1);
+ isl_constraint_set_coefficient(c, isl_dim_param, 0, v);
+ bset = isl_basic_set_add_constraint(bset, c);
+
+ c = isl_inequality_alloc(isl_dim_copy(bset->dim));
+ isl_int_set_si(v, 1);
+ isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
+ isl_int_set_si(v, -5);
+ isl_constraint_set_constant(c, v);
+ bset = isl_basic_set_add_constraint(bset, c);
+
+ isl_basic_set_free(bset);
+
+ isl_int_clear(v);
+}
+
+void test_div(struct isl_ctx *ctx)
+{
+ isl_int v;
+ int pos;
+ struct isl_dim *dim;
+ struct isl_div *div;
+ struct isl_basic_set *bset;
+ struct isl_constraint *c;
+
+ isl_int_init(v);
+
+ /* test 1 */
+ dim = isl_dim_set_alloc(ctx, 0, 1);
+ bset = isl_basic_set_universe(dim);
+
+ c = isl_equality_alloc(isl_dim_copy(bset->dim));
+ isl_int_set_si(v, -1);
+ isl_constraint_set_constant(c, v);
+ isl_int_set_si(v, 1);
+ isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
+ div = isl_div_alloc(isl_dim_copy(bset->dim));
+ c = isl_constraint_add_div(c, div, &pos);
+ isl_int_set_si(v, 3);
+ isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
+ bset = isl_basic_set_add_constraint(bset, c);
+
+ c = isl_equality_alloc(isl_dim_copy(bset->dim));
+ isl_int_set_si(v, 1);
+ isl_constraint_set_constant(c, v);
+ isl_int_set_si(v, -1);
+ isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
+ div = isl_div_alloc(isl_dim_copy(bset->dim));
+ c = isl_constraint_add_div(c, div, &pos);
+ isl_int_set_si(v, 3);
+ isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
+ bset = isl_basic_set_add_constraint(bset, c);
+
+ assert(bset->n_div == 1);
+ isl_basic_set_free(bset);
+
+ /* test 2 */
+ dim = isl_dim_set_alloc(ctx, 0, 1);
+ bset = isl_basic_set_universe(dim);
+
+ c = isl_equality_alloc(isl_dim_copy(bset->dim));
+ isl_int_set_si(v, 1);
+ isl_constraint_set_constant(c, v);
+ isl_int_set_si(v, -1);
+ isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
+ div = isl_div_alloc(isl_dim_copy(bset->dim));
+ c = isl_constraint_add_div(c, div, &pos);
+ isl_int_set_si(v, 3);
+ isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
+ bset = isl_basic_set_add_constraint(bset, c);
+
+ c = isl_equality_alloc(isl_dim_copy(bset->dim));
+ isl_int_set_si(v, -1);
+ isl_constraint_set_constant(c, v);
+ isl_int_set_si(v, 1);
+ isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
+ div = isl_div_alloc(isl_dim_copy(bset->dim));
+ c = isl_constraint_add_div(c, div, &pos);
+ isl_int_set_si(v, 3);
+ isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
+ bset = isl_basic_set_add_constraint(bset, c);
+
+ assert(bset->n_div == 1);
+ isl_basic_set_free(bset);
+
+ /* test 3 */
+ dim = isl_dim_set_alloc(ctx, 0, 1);
+ bset = isl_basic_set_universe(dim);
+
+ c = isl_equality_alloc(isl_dim_copy(bset->dim));
+ isl_int_set_si(v, 1);
+ isl_constraint_set_constant(c, v);
+ isl_int_set_si(v, -1);
+ isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
+ div = isl_div_alloc(isl_dim_copy(bset->dim));
+ c = isl_constraint_add_div(c, div, &pos);
+ isl_int_set_si(v, 3);
+ isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
+ bset = isl_basic_set_add_constraint(bset, c);
+
+ c = isl_equality_alloc(isl_dim_copy(bset->dim));
+ isl_int_set_si(v, -3);
+ isl_constraint_set_constant(c, v);
+ isl_int_set_si(v, 1);
+ isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
+ div = isl_div_alloc(isl_dim_copy(bset->dim));
+ c = isl_constraint_add_div(c, div, &pos);
+ isl_int_set_si(v, 4);
+ isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
+ bset = isl_basic_set_add_constraint(bset, c);
+
+ assert(bset->n_div == 1);
+ isl_basic_set_free(bset);
+
+ /* test 4 */
+ dim = isl_dim_set_alloc(ctx, 0, 1);
+ bset = isl_basic_set_universe(dim);
+
+ c = isl_equality_alloc(isl_dim_copy(bset->dim));
+ isl_int_set_si(v, 2);
+ isl_constraint_set_constant(c, v);
+ isl_int_set_si(v, -1);
+ isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
+ div = isl_div_alloc(isl_dim_copy(bset->dim));
+ c = isl_constraint_add_div(c, div, &pos);
+ isl_int_set_si(v, 3);
+ isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
+ bset = isl_basic_set_add_constraint(bset, c);
+
+ c = isl_equality_alloc(isl_dim_copy(bset->dim));
+ isl_int_set_si(v, -1);
+ isl_constraint_set_constant(c, v);
+ isl_int_set_si(v, 1);
+ isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
+ div = isl_div_alloc(isl_dim_copy(bset->dim));
+ c = isl_constraint_add_div(c, div, &pos);
+ isl_int_set_si(v, 6);
+ isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
+ bset = isl_basic_set_add_constraint(bset, c);
+
+ assert(isl_basic_set_is_empty(bset));
+ isl_basic_set_free(bset);
+
+ /* test 5 */
+ dim = isl_dim_set_alloc(ctx, 0, 2);
+ bset = isl_basic_set_universe(dim);
+
+ c = isl_equality_alloc(isl_dim_copy(bset->dim));
+ isl_int_set_si(v, -1);
+ isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
+ div = isl_div_alloc(isl_dim_copy(bset->dim));
+ c = isl_constraint_add_div(c, div, &pos);
+ isl_int_set_si(v, 3);
+ isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
+ bset = isl_basic_set_add_constraint(bset, c);
+
+ c = isl_equality_alloc(isl_dim_copy(bset->dim));
+ isl_int_set_si(v, 1);
+ isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
+ isl_int_set_si(v, -3);
+ isl_constraint_set_coefficient(c, isl_dim_set, 1, v);
+ bset = isl_basic_set_add_constraint(bset, c);
+
+ assert(bset->n_div == 0);
+ isl_basic_set_free(bset);
+
+ /* test 6 */
+ dim = isl_dim_set_alloc(ctx, 0, 2);
+ bset = isl_basic_set_universe(dim);
+
+ c = isl_equality_alloc(isl_dim_copy(bset->dim));
+ isl_int_set_si(v, -1);
+ isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
+ div = isl_div_alloc(isl_dim_copy(bset->dim));
+ c = isl_constraint_add_div(c, div, &pos);
+ isl_int_set_si(v, 6);
+ isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
+ bset = isl_basic_set_add_constraint(bset, c);
+
+ c = isl_equality_alloc(isl_dim_copy(bset->dim));
+ isl_int_set_si(v, 1);
+ isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
+ isl_int_set_si(v, -3);
+ isl_constraint_set_coefficient(c, isl_dim_set, 1, v);
+ bset = isl_basic_set_add_constraint(bset, c);
+
+ assert(bset->n_div == 1);
+ isl_basic_set_free(bset);
+
+ /* test 7 */
+ /* This test is a bit tricky. We set up an equality
+ * a + 3b + 3c = 6 e0
+ * Normalization of divs creates _two_ divs
+ * a = 3 e0
+ * c - b - e0 = 2 e1
+ * Afterwards e0 is removed again because it has coefficient -1
+ * and we end up with the original equality and div again.
+ * Perhaps we can avoid the introduction of this temporary div.
+ */
+ dim = isl_dim_set_alloc(ctx, 0, 3);
+ bset = isl_basic_set_universe(dim);
+
+ c = isl_equality_alloc(isl_dim_copy(bset->dim));
+ isl_int_set_si(v, -1);
+ isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
+ isl_int_set_si(v, -3);
+ isl_constraint_set_coefficient(c, isl_dim_set, 1, v);
+ isl_int_set_si(v, -3);
+ isl_constraint_set_coefficient(c, isl_dim_set, 2, v);
+ div = isl_div_alloc(isl_dim_copy(bset->dim));
+ c = isl_constraint_add_div(c, div, &pos);
+ isl_int_set_si(v, 6);
+ isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
+ bset = isl_basic_set_add_constraint(bset, c);
+
+ assert(bset->n_div == 1);
+ isl_basic_set_free(bset);
+
+ /* test 8 */
+ dim = isl_dim_set_alloc(ctx, 0, 4);
+ bset = isl_basic_set_universe(dim);
+
+ c = isl_equality_alloc(isl_dim_copy(bset->dim));
+ isl_int_set_si(v, -1);
+ isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
+ isl_int_set_si(v, -3);
+ isl_constraint_set_coefficient(c, isl_dim_set, 1, v);
+ isl_int_set_si(v, -3);
+ isl_constraint_set_coefficient(c, isl_dim_set, 3, v);
+ div = isl_div_alloc(isl_dim_copy(bset->dim));
+ c = isl_constraint_add_div(c, div, &pos);
+ isl_int_set_si(v, 6);
+ isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
+ bset = isl_basic_set_add_constraint(bset, c);
+
+ c = isl_equality_alloc(isl_dim_copy(bset->dim));
+ isl_int_set_si(v, -1);
+ isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
+ isl_int_set_si(v, 1);
+ isl_constraint_set_coefficient(c, isl_dim_set, 2, v);
+ isl_int_set_si(v, 1);
+ isl_constraint_set_constant(c, v);
+ bset = isl_basic_set_add_constraint(bset, c);
+
+ assert(bset->n_div == 1);
+ isl_basic_set_free(bset);
+
+ /* test 9 */
+ dim = isl_dim_set_alloc(ctx, 0, 2);
+ bset = isl_basic_set_universe(dim);
+
+ c = isl_equality_alloc(isl_dim_copy(bset->dim));
+ isl_int_set_si(v, 1);
+ isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
+ isl_int_set_si(v, -1);
+ isl_constraint_set_coefficient(c, isl_dim_set, 1, v);
+ div = isl_div_alloc(isl_dim_copy(bset->dim));
+ c = isl_constraint_add_div(c, div, &pos);
+ isl_int_set_si(v, -2);
+ isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
+ bset = isl_basic_set_add_constraint(bset, c);
+
+ c = isl_equality_alloc(isl_dim_copy(bset->dim));
+ isl_int_set_si(v, -1);
+ isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
+ div = isl_div_alloc(isl_dim_copy(bset->dim));
+ c = isl_constraint_add_div(c, div, &pos);
+ isl_int_set_si(v, 3);
+ isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
+ isl_int_set_si(v, 2);
+ isl_constraint_set_constant(c, v);
+ bset = isl_basic_set_add_constraint(bset, c);
+
+ bset = isl_basic_set_fix_si(bset, isl_dim_set, 0, 2);
+
+ assert(!isl_basic_set_is_empty(bset));
+
+ isl_basic_set_free(bset);
+
+ /* test 10 */
+ dim = isl_dim_set_alloc(ctx, 0, 2);
+ bset = isl_basic_set_universe(dim);
+
+ c = isl_equality_alloc(isl_dim_copy(bset->dim));
+ isl_int_set_si(v, 1);
+ isl_constraint_set_coefficient(c, isl_dim_set, 0, v);
+ div = isl_div_alloc(isl_dim_copy(bset->dim));
+ c = isl_constraint_add_div(c, div, &pos);
+ isl_int_set_si(v, -2);
+ isl_constraint_set_coefficient(c, isl_dim_div, pos, v);
+ bset = isl_basic_set_add_constraint(bset, c);
+
+ bset = isl_basic_set_fix_si(bset, isl_dim_set, 0, 2);
+
+ isl_basic_set_free(bset);
+
+ isl_int_clear(v);
+}
+
void test_application_case(struct isl_ctx *ctx, const char *name)
{
char filename[PATH_MAX];
input = fopen(filename, "r");
assert(input);
- bset1 = isl_basic_set_read_from_file(ctx, input, 0, ISL_FORMAT_OMEGA);
- bmap = isl_basic_map_read_from_file(ctx, input, 0, ISL_FORMAT_OMEGA);
+ bset1 = isl_basic_set_read_from_file(ctx, input, 0);
+ bmap = isl_basic_map_read_from_file(ctx, input, 0);
bset1 = isl_basic_set_apply(bset1, bmap);
- bset2 = isl_basic_set_read_from_file(ctx, input, 0, ISL_FORMAT_OMEGA);
+ bset2 = isl_basic_set_read_from_file(ctx, input, 0);
assert(isl_basic_set_is_equal(bset1, bset2) == 1);
input = fopen(filename, "r");
assert(input);
- bset1 = isl_basic_set_read_from_file(ctx, input, 0, ISL_FORMAT_POLYLIB);
- bset2 = isl_basic_set_read_from_file(ctx, input, 0, ISL_FORMAT_POLYLIB);
+ bset1 = isl_basic_set_read_from_file(ctx, input, 0);
+ bset2 = isl_basic_set_read_from_file(ctx, input, 0);
bset1 = isl_basic_set_affine_hull(bset1);
{
test_affine_hull_case(ctx, "affine2");
test_affine_hull_case(ctx, "affine");
+ test_affine_hull_case(ctx, "affine3");
}
void test_convex_hull_case(struct isl_ctx *ctx, const char *name)
input = fopen(filename, "r");
assert(input);
- bset1 = isl_basic_set_read_from_file(ctx, input, 0, ISL_FORMAT_POLYLIB);
- bset2 = isl_basic_set_read_from_file(ctx, input, 0, ISL_FORMAT_POLYLIB);
+ bset1 = isl_basic_set_read_from_file(ctx, input, 0);
+ bset2 = isl_basic_set_read_from_file(ctx, input, 0);
set = isl_basic_set_union(bset1, bset2);
bset1 = isl_set_convex_hull(set);
- bset2 = isl_basic_set_read_from_file(ctx, input, 0, ISL_FORMAT_POLYLIB);
+ bset2 = isl_basic_set_read_from_file(ctx, input, 0);
assert(isl_basic_set_is_equal(bset1, bset2) == 1);
test_convex_hull_case(ctx, "convex6");
test_convex_hull_case(ctx, "convex7");
test_convex_hull_case(ctx, "convex8");
+ test_convex_hull_case(ctx, "convex9");
+ test_convex_hull_case(ctx, "convex10");
+ test_convex_hull_case(ctx, "convex11");
+ test_convex_hull_case(ctx, "convex12");
+ test_convex_hull_case(ctx, "convex13");
+ test_convex_hull_case(ctx, "convex14");
+}
+
+void test_gist_case(struct isl_ctx *ctx, const char *name)
+{
+ char filename[PATH_MAX];
+ FILE *input;
+ int n;
+ struct isl_basic_set *bset1, *bset2;
+
+ n = snprintf(filename, sizeof(filename),
+ "%s/test_inputs/%s.polylib", srcdir, name);
+ assert(n < sizeof(filename));
+ input = fopen(filename, "r");
+ assert(input);
+
+ bset1 = isl_basic_set_read_from_file(ctx, input, 0);
+ bset2 = isl_basic_set_read_from_file(ctx, input, 0);
+
+ bset1 = isl_basic_set_gist(bset1, bset2);
+
+ bset2 = isl_basic_set_read_from_file(ctx, input, 0);
+
+ assert(isl_basic_set_is_equal(bset1, bset2) == 1);
+
+ isl_basic_set_free(bset1);
+ isl_basic_set_free(bset2);
+
+ fclose(input);
+}
+
+void test_gist(struct isl_ctx *ctx)
+{
+ test_gist_case(ctx, "gist1");
+}
+
+static struct isl_set *s_union(struct isl_ctx *ctx,
+ const char *s1, const char *s2)
+{
+ struct isl_basic_set *bset1;
+ struct isl_basic_set *bset2;
+ struct isl_set *set1, *set2;
+
+ bset1 = isl_basic_set_read_from_str(ctx, s1, 0);
+ bset2 = isl_basic_set_read_from_str(ctx, s2, 0);
+ set1 = isl_set_from_basic_set(bset1);
+ set2 = isl_set_from_basic_set(bset2);
+ return isl_set_union(set1, set2);
+}
+
+void test_coalesce(struct isl_ctx *ctx)
+{
+ struct isl_set *set;
+
+ set = s_union(ctx, "{[x,y]: x >= 0 & x <= 10 & y >= 0 & y <= 10}",
+ "{[x,y]: y >= x & x >= 2 & 5 >= y}");
+ set = isl_set_coalesce(set);
+ assert(set && set->n == 1);
+ isl_set_free(set);
+
+ set = s_union(ctx, "{[x,y]: y >= 0 & 2x + y <= 30 & y <= 10 & x >= 0}",
+ "{[x,y]: x + y >= 10 & y <= x & x + y <= 20 & y >= 0}");
+ set = isl_set_coalesce(set);
+ assert(set && set->n == 1);
+ isl_set_free(set);
+
+ set = s_union(ctx, "{[x,y]: y >= 0 & 2x + y <= 30 & y <= 10 & x >= 0}",
+ "{[x,y]: x + y >= 10 & y <= x & x + y <= 19 & y >= 0}");
+ set = isl_set_coalesce(set);
+ assert(set && set->n == 2);
+ isl_set_free(set);
+
+ set = s_union(ctx, "{[x,y]: y >= 0 & x <= 5 & y <= x}",
+ "{[x,y]: y >= 0 & x >= 6 & x <= 10 & y <= x}");
+ set = isl_set_coalesce(set);
+ assert(set && set->n == 1);
+ isl_set_free(set);
+
+ set = s_union(ctx, "{[x,y]: y >= 0 & x <= 5 & y <= x}",
+ "{[x,y]: y >= 0 & x >= 7 & x <= 10 & y <= x}");
+ set = isl_set_coalesce(set);
+ assert(set && set->n == 2);
+ isl_set_free(set);
+
+ set = s_union(ctx, "{[x,y]: y >= 0 & x <= 5 & y <= x}",
+ "{[x,y]: y >= 0 & x >= 6 & x <= 10 & y + 1 <= x}");
+ set = isl_set_coalesce(set);
+ assert(set && set->n == 2);
+ isl_set_free(set);
+
+ set = s_union(ctx, "{[x,y]: y >= 0 & x <= 5 & y <= x}",
+ "{[x,y]: y >= 0 & x = 6 & y <= 6}");
+ set = isl_set_coalesce(set);
+ assert(set && set->n == 1);
+ isl_set_free(set);
+
+ set = s_union(ctx, "{[x,y]: y >= 0 & x <= 5 & y <= x}",
+ "{[x,y]: y >= 0 & x = 7 & y <= 6}");
+ set = isl_set_coalesce(set);
+ assert(set && set->n == 2);
+ isl_set_free(set);
+
+ set = s_union(ctx, "{[x,y]: y >= 0 & x <= 5 & y <= x}",
+ "{[x,y]: y >= 0 & x = 6 & y <= 5}");
+ set = isl_set_coalesce(set);
+ assert(set && set->n == 2);
+ isl_set_free(set);
+
+ set = s_union(ctx, "{[x,y]: y >= 0 & x <= 5 & y <= x}",
+ "{[x,y]: y >= 0 & x = 6 & y <= 7}");
+ set = isl_set_coalesce(set);
+ assert(set && set->n == 2);
+ isl_set_free(set);
}
int main()
struct isl_ctx *ctx;
srcdir = getenv("srcdir");
+ assert(srcdir);
ctx = isl_ctx_alloc();
+ test_read(ctx);
+ test_construction(ctx);
+ test_div(ctx);
test_application(ctx);
test_affine_hull(ctx);
test_convex_hull(ctx);
+ test_gist(ctx);
+ test_coalesce(ctx);
isl_ctx_free(ctx);
return 0;
}