reimplement isl_basic_map_is_empty in terms of isl_basic_set_sample

diff --git a/Makefile.am b/Makefile.am
index 692b5c2..6d8dd3e 100644 (file)
--- a/Makefile.am
+++ b/Makefile.am
@@ -16,11 +16,13 @@ if HAVE_PIPLIB
 ISL_PIPLIB = \
        isl_lp_piplib.c \
        isl_map_piplib.c \
+       isl_sample_piplib.c \
        isl_piplib.c
 else
 ISL_PIPLIB = \
        isl_lp_no_piplib.c \
-       isl_map_no_piplib.c
+       isl_map_no_piplib.c \
+       isl_sample_no_piplib.c
 endif
 if BUNDLED_PIPLIB
 PIPLIB_LA = $(top_builddir)/piplib/libpiplibMP.la
@@ -41,15 +43,21 @@ libisl_la_SOURCES = \
        isl_map.h \
        isl_map_affine_hull.c \
        isl_map_private.h \
+       isl_sample.h \
+       isl_sample.c \
        isl_set.h \
        isl_seq.c \
-       isl_seq.h
+       isl_seq.h \
+       isl_vec.c \
+       isl_vec.h
 EXTRA_libisl_la_SOURCES = \
        isl_lp_piplib.c \
        isl_lp_no_piplib.c \
        isl_map_piplib.c \
        isl_map_no_piplib.c \
        isl_map_polylib.c \
+       isl_sample_no_piplib.c \
+       isl_sample_piplib.c \
        isl_piplib.c
 libisl_la_LIBADD = $(PIPLIB_LA) @PIPLIB_LIBS@ @POLYLIB_LIBS@ -lgmp
 libisl_la_LDFLAGS = -release @VERSION@ @PIPLIB_LDFLAGS@ @POLYLIB_LDFLAGS@ \

diff --git a/include/isl_ctx.h.in b/include/isl_ctx.h.in
index 4b58276..c412bd2 100644 (file)
--- a/include/isl_ctx.h.in
+++ b/include/isl_ctx.h.in
@@ -37,6 +37,7 @@ extern "C" {
  * (in case of pointer return type).
  * The only exception is the isl_ctx argument, which shoud never be NULL.
  */
+struct isl_vec;
 struct isl_ctx {
        isl_int         one;
 #ifdef ISL_POLYLIB

diff --git a/include/isl_piplib.h b/include/isl_piplib.h
index e58d21e..c07f437 100644 (file)
--- a/include/isl_piplib.h
+++ b/include/isl_piplib.h
@@ -11,6 +11,7 @@
 #include <piplib/piplibMP.h>
 
 void isl_seq_cpy_to_pip(Entier *dst, isl_int *src, unsigned len);
+void isl_seq_cpy_from_pip(isl_int *dst, Entier *src, unsigned len);
 
 PipMatrix *isl_basic_map_to_pip(struct isl_basic_map *bmap, unsigned pip_param,
                         unsigned extra_front, unsigned extra_back);

diff --git a/isl_ctx.c b/isl_ctx.c
index 686a9be..fb491a0 100644 (file)
--- a/isl_ctx.c
+++ b/isl_ctx.c
@@ -1,15 +1,16 @@
 #include "isl_ctx.h"
+#include "isl_vec.h"
 #ifdef ISL_POLYLIB
 #include <polylib/polylibgmp.h>
 #endif
 
 struct isl_ctx *isl_ctx_alloc()
 {
-       struct isl_ctx *ctx;
+       struct isl_ctx *ctx = NULL;
 
        ctx = isl_alloc_type(NULL, struct isl_ctx);
        if (!ctx)
-               return NULL;
+               goto error;
 
        isl_int_init(ctx->one);
        isl_int_set_si(ctx->one, 1);
@@ -19,6 +20,9 @@ struct isl_ctx *isl_ctx_alloc()
 #endif
 
        return ctx;
+error:
+       free(ctx);
+       return NULL;
 }
 
 void isl_ctx_free(struct isl_ctx *ctx)

diff --git a/isl_map.c b/isl_map.c
index 0a8fe3b..13eb705 100644 (file)
--- a/isl_map.c
+++ b/isl_map.c
@@ -7,6 +7,8 @@
 #include "isl_map.h"
 #include "isl_map_private.h"
 #include "isl_map_piplib.h"
+#include "isl_sample.h"
+#include "isl_vec.h"
 
 static struct isl_basic_map *basic_map_init(struct isl_ctx *ctx,
                struct isl_basic_map *bmap,
@@ -1643,6 +1645,26 @@ error:
        return NULL;
 }
 
+static struct isl_basic_set *isl_basic_map_underlying_set(
+               struct isl_ctx *ctx, struct isl_basic_map *bmap)
+{
+       if (!bmap)
+               goto error;
+       if (bmap->nparam == 0 && bmap->n_in == 0 && bmap->n_div == 0)
+               return (struct isl_basic_set *)bmap;
+       bmap = isl_basic_map_cow(ctx, bmap);
+       if (!bmap)
+               goto error;
+       bmap->n_out += bmap->nparam + bmap->n_in + bmap->n_div;
+       bmap->nparam = 0;
+       bmap->n_in = 0;
+       bmap->n_div = 0;
+       bmap = isl_basic_map_finalize(ctx, bmap);
+       return (struct isl_basic_set *)bmap;
+error:
+       return NULL;
+}
+
 struct isl_basic_set *isl_basic_map_domain(struct isl_ctx *ctx,
                struct isl_basic_map *bmap)
 {
@@ -2496,7 +2518,7 @@ int isl_basic_map_is_empty(struct isl_ctx *ctx,
                struct isl_basic_map *bmap)
 {
        struct isl_basic_set *bset = NULL;
-       struct isl_set *min = NULL;
+       struct isl_vec *sample = NULL;
        int empty;
 
        if (!bmap)
@@ -2505,15 +2527,16 @@ int isl_basic_map_is_empty(struct isl_ctx *ctx,
        if (F_ISSET(bmap, ISL_BASIC_MAP_EMPTY))
                return 1;
 
-       bset = isl_basic_set_from_basic_map(ctx,
+       bset = isl_basic_map_underlying_set(ctx,
                        isl_basic_map_copy(ctx, bmap));
        if (!bset)
                return -1;
-       min = isl_basic_set_lexmin(ctx, bset);
-       if (!min)
+       sample = isl_basic_set_sample(ctx, bset);
+       if (!sample)
                return -1;
-       empty = min->n == 0;
-       isl_set_free(ctx, min);
+       empty = sample->size == 0;
+       isl_vec_free(ctx, sample);
+
        return empty;
 }
 

diff --git a/isl_piplib.c b/isl_piplib.c
index d389d73..7d625ef 100644 (file)
--- a/isl_piplib.c
+++ b/isl_piplib.c
@@ -7,3 +7,11 @@ void isl_seq_cpy_to_pip(Entier *dst, isl_int *src, unsigned len)
        for (i = 0; i < len; ++i)
                entier_assign(dst[i], src[i]);
 }
+
+void isl_seq_cpy_from_pip(isl_int *dst, Entier *src, unsigned len)
+{
+       int i;
+
+       for (i = 0; i < len; ++i)
+               entier_assign(dst[i], src[i]);
+}

diff --git a/isl_sample.c b/isl_sample.c
new file mode 100644 (file)
index 0000000..c218593
--- /dev/null
+++ b/isl_sample.c
@@ -0,0 +1,13 @@
+#include "isl_sample.h"
+#include "isl_sample_piplib.h"
+#include "isl_vec.h"
+
+struct isl_vec *isl_basic_set_sample(struct isl_ctx *ctx,
+       struct isl_basic_set *bset)
+{
+       if (F_ISSET(bset, ISL_BASIC_SET_EMPTY)) {
+               isl_basic_set_free(ctx, bset);
+               return isl_vec_alloc(ctx, 0);
+       }
+       return isl_pip_basic_set_sample(ctx, bset);
+}

diff --git a/isl_sample.h b/isl_sample.h
new file mode 100644 (file)
index 0000000..26c8fe3
--- /dev/null
+++ b/isl_sample.h
@@ -0,0 +1,17 @@
+#ifndef ISL_SAMPLE_H
+#define ISL_SAMPLE
+
+#include <isl_set.h>
+
+#if defined(__cplusplus)
+extern "C" {
+#endif
+
+struct isl_vec *isl_basic_set_sample(struct isl_ctx *ctx,
+       struct isl_basic_set *bset);
+
+#if defined(__cplusplus)
+}
+#endif
+
+#endif

diff --git a/isl_sample_no_piplib.c b/isl_sample_no_piplib.c
new file mode 100644 (file)
index 0000000..2f4c1a8
--- /dev/null
+++ b/isl_sample_no_piplib.c
@@ -0,0 +1,8 @@
+#include "isl_sample_piplib.h"
+
+struct isl_vec *isl_pip_basic_set_sample(struct isl_ctx *ctx,
+       struct isl_basic_set *bset)
+{
+       isl_basic_set_free(ctx, bset);
+       return NULL;
+}

diff --git a/isl_sample_piplib.c b/isl_sample_piplib.c
new file mode 100644 (file)
index 0000000..19aa601
--- /dev/null
+++ b/isl_sample_piplib.c
@@ -0,0 +1,63 @@
+#include "isl_vec.h"
+#include "isl_piplib.h"
+#include "isl_sample_piplib.h"
+
+struct isl_vec *isl_pip_basic_set_sample(struct isl_ctx *ctx,
+       struct isl_basic_set *bset)
+{
+       PipOptions      *options = NULL;
+       PipMatrix       *domain = NULL;
+       PipQuast        *sol = NULL;
+       struct isl_basic_map *bmap = (struct isl_basic_map *)bset;
+       struct isl_vec *vec = NULL;
+       unsigned        dim;
+
+       if (!bmap)
+               goto error;
+       dim = bmap->nparam + bmap->n_in + bmap->n_out;
+       domain = isl_basic_map_to_pip(bmap, 0, 0, 0);
+       if (!domain)
+               goto error;
+
+       options = pip_options_init();
+       if (!options)
+               goto error;
+       options->Simplify = 1;
+       options->Urs_unknowns = -1;
+       sol = pip_solve(domain, NULL, -1, options);
+       if (!sol)
+               goto error;
+       if (!sol->list)
+               vec = isl_vec_alloc(ctx, 0);
+       else {
+               PipList *l;
+               int i;
+               vec = isl_vec_alloc(ctx, 1 + dim);
+               if (!vec)
+                       goto error;
+               isl_int_set_si(vec->block.data[0], 1);
+               for (i = 0, l = sol->list; l && i < dim; ++i, l = l->next) {
+                       isl_seq_cpy_from_pip(&vec->block.data[1+i],
+                                       &l->vector->the_vector[0], 1);
+                       if (entier_zero_p(l->vector->the_deno[0]))
+                               isl_int_set_si(vec->block.data[0], 0);
+               }
+               if (i != dim)
+                       goto error;
+       }
+
+       pip_quast_free(sol);
+       pip_options_free(options);
+       pip_matrix_free(domain);
+
+       isl_basic_map_free(ctx, bmap);
+       return vec;
+error:
+       isl_vec_free(ctx, vec);
+       isl_basic_map_free(ctx, bmap);
+       if (sol)
+               pip_quast_free(sol);
+       if (domain)
+               pip_matrix_free(domain);
+       return NULL;
+}

diff --git a/isl_sample_piplib.h b/isl_sample_piplib.h
new file mode 100644 (file)
index 0000000..8f68620
--- /dev/null
+++ b/isl_sample_piplib.h
@@ -0,0 +1,17 @@
+#ifndef ISL_SAMPLE_PIP_H
+#define ISL_SAMPLE_PIP
+
+#include <isl_set.h>
+
+#if defined(__cplusplus)
+extern "C" {
+#endif
+
+struct isl_vec *isl_pip_basic_set_sample(struct isl_ctx *ctx,
+       struct isl_basic_set *bset);
+
+#if defined(__cplusplus)
+}
+#endif
+
+#endif

diff --git a/isl_vec.c b/isl_vec.c
new file mode 100644 (file)
index 0000000..e4ae06b
--- /dev/null
+++ b/isl_vec.c
@@ -0,0 +1,56 @@
+#include "isl_vec.h"
+
+struct isl_vec *isl_vec_alloc(struct isl_ctx *ctx, unsigned size)
+{
+       struct isl_vec *vec;
+
+       vec = isl_alloc_type(ctx, struct isl_vec);
+       if (!vec)
+               return NULL;
+
+       vec->block = isl_blk_alloc(ctx, size);
+       if (!vec->block.data)
+               goto error;
+
+       vec->ref = 1;
+       vec->size = size;
+
+       return vec;
+error:
+       isl_blk_free(ctx, vec->block);
+       return NULL;
+}
+
+struct isl_vec *isl_vec_copy(struct isl_ctx *ctx, struct isl_vec *vec)
+{
+       if (!vec)
+               return NULL;
+
+       vec->ref++;
+       return vec;
+}
+
+void isl_vec_free(struct isl_ctx *ctx, struct isl_vec *vec)
+{
+       if (!vec)
+               return;
+
+       if (--vec->ref > 0)
+               return;
+
+       isl_blk_free(ctx, vec->block);
+       free(vec);
+}
+
+void isl_vec_dump(struct isl_ctx *ctx, struct isl_vec *vec,
+                               FILE *out, int indent)
+{
+       int i;
+       fprintf(out, "%*s[", indent, "");
+       for (i = 0; i < vec->size; ++i) {
+               if (i)
+                   fprintf(out, ",");
+               isl_int_print(out, vec->block.data[i]);
+       }
+       fprintf(out, "]\n");
+}

diff --git a/isl_vec.h b/isl_vec.h
new file mode 100644 (file)
index 0000000..6733616
--- /dev/null
+++ b/isl_vec.h
@@ -0,0 +1,33 @@
+#ifndef ISL_VEC_H
+#define ISL_VEC_H
+
+#include <stdio.h>
+
+#include <isl_int.h>
+#include <isl_ctx.h>
+#include <isl_blk.h>
+
+#if defined(__cplusplus)
+extern "C" {
+#endif
+
+struct isl_vec {
+       int ref;
+
+       unsigned size;
+
+       struct isl_blk block;
+};
+
+struct isl_vec *isl_vec_alloc(struct isl_ctx *ctx, unsigned size);
+struct isl_vec *isl_vec_copy(struct isl_ctx *ctx, struct isl_vec *vec);
+void isl_vec_free(struct isl_ctx *ctx, struct isl_vec *vec);
+
+void isl_vec_dump(struct isl_ctx *ctx, struct isl_vec *vec,
+                               FILE *out, int indent);
+
+#if defined(__cplusplus)
+}
+#endif
+
+#endif