isl_map_simplify.c: normalize_divs: ensure enough existentials are available

[platform/upstream/isl.git] / isl_test.c

diff --git a/isl_test.c b/isl_test.c
index 3ca3879..8db04a4 100644 (file)
--- a/isl_test.c
+++ b/isl_test.c
@@ -7,16 +7,43 @@
 
 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, ISL_FORMAT_OMEGA);
+       bset2 = isl_basic_set_read_from_str(ctx, str, 0, ISL_FORMAT_OMEGA);
+
+       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);
 
-       bset = isl_basic_set_universe(ctx, 1, 1);
+       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);
@@ -37,6 +64,211 @@ void test_construction(struct isl_ctx *ctx)
        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);
+
+       isl_int_clear(v);
+}
+
 void test_application_case(struct isl_ctx *ctx, const char *name)
 {
        char filename[PATH_MAX];
@@ -191,7 +423,9 @@ int main()
        srcdir = getenv("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);