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 "argp.h"
   7 #include "progname.h"
   8 #include "evalue_convert.h"
   9 #include "evalue_read.h"
  10 #include "verify.h"
  11
  12 using std::cout;
  13 using std::cerr;
  14 using std::endl;
  15
  16 #define ALLOCN(type,n) (type*)malloc((n) * sizeof(type))
  17
  18 #define OPT_VARS            (BV_OPT_LAST+1)
  19
  20 struct argp_option argp_options[] = {
  21     { "variables",          OPT_VARS,   "list", 0,
  22         "comma separated list of variables over which to sum" },
  23     { "verbose",            'v',        0,      0, },
  24     { 0 }
  25 };
  26
  27 struct options {
  28     struct convert_options   convert;
  29     struct verify_options    verify;
  30     char* var_list;
  31     int verbose;
  32 };
  33
  34 static error_t parse_opt(int key, char *arg, struct argp_state *state)
  35 {
  36     struct options *options = (struct options*) state->input;
  37
  38     switch (key) {
  39     case ARGP_KEY_INIT:
  40         state->child_inputs[0] = &options->convert;
  41         state->child_inputs[1] = &options->verify;
  42         state->child_inputs[2] = options->verify.barvinok;
  43         options->var_list = NULL;
  44         options->verbose = 0;
  45         break;
  46     case 'v':
  47         options->verbose = 1;
  48         break;
  49     case OPT_VARS:
  50         options->var_list = strdup(arg);
  51         break;
  52     default:
  53         return ARGP_ERR_UNKNOWN;
  54     }
  55     return 0;
  56 }
  57
  58 static int check_poly_sum(const struct check_poly_data *data,
  59                           int nparam, Value *z,
  60                           const struct verify_options *options);
  61
  62 struct check_poly_sum_data : public check_poly_data {
  63     Polyhedron          **S;
  64     evalue               *EP;
  65     evalue               *sum;
  66
  67     check_poly_sum_data(Value *z, evalue *EP, evalue *sum) :
  68                         EP(EP), sum(sum) {
  69         this->z = z;
  70         this->check = check_poly_sum;
  71     }
  72 };
  73
  74 static void sum(Polyhedron *S, int pos, const check_poly_sum_data *data,
  75                 evalue *s, const struct verify_options *options)
  76 {
  77     if (!S) {
  78         evalue *e = evalue_eval(data->EP, data->z+1);
  79         eadd(e, s);
  80         evalue_free(e);
  81     } else {
  82         Value LB, UB;
  83         int ok;
  84         value_init(LB);
  85         value_init(UB);
  86         ok = !(lower_upper_bounds(1+pos, S, data->z, &LB, &UB));
  87         assert(ok);
  88         for (; value_le(LB, UB); value_increment(LB, LB)) {
  89             value_assign(data->z[1+pos], LB);
  90             sum(S->next, pos+1, data, s, options);
  91         }
  92         value_set_si(data->z[1+pos], 0);
  93         value_clear(LB);
  94         value_clear(UB);
  95     }
  96 }
  97
  98 static evalue *sum(const check_poly_sum_data *data,
  99                           const struct verify_options *options)
 100 {
 101     evalue *s = evalue_zero();
 102     for (int i = 0; i < data->EP->x.p->size/2; ++i)
 103         if (!emptyQ2(data->S[i]))
 104             sum(data->S[i], 0, data, s, options);
 105     return s;
 106 }
 107
 108 static int check_poly_sum(const struct check_poly_data *data,
 109                           int nparam, Value *z,
 110                           const struct verify_options *options)
 111 {
 112     const check_poly_sum_data *sum_data;
 113     sum_data = static_cast<const check_poly_sum_data *>(data);
 114     evalue *e, *s;
 115     int k;
 116     int ok;
 117
 118     e = evalue_eval(sum_data->sum, z);
 119     s = sum(sum_data, options);
 120
 121     ok = eequal(e, s);
 122
 123     check_poly_print(ok, nparam, z, s->x.n, s->d, e->x.n, e->d,
 124                      "sum", "sum(EP)", "summation", options);
 125
 126     evalue_free(s);
 127     evalue_free(e);
 128
 129     return ok;
 130 }
 131
 132 static int verify(Polyhedron *P, evalue *sum, evalue *EP,
 133                   unsigned nvar, unsigned nparam, Vector *p,
 134                   struct verify_options *options)
 135 {
 136     Polyhedron *CS;
 137     unsigned MaxRays = options->barvinok->MaxRays;
 138     int error = 0;
 139
 140     CS = check_poly_context_scan(NULL, &P, P->Dimension, options);
 141
 142     check_poly_init(P, options);
 143
 144     if (!(CS && emptyQ2(CS))) {
 145         check_poly_sum_data data(p->p, EP, sum);
 146         data.S = ALLOCN(Polyhedron *, EP->x.p->size/2);
 147         for (int i = 0; i < EP->x.p->size/2; ++i) {
 148             Polyhedron *A = EVALUE_DOMAIN(EP->x.p->arr[2*i]);
 149             data.S[i] = Polyhedron_Scan(A, P, MaxRays & POL_NO_DUAL ? 0 : MaxRays);
 150         }
 151         error = !check_poly(CS, &data, nparam, 0, p->p+1+nvar, options);
 152         for (int i = 0; i < EP->x.p->size/2; ++i)
 153             Domain_Free(data.S[i]);
 154         free(data.S);
 155     }
 156
 157     if (!options->print_all)
 158         printf("\n");
 159
 160     if (CS) {
 161         Domain_Free(CS);
 162         Domain_Free(P);
 163     }
 164
 165     return error;
 166 }
 167
 168 /*
 169  * Project on final dim dimensions
 170  */
 171 Polyhedron *DomainProject(Polyhedron *D, unsigned dim, unsigned MaxRays)
 172 {
 173     Polyhedron *P;
 174     Polyhedron *R;
 175
 176     R = Polyhedron_Project(D, dim);
 177     for (P = D->next; P; P = P->next) {
 178         Polyhedron *R2 = Polyhedron_Project(P, dim);
 179         Polyhedron *R3 = DomainUnion(R, R2, MaxRays);
 180         Polyhedron_Free(R2);
 181         Domain_Free(R);
 182         R = R3;
 183     }
 184     return R;
 185 }
 186
 187 static int verify(evalue *EP, evalue *sum, unsigned nvar, unsigned nparam,
 188                   struct verify_options *options)
 189 {
 190     Vector *p;
 191
 192     p = Vector_Alloc(nvar+nparam+2);
 193     value_set_si(p->p[nvar+nparam+1], 1);
 194
 195     assert(value_zero_p(EP->d));
 196     assert(EP->x.p->type == partition);
 197
 198     Polyhedron *EP_D = EVALUE_DOMAIN(EP->x.p->arr[0]);
 199     Polyhedron *D = Polyhedron_Project(EP_D, nparam);
 200
 201     for (int i = 1; i < EP->x.p->size/2; ++i) {
 202         Polyhedron *D2 = D;
 203         EP_D = DomainProject(EVALUE_DOMAIN(EP->x.p->arr[2*i]), nparam,
 204                              options->barvinok->MaxRays);
 205         D = DomainUnion(EP_D, D, options->barvinok->MaxRays);
 206         Domain_Free(D2);
 207     }
 208
 209     int error = 0;
 210
 211     for (Polyhedron *P = D; P; P = P->next) {
 212         error = verify(P, sum, EP, nvar, nparam, p, options);
 213         if (error && !options->continue_on_error)
 214             break;
 215     }
 216
 217     Domain_Free(D);
 218     Vector_Free(p);
 219
 220     return error;
 221 }
 222
 223 int main(int argc, char **argv)
 224 {
 225     evalue *EP;
 226     char **all_vars = NULL;
 227     unsigned nvar;
 228     unsigned nparam;
 229     struct options options;
 230     struct barvinok_options *bv_options = barvinok_options_new_with_defaults();
 231     static struct argp_child argp_children[] = {
 232         { &convert_argp,        0,      "input conversion",     1 },
 233         { &verify_argp,         0,      "verification",         2 },
 234         { &barvinok_argp,       0,      "barvinok options",     3 },
 235         { 0 }
 236     };
 237     static struct argp argp = { argp_options, parse_opt, 0, 0, argp_children };
 238     int result = 0;
 239
 240     options.verify.barvinok = bv_options;
 241     set_program_name(argv[0]);
 242     argp_parse(&argp, argc, argv, 0, 0, &options);
 243
 244     EP = evalue_read_from_file(stdin, options.var_list, &all_vars,
 245                                &nvar, &nparam, bv_options->MaxRays);
 246     assert(EP);
 247
 248     if (options.verify.verify)
 249         verify_options_set_range(&options.verify, nvar+nparam);
 250
 251     evalue_convert(EP, &options.convert, options.verbose, nparam, all_vars);
 252
 253     if (EVALUE_IS_ZERO(*EP))
 254         print_evalue(stdout, EP, all_vars);
 255     else {
 256         evalue *sum = barvinok_summate(EP, nvar, bv_options);
 257         assert(sum);
 258         if (options.verify.verify)
 259             result = verify(EP, sum, nvar, nparam, &options.verify);
 260         else
 261             print_evalue(stdout, sum, all_vars+nvar);
 262         evalue_free(sum);
 263     }
 264
 265     evalue_free(EP);
 266
 267     if (options.var_list)
 268         free(options.var_list);
 269     Free_ParamNames(all_vars, nvar+nparam);
 270     barvinok_options_free(bv_options);
 271     return result;
 272 }