update isl for extract_interface
[barvinok.git] / verify_lexsmaller.c
blobd2882b88d42e831b067b36707caa22775e4a2c19
1 #include <assert.h>
2 #include <barvinok/options.h>
3 #include <barvinok/util.h>
5 struct arguments {
6 int live;
7 int print_max;
8 int keep_going;
9 Value max;
10 struct barvinok_options *barvinok;
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
21 ISL_ARG_DEF(arguments, struct arguments, arguments_arg)
23 #define LS_OK 1
24 #define LS_P 2 /* continue searching P */
25 #define LS_D 4 /* continue searching D */
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)
31 int i;
32 int ok;
33 Value PLB, PUB, DLB, DUB, LB, UB, tmp, c;
35 if (!SP && !SD)
36 return LS_OK | LS_P | LS_D;
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);
43 if (SP) {
44 ok = !(lower_upper_bounds(1+pos, SP, zP, &PLB, &PUB));
45 assert(ok);
47 if (SD) {
48 ok = !(lower_upper_bounds(1+pos, SD, zD, &DLB, &DUB));
49 assert(ok);
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);
60 if (SD && !SD->next)
61 value_init(c);
63 ok = LS_OK | LS_P | LS_D;
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;
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);
78 if (inD && !SD->next) {
79 Value *ctmp;
81 value_assign(c,*(ctmp=compute_poly(en, zE)));
82 value_clear(*ctmp);
83 free(ctmp);
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]);
92 printf(" ) = ");
93 value_print(stdout, VALUE_FMT, c);
94 printf("; count = ");
95 value_print(stdout, VALUE_FMT, *count);
96 printf("\n");
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]);
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;
117 if (options->live)
118 value_decrement(*count, *count);
120 ok &= ~LS_D;
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;
141 if (!ok && !options->keep_going)
142 goto end;
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;
151 if (SP)
152 value_set_si(zP[pos+1], 0);
153 if (SD)
154 value_set_si(zD[pos+1], 0);
156 end:
157 if (SD && !SD->next)
158 value_clear(c);
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);
165 return ok;
168 int main(int argc,char *argv[])
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();
183 argc = arguments_parse(options, argc, argv, ISL_ARG_ALL);
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);
194 fgets(s, 128, stdin);
195 while ((*s=='#') || (sscanf(s, "D %u", &dim)<1))
196 fgets(s, 128, stdin);
198 M = Matrix_Read();
199 C = Constraints2Polyhedron(M, options->barvinok->MaxRays);
200 assert(C != NULL);
201 Matrix_Free(M);
203 nb_parms = D->Dimension;
204 param_name = Read_ParamNames(stdin, nb_parms);
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);
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);
224 if (options->barvinok->verbose >= 1) {
225 puts("Enumeration");
226 print_evalue(stdout, EP, (const char **)param_name);
228 en = partition2enumeration(EP);
230 assert(C->Dimension == 0); /* for now */
232 /* S = scanning list of polyhedra */
233 SP = Polyhedron_Scan(P, C, options->barvinok->MaxRays);
234 SD = Polyhedron_Scan(D, C, options->barvinok->MaxRays);
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);
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);
248 if (options->print_max) {
249 printf("max = ");
250 value_print(stdout, VALUE_FMT, options->max);
251 printf("\n");
252 value_clear(options->max);
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;