search

pschanely / hypothesis-crosshair

Level-up your Hypothesis tests with CrossHair
MIT License
8 stars 0 forks source link

`smallest_nonzero_magnitude` inclusive #9

Closed tybug closed 4 months ago

tybug commented 4 months ago

Here's a quick one to either fix or dismiss as intended; I'm fairly sure the condition bounds for smallest_nonzero_magnitude should be inclusive <= as smallest_nonzero_magnitude is allowed. https://github.com/pschanely/hypothesis-crosshair/blob/main/hypothesis_crosshair_provider/crosshair_provider.py#L222-L227.

pschanely commented 4 months ago

Yeah, so the situation here is murky, and I honestly don't recall whether this was intentional or not.

Background: CrossHair currently uses simulates floating point numbers as real numbers ("real" in the mathematics sense). Now, Z3 supports actual floating point semantics, but the cost to use them is much higher. (and sadly, one of the most expensive things is int <-> float conversions, which happens in Python all the time)

So ... it's possible that I made these bounds a little tighter than necessary just out of some hope that it would make a false positive counterexample less likely. But that hope is unfounded, and leaving the code using the wrong comparison just makes it more likely that I'll forget what it is supposed to do when I revise CrossHair's float handling later. Therefore, I've revised it to the inclusive bounds as you suggested! Thanks for noticing!