barvinok_enumerate_e.cc

   1 #include <ctype.h>
   2 #include <unistd.h>
   3 #include <stdlib.h>
   4 #include <assert.h>
   5 #include <barvinok/polylib.h>
   6 #include <barvinok/util.h>
   7 #include <barvinok/barvinok.h>
   8 #include "config.h"
   9 #ifdef HAVE_OMEGA
  10 #include "omega_interface/convert.h"
  11 #include "omega_interface/count.h"
  12 #endif
  13 #include "skewed_genfun.h"
  14 #include "verify.h"
  15 #include "verif_ehrhart.h"
  16 #include "verify_series.h"
  17 #include "evalue_convert.h"
  18 #include "barvinok_enumerate_e_options.h"
  19
  20 /* The input of this example program is a polytope in combined
  21  * data and parameter space followed by two lines indicating
  22  * the number of existential variables and parameters respectively.
  23  * The first lines starts with "E ", followed by a number.
  24  * The second lines starts with "P ", followed by a number.
  25  * These two lines are (optionally) followed by the names of the parameters.
  26  * The polytope is in PolyLib notation.
  27  */
  28
  29 #ifdef HAVE_OMEGA
  30
  31 Polyhedron *Omega_simplify(Polyhedron *P,
  32                             unsigned exist, unsigned nparam, const char **parms,
  33                             unsigned MaxRays)
  34 {
  35     varvector varv;
  36     varvector paramv;
  37     Relation r = Polyhedron2relation(P, exist, nparam, parms);
  38     Polyhedron_Free(P);
  39     return relation2Domain(r, varv, paramv, MaxRays);
  40 }
  41 #else
  42 Polyhedron *Omega_simplify(Polyhedron *P,
  43                             unsigned exist, unsigned nparam, const char **parms,
  44                             unsigned MaxRays)
  45 {
  46     return P;
  47 }
  48
  49 evalue *barvinok_enumerate_parker(Polyhedron *P,
  50                                         unsigned exist, unsigned nparam,
  51                                         unsigned MaxRays)
  52 {
  53     assert(0);
  54     return NULL;
  55 }
  56 #endif
  57
  58 static void verify_results(Polyhedron *P, evalue *EP, gen_fun *gf,
  59                            int exist, int nparam,
  60                            enumerate_e_options *options);
  61
  62 static char *next_line(FILE *input, char *line, unsigned len)
  63 {
  64         char *p;
  65
  66         do {
  67                 if (!(p = fgets(line, len, input)))
  68                         return NULL;
  69                 while (isspace(*p) && *p != '\n')
  70                         ++p;
  71         } while (*p == '#' || *p == '\n');
  72
  73         return p;
  74 }
  75
  76 int main(int argc, char **argv)
  77 {
  78     Polyhedron *A;
  79     Matrix *MA;
  80     const char **param_name;
  81     int exist, nparam, nvar;
  82     char s[128];
  83     evalue *EP = NULL;
  84     gen_fun *gf = NULL;
  85     int print_solution = 1;
  86     struct enumerate_e_options *options = enumerate_e_options_new_with_defaults();
  87
  88     argc = enumerate_e_options_parse(options, argc, argv, ISL_ARG_ALL);
  89
  90     MA = Matrix_Read();
  91     A = Constraints2Polyhedron(MA, options->verify->barvinok->MaxRays);
  92     Matrix_Free(MA);
  93
  94     exist = -1;
  95     while (next_line(stdin, s, sizeof(s)))
  96         if (sscanf(s, "E %d", &exist) == 1)
  97             break;
  98     assert(exist >= 0);
  99
 100     nparam = -1;
 101     while (next_line(stdin, s, sizeof(s)))
 102         if (sscanf(s, "P %d", &nparam) == 1)
 103             break;
 104     assert(nparam >= 0);
 105
 106     if (options->verify->verify) {
 107         verify_options_set_range(options->verify, A->Dimension);
 108         if (!options->verify->barvinok->verbose)
 109             print_solution = 0;
 110     }
 111
 112     if (print_solution && options->verify->barvinok->verbose) {
 113         Polyhedron_Print(stdout, P_VALUE_FMT, A);
 114         printf("exist: %d, nparam: %d\n", exist, nparam);
 115     }
 116     param_name = Read_ParamNames(stdin, nparam);
 117     nvar = A->Dimension - exist - nparam;
 118     if (options->omega) {
 119         A = Omega_simplify(A, exist, nparam, param_name,
 120                                 options->verify->barvinok->MaxRays);
 121         assert(!A->next);
 122         exist = A->Dimension - nvar - nparam;
 123     }
 124     if (options->series) {
 125         if (exist == 2 && options->scarf)
 126             gf = barvinok_enumerate_scarf_series(A, exist, nparam,
 127                                                     options->verify->barvinok);
 128         else
 129             gf = barvinok_enumerate_e_series(A, exist, nparam,
 130                                                     options->verify->barvinok);
 131         if (print_solution) {
 132             gf->print(std::cout, nparam, param_name);
 133             puts("");
 134         }
 135         if (options->function) {
 136             EP = *gf;
 137             if (print_solution)
 138                 print_evalue(stdout, EP, param_name);
 139         }
 140     } else {
 141         if (options->parker)
 142             EP = barvinok_enumerate_parker(A, A->Dimension-nparam-exist, nparam,
 143                                             options->verify->barvinok->MaxRays);
 144         else if (exist == 2 && options->scarf)
 145             EP = barvinok_enumerate_scarf(A, exist, nparam,
 146                                                 options->verify->barvinok);
 147         else if (options->isl && exist > 0)
 148             EP = barvinok_enumerate_isl(A, exist, nparam,
 149                                                 options->verify->barvinok);
 150         else
 151             EP = barvinok_enumerate_e_with_options(A, exist, nparam,
 152                                                 options->verify->barvinok);
 153         reduce_evalue(EP);
 154         if (evalue_convert(EP, options->convert,
 155                         options->verify->barvinok->verbose, nparam, param_name))
 156             print_solution = 0;
 157         if (print_solution)
 158             print_evalue(stdout, EP, param_name);
 159     }
 160     if (options->verify->verify) {
 161         options->verify->params = param_name;
 162         verify_results(A, EP, gf, exist, nparam, options);
 163     }
 164     if (gf)
 165         delete gf;
 166     if (EP)
 167         evalue_free(EP);
 168
 169     if (options->verify->barvinok->print_stats)
 170         barvinok_stats_print(options->verify->barvinok->stats, stdout);
 171
 172     Free_ParamNames(param_name, nparam);
 173     Polyhedron_Free(A);
 174     enumerate_e_options_free(options);
 175     return 0;
 176 }
 177
 178 void verify_results(Polyhedron *P, evalue *EP, gen_fun *gf,
 179                        int exist, int nparam,
 180                        enumerate_e_options *options)
 181 {
 182     int res = 0;
 183     Vector *p;
 184     Value tmp;
 185     Polyhedron *S, *CS;
 186     unsigned MaxRays = options->verify->barvinok->MaxRays;
 187     Polyhedron *C = NULL;
 188     value_init(tmp);
 189
 190     p = Vector_Alloc(P->Dimension+2);
 191     value_set_si(p->p[P->Dimension+1], 1);
 192
 193     CS = check_poly_context_scan(P, &C, nparam, options->verify);
 194     if (!C)
 195         C = Universe_Polyhedron(nparam);
 196
 197     /* S = scanning list of polyhedra */
 198     S = Polyhedron_Scan(P, C, MaxRays & POL_NO_DUAL ? 0 : MaxRays);
 199
 200     check_poly_init(C, options->verify);
 201
 202     /******* CHECK NOW *********/
 203     if (S) {
 204         if (!options->series || options->function) {
 205             if (!check_poly_EP(S, CS, EP, exist, nparam, 0, p->p,
 206                                 options->verify))
 207                 res = -1;
 208         } else {
 209             skewed_gen_fun *sgf = new skewed_gen_fun(new gen_fun(gf));
 210             if (!check_poly_gf(S, CS, sgf, exist, nparam, 0, p->p,
 211                                 options->verify))
 212                 res = -1;
 213             delete sgf;
 214         }
 215     }
 216
 217     if (!options->verify->print_all)
 218         printf( "\n" );
 219
 220     Vector_Free(p);
 221     value_clear(tmp);
 222     Domain_Free(S);
 223     Polyhedron_Free(C);
 224     if (CS)
 225         Domain_Free(CS);
 226 }