verify.c

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