test_approx.c

   1 #include <assert.h>
   2 #include <ctype.h>
   3 #include <limits.h>
   4 #include <stdlib.h>
   5 #include <barvinok/barvinok.h>
   6 #include "verify.h"
   7 #include "config.h"
   8
   9 #ifdef HAVE_SYS_TIMES_H
  10
  11 #include <sys/times.h>
  12
  13 typedef clock_t         my_clock_t;
  14
  15 static my_clock_t time_diff(struct tms *before, struct tms *after)
  16 {
  17         return after->tms_utime - before->tms_utime;
  18 }
  19
  20 #else
  21
  22 typedef int             my_clock_t;
  23
  24 struct tms { int dummy; };
  25 static void times(struct tms* time)
  26 {
  27 }
  28 static my_clock_t time_diff(struct tms *before, struct tms *after)
  29 {
  30         return 0;
  31 }
  32
  33 #endif
  34
  35 struct {
  36     int     sign;
  37     int     method;
  38     int     flags;
  39 } methods[] = {
  40 { BV_APPROX_SIGN_NONE,      BV_APPROX_NONE,     0 },
  41 { BV_APPROX_SIGN_APPROX,    BV_APPROX_BERNOULLI,        0 },
  42 { BV_APPROX_SIGN_APPROX,    BV_APPROX_DROP,     0 },
  43 { BV_APPROX_SIGN_APPROX,    BV_APPROX_VOLUME,   BV_VOL_LIFT },
  44 { BV_APPROX_SIGN_APPROX,    BV_APPROX_VOLUME,   BV_VOL_VERTEX },
  45 { BV_APPROX_SIGN_APPROX,    BV_APPROX_VOLUME,   BV_VOL_BARYCENTER },
  46 { BV_APPROX_SIGN_APPROX,    BV_APPROX_SCALE,    0 },
  47 { BV_APPROX_SIGN_APPROX,    BV_APPROX_SCALE,    BV_APPROX_SCALE_CHAMBER },
  48 { BV_APPROX_SIGN_APPROX,    BV_APPROX_SCALE,    BV_APPROX_SCALE_FAST },
  49 { BV_APPROX_SIGN_APPROX,    BV_APPROX_SCALE,    BV_APPROX_SCALE_FAST | BV_APPROX_SCALE_CHAMBER },
  50 { BV_APPROX_SIGN_LOWER,     BV_APPROX_DROP,     0 },
  51 { BV_APPROX_SIGN_LOWER,     BV_APPROX_VOLUME,   BV_VOL_LIFT },
  52 { BV_APPROX_SIGN_LOWER,     BV_APPROX_VOLUME,   BV_VOL_VERTEX },
  53 { BV_APPROX_SIGN_LOWER,     BV_APPROX_VOLUME,   BV_VOL_BARYCENTER },
  54 { BV_APPROX_SIGN_LOWER,     BV_APPROX_SCALE,    0 },
  55 { BV_APPROX_SIGN_LOWER,     BV_APPROX_SCALE,    BV_APPROX_SCALE_CHAMBER },
  56 { BV_APPROX_SIGN_LOWER,     BV_APPROX_SCALE,    BV_APPROX_SCALE_FAST },
  57 { BV_APPROX_SIGN_LOWER,     BV_APPROX_SCALE,    BV_APPROX_SCALE_FAST | BV_APPROX_SCALE_CHAMBER },
  58 { BV_APPROX_SIGN_LOWER,     BV_APPROX_SCALE,    BV_APPROX_SCALE_NARROW },
  59 { BV_APPROX_SIGN_LOWER,     BV_APPROX_SCALE,    BV_APPROX_SCALE_NARROW  | BV_APPROX_SCALE_CHAMBER},
  60 { BV_APPROX_SIGN_LOWER,     BV_APPROX_SCALE,    BV_APPROX_SCALE_FAST | BV_APPROX_SCALE_NARROW },
  61 { BV_APPROX_SIGN_LOWER,     BV_APPROX_SCALE,    BV_APPROX_SCALE_FAST | BV_APPROX_SCALE_NARROW | BV_APPROX_SCALE_CHAMBER },
  62 { BV_APPROX_SIGN_LOWER,     BV_APPROX_SCALE,    BV_APPROX_SCALE_NARROW2 },
  63 { BV_APPROX_SIGN_LOWER,     BV_APPROX_SCALE,    BV_APPROX_SCALE_NARROW2 | BV_APPROX_SCALE_CHAMBER },
  64 { BV_APPROX_SIGN_LOWER,     BV_APPROX_SCALE,    BV_APPROX_SCALE_FAST | BV_APPROX_SCALE_NARROW2 },
  65 { BV_APPROX_SIGN_LOWER,     BV_APPROX_SCALE,    BV_APPROX_SCALE_FAST | BV_APPROX_SCALE_NARROW2 | BV_APPROX_SCALE_CHAMBER },
  66 { BV_APPROX_SIGN_UPPER,     BV_APPROX_DROP,     0 },
  67 { BV_APPROX_SIGN_UPPER,     BV_APPROX_VOLUME,   BV_VOL_LIFT },
  68 { BV_APPROX_SIGN_UPPER,     BV_APPROX_VOLUME,   BV_VOL_VERTEX },
  69 { BV_APPROX_SIGN_UPPER,     BV_APPROX_VOLUME,   BV_VOL_BARYCENTER },
  70 { BV_APPROX_SIGN_UPPER,     BV_APPROX_SCALE,    0 },
  71 { BV_APPROX_SIGN_UPPER,     BV_APPROX_SCALE,    BV_APPROX_SCALE_CHAMBER },
  72 { BV_APPROX_SIGN_UPPER,     BV_APPROX_SCALE,    BV_APPROX_SCALE_FAST },
  73 { BV_APPROX_SIGN_UPPER,     BV_APPROX_SCALE,    BV_APPROX_SCALE_FAST | BV_APPROX_SCALE_CHAMBER },
  74 { BV_APPROX_SIGN_UPPER,     BV_APPROX_SCALE,    BV_APPROX_SCALE_NARROW },
  75 { BV_APPROX_SIGN_UPPER,     BV_APPROX_SCALE,    BV_APPROX_SCALE_NARROW | BV_APPROX_SCALE_CHAMBER },
  76 { BV_APPROX_SIGN_UPPER,     BV_APPROX_SCALE,    BV_APPROX_SCALE_FAST | BV_APPROX_SCALE_NARROW },
  77 { BV_APPROX_SIGN_UPPER,     BV_APPROX_SCALE,    BV_APPROX_SCALE_FAST | BV_APPROX_SCALE_NARROW | BV_APPROX_SCALE_CHAMBER },
  78 { BV_APPROX_SIGN_UPPER,     BV_APPROX_SCALE,    BV_APPROX_SCALE_NARROW2 },
  79 { BV_APPROX_SIGN_UPPER,     BV_APPROX_SCALE,    BV_APPROX_SCALE_NARROW2 | BV_APPROX_SCALE_CHAMBER },
  80 { BV_APPROX_SIGN_UPPER,     BV_APPROX_SCALE,    BV_APPROX_SCALE_FAST | BV_APPROX_SCALE_NARROW2 },
  81 { BV_APPROX_SIGN_UPPER,     BV_APPROX_SCALE,    BV_APPROX_SCALE_FAST | BV_APPROX_SCALE_NARROW2 | BV_APPROX_SCALE_CHAMBER },
  82 };
  83
  84 #define nr_methods (sizeof(methods)/sizeof(*methods))
  85
  86 struct options {
  87     int quiet;
  88     struct verify_options    *verify;
  89 };
  90
  91 ISL_ARGS_START(struct options, options_args)
  92 ISL_ARG_CHILD(struct options, verify, NULL, &verify_options_args, NULL)
  93 ISL_ARG_BOOL(struct options, quiet, 'q', "quiet", 0, NULL)
  94 ISL_ARGS_END
  95
  96 ISL_ARG_DEF(options, struct options, options_args)
  97
  98 struct result_data {
  99     Value                   n;
 100     double                  RE_sum[nr_methods];
 101
 102     my_clock_t              ticks[nr_methods];
 103     size_t                  size[nr_methods];
 104 };
 105
 106 void result_data_init(struct result_data *result)
 107 {
 108     int i;
 109     for (i = 0; i < nr_methods; ++i) {
 110         result->RE_sum[i] = 0;
 111         result->ticks[i] = 0;
 112         result->size[i] = 0;
 113     }
 114     value_init(result->n);
 115 }
 116
 117 void result_data_clear(struct result_data *result)
 118 {
 119     int i;
 120     value_clear(result->n);
 121 }
 122
 123 void result_data_print(struct result_data *result, int n)
 124 {
 125     int i;
 126
 127     fprintf(stderr, "%g", (double)result->ticks[0]/n);
 128     for (i = 1; i < nr_methods; ++i)
 129         fprintf(stderr, ", %g", (double)result->ticks[i]/n);
 130     fprintf(stderr, "\n");
 131
 132     fprintf(stderr, "%zd", result->size[0]/n);
 133     for (i = 1; i < nr_methods; ++i)
 134         fprintf(stderr, ", %zd", result->size[i]/n);
 135     fprintf(stderr, "\n");
 136
 137     fprintf(stderr, "%g\n", VALUE_TO_DOUBLE(result->n));
 138     fprintf(stderr, "%g", result->RE_sum[0]/VALUE_TO_DOUBLE(result->n));
 139     for (i = 1; i < nr_methods; ++i)
 140         fprintf(stderr, ", %g", result->RE_sum[i]/VALUE_TO_DOUBLE(result->n));
 141     fprintf(stderr, "\n");
 142 }
 143
 144 struct test_approx_data {
 145     struct verify_point_data vpd;
 146     isl_pw_qpolynomial      **pwqp;
 147     struct result_data      *result;
 148 };
 149
 150 static __isl_give isl_val *eval(__isl_keep isl_pw_qpolynomial *pwqp,
 151         __isl_keep isl_point *pnt, int sign)
 152 {
 153     isl_val *res;
 154
 155     pwqp = isl_pw_qpolynomial_copy(pwqp);
 156     res = isl_pw_qpolynomial_eval(pwqp, isl_point_copy(pnt));
 157     if (sign == BV_APPROX_SIGN_LOWER)
 158         res = isl_val_ceil(res);
 159     else if (sign == BV_APPROX_SIGN_UPPER)
 160         res = isl_val_floor(res);
 161     else if (sign == BV_APPROX_SIGN_APPROX)
 162         res = isl_val_trunc(res);
 163     else
 164         assert(isl_val_is_int(res));
 165
 166     return res;
 167 }
 168
 169 static int test_approx(__isl_take isl_point *pnt, void *user)
 170 {
 171     struct test_approx_data *ta_data = (struct test_approx_data *) user;
 172     isl_val *exact, *approx;
 173     int i;
 174
 175     ta_data->vpd.n--;
 176
 177     exact = eval(ta_data->pwqp[0], pnt, BV_APPROX_SIGN_NONE);
 178
 179     value_increment(ta_data->result->n, ta_data->result->n);
 180     for (i = 1; i < nr_methods; ++i) {
 181         double error;
 182         approx = eval(ta_data->pwqp[i], pnt, methods[i].sign);
 183         if (methods[i].sign == BV_APPROX_SIGN_LOWER)
 184             assert(isl_val_le(approx, exact));
 185         if (methods[i].sign == BV_APPROX_SIGN_UPPER)
 186             assert(isl_val_ge(approx, exact));
 187         approx = isl_val_sub(approx, isl_val_copy(exact));
 188         if (isl_val_is_zero(exact))
 189             error = abs(isl_val_get_d(approx));
 190         else
 191             error = abs(isl_val_get_d(approx)) / isl_val_get_d(exact);
 192         isl_val_free(approx);
 193         ta_data->result->RE_sum[i] += error;
 194     }
 195
 196     if (!ta_data->vpd.options->print_all &&
 197         (ta_data->vpd.n % ta_data->vpd.s) == 0) {
 198             printf("o");
 199             fflush(stdout);
 200     }
 201
 202     isl_val_free(exact);
 203     isl_point_free(pnt);
 204
 205     return (ta_data->vpd.n >= 1) ? 0 : -1;
 206 }
 207
 208 static int test(__isl_keep isl_set *context,
 209         __isl_keep isl_pw_qpolynomial **pwqp, struct result_data *result,
 210         struct verify_options *options)
 211 {
 212         struct test_approx_data data = { { options } };
 213         int r;
 214
 215         r = verify_point_data_init(&data.vpd, context);
 216
 217         data.pwqp = pwqp;
 218         data.result = result;
 219         if (r == 0)
 220                 isl_set_foreach_point(context, &test_approx, &data);
 221         if (data.vpd.error)
 222                 r = -1;
 223
 224         verify_point_data_fini(&data.vpd);
 225
 226         return r;
 227 }
 228
 229 /* Turn the set dimensions of "context" into parameters and return
 230  * the corresponding parameter domain.
 231  */
 232 static __isl_give isl_set *to_parameter_domain(__isl_take isl_set *context)
 233 {
 234         context = isl_set_move_dims(context, isl_dim_param, 0, isl_dim_set, 0,
 235                                        isl_set_dim(context, isl_dim_set));
 236         return isl_set_params(context);
 237 }
 238
 239 static int handle(isl_ctx *ctx, FILE *in, struct result_data *result,
 240         struct verify_options *options)
 241 {
 242     int i;
 243     int r;
 244     int nparam;
 245     isl_space *space;
 246     isl_set *set;
 247     isl_set *context;
 248     isl_pw_qpolynomial *pwqp[nr_methods];
 249
 250     set = isl_set_read_from_file(ctx, in);
 251     context = isl_set_read_from_file(ctx, in);
 252
 253     context = to_parameter_domain(context);
 254     nparam = isl_set_dim(context, isl_dim_param);
 255     if (nparam != isl_set_dim(set, isl_dim_param)) {
 256             int dim = isl_set_dim(set, isl_dim_set);
 257             set = isl_set_move_dims(set, isl_dim_param, 0,
 258                                         isl_dim_set, dim - nparam, nparam);
 259     }
 260
 261     set = isl_set_intersect_params(set, context);
 262     context = isl_set_params(isl_set_copy(set));
 263     space = isl_set_get_space(context);
 264
 265     context = verify_context_set_bounds(context, options);
 266
 267     for (i = 0; i < nr_methods; ++i) {
 268         struct tms st_cpu;
 269         struct tms en_cpu;
 270         options->barvinok->approx->approximation = methods[i].sign;
 271         options->barvinok->approx->method = methods[i].method;
 272         if (methods[i].method == BV_APPROX_SCALE)
 273             options->barvinok->approx->scale_flags = methods[i].flags;
 274         else if (methods[i].method == BV_APPROX_VOLUME)
 275             options->barvinok->approx->volume_triangulate = methods[i].flags;
 276
 277         times(&st_cpu);
 278         pwqp[i] = isl_set_card(isl_set_copy(set));
 279         times(&en_cpu);
 280         result->ticks[i] = time_diff(&en_cpu, &st_cpu);
 281     }
 282     for (i = 0; i < nr_methods; ++i)
 283         result->size[i] = 0;
 284     r = test(context, pwqp, result, options);
 285     for (i = 0; i < nr_methods; ++i)
 286         isl_pw_qpolynomial_free(pwqp[i]);
 287
 288     isl_space_free(space);
 289     isl_set_free(context);
 290     isl_set_free(set);
 291
 292     return r;
 293 }
 294
 295 int main(int argc, char **argv)
 296 {
 297     isl_ctx *ctx;
 298     char path[PATH_MAX+1];
 299     struct result_data all_result;
 300     int n = 0;
 301     int r = EXIT_SUCCESS;
 302     struct options *options = options_new_with_defaults();
 303
 304     argc = options_parse(options, argc, argv, ISL_ARG_ALL);
 305     ctx = isl_ctx_alloc_with_options(&options_args, options);
 306
 307     if (options->verify->M == INT_MIN)
 308         options->verify->M = 100;
 309     if (options->verify->m == INT_MAX)
 310         options->verify->m = -100;
 311
 312     result_data_init(&all_result);
 313
 314     while (fgets(path, sizeof(path), stdin)) {
 315         struct result_data result;
 316         FILE *in;
 317         int i;
 318
 319         ++n;
 320         result_data_init(&result);
 321         fprintf(stderr, "%s", path);
 322         *strchr(path, '\n') = '\0';
 323         in = fopen(path, "r");
 324         assert(in);
 325         if (handle(ctx, in, &result, options->verify) < 0)
 326             r = EXIT_FAILURE;
 327         fclose(in);
 328
 329         if (!options->quiet)
 330             result_data_print(&result, 1);
 331
 332         value_addto(all_result.n, all_result.n, result.n);
 333         for (i = 0; i < nr_methods; ++i) {
 334             all_result.RE_sum[i] += result.RE_sum[i];
 335             all_result.ticks[i] += result.ticks[i];
 336             all_result.size[i] += result.size[i];
 337         }
 338
 339         result_data_clear(&result);
 340
 341         if (!options->quiet) {
 342             fprintf(stderr, "average\n");
 343             result_data_print(&all_result, n);
 344         }
 345     }
 346
 347     result_data_clear(&all_result);
 348
 349     isl_ctx_free(ctx);
 350
 351     return r;
 352 }