barvinok_enumerate_e.cc

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