Cannot find a root of equation cos(x)=0.5 on the interval [5.0, 7.0]

[shmarovfedor]

I was trying to solve the following formula:

(set-logic QF_NRA)
(declare-fun x_t () Real)

(assert (>= x_t 5.0))
(assert (<= x_t 7.0))

(assert (= (cos x_t) 0.5))

(check-sat)
(exit)

The dReal output is unsat. But in fact, the equation cos(x)=0.5 has a root *x = 5pi/3 on the interval [5.0, 7.0]**

[soonhokong]

@shmarovfedor, @scungao

1) we know that there was an issue with eglibc-2.15 on Ubuntu machines. Recently, we switch from eglibc to filib++ for evaluating elementary functions, and I couldn't find a problem even on the ubuntu machine.

2) This one is indeed a problem and I can reproduce it not only on linux machines but also on macs. I suspect the problem is on the Realpaver side. The following is the trace of pruning operation results:

i1 = [5.00000000000000000, 7.00000000000000]
i2 = [5.00000000000001243, 5.23598775598301103]
i3 = [5.23598775598300126; 5.23598775598302]

and this is the result that we have when we evaluate cos over the intervals

cos(i1) = [0.283662185463226302, 0.753902254343304601]
cos(i2) = [0.283662185463238181, 0.500000000000019318]
cos(i3) = [0.500000000000010769, 0.500000000000027]

We can tell that the pruning step i2 => i3 is not valid. I'll take a closer look at this problem.

[soonhokong]

Fixed by 0615578569656624553c038909fae2202440fcee.

[scungao]

Hooray!

[soonhokong]

:clap:

More emojis at http://www.emoji-cheat-sheet.com/