Hello, <br><br>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. <br><br>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')<br>
<br> Int64_Box b=createIntBox(1, 1);<br> Int64_Box b2=createIntBox(1, 2);<br> out.println(b+", " + b2);<br> <br> b2.CC76_widening_assign(b, new By_Reference<Integer>(0));<br> out.println(b+", " + b2);<br>
<br>I get:<br><br>A in 1, A in [1, 2]<br>A in 1, A in [1, 2]<br><br>I probably misunderstand something, but applying the original definition of widening as defined in CC76, we have the following:<br><br>[1,1] \widening [1,2] = [1, +inf]<br>
<br>which is different from PPL's result above. <br><br><br>Strangely, if I change 'b2' to [1,3] ,i.e.<br> Int64_Box b2=createIntBox(1, 3),<br><br>I will get the expected results, i.e <br>[1,1] \widening [1,3] = [1, +inf]<br>
<br><br>So It becomes a bit confusing. Maybe PPL has another implementation of CC76's widening? Can you clarify a bit?<br><br>Thanks. <br><br>Zell.<br>p.s<br><br>For completeness, here is the 'createIntBox' part:<br>
<br> private static Int64_Box createIntBox(int a, int b) {<br> Linear_Expression_Variable var = new Linear_Expression_Variable(new Variable(0));<br> Linear_Expression le_a = new Linear_Expression_Coefficient(new Coefficient(a));<br>
Linear_Expression le_b = new Linear_Expression_Coefficient(new Coefficient(b));<br> Int64_Box box=new Int64_Box(1, Degenerate_Element.UNIVERSE);<br> box.add_constraint(new Constraint(var, Relation_Symbol.GREATER_OR_EQUAL, le_a));<br>
box.add_constraint(new Constraint(var, Relation_Symbol.LESS_OR_EQUAL, le_b));<br> return box;<br> }<br><br><br><br>