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