comparison tolerance in reluplex [and other algorithms]

[tomerarnon]

@castrong brought this issue up, which may be impacting his results.

See e.g., the following two lines in reluplex, and in particular the comparisons with 0

type_one_broken(ẑᵢⱼ, zᵢⱼ) = (zᵢⱼ > 0.0)  && (zᵢⱼ != ẑᵢⱼ) 
type_two_broken(ẑᵢⱼ, zᵢⱼ) = (zᵢⱼ == 0.0) && (ẑᵢⱼ > 0.0)

Due to the precision of the underlying solvers, sometimes numbers on the order of 1e-10 can be returned, and should probably be considered zeros. We can address this is by introducing a tolerance:

type_one_broken(ẑᵢⱼ, zᵢⱼ) = (zᵢⱼ > TOL)  && (zᵢⱼ != ẑᵢⱼ)  
type_two_broken(ẑᵢⱼ, zᵢⱼ) = (-TOL < zᵢⱼ < TOL) && (ẑᵢⱼ > 0.0)

This is just one example; other optimization solvers also perform similar comparisons. Note that the-TOL is maybe not desirable; it may by more principled to just say z<TOL, not sure.

Does this sound like the right fix for this @changliuliu @mykelk, or do we inadvertantly invalidate completeness if we do this? Is there a principled way of picking the tolerance? We can set it to be user-defined in the Reluplex type, but we'd still have to come up with a default.

[mykelk]

I'm okay with this. These numerical issues are pretty tricky.

[castrong]

I wonder if Julia's ≈ (equivalent to Base.isapprox with default arguments) operator could be helpful? It does some sort of approximate equality using tolerances - I don't know if there's an equivalent built in function for comparisons. Although it may go in the wrong direction for this (since it would make it more liberally consider things as broken instead of being stricter).

[mforets]

Since this library uses LazySets, I would suggest that you control tolerance with LazySets.Tolerance, documented here and the default values are implemented here. In particular you can globally control the tolerance for set operations (membership tests, inclusion checks, etc) for a given numeric type with the set_xtol functions.

It does some sort of approximate equality using tolerances - I don't know if there's an equivalent

See LazySets._isapprox.

[tomerarnon]

Thanks for the tip on this @mforets ! I like the idea of being able to set a global tolerance (per solver maybe) and keep comparisons with literal zeros in the code.