search

dreal / dreal2

Please check dreal4 instead.
https://github.com/dreal/dreal4
GNU General Public License v3.0
13 stars 15 forks source link

FP precision in proof is not precise enough #11

Closed soonhokong closed 10 years ago

soonhokong commented 10 years ago 
[before pruning]
x3: [4 , 6.3504];
x6: [4 , 6.3504];
x5: [4 , 6.3504];
x2: [4 , 6.3504];
x4: [6.3504 , 8];
x1: [4 , 6.3504]
[after pruning]
x3: [4 , 6.3504];
x6: [4 , 6.3504];
x5: [4 , 6.3504];
x2: [4 , 6.3504];
x4: [6.3504 , 8];
x1: [4 , 6.3504]
soonhokong commented 10 years ago

Using %a format specifier seems reasonable. http://stackoverflow.com/questions/4826842/the-format-specifier-a-for-printf-in-c

BatFloat.of_string is able to parse the output formatted by "%a" specifier. http://ocaml-batteries-team.github.io/batteries-included/hdoc2/BatFloat.html

soonhokong commented 10 years ago

fixed by a8d39ad85bd045cfac05d8e6f46cd6a4fb8e3e1c(Ocaml) and 044376cc96494465d51e289fd393842d64849ab9(C++).