Herbie doesn't know that cos(x) <= 1

[oscardssmith]

When asking herbie to optimize cos(y)-x (with ranges 0 to 1e3 for both variables), it suggest the approximation:

if cos(y)≤1:
    cos(y)
else:
     1−x​​

asides from the correctness issues mentioned in #742, it does seem that herbie should realize that the first branch will always be taken. Also the cost model is off since it seems to think that this program requires computing cos(y) twice.

[pavpanchekha]

This is pretty funny and I'm not sure what causes it. Thinking through how the if statements gets there it seems like this shouldn't occur.

[pavpanchekha]

Ok—I dug in and I think I know why this happens and how to fix it. Basically:

• These if statements have three parts: the expression on the left hand side, the value on the right hand side, and then the stuff that goes in the then and else cases
• Here the issue is with the right hand side, which is always a single number

To compute this single number, we first bound it between two values we sampled. We refer to the value by an index in the point list. Sometimes two values are the same, and then we can't insert a split in between.

We're not consistent with what the index refers to: the left-hand value or the right-hand value.