3 #include <barvinok/barvinok.h>
13 { BV_APPROX_SIGN_NONE
, BV_APPROX_NONE
, 0 },
14 { BV_APPROX_SIGN_APPROX
, BV_APPROX_BERNOULLI
, 0 },
15 { BV_APPROX_SIGN_APPROX
, BV_APPROX_DROP
, 0 },
16 { BV_APPROX_SIGN_APPROX
, BV_APPROX_VOLUME
, BV_VOL_LIFT
},
17 { BV_APPROX_SIGN_APPROX
, BV_APPROX_VOLUME
, BV_VOL_VERTEX
},
18 { BV_APPROX_SIGN_APPROX
, BV_APPROX_VOLUME
, BV_VOL_BARYCENTER
},
19 { BV_APPROX_SIGN_APPROX
, BV_APPROX_SCALE
, 0 },
20 { BV_APPROX_SIGN_APPROX
, BV_APPROX_SCALE
, BV_APPROX_SCALE_CHAMBER
},
21 { BV_APPROX_SIGN_APPROX
, BV_APPROX_SCALE
, BV_APPROX_SCALE_FAST
},
22 { BV_APPROX_SIGN_APPROX
, BV_APPROX_SCALE
, BV_APPROX_SCALE_FAST
| BV_APPROX_SCALE_CHAMBER
},
23 { BV_APPROX_SIGN_LOWER
, BV_APPROX_DROP
, 0 },
24 { BV_APPROX_SIGN_LOWER
, BV_APPROX_VOLUME
, BV_VOL_LIFT
},
25 { BV_APPROX_SIGN_LOWER
, BV_APPROX_VOLUME
, BV_VOL_VERTEX
},
26 { BV_APPROX_SIGN_LOWER
, BV_APPROX_VOLUME
, BV_VOL_BARYCENTER
},
27 { BV_APPROX_SIGN_LOWER
, BV_APPROX_SCALE
, 0 },
28 { BV_APPROX_SIGN_LOWER
, BV_APPROX_SCALE
, BV_APPROX_SCALE_CHAMBER
},
29 { BV_APPROX_SIGN_LOWER
, BV_APPROX_SCALE
, BV_APPROX_SCALE_FAST
},
30 { BV_APPROX_SIGN_LOWER
, BV_APPROX_SCALE
, BV_APPROX_SCALE_FAST
| BV_APPROX_SCALE_CHAMBER
},
31 { BV_APPROX_SIGN_LOWER
, BV_APPROX_SCALE
, BV_APPROX_SCALE_NARROW
},
32 { BV_APPROX_SIGN_LOWER
, BV_APPROX_SCALE
, BV_APPROX_SCALE_NARROW
| BV_APPROX_SCALE_CHAMBER
},
33 { BV_APPROX_SIGN_LOWER
, BV_APPROX_SCALE
, BV_APPROX_SCALE_FAST
| BV_APPROX_SCALE_NARROW
},
34 { BV_APPROX_SIGN_LOWER
, BV_APPROX_SCALE
, BV_APPROX_SCALE_FAST
| BV_APPROX_SCALE_NARROW
| BV_APPROX_SCALE_CHAMBER
},
35 { BV_APPROX_SIGN_LOWER
, BV_APPROX_SCALE
, BV_APPROX_SCALE_NARROW2
},
36 { BV_APPROX_SIGN_LOWER
, BV_APPROX_SCALE
, BV_APPROX_SCALE_NARROW2
| BV_APPROX_SCALE_CHAMBER
},
37 { BV_APPROX_SIGN_LOWER
, BV_APPROX_SCALE
, BV_APPROX_SCALE_FAST
| BV_APPROX_SCALE_NARROW2
},
38 { BV_APPROX_SIGN_LOWER
, BV_APPROX_SCALE
, BV_APPROX_SCALE_FAST
| BV_APPROX_SCALE_NARROW2
| BV_APPROX_SCALE_CHAMBER
},
39 { BV_APPROX_SIGN_UPPER
, BV_APPROX_DROP
, 0 },
40 { BV_APPROX_SIGN_UPPER
, BV_APPROX_VOLUME
, BV_VOL_LIFT
},
41 { BV_APPROX_SIGN_UPPER
, BV_APPROX_VOLUME
, BV_VOL_VERTEX
},
42 { BV_APPROX_SIGN_UPPER
, BV_APPROX_VOLUME
, BV_VOL_BARYCENTER
},
43 { BV_APPROX_SIGN_UPPER
, BV_APPROX_SCALE
, 0 },
44 { BV_APPROX_SIGN_UPPER
, BV_APPROX_SCALE
, BV_APPROX_SCALE_CHAMBER
},
45 { BV_APPROX_SIGN_UPPER
, BV_APPROX_SCALE
, BV_APPROX_SCALE_FAST
},
46 { BV_APPROX_SIGN_UPPER
, BV_APPROX_SCALE
, BV_APPROX_SCALE_FAST
| BV_APPROX_SCALE_CHAMBER
},
47 { BV_APPROX_SIGN_UPPER
, BV_APPROX_SCALE
, BV_APPROX_SCALE_NARROW
},
48 { BV_APPROX_SIGN_UPPER
, BV_APPROX_SCALE
, BV_APPROX_SCALE_NARROW
| BV_APPROX_SCALE_CHAMBER
},
49 { BV_APPROX_SIGN_UPPER
, BV_APPROX_SCALE
, BV_APPROX_SCALE_FAST
| BV_APPROX_SCALE_NARROW
},
50 { BV_APPROX_SIGN_UPPER
, BV_APPROX_SCALE
, BV_APPROX_SCALE_FAST
| BV_APPROX_SCALE_NARROW
| BV_APPROX_SCALE_CHAMBER
},
51 { BV_APPROX_SIGN_UPPER
, BV_APPROX_SCALE
, BV_APPROX_SCALE_NARROW2
},
52 { BV_APPROX_SIGN_UPPER
, BV_APPROX_SCALE
, BV_APPROX_SCALE_NARROW2
| BV_APPROX_SCALE_CHAMBER
},
53 { BV_APPROX_SIGN_UPPER
, BV_APPROX_SCALE
, BV_APPROX_SCALE_FAST
| BV_APPROX_SCALE_NARROW2
},
54 { BV_APPROX_SIGN_UPPER
, BV_APPROX_SCALE
, BV_APPROX_SCALE_FAST
| BV_APPROX_SCALE_NARROW2
| BV_APPROX_SCALE_CHAMBER
},
57 #define nr_methods (sizeof(methods)/sizeof(*methods))
59 struct argp_option argp_options
[] = {
66 struct verify_options verify
;
69 static error_t
parse_opt(int key
, char *arg
, struct argp_state
*state
)
71 struct options
*options
= (struct options
*) state
->input
;
75 state
->child_inputs
[0] = options
->verify
.barvinok
;
76 state
->child_inputs
[1] = &options
->verify
;
83 return ARGP_ERR_UNKNOWN
;
90 double RE_sum
[nr_methods
];
92 clock_t ticks
[nr_methods
];
93 size_t size
[nr_methods
];
96 void result_data_init(struct result_data
*result
)
99 for (i
= 0; i
< nr_methods
; ++i
) {
100 result
->RE_sum
[i
] = 0;
101 result
->ticks
[i
] = 0;
104 value_init(result
->n
);
107 void result_data_clear(struct result_data
*result
)
110 value_clear(result
->n
);
113 void result_data_print(struct result_data
*result
, int n
)
117 fprintf(stderr
, "%d", result
->ticks
[0]/n
);
118 for (i
= 1; i
< nr_methods
; ++i
)
119 fprintf(stderr
, ", %d", result
->ticks
[i
]/n
);
120 fprintf(stderr
, "\n");
122 fprintf(stderr
, "%d", result
->size
[0]/n
);
123 for (i
= 1; i
< nr_methods
; ++i
)
124 fprintf(stderr
, ", %d", result
->size
[i
]/n
);
125 fprintf(stderr
, "\n");
127 fprintf(stderr
, "%g\n", VALUE_TO_DOUBLE(result
->n
));
128 fprintf(stderr
, "%g", result
->RE_sum
[0]/VALUE_TO_DOUBLE(result
->n
));
129 for (i
= 1; i
< nr_methods
; ++i
)
130 fprintf(stderr
, ", %g", result
->RE_sum
[i
]/VALUE_TO_DOUBLE(result
->n
));
131 fprintf(stderr
, "\n");
134 struct test_approx_data
{
135 struct check_poly_data cp
;
137 struct result_data
*result
;
140 static void eval(const evalue
*EP
, Value
*z
, int sign
, Value
*v
)
144 res
= evalue_eval(EP
, z
);
145 if (sign
== BV_APPROX_SIGN_LOWER
)
146 mpz_cdiv_q(*v
, res
->x
.n
, res
->d
);
147 else if (sign
== BV_APPROX_SIGN_UPPER
)
148 mpz_fdiv_q(*v
, res
->x
.n
, res
->d
);
149 else if (sign
== BV_APPROX_SIGN_APPROX
)
150 mpz_tdiv_q(*v
, res
->x
.n
, res
->d
);
152 assert(value_one_p(res
->d
));
153 value_assign(*v
, res
->x
.n
);
155 free_evalue_refs(res
);
159 static int test_approx(const struct check_poly_data
*data
, int nparam
, Value
*z
,
160 const struct verify_options
*options
)
162 struct test_approx_data
* ta_data
= (struct test_approx_data
*) data
;
169 eval(ta_data
->EP
[0], z
, BV_APPROX_SIGN_NONE
, &exact
);
172 value_print(stderr, VALUE_FMT, exact);
175 value_increment(ta_data
->result
->n
, ta_data
->result
->n
);
176 for (i
= 1; i
< nr_methods
; ++i
) {
178 eval(ta_data
->EP
[i
], z
, methods
[i
].sign
, &approx
);
180 fprintf(stderr, ", ");
181 value_print(stderr, VALUE_FMT, approx);
183 if (methods
[i
].sign
== BV_APPROX_SIGN_LOWER
)
184 assert(value_le(approx
, exact
));
185 if (methods
[i
].sign
== BV_APPROX_SIGN_UPPER
)
186 assert(value_ge(approx
, exact
));
187 value_subtract(approx
, approx
, exact
);
188 if (value_zero_p(exact
))
189 error
= abs(VALUE_TO_DOUBLE(approx
));
191 error
= abs(VALUE_TO_DOUBLE(approx
)) / VALUE_TO_DOUBLE(exact
);
192 ta_data
->result
->RE_sum
[i
] += error
;
196 fprintf(stderr, "\n");
204 static void test(Polyhedron
*P
, Polyhedron
*C
, evalue
**EP
,
205 struct result_data
*result
,
206 struct verify_options
*options
)
210 unsigned nparam
= C
->Dimension
;
211 struct test_approx_data data
;
213 CS
= check_poly_context_scan(P
, &C
, C
->Dimension
, options
);
215 p
= Vector_Alloc(P
->Dimension
+2);
216 value_set_si(p
->p
[P
->Dimension
+1], 1);
218 check_poly_init(C
, options
);
221 data
.cp
.check
= test_approx
;
223 data
.result
= result
;
224 check_poly(CS
, &data
.cp
, nparam
, 0, p
->p
+P
->Dimension
-nparam
+1,
226 if (!options
->print_all
)
236 void Matrix_File_Read_Input(FILE *in
, Matrix
*Mat
)
240 char *c
, s
[1024],str
[1024];
243 for (i
=0;i
<Mat
->NbRows
;i
++) {
245 c
= fgets(s
, 1024, in
);
246 while(isspace(*c
) && *c
!='\n')
248 } while(c
&& (*c
=='#' || *c
== '\n'));
251 errormsg1( "Matrix_Read", "baddim", "not enough rows" );
254 for (j
=0;j
<Mat
->NbColumns
;j
++) {
255 if(!c
|| *c
=='\n' || *c
=='#') {
256 errormsg1("Matrix_Read", "baddim", "not enough columns");
259 if (sscanf(c
,"%s%n",str
,&n
) == 0) {
260 errormsg1( "Matrix_Read", "baddim", "not enough columns" );
263 value_read(*(p
++),str
);
267 } /* Matrix_Read_Input */
270 * Read the contents of the matrix 'Mat' from standard input.
271 * A '#' in the first column is a comment line
273 Matrix
*Matrix_File_Read(FILE *in
)
276 unsigned NbRows
, NbColumns
;
280 while ((*s
=='#' || *s
=='\n') ||
281 (sscanf(s
, "%d %d", &NbRows
, &NbColumns
)<2))
283 Mat
= Matrix_Alloc(NbRows
,NbColumns
);
285 errormsg1("Matrix_Read", "outofmem", "out of memory space");
288 Matrix_File_Read_Input(in
, Mat
);
292 void handle(FILE *in
, struct result_data
*result
, struct verify_options
*options
)
298 evalue
*EP
[nr_methods
];
300 M
= Matrix_File_Read(in
);
301 A
= Constraints2Polyhedron(M
, options
->barvinok
->MaxRays
);
303 M
= Matrix_File_Read(in
);
304 C
= Constraints2Polyhedron(M
, options
->barvinok
->MaxRays
);
306 param_name
= Read_ParamNames(in
, C
->Dimension
);
308 for (i
= 0; i
< nr_methods
; ++i
) {
311 options
->barvinok
->polynomial_approximation
= methods
[i
].sign
;
312 options
->barvinok
->approximation_method
= methods
[i
].method
;
313 if (methods
[i
].method
== BV_APPROX_SCALE
)
314 options
->barvinok
->scale_flags
= methods
[i
].flags
;
315 else if (methods
[i
].method
== BV_APPROX_VOLUME
)
316 options
->barvinok
->volume_triangulate
= methods
[i
].flags
;
319 EP
[i
] = barvinok_enumerate_with_options(A
, C
, options
->barvinok
);
321 result
->ticks
[i
] = en_cpu
.tms_utime
- st_cpu
.tms_utime
;
323 print_evalue(stdout, EP[i], param_name);
326 for (i
= 0; i
< nr_methods
; ++i
)
327 result
->size
[i
] = evalue_size(EP
[i
])/4;
328 test(A
, C
, EP
, result
, options
);
329 for (i
= 0; i
< nr_methods
; ++i
) {
330 free_evalue_refs(EP
[i
]);
334 Free_ParamNames(param_name
, C
->Dimension
);
339 int main(int argc
, char **argv
)
341 struct barvinok_options
*bv_options
= barvinok_options_new_with_defaults();
342 char path
[PATH_MAX
+1];
343 struct result_data all_result
;
345 static struct argp_child argp_children
[] = {
346 { &barvinok_argp
, 0, 0, 0 },
347 { &verify_argp
, 0, "verification", BV_GRP_LAST
+1 },
350 static struct argp argp
= { argp_options
, parse_opt
, 0, 0, argp_children
};
351 struct options options
;
353 options
.verify
.barvinok
= bv_options
;
354 set_program_name(argv
[0]);
355 argp_parse(&argp
, argc
, argv
, 0, 0, &options
);
357 if (options
.verify
.M
== INT_MIN
)
358 options
.verify
.M
= 100;
359 if (options
.verify
.m
== INT_MAX
)
360 options
.verify
.m
= -100;
362 result_data_init(&all_result
);
364 while (fgets(path
, sizeof(path
), stdin
)) {
365 struct result_data result
;
370 result_data_init(&result
);
371 fprintf(stderr
, "%s", path
);
372 *strchr(path
, '\n') = '\0';
373 in
= fopen(path
, "r");
375 handle(in
, &result
, &options
.verify
);
379 result_data_print(&result
, 1);
381 value_addto(all_result
.n
, all_result
.n
, result
.n
);
382 for (i
= 0; i
< nr_methods
; ++i
) {
383 all_result
.RE_sum
[i
] += result
.RE_sum
[i
];
384 all_result
.ticks
[i
] += result
.ticks
[i
];
385 all_result
.size
[i
] += result
.size
[i
];
388 result_data_clear(&result
);
390 if (!options
.quiet
) {
391 fprintf(stderr
, "average\n");
392 result_data_print(&all_result
, n
);
396 result_data_clear(&all_result
);
398 barvinok_options_free(bv_options
);