barvinok_summate.c

   1 #include <assert.h>
   2 #include <isl/ctx.h>
   3 #include <isl/val.h>
   4 #include <isl/space.h>
   5 #include <isl/point.h>
   6 #include <isl/set.h>
   7 #include <isl/polynomial.h>
   8 #include <isl/stream.h>
   9 #include <isl/printer.h>
  10 #include <barvinok/isl.h>
  11 #include <barvinok/options.h>
  12 #include <barvinok/util.h>
  13 #include "verify.h"
  14
  15 struct options {
  16         struct verify_options    *verify;
  17 };
  18
  19 ISL_ARGS_START(struct options, options_args)
  20 ISL_ARG_CHILD(struct options, verify, NULL,
  21         &verify_options_args, "verification")
  22 ISL_ARGS_END
  23
  24 ISL_ARG_DEF(options, struct options, options_args)
  25
  26 struct verify_point_sum {
  27         struct verify_point_data vpd;
  28         isl_pw_qpolynomial *pwqp;
  29         isl_pw_qpolynomial *sum;
  30
  31         isl_pw_qpolynomial *fixed;
  32         isl_val *manual;
  33 };
  34
  35 static isl_stat manual_sum(__isl_take isl_point *pnt, void *user)
  36 {
  37         struct verify_point_sum *vps = (struct verify_point_sum *) user;
  38         isl_val *v;
  39
  40         v = isl_pw_qpolynomial_eval(isl_pw_qpolynomial_copy(vps->fixed), pnt);
  41         vps->manual = isl_val_add(vps->manual, v);
  42
  43         return isl_stat_ok;
  44 }
  45
  46 static isl_stat verify_point(__isl_take isl_point *pnt, void *user)
  47 {
  48         struct verify_point_sum *vps = (struct verify_point_sum *) user;
  49         int i;
  50         int ok;
  51         unsigned nparam;
  52         isl_val *v;
  53         isl_set *dom;
  54         isl_val *eval;
  55         int r;
  56         FILE *out = vps->vpd.options->print_all ? stdout : stderr;
  57
  58         vps->vpd.n--;
  59
  60         vps->fixed = isl_pw_qpolynomial_copy(vps->pwqp);
  61         nparam = isl_pw_qpolynomial_dim(vps->sum, isl_dim_param);
  62         for (i = 0; i < nparam; ++i) {
  63                 v = isl_point_get_coordinate_val(pnt, isl_dim_param, i);
  64                 vps->fixed = isl_pw_qpolynomial_fix_val(vps->fixed,
  65                                                         isl_dim_param, i, v);
  66         }
  67
  68         eval = isl_pw_qpolynomial_eval(isl_pw_qpolynomial_copy(vps->sum),
  69                                         isl_point_copy(pnt));
  70
  71         vps->manual = isl_val_zero(isl_point_get_ctx(pnt));
  72         dom = isl_pw_qpolynomial_domain(isl_pw_qpolynomial_copy(vps->fixed));
  73         r = isl_set_foreach_point(dom, &manual_sum, user);
  74         isl_set_free(dom);
  75         if (r < 0)
  76                 goto error;
  77
  78         ok = isl_val_eq(eval, vps->manual);
  79
  80         if (vps->vpd.options->print_all || !ok) {
  81                 isl_ctx *ctx = isl_pw_qpolynomial_get_ctx(vps->pwqp);
  82                 isl_printer *p = isl_printer_to_file(ctx, out);
  83                 fprintf(out, "sum(");
  84                 for (i = 0; i < nparam; ++i) {
  85                         if (i)
  86                                 fprintf(out, ", ");
  87                         v = isl_point_get_coordinate_val(pnt, isl_dim_param, i);
  88                         p = isl_printer_print_val(p, v);
  89                         isl_val_free(v);
  90                 }
  91                 fprintf(out, ") = ");
  92                 p = isl_printer_print_val(p, eval);
  93                 fprintf(out, ", sum(EP) = ");
  94                 p = isl_printer_print_val(p, vps->manual);
  95                 if (ok)
  96                         fprintf(out, ". OK\n");
  97                 else
  98                         fprintf(out, ". NOT OK\n");
  99                 isl_printer_free(p);
 100         } else if ((vps->vpd.n % vps->vpd.s) == 0) {
 101                 printf("o");
 102                 fflush(stdout);
 103         }
 104
 105         if (0) {
 106 error:
 107                 ok = 0;
 108         }
 109         isl_val_free(vps->manual);
 110         isl_pw_qpolynomial_free(vps->fixed);
 111         isl_val_free(eval);
 112         isl_point_free(pnt);
 113
 114         if (!ok)
 115                 vps->vpd.error = 1;
 116
 117         if (vps->vpd.options->continue_on_error)
 118                 ok = 1;
 119
 120         return (vps->vpd.n >= 1 && ok) ? isl_stat_ok : isl_stat_error;
 121 }
 122
 123 static int verify(__isl_keep isl_pw_qpolynomial *pwqp,
 124         __isl_keep isl_pw_qpolynomial *sum, struct verify_options *options)
 125 {
 126         struct verify_point_sum vps = { { options } };
 127         isl_set *context;
 128         int r;
 129
 130         vps.pwqp = pwqp;
 131         vps.sum = sum;
 132
 133         context = isl_pw_qpolynomial_domain(isl_pw_qpolynomial_copy(sum));
 134         context = verify_context_set_bounds(context, options);
 135
 136         r = verify_point_data_init(&vps.vpd, context);
 137
 138         if (r == 0)
 139                 isl_set_foreach_point(context, verify_point, &vps);
 140         if (vps.vpd.error)
 141                 r = -1;
 142
 143         isl_set_free(context);
 144
 145         verify_point_data_fini(&vps.vpd);
 146
 147         return r;
 148 }
 149
 150 int main(int argc, char **argv)
 151 {
 152     int result = 0;
 153     isl_ctx *ctx;
 154     isl_pw_qpolynomial *pwqp;
 155     isl_pw_qpolynomial *sum;
 156     struct isl_stream *s;
 157     struct options *options = options_new_with_defaults();
 158
 159     argc = options_parse(options, argc, argv, ISL_ARG_ALL);
 160     ctx = isl_ctx_alloc_with_options(&options_args, options);
 161
 162     s = isl_stream_new_file(ctx, stdin);
 163     pwqp = isl_stream_read_pw_qpolynomial(s);
 164
 165     if (options->verify->verify) {
 166         if (verify_options_set_range_pwqp(options->verify, pwqp) < 0)
 167             pwqp = isl_pw_qpolynomial_free(pwqp);
 168     }
 169
 170     sum = isl_pw_qpolynomial_sum(isl_pw_qpolynomial_copy(pwqp));
 171     if (options->verify->verify)
 172         result = verify(pwqp, sum, options->verify);
 173     else {
 174         isl_printer *p = isl_printer_to_file(ctx, stdout);
 175         p = isl_printer_print_pw_qpolynomial(p, sum);
 176         p = isl_printer_end_line(p);
 177         isl_printer_free(p);
 178     }
 179     isl_pw_qpolynomial_free(sum);
 180     isl_pw_qpolynomial_free(pwqp);
 181
 182     isl_stream_free(s);
 183     isl_ctx_free(ctx);
 184     return result;
 185 }