verify.c

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