2 #include <NTL/mat_ZZ.h>
4 #include <polylib/polylibgmp.h>
5 #include "ev_operations.h"
11 #include "verif_ehrhart.h"
13 #ifdef HAVE_GROWING_CHERNIKOVA
21 #define getopt_long(a,b,c,d,e) getopt(a,b,c)
24 struct option options
[] = {
25 { "explicit", no_argument
, 0, 'e' },
26 { "series", no_argument
, 0, 's' },
27 { "verbose", no_argument
, 0, 'v' },
28 { "version", no_argument
, 0, 'V' },
33 /* RANGE : normal range for evalutations (-RANGE -> RANGE) */
36 /* SRANGE : small range for evalutations */
39 /* if dimension >= BIDDIM, use SRANGE */
42 /* VSRANGE : very small range for evalutations */
45 /* if dimension >= VBIDDIM, use VSRANGE */
48 int check_series(Polyhedron
*S
,Polyhedron
*C
, gen_fun
*gf
,
49 int nparam
,int pos
,Value
*z
)
57 /* Computes the coefficient */
58 gf
->coefficient(&z
[S
->Dimension
-nparam
+1], &c
);
60 /* if c=0 we may be out of context. */
61 /* scanning is useless in this case*/
62 if(!in_domain(C
,&z
[S
->Dimension
-nparam
+1])) {
66 #ifdef PRINT_ALL_RESULTS
68 value_print(stdout
,VALUE_FMT
,z
[S
->Dimension
-nparam
+1]);
69 for(k
=S
->Dimension
-nparam
+2;k
<=S
->Dimension
;++k
) {
71 value_print(stdout
,VALUE_FMT
,z
[k
]);
74 value_print(stdout
,VALUE_FMT
,c
);
77 /* Manually count the number of points */
78 count_points(1,S
,z
,&tmp
);
79 #ifdef PRINT_ALL_RESULTS
81 value_print(stdout
, P_VALUE_FMT
, tmp
);
88 fprintf(stderr
,"Error !\n");
89 fprintf(stderr
,"EP( ");
90 value_print(stderr
,VALUE_FMT
,z
[S
->Dimension
-nparam
+1]);
91 for(k
=S
->Dimension
-nparam
+2;k
<=S
->Dimension
;++k
) {
93 value_print(stderr
,VALUE_FMT
,z
[k
]);
95 fprintf(stderr
," ) should be ");
96 value_print(stderr
,VALUE_FMT
,tmp
);
97 fprintf(stderr
,", while EP eval gives ");
98 value_print(stderr
,VALUE_FMT
,c
);
99 fprintf(stderr
,".\n");
100 #ifndef DONT_BREAK_ON_ERROR
101 value_clear(c
); value_clear(tmp
);
105 #ifdef PRINT_ALL_RESULTS
111 for(value_assign(tmp
,Min
); value_le(tmp
,Max
);
112 value_increment(tmp
,tmp
)) {
113 #ifndef PRINT_ALL_RESULTS
114 k
= VALUE_TO_INT(tmp
);
115 if(!pos
&& !(k
%st
)) {
120 value_assign(z
[pos
+S
->Dimension
-nparam
+1],tmp
);
121 if(!check_series(S
,C
,gf
,nparam
,pos
+1,z
)) {
122 value_clear(c
); value_clear(tmp
);
132 int main(int argc
,char *argv
[]) {
135 Polyhedron
*C
, *P
, *S
;
140 int m
= INT_MAX
, M
= INT_MIN
, r
;
147 while ((c
= getopt_long(argc
, argv
, "m:M:r:sveV", options
, &ind
)) != -1) {
169 printf(barvinok_version());
175 /******* Read the input *********/
179 if(C1
->NbColumns
< 2) {
180 fprintf(stderr
,"Not enough parameters !\n");
184 P
= Constraints2Polyhedron(P1
,MAXRAYS
);
185 C
= Constraints2Polyhedron(C1
,MAXRAYS
);
186 params
= Read_ParamNames(stdin
, C
->Dimension
);
190 /******* Read the options: initialize Min and Max ********/
191 if(P
->Dimension
>= VBIGDIM
)
193 else if(P
->Dimension
>= BIGDIM
)
204 fprintf(stderr
,"Nothing to do: Min > Max !\n");
213 /******* Compute true context *******/
214 CC
= align_context(C
,P
->Dimension
,MAXRAYS
);
215 PP
= DomainIntersection(P
,CC
,MAXRAYS
);
217 C1
= Matrix_Alloc(C
->Dimension
+1,P
->Dimension
+1);
219 for(i
=0;i
<C1
->NbRows
;i
++)
220 for(j
=0;j
<C1
->NbColumns
;j
++)
221 if(i
==j
-P
->Dimension
+C
->Dimension
)
222 value_set_si(C1
->p
[i
][j
],1);
224 value_set_si(C1
->p
[i
][j
],0);
225 CC
= Polyhedron_Image(PP
,C1
,MAXRAYS
);
233 /******* Compute EP *********/
235 en
= barvinok_enumerate(P
,C
,MAXRAYS
);
238 gf
= barvinok_series(P
, C
, MAXRAYS
);
240 gf
->print(C
->Dimension
, params
);
245 en
= partition2enumeration(EP
);
249 /******* Initializations for check *********/
250 p
= (Value
*)malloc(sizeof(Value
) * (P
->Dimension
+2));
251 for(i
=0;i
<=P
->Dimension
;i
++) {
253 value_set_si(p
[i
],0);
256 value_set_si(p
[i
],1);
258 /* S = scanning list of polyhedra */
259 S
= Polyhedron_Scan(P
,C
,MAXRAYS
);
261 #ifndef PRINT_ALL_RESULTS
262 if(C
->Dimension
> 0) {
263 value_subtract(tmp
,Max
,Min
);
264 if (VALUE_TO_INT(tmp
) > 80)
265 st
= 1+(VALUE_TO_INT(tmp
))/80;
268 for(i
=VALUE_TO_INT(Min
);i
<=VALUE_TO_INT(Max
);i
+=st
)
275 /******* CHECK NOW *********/
277 if (!series
|| function
) {
278 if (!check_poly(S
,C
,en
,C
->Dimension
,0,p
))
281 if (!check_series(S
,C
,gf
,C
->Dimension
,0,p
))
288 fprintf(stderr
,"Check failed !\n");
290 #ifndef PRINT_ALL_RESULTS
297 for(i
=0;i
<=(P
->Dimension
+1);i
++)
301 Free_ParamNames(params
, C
->Dimension
);