add isl_val abstraction
authorSven Verdoolaege <skimo@kotnet.org>
Sun, 21 Apr 2013 20:59:57 +0000 (22:59 +0200)
committerSven Verdoolaege <skimo@kotnet.org>
Tue, 28 May 2013 16:15:04 +0000 (18:15 +0200)
An isl_val can represent integer and rational values as well as some
special values.  isl_vals are meant to replace isl_ints in the external
interface as well as some abuses of isl_qpolynomials.

The advantage of isl_vals is that they behave like other isl objects and
that they do not expose how integer values are represented internally.
This means that the user will not have to take into account that GMP
is being used and that GMP can be replaced by another library without
affecting the user.

Signed-off-by: Sven Verdoolaege <skimo@kotnet.org>
Makefile.am
doc/user.pod
include/isl/val.h [new file with mode: 0644]
isl_input.c
isl_test.c
isl_val.c [new file with mode: 0644]
isl_val_private.h [new file with mode: 0644]
print.c

index 2477a73..be498c7 100644 (file)
@@ -137,6 +137,7 @@ libisl_la_SOURCES = \
        isl_transitive_closure.c \
        isl_union_map.c \
        isl_union_map_private.h \
+       isl_val.c \
        isl_vec.c \
        isl_version.c \
        isl_vertices_private.h \
@@ -250,6 +251,7 @@ pkginclude_HEADERS = \
        include/isl/union_map_type.h \
        include/isl/union_set.h \
        include/isl/union_set_type.h \
+       include/isl/val.h \
        include/isl/vec.h \
        include/isl/version.h \
        include/isl/vertices.h
index 2278000..94a0fd6 100644 (file)
@@ -343,7 +343,163 @@ before the C<isl_ctx> itself is freed.
        isl_ctx *isl_ctx_alloc();
        void isl_ctx_free(isl_ctx *ctx);
 
-=head2 Integers
+=head2 Values
+
+An C<isl_val> represents an integer value, a rational value
+or one of three special values, infinity, negative infinity and NaN.
+Some predefined values can be created using the following functions.
+
+       #include <isl/val.h>
+       __isl_give isl_val *isl_val_zero(isl_ctx *ctx);
+       __isl_give isl_val *isl_val_one(isl_ctx *ctx);
+       __isl_give isl_val *isl_val_nan(isl_ctx *ctx);
+       __isl_give isl_val *isl_val_infty(isl_ctx *ctx);
+       __isl_give isl_val *isl_val_neginfty(isl_ctx *ctx);
+
+Specific integer values can be created using the following functions.
+
+       #include <isl/val.h>
+       __isl_give isl_val *isl_val_int_from_si(isl_ctx *ctx,
+               long i);
+       __isl_give isl_val *isl_val_int_from_ui(isl_ctx *ctx,
+               unsigned long u);
+
+They can be copied and freed using the following functions.
+
+       #include <isl/val.h>
+       __isl_give isl_val *isl_val_copy(__isl_keep isl_val *v);
+       void *isl_val_free(__isl_take isl_val *v);
+
+They can be inspected using the following functions.
+
+       #include <isl/val.h>
+       isl_ctx *isl_val_get_ctx(__isl_keep isl_val *val);
+       long isl_val_get_num_si(__isl_keep isl_val *v);
+       long isl_val_get_den_si(__isl_keep isl_val *v);
+       double isl_val_get_d(__isl_keep isl_val *v);
+
+Note that C<isl_val_get_num_si>, C<isl_val_get_den_si> and
+C<isl_val_get_d> can only be applied to rational values.
+
+An C<isl_val> can be modified using the following function.
+
+       #include <isl/val.h>
+       __isl_give isl_val *isl_val_set_si(__isl_take isl_val *v,
+               long i);
+
+The following unary properties are defined on C<isl_val>s.
+
+       #include <isl/val.h>
+       int isl_val_sgn(__isl_keep isl_val *v);
+       int isl_val_is_zero(__isl_keep isl_val *v);
+       int isl_val_is_one(__isl_keep isl_val *v);
+       int isl_val_is_negone(__isl_keep isl_val *v);
+       int isl_val_is_nonneg(__isl_keep isl_val *v);
+       int isl_val_is_nonpos(__isl_keep isl_val *v);
+       int isl_val_is_pos(__isl_keep isl_val *v);
+       int isl_val_is_neg(__isl_keep isl_val *v);
+       int isl_val_is_int(__isl_keep isl_val *v);
+       int isl_val_is_rat(__isl_keep isl_val *v);
+       int isl_val_is_nan(__isl_keep isl_val *v);
+       int isl_val_is_infty(__isl_keep isl_val *v);
+       int isl_val_is_neginfty(__isl_keep isl_val *v);
+
+Note that the sign of NaN is undefined.
+
+The following binary properties are defined on pairs of C<isl_val>s.
+
+       #include <isl/val.h>
+       int isl_val_lt(__isl_keep isl_val *v1,
+               __isl_keep isl_val *v2);
+       int isl_val_le(__isl_keep isl_val *v1,
+               __isl_keep isl_val *v2);
+       int isl_val_gt(__isl_keep isl_val *v1,
+               __isl_keep isl_val *v2);
+       int isl_val_ge(__isl_keep isl_val *v1,
+               __isl_keep isl_val *v2);
+       int isl_val_eq(__isl_keep isl_val *v1,
+               __isl_keep isl_val *v2);
+       int isl_val_ne(__isl_keep isl_val *v1,
+               __isl_keep isl_val *v2);
+
+For integer C<isl_val>s we additionally have the following binary property.
+
+       #include <isl/val.h>
+       int isl_val_is_divisible_by(__isl_keep isl_val *v1,
+               __isl_keep isl_val *v2);
+
+An C<isl_val> can also be compared to an integer using the following
+function.  The result is undefined for NaN.
+
+       #include <isl/val.h>
+       int isl_val_cmp_si(__isl_keep isl_val *v, long i);
+
+The following unary operations are available on C<isl_val>s.
+
+       #include <isl/val.h>
+       __isl_give isl_val *isl_val_abs(__isl_take isl_val *v);
+       __isl_give isl_val *isl_val_neg(__isl_take isl_val *v);
+       __isl_give isl_val *isl_val_floor(__isl_take isl_val *v);
+       __isl_give isl_val *isl_val_ceil(__isl_take isl_val *v);
+       __isl_give isl_val *isl_val_trunc(__isl_take isl_val *v);
+
+The following binary operations are available on C<isl_val>s.
+
+       #include <isl/val.h>
+       __isl_give isl_val *isl_val_abs(__isl_take isl_val *v);
+       __isl_give isl_val *isl_val_neg(__isl_take isl_val *v);
+       __isl_give isl_val *isl_val_floor(__isl_take isl_val *v);
+       __isl_give isl_val *isl_val_ceil(__isl_take isl_val *v);
+       __isl_give isl_val *isl_val_trunc(__isl_take isl_val *v);
+       __isl_give isl_val *isl_val_2exp(__isl_take isl_val *v);
+       __isl_give isl_val *isl_val_min(__isl_take isl_val *v1,
+               __isl_take isl_val *v2);
+       __isl_give isl_val *isl_val_max(__isl_take isl_val *v1,
+               __isl_take isl_val *v2);
+       __isl_give isl_val *isl_val_add(__isl_take isl_val *v1,
+               __isl_take isl_val *v2);
+       __isl_give isl_val *isl_val_add_ui(__isl_take isl_val *v1,
+               unsigned long v2);
+       __isl_give isl_val *isl_val_sub(__isl_take isl_val *v1,
+               __isl_take isl_val *v2);
+       __isl_give isl_val *isl_val_sub_ui(__isl_take isl_val *v1,
+               unsigned long v2);
+       __isl_give isl_val *isl_val_mul(__isl_take isl_val *v1,
+               __isl_take isl_val *v2);
+       __isl_give isl_val *isl_val_mul_ui(__isl_take isl_val *v1,
+               unsigned long v2);
+       __isl_give isl_val *isl_val_div(__isl_take isl_val *v1,
+               __isl_take isl_val *v2);
+
+On integer values, we additionally have the following operations.
+
+       #include <isl/val.h>
+       __isl_give isl_val *isl_val_2exp(__isl_take isl_val *v);
+       __isl_give isl_val *isl_val_mod(__isl_take isl_val *v1,
+               __isl_take isl_val *v2);
+       __isl_give isl_val *isl_val_gcd(__isl_take isl_val *v1,
+               __isl_take isl_val *v2);
+       __isl_give isl_val *isl_val_gcdext(__isl_take isl_val *v1,
+               __isl_take isl_val *v2, __isl_give isl_val **x,
+               __isl_give isl_val **y);
+
+The function C<isl_val_gcdext> returns the greatest common divisor g
+of C<v1> and C<v2> as well as two integers C<*x> and C<*y> such
+that C<*x> * C<v1> + C<*y> * C<v2> = g.
+
+A value can be read from input using
+
+       #include <isl/val.h>
+       __isl_give isl_val *isl_val_read_from_str(isl_ctx *ctx,
+               const char *str);
+
+A value can be printed using
+
+       #include <isl/val.h>
+       __isl_give isl_printer *isl_printer_print_val(
+               __isl_take isl_printer *p, __isl_keep isl_val *v);
+
+=head2 Integers (obsolescent)
 
 All operations on integers, mainly the coefficients
 of the constraints describing the sets and relations,
diff --git a/include/isl/val.h b/include/isl/val.h
new file mode 100644 (file)
index 0000000..8c3a6f0
--- /dev/null
@@ -0,0 +1,87 @@
+#ifndef ISL_VAL_H
+#define ISL_VAL_H
+
+#include <isl/ctx.h>
+#include <isl/printer.h>
+
+#if defined(__cplusplus)
+extern "C" {
+#endif
+
+struct isl_val;
+typedef struct isl_val isl_val;
+
+__isl_give isl_val *isl_val_zero(isl_ctx *ctx);
+__isl_give isl_val *isl_val_one(isl_ctx *ctx);
+__isl_give isl_val *isl_val_nan(isl_ctx *ctx);
+__isl_give isl_val *isl_val_infty(isl_ctx *ctx);
+__isl_give isl_val *isl_val_neginfty(isl_ctx *ctx);
+__isl_give isl_val *isl_val_int_from_si(isl_ctx *ctx, long i);
+__isl_give isl_val *isl_val_int_from_ui(isl_ctx *ctx, unsigned long u);
+
+__isl_give isl_val *isl_val_copy(__isl_keep isl_val *v);
+void *isl_val_free(__isl_take isl_val *v);
+
+isl_ctx *isl_val_get_ctx(__isl_keep isl_val *val);
+long isl_val_get_num_si(__isl_keep isl_val *v);
+long isl_val_get_den_si(__isl_keep isl_val *v);
+double isl_val_get_d(__isl_keep isl_val *v);
+
+__isl_give isl_val *isl_val_set_si(__isl_take isl_val *v, long i);
+
+__isl_give isl_val *isl_val_abs(__isl_take isl_val *v);
+__isl_give isl_val *isl_val_neg(__isl_take isl_val *v);
+__isl_give isl_val *isl_val_floor(__isl_take isl_val *v);
+__isl_give isl_val *isl_val_ceil(__isl_take isl_val *v);
+__isl_give isl_val *isl_val_trunc(__isl_take isl_val *v);
+__isl_give isl_val *isl_val_2exp(__isl_take isl_val *v);
+__isl_give isl_val *isl_val_min(__isl_take isl_val *v1, __isl_take isl_val *v2);
+__isl_give isl_val *isl_val_max(__isl_take isl_val *v1, __isl_take isl_val *v2);
+__isl_give isl_val *isl_val_add(__isl_take isl_val *v1, __isl_take isl_val *v2);
+__isl_give isl_val *isl_val_add_ui(__isl_take isl_val *v1, unsigned long v2);
+__isl_give isl_val *isl_val_sub(__isl_take isl_val *v1, __isl_take isl_val *v2);
+__isl_give isl_val *isl_val_sub_ui(__isl_take isl_val *v1, unsigned long v2);
+__isl_give isl_val *isl_val_mul(__isl_take isl_val *v1, __isl_take isl_val *v2);
+__isl_give isl_val *isl_val_mul_ui(__isl_take isl_val *v1, unsigned long v2);
+__isl_give isl_val *isl_val_div(__isl_take isl_val *v1, __isl_take isl_val *v2);
+__isl_give isl_val *isl_val_mod(__isl_take isl_val *v1, __isl_take isl_val *v2);
+__isl_give isl_val *isl_val_gcd(__isl_take isl_val *v1, __isl_take isl_val *v2);
+__isl_give isl_val *isl_val_gcdext(__isl_take isl_val *v1,
+       __isl_take isl_val *v2, __isl_give isl_val **x, __isl_give isl_val **y);
+
+int isl_val_sgn(__isl_keep isl_val *v);
+int isl_val_is_zero(__isl_keep isl_val *v);
+int isl_val_is_one(__isl_keep isl_val *v);
+int isl_val_is_negone(__isl_keep isl_val *v);
+int isl_val_is_nonneg(__isl_keep isl_val *v);
+int isl_val_is_nonpos(__isl_keep isl_val *v);
+int isl_val_is_pos(__isl_keep isl_val *v);
+int isl_val_is_neg(__isl_keep isl_val *v);
+int isl_val_is_int(__isl_keep isl_val *v);
+int isl_val_is_rat(__isl_keep isl_val *v);
+int isl_val_is_nan(__isl_keep isl_val *v);
+int isl_val_is_infty(__isl_keep isl_val *v);
+int isl_val_is_neginfty(__isl_keep isl_val *v);
+
+int isl_val_cmp_si(__isl_keep isl_val *v, long i);
+
+int isl_val_lt(__isl_keep isl_val *v1, __isl_keep isl_val *v2);
+int isl_val_le(__isl_keep isl_val *v1, __isl_keep isl_val *v2);
+int isl_val_gt(__isl_keep isl_val *v1, __isl_keep isl_val *v2);
+int isl_val_ge(__isl_keep isl_val *v1, __isl_keep isl_val *v2);
+int isl_val_eq(__isl_keep isl_val *v1, __isl_keep isl_val *v2);
+int isl_val_ne(__isl_keep isl_val *v1, __isl_keep isl_val *v2);
+
+int isl_val_is_divisible_by(__isl_keep isl_val *v1, __isl_keep isl_val *v2);
+
+__isl_give isl_val *isl_val_read_from_str(isl_ctx *ctx, const char *str);
+__isl_give isl_printer *isl_printer_print_val(__isl_take isl_printer *p,
+       __isl_keep isl_val *v);
+void isl_val_dump(__isl_keep isl_val *v);
+__isl_give char *isl_val_to_str(__isl_keep isl_val *v);
+
+#if defined(__cplusplus)
+}
+#endif
+
+#endif
index 7400629..164a269 100644 (file)
@@ -26,6 +26,7 @@
 #include <isl_mat_private.h>
 #include <isl_aff_private.h>
 #include <isl/list.h>
+#include <isl_val_private.h>
 
 struct variable {
        char                    *name;
@@ -168,6 +169,86 @@ error:
        return NULL;
 }
 
+/* Read an isl_val from "s".
+ *
+ * The following token sequences are recognized
+ *
+ *     "infty"         ->      infty
+ *     "-" "infty"     ->      -infty
+ *     "NaN"           ->      NaN
+ *     n "/" d         ->      n/d
+ *     v               ->      v
+ *
+ * where n, d and v are integer constants.
+ */
+__isl_give isl_val *isl_stream_read_val(struct isl_stream *s)
+{
+       struct isl_token *tok = NULL;
+       struct isl_token *tok2 = NULL;
+       isl_val *val;
+
+       tok = next_token(s);
+       if (!tok) {
+               isl_stream_error(s, NULL, "unexpected EOF");
+               goto error;
+       }
+       if (tok->type == ISL_TOKEN_INFTY) {
+               isl_token_free(tok);
+               return isl_val_infty(s->ctx);
+       }
+       if (tok->type == '-' &&
+           isl_stream_eat_if_available(s, ISL_TOKEN_INFTY)) {
+               isl_token_free(tok);
+               return isl_val_neginfty(s->ctx);
+       }
+       if (tok->type == ISL_TOKEN_NAN) {
+               isl_token_free(tok);
+               return isl_val_nan(s->ctx);
+       }
+       if (tok->type != ISL_TOKEN_VALUE) {
+               isl_stream_error(s, tok, "expecting value");
+               goto error;
+       }
+
+       if (isl_stream_eat_if_available(s, '/')) {
+               tok2 = next_token(s);
+               if (!tok2) {
+                       isl_stream_error(s, NULL, "unexpected EOF");
+                       goto error;
+               }
+               if (tok2->type != ISL_TOKEN_VALUE) {
+                       isl_stream_error(s, tok2, "expecting value");
+                       goto error;
+               }
+               val = isl_val_rat_from_isl_int(s->ctx, tok->u.v, tok2->u.v);
+               val = isl_val_normalize(val);
+       } else {
+               val = isl_val_int_from_isl_int(s->ctx, tok->u.v);
+       }
+
+       isl_token_free(tok);
+       isl_token_free(tok2);
+       return val;
+error:
+       isl_token_free(tok);
+       isl_token_free(tok2);
+       return NULL;
+}
+
+/* Read an isl_val from "str".
+ */
+struct isl_val *isl_val_read_from_str(struct isl_ctx *ctx,
+       const char *str)
+{
+       isl_val *val;
+       struct isl_stream *s = isl_stream_new_str(ctx, str);
+       if (!s)
+               return NULL;
+       val = isl_stream_read_val(s);
+       isl_stream_free(s);
+       return val;
+}
+
 static int accept_cst_factor(struct isl_stream *s, isl_int *f)
 {
        struct isl_token *tok;
index ee1bd04..df7de06 100644 (file)
@@ -23,6 +23,7 @@
 #include <isl_options_private.h>
 #include <isl/vertices.h>
 #include <isl/ast_build.h>
+#include <isl/val.h>
 
 #define ARRAY_SIZE(array) (sizeof(array)/sizeof(*array))
 
@@ -322,6 +323,221 @@ void test_dim(struct isl_ctx *ctx)
        isl_map_free(map2);
 }
 
+struct {
+       __isl_give isl_val *(*op)(__isl_take isl_val *v);
+       const char *arg;
+       const char *res;
+} val_un_tests[] = {
+       { &isl_val_neg, "0", "0" },
+       { &isl_val_abs, "0", "0" },
+       { &isl_val_2exp, "0", "1" },
+       { &isl_val_floor, "0", "0" },
+       { &isl_val_ceil, "0", "0" },
+       { &isl_val_neg, "1", "-1" },
+       { &isl_val_neg, "-1", "1" },
+       { &isl_val_neg, "1/2", "-1/2" },
+       { &isl_val_neg, "-1/2", "1/2" },
+       { &isl_val_neg, "infty", "-infty" },
+       { &isl_val_neg, "-infty", "infty" },
+       { &isl_val_neg, "NaN", "NaN" },
+       { &isl_val_abs, "1", "1" },
+       { &isl_val_abs, "-1", "1" },
+       { &isl_val_abs, "1/2", "1/2" },
+       { &isl_val_abs, "-1/2", "1/2" },
+       { &isl_val_abs, "infty", "infty" },
+       { &isl_val_abs, "-infty", "infty" },
+       { &isl_val_abs, "NaN", "NaN" },
+       { &isl_val_floor, "1", "1" },
+       { &isl_val_floor, "-1", "-1" },
+       { &isl_val_floor, "1/2", "0" },
+       { &isl_val_floor, "-1/2", "-1" },
+       { &isl_val_floor, "infty", "infty" },
+       { &isl_val_floor, "-infty", "-infty" },
+       { &isl_val_floor, "NaN", "NaN" },
+       { &isl_val_ceil, "1", "1" },
+       { &isl_val_ceil, "-1", "-1" },
+       { &isl_val_ceil, "1/2", "1" },
+       { &isl_val_ceil, "-1/2", "0" },
+       { &isl_val_ceil, "infty", "infty" },
+       { &isl_val_ceil, "-infty", "-infty" },
+       { &isl_val_ceil, "NaN", "NaN" },
+       { &isl_val_2exp, "-3", "1/8" },
+       { &isl_val_2exp, "-1", "1/2" },
+       { &isl_val_2exp, "1", "2" },
+       { &isl_val_2exp, "2", "4" },
+       { &isl_val_2exp, "3", "8" },
+};
+
+/* Perform some basic tests of unary operations on isl_val objects.
+ */
+static int test_un_val(isl_ctx *ctx)
+{
+       int i;
+       isl_val *v, *res;
+       __isl_give isl_val *(*fn)(__isl_take isl_val *v);
+       int ok;
+
+       for (i = 0; i < ARRAY_SIZE(val_un_tests); ++i) {
+               v = isl_val_read_from_str(ctx, val_un_tests[i].arg);
+               res = isl_val_read_from_str(ctx, val_un_tests[i].res);
+               fn = val_un_tests[i].op;
+               v = fn(v);
+               if (isl_val_is_nan(res))
+                       ok = isl_val_is_nan(v);
+               else
+                       ok = isl_val_eq(v, res);
+               isl_val_free(v);
+               isl_val_free(res);
+               if (ok < 0)
+                       return -1;
+               if (!ok)
+                       isl_die(ctx, isl_error_unknown,
+                               "unexpected result", return -1);
+       }
+
+       return 0;
+}
+
+struct {
+       __isl_give isl_val *(*fn)(__isl_take isl_val *v1,
+                               __isl_take isl_val *v2);
+} val_bin_op[] = {
+       ['+'] = { &isl_val_add },
+       ['-'] = { &isl_val_sub },
+       ['*'] = { &isl_val_mul },
+       ['/'] = { &isl_val_div },
+       ['g'] = { &isl_val_gcd },
+       ['m'] = { &isl_val_min },
+       ['M'] = { &isl_val_max },
+};
+
+struct {
+       const char *arg1;
+       unsigned char op;
+       const char *arg2;
+       const char *res;
+} val_bin_tests[] = {
+       { "0", '+', "0", "0" },
+       { "1", '+', "0", "1" },
+       { "1", '+', "1", "2" },
+       { "1", '-', "1", "0" },
+       { "1", '*', "1", "1" },
+       { "1", '/', "1", "1" },
+       { "2", '*', "3", "6" },
+       { "2", '*', "1/2", "1" },
+       { "2", '*', "1/3", "2/3" },
+       { "2/3", '*', "3/5", "2/5" },
+       { "2/3", '*', "7/5", "14/15" },
+       { "2", '/', "1/2", "4" },
+       { "-2", '/', "-1/2", "4" },
+       { "-2", '/', "1/2", "-4" },
+       { "2", '/', "-1/2", "-4" },
+       { "2", '/', "2", "1" },
+       { "2", '/', "3", "2/3" },
+       { "2/3", '/', "5/3", "2/5" },
+       { "2/3", '/', "5/7", "14/15" },
+       { "0", '/', "0", "NaN" },
+       { "42", '/', "0", "NaN" },
+       { "-42", '/', "0", "NaN" },
+       { "infty", '/', "0", "NaN" },
+       { "-infty", '/', "0", "NaN" },
+       { "NaN", '/', "0", "NaN" },
+       { "0", '/', "NaN", "NaN" },
+       { "42", '/', "NaN", "NaN" },
+       { "-42", '/', "NaN", "NaN" },
+       { "infty", '/', "NaN", "NaN" },
+       { "-infty", '/', "NaN", "NaN" },
+       { "NaN", '/', "NaN", "NaN" },
+       { "0", '/', "infty", "0" },
+       { "42", '/', "infty", "0" },
+       { "-42", '/', "infty", "0" },
+       { "infty", '/', "infty", "NaN" },
+       { "-infty", '/', "infty", "NaN" },
+       { "NaN", '/', "infty", "NaN" },
+       { "0", '/', "-infty", "0" },
+       { "42", '/', "-infty", "0" },
+       { "-42", '/', "-infty", "0" },
+       { "infty", '/', "-infty", "NaN" },
+       { "-infty", '/', "-infty", "NaN" },
+       { "NaN", '/', "-infty", "NaN" },
+       { "1", '-', "1/3", "2/3" },
+       { "1/3", '+', "1/2", "5/6" },
+       { "1/2", '+', "1/2", "1" },
+       { "3/4", '-', "1/4", "1/2" },
+       { "1/2", '-', "1/3", "1/6" },
+       { "infty", '+', "42", "infty" },
+       { "infty", '+', "infty", "infty" },
+       { "42", '+', "infty", "infty" },
+       { "infty", '-', "infty", "NaN" },
+       { "infty", '*', "infty", "infty" },
+       { "infty", '*', "-infty", "-infty" },
+       { "-infty", '*', "infty", "-infty" },
+       { "-infty", '*', "-infty", "infty" },
+       { "0", '*', "infty", "NaN" },
+       { "1", '*', "infty", "infty" },
+       { "infty", '*', "0", "NaN" },
+       { "infty", '*', "42", "infty" },
+       { "42", '-', "infty", "-infty" },
+       { "infty", '+', "-infty", "NaN" },
+       { "4", 'g', "6", "2" },
+       { "5", 'g', "6", "1" },
+       { "42", 'm', "3", "3" },
+       { "42", 'M', "3", "42" },
+       { "3", 'm', "42", "3" },
+       { "3", 'M', "42", "42" },
+       { "42", 'm', "infty", "42" },
+       { "42", 'M', "infty", "infty" },
+       { "42", 'm', "-infty", "-infty" },
+       { "42", 'M', "-infty", "42" },
+       { "42", 'm', "NaN", "NaN" },
+       { "42", 'M', "NaN", "NaN" },
+       { "infty", 'm', "-infty", "-infty" },
+       { "infty", 'M', "-infty", "infty" },
+};
+
+/* Perform some basic tests of binary operations on isl_val objects.
+ */
+static int test_bin_val(isl_ctx *ctx)
+{
+       int i;
+       isl_val *v1, *v2, *res;
+       __isl_give isl_val *(*fn)(__isl_take isl_val *v1,
+                               __isl_take isl_val *v2);
+       int ok;
+
+       for (i = 0; i < ARRAY_SIZE(val_bin_tests); ++i) {
+               v1 = isl_val_read_from_str(ctx, val_bin_tests[i].arg1);
+               v2 = isl_val_read_from_str(ctx, val_bin_tests[i].arg2);
+               res = isl_val_read_from_str(ctx, val_bin_tests[i].res);
+               fn = val_bin_op[val_bin_tests[i].op].fn;
+               v1 = fn(v1, v2);
+               if (isl_val_is_nan(res))
+                       ok = isl_val_is_nan(v1);
+               else
+                       ok = isl_val_eq(v1, res);
+               isl_val_free(v1);
+               isl_val_free(res);
+               if (ok < 0)
+                       return -1;
+               if (!ok)
+                       isl_die(ctx, isl_error_unknown,
+                               "unexpected result", return -1);
+       }
+
+       return 0;
+}
+
+/* Perform some basic tests on isl_val objects.
+ */
+static int test_val(isl_ctx *ctx)
+{
+       if (test_un_val(ctx) < 0)
+               return -1;
+       if (test_bin_val(ctx) < 0)
+               return -1;
+       return 0;
+}
+
 static int test_div(isl_ctx *ctx)
 {
        unsigned n;
@@ -4048,6 +4264,7 @@ struct {
        const char *name;
        int (*fn)(isl_ctx *ctx);
 } tests [] = {
+       { "val", &test_val },
        { "compute divs", &test_compute_divs },
        { "partial lexmin", &test_partial_lexmin },
        { "simplify", &test_simplify },
diff --git a/isl_val.c b/isl_val.c
new file mode 100644 (file)
index 0000000..ff091c3
--- /dev/null
+++ b/isl_val.c
@@ -0,0 +1,1251 @@
+/*
+ * Copyright 2013      Ecole Normale Superieure
+ *
+ * Use of this software is governed by the MIT license
+ *
+ * Written by Sven Verdoolaege,
+ * Ecole Normale Superieure, 45 rue d'Ulm, 75230 Paris, France
+ */
+
+#include <isl_int.h>
+#include <isl_ctx_private.h>
+#include <isl_val_private.h>
+
+/* Allocate an isl_val object with indeterminate value.
+ */
+__isl_give isl_val *isl_val_alloc(isl_ctx *ctx)
+{
+       isl_val *v;
+
+       v = isl_alloc_type(ctx, struct isl_val);
+       if (!v)
+               return NULL;
+
+       v->ctx = ctx;
+       isl_ctx_ref(ctx);
+       v->ref = 1;
+       isl_int_init(v->n);
+       isl_int_init(v->d);
+
+       return v;
+}
+
+/* Return a reference to an isl_val representing zero.
+ */
+__isl_give isl_val *isl_val_zero(isl_ctx *ctx)
+{
+       return isl_val_int_from_si(ctx, 0);
+}
+
+/* Return a reference to an isl_val representing one.
+ */
+__isl_give isl_val *isl_val_one(isl_ctx *ctx)
+{
+       return isl_val_int_from_si(ctx, 1);
+}
+
+/* Return a reference to an isl_val representing NaN.
+ */
+__isl_give isl_val *isl_val_nan(isl_ctx *ctx)
+{
+       isl_val *v;
+
+       v = isl_val_alloc(ctx);
+       if (!v)
+               return NULL;
+
+       isl_int_set_si(v->n, 0);
+       isl_int_set_si(v->d, 0);
+
+       return v;
+}
+
+/* Change "v" into a NaN.
+ */
+__isl_give isl_val *isl_val_set_nan(__isl_take isl_val *v)
+{
+       if (!v)
+               return NULL;
+       if (isl_val_is_nan(v))
+               return v;
+       v = isl_val_cow(v);
+       if (!v)
+               return NULL;
+
+       isl_int_set_si(v->n, 0);
+       isl_int_set_si(v->d, 0);
+
+       return v;
+}
+
+/* Return a reference to an isl_val representing +infinity.
+ */
+__isl_give isl_val *isl_val_infty(isl_ctx *ctx)
+{
+       isl_val *v;
+
+       v = isl_val_alloc(ctx);
+       if (!v)
+               return NULL;
+
+       isl_int_set_si(v->n, 1);
+       isl_int_set_si(v->d, 0);
+
+       return v;
+}
+
+/* Return a reference to an isl_val representing -infinity.
+ */
+__isl_give isl_val *isl_val_neginfty(isl_ctx *ctx)
+{
+       isl_val *v;
+
+       v = isl_val_alloc(ctx);
+       if (!v)
+               return NULL;
+
+       isl_int_set_si(v->n, -1);
+       isl_int_set_si(v->d, 0);
+
+       return v;
+}
+
+/* Return a reference to an isl_val representing the integer "i".
+ */
+__isl_give isl_val *isl_val_int_from_si(isl_ctx *ctx, long i)
+{
+       isl_val *v;
+
+       v = isl_val_alloc(ctx);
+       if (!v)
+               return NULL;
+
+       isl_int_set_si(v->n, i);
+       isl_int_set_si(v->d, 1);
+
+       return v;
+}
+
+/* Change the value of "v" to be equal to the integer "i".
+ */
+__isl_give isl_val *isl_val_set_si(__isl_take isl_val *v, long i)
+{
+       if (!v)
+               return NULL;
+       if (isl_val_is_int(v) && isl_int_cmp_si(v->n, i) == 0)
+               return v;
+       v = isl_val_cow(v);
+       if (!v)
+               return NULL;
+
+       isl_int_set_si(v->n, i);
+       isl_int_set_si(v->d, 1);
+
+       return v;
+}
+
+/* Change the value of "v" to be equal to zero.
+ */
+__isl_give isl_val *isl_val_set_zero(__isl_take isl_val *v)
+{
+       return isl_val_set_si(v, 0);
+}
+
+/* Return a reference to an isl_val representing the unsigned integer "u".
+ */
+__isl_give isl_val *isl_val_int_from_ui(isl_ctx *ctx, unsigned long u)
+{
+       isl_val *v;
+
+       v = isl_val_alloc(ctx);
+       if (!v)
+               return NULL;
+
+       isl_int_set_ui(v->n, u);
+       isl_int_set_si(v->d, 1);
+
+       return v;
+}
+
+/* Return a reference to an isl_val representing the integer "n".
+ */
+__isl_give isl_val *isl_val_int_from_isl_int(isl_ctx *ctx, isl_int n)
+{
+       isl_val *v;
+
+       v = isl_val_alloc(ctx);
+       if (!v)
+               return NULL;
+
+       isl_int_set(v->n, n);
+       isl_int_set_si(v->d, 1);
+
+       return v;
+}
+
+/* Return a reference to an isl_val representing the rational value "n"/"d".
+ * Normalizing the isl_val (if needed) is left to the caller.
+ */
+__isl_give isl_val *isl_val_rat_from_isl_int(isl_ctx *ctx,
+       isl_int n, isl_int d)
+{
+       isl_val *v;
+
+       v = isl_val_alloc(ctx);
+       if (!v)
+               return NULL;
+
+       isl_int_set(v->n, n);
+       isl_int_set(v->d, d);
+
+       return v;
+}
+
+/* Return a new reference to "v".
+ */
+__isl_give isl_val *isl_val_copy(__isl_keep isl_val *v)
+{
+       if (!v)
+               return NULL;
+
+       v->ref++;
+       return v;
+}
+
+/* Return a fresh copy of "val".
+ */
+__isl_give isl_val *isl_val_dup(__isl_keep isl_val *val)
+{
+       isl_val *dup;
+
+       if (!val)
+               return NULL;
+
+       dup = isl_val_alloc(isl_val_get_ctx(val));
+       if (!dup)
+               return NULL;
+
+       isl_int_set(dup->n, val->n);
+       isl_int_set(dup->d, val->d);
+
+       return dup;
+}
+
+/* Return an isl_val that is equal to "val" and that has only
+ * a single reference.
+ */
+__isl_give isl_val *isl_val_cow(__isl_take isl_val *val)
+{
+       if (!val)
+               return NULL;
+
+       if (val->ref == 1)
+               return val;
+       val->ref--;
+       return isl_val_dup(val);
+}
+
+/* Free "v" and return NULL.
+ */
+void *isl_val_free(__isl_take isl_val *v)
+{
+       if (!v)
+               return NULL;
+
+       if (--v->ref > 0)
+               return NULL;
+
+       isl_ctx_deref(v->ctx);
+       isl_int_clear(v->n);
+       isl_int_clear(v->d);
+       free(v);
+       return NULL;
+}
+
+/* Extract the numerator of a rational value "v" as an integer.
+ *
+ * If "v" is not a rational value, then the result is undefined.
+ */
+long isl_val_get_num_si(__isl_keep isl_val *v)
+{
+       if (!v)
+               return 0;
+       if (!isl_val_is_rat(v))
+               isl_die(isl_val_get_ctx(v), isl_error_invalid,
+                       "expecting rational value", return 0);
+       if (!isl_int_fits_slong(v->n))
+               isl_die(isl_val_get_ctx(v), isl_error_invalid,
+                       "numerator too large", return 0);
+       return isl_int_get_si(v->n);
+}
+
+/* Extract the denominator of a rational value "v" as an integer.
+ *
+ * If "v" is not a rational value, then the result is undefined.
+ */
+long isl_val_get_den_si(__isl_keep isl_val *v)
+{
+       if (!v)
+               return 0;
+       if (!isl_val_is_rat(v))
+               isl_die(isl_val_get_ctx(v), isl_error_invalid,
+                       "expecting rational value", return 0);
+       if (!isl_int_fits_slong(v->d))
+               isl_die(isl_val_get_ctx(v), isl_error_invalid,
+                       "denominator too large", return 0);
+       return isl_int_get_si(v->d);
+}
+
+/* Return an approximation of "v" as a double.
+ */
+double isl_val_get_d(__isl_keep isl_val *v)
+{
+       if (!v)
+               return 0;
+       if (!isl_val_is_rat(v))
+               isl_die(isl_val_get_ctx(v), isl_error_invalid,
+                       "expecting rational value", return 0);
+       return isl_int_get_d(v->n) / isl_int_get_d(v->d);
+}
+
+/* Return the isl_ctx to which "val" belongs.
+ */
+isl_ctx *isl_val_get_ctx(__isl_keep isl_val *val)
+{
+       return val ? val->ctx : NULL;
+}
+
+/* Normalize "v".
+ *
+ * In particular, make sure that the denominator of a rational value
+ * is positive and the numerator and denominator do not have any
+ * common divisors.
+ *
+ * This function should not be called by an external user
+ * since it will only be given normalized values.
+ */
+__isl_give isl_val *isl_val_normalize(__isl_take isl_val *v)
+{
+       isl_ctx *ctx;
+
+       if (!v)
+               return NULL;
+       if (isl_val_is_int(v))
+               return v;
+       if (!isl_val_is_rat(v))
+               return v;
+       if (isl_int_is_neg(v->d)) {
+               isl_int_neg(v->d, v->d);
+               isl_int_neg(v->n, v->n);
+       }
+       ctx = isl_val_get_ctx(v);
+       isl_int_gcd(ctx->normalize_gcd, v->n, v->d);
+       if (isl_int_is_one(ctx->normalize_gcd))
+               return v;
+       isl_int_divexact(v->n, v->n, ctx->normalize_gcd);
+       isl_int_divexact(v->d, v->d, ctx->normalize_gcd);
+       return v;
+}
+
+/* Return the opposite of "v".
+ */
+__isl_give isl_val *isl_val_neg(__isl_take isl_val *v)
+{
+       if (!v)
+               return NULL;
+       if (isl_val_is_nan(v))
+               return v;
+       if (isl_val_is_zero(v))
+               return v;
+
+       v = isl_val_cow(v);
+       if (!v)
+               return NULL;
+       isl_int_neg(v->n, v->n);
+
+       return v;
+}
+
+/* Return the absolute value of "v".
+ */
+__isl_give isl_val *isl_val_abs(__isl_take isl_val *v)
+{
+       if (!v)
+               return NULL;
+       if (isl_val_is_nan(v))
+               return v;
+       if (isl_val_is_nonneg(v))
+               return v;
+       return isl_val_neg(v);
+}
+
+/* Return the "floor" (greatest integer part) of "v".
+ * That is, return the result of rounding towards -infinity.
+ */
+__isl_give isl_val *isl_val_floor(__isl_take isl_val *v)
+{
+       if (!v)
+               return NULL;
+       if (isl_val_is_int(v))
+               return v;
+       if (!isl_val_is_rat(v))
+               return v;
+
+       v = isl_val_cow(v);
+       if (!v)
+               return NULL;
+       isl_int_fdiv_q(v->n, v->n, v->d);
+       isl_int_set_si(v->d, 1);
+
+       return v;
+}
+
+/* Return the "ceiling" of "v".
+ * That is, return the result of rounding towards +infinity.
+ */
+__isl_give isl_val *isl_val_ceil(__isl_take isl_val *v)
+{
+       if (!v)
+               return NULL;
+       if (isl_val_is_int(v))
+               return v;
+       if (!isl_val_is_rat(v))
+               return v;
+
+       v = isl_val_cow(v);
+       if (!v)
+               return NULL;
+       isl_int_cdiv_q(v->n, v->n, v->d);
+       isl_int_set_si(v->d, 1);
+
+       return v;
+}
+
+/* Truncate "v".
+ * That is, return the result of rounding towards zero.
+ */
+__isl_give isl_val *isl_val_trunc(__isl_take isl_val *v)
+{
+       if (!v)
+               return NULL;
+       if (isl_val_is_int(v))
+               return v;
+       if (!isl_val_is_rat(v))
+               return v;
+
+       v = isl_val_cow(v);
+       if (!v)
+               return NULL;
+       isl_int_tdiv_q(v->n, v->n, v->d);
+       isl_int_set_si(v->d, 1);
+
+       return v;
+}
+
+/* Return 2^v, where v is an integer (that is not too large).
+ */
+__isl_give isl_val *isl_val_2exp(__isl_take isl_val *v)
+{
+       unsigned long exp;
+       int neg;
+
+       v = isl_val_cow(v);
+       if (!v)
+               return NULL;
+       if (!isl_val_is_int(v))
+               isl_die(isl_val_get_ctx(v), isl_error_invalid,
+                       "can only compute integer powers",
+                       return isl_val_free(v));
+       neg = isl_val_is_neg(v);
+       if (neg)
+               isl_int_neg(v->n, v->n);
+       if (!isl_int_fits_ulong(v->n))
+               isl_die(isl_val_get_ctx(v), isl_error_invalid,
+                       "exponent too large", return isl_val_free(v));
+       exp = isl_int_get_ui(v->n);
+       if (neg) {
+               isl_int_mul_2exp(v->d, v->d, exp);
+               isl_int_set_si(v->n, 1);
+       } else {
+               isl_int_mul_2exp(v->n, v->d, exp);
+       }
+
+       return v;
+}
+
+/* Return the minimum of "v1" and "v2".
+ */
+__isl_give isl_val *isl_val_min(__isl_take isl_val *v1, __isl_take isl_val *v2)
+{
+       if (!v1 || !v2)
+               goto error;
+
+       if (isl_val_is_nan(v1)) {
+               isl_val_free(v2);
+               return v1;
+       }
+       if (isl_val_is_nan(v2)) {
+               isl_val_free(v1);
+               return v2;
+       }
+       if (isl_val_le(v1, v2)) {
+               isl_val_free(v2);
+               return v1;
+       } else {
+               isl_val_free(v1);
+               return v2;
+       }
+error:
+       isl_val_free(v1);
+       isl_val_free(v2);
+       return NULL;
+}
+
+/* Return the maximum of "v1" and "v2".
+ */
+__isl_give isl_val *isl_val_max(__isl_take isl_val *v1, __isl_take isl_val *v2)
+{
+       if (!v1 || !v2)
+               goto error;
+
+       if (isl_val_is_nan(v1)) {
+               isl_val_free(v2);
+               return v1;
+       }
+       if (isl_val_is_nan(v2)) {
+               isl_val_free(v1);
+               return v2;
+       }
+       if (isl_val_ge(v1, v2)) {
+               isl_val_free(v2);
+               return v1;
+       } else {
+               isl_val_free(v1);
+               return v2;
+       }
+error:
+       isl_val_free(v1);
+       isl_val_free(v2);
+       return NULL;
+}
+
+/* Return the sum of "v1" and "v2".
+ */
+__isl_give isl_val *isl_val_add(__isl_take isl_val *v1, __isl_take isl_val *v2)
+{
+       if (!v1 || !v2)
+               goto error;
+       if (isl_val_is_nan(v1)) {
+               isl_val_free(v2);
+               return v1;
+       }
+       if (isl_val_is_nan(v2)) {
+               isl_val_free(v1);
+               return v2;
+       }
+       if ((isl_val_is_infty(v1) && isl_val_is_neginfty(v2)) ||
+           (isl_val_is_neginfty(v1) && isl_val_is_infty(v2))) {
+               isl_val_free(v2);
+               return isl_val_set_nan(v1);
+       }
+       if (isl_val_is_infty(v1) || isl_val_is_neginfty(v1)) {
+               isl_val_free(v2);
+               return v1;
+       }
+       if (isl_val_is_infty(v2) || isl_val_is_neginfty(v2)) {
+               isl_val_free(v1);
+               return v2;
+       }
+       if (isl_val_is_zero(v1)) {
+               isl_val_free(v1);
+               return v2;
+       }
+       if (isl_val_is_zero(v2)) {
+               isl_val_free(v2);
+               return v1;
+       }
+
+       v1 = isl_val_cow(v1);
+       if (!v1)
+               goto error;
+       if (isl_val_is_int(v1) && isl_val_is_int(v2))
+               isl_int_add(v1->n, v1->n, v2->n);
+       else {
+               if (isl_int_eq(v1->d, v2->d))
+                       isl_int_add(v1->n, v1->n, v2->n);
+               else {
+                       isl_int_mul(v1->n, v1->n, v2->d);
+                       isl_int_addmul(v1->n, v2->n, v1->d);
+                       isl_int_mul(v1->d, v1->d, v2->d);
+               }
+               v1 = isl_val_normalize(v1);
+       }
+       isl_val_free(v2);
+       return v1;
+error:
+       isl_val_free(v1);
+       isl_val_free(v2);
+       return NULL;
+}
+
+/* Return the sum of "v1" and "v2".
+ */
+__isl_give isl_val *isl_val_add_ui(__isl_take isl_val *v1, unsigned long v2)
+{
+       if (!v1)
+               return NULL;
+       if (!isl_val_is_rat(v1))
+               return v1;
+       if (v2 == 0)
+               return v1;
+       v1 = isl_val_cow(v1);
+       if (!v1)
+               return NULL;
+
+       isl_int_addmul_ui(v1->n, v1->d, v2);
+
+       return v1;
+}
+
+/* Subtract "v2" from "v1".
+ */
+__isl_give isl_val *isl_val_sub(__isl_take isl_val *v1, __isl_take isl_val *v2)
+{
+       if (!v1 || !v2)
+               goto error;
+       if (isl_val_is_nan(v1)) {
+               isl_val_free(v2);
+               return v1;
+       }
+       if (isl_val_is_nan(v2)) {
+               isl_val_free(v1);
+               return v2;
+       }
+       if ((isl_val_is_infty(v1) && isl_val_is_infty(v2)) ||
+           (isl_val_is_neginfty(v1) && isl_val_is_neginfty(v2))) {
+               isl_val_free(v2);
+               return isl_val_set_nan(v1);
+       }
+       if (isl_val_is_infty(v1) || isl_val_is_neginfty(v1)) {
+               isl_val_free(v2);
+               return v1;
+       }
+       if (isl_val_is_infty(v2) || isl_val_is_neginfty(v2)) {
+               isl_val_free(v1);
+               return isl_val_neg(v2);
+       }
+       if (isl_val_is_zero(v2)) {
+               isl_val_free(v2);
+               return v1;
+       }
+       if (isl_val_is_zero(v1)) {
+               isl_val_free(v1);
+               return isl_val_neg(v2);
+       }
+
+       v1 = isl_val_cow(v1);
+       if (!v1)
+               goto error;
+       if (isl_val_is_int(v1) && isl_val_is_int(v2))
+               isl_int_sub(v1->n, v1->n, v2->n);
+       else {
+               if (isl_int_eq(v1->d, v2->d))
+                       isl_int_sub(v1->n, v1->n, v2->n);
+               else {
+                       isl_int_mul(v1->n, v1->n, v2->d);
+                       isl_int_submul(v1->n, v2->n, v1->d);
+                       isl_int_mul(v1->d, v1->d, v2->d);
+               }
+               v1 = isl_val_normalize(v1);
+       }
+       isl_val_free(v2);
+       return v1;
+error:
+       isl_val_free(v1);
+       isl_val_free(v2);
+       return NULL;
+}
+
+/* Subtract "v2" from "v1".
+ */
+__isl_give isl_val *isl_val_sub_ui(__isl_take isl_val *v1, unsigned long v2)
+{
+       if (!v1)
+               return NULL;
+       if (!isl_val_is_rat(v1))
+               return v1;
+       if (v2 == 0)
+               return v1;
+       v1 = isl_val_cow(v1);
+       if (!v1)
+               return NULL;
+
+       isl_int_submul_ui(v1->n, v1->d, v2);
+
+       return v1;
+}
+
+/* Return the product of "v1" and "v2".
+ */
+__isl_give isl_val *isl_val_mul(__isl_take isl_val *v1, __isl_take isl_val *v2)
+{
+       if (!v1 || !v2)
+               goto error;
+       if (isl_val_is_nan(v1)) {
+               isl_val_free(v2);
+               return v1;
+       }
+       if (isl_val_is_nan(v2)) {
+               isl_val_free(v1);
+               return v2;
+       }
+       if ((!isl_val_is_rat(v1) && isl_val_is_zero(v2)) ||
+           (isl_val_is_zero(v1) && !isl_val_is_rat(v2))) {
+               isl_val_free(v2);
+               return isl_val_set_nan(v1);
+       }
+       if (isl_val_is_zero(v1)) {
+               isl_val_free(v2);
+               return v1;
+       }
+       if (isl_val_is_zero(v2)) {
+               isl_val_free(v1);
+               return v2;
+       }
+       if (isl_val_is_infty(v1) || isl_val_is_neginfty(v1)) {
+               if (isl_val_is_neg(v2))
+                       v1 = isl_val_neg(v1);
+               isl_val_free(v2);
+               return v1;
+       }
+       if (isl_val_is_infty(v2) || isl_val_is_neginfty(v2)) {
+               if (isl_val_is_neg(v1))
+                       v2 = isl_val_neg(v2);
+               isl_val_free(v1);
+               return v2;
+       }
+
+       v1 = isl_val_cow(v1);
+       if (!v1)
+               goto error;
+       if (isl_val_is_int(v1) && isl_val_is_int(v2))
+               isl_int_mul(v1->n, v1->n, v2->n);
+       else {
+               isl_int_mul(v1->n, v1->n, v2->n);
+               isl_int_mul(v1->d, v1->d, v2->d);
+               v1 = isl_val_normalize(v1);
+       }
+       isl_val_free(v2);
+       return v1;
+error:
+       isl_val_free(v1);
+       isl_val_free(v2);
+       return NULL;
+}
+
+/* Return the product of "v1" and "v2".
+ */
+__isl_give isl_val *isl_val_mul_ui(__isl_take isl_val *v1, unsigned long v2)
+{
+       if (!v1)
+               return NULL;
+       if (isl_val_is_nan(v1))
+               return v1;
+       if (!isl_val_is_rat(v1)) {
+               if (v2 == 0)
+                       v1 = isl_val_set_nan(v1);
+               return v1;
+       }
+       if (v2 == 1)
+               return v1;
+       v1 = isl_val_cow(v1);
+       if (!v1)
+               return NULL;
+
+       isl_int_mul_ui(v1->n, v1->n, v2);
+
+       return isl_val_normalize(v1);
+}
+
+/* Divide "v1" by "v2".
+ */
+__isl_give isl_val *isl_val_div(__isl_take isl_val *v1, __isl_take isl_val *v2)
+{
+       if (!v1 || !v2)
+               goto error;
+       if (isl_val_is_nan(v1)) {
+               isl_val_free(v2);
+               return v1;
+       }
+       if (isl_val_is_nan(v2)) {
+               isl_val_free(v1);
+               return v2;
+       }
+       if (isl_val_is_zero(v2) ||
+           (!isl_val_is_rat(v1) && !isl_val_is_rat(v2))) {
+               isl_val_free(v2);
+               return isl_val_set_nan(v1);
+       }
+       if (isl_val_is_zero(v1)) {
+               isl_val_free(v2);
+               return v1;
+       }
+       if (isl_val_is_infty(v1) || isl_val_is_neginfty(v1)) {
+               if (isl_val_is_neg(v2))
+                       v1 = isl_val_neg(v1);
+               isl_val_free(v2);
+               return v1;
+       }
+       if (isl_val_is_infty(v2) || isl_val_is_neginfty(v2)) {
+               isl_val_free(v2);
+               return isl_val_set_zero(v1);
+       }
+
+       v1 = isl_val_cow(v1);
+       if (!v1)
+               goto error;
+       if (isl_val_is_int(v2)) {
+               isl_int_mul(v1->d, v1->d, v2->n);
+               v1 = isl_val_normalize(v1);
+       } else {
+               isl_int_mul(v1->d, v1->d, v2->n);
+               isl_int_mul(v1->n, v1->n, v2->d);
+               v1 = isl_val_normalize(v1);
+       }
+       isl_val_free(v2);
+       return v1;
+error:
+       isl_val_free(v1);
+       isl_val_free(v2);
+       return NULL;
+}
+
+/* Given two integer values "v1" and "v2", check if "v1" is divisible by "v2".
+ */
+int isl_val_is_divisible_by(__isl_keep isl_val *v1, __isl_keep isl_val *v2)
+{
+       if (!v1 || !v2)
+               return -1;
+
+       if (!isl_val_is_int(v1) || !isl_val_is_int(v2))
+               isl_die(isl_val_get_ctx(v1), isl_error_invalid,
+                       "expecting two integers", return -1);
+
+       return isl_int_is_divisible_by(v1->n, v2->n);
+}
+
+/* Given two integer values "v1" and "v2", return the residue of "v1"
+ * modulo "v2".
+ */
+__isl_give isl_val *isl_val_mod(__isl_take isl_val *v1, __isl_take isl_val *v2)
+{
+       if (!v1 || !v2)
+               goto error;
+       if (!isl_val_is_int(v1) || !isl_val_is_int(v2))
+               isl_die(isl_val_get_ctx(v1), isl_error_invalid,
+                       "expecting two integers", goto error);
+       if (isl_val_is_nonneg(v1) && isl_val_lt(v1, v2)) {
+               isl_val_free(v2);
+               return v1;
+       }
+       v1 = isl_val_cow(v1);
+       if (!v1)
+               goto error;
+       isl_int_fdiv_r(v1->n, v1->n, v2->n);
+       isl_val_free(v2);
+       return v1;
+error:
+       isl_val_free(v1);
+       isl_val_free(v2);
+       return NULL;
+}
+
+/* Given two integer values, return their greatest common divisor.
+ */
+__isl_give isl_val *isl_val_gcd(__isl_take isl_val *v1, __isl_take isl_val *v2)
+{
+       if (!v1 || !v2)
+               goto error;
+       if (!isl_val_is_int(v1) || !isl_val_is_int(v2))
+               isl_die(isl_val_get_ctx(v1), isl_error_invalid,
+                       "expecting two integers", goto error);
+       if (isl_val_eq(v1, v2)) {
+               isl_val_free(v2);
+               return v1;
+       }
+       if (isl_val_is_one(v1)) {
+               isl_val_free(v2);
+               return v1;
+       }
+       if (isl_val_is_one(v2)) {
+               isl_val_free(v1);
+               return v2;
+       }
+       v1 = isl_val_cow(v1);
+       if (!v1)
+               goto error;
+       isl_int_gcd(v1->n, v1->n, v2->n);
+       isl_val_free(v2);
+       return v1;
+error:
+       isl_val_free(v1);
+       isl_val_free(v2);
+       return NULL;
+}
+
+/* Given two integer values v1 and v2, return their greatest common divisor g,
+ * as well as two integers x and y such that x * v1 + y * v2 = g.
+ */
+__isl_give isl_val *isl_val_gcdext(__isl_take isl_val *v1,
+       __isl_take isl_val *v2, __isl_give isl_val **x, __isl_give isl_val **y)
+{
+       isl_ctx *ctx;
+       isl_val *a = NULL, *b = NULL;
+
+       if (!x && !y)
+               return isl_val_gcd(v1, v2);
+
+       if (!v1 || !v2)
+               goto error;
+
+       ctx = isl_val_get_ctx(v1);
+       if (!isl_val_is_int(v1) || !isl_val_is_int(v2))
+               isl_die(ctx, isl_error_invalid,
+                       "expecting two integers", goto error);
+
+       v1 = isl_val_cow(v1);
+       a = isl_val_alloc(ctx);
+       b = isl_val_alloc(ctx);
+       if (!v1 || !a || !b)
+               goto error;
+       isl_int_gcdext(v1->n, a->n, b->n, v1->n, v2->n);
+       if (x) {
+               isl_int_set_si(a->d, 1);
+               *x = a;
+       } else
+               isl_val_free(a);
+       if (y) {
+               isl_int_set_si(b->d, 1);
+               *y = b;
+       } else
+               isl_val_free(b);
+       isl_val_free(v2);
+       return v1;
+error:
+       isl_val_free(v1);
+       isl_val_free(v2);
+       isl_val_free(a);
+       isl_val_free(b);
+       if (x)
+               *x = NULL;
+       if (y)
+               *y = NULL;
+       return NULL;
+}
+
+/* Does "v" represent an integer value?
+ */
+int isl_val_is_int(__isl_keep isl_val *v)
+{
+       if (!v)
+               return -1;
+
+       return isl_int_is_one(v->d);
+}
+
+/* Does "v" represent a rational value?
+ */
+int isl_val_is_rat(__isl_keep isl_val *v)
+{
+       if (!v)
+               return -1;
+
+       return !isl_int_is_zero(v->d);
+}
+
+/* Does "v" represent NaN?
+ */
+int isl_val_is_nan(__isl_keep isl_val *v)
+{
+       if (!v)
+               return -1;
+
+       return isl_int_is_zero(v->n) && isl_int_is_zero(v->d);
+}
+
+/* Does "v" represent +infinity?
+ */
+int isl_val_is_infty(__isl_keep isl_val *v)
+{
+       if (!v)
+               return -1;
+
+       return isl_int_is_pos(v->n) && isl_int_is_zero(v->d);
+}
+
+/* Does "v" represent -infinity?
+ */
+int isl_val_is_neginfty(__isl_keep isl_val *v)
+{
+       if (!v)
+               return -1;
+
+       return isl_int_is_neg(v->n) && isl_int_is_zero(v->d);
+}
+
+/* Does "v" represent the integer zero?
+ */
+int isl_val_is_zero(__isl_keep isl_val *v)
+{
+       if (!v)
+               return -1;
+
+       return isl_int_is_zero(v->n) && !isl_int_is_zero(v->d);
+}
+
+/* Does "v" represent the integer one?
+ */
+int isl_val_is_one(__isl_keep isl_val *v)
+{
+       if (!v)
+               return -1;
+
+       return isl_int_eq(v->n, v->d);
+}
+
+/* Does "v" represent the integer negative one?
+ */
+int isl_val_is_negone(__isl_keep isl_val *v)
+{
+       if (!v)
+               return -1;
+
+       return isl_int_is_neg(v->n) && isl_int_abs_eq(v->n, v->d);
+}
+
+/* Is "v" (strictly) positive?
+ */
+int isl_val_is_pos(__isl_keep isl_val *v)
+{
+       if (!v)
+               return -1;
+
+       return isl_int_is_pos(v->n);
+}
+
+/* Is "v" (strictly) negative?
+ */
+int isl_val_is_neg(__isl_keep isl_val *v)
+{
+       if (!v)
+               return -1;
+
+       return isl_int_is_neg(v->n);
+}
+
+/* Is "v" non-negative?
+ */
+int isl_val_is_nonneg(__isl_keep isl_val *v)
+{
+       if (!v)
+               return -1;
+
+       if (isl_val_is_nan(v))
+               return 0;
+
+       return isl_int_is_nonneg(v->n);
+}
+
+/* Is "v" non-positive?
+ */
+int isl_val_is_nonpos(__isl_keep isl_val *v)
+{
+       if (!v)
+               return -1;
+
+       if (isl_val_is_nan(v))
+               return 0;
+
+       return isl_int_is_nonpos(v->n);
+}
+
+/* Return the sign of "v".
+ *
+ * The sign of NaN is undefined.
+ */
+int isl_val_sgn(__isl_keep isl_val *v)
+{
+       if (!v)
+               return 0;
+       if (isl_val_is_zero(v))
+               return 0;
+       if (isl_val_is_pos(v))
+               return 1;
+       return -1;
+}
+
+/* Is "v1" (strictly) less than "v2"?
+ */
+int isl_val_lt(__isl_keep isl_val *v1, __isl_keep isl_val *v2)
+{
+       isl_int t;
+       int lt;
+
+       if (!v1 || !v2)
+               return -1;
+       if (isl_val_is_int(v1) && isl_val_is_int(v2))
+               return isl_int_lt(v1->n, v2->n);
+       if (isl_val_is_nan(v1) || isl_val_is_nan(v2))
+               return 0;
+       if (isl_val_eq(v1, v2))
+               return 0;
+       if (isl_val_is_infty(v2))
+               return 1;
+       if (isl_val_is_infty(v1))
+               return 0;
+       if (isl_val_is_neginfty(v1))
+               return 1;
+       if (isl_val_is_neginfty(v2))
+               return 0;
+
+       isl_int_init(t);
+       isl_int_mul(t, v1->n, v2->d);
+       isl_int_submul(t, v2->n, v1->d);
+       lt = isl_int_is_neg(t);
+       isl_int_clear(t);
+
+       return lt;
+}
+
+/* Is "v1" (strictly) greater than "v2"?
+ */
+int isl_val_gt(__isl_keep isl_val *v1, __isl_keep isl_val *v2)
+{
+       return isl_val_lt(v2, v1);
+}
+
+/* Is "v1" less than or equal to "v2"?
+ */
+int isl_val_le(__isl_keep isl_val *v1, __isl_keep isl_val *v2)
+{
+       isl_int t;
+       int le;
+
+       if (!v1 || !v2)
+               return -1;
+       if (isl_val_is_int(v1) && isl_val_is_int(v2))
+               return isl_int_le(v1->n, v2->n);
+       if (isl_val_is_nan(v1) || isl_val_is_nan(v2))
+               return 0;
+       if (isl_val_eq(v1, v2))
+               return 1;
+       if (isl_val_is_infty(v2))
+               return 1;
+       if (isl_val_is_infty(v1))
+               return 0;
+       if (isl_val_is_neginfty(v1))
+               return 1;
+       if (isl_val_is_neginfty(v2))
+               return 0;
+
+       isl_int_init(t);
+       isl_int_mul(t, v1->n, v2->d);
+       isl_int_submul(t, v2->n, v1->d);
+       le = isl_int_is_nonpos(t);
+       isl_int_clear(t);
+
+       return le;
+}
+
+/* Is "v1" greater than or equal to "v2"?
+ */
+int isl_val_ge(__isl_keep isl_val *v1, __isl_keep isl_val *v2)
+{
+       return isl_val_le(v2, v1);
+}
+
+/* How does "v" compare to "i"?
+ *
+ * Return 1 if v is greater, -1 if v is smaller and 0 if v is equal to i.
+ *
+ * If v is NaN (or NULL), then the result is undefined.
+ */
+int isl_val_cmp_si(__isl_keep isl_val *v, long i)
+{
+       isl_int t;
+       int cmp;
+
+       if (!v)
+               return 0;
+       if (isl_val_is_int(v))
+               return isl_int_cmp_si(v->n, i);
+       if (isl_val_is_nan(v))
+               return 0;
+       if (isl_val_is_infty(v))
+               return 1;
+       if (isl_val_is_neginfty(v))
+               return -1;
+
+       isl_int_init(t);
+       isl_int_mul_si(t, v->d, i);
+       isl_int_sub(t, v->n, t);
+       cmp = isl_int_sgn(t);
+       isl_int_clear(t);
+
+       return cmp;
+}
+
+/* Is "v1" equal to "v2"?
+ */
+int isl_val_eq(__isl_keep isl_val *v1, __isl_keep isl_val *v2)
+{
+       if (!v1 || !v2)
+               return -1;
+       if (isl_val_is_nan(v1) || isl_val_is_nan(v2))
+               return 0;
+
+       return isl_int_eq(v1->n, v2->n) && isl_int_eq(v1->d, v2->d);
+}
+
+/* Is "v1" different from "v2"?
+ */
+int isl_val_ne(__isl_keep isl_val *v1, __isl_keep isl_val *v2)
+{
+       if (!v1 || !v2)
+               return -1;
+       if (isl_val_is_nan(v1) || isl_val_is_nan(v2))
+               return 0;
+
+       return isl_int_ne(v1->n, v2->n) || isl_int_ne(v1->d, v2->d);
+}
+
+/* Print a textual representation of "v" onto "p".
+ */
+__isl_give isl_printer *isl_printer_print_val(__isl_take isl_printer *p,
+       __isl_keep isl_val *v)
+{
+       int neg;
+
+       if (!p || !v)
+               return isl_printer_free(p);
+
+       neg = isl_int_is_neg(v->n);
+       if (neg) {
+               p = isl_printer_print_str(p, "-");
+               isl_int_neg(v->n, v->n);
+       }
+       if (isl_int_is_zero(v->d)) {
+               int sgn = isl_int_sgn(v->n);
+               p = isl_printer_print_str(p, sgn < 0 ? "-infty" :
+                                           sgn == 0 ? "NaN" : "infty");
+       } else
+               p = isl_printer_print_isl_int(p, v->n);
+       if (neg)
+               isl_int_neg(v->n, v->n);
+       if (!isl_int_is_zero(v->d) && !isl_int_is_one(v->d)) {
+               p = isl_printer_print_str(p, "/");
+               p = isl_printer_print_isl_int(p, v->d);
+       }
+
+       return p;
+}
diff --git a/isl_val_private.h b/isl_val_private.h
new file mode 100644 (file)
index 0000000..92d484c
--- /dev/null
@@ -0,0 +1,30 @@
+#ifndef ISL_VAL_PRIVATE_H
+#define ISL_VAL_PRIVATE_H
+
+#include <isl/int.h>
+#include <isl/val.h>
+
+/* Represents a "value", which may be an integer value, a rational value,
+ * plus or minus infinity or "not a number".
+ *
+ * Internally, +infinity is represented as 1/0,
+ * -infinity as -1/0 and NaN as 0/0.
+ *
+ * A rational value is always normalized before it is passed to the user.
+ */
+struct isl_val {
+       int ref;
+       isl_ctx *ctx;
+
+       isl_int n;
+       isl_int d;
+};
+
+__isl_give isl_val *isl_val_alloc(isl_ctx *ctx);
+__isl_give isl_val *isl_val_normalize(__isl_take isl_val *v);
+__isl_give isl_val *isl_val_int_from_isl_int(isl_ctx *ctx, isl_int n);
+__isl_give isl_val *isl_val_rat_from_isl_int(isl_ctx *ctx,
+       isl_int n, isl_int d);
+__isl_give isl_val *isl_val_cow(__isl_take isl_val *val);
+
+#endif
diff --git a/print.c b/print.c
index b4c9d23..1aefc5f 100644 (file)
--- a/print.c
+++ b/print.c
 #include <isl/aff.h>
 #include <isl/ast.h>
 #include <isl/printer.h>
+#include <isl/val.h>
 
 #undef BASE
 #define BASE id
 #include <print_templ.c>
 #undef BASE
+#define BASE val
+#include <print_templ.c>
+#undef BASE
 #define BASE space
 #include <print_templ.c>
 #undef BASE