handle constants as intervals

dreal / dreal3

There is a new version of dReal, available at https://github.com/dreal/dreal4

GNU General Public License v3.0

48 stars 36 forks source link

handle constants as intervals #262

Closed soonhokong closed 8 years ago

soonhokong commented 8 years ago

Without this, for example, the following fails:

(set-logic QF_NRA)
(declare-fun x () Real)
(declare-fun y () Real)
(declare-fun z () Real)
(assert (= x 0.7))
(assert (= y 0.0647))
(assert (= z 0.6353))
(assert (= (+ y z) x))
(check-sat)
(exit)

There are more than one layer to fix:

how to represent constants in Enode - done by f3b79530577ba20ed545cd0052229ba4e75aa3f4
simplification - done by 727b145d7dcd217d3c756da2f9cc1881465bccc0
contractors (i.e. IBEX) - done by bec7e4e9c0b83d7fcebf937b376ab0d6c0da0193

soonhokong commented 8 years ago

There was a problem in strtod function which parses a char const * to double . eglibc (<= 2.16) doesn't honor rounding mode. As a result, some tests fail in Ubuntu-12.04. I've added a custom strtod function (from 1) as a workaround. Now it works on Ubuntu-12.04.

soonhokong commented 8 years ago

While testing, I found a case where this custom version is not correct. It violates the invariant lb <= ub. Possibly it's my mistake, I'm checking things..

soonhokong commented 8 years ago

Updated to the latest version of dtoa.c and it seems that it works. When testing finishes, I'll update the repo.