[PPL-devel] PPL's Int64_Box's CC76_widening

[Zhoulai]

Hello,

By PPL's Int64_Box.CC76_widening_assign , I get [1,1] \widen [1,2] = [1,2]
whereas [1,+inf] is expected in this case.

Here is my Java test code (below createIntBox (a,b) is a help function that
creates an interval of dimension 1 between integers 'a' and 'b')

    Int64_Box b=createIntBox(1, 1);
    Int64_Box b2=createIntBox(1, 2);
    out.println(b+",      " + b2);

    b2.CC76_widening_assign(b, new By_Reference<Integer>(0));
    out.println(b+",      " + b2);

I get:

A in 1,      A in [1, 2]
A in 1,      A in [1, 2]

I probably misunderstand something, but applying the original definition of
widening as defined in CC76, we have the following:

[1,1] \widening [1,2] = [1, +inf]

which is different from PPL's result above.


Strangely, if I change 'b2' to [1,3] ,i.e.
   Int64_Box b2=createIntBox(1, 3),

I will get the expected results, i.e
[1,1] \widening [1,3] = [1, +inf]


So It becomes a bit confusing. Maybe PPL has another implementation of
CC76's widening?  Can you clarify a bit?

Thanks.

Zell.
p.s

For completeness, here is the 'createIntBox' part:

    private static Int64_Box createIntBox(int a, int b) {
        Linear_Expression_Variable var = new
Linear_Expression_Variable(new  Variable(0));
        Linear_Expression le_a = new Linear_Expression_Coefficient(new
Coefficient(a));
        Linear_Expression le_b = new Linear_Expression_Coefficient(new
Coefficient(b));
        Int64_Box box=new Int64_Box(1, Degenerate_Element.UNIVERSE);
        box.add_constraint(new Constraint(var,
Relation_Symbol.GREATER_OR_EQUAL, le_a));
        box.add_constraint(new Constraint(var,
Relation_Symbol.LESS_OR_EQUAL, le_b));
        return box;
    }
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.cs.unipr.it/pipermail/ppl-devel/attachments/20120902/ad0328c3/attachment.htm>