verify_lexsmaller.c

   1 #include <assert.h>
   2 #include <barvinok/options.h>
   3 #include <barvinok/util.h>
   4
   5 struct arguments {
   6     int live;
   7     int print_max;
   8     int keep_going;
   9     Value max;
  10     struct barvinok_options     *barvinok;
  11 };
  12
  13 ISL_ARGS_START(struct arguments, arguments_args)
  14 ISL_ARG_CHILD(struct arguments, barvinok, NULL, &barvinok_options_args, NULL)
  15 ISL_ARG_BOOL(struct arguments, live, 'l', "live", 0, NULL)
  16 ISL_ARG_BOOL(struct arguments, print_max, 'M', "max", 0, NULL)
  17 ISL_ARG_BOOL(struct arguments, keep_going, 'k', "continue", 0, NULL)
  18 ISL_ARGS_END
  19
  20 ISL_ARG_DEF(arguments, struct arguments, arguments_args)
  21
  22 #define LS_OK       1
  23 #define LS_P        2       /* continue searching P */
  24 #define LS_D        4       /* continue searching D */
  25
  26 static int check_lexsmaller(Polyhedron *SP, Polyhedron *SD, Enumeration *en,
  27                          int pos, int nvar, Value *zP, Value *zD, Value *zE,
  28                          Value *count, struct arguments *options)
  29 {
  30     int i;
  31     int ok;
  32     Value PLB, PUB, DLB, DUB, LB, UB, tmp, c;
  33
  34     if (!SP && !SD)
  35         return LS_OK | LS_P | LS_D;
  36
  37     value_init(PLB); value_init(PUB);
  38     value_init(DLB); value_init(DUB);
  39     value_init(LB); value_init(UB);
  40     value_init(tmp);
  41
  42     if (SP) {
  43         ok = !(lower_upper_bounds(1+pos, SP, zP, &PLB, &PUB));
  44         assert(ok);
  45     }
  46     if (SD) {
  47         ok = !(lower_upper_bounds(1+pos, SD, zD, &DLB, &DUB));
  48         assert(ok);
  49     }
  50     if (!SD || (SP && value_lt(PLB, DLB)))
  51         value_assign(LB, PLB);
  52     else
  53         value_assign(LB, DLB);
  54     if (!SD || (SP && value_gt(PUB, DUB)))
  55         value_assign(UB, PUB);
  56     else
  57         value_assign(UB, DUB);
  58
  59     if (SD && !SD->next)
  60         value_init(c);
  61
  62     ok = LS_OK | LS_P | LS_D;
  63
  64     for(value_assign(tmp,LB); value_le(tmp,UB); value_increment(tmp,tmp)) {
  65         int inP = SP && value_ge(tmp, PLB) && value_le(tmp, PUB);
  66         int inD = SD && value_ge(tmp, DLB) && value_le(tmp, DUB);
  67         if (!inP && !inD)
  68             continue;
  69
  70         if (inP)
  71             value_assign(zP[pos+1], tmp);
  72         if (inD)
  73             value_assign(zD[pos+1], tmp);
  74         if (inD && pos < nvar)
  75             value_assign(zE[pos], tmp);
  76
  77         if (inD && !SD->next) {
  78             Value *ctmp;
  79
  80             value_assign(c,*(ctmp=compute_poly(en, zE)));
  81             value_clear(*ctmp);
  82             free(ctmp);
  83
  84             if (options->barvinok->verbose >= 2) {
  85                 printf("EP( ");
  86                 value_print(stdout, VALUE_FMT, zE[0]);
  87                 for (i = 1; i < nvar; ++i) {
  88                     printf(", ");
  89                     value_print(stdout, VALUE_FMT, zE[i]);
  90                 }
  91                 printf(" ) = ");
  92                 value_print(stdout, VALUE_FMT, c);
  93                 printf("; count = ");
  94                 value_print(stdout, VALUE_FMT, *count);
  95                 printf("\n");
  96             }
  97
  98             if (value_ne(c, *count)) {
  99                 printf("\n");
 100                 fflush(stdout);
 101                 fprintf(stderr,"Error !\n");
 102                 fprintf(stderr, "EP( ");
 103                 value_print(stderr, VALUE_FMT, zE[0]);
 104                 for (i = 1; i < nvar; ++i) {
 105                     fprintf(stderr, ", ");
 106                     value_print(stderr, VALUE_FMT, zE[i]);
 107                 }
 108                 fprintf(stderr, " ) = ");
 109                 value_print(stderr, VALUE_FMT, c);
 110                 fprintf(stderr, " but count = ");
 111                 value_print(stderr, VALUE_FMT, *count);
 112                 printf("\n");
 113                 ok = 0;
 114             }
 115
 116             if (options->live)
 117                 value_decrement(*count, *count);
 118
 119             ok &= ~LS_D;
 120         }
 121
 122         if (pos < nvar-1)
 123             ok &= check_lexsmaller(inP ? SP->next : NULL,
 124                                    inD ? SD->next : NULL,
 125                                    en, pos+1, nvar, zP, zD, zE, count,
 126                                    options);
 127         else {
 128             ok &= check_lexsmaller(NULL, inD ? SD->next : NULL,
 129                                    en, pos+1, nvar, zP, zD, zE, count,
 130                                    options)
 131                &  check_lexsmaller(inP ? SP->next : NULL, NULL,
 132                                    en, pos+1, nvar, zP, zD, zE, count,
 133                                    options);
 134             if (pos >= nvar && !(ok & LS_D))
 135                 break;
 136             if (pos >= nvar && !(ok & LS_P))
 137                 break;
 138         }
 139
 140         if (!ok && !options->keep_going)
 141             goto end;
 142
 143         if (inP && !SP->next) {
 144             value_increment(*count, *count);
 145             if (value_gt(*count, options->max))
 146                 value_assign(options->max, *count);
 147             ok &= ~LS_P;
 148         }
 149     }
 150     if (SP)
 151         value_set_si(zP[pos+1], 0);
 152     if (SD)
 153         value_set_si(zD[pos+1], 0);
 154
 155 end:
 156     if (SD && !SD->next)
 157         value_clear(c);
 158
 159     value_clear(PLB); value_clear(PUB);
 160     value_clear(DLB); value_clear(DUB);
 161     value_clear(LB); value_clear(UB);
 162     value_clear(tmp);
 163
 164     return ok;
 165 }
 166
 167 int main(int argc,char *argv[])
 168 {
 169     Matrix *M;
 170     Polyhedron *P, *D, *C;
 171     Polyhedron *SP, *SD;
 172     int nb_parms;
 173     const char **param_name = NULL;
 174     evalue *EP;
 175     Enumeration *en;
 176     Vector *zP, *zD, *zE;
 177     Value count;
 178     char s[128];
 179     unsigned dim;
 180     struct arguments *options = arguments_new_with_defaults();
 181
 182     argc = arguments_parse(options, argc, argv, ISL_ARG_ALL);
 183
 184     M = Matrix_Read();
 185     P = Constraints2Polyhedron(M, options->barvinok->MaxRays);
 186     assert(P != NULL);
 187     Matrix_Free(M);
 188     M = Matrix_Read();
 189     D = Constraints2Polyhedron(M, options->barvinok->MaxRays);
 190     assert(D != NULL);
 191     Matrix_Free(M);
 192
 193     fgets(s, 128, stdin);
 194     while ((*s=='#') || (sscanf(s, "D %u", &dim)<1))
 195         fgets(s, 128, stdin);
 196
 197     M = Matrix_Read();
 198     C = Constraints2Polyhedron(M, options->barvinok->MaxRays);
 199     assert(C != NULL);
 200     Matrix_Free(M);
 201
 202     nb_parms = D->Dimension;
 203     param_name = Read_ParamNames(stdin, nb_parms);
 204
 205     EP = barvinok_lexsmaller_ev(P, D, dim, C, options->barvinok->MaxRays);
 206     if (options->live) {
 207         evalue mone;
 208         evalue *EC = barvinok_lexsmaller_ev(D, D, dim, C, options->barvinok->MaxRays);
 209         if (options->barvinok->verbose >= 2) {
 210             puts("EP");
 211             print_evalue(stdout, EP, (const char **)param_name);
 212             puts("EC");
 213             print_evalue(stdout, EC, (const char **)param_name);
 214         }
 215         value_init(mone.d);
 216         evalue_set_si(&mone, -1, 1);
 217         emul(&mone, EC);
 218         eadd(EC, EP);
 219         free_evalue_refs(&mone);
 220         evalue_free(EC);
 221         reduce_evalue(EP);
 222     }
 223     if (options->barvinok->verbose >= 1) {
 224         puts("Enumeration");
 225         print_evalue(stdout, EP, (const char **)param_name);
 226     }
 227     en = partition2enumeration(EP);
 228
 229     assert(C->Dimension == 0); /* for now */
 230
 231     /* S = scanning list of polyhedra */
 232     SP = Polyhedron_Scan(P, C, options->barvinok->MaxRays);
 233     SD = Polyhedron_Scan(D, C, options->barvinok->MaxRays);
 234
 235     zP = Vector_Alloc(1+P->Dimension+1);
 236     value_set_si(zP->p[1+P->Dimension], 1);
 237     zD = Vector_Alloc(1+D->Dimension+1);
 238     value_set_si(zD->p[1+D->Dimension], 1);
 239     zE = Vector_Alloc(dim+C->Dimension);
 240
 241     if (options->print_max)
 242         value_init(options->max);
 243     value_init(count);
 244     check_lexsmaller(SP, SD, en, 0, dim, zP->p, zD->p, zE->p, &count, options);
 245     value_clear(count);
 246
 247     if (options->print_max) {
 248         printf("max = ");
 249         value_print(stdout, VALUE_FMT, options->max);
 250         printf("\n");
 251         value_clear(options->max);
 252     }
 253
 254     Enumeration_Free(en);
 255     Free_ParamNames(param_name, nb_parms);
 256     Polyhedron_Free(P);
 257     Polyhedron_Free(D);
 258     Polyhedron_Free(C);
 259     Domain_Free(SP);
 260     Domain_Free(SD);
 261     Vector_Free(zP);
 262     Vector_Free(zD);
 263     Vector_Free(zE);
 264     arguments_free(options);
 265     return 0;
 266 }