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