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