`intMax` is sensitive to argument ordering when applying abstract domains
danmatichuk opened this issue · 1 comments
As an example, for some integer i with an abstract domain of 0 <= i, we would expect intMax 0 i = i and intMax i 0 = i to always be the case. However at the moment we get that intMax i 0 = (if i <= 0 then 0 else i).
This is a problem for the default constructor for SymNat, since it is almost never able to reduce the incoming integer based on its abstract domain.
A short term fix for SymNat would be to flip the order that the arguments are applied in, but it seems like this is a more general problem for any usage of intMax.
Somewhat related to #101
I think this is a perfect example of the kind of think I had in mind when I opened #101. The other solution might be to change the definition of intMax to if i < 0 then 0 else i which should have the same semantics, but I think will reduce more often.