Qualify the use of NeuralVerification.jl's "complement" function

[castrong]

The complement function was breaking Travis builds for Julia 1.5 at least, where when complements.jl tests the complement function it wasn't sure whether it referred to LazySets.complement or NeuralVerification.complement. I added on NeuralVerification.jl to all uses of complement in that file.

[tomerarnon]

Instead of this patch, we should actually be able to adopt LazySets's Complement type. We'll need to:

• replace uses of complement with Complement (since they are not interchangeable in LazySets),
• replace references to the field P to the field X

but otherwise it seems all of the same operations should work

[castrong]

Okay that's a good idea, I'll work on that refactor now!

[castrong]

@tomerarnon One interesting bit of behavior from the LazySets implementation:

HS = HalfSpace([-1.0, -1.0], 0.0)
PC = Complement(HS)

println(Complement(HS) == Complement(HS))
println(Complement(Complement(HS)) == Complement(Complement(HS)))

The first will print false while the second prints true. So even though the left and right of the first equals check are the same geometric object, they don't get evaluated as equal right now. Will this break anything? I added an issue on LazySets JuliaReach/LazySets.jl#2686 to see if this is a bug or if it's expected behavior.

[tomerarnon]

Can we go with just Complement? There shouldn't be a need for the type parameters.

[castrong]

Yeah, I was worried we would need some way to make sure it's the complement of a polytope. Eventually we convert it to a matrix representation, so if it were the complement of an L-2 Ball or something we wouldn't want to let it in. Is there some less restrictive way to ensure it will be convertible to hrep?

[mforets]

Is there some less restrictive way to ensure it will be convertible to hrep?

we usually use applicable(constraints_list, X)

[tomerarnon]

Also, since the functions that use Complement just unwrap it and pass to the complementary function (which are all strictly typed (HalfSpace, HPolytope, etc.), we will just run into the same method error one layer deeper, which is fine. So we should be able to stick to ::Complement without a problem.

[castrong]

oh got it, then typing to Complement alone should address the problem right? I just updated it to be like that and have re-requested review.

[tomerarnon]

So even though the left and right of the first equals check are the same geometric object, they don't get evaluated as equal right now.

Yes, this is a bit annoying. It's just because LazySets hasn't defined == to work on Complements because they are not <:LazySet (which is their generic fallback; the even more generic one is Base's ===, which is what returns false in this case.).

I'm not sure whether we check equality of Complements anywhere 😳

[castrong]

Yeah I also can't think of anywhere we use that equality. For the most part, we seem to use it to wrap up a polytope, and eventually that polytope gets unwrapped and turned into linear constraints, or its intersection / other set type operations are performed on it, both of which should still work fine without the equality operator.