On Mon, 20 Jun 2011 00:52:47 +0530, Gokul Ramaswamy wrote:
Prof. Roberto Bagnara,
I need your help again. I have an example (the attached file). It gives the following output : { A - C = 0, -A >= -9, A >= 1 }, { B = 63 } But I was expecting the answer : { A - C = 0, A >= 1 }, { B = 63 } as the constraint A<=9 is violated by A==10 in the powerset poly3.
I may be wrong as I am still learning Powerset Abstraction.
Hi Gokul.
The documentation of
void BHZ03_widening_assign(const Pointset_Powerset& y, Widening wf);
clearly states that `y' /must/ definitely entail `*this. In your example, `*this' is { A - C = 0, -A >= -9, A >= 1 }, { B = 63 } and `y' is { C = 10, A = 10 }, so entailment does not hold. Cheers,
Roberto
P.S. Please direct all messages to ppl-devel@cs.unipr.it