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     if (options->verify->verify) {
 106         verify_options_set_range(options->verify, A->Dimension);
 107         if (!options->verify->barvinok->verbose)
 108             print_solution = 0;
 109     }
 110
 111     if (print_solution && options->verify->barvinok->verbose) {
 112         Polyhedron_Print(stdout, P_VALUE_FMT, A);
 113         printf("exist: %d, nparam: %d\n", exist, nparam);
 114     }
 115     param_name = Read_ParamNames(stdin, nparam);
 116     nvar = A->Dimension - exist - nparam;
 117     if (options->omega) {
 118         A = Omega_simplify(A, exist, nparam, param_name,
 119                                 options->verify->barvinok->MaxRays);
 120         assert(!A->next);
 121         exist = A->Dimension - nvar - nparam;
 122     }
 123     if (options->series) {
 124         if (exist == 2 && options->scarf)
 125             gf = barvinok_enumerate_scarf_series(A, exist, nparam,
 126                                                     options->verify->barvinok);
 127         else
 128             gf = barvinok_enumerate_e_series(A, exist, nparam,
 129                                                     options->verify->barvinok);
 130         if (print_solution) {
 131             gf->print(std::cout, nparam, param_name);
 132             puts("");
 133         }
 134         if (options->function) {
 135             EP = *gf;
 136             if (print_solution)
 137                 print_evalue(stdout, EP, param_name);
 138         }
 139     } else {
 140         if (options->parker)
 141             EP = barvinok_enumerate_parker(A, A->Dimension-nparam-exist, nparam,
 142                                             options->verify->barvinok->MaxRays);
 143         else if (exist == 2 && options->scarf)
 144             EP = barvinok_enumerate_scarf(A, exist, nparam,
 145                                                 options->verify->barvinok);
 146         else if (options->isl && exist > 0)
 147             EP = barvinok_enumerate_isl(A, exist, nparam,
 148                                                 options->verify->barvinok);
 149         else
 150             EP = barvinok_enumerate_e_with_options(A, exist, nparam,
 151                                                 options->verify->barvinok);
 152         reduce_evalue(EP);
 153         if (evalue_convert(EP, options->convert,
 154                         options->verify->barvinok->verbose, nparam, param_name))
 155             print_solution = 0;
 156         if (print_solution)
 157             print_evalue(stdout, EP, param_name);
 158     }
 159     if (options->verify->verify) {
 160         options->verify->params = param_name;
 161         verify_results(A, EP, gf, exist, nparam, options);
 162     }
 163     if (gf)
 164         delete gf;
 165     if (EP)
 166         evalue_free(EP);
 167
 168     if (options->verify->barvinok->print_stats)
 169         barvinok_stats_print(options->verify->barvinok->stats, stdout);
 170
 171     Free_ParamNames(param_name, nparam);
 172     Polyhedron_Free(A);
 173     enumerate_e_options_free(options);
 174     return 0;
 175 }
 176
 177 void verify_results(Polyhedron *P, evalue *EP, gen_fun *gf,
 178                        int exist, int nparam,
 179                        enumerate_e_options *options)
 180 {
 181     int i;
 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 }