Closed yixin-09 closed 5 years ago
HazardousPeach
commented
5 years ago You won't be able to print the ranges to an arbitrary number of digits, since they refer to values that actually flowed through the client program, not their high-precision equivalents. But I added a --double-ranges flag that will print them in double precision by converting to MPFR and using that printer, instead of using the built-in valgrind printer. #46
yixin-09
commented
5 years ago You won't be able to print the ranges to an arbitrary number of digits, since they refer to values that actually flowed through the client program, not their high-precision equivalents. But I added a
--double-rangesflag that will print them in double precision by converting to MPFR and using that printer, instead of using the built-in valgrind printer. #46
I have test the "--double-ranges", it works on ranges, however, I found the value in the expression still not print in double precision. Can you make it change at same time? E.g. In (- (+ (- ( (+ x y) (/ z 2.000000)) (+ (- a b) c)) ( 5.000000e-1 2.142694)) (log i))) 2.142694 only have single precision. PS: (FPCore (x y z a b c i) :pre (and (and (<= 0.00000000000000e-1 x) (<= x 2.13587029916989e-3)) (and (<= 4.00000000000000e-19 y) (<= y 7.23324281221258e-2)) (and (<= 1.99955155148761e0 z) (<= z 1.99999999654907e0)) (and (<= 0.00000000000000e-1 a) (<= a 2.17118891448016e-3)) (and (<= 0.00000000000000e-1 b) (<= b 3.53186153102728e-5)) (and (<= 4.00000000000000e-19 c) (<= c 7.23324281221258e-2)) (and (<= 3.14141654333462e0 i) (<= i 3.14159265223462e0))) (- (+ (- ( (+ x y) (/ z 2.000000)) (+ (- a b) c)) ( 5.000000e-1 2.142694)) (log i)))
HazardousPeach
commented
5 years ago Hey @yixin-09, just fixed your issue here. The option is now renamed to --full-precision-exprs and turns all the numbers printed in the output to double precision. Hope that covers what you needed, please feel free to reopen the issue if not.
HazardousPeach
commented
5 years ago As of 8840fbc origin/develop origin/master Change flag name
I had used the commend:
to test GSL's function gsl_sf_bessel_J0(x) with 10000 input in a range [200.27708813286995,200.2772234538162]
I get the output in test_gsl_sf_bessel_J0.out.gh is :
The FPcore expression in the out file is : `(FPCore (x y z a b c) :pre (and (and (<= 2.002771e2 x) (<= x 2.002772e2)) (and (<= 3.895342e-7 y) (<= y 3.895348e-7)) (and (<= 3.246119e-8 z) (<= z 3.246123e-8)) (and (<= -1.802558e-3 a) (<= a -1.802558e-3)) (and (<= 6.492237e-8 b) (<= b 6.492246e-8)) (and (<= 10.000000e-1 c) (<= c 10.000000e-1))) (- ( (+ (sin x) (cos x)) (- 1.000000 ( ( y 5.000000e-1) (- 1.000000 z)))) ( (- (sin x) (cos x)) ( (/ (+ -1.231958e-1 a) x) (- 1.000000 ( b c)))))))
The variable range in the expression seems only have single precision ((<= 2.002771e2 x) (<= x 2.002772e2)), how can I get more digits, e.g.((<= 200.27708813286995 x) (<= x 200.2772234538162))? The option "--longprint-len" seems not work for this.
I think it will influence the connection between Herbgrind and Herbie to repair floating-point expression in a small input range.