antoinemine / apron

Apron Numerical Abstract Domain Library
Other
114 stars 33 forks source link

Improved use of minimization routines in PPL wrapper #72

Closed ezaffanella closed 1 year ago

ezaffanella commented 1 year ago

The patch attached improves the use of minimization procedures in the PPL wrapper.

When using strict polyhedra, calling minimized_generators() just after a call to minimized_constraints() is probably NOT going to obtain the desired effect (i.e., minimize both descriptions); due to epsilon-representation implementation details, one can only minimize one description at a time. My guess is that in most cases (probably, all cases except add_generators_array) one is interested in obtaining a minimized constraint representation. As a side note, I also think this explains some old reports of users complaining that when using the PPL in Apron they were sometimes seeing redundant constraints even after a call to minimize().

Note: in contrast, on non-strict polyhedra, the second time you call a PPL minimization procedure it does nothing at all.

ppl-patch.txt