summate.cc

   1 #include <iostream>
   2 #include <barvinok/evalue.h>
   3 #include <barvinok/options.h>
   4 #include <barvinok/util.h>
   5 #include "argp.h"
   6 #include "progname.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 #define OPT_VARS            (BV_OPT_LAST+1)
  18
  19 struct argp_option argp_options[] = {
  20     { "variables",          OPT_VARS,   "list", 0,
  21         "comma separated list of variables over which to maximize" },
  22     { "verbose",            'v',        0,      0, },
  23     { 0 }
  24 };
  25
  26 struct options {
  27     struct convert_options   convert;
  28     struct verify_options    verify;
  29     char* var_list;
  30     int verbose;
  31 };
  32
  33 static error_t parse_opt(int key, char *arg, struct argp_state *state)
  34 {
  35     struct options *options = (struct options*) state->input;
  36
  37     switch (key) {
  38     case ARGP_KEY_INIT:
  39         state->child_inputs[0] = &options->convert;
  40         state->child_inputs[1] = &options->verify;
  41         state->child_inputs[2] = options->verify.barvinok;
  42         options->var_list = NULL;
  43         options->verbose = 0;
  44         break;
  45     case 'v':
  46         options->verbose = 1;
  47         break;
  48     case OPT_VARS:
  49         options->var_list = strdup(arg);
  50         break;
  51     default:
  52         return ARGP_ERR_UNKNOWN;
  53     }
  54     return 0;
  55 }
  56
  57 static int check_poly_sum(const struct check_poly_data *data,
  58                           int nparam, Value *z,
  59                           const struct verify_options *options);
  60
  61 struct check_poly_sum_data : public check_poly_data {
  62     Polyhedron          **S;
  63     evalue               *EP;
  64     evalue               *sum;
  65
  66     check_poly_sum_data(Value *z, evalue *EP, evalue *sum) :
  67                         EP(EP), sum(sum) {
  68         this->z = z;
  69         this->check = check_poly_sum;
  70     }
  71 };
  72
  73 static void sum(Polyhedron *S, int pos, const check_poly_sum_data *data,
  74                 evalue *s, const struct verify_options *options)
  75 {
  76     if (!S) {
  77         evalue *e = evalue_eval(data->EP, data->z+1);
  78         eadd(e, s);
  79         free_evalue_refs(e);
  80         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     if (options->print_all) {
 120         printf("sum(");
 121         value_print(stdout, VALUE_FMT, z[0]);
 122         for (k = 1; k < nparam; ++k) {
 123             printf(", ");
 124             value_print(stdout, VALUE_FMT, z[k]);
 125         }
 126         printf(") = ");
 127         value_print(stdout, VALUE_FMT, e->x.n);
 128         if (value_notone_p(e->d)) {
 129             printf("/");
 130             value_print(stdout, VALUE_FMT, e->d);
 131         }
 132     }
 133
 134     s = sum(sum_data, options);
 135
 136     if (options->print_all) {
 137         printf(", sum(EP) = ");
 138         value_print(stdout, VALUE_FMT, s->x.n);
 139         if (value_notone_p(s->d)) {
 140             printf("/");
 141             value_print(stdout, VALUE_FMT, s->d);
 142         }
 143         printf(". ");
 144     }
 145
 146     ok = eequal(e, s);
 147
 148     if (!ok) {
 149         printf("\n");
 150         fflush(stdout);
 151         fprintf(stderr,"Error !\n");
 152         fprintf(stderr,"sum( ");
 153         value_print(stderr, VALUE_FMT, z[0]);
 154         for (k = 1; k < nparam; ++k) {
 155             fprintf(stderr, ", ");
 156             value_print(stderr, VALUE_FMT, z[k]);
 157         }
 158         fprintf(stderr," ) should be ");
 159         value_print(stderr, VALUE_FMT, s->x.n);
 160         if (value_notone_p(s->d)) {
 161             fprintf(stderr, "/");
 162             value_print(stderr, VALUE_FMT, s->d);
 163         }
 164         fprintf(stderr,", while summation gives ");
 165         value_print(stderr, VALUE_FMT, e->x.n);
 166         if (value_notone_p(e->d)) {
 167             fprintf(stderr, "/");
 168             value_print(stderr, VALUE_FMT, e->d);
 169         }
 170         fprintf(stderr, ".\n");
 171     } else if (options->print_all)
 172         printf("OK.\n");
 173
 174     free_evalue_refs(s);
 175     free(s);
 176     free_evalue_refs(e);
 177     free(e);
 178
 179     return ok;
 180 }
 181
 182 static int verify(Polyhedron *P, evalue *sum, evalue *EP,
 183                   unsigned nvar, unsigned nparam, Vector *p,
 184                   struct verify_options *options)
 185 {
 186     Polyhedron *CS;
 187     unsigned MaxRays = options->barvinok->MaxRays;
 188     int error = 0;
 189
 190     CS = check_poly_context_scan(NULL, &P, P->Dimension, options);
 191
 192     check_poly_init(P, options);
 193
 194     if (!(CS && emptyQ2(CS))) {
 195         check_poly_sum_data data(p->p, EP, sum);
 196         data.S = ALLOCN(Polyhedron *, EP->x.p->size/2);
 197         for (int i = 0; i < EP->x.p->size/2; ++i) {
 198             Polyhedron *A = EVALUE_DOMAIN(EP->x.p->arr[2*i]);
 199             data.S[i] = Polyhedron_Scan(A, P, MaxRays & POL_NO_DUAL ? 0 : MaxRays);
 200         }
 201         error = !check_poly(CS, &data, nparam, 0, p->p+1+nvar, options);
 202         for (int i = 0; i < EP->x.p->size/2; ++i)
 203             Domain_Free(data.S[i]);
 204         free(data.S);
 205     }
 206
 207     if (!options->print_all)
 208         printf("\n");
 209
 210     if (CS) {
 211         Domain_Free(CS);
 212         Domain_Free(P);
 213     }
 214
 215     return error;
 216 }
 217
 218 static int verify(evalue *EP, evalue *sum, unsigned nvar, unsigned nparam,
 219                   struct verify_options *options)
 220 {
 221     Vector *p;
 222
 223     p = Vector_Alloc(nvar+nparam+2);
 224     value_set_si(p->p[nvar+nparam+1], 1);
 225
 226     assert(value_zero_p(sum->d));
 227     assert(sum->x.p->type == partition);
 228     int error = 0;
 229
 230     for (int i = 0; i < sum->x.p->size/2; ++i) {
 231         Polyhedron *D = EVALUE_DOMAIN(sum->x.p->arr[2*i]);
 232         for (Polyhedron *P = D; P; P = P->next) {
 233             error = verify(P, sum, EP, nvar, nparam, p, options);
 234             if (error && !options->continue_on_error)
 235                 break;
 236         }
 237         if (error && !options->continue_on_error)
 238             break;
 239     }
 240
 241     Vector_Free(p);
 242
 243     return error;
 244 }
 245
 246 int main(int argc, char **argv)
 247 {
 248     evalue *EP;
 249     char **all_vars = NULL;
 250     unsigned nvar;
 251     unsigned nparam;
 252     struct options options;
 253     struct barvinok_options *bv_options = barvinok_options_new_with_defaults();
 254     static struct argp_child argp_children[] = {
 255         { &convert_argp,        0,      "input conversion",     1 },
 256         { &verify_argp,         0,      "verification",         2 },
 257         { &barvinok_argp,       0,      "barvinok options",     3 },
 258         { 0 }
 259     };
 260     static struct argp argp = { argp_options, parse_opt, 0, 0, argp_children };
 261     int result = 0;
 262
 263     options.verify.barvinok = bv_options;
 264     set_program_name(argv[0]);
 265     argp_parse(&argp, argc, argv, 0, 0, &options);
 266
 267     EP = evalue_read_from_file(stdin, options.var_list, &all_vars,
 268                                &nvar, &nparam, bv_options->MaxRays);
 269     assert(EP);
 270
 271     if (options.verify.verify)
 272         verify_options_set_range(&options.verify, nvar+nparam);
 273
 274     evalue_convert(EP, &options.convert, options.verbose, nparam, all_vars);
 275
 276     if (EVALUE_IS_ZERO(*EP))
 277         print_evalue(stdout, EP, all_vars);
 278     else {
 279         evalue *sum = evalue_sum(EP, nvar, bv_options->MaxRays);
 280         if (options.verify.verify)
 281             result = verify(EP, sum, nvar, nparam, &options.verify);
 282         else
 283             print_evalue(stdout, sum, all_vars+nvar);
 284         free_evalue_refs(sum);
 285         free(sum);
 286     }
 287
 288     free_evalue_refs(EP);
 289     free(EP);
 290
 291     if (options.var_list)
 292         free(options.var_list);
 293     Free_ParamNames(all_vars, nvar+nparam);
 294     barvinok_options_free(bv_options);
 295     return result;
 296 }