barvinok_summate.c

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