On 11/07/12 16:34, Zhoulai wrote:
This may be a silly question. But I would like to know why narrowing for polyhedral domains is not implemented in PPL? I recently experienced many cases where analysis using Int64_Box gives more precise results than NNC_Polyhedral because the former provides a narrowing.
What do you think?
Dear Zell,
the study of narrowing operators for the domain of (C or NNC) polyhedra has not received much attention. This is due in part to the fact that there is little incentive. Intersection (the domain glb) satisfies the first part of the definition of narrowing operator (that it yields a lower bound of the argument) in the most precise way; the second part of the definition (eventual stabilization of the decreasing iteration sequence) can be dispensed with: just enforce an external limit to the length of the decresing iteration sequence and you are done. Experience shows that decreasing iterations sequences longer than 1 often give little or no extra precision. Kind regards,
Roberto