Dear Enrico,
I assume you are working with PPL 0.5, and that by "[our] operator" you mean the BHRZ03 widening. If so, notice that the widening proposed in the PhD thesis of Nicholas Halbwachs (which is a refinement of the one proposed by Patrick Cousot and Halbwachs himself in their POPL'78 paper) is already present in the version of the library you have, where it is called H79. So implementation of the Cousot & Halbwachs widening and extrapolation operators are provided by methods
void H79_widening_assign(const Polyhedron& y, unsigned* tp = 0); void limited_H79_extrapolation_assign(const Polyhedron& y, const ConSys& cs, unsigned* tp = 0); void bounded_H79_extrapolation_assign(const Polyhedron& y, const ConSys& cs, unsigned* tp = 0);
[...]
Please, do not hesitate to come back to us if I have misunderstood your question.
Dear all, yes I use PPL 0.5. I used exactly H79 widening operator, I have, i.e., two polyhedra:
ph1 : -A - 2*B >= -6, B >= 0, A - 2*B >= 2.
ph2: -A - 2*B >= -10, B >= 0, A - 2*B >= 2.
if I call the function ph1.H79_widening_assign(ph2) the result is -A - 2*B >= -6, B >= 0, A - 2*B >= 2
which is the first one (ph1). In the Cousot & Halbwachs's article the same example gives a different result: B >= 0, A - 2*B >= 2
Maybe I wrong something when I invoke these functions.
All the best,
Enrico.