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