defines == generically to work on LazySet pairs #604

tomerarnon · 2018-09-03T03:01:28Z

No description provided.

schillic

Works like a charm.
@mforets: I leave the merge to you.

schillic · 2018-09-03T07:19:18Z

Cross-reference: #378.

mforets · 2018-09-03T12:38:31Z

@tomerarnon Thanks for the contribution. Would you please add a docstring? We've got some guidelines in this wiki.

tomerarnon · 2018-09-04T01:25:01Z

Sure, I can add a docstring.

I am noting now however that the previous definition of equals only works for L{N} == L{N} where L and N are the same. So, e.g., comparing a HalfSpace{Int64} with a HalfSpace{Float64} is not covered (still uses the default false definition).

I tried to come up with a definition which would allow L{N} == L{M} where only L is the same, but had considerable trouble. The following definition is the best attempt so far, but it too has problems. It works for all of the cases shown, including the potentially problematic case at the end.

function ==(a::LazySet, b::LazySet)
    afields = fieldnames(a)
    bfields = fieldnames(b)

    if afields != bfields
        return false
    end

    for f in afields
        if getfield(a, f) != getfield(b, f)
            return false
        end
    end
    return true
end


hs_int   = HalfSpace([1,  1], 1) 
hs_float = HalfSpace([1.0,  1.0], 1.0)

### all return true:
hs_int   == deepcopy(hs_int) 
hs_float == deepcopy(hs_float)
hs_int == hs_float 
#######

As = [ [1,  1], [1, -1], [-1, 0] ]
Bs = [1, 0, 0]

intconst   = [HalfSpace(As[i], Bs[i])                    for i in 1:length(As)]
floatconst = [HalfSpace(Float64.(As[i]), Float64(Bs[i])) for i in 1:length(As)]
hpoly_int   = HPolygon(intconst)
hpoly_float = HPolygon(floatconst)

#### all return true:
intconst    == deepcopy(intconst)
floatconst  == deepcopy(floatconst)
floatconst  == intconst
hpoly_float == deepcopy(hpoly_float)
hpoly_int   == deepcopy(hpoly_int)
hpoly_int   == hpoly_float
########

### NOTE: also return true:
HPolygon(intconst) == HPolytope(intconst)
HPolygon(intconst) == HPolytope(floatconst)
etc.

Let me know what you think of this as opposed to the other definition. On the one hand it is more general and therefore perhaps more useful. On the other hand perhaps it allows comparisons which are problematic. Likewise, if you can think of a definition which is the best of both worlds, please let me know! There is perhaps something that can be done with checking if the promotion type of the inputs is an abstract or concrete type, etc., and I have not yet gone that route.

Whichever the decided behavior, I can note it in the docs.

tomerarnon · 2018-09-04T03:27:10Z

Actually, here is a definition which I believe works in all cases without the trouble described earlier:

function ==(a::LazySet, b::LazySet)
    # If the common supertype of a and b is abstract, they cannot be compared.
    if Base.isabstract(promote_type(typeof(a), typeof(b)))
        return false
    end

    for f in fieldnames(a)
        if getfield(a, f) != getfield(b, f)
            return false
        end
    end
    return true
end

# returns false for:
HPolygon(intconst) == HPolytope(intconst)
HPolygon(intconst) == HPolytope(floatconst)

It first checks to see if the common supertype of the two types is abstract, thereby not allowing comparisons between different types. I believe in v1.0 the function is called isabstracttype, and an equivalent isconcretetype also exists.

mforets · 2018-09-04T03:44:23Z

Hmm I prefer the original option, making it explicit in the new function's signature:

function ==(a::LazySet{N}, b::LazySet{N}) where {N}
....
end

We can add some approach at a later stage that covers the case of different N if usage arises..

mforets · 2018-09-04T03:48:45Z

Actually, here is a definition which I believe works in all cases without the trouble described earlier:

Good!

I believe in v1.0 the function is called isabstracttype,

True. You can use Compat.isabstracttype

tomerarnon · 2018-09-04T03:53:51Z

Good

Does this mean you prefer the newest version?

schillic · 2018-09-04T05:36:46Z

Hmm I prefer the original option, making it explicit in the new function's signature:

function ==(a::LazySet{N}, b::LazySet{N}) where {N}
....
end

We can add some approach at a later stage that covers the case of different N if usage arises..

I agree here.
The new function might return true (not checked) for Ball1([0.], 1.) == Ball2([0.], 1.) because the field names, field types, and field content are equal.

@tomerarnon: Do you have this use case that you switch between numeric types? Otherwise I would keep your initial function (sorry).

tomerarnon · 2018-09-04T05:55:12Z

The new function might return true (not checked) for Ball1([0.], 1.) == Ball2([0.], 1.) because the field names, field types, and field content are equal.

It does not. The last version I included returns false if the promotion type of a and b is not a concrete type. The docstring I have written for it features this explanation:

Will not convert a or b in order to check equivalence of different LazySet types.
I.e. a::HPolytope{Int64} == b::HPolytope{Float64} is a valid comparison,
but a::VPolytope == b::HPolytope is not, and therefore returns false even if a and b
represent the same polytope.

By contrast, the first version (from the issue) would not feature the piece about the L{M} == L{N} being a valid comparison.

Do you have this use case that you switch between numeric types?

Admittedly, I do not, I just liked the general solution! If you prefer the original one, I can revert to it, and note the restriction in the docstring.

schillic · 2018-09-04T06:47:59Z

The new function might return true (not checked) for Ball1([0.], 1.) == Ball2([0.], 1.) because the field names, field types, and field content are equal.

It does not. The last version I included returns false if the promotion type of a and b is not a concrete type.

Indeed, I must have looked at the second version. Then, since the solution is so simple and with no particular overhead, from my side we can go for the new version. A typical Julia user might expect that behavior anyway.

julia> 1. == 1f0
true

help?> ==
[...] For example, all numeric types are compared by numeric value, ignoring type. [...]

schillic · 2018-09-04T06:51:33Z

Actually, we can have both versions. The first version takes precedence if the type parameters are identical (and this version is faster), while the second version is the fallback option for the less typical case.

function ==(X::L, Y::L) where L<:LazySet
    return equality_helper(X, Y)
end

function ==(X::LazySet, Y::LazySet)
    # if the common supertype of a and b is abstract, they cannot be compared
    if Base.isabstract(promote_type(typeof(X), typeof(Y)))
        return false
    end
    return equality_helper(X, Y)
end

@inline function equality_helper(X::LazySet, Y::LazySet)
    for f in fieldnames(X)
        if getfield(X, f) != getfield(Y, f)
            return false
        end
    end
    return true
end

tomerarnon · 2018-09-04T07:24:16Z

Sure, I can implement it as you have it there. As for the docs, I think == maybe be intuitive enough not to require all of the mandatory fields from the wiki, let me know your thoughts on the following options. (This is maybe the longest thread over a 13 line pull request ever 😄)

I followed the wiki to produce:

wiki style

"""
==(a::LazySet, b::LazySet)

Return whether two LazySets of the same type are exactly equal by recursively
comparing their fields until a mismatch is found.

Input

a -- any LazySet

b -- another LazySet of the same type as a

Output

true iff a is equivalent to b. Otherwise false

Notes

Will not convert in order to check equivalence of different LazySet types.
I.e. a::VPolytope == b::HPolytope returns false even if a and b represent the
same polytope. However L{N} == L{M} where {M, N, L<:LazySet} is a valid comparison.

Examples
julia> a = HalfSpace([1], 1);
julia> b = HalfSpace([1.0], 1.0);

julia> a == deepcopy(a)
true

julia> a == b
true
"""

shorter than wiki style

"""
==(a::LazySet, b::LazySet)

Return whether two LazySets of the same type are equal by recursively comparing their fields.
Will not convert a or b in order to check equivalence of different LazySet types.
I.e. a::HPolytope{Int64} == b::HPolytope{Float64} is a valid comparison,
but a::VPolytope == b::HPolytope is not, and therefore returns false even if a and b
represent the same polytope.

Examples
julia> a = HalfSpace([1], 1);

julia> b = HalfSpace([1.0], 1.0);

julia> a == deepcopy(a)
true

julia> a == b
true
"""

schillic · 2018-09-04T07:35:27Z

true iff a is equivalent to b. Otherwise false

I would use equal instead of equivalent.
Otherwise false is not needed.

Will not convert in order to check equivalence of different LazySet types.

This sentence is not clear to me. Maybe:
The check is purely syntactic and the sets need to have the same base type.

tomerarnon · 2018-09-04T07:36:11Z

On second thought, one branch or the other compiles away in the == that has the isabstract() check, so actually it should not be slower.

julia> @code_warntype Ball1([0.], 1.) == Ball2([0.], 1.)
Variables:
  #temp#@_1 <optimized out>
  #temp#@_2 <optimized out>
  #temp#@_3 <optimized out>

Body:
  begin 
      return $(QuoteNode(false))
  end::Bool

julia> @code_warntype hs_int == hs_float
Variables:
  #self# <optimized out>
  X::LazySets.HalfSpace{Int64}
  Y::LazySets.HalfSpace{Float64}
  f <optimized out>
  #temp#@_5::Int64
  t::Type{LazySets.HalfSpace{Int64}}
  #temp#@_7::Core.MethodInstance
  #temp#@_8::Bool
  #temp#@_9::Bool

Body:
  begin 
      goto 3 # line 4:
      3:  # line 6:
      $(Expr(:inbounds, false))
      # meta: location REPL[5] equality_helper 2
      # meta: location reflection.jl fieldnames 137
      t::Type{LazySets.HalfSpace{Int64}} = LazySets.HalfSpace{Int64} # line 138:
      goto 12 # line 139:
      12: 
      # meta: pop location
      SSAValue(0) = $(Expr(:invoke, MethodInstance for fieldnames(::DataType), :(Base.fieldnames), :(t)))
      #temp#@_5::Int64 = 1
      16: 
      unless (Base.not_int)((#temp#@_5::Int64 === (Base.add_int)((Base.arraylen)(SSAValue(0))::Int64, 1)::Int64)::Bool)::Bool goto 45
      SSAValue(2) = (Base.arrayref)(SSAValue(0), #temp#@_5::Int64)::Symbol
      SSAValue(3) = (Base.add_int)(#temp#@_5::Int64, 1)::Int64
      #temp#@_5::Int64 = SSAValue(3) # line 3:
      unless ((Main.getfield)(Y::LazySets.HalfSpace{Float64}, SSAValue(2))::Union{AbstractArray{Float64,1}, Float64} isa AbstractArray{Float64,1})::Bool goto 24
      goto 33
      24: 
      unless ((Main.getfield)(Y::LazySets.HalfSpace{Float64}, SSAValue(2))::Union{AbstractArray{Float64,1}, Float64} isa Float64)::Bool goto 31
      unless ((Main.getfield)(X::LazySets.HalfSpace{Int64}, SSAValue(2))::Union{AbstractArray{Int64,1}, Int64} isa Int64)::Bool goto 29
      #temp#@_7::Core.MethodInstance = MethodInstance for !=(::Int64, ::Float64)
      goto 36
      29: 
      goto 33
      31: 
      goto 33
      33: 
      #temp#@_8::Bool = ((Main.getfield)(X::LazySets.HalfSpace{Int64}, SSAValue(2))::Union{AbstractArray{Int64,1}, Int64} != (Main.getfield)(Y::LazySets.HalfSpace{Float64}, SSAValue(2))::Union{AbstractArray{Float64,1}, Float64})::Bool
      goto 38
      36: 
      #temp#@_8::Bool = $(Expr(:invoke, :(#temp#@_7), :(Main.!=), :((Main.getfield)(X, SSAValue(2))::Union{AbstractArray{Int64,1}, Int64}), :((Main.getfield)(Y, SSAValue(2))::Union{AbstractArray{Float64,1}, Float64})))
      38: 
      unless #temp#@_8::Bool goto 43 # line 4:
      #temp#@_9::Bool = false
      goto 48
      43: 
      goto 16
      45:  # line 7:
      #temp#@_9::Bool = true
      48: 
      # meta: pop location
      $(Expr(:inbounds, :pop))
      return #temp#@_9::Bool
  end::Bool

schillic · 2018-09-04T07:38:47Z

I would also give a negative example. Also, please use jldoctest for the examples.

tomerarnon · 2018-09-04T07:39:45Z

true iff a is equivalent to b. Otherwise false

I would use equal instead of equivalent.
Otherwise false is not needed.

Will not convert in order to check equivalence of different LazySet types.

This sentence is not clear to me. Maybe:
The check is purely syntactic and the sets need to have the same base type.

Got it, Made the change.

tomerarnon · 2018-09-04T07:42:06Z

I would also give a negative example.

Will do.

Also, please use jldoctest for the examples.

I am, but it does not show up when I copy-paste to here, interestingly.

You prefer the full version of the docstring though, yes?

schillic · 2018-09-04T07:46:25Z

You prefer the full version of the docstring though, yes?

Yes, since you already wrote it 😉

schillic · 2018-09-04T07:52:12Z

Got it, Made the change.

Did you push the changes already? I do not see them in this PR.
If you have pushed, this might be related to the fact that you work in a fork. The newest comments below the answer here indicate that this might be a Github bug, but they are quite old already...

tomerarnon · 2018-09-04T07:54:49Z

No, I hadn't yet pushed, I was waiting for your thoughts on the docstring. Now you should see it .

schillic · 2018-09-04T07:55:46Z

src/LazySet.jl

+```
+"""
+function ==(X::LazySet, Y::LazySet)
+    # if the common supertype of a and b is abstract, they cannot be compared


Sorry, I renamed the variables, but not in the comment 😞

Ha! I hadn't noticed. If you don't mind I'll change them back to a and b to match the doc

Really I was just being lazy 😞
I prefer X and Y too honestly...
Renamed again.

schillic · 2018-09-04T08:24:29Z

Almost done! We still need to include in the docs.
In this block add the following line:
==(::LazySet, ::LazySet)

schillic · 2018-09-04T08:26:49Z

In Julia v0.7:

Warning: `fieldnames(v)` is deprecated, use `fieldnames(typeof(v))` instead.

…mes()

schillic

Thanks for your endurance 😄

tomerarnon · 2018-09-04T08:44:36Z

Not a problem. As they say, "if you're going to do something, do it right"!

Just to note again something I alluded to in the original issue, this catch-all definition is not as fast as a function defined on each type. That is primarily because the for-loop creates variables which are Unions over all the field types in X, which is a little bit type unstable. So unrolling the loop manually will be faster.

schillic · 2018-09-04T11:31:36Z

@tomerarnon: Feel free to add yourself to the list of contributors.

defined == generically to work on LazySet pairs

3bb7b51

schillic approved these changes Sep 3, 2018

View reviewed changes

schillic mentioned this pull request Sep 3, 2018

Implement comparison operator for set types #378

Closed

tomerarnon mentioned this pull request Sep 3, 2018

==/issubset on HPolytopes #598

Closed

Add docstring and define == more generically

1ad3601

schillic reviewed Sep 4, 2018

View reviewed changes

rename a, b to X, Y

d141b80

tomerarnon force-pushed the defineequals branch from 988fce9 to d141b80 Compare September 4, 2018 08:12

list == in interfaces.md and fix v0.7 deprecation warning for fieldna…

0e9996d

…mes()

schillic approved these changes Sep 4, 2018

View reviewed changes

mforets approved these changes Sep 4, 2018

View reviewed changes

mforets merged commit 4febb28 into JuliaReach:master Sep 4, 2018

mforets mentioned this pull request Sep 4, 2018

Specialized == for types #608

Closed

tomerarnon mentioned this pull request Sep 5, 2018

Add "Tomer Arnon" to "Credits" #611

Merged

defines == generically to work on LazySet pairs #604

defines == generically to work on LazySet pairs #604

Conversation

tomerarnon commented Sep 3, 2018

schillic left a comment

Choose a reason for hiding this comment

schillic commented Sep 3, 2018

mforets commented Sep 3, 2018

tomerarnon commented Sep 4, 2018

tomerarnon commented Sep 4, 2018

mforets commented Sep 4, 2018 • edited Loading

mforets commented Sep 4, 2018

tomerarnon commented Sep 4, 2018

schillic commented Sep 4, 2018

tomerarnon commented Sep 4, 2018 • edited Loading

schillic commented Sep 4, 2018

schillic commented Sep 4, 2018 • edited Loading

tomerarnon commented Sep 4, 2018

wiki style

Input

Output

Notes

Examples

shorter than wiki style

Examples

schillic commented Sep 4, 2018

tomerarnon commented Sep 4, 2018

schillic commented Sep 4, 2018

tomerarnon commented Sep 4, 2018

tomerarnon commented Sep 4, 2018

schillic commented Sep 4, 2018

schillic commented Sep 4, 2018

tomerarnon commented Sep 4, 2018

schillic Sep 4, 2018

Choose a reason for hiding this comment

tomerarnon Sep 4, 2018

Choose a reason for hiding this comment

schillic Sep 4, 2018

Choose a reason for hiding this comment

tomerarnon Sep 4, 2018

Choose a reason for hiding this comment

schillic commented Sep 4, 2018

schillic commented Sep 4, 2018

schillic left a comment

Choose a reason for hiding this comment

tomerarnon commented Sep 4, 2018

schillic commented Sep 4, 2018

mforets commented Sep 4, 2018 •

edited

Loading

tomerarnon commented Sep 4, 2018 •

edited

Loading

schillic commented Sep 4, 2018 •

edited

Loading