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 static void print_rational(FILE *out, Value n, Value d)
 170 {
 171     value_print(out, VALUE_FMT, n);
 172     if (value_notone_p(d)) {
 173         fprintf(out, "/");
 174         value_print(out, VALUE_FMT, d);
 175     }
 176 }
 177
 178 void check_poly_print(int ok, int nparam, Value *z,
 179                       Value want_n, Value want_d,
 180                       Value got_n, Value got_d,
 181                       const char *op, const char *check,
 182                       const char *long_op,
 183                       const struct verify_options *options)
 184 {
 185     int k;
 186
 187     if (options->print_all) {
 188         printf("%s(", op);
 189         value_print(stdout, VALUE_FMT, z[0]);
 190         for (k = 1; k < nparam; ++k) {
 191             printf(", ");
 192             value_print(stdout, VALUE_FMT, z[k]);
 193         }
 194         printf(") = ");
 195         print_rational(stdout, got_n, got_d);
 196         printf(", %s = ", check);
 197         print_rational(stdout, want_n, want_d);
 198         printf(". ");
 199     }
 200
 201     if (!ok) {
 202         printf("\n");
 203         fflush(stdout);
 204         fprintf(stderr, "Error !\n");
 205         fprintf(stderr, "%s(", op);
 206         value_print(stderr, VALUE_FMT, z[0]);
 207         for (k = 1; k < nparam; ++k) {
 208             fprintf(stderr,", ");
 209             value_print(stderr, VALUE_FMT, z[k]);
 210         }
 211         fprintf(stderr, ") should be ");
 212         print_rational(stderr, want_n, want_d);
 213         fprintf(stderr, ", while %s gives ", long_op);
 214         print_rational(stderr, got_n, got_d);
 215         fprintf(stderr, ".\n");
 216     } else if (options->print_all)
 217         printf("OK.\n");
 218 }
 219
 220 /****************************************************/
 221 /* function check_poly :                            */
 222 /* scans the parameter space from Min to Max (all   */
 223 /* directions). Computes the number of points in    */
 224 /* the polytope using both methods, and compare them*/
 225 /* returns 1 on success                             */
 226 /****************************************************/
 227
 228 int check_poly(Polyhedron *CS, const struct check_poly_data *data,
 229                int nparam, int pos, Value *z,
 230                const struct verify_options *options)
 231 {
 232     if (pos == nparam) {
 233         if (!data->check(data, nparam, z, options) && !options->continue_on_error)
 234             return 0;
 235     } else {
 236         Value LB, UB;
 237         int ok;
 238         value_init(LB);
 239         value_init(UB);
 240         ok = !(lower_upper_bounds(1+pos, CS, z-1, &LB, &UB));
 241         assert(ok);
 242         for (; value_le(LB, UB); value_increment(LB, LB)) {
 243             if (!options->print_all) {
 244                 int k = VALUE_TO_INT(LB);
 245                 if (!pos && !(k % options->st)) {
 246                     printf("o");
 247                     fflush(stdout);
 248                 }
 249             }
 250
 251             value_assign(z[pos], LB);
 252             if (!check_poly(CS->next, data, nparam, pos+1, z, options)) {
 253                 value_clear(LB);
 254                 value_clear(UB);
 255                 return 0;
 256             }
 257         }
 258         value_set_si(z[pos], 0);
 259         value_clear(LB);
 260         value_clear(UB);
 261     }
 262     return 1;
 263 } /* check_poly */