From 9c714195d6148df1dd5955c0a977ddee3125368f Mon Sep 17 00:00:00 2001 From: Sven Verdoolaege Date: Wed, 10 Mar 2010 16:31:02 +0100 Subject: [PATCH] iscc: support transitive closure --- Makefile.am | 4 ++ doc/isl.tex | 81 +++++++++++++++++++----------------- iscc.c | 129 +++++++++++++++++++++++++++++++++++++++++++++++++++------ isl_obj_list.c | 116 +++++++++++++++++++++++++++++++++++++++++++++++++++ isl_obj_list.h | 16 +++++++ 5 files changed, 295 insertions(+), 51 deletions(-) create mode 100644 isl_obj_list.c create mode 100644 isl_obj_list.h diff --git a/Makefile.am b/Makefile.am index c284a34..4c5b540 100644 --- a/Makefile.am +++ b/Makefile.am @@ -365,6 +365,10 @@ evalue_convert_SOURCES = \ evalue_read.c \ evalue_read.h \ $(FDSTREAM) +iscc_SOURCES = \ + isl_obj_list.h \ + isl_obj_list.c \ + iscc.c iscc_LDADD = \ libbarvinok.la libbarvinok-core.la @ISL_POLYLIB_LIBS@ @ISL_LIBS@ \ @POLYLIB_LIBS@ @PIPLIB_LIBS@ diff --git a/doc/isl.tex b/doc/isl.tex index 0fef5bf..b30258b 100644 --- a/doc/isl.tex +++ b/doc/isl.tex @@ -36,8 +36,7 @@ quasipolynomial that only involves the parameters. The \ai[\tt]{iscc} calculator offers an interface to some of the functionality provided by the \isl/ and \barvinok/ libraries. -The unary operations are shown in \autoref{t:iscc:unary}, -while the binary operations are shown in \autoref{t:iscc:binary}. +The supported operations are shown in \autoref{t:iscc}. Here are some examples: \begin{verbatim} P := [n, m] -> { [i,j] : 0 <= i <= n and i <= j <= m }; @@ -54,93 +53,97 @@ f := [n] -> { [i] -> 2*n*i - n*n + 3*n - 1/2*i*i - 3/2*i-1 : ub f; u := ub f; u @ [n] -> { [] : 0 <= n <= 10 }; + +m := [n] -> { [i,j] -> [i+1,j+1] : 1 <= i,j < n; + [i,j] -> [i+1,j-1] : 1 <= i < n and 2 <= j <= n }; +m^+; +(m^+)[0]; \end{verbatim} \begin{table} -\begin{tabular}{lllp{0.5\textwidth}} -Name & Argument type & Result type & Meaning +\begin{tabular}{llp{0.5\textwidth}} +Syntax & Result type & Meaning \\ \hline -\ai[\tt]{card} & set & pw quasipolynomial & +\ai[\tt]{card} {\it set } & pw quasipolynomial & number of elements in the set \\ -\ai[\tt]{card} & map & pw quasipolynomial & +\ai[\tt]{card} {\it map } & pw quasipolynomial & number of elements in the image of a domain element \\ -\ai[\tt]{dom} & map & set & +\ai[\tt]{dom} {\it map } & set & domain of map \\ -\ai[\tt]{ran} & map & set & +\ai[\tt]{ran} {\it map } & set & range of map \\ -\ai[\tt]{lexmin} & set & set & +\ai[\tt]{lexmin} {\it set } & set & lexicographically minimal element of a set \\ -\ai[\tt]{lexmin} & map & map & +\ai[\tt]{lexmin} {\it map } & map & lexicographically minimal image element \\ -\ai[\tt]{lexmax} & set & set & +\ai[\tt]{lexmax} {\it set } & set & lexicographically maximal element of a set \\ -\ai[\tt]{lexmax} & map & map & +\ai[\tt]{lexmax} {\it map } & map & lexicographically maximal image element \\ -\ai[\tt]{sample} & set & set & +\ai[\tt]{sample} {\it set } & set & a sample element of the set \\ -\ai[\tt]{sample} & map & map & +\ai[\tt]{sample} {\it map } & map & a sample element of the map \\ -\ai[\tt]{sum} & pw qp & pw qp & +\ai[\tt]{sum} {\it pw\_qp } & pw qp & sum over all integer points in the domain \\ -\ai[\tt]{ub} & pw qp & pw qp fold & +\ai[\tt]{ub} {\it pwqp } & pw qp fold & upper bound on the quasipolynomial over all integer points in the domain. This operation is only available if \ai[\tt]{GiNaC} support was compiled in. \\ -\end{tabular} -\caption{\protect\ai[\tt]{iscc} unary operations} -\label{t:iscc:unary} -\end{table} - -\begin{table} -\begin{tabular}{llllp{0.5\textwidth}} -LHS type & Name & RHS type & Result type & Meaning +{\it set} \ai{$+$} {\it set} & set & union \\ -\hline -set & \ai{$+$} & set & set & union -\\ -map & \ai{$+$} & map & map & union +{\it map} \ai{$+$} {\it map} & map & union \\ -pwqp & \ai{$+$} & pwqp & pwqp & sum +{\it pwqp} \ai{$+$} {\it pwqp} & pwqp & sum \\ -set & \ai{$-$} & set & set & set difference +{\it set} \ai{$-$} {\it set} & set & set difference \\ -map & \ai{$-$} & map & map & set difference +{\it map} \ai{$-$} {\it map} & map & set difference \\ -pwqp & \ai{$-$} & pwqp & pwqp & difference +{\it pwqp} \ai{$-$} {\it pwqp} & pwqp & difference \\ -set & \ai{$*$} & set & set & intersection +{\it set} \ai{$*$} {\it set} & set & intersection \\ -map & \ai{$*$} & map & map & intersection +{\it map} \ai{$*$} {\it map} & map & intersection \\ -pwqp & \ai{$*$} & pwqp & pwqp & product +{\it pwqp} \ai{$*$} {\it pwqp} & pwqp & product \\ -pwqp & \ai{@} & set & pwqp & +{\it pwqp} \ai{@} {\it set} & pwqp & evaluate the piecewise quasipolynomial in each element of the set and return a piecewise quasipolynomial mapping each of the individual elements to the resulting constant \\ -pw qp fold & \ai{@} & set & pwqp & +{\it pwqpfold} \ai{@} {\it set} & pwqp & evaluate the piecewise quasipolynomial fold in each element of the set and return a piecewise quasipolynomial mapping each of the individual elements to the resulting constant \\ +{\it map} \ai[\tt]{\^{}+} & list & +compute an overapproximation of the transitive closure +and return a list containing the overapproximation +and a boolean that is true if the overapproximation +is known to be exact +\\ +{\it list} [{\it int}] & & +the element at the given position in the list +\\ \end{tabular} -\caption{\protect\ai[\tt]{iscc} binary operations} -\label{t:iscc:binary} +\caption{\protect\ai[\tt]{iscc} operations} +\label{t:iscc} \end{table} diff --git a/iscc.c b/iscc.c index 4e828f5..8af3d62 100644 --- a/iscc.c +++ b/iscc.c @@ -3,6 +3,7 @@ #include #include #include +#include #include #include "config.h" @@ -10,6 +11,45 @@ #include #endif +static int isl_bool_false = 0; +static int isl_bool_true = 1; +static int isl_bool_error = -1; + +static void *isl_obj_bool_copy(void *v) +{ + return v; +} + +static void isl_obj_bool_free(void *v) +{ +} + +static void isl_obj_bool_print(void *v, FILE *out) +{ + if (v == &isl_bool_true) + fprintf(out, "True"); + else if (v == &isl_bool_false) + fprintf(out, "False"); + else + fprintf(out, "Error"); +} + +static void *isl_obj_bool_add(void *v1, void *v2) +{ + return v1; +} + +struct isl_obj_vtable isl_obj_bool_vtable = { + isl_obj_bool_copy, + isl_obj_bool_add, + isl_obj_bool_print, + isl_obj_bool_free +}; +#define isl_obj_bool (&isl_obj_bool_vtable) + +extern struct isl_obj_vtable isl_obj_list_vtable; +#define isl_obj_list (&isl_obj_list_vtable) + typedef void *(*isc_bin_op_fn)(void *lhs, void *rhs); struct isc_bin_op { enum isl_token_type op; @@ -370,6 +410,65 @@ error: return obj; } +static struct isl_obj transitive_closure(struct isl_ctx *ctx, struct isl_obj obj) +{ + struct isl_list *list; + int exact; + + isl_assert(ctx, obj.type == isl_obj_map, goto error); + list = isl_list_alloc(ctx, 2); + if (!list) + goto error; + + list->obj[0].type = isl_obj_map; + list->obj[0].v = isl_map_transitive_closure(obj.v, &exact); + list->obj[1].type = isl_obj_bool; + list->obj[1].v = exact ? &isl_bool_true : &isl_bool_false; + obj.v = list; + obj.type = isl_obj_list; + if (exact < 0 || !list->obj[0].v) + goto error; + + return obj; +error: + free_obj(obj); + obj.type = isl_obj_none; + obj.v = NULL; + return obj; +} + +static struct isl_obj obj_at_index(struct isl_stream *s, struct isl_obj obj) +{ + struct isl_list *list = obj.v; + struct isl_token *tok; + int i; + + tok = isl_stream_next_token(s); + if (!tok || tok->type != ISL_TOKEN_VALUE) { + isl_stream_error(s, tok, "expecting index"); + if (tok) + isl_stream_push_token(s, tok); + goto error; + } + i = isl_int_get_si(tok->u.v); + isl_token_free(tok); + isl_assert(s, i < list->n, goto error); + if (isl_stream_eat(s, ']')) + goto error; + + obj = list->obj[i]; + obj.v = obj.type->copy(obj.v); + + isl_list_free(list); + + return obj; +error: + free_obj(obj); + obj.type = isl_obj_none; + obj.v = NULL; + return obj; +} + static struct isl_obj read_obj(struct isl_stream *s, struct isl_hash_table *table) { @@ -381,21 +480,27 @@ static struct isl_obj read_obj(struct isl_stream *s, obj = read_expr(s, table); if (isl_stream_eat(s, ')')) goto error; - return obj; - } - - op = read_prefix_un_op_if_available(s); - if (op) - return read_un_op_expr(s, table, op); - - name = isl_stream_read_ident_if_available(s); - if (name) { - obj = stored_obj(s->ctx, table, name); } else { - obj = isl_stream_read_obj(s); - assert(obj.v); + op = read_prefix_un_op_if_available(s); + if (op) + return read_un_op_expr(s, table, op); + + name = isl_stream_read_ident_if_available(s); + if (name) { + obj = stored_obj(s->ctx, table, name); + } else { + obj = isl_stream_read_obj(s); + assert(obj.v); + } } + if (isl_stream_eat_if_available(s, '^')) { + if (isl_stream_eat(s, '+')) + goto error; + obj = transitive_closure(s->ctx, obj); + } else if (obj.type == isl_obj_list && isl_stream_eat_if_available(s, '[')) + obj = obj_at_index(s, obj); + return obj; error: free_obj(obj); diff --git a/isl_obj_list.c b/isl_obj_list.c new file mode 100644 index 0000000..9c020ad --- /dev/null +++ b/isl_obj_list.c @@ -0,0 +1,116 @@ +#include + +struct isl_list *isl_list_alloc(struct isl_ctx *ctx, int n) +{ + int i; + struct isl_list *list; + + isl_assert(ctx, n >= 0, return NULL); + list = isl_alloc(ctx, struct isl_list, + sizeof(struct isl_list) + + (n - 1) * sizeof(struct isl_obj)); + if (!list) + return NULL; + + list->ctx = ctx; + isl_ctx_ref(list->ctx); + list->ref = 1; + list->n = n; + + for (i = 0; i < n; ++i) { + list->obj[i].type = isl_obj_none; + list->obj[i].v = NULL; + } + + return list; +} + +struct isl_list *isl_list_copy(struct isl_list *list) +{ + if (!list) + return NULL; + + list->ref++; + return list; +} + +void isl_list_free(struct isl_list *list) +{ + int i; + + if (!list) + return; + + if (--list->ref > 0) + return; + + for (i = 0; i < list->n; ++i) + list->obj[i].type->free(list->obj[i].v); + isl_ctx_deref(list->ctx); + free(list); +} + +static void *isl_obj_list_copy(void *v) +{ + return isl_list_copy((struct isl_list *)v); +} + +static void isl_obj_list_free(void *v) +{ + isl_list_free((struct isl_list *)v); +} + +static void isl_obj_list_print(void *v, FILE *out) +{ + struct isl_list *list = (struct isl_list *)v; + int i; + + fprintf(out, "("); + for (i = 0; i < list->n; ++i) { + if (i) + fprintf(out, ", "); + list->obj[i].type->print(list->obj[i].v, out); + } + fprintf(out, ")"); +} + +static void *isl_obj_list_add(void *v1, void *v2) +{ + int i; + struct isl_list *list1 = (struct isl_list *)v1; + struct isl_list *list2 = (struct isl_list *)v2; + struct isl_list *list; + + if (!list1 || !list2) + goto error; + + list = isl_list_alloc(list1->ctx, list1->n + list2->n); + if (!list) + goto error; + + for (i = 0; i < list1->n; ++i) { + list->obj[i].type = list1->obj[i].type; + list->obj[i].v = list1->obj[i].type->copy(list1->obj[i].v); + } + + for (i = 0; i < list2->n; ++i) { + list->obj[list1->n + i].type = list2->obj[i].type; + list->obj[list1->n + i].v = list2->obj[i].type->copy(list2->obj[i].v); + } + + isl_list_free(list1); + isl_list_free(list2); + + return list; +error: + isl_list_free(list1); + isl_list_free(list2); + return NULL; +} + +struct isl_obj_vtable isl_obj_list_vtable = { + isl_obj_list_copy, + isl_obj_list_add, + isl_obj_list_print, + isl_obj_list_free +}; diff --git a/isl_obj_list.h b/isl_obj_list.h new file mode 100644 index 0000000..671f8a2 --- /dev/null +++ b/isl_obj_list.h @@ -0,0 +1,16 @@ +#include + +struct isl_list { + int ref; + + struct isl_ctx *ctx; + + int n; + struct isl_obj obj[1]; +}; + +struct isl_list *isl_list_alloc(struct isl_ctx *ctx, int n); +void isl_list_free(struct isl_list *list); + +extern struct isl_obj_vtable isl_obj_list_vtable; +#define isl_obj_list (&isl_obj_list_vtable) -- 2.11.4.GIT