verify.c

   1 #include <stdlib.h>
   2 #include <barvinok/options.h>
   3 #include "verify.h"
   4
   5 /* RANGE : normal range for evalutations (-RANGE -> RANGE) */
   6 #define RANGE 50
   7
   8 /* SRANGE : small range for evalutations */
   9 #define SRANGE 15
  10
  11 /* if dimension >= BIDDIM, use SRANGE */
  12 #define BIGDIM 5
  13
  14 /* VSRANGE : very small range for evalutations */
  15 #define VSRANGE 5
  16
  17 /* if dimension >= VBIDDIM, use VSRANGE */
  18 #define VBIGDIM 8
  19
  20 static struct argp_option argp_options[] = {
  21     { "verify",             'T',    0,      0 },
  22     { "exact",              'E',    0,      0 },
  23     { "print-all",          'A',    0,      0 },
  24     { "continue-on-error",  'C',    0,      0 },
  25     { "min",                'm',    "int",  0 },
  26     { "max",                'M',    "int",  0 },
  27     { "range",              'r',    "int",  0 },
  28     { 0 }
  29 };
  30
  31 static error_t parse_opt(int key, char *arg, struct argp_state *state)
  32 {
  33     struct verify_options *options = state->input;
  34
  35     switch (key) {
  36     case ARGP_KEY_INIT:
  37         options->verify = 0;
  38         options->exact = 0;
  39         options->print_all = 0;
  40         options->continue_on_error = 0;
  41         options->m = INT_MAX;
  42         options->M = INT_MIN;
  43         break;
  44     case ARGP_KEY_FINI:
  45         break;
  46     case 'T':
  47         options->verify = 1;
  48         break;
  49     case 'E':
  50         options->exact = 1;
  51         break;
  52     case 'A':
  53         options->print_all = 1;
  54         break;
  55     case 'C':
  56         options->continue_on_error = 1;
  57         break;
  58     case 'm':
  59         options->m = atoi(arg);
  60         options->verify = 1;
  61         break;
  62     case 'M':
  63         options->M = atoi(arg);
  64         options->verify = 1;
  65         break;
  66     case 'r':
  67         options->M = atoi(arg);
  68         options->m = -options->M;
  69         options->verify = 1;
  70         break;
  71     default:
  72         return ARGP_ERR_UNKNOWN;
  73     }
  74     return 0;
  75 }
  76
  77 void verify_options_set_range(struct verify_options *options, int dim)
  78 {
  79     int r;
  80
  81     if (dim >= VBIGDIM)
  82         r = VSRANGE;
  83     else if (dim >= BIGDIM)
  84         r = SRANGE;
  85     else
  86         r = RANGE;
  87     if (options->M == INT_MIN)
  88         options->M = r;
  89     if (options->m == INT_MAX)
  90         options->m = -r;
  91
  92     if (options->verify && options->m > options->M) {
  93         fprintf(stderr,"Nothing to do: min > max !\n");
  94         exit(0);
  95     }
  96 }
  97
  98 struct argp verify_argp = {
  99     argp_options, parse_opt, 0, 0
 100 };
 101
 102 Polyhedron *check_poly_context_scan(Polyhedron *C,
 103                                     const struct verify_options *options)
 104 {
 105     int i;
 106     Matrix *MM;
 107     Polyhedron *CC, *CS, *U;
 108     unsigned MaxRays = options->barvinok->MaxRays;
 109
 110     if (C->Dimension <= 0)
 111         return NULL;
 112
 113     /* Intersect context with range */
 114     MM = Matrix_Alloc(2*C->Dimension, C->Dimension+2);
 115     for (i = 0; i < C->Dimension; ++i) {
 116         value_set_si(MM->p[2*i][0], 1);
 117         value_set_si(MM->p[2*i][1+i], 1);
 118         value_set_si(MM->p[2*i][1+C->Dimension], -options->m);
 119         value_set_si(MM->p[2*i+1][0], 1);
 120         value_set_si(MM->p[2*i+1][1+i], -1);
 121         value_set_si(MM->p[2*i+1][1+C->Dimension], options->M);
 122     }
 123     CC = AddConstraints(MM->p[0], 2*C->Dimension, C, options->barvinok->MaxRays);
 124     U = Universe_Polyhedron(0);
 125     CS = Polyhedron_Scan(CC, U, MaxRays & POL_NO_DUAL ? 0 : MaxRays);
 126     Polyhedron_Free(U);
 127     Polyhedron_Free(CC);
 128     Matrix_Free(MM);
 129     return CS;
 130 }
 131
 132 void check_poly_init(Polyhedron *C, struct verify_options *options)
 133 {
 134     int d, i;
 135
 136     if (options->print_all)
 137         return;
 138     if (C->Dimension <= 0)
 139         return;
 140
 141     d = options->M - options->m;
 142     if (d > 80)
 143         options->st = 1+d/80;
 144     else
 145         options->st = 1;
 146     for (i = options->m; i <= options->M; i += options->st)
 147         printf(".");
 148     printf( "\r" );
 149     fflush(stdout);
 150 }
 151
 152 /****************************************************/
 153 /* function check_poly :                            */
 154 /* scans the parameter space from Min to Max (all   */
 155 /* directions). Computes the number of points in    */
 156 /* the polytope using both methods, and compare them*/
 157 /* returns 1 on success                             */
 158 /****************************************************/
 159
 160 int check_poly(Polyhedron *CS, const struct check_poly_data *data,
 161                int nparam, int pos, Value *z,
 162                const struct verify_options *options)
 163 {
 164     if (pos == nparam) {
 165         if (!data->check(data, nparam, z, options) && !options->continue_on_error)
 166             return 0;
 167     } else {
 168         Value LB, UB;
 169         int ok;
 170         value_init(LB);
 171         value_init(UB);
 172         ok = !(lower_upper_bounds(1+pos, CS, z-1, &LB, &UB));
 173         assert(ok);
 174         for (; value_le(LB, UB); value_increment(LB, LB)) {
 175             if (!options->print_all) {
 176                 int k = VALUE_TO_INT(LB);
 177                 if (!pos && !(k % options->st)) {
 178                     printf("o");
 179                     fflush(stdout);
 180                 }
 181             }
 182
 183             value_assign(z[pos], LB);
 184             if (!check_poly(CS->next, data, nparam, pos+1, z, options)) {
 185                 value_clear(LB);
 186                 value_clear(UB);
 187                 return 0;
 188             }
 189         }
 190         value_set_si(z[pos], 0);
 191         value_clear(LB);
 192         value_clear(UB);
 193     }
 194     return 1;
 195 } /* check_poly */