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; }