Herbie run

Date:Wednesday, March 26th, 2025
Commit:a931ba94 on hardware-accelerators
Seed:2025085
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:81 161.4 MB

Time bar (total: 1.3min)

sample39.4s (48.8%)

Memory
707.2MiB live, 38 764.4MiB allocated; 11.9s collecting garbage
Samples
11.8s16 377×5exit
6.8s39 448×1valid
6.6s108 825×0valid
5.3s16 847×2valid
428.0ms3 867×0invalid
136.0ms1 376×0exit
Precisions
Click to see histograms. Total time spent on operations: 24.7s
ival-pow: 4.5s (18% of total)
ival-exp: 4.4s (17.9% of total)
adjust: 2.8s (11.3% of total)
ival-cos: 2.0s (8.1% of total)
ival-log: 1.6s (6.5% of total)
ival-mult!: 1.5s (6.1% of total)
ival-tan: 1.4s (5.6% of total)
ival-sqrt: 1.4s (5.5% of total)
ival-sinh: 792.0ms (3.2% of total)
ival-fmod: 767.0ms (3.1% of total)
ival-div!: 685.0ms (2.8% of total)
ival-sin: 676.0ms (2.7% of total)
ival-acos: 484.0ms (2% of total)
ival-pow2: 466.0ms (1.9% of total)
ival-sub!: 346.0ms (1.4% of total)
ival-add!: 330.0ms (1.3% of total)
ival-neg: 241.0ms (1% of total)
ival-hypot: 183.0ms (0.7% of total)
ival-<=: 74.0ms (0.3% of total)
ival-atan: 49.0ms (0.2% of total)
ival-and: 35.0ms (0.1% of total)
ival-or: 16.0ms (0.1% of total)
ival-assert: 3.0ms (0% of total)
ival-<: 2.0ms (0% of total)
ival->: 1.0ms (0% of total)
Bogosity

rewrite11.1s (13.8%)

Memory
99.4MiB live, 10 180.8MiB allocated; 3.0s collecting garbage
Stop Event
190×iter limit
50×node limit
17×unsound
saturated
Counts
7 827 → 15 998

regimes6.1s (7.6%)

Memory
-170.8MiB live, 7 409.7MiB allocated; 1.9s collecting garbage
Counts
3 946 → 200
Calls

53 calls:

798.0ms
b
786.0ms
x
620.0ms
a
397.0ms
r
262.0ms
(+.f64 x (-.f64 (tan.f64 (+.f64 y z)) (tan.f64 a)))
Compiler

Compiled 1 724 to 2 035 computations (-18% saved)

preprocess5.6s (7%)

Memory
232.7MiB live, 4 519.2MiB allocated; 813ms collecting garbage
Stop Event
38×iter limit
29×node limit
13×saturated
Compiler

Compiled 10 539 to 3 412 computations (67.6% saved)

eval3.3s (4.1%)

Memory
-48.1MiB live, 3 785.3MiB allocated; 1.4s collecting garbage
Compiler

Compiled 633 615 to 78 705 computations (87.6% saved)

derivations3.1s (3.9%)

Memory
62.6MiB live, 2 717.2MiB allocated; 364ms collecting garbage
Stop Event
12×fuel
done
Compiler

Compiled 4 193 to 1 030 computations (75.4% saved)

series3.1s (3.8%)

Memory
-331.3MiB live, 3 610.9MiB allocated; 1.0s collecting garbage
Counts
1 526 → 6 301
Calls

390 calls:

TimeVariablePointExpression
318.0ms
r
@0
((/ (* r (sin b)) (+ (* (sin a) (neg (sin b))) (* (cos a) (cos b)))) (* r (sin b)) r (sin b) b (+ (* (sin a) (neg (sin b))) (* (cos a) (cos b))) (sin a) a (neg (sin b)) (* (cos a) (cos b)) (cos a) (cos b) (/ (* r (sin b)) (cos (+ a b))) (* r (tan b)) (* (+ (* 1/3 (* (* b b) r)) r) b) (+ (* 1/3 (* (* b b) r)) r) 1/3 (* (* b b) r) (* b b) (/ (* r (sin b)) (sin (+ (neg (+ a b)) (/ (PI) 2)))) (sin (+ (neg (+ a b)) (/ (PI) 2))) (+ (neg (+ a b)) (/ (PI) 2)) (neg (+ a b)) (+ a b) (/ (PI) 2) (PI) 2 (/ (* r (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)) (/ (* r (sin b)) (cos (+ a b))) (cos (+ a b)) (+ a b) (* (/ (+ (pow (/ b a) 3) 1) (+ (pow (/ b a) 2) (- 1 (/ b a)))) a) (/ (+ (pow (/ b a) 3) 1) (+ (pow (/ b a) 2) (- 1 (/ b a)))) (+ (pow (/ b a) 3) 1) (pow (/ b a) 3) (/ b a) 3 1 (+ (pow (/ b a) 2) (- 1 (/ b a))) (pow (/ b a) 2) (- 1 (/ b a)))
109.0ms
x
@inf
((log (/ (sinh x) x)) (/ (sinh x) x) (sinh x) x)
79.0ms
x
@0
((* (fmod (exp x) (sqrt (cos x))) (exp (neg x))) (fmod (exp x) (sqrt (cos x))) (exp x) x (sqrt (cos x)) (+ (* (* x x) -1/4) 1) (* (* (- (pow x -2) 1/4) x) x) (* (- (pow x -2) 1/4) x) (- (pow x -2) 1/4) (pow x -2) -2 1/4 (exp (neg x)) (neg x) (* (fmod (exp x) (sqrt (cos x))) (/ (- (* (cosh x) (cosh x)) (* (sinh x) (sinh x))) (exp x))) (fmod (exp x) (sqrt (cos x))) (exp x) 1 (sqrt (cos x)) (cos x) (/ (- (* (cosh x) (cosh x)) (* (sinh x) (sinh x))) (exp x)) (+ (* (- (* 1/2 x) 1) x) 1) (- (* 1/2 x) 1) (* 1/2 x) 1/2 (* (fmod (exp x) (sqrt (cos x))) (/ (- (* (cosh x) (cosh x)) (* (sinh x) (sinh x))) (exp x))) (fmod (exp x) (sqrt (cos x))) (sqrt (cos x)) (+ (* (* x x) -1/4) 1) (* x x) -1/4 (* (fmod (exp x) (sqrt (cos x))) (exp (neg x))) (fmod (exp x) (sqrt (cos x))) (sqrt (cos x)) (+ (* (* x x) -1/4) 1) (* (- (* (/ -1 x) (/ -1 x)) 1/4) (* x x)) (- (* (/ -1 x) (/ -1 x)) 1/4) (* (/ -1 x) (/ -1 x)) (/ -1 x) -1 (* (fmod (exp x) (sqrt (cos x))) (exp (neg x))) (fmod (exp x) (sqrt (cos x))) (sqrt (cos x)) (+ (* (* x x) -1/4) 1) (* (- (pow x -2) 1/4) (exp (* (log x) 2))) (exp (* (log x) 2)) (* (log x) 2) (log x) 2)
74.0ms
x
@inf
((- (log (sinh x)) (log 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) 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) (+ (* -1/37800 (* x x)) 1/2835) 1/2835 x -1/180 (* x x) 1/6 (- (log (sinh x)) (log 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) 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) (log (/ (sinh x) x)) (/ (sinh x) x) (+ (* (* 1/6 x) x) 1) (* 1/6 x) 1 (log (/ (sinh x) x)) (* (/ (* x (- (pow (* (* (+ (* (* x x) 1/2835) -1/180) x) x) 2) 1/36)) (+ (* (+ (* (* x x) 1/2835) -1/180) (* x x)) -1/6)) x) (/ (* x (- (pow (* (* (+ (* (* x x) 1/2835) -1/180) x) x) 2) 1/36)) (+ (* (+ (* (* x x) 1/2835) -1/180) (* x x)) -1/6)) (* x (- (pow (* (* (+ (* (* x x) 1/2835) -1/180) x) x) 2) 1/36)) (- (pow (* (* (+ (* (* x x) 1/2835) -1/180) x) x) 2) 1/36) (pow (* (* (+ (* (* x x) 1/2835) -1/180) x) x) 2) (* (* (+ (* (* x x) 1/2835) -1/180) x) x) (* (+ (* (* x x) 1/2835) -1/180) x) (+ (* (* x x) 1/2835) -1/180) 2 1/36 (+ (* (+ (* (* x x) 1/2835) -1/180) (* x x)) -1/6) -1/6 (log (/ (sinh x) x)) (/ (* (* x x) (+ 1/216 (* (pow (+ (* (* x x) 1/2835) -1/180) 3) (pow x 6)))) (+ 1/36 (* (* (* (+ (* (* x x) 1/2835) -1/180) x) x) (+ (* (+ (* (* x x) 1/2835) -1/180) (* x x)) -1/6)))) (* (- (+ (/ 1/6 (pow x 4)) 1/2835) (* (pow x -2) 1/180)) (pow x 6)) (- (+ (/ 1/6 (pow x 4)) 1/2835) (* (pow x -2) 1/180)) (+ (/ 1/6 (pow x 4)) 1/2835) (/ 1/6 (pow x 4)) (pow x 4) 4 (* (pow x -2) 1/180) (pow x -2) -2 1/180 (pow x 6) 6)
66.0ms
x
@-inf
((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)) 1/2835 (* x x) x 1/180 1/6 (log (/ (sinh x) x)) (* (* x x) 1/6) (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 (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))

explain2.6s (3.2%)

Memory
-171.0MiB live, 2 746.1MiB allocated; 624ms collecting garbage
Explanations
Click to see full explanations table
OperatorSubexpressionExplanationCount
sqrt.f64#foflow-rescue5830
cos.f64#fsensitivity5162
-.f64#fcancellation3440
sqrt.f64#fuflow-rescue3270
/.f64#fn/o2600
acos.f64(acos.f64 (-.f64 #s(literal 1 binary64) x))sensitivity2510
log.f64(log.f64 (/.f64 (sinh.f64 x) x))sensitivity2451
tan.f64(tan.f64 (+.f64 y z))sensitivity1950
pow.f64(pow.f64 l (exp.f64 w))sensitivity12116
*.f64#fn*o350
*.f64#fn*u350
*.f64(*.f64 (pow.f64 c #s(literal 2 binary64)) (*.f64 (*.f64 x (pow.f64 s #s(literal 2 binary64))) x))u*o180
(pow.f64 c #s(literal 2 binary64))underflow75
(*.f64 (*.f64 x (pow.f64 s #s(literal 2 binary64))) x)overflow65
(*.f64 x (pow.f64 s #s(literal 2 binary64)))overflow60
(pow.f64 s #s(literal 2 binary64))overflow67
*.f64(*.f64 (pow.f64 c #s(literal 2 binary64)) (*.f64 (*.f64 x (pow.f64 s #s(literal 2 binary64))) x))o*u170
(pow.f64 c #s(literal 2 binary64))overflow56
(*.f64 (*.f64 x (pow.f64 s #s(literal 2 binary64))) x)underflow81
(*.f64 x (pow.f64 s #s(literal 2 binary64)))underflow72
(pow.f64 s #s(literal 2 binary64))underflow70
-.f64(-.f64 (*.f64 a a) (*.f64 b b))nan-rescue90
(*.f64 a a)overflow110
(*.f64 b b)overflow9
log.f64(log.f64 (/.f64 (sinh.f64 x) x))oflow-rescue50
(sinh.f64 x)overflow5
(/.f64 (sinh.f64 x) x)overflow5
tan.f64(tan.f64 (+.f64 y z))cancellation10
+.f64(+.f64 x (-.f64 (tan.f64 (+.f64 y z)) (tan.f64 a)))cancellation10
Confusion
Predicted +Predicted -
+2214271
-6821953
Precision
0.7645027624309392
Recall
0.8909456740442656
Confusion?
Predicted +Predicted MaybePredicted -
+22143268
-682161937
Precision?
0.760548885077187
Recall?
0.8921529175050302
Freqs
test
numberfreq
02224
12830
265
31
Total Confusion?
Predicted +Predicted MaybePredicted -
+1701
-002
Precision?
1.0
Recall?
0.9444444444444444
Samples
612.0ms2 496×1valid
378.0ms6 594×0valid
324.0ms1 046×2valid
14.0ms104×1exit
Compiler

Compiled 1 067 to 440 computations (58.8% saved)

Precisions
Click to see histograms. Total time spent on operations: 905.0ms
ival-sqrt: 128.0ms (14.1% of total)
ival-tan: 115.0ms (12.7% of total)
ival-cos: 105.0ms (11.6% of total)
adjust: 84.0ms (9.3% of total)
ival-mult!: 73.0ms (8.1% of total)
ival-log: 66.0ms (7.3% of total)
ival-sinh: 57.0ms (6.3% of total)
ival-exp: 40.0ms (4.4% of total)
ival-sub!: 40.0ms (4.4% of total)
ival-sin: 40.0ms (4.4% of total)
ival-pow2: 35.0ms (3.9% of total)
ival-fmod: 29.0ms (3.2% of total)
ival-acos: 29.0ms (3.2% of total)
ival-div!: 23.0ms (2.5% of total)
ival-add!: 18.0ms (2% of total)
ival-hypot: 9.0ms (1% of total)
ival-pow: 8.0ms (0.9% of total)
ival-neg: 5.0ms (0.6% of total)
ival-atan: 3.0ms (0.3% of total)

prune2.4s (3%)

Memory
197.3MiB live, 3 190.7MiB allocated; 393ms collecting garbage
Counts
20 068 → 1 556
Compiler

Compiled 86 998 to 45 219 computations (48% saved)

analyze2.0s (2.4%)

Memory
-46.5MiB live, 2 107.2MiB allocated; 543ms 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)

bsearch1.1s (1.3%)

Memory
19.0MiB live, 1 163.6MiB allocated; 122ms collecting garbage
Algorithm
51×binary-search
18×left-value
Stop Event
31×narrow-enough
11×predicate-same
predicate-failed
Samples
338.0ms1 516×1valid
127.0ms1 316×0valid
106.0ms909×0invalid
93.0ms160×2valid
Compiler

Compiled 13 315 to 10 511 computations (21.1% saved)

Precisions
Click to see histograms. Total time spent on operations: 541.0ms
ival-cos: 131.0ms (24.2% of total)
ival-exp: 112.0ms (20.7% of total)
ival-tan: 70.0ms (12.9% of total)
ival-fmod: 50.0ms (9.2% of total)
ival-sin: 38.0ms (7% of total)
adjust: 36.0ms (6.7% of total)
ival-mult!: 28.0ms (5.2% of total)
ival-div!: 26.0ms (4.8% of total)
ival-sqrt: 16.0ms (3% of total)
ival-pow2: 10.0ms (1.8% of total)
ival-add!: 9.0ms (1.7% of total)
ival-neg: 6.0ms (1.1% of total)
ival-acos: 4.0ms (0.7% of total)
ival-sub!: 3.0ms (0.6% of total)
ival-pow: 1.0ms (0.2% of total)

simplify917.0ms (1.1%)

Memory
-25.8MiB live, 964.9MiB allocated; 154ms collecting garbage
Stop Event
15×node limit
saturated

start1.0ms (0%)

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

end0.0ms (0%)

Memory
0.1MiB live, 0.2MiB allocated; 0ms collecting garbage

Profiling

Loading profile data...