barvinok_summate.cc

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