barvinok_summate.cc

   1 #include <assert.h>
   2 #include <iostream>
   3 #include <barvinok/barvinok.h>
   4 #include <barvinok/options.h>
   5 #include <barvinok/util.h>
   6 #include "barvinok_summate_options.h"
   7 #include "evalue_convert.h"
   8 #include "evalue_read.h"
   9 #include "verify.h"
  10
  11 using std::cout;
  12 using std::cerr;
  13 using std::endl;
  14
  15 #define ALLOCN(type,n) (type*)malloc((n) * sizeof(type))
  16
  17 static int check_poly_sum(const struct check_poly_data *data,
  18                           int nparam, Value *z,
  19                           const struct verify_options *options);
  20
  21 struct check_poly_sum_data : public check_EP_data {
  22     evalue               *sum;
  23
  24     check_poly_sum_data(const evalue *EP, evalue *sum) : sum(sum) {
  25         this->EP = EP;
  26         this->cp.check = check_poly_sum;
  27     }
  28 };
  29
  30 static void sum(Polyhedron *S, int pos, const check_poly_sum_data *data,
  31                 evalue *s, const struct verify_options *options)
  32 {
  33     if (!S) {
  34         evalue *e = evalue_eval(data->EP, data->cp.z+1);
  35         eadd(e, s);
  36         evalue_free(e);
  37     } else {
  38         Value LB, UB;
  39         int ok;
  40         value_init(LB);
  41         value_init(UB);
  42         ok = !(lower_upper_bounds(1+pos, S, data->cp.z, &LB, &UB));
  43         assert(ok);
  44         for (; value_le(LB, UB); value_increment(LB, LB)) {
  45             value_assign(data->cp.z[1+pos], LB);
  46             sum(S->next, pos+1, data, s, options);
  47         }
  48         value_set_si(data->cp.z[1+pos], 0);
  49         value_clear(LB);
  50         value_clear(UB);
  51     }
  52 }
  53
  54 static evalue *sum(const check_poly_sum_data *data,
  55                           const struct verify_options *options)
  56 {
  57     evalue *s = evalue_zero();
  58     for (int i = 0; i < data->n_S; ++i)
  59         if (!emptyQ2(data->S[i]))
  60             sum(data->S[i], 0, data, s, options);
  61     return s;
  62 }
  63
  64 static int check_poly_sum(const struct check_poly_data *data,
  65                           int nparam, Value *z,
  66                           const struct verify_options *options)
  67 {
  68     const check_poly_sum_data *sum_data;
  69     sum_data = (const check_poly_sum_data *)data;
  70     evalue *e, *s;
  71     int k;
  72     int ok;
  73
  74     e = evalue_eval(sum_data->sum, z);
  75     s = sum(sum_data, options);
  76
  77     ok = eequal(e, s);
  78
  79     check_poly_print(ok, nparam, z, s->x.n, s->d, e->x.n, e->d,
  80                      "sum", "sum(EP)", "summation", options);
  81
  82     evalue_free(s);
  83     evalue_free(e);
  84
  85     return ok;
  86 }
  87
  88 static int verify(evalue *EP, evalue *sum, unsigned nvar, unsigned nparam,
  89                   struct verify_options *options)
  90 {
  91     check_poly_sum_data data(EP, sum);
  92     return !check_EP(&data, nvar, nparam, options);
  93 }
  94
  95 int main(int argc, char **argv)
  96 {
  97     evalue *EP;
  98     const char **all_vars = NULL;
  99     unsigned nvar;
 100     unsigned nparam;
 101     int result = 0;
 102     struct options *options = options_new_with_defaults();
 103
 104     argc = options_parse(options, argc, argv, ISL_ARG_ALL);
 105
 106     EP = evalue_read_from_file(stdin, options->var_list, &all_vars,
 107                                &nvar, &nparam, options->verify->barvinok->MaxRays);
 108     assert(EP);
 109
 110     if (options->verify->verify)
 111         verify_options_set_range(options->verify, nvar+nparam);
 112
 113     evalue_convert(EP, options->convert, options->verify->barvinok->verbose,
 114                         nparam, all_vars);
 115
 116     if (EVALUE_IS_ZERO(*EP))
 117         print_evalue(stdout, EP, all_vars);
 118     else {
 119         evalue *sum = barvinok_summate(EP, nvar, options->verify->barvinok);
 120         assert(sum);
 121         if (options->verify->verify)
 122             result = verify(EP, sum, nvar, nparam, options->verify);
 123         else
 124             print_evalue(stdout, sum, all_vars+nvar);
 125         evalue_free(sum);
 126     }
 127
 128     evalue_free(EP);
 129
 130     Free_ParamNames(all_vars, nvar+nparam);
 131     options_free(options);
 132     return result;
 133 }