Bug in Contractor

[DavidWz]

See example contraction_bug.smt2.

Since the contractor intersect with the original interval, we lose the contracted upper / lower bounds. We need those bounds in the case of inequalities (which bound to use).

Current workaround simply uses the original bound.

Fix: Use VariableSolution instead of Contractor, because there we can access the contracted bounds without intersection.

[Verdict7]

Fixed this bug, though the current version ignores all unbounded intervals when contracting. This is due to the fact that the case distinction is really tedious. Maybe someone else wants to take a look at the fix to confirm everything is alright and take a shot at those cases?

[Verdict7]

Maybe return the original interval if one of the intervals is unbounded.

[DavidWz]

Instead of all the case distinctions, we can simply replace the upper/lower bound of the result interval with infinity and then intersect it with the original interval.

Also, think about LESS LEQ again.

[Verdict7]

Done. It seems that Interval::setLowerBoundType (and setUpperBoundType) called with carl::BoundType::INFTY leads to also changing the upper (lower) bound to the original lower (upper bound). Example [-10,5] becomes [-INFTY,-10] instead of the expected [-INFTY,5]. Interval::setLowerBound on the other hand seems to work as expected.

[DavidWz]

I found another bug (see commit 727e7058aa3ed256e0d50d444df1fc8a4e67b302). In case the result of the contraction was [-inf,inf], the first case check still used the upper/lower bound of that infinite interval (which is internally stored as 0). I added an additional check for infty.

Maybe it would be easier to simply always replace one bound of resultA by Infty and then intersect with originalInterval (without the slides 18 case distinction).

[Verdict7]

The only case where this does not work is with LESS and GREATER, where an intersection containing only a single point should become an empty interval. This could be fixed by simply checking for that case. Thanks for noticing the bug though, I actually had that problem before but forgot about it when fixing the INFTY stuff...