Narrowing operator

[Gustavo Gutierrez Sabogal]

Hello,

I have a question concerning with the efficiency.  I am trying to implement the times narrowing function, this one takes three arguments as inputs, and returns false in case any of the intervals gets empty:

bool narrow_times(interval x, interval y, interval z){
//x*y=z
  z &= x * y;
  if( z.is_empty())
    return false;
  x &= div_rel(z,y,x);
  if(x.is_empty())
     return false;
  y &= div_rel(z,x,y);
  if(y.is_empty())
     return false;
  return true;
}

My question is, what difference make the use of div_rel or the overload operator % in this case?

Thanks a lot.
Gustavo

[Frederic Goualard]

Hello Gustavo,

Consider the constraint narrow_times(x,y,z) with
x = [1,4], y=[-3,3], and z=[4,5].

The result of z/y is [-oo, -4/3] \cup [4/3, +oo].

If you perform the "relational" division without any knowledge of x, you will return [-oo,+oo], so that

x &= z%y;

does not narrow x.

On the other hand,

x = div_rel(z,y,x);

will assign [4/3,4] to x because the intersection with the domain of x is performed internally by div_rel by considering each part of the domain computed separately.

So, div_rel is the way to go for your purpose.

Frederic.