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