use isl for code generation
[barvinok.git] / verify_lexsmaller.c
blob65c57420dc1b0eda90d77558255e7a7665839375
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 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
20 ISL_ARG_DEF(arguments, struct arguments, arguments_args)
22 #define LS_OK 1
23 #define LS_P 2 /* continue searching P */
24 #define LS_D 4 /* continue searching D */
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)
30 int i;
31 int ok;
32 Value PLB, PUB, DLB, DUB, LB, UB, tmp, c;
34 if (!SP && !SD)
35 return LS_OK | LS_P | LS_D;
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);
42 if (SP) {
43 ok = !(lower_upper_bounds(1+pos, SP, zP, &PLB, &PUB));
44 assert(ok);
46 if (SD) {
47 ok = !(lower_upper_bounds(1+pos, SD, zD, &DLB, &DUB));
48 assert(ok);
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);
59 if (SD && !SD->next)
60 value_init(c);
62 ok = LS_OK | LS_P | LS_D;
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;
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);
77 if (inD && !SD->next) {
78 Value *ctmp;
80 value_assign(c,*(ctmp=compute_poly(en, zE)));
81 value_clear(*ctmp);
82 free(ctmp);
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]);
91 printf(" ) = ");
92 value_print(stdout, VALUE_FMT, c);
93 printf("; count = ");
94 value_print(stdout, VALUE_FMT, *count);
95 printf("\n");
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]);
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;
116 if (options->live)
117 value_decrement(*count, *count);
119 ok &= ~LS_D;
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;
140 if (!ok && !options->keep_going)
141 goto end;
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;
150 if (SP)
151 value_set_si(zP[pos+1], 0);
152 if (SD)
153 value_set_si(zD[pos+1], 0);
155 end:
156 if (SD && !SD->next)
157 value_clear(c);
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);
164 return ok;
167 int main(int argc,char *argv[])
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();
182 argc = arguments_parse(options, argc, argv, ISL_ARG_ALL);
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);
193 fgets(s, 128, stdin);
194 while ((*s=='#') || (sscanf(s, "D %u", &dim)<1))
195 fgets(s, 128, stdin);
197 M = Matrix_Read();
198 C = Constraints2Polyhedron(M, options->barvinok->MaxRays);
199 assert(C != NULL);
200 Matrix_Free(M);
202 nb_parms = D->Dimension;
203 param_name = Read_ParamNames(stdin, nb_parms);
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);
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);
223 if (options->barvinok->verbose >= 1) {
224 puts("Enumeration");
225 print_evalue(stdout, EP, (const char **)param_name);
227 en = partition2enumeration(EP);
229 assert(C->Dimension == 0); /* for now */
231 /* S = scanning list of polyhedra */
232 SP = Polyhedron_Scan(P, C, options->barvinok->MaxRays);
233 SD = Polyhedron_Scan(D, C, options->barvinok->MaxRays);
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);
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);
247 if (options->print_max) {
248 printf("max = ");
249 value_print(stdout, VALUE_FMT, options->max);
250 printf("\n");
251 value_clear(options->max);
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;