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