From 93be1535a464dae5359f46b715cde13567ffc157 Mon Sep 17 00:00:00 2001 From: Sven Verdoolaege Date: Mon, 10 May 2010 13:14:49 +0200 Subject: [PATCH] add isl_bound test application --- Makefile.am | 10 +- bound.c | 266 +++++++++++++++++++++++++++++ bound_test.sh | 32 ++++ test_inputs/basicLinear.pwqp | 1 + test_inputs/basicLinear2.pwqp | 1 + test_inputs/basicTest.pwqp | 1 + test_inputs/basicTestParameterPosNeg.pwqp | 1 + test_inputs/devos.pwqp | 1 + test_inputs/equality1.pwqp | 1 + test_inputs/equality2.pwqp | 1 + test_inputs/equality3.pwqp | 1 + test_inputs/equality4.pwqp | 1 + test_inputs/equality5.pwqp | 1 + test_inputs/faddeev.pwqp | 1 + test_inputs/linearExample.pwqp | 1 + test_inputs/neg.pwqp | 1 + test_inputs/philippe.pwqp | 1 + test_inputs/philippe3vars.pwqp | 1 + test_inputs/philippe3vars3pars.pwqp | 1 + test_inputs/philippeNeg.pwqp | 1 + test_inputs/philippePolynomialCoeff.pwqp | 1 + test_inputs/philippePolynomialCoeff1P.pwqp | 1 + test_inputs/product.pwqp | 1 + test_inputs/split.pwqp | 1 + test_inputs/test3Deg3Var.pwqp | 1 + test_inputs/toplas.pwqp | 1 + test_inputs/unexpanded.pwqp | 1 + 27 files changed, 330 insertions(+), 2 deletions(-) create mode 100644 bound.c create mode 100755 bound_test.sh create mode 100644 test_inputs/basicLinear.pwqp create mode 100644 test_inputs/basicLinear2.pwqp create mode 100644 test_inputs/basicTest.pwqp create mode 100644 test_inputs/basicTestParameterPosNeg.pwqp create mode 100644 test_inputs/devos.pwqp create mode 100644 test_inputs/equality1.pwqp create mode 100644 test_inputs/equality2.pwqp create mode 100644 test_inputs/equality3.pwqp create mode 100644 test_inputs/equality4.pwqp create mode 100644 test_inputs/equality5.pwqp create mode 100644 test_inputs/faddeev.pwqp create mode 100644 test_inputs/linearExample.pwqp create mode 100644 test_inputs/neg.pwqp create mode 100644 test_inputs/philippe.pwqp create mode 100644 test_inputs/philippe3vars.pwqp create mode 100644 test_inputs/philippe3vars3pars.pwqp create mode 100644 test_inputs/philippeNeg.pwqp create mode 100644 test_inputs/philippePolynomialCoeff.pwqp create mode 100644 test_inputs/philippePolynomialCoeff1P.pwqp create mode 100644 test_inputs/product.pwqp create mode 100644 test_inputs/split.pwqp create mode 100644 test_inputs/test3Deg3Var.pwqp create mode 100644 test_inputs/toplas.pwqp create mode 100644 test_inputs/unexpanded.pwqp diff --git a/Makefile.am b/Makefile.am index c70f33e..7188ccf 100644 --- a/Makefile.am +++ b/Makefile.am @@ -7,8 +7,8 @@ lib_LTLIBRARIES = libisl.la noinst_PROGRAMS = isl_test isl_polyhedron_sample isl_pip \ isl_polyhedron_minimize isl_polytope_scan \ isl_polyhedron_detect_equalities isl_cat \ - isl_closure -TESTS = isl_test pip_test.sh + isl_closure isl_bound +TESTS = isl_test pip_test.sh bound_test.sh if HAVE_PIPLIB ISL_PIPLIB = \ @@ -116,6 +116,12 @@ isl_pip_LDADD = libisl.la isl_pip_SOURCES = \ pip.c +isl_bound_CPPFLAGS = -I$(srcdir)/include -Iinclude/ \ + @GMP_CPPFLAGS@ +isl_bound_LDADD = libisl.la +isl_bound_SOURCES = \ + bound.c + isl_polyhedron_minimize_CPPFLAGS = -I$(srcdir)/include -Iinclude/ \ @GMP_CPPFLAGS@ isl_polyhedron_minimize_LDADD = libisl.la diff --git a/bound.c b/bound.c new file mode 100644 index 0000000..327705c --- /dev/null +++ b/bound.c @@ -0,0 +1,266 @@ +#include +#include +#include +#include + +struct bound_options { + struct isl_options *isl; + unsigned verify; + int print_all; + int continue_on_error; +}; + +struct isl_arg bound_options_arg[] = { +ISL_ARG_CHILD(struct bound_options, isl, "isl", isl_options_arg) +ISL_ARG_BOOL(struct bound_options, verify, 'T', "verify", 0) +ISL_ARG_BOOL(struct bound_options, print_all, 'A', "print-all", 0) +ISL_ARG_BOOL(struct bound_options, continue_on_error, '\0', "continue-on-error", 0) +ISL_ARG_END +}; + +ISL_ARG_DEF(bound_options, struct bound_options, bound_options_arg) + +static __isl_give isl_set *set_bounds(__isl_take isl_set *set) +{ + unsigned nparam; + int i, r; + isl_point *pt, *pt2; + isl_set *box; + + nparam = isl_set_dim(set, isl_dim_param); + r = nparam >= 8 ? 5 : nparam >= 5 ? 15 : 50; + + pt = isl_set_sample_point(isl_set_copy(set)); + pt2 = isl_point_copy(pt); + + for (i = 0; i < nparam; ++i) { + pt = isl_point_add_ui(pt, isl_dim_param, i, r); + pt2 = isl_point_sub_ui(pt2, isl_dim_param, i, r); + } + + box = isl_set_box_from_points(pt, pt2); + + return isl_set_intersect(set, box); +} + +struct verify_point_bound { + struct bound_options *options; + int stride; + int n; + int exact; + int error; + + isl_pw_qpolynomial *pwqp; + isl_pw_qpolynomial_fold *pwf; +}; + +static int verify_point(__isl_take isl_point *pnt, void *user) +{ + int i; + unsigned nparam; + struct verify_point_bound *vpb = (struct verify_point_bound *) user; + isl_int t; + isl_pw_qpolynomial *pwqp; + isl_qpolynomial *bound = NULL; + isl_qpolynomial *opt = NULL; + isl_set *dom = NULL; + const char *minmax; + int bounded; + int sign; + int ok; + int cst; + FILE *out = vpb->options->print_all ? stdout : stderr; + + vpb->n--; + + if (1) { + minmax = "ub"; + sign = 1; + } else { + minmax = "lb"; + sign = -1; + } + + isl_int_init(t); + + pwqp = isl_pw_qpolynomial_copy(vpb->pwqp); + + nparam = isl_pw_qpolynomial_dim(pwqp, isl_dim_param); + for (i = 0; i < nparam; ++i) { + isl_point_get_coordinate(pnt, isl_dim_param, i, &t); + pwqp = isl_pw_qpolynomial_fix_dim(pwqp, isl_dim_param, i, t); + } + + bound = isl_pw_qpolynomial_fold_eval(isl_pw_qpolynomial_fold_copy(vpb->pwf), + isl_point_copy(pnt)); + + dom = isl_pw_qpolynomial_domain(isl_pw_qpolynomial_copy(pwqp)); + bounded = isl_set_is_bounded(dom); + + if (bounded < 0) + goto error; + + if (!bounded) + opt = isl_pw_qpolynomial_eval(isl_pw_qpolynomial_copy(pwqp), + isl_set_sample_point(isl_set_copy(dom))); + else if (sign > 0) + opt = isl_pw_qpolynomial_max(isl_pw_qpolynomial_copy(pwqp)); + else + opt = isl_pw_qpolynomial_min(isl_pw_qpolynomial_copy(pwqp)); + + if (vpb->exact && bounded) + ok = isl_qpolynomial_is_equal(opt, bound); + else if (sign > 0) + ok = isl_qpolynomial_le_cst(opt, bound); + else + ok = isl_qpolynomial_le_cst(bound, opt); + if (ok < 0) + goto error; + + if (vpb->options->print_all || !ok) { + fprintf(out, "%s(", minmax); + for (i = 0; i < nparam; ++i) { + if (i) + fprintf(out, ", "); + isl_point_get_coordinate(pnt, isl_dim_param, i, &t); + isl_int_print(out, t, 0); + } + fprintf(out, ") = "); + isl_qpolynomial_print(bound, out, ISL_FORMAT_ISL); + fprintf(out, ", %s = ", bounded ? "opt" : "sample"); + isl_qpolynomial_print(opt, out, ISL_FORMAT_ISL); + if (ok) + fprintf(out, ". OK\n"); + else + fprintf(out, ". NOT OK\n"); + } else if ((vpb->n % vpb->stride) == 0) { + printf("o"); + fflush(stdout); + } + + if (0) { +error: + ok = 0; + } + + isl_pw_qpolynomial_free(pwqp); + isl_qpolynomial_free(bound); + isl_qpolynomial_free(opt); + isl_point_free(pnt); + isl_set_free(dom); + + isl_int_clear(t); + + if (!ok) + vpb->error = 1; + + if (vpb->options->continue_on_error) + ok = 1; + + return (vpb->n >= 1 && ok) ? 0 : -1; +} + +static int check_solution(__isl_take isl_pw_qpolynomial *pwqp, + __isl_take isl_pw_qpolynomial_fold *pwf, int exact, + struct bound_options *options) +{ + struct verify_point_bound vpb; + isl_int count, max; + isl_set *dom; + isl_set *context; + int i, r, n; + + dom = isl_pw_qpolynomial_domain(isl_pw_qpolynomial_copy(pwqp)); + context = isl_set_remove(isl_set_copy(dom), isl_dim_set, + 0, isl_set_dim(dom, isl_dim_set)); + context = isl_set_remove_divs(context); + context = set_bounds(context); + + isl_int_init(count); + isl_int_init(max); + + isl_int_set_si(max, 200); + r = isl_set_count_upto(context, max, &count); + assert(r >= 0); + n = isl_int_get_si(count); + + isl_int_clear(max); + isl_int_clear(count); + + vpb.options = options; + vpb.pwqp = pwqp; + vpb.pwf = pwf; + vpb.n = n; + vpb.stride = n > 70 ? 1 + (n + 1)/70 : 1; + vpb.error = 0; + vpb.exact = exact; + + if (!options->print_all) { + for (i = 0; i < vpb.n; i += vpb.stride) + printf("."); + printf("\r"); + fflush(stdout); + } + + isl_set_foreach_point(context, verify_point, &vpb); + + isl_set_free(context); + isl_set_free(dom); + isl_pw_qpolynomial_free(pwqp); + isl_pw_qpolynomial_fold_free(pwf); + + if (!options->print_all) + printf("\n"); + + if (vpb.error) { + fprintf(stderr, "Check failed !\n"); + return -1; + } + + return 0; +} + +int main(int argc, char **argv) +{ + isl_ctx *ctx; + isl_pw_qpolynomial *pwqp; + isl_pw_qpolynomial *copy; + isl_pw_qpolynomial_fold *pwf; + struct isl_stream *s; + struct bound_options *options; + int exact; + int r = 0; + + options = bound_options_new_with_defaults(); + assert(options); + argc = bound_options_parse(options, argc, argv, ISL_ARG_ALL); + + ctx = isl_ctx_alloc_with_options(options->isl); + options->isl = NULL; + + s = isl_stream_new_file(ctx, stdin); + pwqp = isl_stream_read_pw_qpolynomial(s); + + if (options->verify) + copy = isl_pw_qpolynomial_copy(pwqp); + + pwf = isl_pw_qpolynomial_bound_range(pwqp, isl_fold_max, &exact); + pwf = isl_pw_qpolynomial_fold_coalesce(pwf); + + if (options->verify) { + r = check_solution(copy, pwf, exact, options); + } else { + if (!exact) + printf("# NOT exact\n"); + isl_pw_qpolynomial_fold_print(pwf, stdout, 0); + fprintf(stdout, "\n"); + isl_pw_qpolynomial_fold_free(pwf); + } + + isl_stream_free(s); + + isl_ctx_free(ctx); + free(options); + + return r; +} diff --git a/bound_test.sh b/bound_test.sh new file mode 100755 index 0000000..28f27e7 --- /dev/null +++ b/bound_test.sh @@ -0,0 +1,32 @@ +#!/bin/sh + +BOUND_TESTS="\ + basicLinear2.pwqp \ + basicLinear.pwqp \ + basicTestParameterPosNeg.pwqp \ + basicTest.pwqp \ + devos.pwqp \ + equality1.pwqp \ + equality2.pwqp \ + equality3.pwqp \ + equality4.pwqp \ + equality5.pwqp \ + faddeev.pwqp \ + linearExample.pwqp \ + neg.pwqp \ + philippe3vars3pars.pwqp \ + philippe3vars.pwqp \ + philippeNeg.pwqp \ + philippePolynomialCoeff1P.pwqp \ + philippePolynomialCoeff.pwqp \ + philippe.pwqp \ + product.pwqp \ + split.pwqp \ + test3Deg3Var.pwqp \ + toplas.pwqp \ + unexpanded.pwqp" + +for i in $BOUND_TESTS; do + echo $i; + ./isl_bound$EXEEXT -T < $srcdir/test_inputs/$i || exit +done diff --git a/test_inputs/basicLinear.pwqp b/test_inputs/basicLinear.pwqp new file mode 100644 index 0000000..0af7fab --- /dev/null +++ b/test_inputs/basicLinear.pwqp @@ -0,0 +1 @@ +[P, Q] -> { [n, m] -> n : n >= 1 and m >= n and m <= P and m <= Q } diff --git a/test_inputs/basicLinear2.pwqp b/test_inputs/basicLinear2.pwqp new file mode 100644 index 0000000..d411a36 --- /dev/null +++ b/test_inputs/basicLinear2.pwqp @@ -0,0 +1 @@ +[P, Q] -> { [n, m] -> n : n >= 1 and m >= n and m <= P and n >= -1 + Q } diff --git a/test_inputs/basicTest.pwqp b/test_inputs/basicTest.pwqp new file mode 100644 index 0000000..52e7fc8 --- /dev/null +++ b/test_inputs/basicTest.pwqp @@ -0,0 +1 @@ +[p] -> { [n, m] -> (n + n^2) : n >= 1 and m >= n and m <= p } diff --git a/test_inputs/basicTestParameterPosNeg.pwqp b/test_inputs/basicTestParameterPosNeg.pwqp new file mode 100644 index 0000000..6cb4490 --- /dev/null +++ b/test_inputs/basicTestParameterPosNeg.pwqp @@ -0,0 +1 @@ +[p] -> { [n, m] -> (n + n^3) : n >= -1 and m >= n and m <= p } diff --git a/test_inputs/devos.pwqp b/test_inputs/devos.pwqp new file mode 100644 index 0000000..b452544 --- /dev/null +++ b/test_inputs/devos.pwqp @@ -0,0 +1 @@ +[U] -> { [i0] -> ((1/3 * U + 2/3 * i0) - [(U + 2i0)/3]) : 2i0 >= -3 - U and 2i0 <= -U and U >= 0 and U <= 10 } diff --git a/test_inputs/equality1.pwqp b/test_inputs/equality1.pwqp new file mode 100644 index 0000000..eb16a4b --- /dev/null +++ b/test_inputs/equality1.pwqp @@ -0,0 +1 @@ +[n] -> { [x] -> 1 + [(x+1)/3] : exists a : x = 3a +1 && 0 <= x <= n } diff --git a/test_inputs/equality2.pwqp b/test_inputs/equality2.pwqp new file mode 100644 index 0000000..1629a65 --- /dev/null +++ b/test_inputs/equality2.pwqp @@ -0,0 +1 @@ +[n] -> { [x,y] -> x^2 * y : n = 2x + 4y and 0 <= x,y <= 10 } diff --git a/test_inputs/equality3.pwqp b/test_inputs/equality3.pwqp new file mode 100644 index 0000000..c6f8c3a --- /dev/null +++ b/test_inputs/equality3.pwqp @@ -0,0 +1 @@ +[m,n] -> { [x,y] -> x^2 * y : n = 2x + 4y and 0 <= x,y <= 10 and 3 n = 5 m } diff --git a/test_inputs/equality4.pwqp b/test_inputs/equality4.pwqp new file mode 100644 index 0000000..49da2e7 --- /dev/null +++ b/test_inputs/equality4.pwqp @@ -0,0 +1 @@ +[m,n] -> { [x,y] -> x^2 * y + m + 13 * n: n = 2x + 4y and 0 <= x,y <= 10 and 3 n = 5 m } diff --git a/test_inputs/equality5.pwqp b/test_inputs/equality5.pwqp new file mode 100644 index 0000000..09cb752 --- /dev/null +++ b/test_inputs/equality5.pwqp @@ -0,0 +1 @@ +[m,n] -> { [x,y,z] -> x^2 * y + z + m + 13 * n: n = 2x + 4y and 0 <= x,y <= 10 and 3 n = 5 m and z = x + y } diff --git a/test_inputs/faddeev.pwqp b/test_inputs/faddeev.pwqp new file mode 100644 index 0000000..e7db61d --- /dev/null +++ b/test_inputs/faddeev.pwqp @@ -0,0 +1 @@ +[N] -> { [i, j, k] -> (((4 + 6 * N + 2 * N^2) + (-2 - 2 * N) * j) + ((-2 - N) + j) * k) : j = 1 + i and k = 1 + i and i >= 3 and N <= 100 and i <= N and N >= 10 } diff --git a/test_inputs/linearExample.pwqp b/test_inputs/linearExample.pwqp new file mode 100644 index 0000000..24c5394 --- /dev/null +++ b/test_inputs/linearExample.pwqp @@ -0,0 +1 @@ +[N, M, L] -> { [i, j, k] -> ((1/2 * i + 5 * j) + 1/7 * k) : i >= 0 and k >= -N + i and k >= -M - j and j <= L + i and L >= 0 and L >= -M } diff --git a/test_inputs/neg.pwqp b/test_inputs/neg.pwqp new file mode 100644 index 0000000..596a7d7 --- /dev/null +++ b/test_inputs/neg.pwqp @@ -0,0 +1 @@ +[n] -> { [i0] -> i0^2 : i0 >= -20 - n and i0 <= n and i0 <= -1 and n >= 0 } diff --git a/test_inputs/philippe.pwqp b/test_inputs/philippe.pwqp new file mode 100644 index 0000000..1c56e7a --- /dev/null +++ b/test_inputs/philippe.pwqp @@ -0,0 +1 @@ +[N] -> { [i, j] -> ((1/2 * i + 1/2 * i^2) + j) : i <= N and j >= 0 and j <= i } diff --git a/test_inputs/philippe3vars.pwqp b/test_inputs/philippe3vars.pwqp new file mode 100644 index 0000000..8d07496 --- /dev/null +++ b/test_inputs/philippe3vars.pwqp @@ -0,0 +1 @@ +[N] -> { [i, j, k] -> (((1/2 * i + 1/2 * i^2) + j) + k^3) : i >= 0 and k >= -N + i and k >= -j and j <= i } diff --git a/test_inputs/philippe3vars3pars.pwqp b/test_inputs/philippe3vars3pars.pwqp new file mode 100644 index 0000000..f81b8cc --- /dev/null +++ b/test_inputs/philippe3vars3pars.pwqp @@ -0,0 +1 @@ +[N, M, L] -> { [i, j, k] -> (((1/2 * i + 1/2 * i^2) + j) + k^3) : i >= 0 and k >= -N + i and k >= -M - j and j <= L + i and L >= 0 and L >= -M } diff --git a/test_inputs/philippeNeg.pwqp b/test_inputs/philippeNeg.pwqp new file mode 100644 index 0000000..24dc805 --- /dev/null +++ b/test_inputs/philippeNeg.pwqp @@ -0,0 +1 @@ +[N] -> { [i, j] -> ((1/2 * i + 1/2 * i^2) + j) : i <= N and j >= -1 and j <= i } diff --git a/test_inputs/philippePolynomialCoeff.pwqp b/test_inputs/philippePolynomialCoeff.pwqp new file mode 100644 index 0000000..e6327c7 --- /dev/null +++ b/test_inputs/philippePolynomialCoeff.pwqp @@ -0,0 +1 @@ +[N, M] -> { [i, j] -> ((N * i + (1/5 * N + N^2) * i^2) + 5 * j) : i <= N and j >= 0 and j <= i and M >= 0 } diff --git a/test_inputs/philippePolynomialCoeff1P.pwqp b/test_inputs/philippePolynomialCoeff1P.pwqp new file mode 100644 index 0000000..ae01d2f --- /dev/null +++ b/test_inputs/philippePolynomialCoeff1P.pwqp @@ -0,0 +1 @@ +[N] -> { [i, j] -> ((N * i + (1/5 * N + N^2) * i^2) + 5 * j) : i <= N and j >= 0 and j <= i } diff --git a/test_inputs/product.pwqp b/test_inputs/product.pwqp new file mode 100644 index 0000000..ee48b85 --- /dev/null +++ b/test_inputs/product.pwqp @@ -0,0 +1 @@ +[N] -> { [i0, i1, i2] -> (i0^3 * i1^2 + N * i1 * i2) : i0 >= 0 and i0 <= N and i1 >= 0 and i1 <= N and i2 >= 0 and i2 <= N } diff --git a/test_inputs/split.pwqp b/test_inputs/split.pwqp new file mode 100644 index 0000000..1804563 --- /dev/null +++ b/test_inputs/split.pwqp @@ -0,0 +1 @@ +[n] -> { [x] -> -1 + [(x+5)/7] : -n - 20 <= x <= n } diff --git a/test_inputs/test3Deg3Var.pwqp b/test_inputs/test3Deg3Var.pwqp new file mode 100644 index 0000000..d9a9ea9 --- /dev/null +++ b/test_inputs/test3Deg3Var.pwqp @@ -0,0 +1 @@ +[p] -> { [n, m] -> (n + n^3) : n >= 1 and m >= n and m <= p } diff --git a/test_inputs/toplas.pwqp b/test_inputs/toplas.pwqp new file mode 100644 index 0000000..9c09995 --- /dev/null +++ b/test_inputs/toplas.pwqp @@ -0,0 +1 @@ +[n] -> { [i0, i1] -> (((4 * n - n^2) + (-3/2 + 2 * n) * i0 - 1/2 * i0^2) - i1) : i1 >= -1 + 3n - i0 and i1 >= -1 + 2n - i0 and i0 >= 0 and i1 <= -2 + 4n - i0 and i0 <= -2 + 4n and i0 <= -1 + 3n and i1 >= 0 and i1 <= -1 + n } diff --git a/test_inputs/unexpanded.pwqp b/test_inputs/unexpanded.pwqp new file mode 100644 index 0000000..5626d3b --- /dev/null +++ b/test_inputs/unexpanded.pwqp @@ -0,0 +1 @@ +{ [x, y] -> ((x - x^2) * y + (-x + x^2) * y^2) : x >= 0 and x <= 2 and y >= 0 and y <= 2 } -- 2.7.4