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_EP_data {
  57     evalue               *sum;
  58
  59     check_poly_sum_data(const evalue *EP, evalue *sum) : sum(sum) {
  60         this->EP = EP;
  61         this->cp.check = check_poly_sum;
  62     }
  63 };
  64
  65 static void sum(Polyhedron *S, int pos, const check_poly_sum_data *data,
  66                 evalue *s, const struct verify_options *options)
  67 {
  68     if (!S) {
  69         evalue *e = evalue_eval(data->EP, data->cp.z+1);
  70         eadd(e, s);
  71         evalue_free(e);
  72     } else {
  73         Value LB, UB;
  74         int ok;
  75         value_init(LB);
  76         value_init(UB);
  77         ok = !(lower_upper_bounds(1+pos, S, data->cp.z, &LB, &UB));
  78         assert(ok);
  79         for (; value_le(LB, UB); value_increment(LB, LB)) {
  80             value_assign(data->cp.z[1+pos], LB);
  81             sum(S->next, pos+1, data, s, options);
  82         }
  83         value_set_si(data->cp.z[1+pos], 0);
  84         value_clear(LB);
  85         value_clear(UB);
  86     }
  87 }
  88
  89 static evalue *sum(const check_poly_sum_data *data,
  90                           const struct verify_options *options)
  91 {
  92     evalue *s = evalue_zero();
  93     for (int i = 0; i < data->n_S; ++i)
  94         if (!emptyQ2(data->S[i]))
  95             sum(data->S[i], 0, data, s, options);
  96     return s;
  97 }
  98
  99 static int check_poly_sum(const struct check_poly_data *data,
 100                           int nparam, Value *z,
 101                           const struct verify_options *options)
 102 {
 103     const check_poly_sum_data *sum_data;
 104     sum_data = (const check_poly_sum_data *)data;
 105     evalue *e, *s;
 106     int k;
 107     int ok;
 108
 109     e = evalue_eval(sum_data->sum, z);
 110     s = sum(sum_data, options);
 111
 112     ok = eequal(e, s);
 113
 114     check_poly_print(ok, nparam, z, s->x.n, s->d, e->x.n, e->d,
 115                      "sum", "sum(EP)", "summation", options);
 116
 117     evalue_free(s);
 118     evalue_free(e);
 119
 120     return ok;
 121 }
 122
 123 static int verify(evalue *EP, evalue *sum, unsigned nvar, unsigned nparam,
 124                   struct verify_options *options)
 125 {
 126     check_poly_sum_data data(EP, sum);
 127     return !check_EP(&data, nvar, nparam, options);
 128 }
 129
 130 int main(int argc, char **argv)
 131 {
 132     evalue *EP;
 133     char **all_vars = NULL;
 134     unsigned nvar;
 135     unsigned nparam;
 136     struct options options;
 137     struct barvinok_options *bv_options = barvinok_options_new_with_defaults();
 138     static struct argp_child argp_children[] = {
 139         { &convert_argp,        0,      "input conversion",     1 },
 140         { &verify_argp,         0,      "verification",         2 },
 141         { &barvinok_argp,       0,      "barvinok options",     3 },
 142         { 0 }
 143     };
 144     static struct argp argp = { argp_options, parse_opt, 0, 0, argp_children };
 145     int result = 0;
 146
 147     options.verify.barvinok = bv_options;
 148     set_program_name(argv[0]);
 149     argp_parse(&argp, argc, argv, 0, 0, &options);
 150
 151     EP = evalue_read_from_file(stdin, options.var_list, &all_vars,
 152                                &nvar, &nparam, bv_options->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, bv_options->verbose, nparam, all_vars);
 159
 160     if (EVALUE_IS_ZERO(*EP))
 161         print_evalue(stdout, EP, all_vars);
 162     else {
 163         evalue *sum = barvinok_summate(EP, nvar, bv_options);
 164         assert(sum);
 165         if (options.verify.verify)
 166             result = verify(EP, sum, nvar, nparam, &options.verify);
 167         else
 168             print_evalue(stdout, sum, all_vars+nvar);
 169         evalue_free(sum);
 170     }
 171
 172     evalue_free(EP);
 173
 174     if (options.var_list)
 175         free(options.var_list);
 176     Free_ParamNames(all_vars, nvar+nparam);
 177     barvinok_options_free(bv_options);
 178     return result;
 179 }