[PPL-devel] Put the constraint (x!=0) to a Int64_Box ?

[Enea Zaffanella]

On 08/12/2012 09:16 PM, Zell wrote:
> Hi, all,
>
> What are we supposed to do if Int64_Box does not support the not_equal
> constraints?
>
> Int64_Box.add_constrain(x!-=0) does not work for me. PPL gives me:
> terminate called after throwing an instance of 'std::runtime_error'
>    what():  PPL Java interface internal error
>
> I think this error is expected.

Yes, the exception thrown is expected.
You can not construct a Constraint object using relation symbol !=.

> What would be the work-around then ?
> (except putting x!=0 to ((x>=1) or (x<=-1)) )

No, the thing above is not going to be a valid workaround (if you map 
the "or" into the upper bound operation of intervals). Strictly 
speaking, the only correct interval approximation for x != 0 is the 
universe interval (because the underlying approximation is meant to be 
convex).

If you already have a Box object B whose class is approximating a 
*rational* box with possibly open boundaries, then you can code your own 
function to refine the box wrt "constraint" (x != C):
  - if B satisfies (x == C), then make B empty;
  - if B satisfies (x >= C), then call B.refine_with_constraint(x > C);
  - if B satisfies (x <= C), then call B.refine_with_constraint(x < C);
  - in all other cases, B is unchanged.

If the Box class is representing *integral* boxes, then:
  - if B satisfies (x == C), then make B empty;
  - if B satisfies (x >= C), then call B.refine_with_constraint(x >= C + 1);
  - if B satisfies (x <= C), then call B.refine_with_constraint(x <= C - 1);
  - in all other cases, B is unchanged.

Enea.


> Thanks.
> Zell.