add convex hull computation
authorSven Verdoolaege <skimo@kotnet.org>
Fri, 15 Aug 2008 19:56:30 +0000 (21:56 +0200)
committerSven Verdoolaege <skimo@kotnet.org>
Mon, 25 Aug 2008 08:15:08 +0000 (10:15 +0200)
24 files changed:
Makefile.am
include/isl_int.h
include/isl_lp.h
include/isl_lp_piplib.h
include/isl_map.h
include/isl_set.h
isl_affine_hull.c
isl_convex_hull.c [new file with mode: 0644]
isl_lp.c
isl_lp_no_piplib.c
isl_lp_piplib.c
isl_map.c
isl_map_private.h
isl_mat.c
isl_mat.h
isl_test.c [new file with mode: 0644]
test_inputs/convex0.polylib [new file with mode: 0644]
test_inputs/convex1.polylib [new file with mode: 0644]
test_inputs/convex2.polylib [new file with mode: 0644]
test_inputs/convex3.polylib [new file with mode: 0644]
test_inputs/convex4.polylib [new file with mode: 0644]
test_inputs/convex5.polylib [new file with mode: 0644]
test_inputs/convex6.polylib [new file with mode: 0644]
test_inputs/convex7.polylib [new file with mode: 0644]

index 9ef7107..8171c28 100644 (file)
@@ -5,6 +5,8 @@ endif
 SUBDIRS = $(MAYBE_PIPLIB) .
 
 lib_LTLIBRARIES = libisl.la
+noinst_PROGRAMS = isl_test
+TESTS = isl_test
 
 if HAVE_POLYLIB
 ISL_POLYLIB = \
@@ -34,6 +36,7 @@ libisl_la_SOURCES = \
        isl_affine_hull.c \
        isl_blk.c \
        isl_blk.h \
+       isl_convex_hull.c \
        isl_ctx.c \
        isl_ctx.h \
        isl_equalities.c \
@@ -71,6 +74,9 @@ libisl_la_CPPFLAGS = -I$(srcdir)/include -Iinclude/ \
        @PIPLIB_CPPFLAGS@ @POLYLIB_CPPFLAGS@ \
        @GMP_CPPFLAGS@
 
+isl_test_CPPFLAGS = -I$(srcdir)/include -Iinclude/
+isl_test_LDADD = libisl.la
+
 pkginclude_HEADERS = \
        include/isl_blk.h \
        include/isl_ctx.h \
index 4164170..5dcc0b6 100644 (file)
@@ -55,6 +55,7 @@ typedef mpz_t isl_int;
 #define isl_int_eq(i,j)                (mpz_cmp(i,j) == 0)
 #define isl_int_ne(i,j)                (mpz_cmp(i,j) != 0)
 #define isl_int_lt(i,j)                (mpz_cmp(i,j) < 0)
+#define isl_int_gt(i,j)                (mpz_cmp(i,j) > 0)
 #define isl_int_abs_eq(i,j)    (mpz_cmpabs(i,j) == 0)
 #define isl_int_abs_ne(i,j)    (mpz_cmpabs(i,j) != 0)
 #define isl_int_abs_lt(i,j)    (mpz_cmpabs(i,j) < 0)
index 5179cac..c86b93b 100644 (file)
@@ -15,7 +15,8 @@ extern "C" {
 #endif
 
 enum isl_lp_result isl_solve_lp(struct isl_basic_map *bmap, int maximize,
-                                     isl_int *f, isl_int denom, isl_int *opt);
+                                     isl_int *f, isl_int denom, isl_int *opt,
+                                     isl_int *opt_denom);
 
 #if defined(__cplusplus)
 }
index c1363ea..190606e 100644 (file)
@@ -8,7 +8,8 @@ extern "C" {
 #endif
 
 enum isl_lp_result isl_pip_solve_lp(struct isl_basic_map *bmap, int maximize,
-                                     isl_int *f, isl_int denom, isl_int *opt);
+                                     isl_int *f, isl_int denom, isl_int *opt,
+                                     isl_int *opt_denom);
 
 #if defined(__cplusplus)
 }
index 8aa8086..dc6437e 100644 (file)
@@ -39,6 +39,8 @@ struct isl_basic_map {
 #define ISL_BASIC_MAP_FINAL            (1 << 0)
 #define ISL_BASIC_MAP_EMPTY            (1 << 1)
 #define ISL_BASIC_MAP_NO_IMPLICIT      (1 << 2)
+#define ISL_BASIC_MAP_NO_REDUNDANT     (1 << 3)
+#define ISL_BASIC_MAP_RATIONAL         (1 << 4)
        unsigned flags;
 
        unsigned nparam;
@@ -108,6 +110,8 @@ struct isl_basic_map *isl_basic_map_more_at(struct isl_ctx *ctx,
                unsigned nparam, unsigned in, unsigned out, unsigned pos);
 struct isl_basic_map *isl_basic_map_empty(struct isl_ctx *ctx,
                unsigned nparam, unsigned in, unsigned out);
+struct isl_basic_map *isl_basic_map_universe(struct isl_ctx *ctx,
+               unsigned nparam, unsigned in, unsigned out);
 
 struct isl_basic_map *isl_basic_map_intersect_domain(
                struct isl_ctx *ctx, struct isl_basic_map *bmap,
@@ -148,6 +152,8 @@ struct isl_map *isl_basic_map_lexmin(struct isl_ctx *ctx,
 void isl_basic_map_dump(struct isl_ctx *ctx, struct isl_basic_map *bmap,
                                FILE *out, int indent);
 
+int isl_basic_map_is_universe(struct isl_ctx *ctx,
+               struct isl_basic_map *bmap);
 int isl_basic_map_is_empty(struct isl_ctx *ctx,
                struct isl_basic_map *bmap);
 int isl_basic_map_is_subset(struct isl_ctx *ctx,
index 501ca30..48d474c 100644 (file)
@@ -69,6 +69,8 @@ struct isl_basic_set *isl_basic_set_finalize(struct isl_ctx *ctx,
 void isl_basic_set_free(struct isl_ctx *ctx, struct isl_basic_set *bset);
 struct isl_basic_set *isl_basic_set_copy(struct isl_ctx *ctx,
                                        struct isl_basic_set *bset);
+struct isl_basic_set *isl_basic_set_universe(struct isl_ctx *ctx,
+               unsigned nparam, unsigned dim);
 void isl_basic_set_dump(struct isl_ctx *ctx, struct isl_basic_set *bset,
                                FILE *out, int indent);
 struct isl_basic_set *isl_basic_set_swap_vars(struct isl_ctx *ctx,
@@ -86,6 +88,9 @@ struct isl_basic_set *isl_basic_set_simplify(
 struct isl_basic_set *isl_basic_set_read_from_file(struct isl_ctx *ctx,
                FILE *input, unsigned input_format);
 
+int isl_basic_set_is_equal(struct isl_ctx *ctx,
+               struct isl_basic_set *bset1, struct isl_basic_set *bset2);
+
 struct isl_set *isl_basic_set_lexmin(struct isl_ctx *ctx,
                struct isl_basic_set *bset);
 struct isl_set *isl_basic_set_union(
@@ -106,6 +111,8 @@ struct isl_set *isl_set_from_basic_set(struct isl_ctx *ctx,
                                struct isl_basic_set *bset);
 struct isl_basic_set *isl_set_affine_hull(struct isl_ctx *ctx,
                struct isl_set *set);
+struct isl_basic_set *isl_set_convex_hull(struct isl_ctx *ctx,
+               struct isl_set *set);
 
 struct isl_set *isl_set_union_disjoint(struct isl_ctx *ctx,
                        struct isl_set *set1, struct isl_set *set2);
index e8df67c..4dae661 100644 (file)
@@ -22,7 +22,7 @@ struct isl_basic_map *isl_basic_map_implicit_equalities(struct isl_ctx *ctx,
        isl_int_init(opt);
        for (i = 0; i < bmap->n_ineq; ++i) {
                enum isl_lp_result res;
-               res = isl_solve_lp(bmap, 1, bmap->ineq[i]+1, ctx->one, &opt);
+               res = isl_solve_lp(bmap, 1, bmap->ineq[i]+1, ctx->one, &opt, NULL);
                if (res == isl_lp_unbounded)
                        continue;
                if (res == isl_lp_error)
diff --git a/isl_convex_hull.c b/isl_convex_hull.c
new file mode 100644 (file)
index 0000000..b140b47
--- /dev/null
@@ -0,0 +1,1017 @@
+#include "isl_lp.h"
+#include "isl_map.h"
+#include "isl_map_private.h"
+#include "isl_mat.h"
+#include "isl_set.h"
+#include "isl_seq.h"
+#include "isl_equalities.h"
+
+static struct isl_basic_set *uset_convex_hull(struct isl_ctx *ctx,
+       struct isl_set *set);
+
+static swap_ineq(struct isl_basic_map *bmap, unsigned i, unsigned j)
+{
+       isl_int *t;
+
+       if (i != j) {
+               t = bmap->ineq[i];
+               bmap->ineq[i] = bmap->ineq[j];
+               bmap->ineq[j] = t;
+       }
+}
+
+/* Compute the convex hull of a basic map, by removing the redundant
+ * constraints.  If the minimal value along the normal of a constraint
+ * is the same if the constraint is removed, then the constraint is redundant.
+ *
+ * Alternatively, we could have intersected the basic map with the
+ * corresponding equality and the checked if the dimension was that
+ * of a facet.
+ */
+struct isl_basic_map *isl_basic_map_convex_hull(struct isl_ctx *ctx,
+                                               struct isl_basic_map *bmap)
+{
+       int i;
+       isl_int opt_n;
+       isl_int opt_d;
+
+       bmap = isl_basic_map_implicit_equalities(ctx, bmap);
+       if (!bmap)
+               return NULL;
+
+       if (F_ISSET(bmap, ISL_BASIC_MAP_EMPTY))
+               return bmap;
+       if (F_ISSET(bmap, ISL_BASIC_MAP_NO_REDUNDANT))
+               return bmap;
+
+       isl_int_init(opt_n);
+       isl_int_init(opt_d);
+       for (i = bmap->n_ineq-1; i >= 0; --i) {
+               enum isl_lp_result res;
+               swap_ineq(bmap, i, bmap->n_ineq-1);
+               bmap->n_ineq--;
+               res = isl_solve_lp(bmap, 0,
+                       bmap->ineq[bmap->n_ineq]+1, ctx->one, &opt_n, &opt_d);
+               bmap->n_ineq++;
+               swap_ineq(bmap, i, bmap->n_ineq-1);
+               if (res == isl_lp_unbounded)
+                       continue;
+               if (res == isl_lp_error)
+                       goto error;
+               if (res == isl_lp_empty) {
+                       bmap = isl_basic_map_set_to_empty(ctx, bmap);
+                       break;
+               }
+               isl_int_addmul(opt_n, opt_d, bmap->ineq[i][0]);
+               if (!isl_int_is_neg(opt_n))
+                       isl_basic_map_drop_inequality(ctx, bmap, i);
+       }
+       isl_int_clear(opt_n);
+       isl_int_clear(opt_d);
+
+       F_SET(bmap, ISL_BASIC_MAP_NO_REDUNDANT);
+       return bmap;
+error:
+       isl_int_clear(opt_n);
+       isl_int_clear(opt_d);
+       isl_basic_map_free(ctx, bmap);
+       return NULL;
+}
+
+struct isl_basic_set *isl_basic_set_convex_hull(struct isl_ctx *ctx,
+                                               struct isl_basic_set *bset)
+{
+       return (struct isl_basic_set *)isl_basic_map_convex_hull(ctx,
+                                               (struct isl_basic_map *)bset);
+}
+
+/* Check if "c" is a direction with a lower bound in "set" that is independent
+ * of the previously found "n" bounds in "dirs".
+ * If so, add it to the list, with the negative of the lower bound
+ * in the constant position, i.e., such that c correspond to a bounding
+ * hyperplane (but not necessarily a facet).
+ */
+static int is_independent_bound(struct isl_ctx *ctx,
+       struct isl_set *set, isl_int *c,
+       struct isl_mat *dirs, int n)
+{
+       int first;
+       int i = 0, j;
+       isl_int opt;
+       isl_int opt_denom;
+
+       isl_seq_cpy(dirs->row[n]+1, c+1, dirs->n_col-1);
+       if (n != 0) {
+               int pos = isl_seq_first_non_zero(dirs->row[n]+1, dirs->n_col-1);
+               if (pos < 0)
+                       return 0;
+               for (i = 0; i < n; ++i) {
+                       int pos_i;
+                       pos_i = isl_seq_first_non_zero(dirs->row[i]+1, dirs->n_col-1);
+                       if (pos_i < pos)
+                               continue;
+                       if (pos_i > pos)
+                               break;
+                       isl_seq_elim(dirs->row[n]+1, dirs->row[i]+1, pos,
+                                       dirs->n_col-1, NULL);
+                       pos = isl_seq_first_non_zero(dirs->row[n]+1, dirs->n_col-1);
+                       if (pos < 0)
+                               return 0;
+               }
+       }
+
+       isl_int_init(opt);
+       isl_int_init(opt_denom);
+       first = 1;
+       for (j = 0; j < set->n; ++j) {
+               enum isl_lp_result res;
+
+               if (F_ISSET(set->p[j], ISL_BASIC_MAP_EMPTY))
+                       continue;
+
+               res = isl_solve_lp((struct isl_basic_map*)set->p[j],
+                               0, dirs->row[n]+1, ctx->one, &opt, &opt_denom);
+               if (res == isl_lp_unbounded)
+                       break;
+               if (res == isl_lp_error)
+                       goto error;
+               if (res == isl_lp_empty) {
+                       set->p[j] = isl_basic_set_set_to_empty(ctx, set->p[j]);
+                       if (!set->p[j])
+                               goto error;
+                       continue;
+               }
+               if (!isl_int_is_one(opt_denom))
+                       isl_seq_scale(dirs->row[n], dirs->row[n], opt_denom,
+                                       dirs->n_col);
+               if (first || isl_int_lt(opt, dirs->row[n][0]))
+                       isl_int_set(dirs->row[n][0], opt);
+               first = 0;
+       }
+       isl_int_clear(opt);
+       isl_int_clear(opt_denom);
+       if (j < set->n)
+               return 0;
+       isl_int_neg(dirs->row[n][0], dirs->row[n][0]);
+       if (i < n) {
+               int k;
+               isl_int *t = dirs->row[n];
+               for (k = n; k > i; --k)
+                       dirs->row[k] = dirs->row[k-1];
+               dirs->row[i] = t;
+       }
+       return 1;
+error:
+       isl_int_clear(opt);
+       isl_int_clear(opt_denom);
+       return -1;
+}
+
+/* Compute and return a maximal set of linearly independent bounds
+ * on the set "set", based on the constraints of the basic sets
+ * in "set".
+ */
+static struct isl_mat *independent_bounds(struct isl_ctx *ctx,
+       struct isl_set *set)
+{
+       int i, j, n;
+       struct isl_mat *dirs = NULL;
+
+       dirs = isl_mat_alloc(ctx, set->dim, 1+set->dim);
+       if (!dirs)
+               goto error;
+
+       n = 0;
+       for (i = 0; n < set->dim && i < set->n; ++i) {
+               int f;
+               struct isl_basic_set *bset = set->p[i];
+
+               for (j = 0; n < set->dim && j < bset->n_eq; ++j) {
+                       f = is_independent_bound(ctx, set, bset->eq[j],
+                                               dirs, n);
+                       if (f < 0)
+                               goto error;
+                       if (f) {
+                               ++n;
+                               continue;
+                       }
+                       isl_seq_neg(bset->eq[j], bset->eq[j], 1+set->dim);
+                       f = is_independent_bound(ctx, set, bset->eq[j],
+                                               dirs, n);
+                       isl_seq_neg(bset->eq[j], bset->eq[j], 1+set->dim);
+                       if (f < 0)
+                               goto error;
+                       if (f)
+                               ++n;
+               }
+               for (j = 0; n < set->dim && j < bset->n_ineq; ++j) {
+                       f = is_independent_bound(ctx, set, bset->ineq[j],
+                                               dirs, n);
+                       if (f < 0)
+                               goto error;
+                       if (f)
+                               ++n;
+               }
+       }
+       dirs->n_row = n;
+       return dirs;
+error:
+       isl_mat_free(ctx, dirs);
+       return NULL;
+}
+
+static struct isl_basic_set *isl_basic_set_set_rational(struct isl_ctx *ctx,
+       struct isl_basic_set *bset)
+{
+       if (!bset)
+               return NULL;
+
+       if (F_ISSET(bset, ISL_BASIC_MAP_RATIONAL))
+               return bset;
+
+       bset = isl_basic_set_cow(ctx, bset);
+       if (!bset)
+               return NULL;
+
+       F_SET(bset, ISL_BASIC_MAP_RATIONAL);
+
+       return bset;
+}
+
+static struct isl_set *isl_set_set_rational(struct isl_ctx *ctx,
+       struct isl_set *set)
+{
+       int i;
+
+       set = isl_set_cow(ctx, set);
+       if (!set)
+               return NULL;
+       for (i = 0; i < set->n; ++i) {
+               set->p[i] = isl_basic_set_set_rational(ctx, set->p[i]);
+               if (!set->p[i])
+                       goto error;
+       }
+       return set;
+error:
+       isl_set_free(ctx, set);
+       return NULL;
+}
+
+static struct isl_basic_set *isl_basic_set_add_equality(struct isl_ctx *ctx,
+       struct isl_basic_set *bset, isl_int *c)
+{
+       int i;
+       unsigned total;
+
+       isl_assert(ctx, bset->nparam == 0, goto error);
+       isl_assert(ctx, bset->n_div == 0, goto error);
+       bset = isl_basic_set_extend(ctx, bset, 0, bset->dim, 0, 1, 0);
+       i = isl_basic_set_alloc_equality(ctx, bset);
+       if (i < 0)
+               goto error;
+       isl_seq_cpy(bset->eq[i], c, 1 + bset->dim);
+       return bset;
+error:
+       isl_basic_set_free(ctx, bset);
+       return NULL;
+}
+
+static struct isl_set *isl_set_add_equality(struct isl_ctx *ctx,
+       struct isl_set *set, isl_int *c)
+{
+       int i;
+
+       set = isl_set_cow(ctx, set);
+       if (!set)
+               return NULL;
+       for (i = 0; i < set->n; ++i) {
+               set->p[i] = isl_basic_set_add_equality(ctx, set->p[i], c);
+               if (!set->p[i])
+                       goto error;
+       }
+       return set;
+error:
+       isl_set_free(ctx, set);
+       return NULL;
+}
+
+/* Given a union of basic sets, construct the constraints for wrapping
+ * a facet around one of its ridges.
+ * In particular, if each of n the d-dimensional basic sets i in "set"
+ * contains the origin, satisfies the constraints x_1 >= 0 and x_2 >= 0
+ * and is defined by the constraints
+ *                                 [ 1 ]
+ *                             A_i [ x ]  >= 0
+ *
+ * then the resulting set is of dimension n*(1+d) and has as contraints
+ *
+ *                                 [ a_i ]
+ *                             A_i [ x_i ] >= 0
+ *
+ *                                   a_i   >= 0
+ *
+ *                     \sum_i x_{i,1} = 1
+ */
+static struct isl_basic_set *wrap_constraints(struct isl_ctx *ctx,
+                                                       struct isl_set *set)
+{
+       struct isl_basic_set *lp;
+       unsigned n_eq;
+       unsigned n_ineq;
+       int i, j, k;
+       unsigned dim;
+
+       if (!set)
+               return NULL;
+
+       dim = 1 + set->dim;
+       n_eq = 1;
+       n_ineq = set->n;
+       for (i = 0; i < set->n; ++i) {
+               n_eq += set->p[i]->n_eq;
+               n_ineq += set->p[i]->n_ineq;
+       }
+       lp = isl_basic_set_alloc(ctx, 0, dim * set->n, 0, n_eq, n_ineq);
+       if (!lp)
+               return NULL;
+       k = isl_basic_set_alloc_equality(ctx, lp);
+       isl_int_set_si(lp->eq[k][0], -1);
+       for (i = 0; i < set->n; ++i) {
+               isl_int_set_si(lp->eq[k][1+dim*i], 0);
+               isl_int_set_si(lp->eq[k][1+dim*i+1], 1);
+               isl_seq_clr(lp->eq[k]+1+dim*i+2, dim-2);
+       }
+       for (i = 0; i < set->n; ++i) {
+               k = isl_basic_set_alloc_inequality(ctx, lp);
+               isl_seq_clr(lp->ineq[k], 1+lp->dim);
+               isl_int_set_si(lp->ineq[k][1+dim*i], 1);
+
+               for (j = 0; j < set->p[i]->n_eq; ++j) {
+                       k = isl_basic_set_alloc_equality(ctx, lp);
+                       isl_seq_clr(lp->eq[k], 1+dim*i);
+                       isl_seq_cpy(lp->eq[k]+1+dim*i, set->p[i]->eq[j], dim);
+                       isl_seq_clr(lp->eq[k]+1+dim*(i+1), dim*(set->n-i-1));
+               }
+
+               for (j = 0; j < set->p[i]->n_ineq; ++j) {
+                       k = isl_basic_set_alloc_inequality(ctx, lp);
+                       isl_seq_clr(lp->ineq[k], 1+dim*i);
+                       isl_seq_cpy(lp->ineq[k]+1+dim*i, set->p[i]->ineq[j], dim);
+                       isl_seq_clr(lp->ineq[k]+1+dim*(i+1), dim*(set->n-i-1));
+               }
+       }
+       return lp;
+}
+
+/* Given a facet "facet" of the convex hull of "set" and a facet "ridge"
+ * of that facet, compute the other facet of the convex hull that contains
+ * the ridge.
+ *
+ * We first transform the set such that the facet constraint becomes
+ *
+ *                     x_1 >= 0
+ *
+ * I.e., the facet is
+ *
+ *                     x_1 = 0
+ *
+ * and on that facet, the constraint that defines the ridge is
+ *
+ *                     x_2 >= 0
+ *
+ * (This transformation is not strictly needed, all that is needed is
+ * that the ridge contains the origin.)
+ *
+ * Since the ridge contains the origin, the cone of the convex hull
+ * will be of the form
+ *
+ *                     x_1 >= 0
+ *                     x_2 >= a x_1
+ *
+ * with this second constraint defining the new facet.
+ * The constant a is obtained by settting x_1 in the cone of the
+ * convex hull to 1 and minimizing x_2.
+ * Now, each element in the cone of the convex hull is the sum
+ * of elements in the cones of the basic sets.
+ * If a_i is the dilation factor of basic set i, then the problem
+ * we need to solve is
+ *
+ *                     min \sum_i x_{i,2}
+ *                     st
+ *                             \sum_i x_{i,1} = 1
+ *                                 a_i   >= 0
+ *                               [ a_i ]
+ *                             A [ x_i ] >= 0
+ *
+ * with
+ *                                 [  1  ]
+ *                             A_i [ x_i ] >= 0
+ *
+ * the constraints of each (transformed) basic set.
+ * If a = n/d, then the consstraint defining the new facet (in the transformed
+ * space) is
+ *
+ *                     -n x_1 + d x_2 >= 0
+ *
+ * In the original space, we need to take the same combination of the
+ * corresponding constraints "facet" and "ridge".
+ */
+static isl_int *wrap_facet(struct isl_ctx *ctx, struct isl_set *set,
+       isl_int *facet, isl_int *ridge)
+{
+       int i;
+       struct isl_mat *T = NULL;
+       struct isl_basic_set *lp = NULL;
+       struct isl_vec *obj;
+       enum isl_lp_result res;
+       isl_int num, den;
+       unsigned dim;
+
+       set = isl_set_copy(ctx, set);
+
+       dim = 1 + set->dim;
+       T = isl_mat_alloc(ctx, 3, 1 + set->dim);
+       if (!T)
+               goto error;
+       isl_int_set_si(T->row[0][0], 1);
+       isl_seq_clr(T->row[0]+1, set->dim);
+       isl_seq_cpy(T->row[1], facet, 1+set->dim);
+       isl_seq_cpy(T->row[2], ridge, 1+set->dim);
+       T = isl_mat_right_inverse(ctx, T);
+       set = isl_set_preimage(ctx, set, T);
+       T = NULL;
+       lp = wrap_constraints(ctx, set);
+       obj = isl_vec_alloc(ctx, dim*set->n);
+       if (!obj)
+               goto error;
+       for (i = 0; i < set->n; ++i) {
+               isl_seq_clr(obj->block.data+dim*i, 2);
+               isl_int_set_si(obj->block.data[dim*i+2], 1);
+               isl_seq_clr(obj->block.data+dim*i+3, dim-3);
+       }
+       isl_int_init(num);
+       isl_int_init(den);
+       res = isl_solve_lp((struct isl_basic_map *)lp, 0,
+                                       obj->block.data, ctx->one, &num, &den);
+       if (res == isl_lp_ok) {
+               isl_int_neg(num, num);
+               isl_seq_combine(facet, num, facet, den, ridge, dim);
+       }
+       isl_int_clear(num);
+       isl_int_clear(den);
+       isl_vec_free(ctx, obj);
+       isl_basic_set_free(ctx, lp);
+       isl_set_free(ctx, set);
+       return (res == isl_lp_ok) ? facet : NULL;
+error:
+       isl_basic_set_free(ctx, lp);
+       isl_mat_free(ctx, T);
+       isl_set_free(ctx, set);
+       return NULL;
+}
+
+/* Given a direction of a constraint, compute the constant term
+ * such that the resulting constraint is a bounding constraint
+ * of the set "set" (which just happens to be a face of the
+ * original set).
+ */
+static int compute_bound_on_face(struct isl_ctx *ctx,
+       struct isl_set *set, isl_int *c)
+{
+       int first = 1;
+       int j;
+       isl_int opt;
+       isl_int opt_denom;
+
+       isl_int_init(opt);
+       isl_int_init(opt_denom);
+       for (j = 0; j < set->n; ++j) {
+               enum isl_lp_result res;
+
+               if (F_ISSET(set->p[j], ISL_BASIC_MAP_EMPTY))
+                       continue;
+
+               res = isl_solve_lp((struct isl_basic_map*)set->p[j],
+                                       0, c+1, ctx->one, &opt, &opt_denom);
+               if (res == isl_lp_unbounded)
+                       goto error;
+               if (res == isl_lp_error)
+                       goto error;
+               if (res == isl_lp_empty) {
+                       set->p[j] = isl_basic_set_set_to_empty(ctx, set->p[j]);
+                       if (!set->p[j])
+                               goto error;
+                       continue;
+               }
+               if (!isl_int_is_one(opt_denom))
+                       isl_seq_scale(c, c, opt_denom, 1+set->dim);
+               if (first || isl_int_lt(opt, c[0]))
+                       isl_int_set(c[0], opt);
+               first = 0;
+       }
+       isl_assert(ctx, !first, goto error);
+       isl_int_clear(opt);
+       isl_int_clear(opt_denom);
+       isl_int_neg(c[0], c[0]);
+       return 0;
+error:
+       isl_int_clear(opt);
+       isl_int_clear(opt_denom);
+       return -1;
+}
+
+/* Given a set of d linearly independent bounding constraints of the
+ * convex hull of "set", compute the constraint of a facet of "set".
+ *
+ * We first compute the intersection with the first bounding hyperplane
+ * and shift the second bounding constraint to be a bounding constraint
+ * of the resulting face.  We then wrap around the next bounding constraint
+ * and continue the process until all bounding constraints have been
+ * taken into account.
+ * The resulting linear combination of the bounding constraints will
+ * correspond to a facet of the convex hull.
+ */
+static struct isl_mat *initial_facet_constraint(struct isl_ctx *ctx,
+       struct isl_set *set, struct isl_mat *bounds)
+{
+       struct isl_set *face = NULL;
+       int i;
+
+       isl_assert(ctx, set->n > 0, goto error);
+       isl_assert(ctx, bounds->n_row == set->dim, goto error);
+
+       face = isl_set_copy(ctx, set);
+       if (!face)
+               goto error;
+       for (i = 1; i < set->dim; ++i) {
+               face = isl_set_add_equality(ctx, face, bounds->row[i-1]);
+               if (compute_bound_on_face(ctx, face, bounds->row[i]) < 0)
+                       goto error;
+               if (!wrap_facet(ctx, set, bounds->row[0], bounds->row[i]))
+                       goto error;
+       }
+       isl_set_free(ctx, face);
+       return bounds;
+error:
+       isl_set_free(ctx, face);
+       isl_mat_free(ctx, bounds);
+       return NULL;
+}
+
+/* Given the bounding constraint "c" of a facet of the convex hull of "set",
+ * compute a hyperplane description of the facet, i.e., compute the facets
+ * of the facet.
+ *
+ * We compute an affine transformation that transforms the constraint
+ *
+ *                       [ 1 ]
+ *                     c [ x ] = 0
+ *
+ * to the constraint
+ *
+ *                        z_1  = 0
+ *
+ * by computing the right inverse U of a matrix that starts with the rows
+ *
+ *                     [ 1 0 ]
+ *                     [  c  ]
+ *
+ * Then
+ *                     [ 1 ]     [ 1 ]
+ *                     [ x ] = U [ z ]
+ * and
+ *                     [ 1 ]     [ 1 ]
+ *                     [ z ] = Q [ x ]
+ *
+ * with Q = U^{-1}
+ * Since z_1 is zero, we can drop this variable as well as the corresponding
+ * column of U to obtain
+ *
+ *                     [ 1 ]      [ 1  ]
+ *                     [ x ] = U' [ z' ]
+ * and
+ *                     [ 1  ]      [ 1 ]
+ *                     [ z' ] = Q' [ x ]
+ *
+ * with Q' equal to Q, but without the corresponding row.
+ * After computing the facets of the facet in the z' space,
+ * we convert them back to the x space through Q.
+ */
+static struct isl_basic_set *compute_facet(struct isl_ctx *ctx,
+       struct isl_set *set, isl_int *c)
+{
+       struct isl_mat *m, *U, *Q;
+       struct isl_basic_set *facet;
+
+       set = isl_set_copy(ctx, set);
+       m = isl_mat_alloc(ctx, 2, 1 + set->dim);
+       if (!m)
+               goto error;
+       isl_int_set_si(m->row[0][0], 1);
+       isl_seq_clr(m->row[0]+1, set->dim);
+       isl_seq_cpy(m->row[1], c, 1+set->dim);
+       m = isl_mat_left_hermite(ctx, m, &U, &Q);
+       if (!m)
+               goto error;
+       U = isl_mat_drop_col(ctx, U, 1);
+       Q = isl_mat_drop_rows(ctx, Q, 1, 1);
+       set = isl_set_preimage(ctx, set, U);
+       facet = uset_convex_hull(ctx, set);
+       facet = isl_basic_set_preimage(ctx, facet, Q);
+       isl_mat_free(ctx, m);
+       return facet;
+error:
+       isl_set_free(ctx, set);
+       return NULL;
+}
+
+/* Given an initial facet constraint, compute the remaining facets.
+ * We do this by running through all facets found so far and computing
+ * the adjacent facets through wrapping, adding those facets that we
+ * hadn't already found before.
+ *
+ * This function can still be significantly optimized by checking which of
+ * the facets of the basic sets are also facets of the convex hull and
+ * using all the facets so far to help in constructing the facets of the
+ * facets
+ * and/or
+ * using the technique in section "3.1 Ridge Generation" of
+ * "Extended Convex Hull" by Fukuda et al.
+ */
+static struct isl_basic_set *extend(struct isl_ctx *ctx, struct isl_set *set,
+       struct isl_mat *initial)
+{
+       int i, j, f;
+       int k;
+       struct isl_basic_set *hull = NULL;
+       struct isl_basic_set *facet = NULL;
+       unsigned n_ineq;
+       unsigned total;
+
+       isl_assert(ctx, set->n > 0, goto error);
+
+       n_ineq = 1;
+       for (i = 0; i < set->n; ++i) {
+               n_ineq += set->p[i]->n_eq;
+               n_ineq += set->p[i]->n_ineq;
+       }
+       isl_assert(ctx, 1 + set->dim == initial->n_col, goto error);
+       hull = isl_basic_set_alloc(ctx, 0, set->dim, 0,
+                   0, n_ineq + 2 * set->p[0]->n_div);
+       if (!hull)
+               goto error;
+       k = isl_basic_set_alloc_inequality(ctx, hull);
+       if (k < 0)
+               goto error;
+       isl_seq_cpy(hull->ineq[k], initial->row[0], initial->n_col);
+       for (i = 0; i < hull->n_ineq; ++i) {
+               facet = compute_facet(ctx, set, hull->ineq[i]);
+               if (!facet)
+                       goto error;
+               for (j = 0; j < facet->n_ineq; ++j) {
+                       k = isl_basic_set_alloc_inequality(ctx, hull);
+                       if (k < 0)
+                               goto error;
+                       isl_seq_cpy(hull->ineq[k], hull->ineq[i], 1+hull->dim);
+                       if (!wrap_facet(ctx, set, hull->ineq[k], facet->ineq[j]))
+                               goto error;
+                       for (f = 0; f < k; ++f)
+                               if (isl_seq_eq(hull->ineq[f], hull->ineq[k],
+                                               1+hull->dim))
+                                       break;
+                       if (f < k)
+                               isl_basic_set_free_inequality(ctx, hull, 1);
+               }
+               isl_basic_set_free(ctx, facet);
+       }
+       hull = isl_basic_set_simplify(ctx, hull);
+       hull = isl_basic_set_finalize(ctx, hull);
+       return hull;
+error:
+       isl_basic_set_free(ctx, hull);
+       return NULL;
+}
+
+/* Special case for computing the convex hull of a one dimensional set.
+ * We simply collect the lower and upper bounds of each basic set
+ * and the biggest of those.
+ */
+static struct isl_basic_set *convex_hull_1d(struct isl_ctx *ctx,
+       struct isl_set *set)
+{
+       struct isl_mat *c = NULL;
+       isl_int *lower = NULL;
+       isl_int *upper = NULL;
+       int i, j, k;
+       isl_int a, b;
+       struct isl_basic_set *hull;
+
+       for (i = 0; i < set->n; ++i) {
+               set->p[i] = isl_basic_set_simplify(ctx, set->p[i]);
+               if (!set->p[i])
+                       goto error;
+       }
+       set = isl_set_remove_empty_parts(ctx, set);
+       if (!set)
+               goto error;
+       isl_assert(ctx, set->n > 0, goto error);
+       c = isl_mat_alloc(ctx, 2, 2);
+       if (!c)
+               goto error;
+
+       if (set->p[0]->n_eq > 0) {
+               isl_assert(ctx, set->p[0]->n_eq == 1, goto error);
+               lower = c->row[0];
+               upper = c->row[1];
+               if (isl_int_is_pos(set->p[0]->eq[0][1])) {
+                       isl_seq_cpy(lower, set->p[0]->eq[0], 2);
+                       isl_seq_neg(upper, set->p[0]->eq[0], 2);
+               } else {
+                       isl_seq_neg(lower, set->p[0]->eq[0], 2);
+                       isl_seq_cpy(upper, set->p[0]->eq[0], 2);
+               }
+       } else {
+               for (j = 0; j < set->p[0]->n_ineq; ++j) {
+                       if (isl_int_is_pos(set->p[0]->ineq[j][1])) {
+                               lower = c->row[0];
+                               isl_seq_cpy(lower, set->p[0]->ineq[j], 2);
+                       } else {
+                               upper = c->row[1];
+                               isl_seq_cpy(upper, set->p[0]->ineq[j], 2);
+                       }
+               }
+       }
+
+       isl_int_init(a);
+       isl_int_init(b);
+       for (i = 0; i < set->n; ++i) {
+               struct isl_basic_set *bset = set->p[i];
+               int has_lower = 0;
+               int has_upper = 0;
+
+               for (j = 0; j < bset->n_eq; ++j) {
+                       has_lower = 1;
+                       has_upper = 1;
+                       if (lower) {
+                               isl_int_mul(a, lower[0], bset->eq[j][1]);
+                               isl_int_mul(b, lower[1], bset->eq[j][0]);
+                               if (isl_int_lt(a, b) && isl_int_is_pos(bset->eq[j][1]))
+                                       isl_seq_cpy(lower, bset->eq[j], 2);
+                               if (isl_int_gt(a, b) && isl_int_is_neg(bset->eq[j][1]))
+                                       isl_seq_neg(lower, bset->eq[j], 2);
+                       }
+                       if (upper) {
+                               isl_int_mul(a, upper[0], bset->eq[j][1]);
+                               isl_int_mul(b, upper[1], bset->eq[j][0]);
+                               if (isl_int_lt(a, b) && isl_int_is_pos(bset->eq[j][1]))
+                                       isl_seq_neg(upper, bset->eq[j], 2);
+                               if (isl_int_gt(a, b) && isl_int_is_neg(bset->eq[j][1]))
+                                       isl_seq_cpy(upper, bset->eq[j], 2);
+                       }
+               }
+               for (j = 0; j < bset->n_ineq; ++j) {
+                       if (isl_int_is_pos(bset->ineq[j][1]))
+                               has_lower = 1;
+                       if (isl_int_is_neg(bset->ineq[j][1]))
+                               has_upper = 1;
+                       if (lower && isl_int_is_pos(bset->ineq[j][1])) {
+                               isl_int_mul(a, lower[0], bset->ineq[j][1]);
+                               isl_int_mul(b, lower[1], bset->ineq[j][0]);
+                               if (isl_int_lt(a, b))
+                                       isl_seq_cpy(lower, bset->ineq[j], 2);
+                       }
+                       if (upper && isl_int_is_neg(bset->ineq[j][1])) {
+                               isl_int_mul(a, upper[0], bset->ineq[j][1]);
+                               isl_int_mul(b, upper[1], bset->ineq[j][0]);
+                               if (isl_int_gt(a, b))
+                                       isl_seq_cpy(upper, bset->ineq[j], 2);
+                       }
+               }
+               if (!has_lower)
+                       lower = NULL;
+               if (!has_upper)
+                       upper = NULL;
+       }
+       isl_int_clear(a);
+       isl_int_clear(b);
+
+       hull = isl_basic_set_alloc(ctx, 0, 1, 0, 0, 2);
+       if (!hull)
+               goto error;
+       if (lower) {
+               k = isl_basic_set_alloc_inequality(ctx, hull);
+               isl_seq_cpy(hull->ineq[k], lower, 2);
+       }
+       if (upper) {
+               k = isl_basic_set_alloc_inequality(ctx, hull);
+               isl_seq_cpy(hull->ineq[k], upper, 2);
+       }
+       hull = isl_basic_set_finalize(ctx, hull);
+       isl_set_free(ctx, set);
+       isl_mat_free(ctx, c);
+       return hull;
+error:
+       isl_set_free(ctx, set);
+       isl_mat_free(ctx, c);
+       return NULL;
+}
+
+/* Project out final n dimensions using Fourier-Motzkin */
+static struct isl_set *set_project_out(struct isl_ctx *ctx,
+       struct isl_set *set, unsigned n)
+{
+       int i;
+
+       set = isl_set_cow(ctx, set);
+       if (!set)
+               return NULL;
+       
+       for (i = 0; i < set->n; ++i) {
+               set->p[i] = isl_basic_set_eliminate_vars(ctx, set->p[i],
+                                                           set->dim - n, n);
+               if (!set->p[i])
+                       goto error;
+       }
+       set = isl_set_drop_vars(ctx, set, set->dim - n, n);
+       return set;
+error:
+       isl_set_free(ctx, set);
+       return NULL;
+}
+
+/* If the number of linearly independent bounds we found is smaller
+ * than the dimension, then the convex hull will have a lineality space,
+ * so we may as well project out this lineality space.
+ * We first transform the set such that the first variables correspond
+ * to the directions of the linearly independent bounds and then
+ * project out the remaining variables.
+ */
+static struct isl_basic_set *modulo_lineality(struct isl_ctx *ctx,
+       struct isl_set *set, struct isl_mat *bounds)
+{
+       int i, j;
+       unsigned old_dim, new_dim;
+       struct isl_mat *H = NULL, *U = NULL, *Q = NULL;
+       struct isl_basic_set *hull;
+
+       old_dim = set->dim;
+       new_dim = bounds->n_row;
+       H = isl_mat_sub_alloc(ctx, bounds->row, 0, bounds->n_row, 1, set->dim);
+       H = isl_mat_left_hermite(ctx, H, &U, &Q);
+       if (!H)
+               goto error;
+       U = isl_mat_lin_to_aff(ctx, U);
+       Q = isl_mat_lin_to_aff(ctx, Q);
+       Q->n_row = 1 + new_dim;
+       isl_mat_free(ctx, H);
+       set = isl_set_preimage(ctx, set, U);
+       set = set_project_out(ctx, set, old_dim - new_dim);
+       hull = uset_convex_hull(ctx, set);
+       hull = isl_basic_set_preimage(ctx, hull, Q);
+       isl_mat_free(ctx, bounds);
+       return hull;
+error:
+       isl_mat_free(ctx, bounds);
+       isl_mat_free(ctx, Q);
+       isl_set_free(ctx, set);
+       return NULL;
+}
+
+/* This is the core procedure, where "set" is a "pure" set, i.e.,
+ * without parameters or divs and where the convex hull of set is
+ * known to be full-dimensional.
+ */
+static struct isl_basic_set *uset_convex_hull(struct isl_ctx *ctx,
+       struct isl_set *set)
+{
+       int i;
+       struct isl_basic_set *convex_hull = NULL;
+       struct isl_mat *bounds;
+
+       if (set->dim == 0) {
+               convex_hull = isl_basic_set_universe(ctx, 0, 0);
+               isl_set_free(ctx, set);
+               return convex_hull;
+       }
+
+       set = isl_set_set_rational(ctx, set);
+
+       if (!set)
+               goto error;
+       for (i = 0; i < set->n; ++i) {
+               set->p[i] = isl_basic_set_convex_hull(ctx, set->p[i]);
+               if (!set->p[i])
+                       goto error;
+       }
+       set = isl_set_remove_empty_parts(ctx, set);
+       if (!set)
+               goto error;
+       if (set->n == 1) {
+               convex_hull = isl_basic_set_copy(ctx, set->p[0]);
+               isl_set_free(ctx, set);
+               return convex_hull;
+       }
+       if (set->dim == 1)
+               return convex_hull_1d(ctx, set);
+
+       bounds = independent_bounds(ctx, set);
+       if (!bounds)
+               goto error;
+       if (bounds->n_row < set->dim)
+               return modulo_lineality(ctx, set, bounds);
+       bounds = initial_facet_constraint(ctx, set, bounds);
+       if (!bounds)
+               goto error;
+       convex_hull = extend(ctx, set, bounds);
+       isl_mat_free(ctx, bounds);
+       isl_set_free(ctx, set);
+
+       return convex_hull;
+error:
+       isl_set_free(ctx, set);
+       return NULL;
+}
+
+/* Compute the convex hull of set "set" with affine hull "affine_hull",
+ * We first remove the equalities (transforming the set), compute the
+ * convex hull of the transformed set and then add the equalities back
+ * (after performing the inverse transformation.
+ */
+static struct isl_basic_set *modulo_affine_hull(struct isl_ctx *ctx,
+       struct isl_set *set, struct isl_basic_set *affine_hull)
+{
+       struct isl_mat *T;
+       struct isl_mat *T2;
+       struct isl_basic_set *dummy;
+       struct isl_basic_set *convex_hull;
+
+       dummy = isl_basic_set_remove_equalities(ctx,
+                       isl_basic_set_copy(ctx, affine_hull), &T, &T2);
+       if (!dummy)
+               goto error;
+       isl_basic_set_free(ctx, dummy);
+       set = isl_set_preimage(ctx, set, T);
+       convex_hull = uset_convex_hull(ctx, set);
+       convex_hull = isl_basic_set_preimage(ctx, convex_hull, T2);
+       convex_hull = isl_basic_set_intersect(ctx, convex_hull, affine_hull);
+       return convex_hull;
+error:
+       isl_basic_set_free(ctx, affine_hull);
+       isl_set_free(ctx, set);
+       return NULL;
+}
+
+/* Compute the convex hull of a map.
+ *
+ * The implementation was inspired by "Extended Convex Hull" by Fukuda et al.,
+ * specifically, the wrapping of facets to obtain new facets.
+ */
+struct isl_basic_map *isl_map_convex_hull(struct isl_ctx *ctx,
+                                               struct isl_map *map)
+{
+       struct isl_basic_set *bset;
+       struct isl_basic_set *affine_hull = NULL;
+       struct isl_basic_map *convex_hull = NULL;
+       struct isl_set *set = NULL;
+
+       if (!map)
+               goto error;
+
+       if (map->n == 0) {
+               convex_hull = isl_basic_map_empty(ctx,
+                                           map->nparam, map->n_in, map->n_out);
+               isl_map_free(ctx, map);
+               return convex_hull;
+       }
+
+       set = isl_map_underlying_set(ctx, isl_map_copy(ctx, map));
+       if (!set)
+               goto error;
+
+       affine_hull = isl_set_affine_hull(ctx, isl_set_copy(ctx, set));
+       if (!affine_hull)
+               goto error;
+       if (affine_hull->n_eq != 0)
+               bset = modulo_affine_hull(ctx, set, affine_hull);
+       else {
+               isl_basic_set_free(ctx, affine_hull);
+               bset = uset_convex_hull(ctx, set);
+       }
+
+       convex_hull = isl_basic_map_overlying_set(ctx, bset,
+                       isl_basic_map_copy(ctx, map->p[0]));
+
+       isl_map_free(ctx, map);
+       return convex_hull;
+error:
+       isl_set_free(ctx, set);
+       isl_map_free(ctx, map);
+       return NULL;
+}
+
+struct isl_basic_set *isl_set_convex_hull(struct isl_ctx *ctx,
+                                               struct isl_set *set)
+{
+       return (struct isl_basic_set *)
+               isl_map_convex_hull(ctx, (struct isl_map *)set);
+}
index d9da0d5..acecd22 100644 (file)
--- a/isl_lp.c
+++ b/isl_lp.c
@@ -3,7 +3,8 @@
 #include "isl_lp_piplib.h"
 
 enum isl_lp_result isl_solve_lp(struct isl_basic_map *bmap, int maximize,
-                                     isl_int *f, isl_int denom, isl_int *opt)
+                                     isl_int *f, isl_int denom, isl_int *opt,
+                                     isl_int *opt_denom)
 {
-       return isl_pip_solve_lp(bmap, maximize, f, denom, opt);
+       return isl_pip_solve_lp(bmap, maximize, f, denom, opt, opt_denom);
 }
index 9258272..c55fad0 100644 (file)
@@ -1,7 +1,8 @@
 #include "isl_lp_piplib.h"
 
 enum isl_lp_result isl_pip_solve_lp(struct isl_basic_map *bmap, int maximize,
-                                     isl_int *f, isl_int denom, isl_int *opt)
+                                     isl_int *f, isl_int denom, isl_int *opt,
+                                     isl_int *opt_denom)
 {
        return isl_lp_error;
 }
index 0072295..8289e79 100644 (file)
@@ -4,7 +4,8 @@
 #include "isl_map_piplib.h"
 
 enum isl_lp_result isl_pip_solve_lp(struct isl_basic_map *bmap, int maximize,
-                                     isl_int *f, isl_int denom, isl_int *opt)
+                                     isl_int *f, isl_int denom, isl_int *opt,
+                                     isl_int *opt_denom)
 {
        enum isl_lp_result res = isl_lp_ok;
        PipMatrix       *domain = NULL;
@@ -35,7 +36,12 @@ enum isl_lp_result isl_pip_solve_lp(struct isl_basic_map *bmap, int maximize,
        else if (entier_zero_p(sol->list->vector->the_deno[0]))
                res = isl_lp_unbounded;
        else {
-               if (maximize)
+               if (opt_denom) {
+                       isl_seq_cpy_from_pip(opt,
+                                &sol->list->vector->the_vector[0], 1);
+                       isl_seq_cpy_from_pip(opt_denom,
+                                &sol->list->vector->the_deno[0], 1);
+               } else if (maximize)
                        mpz_fdiv_q(*opt, sol->list->vector->the_vector[0],
                                         sol->list->vector->the_deno[0]);
                else
index 61f2277..67d1320 100644 (file)
--- a/isl_map.c
+++ b/isl_map.c
@@ -131,6 +131,7 @@ struct isl_basic_map *isl_basic_map_dup(struct isl_ctx *ctx,
                        bmap->n_div, bmap->n_eq, bmap->n_ineq);
        if (!dup)
                return NULL;
+       dup->flags = bmap->flags;
        dup_constraints(ctx, dup, bmap);
        dup->sample = isl_vec_copy(ctx, bmap->sample);
        return dup;
@@ -260,6 +261,13 @@ int isl_basic_map_drop_equality(struct isl_ctx *ctx,
        return 0;
 }
 
+int isl_basic_set_drop_equality(struct isl_ctx *ctx,
+               struct isl_basic_set *bset, unsigned pos)
+{
+       return isl_basic_map_drop_equality(ctx,
+                       (struct isl_basic_map *)bset, pos);
+}
+
 void isl_basic_map_inequality_to_equality(struct isl_ctx *ctx,
                struct isl_basic_map *bmap, unsigned pos)
 {
@@ -280,6 +288,7 @@ int isl_basic_map_alloc_inequality(struct isl_ctx *ctx,
        isl_assert(ctx, (bmap->ineq - bmap->eq) + bmap->n_ineq < bmap->c_size,
                        return -1);
        F_CLR(bmap, ISL_BASIC_MAP_NO_IMPLICIT);
+       F_CLR(bmap, ISL_BASIC_MAP_NO_REDUNDANT);
        return bmap->n_ineq++;
 }
 
@@ -297,6 +306,13 @@ int isl_basic_map_free_inequality(struct isl_ctx *ctx,
        return 0;
 }
 
+int isl_basic_set_free_inequality(struct isl_ctx *ctx,
+               struct isl_basic_set *bset, unsigned n)
+{
+       return isl_basic_map_free_inequality(ctx,
+                                           (struct isl_basic_map *)bset, n);
+}
+
 int isl_basic_map_drop_inequality(struct isl_ctx *ctx,
                struct isl_basic_map *bmap, unsigned pos)
 {
@@ -312,6 +328,13 @@ int isl_basic_map_drop_inequality(struct isl_ctx *ctx,
        return 0;
 }
 
+int isl_basic_set_drop_inequality(struct isl_ctx *ctx,
+               struct isl_basic_set *bset, unsigned pos)
+{
+       return isl_basic_map_drop_inequality(ctx,
+                       (struct isl_basic_map *)bset, pos);
+}
+
 int isl_basic_map_alloc_div(struct isl_ctx *ctx,
                struct isl_basic_map *bmap)
 {
@@ -420,6 +443,7 @@ struct isl_basic_map *isl_basic_map_extend(struct isl_ctx *ctx,
                unsigned n_eq, unsigned n_ineq)
 {
        struct isl_basic_map *ext;
+       unsigned flags;
        int dims_ok;
 
        base = isl_basic_map_cow(ctx, base);
@@ -449,7 +473,12 @@ struct isl_basic_map *isl_basic_map_extend(struct isl_ctx *ctx,
        if (!ext)
                goto error;
 
+       flags = base->flags;
        ext = add_constraints(ctx, ext, base, 0, 0);
+       if (ext) {
+               ext->flags = flags;
+               F_CLR(ext, ISL_BASIC_SET_FINAL);
+       }
 
        return ext;
 
@@ -624,6 +653,35 @@ error:
        return NULL;
 }
 
+struct isl_set *isl_set_drop_vars(struct isl_ctx *ctx,
+               struct isl_set *set, unsigned first, unsigned n)
+{
+       int i;
+
+       if (!set)
+               goto error;
+
+       isl_assert(ctx, first + n <= set->dim, goto error);
+
+       if (n == 0)
+               return set;
+       set = isl_set_cow(ctx, set);
+       if (!set)
+               goto error;
+
+       for (i = 0; i < set->n; ++i) {
+               set->p[i] = isl_basic_set_drop_vars(ctx, set->p[i], first, n);
+               if (!set->p[i])
+                       goto error;
+       }
+       set->dim -= n;
+
+       return set;
+error:
+       isl_set_free(ctx, set);
+       return NULL;
+}
+
 /*
  * We don't cow, as the div is assumed to be redundant.
  */
@@ -1054,6 +1112,8 @@ static struct isl_basic_map *normalize_constraints(
                        isl_basic_map_drop_equality(ctx, bmap, i);
                        continue;
                }
+               if (F_ISSET(bmap, ISL_BASIC_MAP_RATIONAL))
+                       isl_int_gcd(gcd, gcd, bmap->eq[i][0]);
                if (isl_int_is_one(gcd))
                        continue;
                if (!isl_int_is_divisible_by(bmap->eq[i][0], gcd)) {
@@ -1073,6 +1133,8 @@ static struct isl_basic_map *normalize_constraints(
                        isl_basic_map_drop_inequality(ctx, bmap, i);
                        continue;
                }
+               if (F_ISSET(bmap, ISL_BASIC_MAP_RATIONAL))
+                       isl_int_gcd(gcd, gcd, bmap->ineq[i][0]);
                if (isl_int_is_one(gcd))
                        continue;
                isl_int_fdiv_q(bmap->ineq[i][0], bmap->ineq[i][0], gcd);
@@ -1363,9 +1425,9 @@ void isl_basic_map_dump(struct isl_ctx *ctx, struct isl_basic_map *bmap,
        }
 
        fprintf(out, "%*s", indent, "");
-       fprintf(out, "ref: %d, nparam: %d, in: %d, out: %d, extra: %d\n",
+       fprintf(out, "ref: %d, nparam: %d, in: %d, out: %d, extra: %d, flags: %x\n",
                bmap->ref,
-               bmap->nparam, bmap->n_in, bmap->n_out, bmap->extra);
+               bmap->nparam, bmap->n_in, bmap->n_out, bmap->extra, bmap->flags);
        dump(bmap, out, indent);
 }
 
@@ -1947,6 +2009,7 @@ static struct isl_basic_set *isl_basic_map_underlying_set(
        bmap->n_out += bmap->nparam + bmap->n_in + bmap->n_div;
        bmap->nparam = 0;
        bmap->n_in = 0;
+       bmap->extra -= bmap->n_div;
        bmap->n_div = 0;
        bmap = isl_basic_map_finalize(ctx, bmap);
        return (struct isl_basic_set *)bmap;
@@ -2144,6 +2207,22 @@ struct isl_basic_map *isl_basic_map_empty(struct isl_ctx *ctx,
        return bmap;
 }
 
+struct isl_basic_map *isl_basic_map_universe(struct isl_ctx *ctx,
+               unsigned nparam, unsigned in, unsigned out)
+{
+       struct isl_basic_map *bmap;
+       bmap = isl_basic_map_alloc(ctx, nparam, in, out, 0, 0, 0);
+       return bmap;
+}
+
+struct isl_basic_set *isl_basic_set_universe(struct isl_ctx *ctx,
+               unsigned nparam, unsigned dim)
+{
+       struct isl_basic_set *bset;
+       bset = isl_basic_set_alloc(ctx, nparam, dim, 0, 0, 0);
+       return bset;
+}
+
 struct isl_map *isl_map_empty(struct isl_ctx *ctx,
                unsigned nparam, unsigned in, unsigned out)
 {
@@ -2819,6 +2898,27 @@ int isl_basic_map_is_subset(struct isl_ctx *ctx,
        return is_subset;
 }
 
+int isl_basic_map_is_equal(struct isl_ctx *ctx,
+               struct isl_basic_map *bmap1, struct isl_basic_map *bmap2)
+{
+       int is_subset;
+
+       if (!bmap1 || !bmap2)
+               return -1;
+       is_subset = isl_basic_map_is_subset(ctx, bmap1, bmap2);
+       if (is_subset != 1)
+               return is_subset;
+       is_subset = isl_basic_map_is_subset(ctx, bmap2, bmap1);
+       return is_subset;
+}
+
+int isl_basic_set_is_equal(struct isl_ctx *ctx,
+               struct isl_basic_set *bset1, struct isl_basic_set *bset2)
+{
+       return isl_basic_map_is_equal(ctx,
+               (struct isl_basic_map *)bset1, (struct isl_basic_map *)bset2);
+}
+
 int isl_map_is_empty(struct isl_ctx *ctx, struct isl_map *map)
 {
        int i;
@@ -2933,6 +3033,14 @@ static int basic_map_contains(struct isl_ctx *ctx, struct isl_basic_map *bmap,
        return 1;
 }
 
+int isl_basic_map_is_universe(struct isl_ctx *ctx,
+               struct isl_basic_map *bmap)
+{
+       if (!bmap)
+               return -1;
+       return bmap->n_eq == 0 && bmap->n_ineq == 0;
+}
+
 int isl_basic_map_is_empty(struct isl_ctx *ctx,
                struct isl_basic_map *bmap)
 {
index 22411d5..f3cef4e 100644 (file)
@@ -5,6 +5,8 @@ int isl_basic_map_alloc_equality(struct isl_ctx *ctx,
                struct isl_basic_map *bmap);
 int isl_basic_set_alloc_equality(struct isl_ctx *ctx,
                struct isl_basic_set *bset);
+int isl_basic_set_free_inequality(struct isl_ctx *ctx,
+               struct isl_basic_set *bset, unsigned n);
 int isl_basic_map_free_equality(struct isl_ctx *ctx,
                struct isl_basic_map *bmap, unsigned n);
 int isl_basic_set_alloc_inequality(struct isl_ctx *ctx,
@@ -19,6 +21,10 @@ int isl_basic_map_free_div(struct isl_ctx *ctx,
                struct isl_basic_map *bmap, unsigned n);
 void isl_basic_map_inequality_to_equality(struct isl_ctx *ctx,
                struct isl_basic_map *bmap, unsigned pos);
+int isl_basic_set_drop_equality(struct isl_ctx *ctx,
+               struct isl_basic_set *bset, unsigned pos);
+int isl_basic_set_drop_inequality(struct isl_ctx *ctx,
+               struct isl_basic_set *bset, unsigned pos);
 
 int isl_inequality_negate(struct isl_ctx *ctx,
                struct isl_basic_map *bmap, unsigned pos);
@@ -44,6 +50,8 @@ struct isl_basic_map *isl_basic_map_gauss(struct isl_ctx *ctx,
        struct isl_basic_map *bmap, int *progress);
 struct isl_basic_set *isl_basic_set_gauss(struct isl_ctx *ctx,
        struct isl_basic_set *bset, int *progress);
+struct isl_basic_map *isl_basic_map_implicit_equalities(struct isl_ctx *ctx,
+                                               struct isl_basic_map *bmap);
 struct isl_set *isl_map_underlying_set(struct isl_ctx *ctx, struct isl_map *map);
 struct isl_basic_map *isl_basic_map_overlying_set(
        struct isl_ctx *ctx, struct isl_basic_set *bset,
@@ -54,5 +62,8 @@ struct isl_map *isl_map_remove_empty_parts(struct isl_ctx *ctx,
 struct isl_set *isl_set_remove_empty_parts(struct isl_ctx *ctx,
        struct isl_set *set);
 
+struct isl_set *isl_set_drop_vars(struct isl_ctx *ctx,
+               struct isl_set *set, unsigned first, unsigned n);
+
 struct isl_basic_set *isl_basic_set_eliminate_vars(struct isl_ctx *ctx,
        struct isl_basic_set *bset, unsigned pos, unsigned n);
index fb7c915..9b4558c 100644 (file)
--- a/isl_mat.c
+++ b/isl_mat.c
@@ -516,6 +516,108 @@ error:
        return NULL;
 }
 
+void isl_mat_col_scale(struct isl_mat *mat, unsigned col, isl_int m)
+{
+       int i;
+
+       for (i = 0; i < mat->n_row; ++i)
+               isl_int_mul(mat->row[i][col], mat->row[i][col], m);
+}
+
+isl_mat_col_combine(struct isl_mat *mat, unsigned dst,
+       isl_int m1, unsigned src1, isl_int m2, unsigned src2)
+{
+       int i;
+       isl_int tmp;
+
+       isl_int_init(tmp);
+       for (i = 0; i < mat->n_row; ++i) {
+               isl_int_mul(tmp, m1, mat->row[i][src1]);
+               isl_int_addmul(tmp, m2, mat->row[i][src2]);
+               isl_int_set(mat->row[i][dst], tmp);
+       }
+       isl_int_clear(tmp);
+}
+
+struct isl_mat *isl_mat_right_inverse(struct isl_ctx *ctx,
+       struct isl_mat *mat)
+{
+       struct isl_mat *inv;
+       int row;
+       isl_int a, b;
+
+       mat = isl_mat_cow(ctx, mat);
+       if (!mat)
+               return NULL;
+
+       inv = isl_mat_identity(ctx, mat->n_col);
+       inv = isl_mat_cow(ctx, inv);
+       if (!inv)
+               goto error;
+
+       isl_int_init(a);
+       isl_int_init(b);
+       for (row = 0; row < mat->n_row; ++row) {
+               int pivot, first, i, off;
+               pivot = isl_seq_abs_min_non_zero(mat->row[row]+row, mat->n_col-row);
+               if (pivot < 0) {
+                       isl_int_clear(a);
+                       isl_int_clear(b);
+                       goto error;
+               }
+               pivot += row;
+               if (pivot != row)
+                       exchange(ctx, mat, &inv, NULL, row, pivot, row);
+               if (isl_int_is_neg(mat->row[row][row]))
+                       oppose(ctx, mat, &inv, NULL, row, row);
+               first = row+1;
+               while ((off = isl_seq_first_non_zero(mat->row[row]+first,
+                                                   mat->n_col-first)) != -1) {
+                       first += off;
+                       isl_int_fdiv_q(a, mat->row[row][first],
+                                                   mat->row[row][row]);
+                       subtract(ctx, mat, &inv, NULL, row, row, first, a);
+                       if (!isl_int_is_zero(mat->row[row][first]))
+                               exchange(ctx, mat, &inv, NULL, row, row, first);
+                       else
+                               ++first;
+               }
+               for (i = 0; i < row; ++i) {
+                       if (isl_int_is_zero(mat->row[row][i]))
+                               continue;
+                       isl_int_gcd(a, mat->row[row][row], mat->row[row][i]);
+                       isl_int_divexact(b, mat->row[row][i], a);
+                       isl_int_divexact(a, mat->row[row][row], a);
+                       isl_int_neg(a, a);
+                       isl_mat_col_combine(mat, i, a, i, b, row);
+                       isl_mat_col_combine(inv, i, a, i, b, row);
+               }
+       }
+       isl_int_clear(b);
+
+       isl_int_set(a, mat->row[0][0]);
+       for (row = 1; row < mat->n_row; ++row)
+               isl_int_lcm(a, a, mat->row[row][row]);
+       if (isl_int_is_zero(a)){
+               isl_int_clear(a);
+               goto error;
+       }
+       for (row = 0; row < mat->n_row; ++row) {
+               isl_int_divexact(mat->row[row][row], a, mat->row[row][row]);
+               if (isl_int_is_one(mat->row[row][row]))
+                       continue;
+               isl_mat_col_scale(inv, row, mat->row[row][row]);
+       }
+       isl_int_clear(a);
+
+       isl_mat_free(ctx, mat);
+
+       return inv;
+error:
+       isl_mat_free(ctx, mat);
+       return NULL;
+}
+
 struct isl_mat *isl_mat_swap_rows(struct isl_ctx *ctx,
        struct isl_mat *mat, unsigned i, unsigned j)
 {
@@ -584,39 +686,80 @@ struct isl_basic_set *isl_basic_set_preimage(struct isl_ctx *ctx,
        isl_assert(ctx, bset->n_div == 0, goto error);
        isl_assert(ctx, 1+bset->dim == mat->n_row, goto error);
 
+       if (mat->n_col > mat->n_row)
+               bset = isl_basic_set_extend(ctx, bset, 0, mat->n_col-1, 0,
+                                               0, 0);
+       else {
+               bset->dim -= mat->n_row - mat->n_col;
+               bset->extra += mat->n_row - mat->n_col;
+       }
+
        t = isl_mat_sub_alloc(ctx, bset->eq, 0, bset->n_eq, 0, mat->n_row);
        t = isl_mat_product(ctx, t, isl_mat_copy(ctx, mat));
        if (!t)
                goto error;
-       for (i = 0; i < bset->n_eq; ++i)
+       for (i = 0; i < bset->n_eq; ++i) {
                isl_seq_swp_or_cpy(bset->eq[i], t->row[i], t->n_col);
+               isl_seq_clr(bset->eq[i]+t->n_col, bset->extra);
+       }
        isl_mat_free(ctx, t);
 
        t = isl_mat_sub_alloc(ctx, bset->ineq, 0, bset->n_ineq, 0, mat->n_row);
-       t = isl_mat_product(ctx, t, isl_mat_copy(ctx, mat));
+       t = isl_mat_product(ctx, t, mat);
        if (!t)
-               goto error;
-       for (i = 0; i < bset->n_ineq; ++i)
+               goto error2;
+       for (i = 0; i < bset->n_ineq; ++i) {
                isl_seq_swp_or_cpy(bset->ineq[i], t->row[i], t->n_col);
+               isl_seq_clr(bset->ineq[i]+t->n_col, bset->extra);
+       }
        isl_mat_free(ctx, t);
 
-       bset->dim -= mat->n_row - mat->n_col;
        bset = isl_basic_set_simplify(ctx, bset);
        bset = isl_basic_set_finalize(ctx, bset);
 
-       isl_mat_free(ctx, mat);
        return bset;
 error:
        isl_mat_free(ctx, mat);
+error2:
        isl_basic_set_free(ctx, bset);
        return NULL;
 }
 
+struct isl_set *isl_set_preimage(struct isl_ctx *ctx,
+       struct isl_set *set, struct isl_mat *mat)
+{
+       int i;
+
+       set = isl_set_cow(ctx, set);
+       if (!set)
+               return NULL;
+
+       for (i = 0; i < set->n; ++i) {
+               set->p[i] = isl_basic_set_preimage(ctx, set->p[i],
+                                                   isl_mat_copy(ctx, mat));
+               if (!set->p[i])
+                       goto error;
+       }
+       set->dim += mat->n_col;
+       set->dim -= mat->n_row;
+       isl_mat_free(ctx, mat);
+       return set;
+error:
+       isl_set_free(ctx, set);
+       isl_mat_free(ctx, mat);
+       return NULL;
+}
+
 void isl_mat_dump(struct isl_ctx *ctx, struct isl_mat *mat,
                                FILE *out, int indent)
 {
        int i, j;
 
+       if (!mat) {
+               fprintf(out, "null mat\n");
+               return;
+       }
+
        if (mat->n_row == 0)
                fprintf(out, "%*s[]\n", indent, "");
 
index 12346fa..dc17fd2 100644 (file)
--- a/isl_mat.h
+++ b/isl_mat.h
@@ -55,6 +55,8 @@ struct isl_mat *isl_mat_inverse_product(struct isl_ctx *ctx,
        struct isl_mat *left, struct isl_mat *right);
 struct isl_mat *isl_mat_product(struct isl_ctx *ctx,
        struct isl_mat *left, struct isl_mat *right);
+struct isl_mat *isl_mat_right_inverse(struct isl_ctx *ctx,
+       struct isl_mat *mat);
 
 struct isl_mat *isl_mat_drop_col(struct isl_ctx *ctx, struct isl_mat *mat,
                                unsigned col);
@@ -63,6 +65,8 @@ struct isl_mat *isl_mat_drop_rows(struct isl_ctx *ctx, struct isl_mat *mat,
 
 struct isl_basic_set *isl_basic_set_preimage(struct isl_ctx *ctx,
        struct isl_basic_set *bset, struct isl_mat *mat);
+struct isl_set *isl_set_preimage(struct isl_ctx *ctx,
+       struct isl_set *set, struct isl_mat *mat);
 
 void isl_mat_dump(struct isl_ctx *ctx, struct isl_mat *mat,
                                FILE *out, int indent);
diff --git a/isl_test.c b/isl_test.c
new file mode 100644 (file)
index 0000000..c5fdd92
--- /dev/null
@@ -0,0 +1,61 @@
+#include <assert.h>
+#include <stdio.h>
+#include <limits.h>
+#include <isl_ctx.h>
+#include <isl_set.h>
+
+static char *srcdir;
+
+void test_convex_hull_case(struct isl_ctx *ctx, const char *name)
+{
+       char filename[PATH_MAX];
+       FILE *input;
+       int n;
+       struct isl_basic_set *bset1, *bset2;
+       struct isl_set *set;
+
+       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, ISL_FORMAT_POLYLIB);
+       bset2 = isl_basic_set_read_from_file(ctx, input, ISL_FORMAT_POLYLIB);
+
+       set = isl_basic_set_union(ctx, bset1, bset2);
+       bset1 = isl_set_convex_hull(ctx, set);
+
+       bset2 = isl_basic_set_read_from_file(ctx, input, ISL_FORMAT_POLYLIB);
+
+       assert(isl_basic_set_is_equal(ctx, bset1, bset2) == 1);
+
+       isl_basic_set_free(ctx, bset1);
+       isl_basic_set_free(ctx, bset2);
+
+       fclose(input);
+}
+
+void test_convex_hull(struct isl_ctx *ctx)
+{
+       test_convex_hull_case(ctx, "convex0");
+       test_convex_hull_case(ctx, "convex1");
+       test_convex_hull_case(ctx, "convex2");
+       test_convex_hull_case(ctx, "convex3");
+       test_convex_hull_case(ctx, "convex4");
+       test_convex_hull_case(ctx, "convex5");
+       test_convex_hull_case(ctx, "convex6");
+       test_convex_hull_case(ctx, "convex7");
+}
+
+int main()
+{
+       struct isl_ctx *ctx;
+
+       srcdir = getenv("srcdir");
+
+       ctx = isl_ctx_alloc();
+       test_convex_hull(ctx);
+       isl_ctx_free(ctx);
+       return 0;
+}
diff --git a/test_inputs/convex0.polylib b/test_inputs/convex0.polylib
new file mode 100644 (file)
index 0000000..cbc4d3b
--- /dev/null
@@ -0,0 +1,11 @@
+2 3
+1 1 0
+1 -1 1
+
+2 3
+1 1 -1
+1 -1 2
+
+2 3
+1 1 0
+1 -1 2
diff --git a/test_inputs/convex1.polylib b/test_inputs/convex1.polylib
new file mode 100644 (file)
index 0000000..b563d8d
--- /dev/null
@@ -0,0 +1,17 @@
+# {j,N | 0<=j<=N-1; 2<=N}
+4 4
+1   1  0   0
+1  -1  1  -1
+1   0  1  -2
+1   0  0   1
+# {j, N | 1<=j<=N; 1<=N}
+4 4
+1  1  0  -1
+1 -1  1   0
+1  0  1  -1
+1  0  0   1
+# {j,N | 0<=j<=N; 2<=j+N}
+3 4
+   1    1    1   -2
+   1    1    0    0
+   1   -1    1    0
diff --git a/test_inputs/convex2.polylib b/test_inputs/convex2.polylib
new file mode 100644 (file)
index 0000000..0bfd737
--- /dev/null
@@ -0,0 +1,24 @@
+# {i,j,N | 1<=i<=N; 0<=j<=N-1; 2<=N}
+6 5
+1  1  0  0 -1
+1 -1  0  1  0
+1  0  1  0  0
+1  0 -1  1 -1 
+1  0  0  1 -2
+1  0  0  0  1
+# {i,j,N | 1<=i<=N; 1<=j<=N; 2<=N}
+6 5
+1  1  0  0 -1
+1 -1  0  1  0
+1  0  1  0 -1
+1  0 -1  1  0
+1  0  0  1 -2
+1  0  0  0  1
+# {i,j,N | 1<=i<=N; 0<=j<=N; 2<=N}
+6 5
+   1    0    0    1   -2
+   1   -1    0    1    0
+   1    0   -1    1    0
+   1    1    0    0   -1
+   1    0    1    0    0
+   1    0    0    0    1
diff --git a/test_inputs/convex3.polylib b/test_inputs/convex3.polylib
new file mode 100644 (file)
index 0000000..ea612c6
--- /dev/null
@@ -0,0 +1,10 @@
+1 4
+1 1 1 -6
+
+3 4
+1 1 1 -3
+1 1 0 -5
+1 -1 0 10
+
+1 4
+1 1 1 -3
diff --git a/test_inputs/convex4.polylib b/test_inputs/convex4.polylib
new file mode 100644 (file)
index 0000000..0c08653
--- /dev/null
@@ -0,0 +1,9 @@
+1 4
+1 1 1 -6
+
+2 4
+0 1 0 -1
+0 0 1 -4
+
+1 4
+1 1 1 -5
diff --git a/test_inputs/convex5.polylib b/test_inputs/convex5.polylib
new file mode 100644 (file)
index 0000000..3aae7c2
--- /dev/null
@@ -0,0 +1,12 @@
+2 4
+0 1 0 -2
+0 0 1 -6
+
+2 4
+0 1 0 -1
+0 0 1 -4
+
+3 4
+0 -2 1 -2
+1  1 0 -1
+1 -1 0  2
diff --git a/test_inputs/convex6.polylib b/test_inputs/convex6.polylib
new file mode 100644 (file)
index 0000000..1bdb4e1
--- /dev/null
@@ -0,0 +1,17 @@
+3 4
+1   1    1   -2
+1  -1    1    2
+1   0   -1    2
+
+3 4
+1   0    1   -1
+1   1   -1    1
+1  -1   -1    5
+
+6 4
+1  -1    0    4
+1   1    0    0
+1   1    2   -2
+1  -1    2    2
+1   1   -2    4
+1  -1   -2    8
diff --git a/test_inputs/convex7.polylib b/test_inputs/convex7.polylib
new file mode 100644 (file)
index 0000000..70eb483
--- /dev/null
@@ -0,0 +1,9 @@
+1 4
+0 0 1 0
+
+2 4
+1 1 -1 1
+1 -1 -1 1
+
+1 4
+1 0 -1 1