Herbie run

Date:Thursday, March 20th, 2025
Commit:5f89ad90 on remove_exactness_test
Seed:2025079
Parameters:256 points for 4 iterations
Flags:
reduce:regimesreduce:binary-searchreduce:branch-expressionsreduce:simplifysetup:simplifysetup:searchrules:arithmeticrules:polynomialsrules:fractionsrules:exponentsrules:trigonometryrules:hyperbolicrules:numericsrules:specialrules:boolsrules:branchesgenerate:rrgenerate:taylorgenerate:simplifygenerate:proofs
default
Memory:77 334.1 MB

Time bar (total: 1.4min)

sample45.2s (55.1%)

Memory
655.7MiB live, 41 253.5MiB allocated; 12.7s collecting garbage
Samples
14.3s16 561×5exit
8.3s108 709×0valid
7.6s39 953×1valid
5.9s16 458×2valid
519.0ms3 931×0invalid
131.0ms1 412×0exit
Precisions
Click to see histograms. Total time spent on operations: 29.5s
ival-exp: 4.2s (14.3% of total)
adjust: 3.6s (12.2% of total)
ival-pow: 3.5s (11.8% of total)
ival-log: 3.0s (10% of total)
ival-cos: 2.3s (7.8% of total)
ival-mult: 2.0s (6.7% of total)
ival-sinh: 1.5s (5.2% of total)
ival-tan: 1.3s (4.4% of total)
ival-sub: 1.2s (4.1% of total)
ival-sqrt: 1.2s (4% of total)
ival-div: 911.0ms (3.1% of total)
ival-fmod: 872.0ms (3% of total)
ival-sin: 674.0ms (2.3% of total)
ival-add: 659.0ms (2.2% of total)
ival-acos: 510.0ms (1.7% of total)
ival-pow2: 493.0ms (1.7% of total)
ival-hypot: 475.0ms (1.6% of total)
const: 374.0ms (1.3% of total)
ival-atan: 321.0ms (1.1% of total)
ival-neg: 241.0ms (0.8% of total)
ival-<=: 85.0ms (0.3% of total)
ival-assert: 75.0ms (0.3% of total)
ival-and: 42.0ms (0.1% of total)
exact: 42.0ms (0.1% of total)
ival-or: 21.0ms (0.1% of total)
ival->: 2.0ms (0% of total)
ival-==: 2.0ms (0% of total)
ival-<: 2.0ms (0% of total)
Bogosity

rewrite10.1s (12.4%)

Memory
169.6MiB live, 9 341.3MiB allocated; 1.7s collecting garbage
Stop Event
192×iter limit
50×node limit
17×unsound
4×saturated
Counts
7 518 → 15 801

regimes4.8s (5.8%)

Memory
-112.4MiB live, 4 822.5MiB allocated; 1.4s collecting garbage
Counts
3 004 → 172
Calls

53 calls:

596.0ms
x
435.0ms
a
331.0ms
b
244.0ms
(+.f64 y z)
224.0ms
r
Compiler

Compiled 1 538 to 1 822 computations (-18.5% saved)

preprocess4.4s (5.4%)

Memory
129.0MiB live, 3 540.0MiB allocated; 653ms collecting garbage
Stop Event
38×iter limit
29×node limit
13×saturated
Compiler

Compiled 8 423 to 3 006 computations (64.3% saved)

derivations2.9s (3.6%)

Memory
-1.4MiB live, 2 245.1MiB allocated; 255ms collecting garbage
Stop Event
11×fuel
9×done
Compiler

Compiled 3 362 to 927 computations (72.4% saved)

eval2.9s (3.5%)

Memory
128.5MiB live, 3 844.3MiB allocated; 863ms collecting garbage
Compiler

Compiled 630 217 to 78 362 computations (87.6% saved)

explain2.9s (3.5%)

Memory
61.5MiB live, 3 201.9MiB allocated; 423ms collecting garbage
Explanations
Click to see full explanations table
OperatorSubexpressionExplanationCount
sqrt.f64#foflow-rescue5810
cos.f64#fsensitivity5070
-.f64#fcancellation3440
sqrt.f64#fuflow-rescue3350
acos.f64(acos.f64 (-.f64 #s(literal 1 binary64) x))sensitivity2560
/.f64(/.f64 (-.f64 x lo) (-.f64 hi lo))n/o2550
↳(-.f64 hi lo)overflow256
log.f64(log.f64 (/.f64 (sinh.f64 x) x))sensitivity2511
tan.f64(tan.f64 (+.f64 y z))sensitivity1941
pow.f64(pow.f64 l (exp.f64 w))sensitivity11915
*.f64#fn*o390
*.f64#fn*u300
*.f64(*.f64 (pow.f64 c #s(literal 2 binary64)) (*.f64 (*.f64 x (pow.f64 s #s(literal 2 binary64))) x))o*u200
↳(pow.f64 c #s(literal 2 binary64))overflow67
↳(*.f64 (*.f64 x (pow.f64 s #s(literal 2 binary64))) x)underflow76
↳(*.f64 x (pow.f64 s #s(literal 2 binary64)))underflow63
↳(pow.f64 s #s(literal 2 binary64))underflow61
*.f64#fu*o170
-.f64(-.f64 (*.f64 a a) (*.f64 b b))nan-rescue120
↳(*.f64 a a)overflow121
↳(*.f64 b b)overflow12
log.f64(log.f64 (/.f64 (sinh.f64 x) x))oflow-rescue20
↳(sinh.f64 x)overflow2
↳(/.f64 (sinh.f64 x) x)overflow2
/.f64(/.f64 (-.f64 x lo) (-.f64 hi lo))o/o10
↳(-.f64 x lo)overflow1
↳(-.f64 hi lo)overflow256
exp.f64(exp.f64 (neg.f64 x))sensitivity10
+.f64(+.f64 x (-.f64 (tan.f64 (+.f64 y z)) (tan.f64 a)))cancellation10
Confusion
Predicted +Predicted -
+2242263
-6601955
Precision
0.7725706409372847
Recall
0.8950099800399202
Confusion?
Predicted +Predicted MaybePredicted -
+22421262
-660161939
Precision?
0.7684138403562863
Recall?
0.8954091816367266
Freqs
test
numberfreq
02218
12841
259
32
Total Confusion?
Predicted +Predicted MaybePredicted -
+1800
-002
Precision?
1.0
Recall?
1.0
Samples
454.0ms6 640×0valid
441.0ms2 472×1valid
440.0ms90×5exit
369.0ms1 038×2valid
Compiler

Compiled 1 067 to 440 computations (58.8% saved)

Precisions
Click to see histograms. Total time spent on operations: 1.3s
ival-cos: 442.0ms (34.1% of total)
adjust: 126.0ms (9.7% of total)
ival-log: 94.0ms (7.3% of total)
ival-mult: 87.0ms (6.7% of total)
ival-tan: 75.0ms (5.8% of total)
ival-sqrt: 68.0ms (5.2% of total)
ival-exp: 66.0ms (5.1% of total)
ival-fmod: 50.0ms (3.9% of total)
ival-sin: 40.0ms (3.1% of total)
ival-sinh: 39.0ms (3% of total)
ival-sub: 37.0ms (2.9% of total)
ival-add: 36.0ms (2.8% of total)
ival-pow2: 35.0ms (2.7% of total)
ival-div: 30.0ms (2.3% of total)
ival-acos: 29.0ms (2.2% of total)
ival-true: 9.0ms (0.7% of total)
ival-hypot: 9.0ms (0.7% of total)
ival-pow: 8.0ms (0.6% of total)
ival-neg: 7.0ms (0.5% of total)
ival-assert: 5.0ms (0.4% of total)
ival-atan: 3.0ms (0.2% of total)
exact: 2.0ms (0.2% of total)

analyze2.8s (3.5%)

Memory
-10.9MiB live, 2 541.9MiB allocated; 1.2s collecting garbage
Algorithm
20×search
Search
ProbabilityValidUnknownPreconditionInfiniteDomainCan'tIter
0%0%73.7%26.3%0%0%0%0
28.8%21.3%52.5%26.3%0%0%0%1
44.1%32.5%41.2%26.3%0%0%0%2
52.6%38.7%35%26.3%0%0%0%3
61.9%45.6%28.1%26.3%0%0%0%4
65.2%47.5%25.3%26.3%0%0.9%0%5
66.8%48.4%24%26.3%0%1.2%0%6
71.1%51.1%20.8%26.3%0%1.9%0%7
72.1%51.6%20%26.3%0%2.1%0%8
74.4%53%18.2%26.3%0%2.5%0%9
75.8%53.9%17.2%26.3%0%2.6%0%10
76.6%54.3%16.6%26.3%0%2.8%0%11
77.3%54.8%16.1%26.3%0%2.9%0%12
Compiler

Compiled 279 to 216 computations (22.6% saved)

prune2.7s (3.2%)

Memory
-248.8MiB live, 2 835.6MiB allocated; 1.9s collecting garbage
Counts
19 585 → 1 376
Compiler

Compiled 68 956 to 37 447 computations (45.7% saved)

series2.6s (3.1%)

Memory
293.0MiB live, 3 196.4MiB allocated; 429ms collecting garbage
Counts
1 443 → 6 075
Calls

387 calls:

TimeVariablePointExpression
88.0ms
l
@-inf
((/ (exp (neg w)) (pow l (neg (exp w)))) (exp (neg w)) (neg w) w (pow l (neg (exp w))) l (neg (exp w)) (exp w) (exp (+ (neg w) (* (log l) (exp w)))) (+ (neg w) (* (log l) (exp w))) (* (exp (neg w)) (pow l (exp w))) (exp (neg w)) (- 1 w) 1 (pow l (exp w)) (exp w) (+ (* (+ (* (+ (* 1/6 w) 1/2) w) 1) w) 1) (+ (* (+ (* 1/6 w) 1/2) w) 1) (+ (* 1/6 w) 1/2) 1/6 1/2 (exp (+ (neg w) (* (log l) (exp w)))) (+ (neg w) (* (log l) (exp w))) (- (* (log l) (exp w)) w) (* (log l) (exp w)) (log l) (exp (+ (neg w) (* (log l) (exp w)))) (+ (* (* l (+ (* (+ (* (pow (- (log l) 1) 2) 1/2) (log (sqrt l))) w) (- (log l) 1))) w) l) (* l (+ (* (+ (* (pow (- (log l) 1) 2) 1/2) (log (sqrt l))) w) (- (log l) 1))) (+ (* (+ (* (pow (- (log l) 1) 2) 1/2) (log (sqrt l))) w) (- (log l) 1)) (+ (* (pow (- (log l) 1) 2) 1/2) (log (sqrt l))) (pow (- (log l) 1) 2) (- (log l) 1) 2 (log (sqrt l)) (sqrt l))
85.0ms
x
@inf
((log (/ (sinh x) x)) (+ (* (* (* (+ (* (* (+ (* (* x x) -1/37800) 1/2835) x) x) -1/180) x) x) (* x x)) (* 1/6 (* x x))) (* (* (+ (* (* (+ (* (* x x) -1/37800) 1/2835) x) x) -1/180) x) x) (* (+ (* (* (+ (* (* x x) -1/37800) 1/2835) x) x) -1/180) x) (+ (* (* (+ (* (* x x) -1/37800) 1/2835) x) x) -1/180) (* (+ (* (* x x) -1/37800) 1/2835) x) (+ (* (* x x) -1/37800) 1/2835) (* x x) x -1/37800 1/2835 -1/180 (* 1/6 (* x x)) 1/6 (- (log (sinh x)) (log x)) (* (* (+ (* (+ (* (* (+ (* (* x x) -1/37800) 1/2835) x) x) -1/180) (* x x)) 1/6) x) x) (* (+ (* (* x x) -1/180) 1/6) (* x x)) (+ (* (* x x) -1/180) 1/6) (log (/ (sinh x) x)) (* (+ (* (+ (* (* 1/2835 x) x) -1/180) (* x x)) 1/6) (* x x)) (+ (* (+ (* (* 1/2835 x) x) -1/180) (* x x)) 1/6) (+ (* (* 1/2835 x) x) -1/180) (* 1/2835 x) (log (/ (sinh x) x)) (/ (sinh x) x) (+ (* (+ (* 1/120 (* x x)) 1/6) (* x x)) 1) (+ (* 1/120 (* x x)) 1/6) (* 1/120 (* x x)) 1/120 1 (log (/ (sinh x) x)) (/ (* (* x x) (- (pow (* (* (+ (* (* (+ (* (* x x) -1/37800) 1/2835) x) x) -1/180) x) x) 2) 1/36)) (+ (* (+ (* (* (+ (* (* x x) -1/37800) 1/2835) x) x) -1/180) (* x x)) -1/6)) (* (* x x) (- (pow (* (* (+ (* (* (+ (* (* x x) -1/37800) 1/2835) x) x) -1/180) x) x) 2) 1/36)) (- (pow (* (* (+ (* (* (+ (* (* x x) -1/37800) 1/2835) x) x) -1/180) x) x) 2) 1/36) (pow (* (* (+ (* (* (+ (* (* x x) -1/37800) 1/2835) x) x) -1/180) x) x) 2) 2 1/36 (+ (* (+ (* (* (+ (* (* x x) -1/37800) 1/2835) x) x) -1/180) (* x x)) -1/6) -1/6)
66.0ms
x
@-inf
((log (/ (sinh x) x)) (* (+ (* (- (* (* (+ (* -1/37800 (* x x)) 1/2835) x) x) 1/180) (* x x)) 1/6) (* x x)) (+ (* (- (* (* (+ (* -1/37800 (* x x)) 1/2835) x) x) 1/180) (* x x)) 1/6) (- (* (* (+ (* -1/37800 (* x x)) 1/2835) x) x) 1/180) (* (* (+ (* -1/37800 (* x x)) 1/2835) x) x) (* (+ (* -1/37800 (* x x)) 1/2835) x) (+ (* -1/37800 (* x x)) 1/2835) -1/37800 (* x x) x 1/2835 1/180 1/6 (log (/ (sinh x) x)) (* (* x x) 1/6) (log (/ (sinh x) x)) (* (* (+ (* (- (* 1/2835 (* x x)) 1/180) (* x x)) 1/6) x) x) (* (+ (* (- (* 1/2835 (* x x)) 1/180) (* x x)) 1/6) x) (+ (* (- (* 1/2835 (* x x)) 1/180) (* x x)) 1/6) (- (* 1/2835 (* x x)) 1/180) (* 1/2835 (* x x)) (log (/ (sinh x) x)) (/ (sinh x) x) (+ (* (+ (* 1/120 (* x x)) 1/6) (* x x)) 1) (+ (* 1/120 (* x x)) 1/6) 1/120 1 (- (log (sinh x)) (log x)) (log (sinh x)) (sinh x) (log x))
66.0ms
x
@-inf
((log (/ (sinh x) x)) (+ (* (* (* (+ (* (* (+ (* (* x x) -1/37800) 1/2835) x) x) -1/180) x) x) (* x x)) (* 1/6 (* x x))) (* (* (+ (* (* (+ (* (* x x) -1/37800) 1/2835) x) x) -1/180) x) x) (* (+ (* (* (+ (* (* x x) -1/37800) 1/2835) x) x) -1/180) x) (+ (* (* (+ (* (* x x) -1/37800) 1/2835) x) x) -1/180) (* (+ (* (* x x) -1/37800) 1/2835) x) (+ (* (* x x) -1/37800) 1/2835) (* x x) x -1/37800 1/2835 -1/180 (* 1/6 (* x x)) 1/6 (- (log (sinh x)) (log x)) (* (* (+ (* (+ (* (* (+ (* (* x x) -1/37800) 1/2835) x) x) -1/180) (* x x)) 1/6) x) x) (* (+ (* (* x x) -1/180) 1/6) (* x x)) (+ (* (* x x) -1/180) 1/6) (log (/ (sinh x) x)) (* (+ (* (+ (* (* 1/2835 x) x) -1/180) (* x x)) 1/6) (* x x)) (+ (* (+ (* (* 1/2835 x) x) -1/180) (* x x)) 1/6) (+ (* (* 1/2835 x) x) -1/180) (* 1/2835 x) (log (/ (sinh x) x)) (/ (sinh x) x) (+ (* (+ (* 1/120 (* x x)) 1/6) (* x x)) 1) (+ (* 1/120 (* x x)) 1/6) (* 1/120 (* x x)) 1/120 1 (log (/ (sinh x) x)) (/ (* (* x x) (- (pow (* (* (+ (* (* (+ (* (* x x) -1/37800) 1/2835) x) x) -1/180) x) x) 2) 1/36)) (+ (* (+ (* (* (+ (* (* x x) -1/37800) 1/2835) x) x) -1/180) (* x x)) -1/6)) (* (* x x) (- (pow (* (* (+ (* (* (+ (* (* x x) -1/37800) 1/2835) x) x) -1/180) x) x) 2) 1/36)) (- (pow (* (* (+ (* (* (+ (* (* x x) -1/37800) 1/2835) x) x) -1/180) x) x) 2) 1/36) (pow (* (* (+ (* (* (+ (* (* x x) -1/37800) 1/2835) x) x) -1/180) x) x) 2) 2 1/36 (+ (* (+ (* (* (+ (* (* x x) -1/37800) 1/2835) x) x) -1/180) (* x x)) -1/6) -1/6)
57.0ms
r
@0
((* r (/ (sin b) (+ (* (cos b) (cos a)) (* (neg (sin b)) (sin a))))) r (/ (sin b) (+ (* (cos b) (cos a)) (* (neg (sin b)) (sin a)))) (sin b) b (+ (* (cos b) (cos a)) (* (neg (sin b)) (sin a))) (cos b) (cos a) a (* (neg (sin b)) (sin a)) (neg (sin b)) (sin a) (* r (/ (sin b) (cos (+ a b)))) (/ (sin b) (cos (+ a b))) (tan b) (* r (/ (sin b) (cos (+ a b)))) (/ (sin b) (cos (+ a b))) (sin b) (* (+ (* (* b b) -1/6) 1) b) (+ (* (* b b) -1/6) 1) (* b b) -1/6 1 (cos (+ a b)) (+ a b) (* r (/ (sin b) (- (* (cos b) (cos a)) (* (sin b) (sin a))))) (/ (* (sin b) r) (sin (+ (+ (* 1/2 (PI)) b) a))) (* (sin b) r) (sin (+ (+ (* 1/2 (PI)) b) a)) (+ (+ (* 1/2 (PI)) b) a) (+ (* 1/2 (PI)) b) 1/2 (PI) (* r (/ (sin b) (- (* (cos b) (cos a)) (* (sin b) (sin a))))) (/ (sin b) (- (* (cos b) (cos a)) (* (sin b) (sin a)))) (- (* (cos b) (cos a)) (* (sin b) (sin a))) (* (cos b) (cos a)) (* (sin b) (sin a)))

bsearch715.0ms (0.9%)

Memory
-65.1MiB live, 509.9MiB allocated; 73ms collecting garbage
Algorithm
36×binary-search
15×left-value
Stop Event
35×narrow-enough
1×predicate-same
Samples
295.0ms1 136×1valid
144.0ms1 904×0valid
53.0ms128×2valid
1.0ms8×0exit
Compiler

Compiled 10 926 to 9 225 computations (15.6% saved)

Precisions
Click to see histograms. Total time spent on operations: 399.0ms
ival-tan: 102.0ms (25.5% of total)
adjust: 70.0ms (17.5% of total)
ival-mult: 39.0ms (9.8% of total)
ival-cos: 38.0ms (9.5% of total)
ival-exp: 35.0ms (8.8% of total)
ival-sin: 29.0ms (7.3% of total)
ival-add: 26.0ms (6.5% of total)
ival-pow: 14.0ms (3.5% of total)
ival-div: 11.0ms (2.8% of total)
ival-fmod: 11.0ms (2.8% of total)
ival-sub: 7.0ms (1.8% of total)
ival-pow2: 5.0ms (1.3% of total)
ival-neg: 4.0ms (1% of total)
ival-sqrt: 3.0ms (0.8% of total)
ival-true: 2.0ms (0.5% of total)
ival-assert: 1.0ms (0.3% of total)
exact: 0.0ms (0% of total)

start1.0ms (0%)

Memory
1.5MiB live, 1.5MiB allocated; 0ms collecting garbage

end0.0ms (0%)

Memory
0.3MiB live, 0.3MiB allocated; 0ms collecting garbage

Profiling

Loading profile data...