3 #include <barvinok/evalue.h>
4 #include <barvinok/util.h>
5 #include <barvinok/barvinok.h>
9 #include "verif_ehrhart.h"
10 #include "remove_equalities.h"
11 #include "evalue_convert.h"
12 #include "conversion.h"
14 #undef CS /* for Solaris 10 */
19 /* The input of this example program is the same as that of testehrhart
20 * in the PolyLib distribution, i.e., a polytope in combined
21 * data and parameter space, a context polytope in parameter space
22 * and (optionally) the names of the parameters.
23 * Both polytopes are in PolyLib notation.
26 #define PRINT_STATS (BV_OPT_LAST+1)
28 struct argp_option argp_options
[] = {
30 { "series", 's', 0, 0, "compute rational generating function" },
31 { "explicit", 'e', 0, 0, "convert rgf to psp" },
33 { "print-stats", PRINT_STATS
, 0, 0 },
43 struct verify_options verify
;
44 struct convert_options convert
;
47 static error_t
parse_opt(int key
, char *arg
, struct argp_state
*state
)
49 struct arguments
*options
= (struct arguments
*) state
->input
;
53 state
->child_inputs
[0] = options
->verify
.barvinok
;
54 state
->child_inputs
[1] = &options
->verify
;
55 state
->child_inputs
[2] = &options
->convert
;
58 options
->function
= 0;
60 options
->print_stats
= 0;
63 options
->print_stats
= 1;
69 options
->function
= 1;
78 return ARGP_ERR_UNKNOWN
;
83 struct skewed_gen_fun
{
85 /* maps original space to space in which gf is defined */
87 /* equalities in the original space that need to be satisfied for
91 /* divisibilities in the original space that need to be satisfied for
96 skewed_gen_fun(gen_fun
*gf
, Matrix
*T
, Matrix
*eq
, Matrix
*div
) :
97 gf(gf
), T(T
), eq(eq
), div(div
) {}
108 void print(std::ostream
& os
, unsigned int nparam
, char **param_name
) const;
109 operator evalue
*() const {
110 assert(T
== NULL
&& eq
== NULL
); /* other cases not supported for now */
113 void coefficient(Value
* params
, Value
* c
, barvinok_options
*options
) const;
116 void skewed_gen_fun::print(std::ostream
& os
, unsigned int nparam
,
117 char **param_name
) const
122 matrix2zz(T
, m
, T
->NbRows
, T
->NbColumns
);
127 matrix2zz(eq
, m
, eq
->NbRows
, eq
->NbColumns
);
131 os
<< "div:" << endl
;
132 matrix2zz(div
, m
, div
->NbRows
, div
->NbColumns
);
135 gf
->print(os
, nparam
, param_name
);
138 void skewed_gen_fun::coefficient(Value
* params
, Value
* c
,
139 barvinok_options
*options
) const
142 for (int i
= 0; i
< eq
->NbRows
; ++i
) {
143 Inner_Product(eq
->p
[i
]+1, params
, eq
->NbColumns
-2, eq
->p
[i
]);
144 if (value_notzero_p(eq
->p
[i
][0])) {
153 for (int i
= 0; i
< div
->NbRows
; ++i
) {
154 Inner_Product(div
->p
[i
], params
, div
->NbColumns
-1, &tmp
);
155 if (!mpz_divisible_p(tmp
, div
->p
[i
][div
->NbColumns
-1])) {
165 coeff
= gf
->coefficient(params
, options
);
167 Vector
*p2
= Vector_Alloc(T
->NbRows
);
168 Matrix_Vector_Product(T
, params
, p2
->p
);
169 if (value_notone_p(p2
->p
[T
->NbRows
-1]))
170 Vector_AntiScale(p2
->p
, p2
->p
, p2
->p
[T
->NbRows
-1], T
->NbRows
);
171 coeff
= gf
->coefficient(p2
->p
, options
);
178 static int check_series(Polyhedron
*S
, Polyhedron
*CS
, skewed_gen_fun
*gf
,
179 int nparam
, int pos
, Value
*z
, verify_options
*options
)
191 /* Computes the coefficient */
192 gf
->coefficient(&z
[S
->Dimension
-nparam
+1], &c
, options
->barvinok
);
194 /* if c=0 we may be out of context. */
195 /* scanning is useless in this case*/
197 if (options
->print_all
) {
199 value_print(stdout
,VALUE_FMT
,z
[S
->Dimension
-nparam
+1]);
200 for(k
=S
->Dimension
-nparam
+2;k
<=S
->Dimension
;++k
) {
202 value_print(stdout
,VALUE_FMT
,z
[k
]);
205 value_print(stdout
,VALUE_FMT
,c
);
209 /* Manually count the number of points */
210 count_points(1,S
,z
,&tmp
);
211 if (options
->print_all
) {
212 printf(", count = ");
213 value_print(stdout
, P_VALUE_FMT
, tmp
);
217 if (value_ne(tmp
,c
)) {
220 fprintf(stderr
,"Error !\n");
221 fprintf(stderr
,"EP( ");
222 value_print(stderr
,VALUE_FMT
,z
[S
->Dimension
-nparam
+1]);
223 for (k
=S
->Dimension
-nparam
+2;k
<=S
->Dimension
;++k
) {
224 fprintf(stderr
,", ");
225 value_print(stderr
,VALUE_FMT
,z
[k
]);
227 fprintf(stderr
," ) should be ");
228 value_print(stderr
,VALUE_FMT
,tmp
);
229 fprintf(stderr
,", while EP eval gives ");
230 value_print(stderr
,VALUE_FMT
,c
);
231 fprintf(stderr
,".\n");
232 if (!options
->continue_on_error
) {
233 value_clear(c
); value_clear(tmp
);
236 } else if (options
->print_all
)
240 !(lower_upper_bounds(1+pos
, CS
, &z
[S
->Dimension
-nparam
], &LB
, &UB
));
242 for (value_assign(tmp
,LB
); value_le(tmp
,UB
); value_increment(tmp
,tmp
)) {
243 if (!options
->print_all
) {
244 k
= VALUE_TO_INT(tmp
);
245 if(!pos
&& !(k
% options
->st
)) {
250 value_assign(z
[pos
+S
->Dimension
-nparam
+1],tmp
);
251 if (!check_series(S
, CS
->next
, gf
, nparam
, pos
+1, z
, options
)) {
252 value_clear(c
); value_clear(tmp
);
258 value_set_si(z
[pos
+S
->Dimension
-nparam
+1],0);
268 static int verify(Polyhedron
*P
, Polyhedron
*C
, evalue
*EP
, skewed_gen_fun
*gf
,
275 CS
= check_poly_context_scan(P
, &C
, C
->Dimension
, &options
->verify
);
277 p
= Vector_Alloc(P
->Dimension
+2);
278 value_set_si(p
->p
[P
->Dimension
+1], 1);
280 /* S = scanning list of polyhedra */
281 S
= Polyhedron_Scan(P
, C
, options
->verify
.barvinok
->MaxRays
);
283 check_poly_init(C
, &options
->verify
);
285 /******* CHECK NOW *********/
287 if (!options
->series
|| options
->function
) {
288 if (!check_poly_EP(S
, CS
, EP
, 0, C
->Dimension
, 0, p
->p
,
292 if (!check_series(S
, CS
, gf
, C
->Dimension
, 0, p
->p
, &options
->verify
))
299 fprintf(stderr
,"Check failed !\n");
301 if (!options
->verify
.print_all
)
313 /* frees M and Minv */
314 static void apply_transformation(Polyhedron
**P
, Polyhedron
**C
,
315 bool free_P
, bool free_C
,
316 Matrix
*M
, Matrix
*Minv
, Matrix
**inv
,
317 barvinok_options
*options
)
322 M2
= align_matrix(M
, (*P
)->Dimension
+ 1);
324 *P
= Polyhedron_Preimage(*P
, M2
, options
->MaxRays
);
330 *C
= Polyhedron_Preimage(*C
, M
, options
->MaxRays
);
338 *inv
= Matrix_Alloc(Minv
->NbRows
, T
->NbColumns
);
339 Matrix_Product(Minv
, T
, *inv
);
346 /* Since we have "compressed" the parameters (in case there were
347 * any equalities), the result is independent of the coordinates in the
348 * coordinate subspace spanned by the lines. We can therefore assume
349 * these coordinates are zero and compute the inverse image of the map
350 * from a lower dimensional space that adds zeros in the appropriate
353 static void remove_lines(Polyhedron
*C
, Matrix
**M
, Matrix
**Minv
)
355 Matrix
*L
= Matrix_Alloc(C
->Dimension
+1, C
->Dimension
+1);
356 for (int r
= 0; r
< C
->NbBid
; ++r
)
357 Vector_Copy(C
->Ray
[r
]+1, L
->p
[r
], C
->Dimension
);
358 unimodular_complete(L
, C
->NbBid
);
359 assert(value_one_p(L
->p
[C
->Dimension
][C
->Dimension
]));
360 assert(First_Non_Zero(L
->p
[C
->Dimension
], C
->Dimension
) == -1);
361 Matrix_Transposition(L
);
362 assert(First_Non_Zero(L
->p
[C
->Dimension
], C
->Dimension
) == -1);
364 *M
= Matrix_Alloc(C
->Dimension
+1, C
->Dimension
-C
->NbBid
+1);
365 for (int i
= 0; i
< C
->Dimension
+1; ++i
)
366 Vector_Copy(L
->p
[i
]+C
->NbBid
, (*M
)->p
[i
], C
->Dimension
-C
->NbBid
+1);
368 Matrix
*Linv
= Matrix_Alloc(C
->Dimension
+1, C
->Dimension
+1);
369 int ok
= Matrix_Inverse(L
, Linv
);
373 *Minv
= Matrix_Alloc(C
->Dimension
-C
->NbBid
+1, C
->Dimension
+1);
374 for (int i
= C
->NbBid
; i
< C
->Dimension
+1; ++i
)
375 Vector_AntiScale(Linv
->p
[i
], (*Minv
)->p
[i
-C
->NbBid
],
376 Linv
->p
[C
->Dimension
][C
->Dimension
], C
->Dimension
+1);
380 static skewed_gen_fun
*series(Polyhedron
*P
, Polyhedron
* C
,
381 barvinok_options
*options
)
390 /* Compute true context */
391 C1
= Polyhedron_Project(P
, C
->Dimension
);
392 C2
= DomainIntersection(C
, C1
, options
->MaxRays
);
395 POL_ENSURE_VERTICES(C2
);
396 if (C2
->NbBid
!= 0) {
398 Matrix
*M
, *Minv
, *M2
;
400 if (C2
->NbEq
|| P
->NbEq
) {
401 /* We remove all equalities to be sure all lines are unit vectors */
403 remove_all_equalities(&PT
, &CT
, &CP
, NULL
, C2
->Dimension
,
410 inv
= left_inverse(CP
, &eq
);
416 div
= Matrix_Alloc(inv
->NbRows
-1, inv
->NbColumns
+1);
417 for (int i
= 0; i
< inv
->NbRows
-1; ++i
) {
418 Vector_Gcd(inv
->p
[i
], inv
->NbColumns
, &tmp
);
419 if (mpz_divisible_p(tmp
,
420 inv
->p
[inv
->NbRows
-1][inv
->NbColumns
-1]))
422 Vector_Copy(inv
->p
[i
], div
->p
[d
], inv
->NbColumns
);
423 value_assign(div
->p
[d
][inv
->NbColumns
],
424 inv
->p
[inv
->NbRows
-1][inv
->NbColumns
-1]);
436 POL_ENSURE_VERTICES(C2
);
440 remove_lines(C2
, &M
, &Minv
);
441 apply_transformation(&PT
, &C2
, PT
!= P
, C2
!= C
, M
, Minv
, &inv
,
445 POL_ENSURE_VERTICES(C2
);
446 if (!Polyhedron_has_revlex_positive_rays(C2
, C2
->Dimension
)) {
450 Constraints
= Matrix_Alloc(C2
->NbConstraints
, C2
->Dimension
+1);
451 for (int i
= 0; i
< C2
->NbConstraints
; ++i
)
452 Vector_Copy(C2
->Constraint
[i
]+1, Constraints
->p
[i
], C2
->Dimension
);
453 left_hermite(Constraints
, &H
, &Q
, &U
);
454 Matrix_Free(Constraints
);
456 for (int i
= 0; i
< C2
->Dimension
/2; ++i
)
457 Vector_Exchange(Q
->p
[i
], Q
->p
[C2
->Dimension
-1-i
], C2
->Dimension
);
460 Matrix
*M
= Matrix_Alloc(C2
->Dimension
+1, C2
->Dimension
+1);
462 int ok
= Matrix_Inverse(U
, M
);
466 apply_transformation(&PT
, &C2
, PT
!= P
, C2
!= C
, M
, Q
, &inv
, options
);
468 gf
= barvinok_series_with_options(PT
, C2
, options
);
472 return new skewed_gen_fun(gf
, inv
, eq
, div
);
475 int main(int argc
, char **argv
)
480 skewed_gen_fun
*gf
= NULL
;
482 int print_solution
= 1;
484 struct arguments options
;
485 static struct argp_child argp_children
[] = {
486 { &barvinok_argp
, 0, 0, 0 },
487 { &verify_argp
, 0, "verification", BV_GRP_LAST
+1 },
488 { &convert_argp
, 0, "output conversion", BV_GRP_LAST
+2 },
491 static struct argp argp
= { argp_options
, parse_opt
, 0, 0, argp_children
};
492 struct barvinok_options
*bv_options
= barvinok_options_new_with_defaults();
494 options
.verify
.barvinok
= bv_options
;
495 set_program_name(argv
[0]);
496 argp_parse(&argp
, argc
, argv
, 0, 0, &options
);
499 A
= Constraints2Polyhedron(M
, bv_options
->MaxRays
);
502 C
= Constraints2Polyhedron(M
, bv_options
->MaxRays
);
504 param_name
= Read_ParamNames(stdin
, C
->Dimension
);
506 if (options
.verify
.verify
) {
507 verify_options_set_range(&options
.verify
, A
->Dimension
);
508 if (!options
.verbose
)
512 if (print_solution
&& options
.verbose
) {
513 Polyhedron_Print(stdout
, P_VALUE_FMT
, A
);
514 Polyhedron_Print(stdout
, P_VALUE_FMT
, C
);
517 if (options
.series
) {
518 gf
= series(A
, C
, bv_options
);
519 if (print_solution
) {
520 gf
->print(cout
, C
->Dimension
, param_name
);
523 if (options
.function
) {
526 print_evalue(stdout
, EP
, param_name
);
529 EP
= barvinok_enumerate_with_options(A
, C
, bv_options
);
530 if (evalue_convert(EP
, &options
.convert
, options
.verbose
, C
->Dimension
,
534 printf("\nSize: %d\n", evalue_size(EP
));
536 print_evalue(stdout
, EP
, param_name
);
539 if (options
.verify
.verify
) {
540 options
.verify
.params
= param_name
;
541 result
= verify(A
, C
, EP
, gf
, &options
);
547 free_evalue_refs(EP
);
551 if (options
.print_stats
)
552 barvinok_stats_print(options
.verify
.barvinok
->stats
, stdout
);
554 Free_ParamNames(param_name
, C
->Dimension
);
557 barvinok_options_free(bv_options
);