Herbie run

Date:Thursday, April 24th, 2025
Commit:d5acc5eb on main
Seed:2025114
Parameters:256 points for 4 iterations
Flags:
reduce:regimesreduce:binary-searchreduce:branch-expressionssetup:searchrules:arithmeticrules:polynomialsrules:fractionsrules:exponentsrules:trigonometryrules:hyperbolicrules:numericsrules:specialrules:boolsrules:branchesgenerate:rrgenerate:taylorgenerate:proofs
default
Memory:219 301.6 MB

Time bar (total: 2.9min)

sample1.1min (37.5%)

Memory
1 522.8MiB live, 86 930.6MiB allocated; 21.4s collecting garbage
Samples
34.6s433 888×0valid
7.0s26 376×1valid
3.9s9 400×2valid
1.0s4 431×0invalid
507.0ms8 217×0exit
326.0ms937×3valid
Precisions
Click to see histograms. Total time spent on operations: 32.0s
ival-mult!: 9.8s (30.6% of total)
ival-exp: 3.2s (9.9% of total)
ival-add!: 2.5s (7.9% of total)
ival-hypot: 2.0s (6.2% of total)
ival-div!: 2.0s (6.1% of total)
adjust: 1.7s (5.3% of total)
ival-log: 1.6s (4.9% of total)
ival-asin: 1.3s (4.2% of total)
ival-cos: 1.3s (4% of total)
ival-sub!: 1.2s (3.9% of total)
ival-sin: 1.2s (3.8% of total)
ival-atan2: 888.0ms (2.8% of total)
ival-sqrt: 827.0ms (2.6% of total)
ival-sinu: 512.0ms (1.6% of total)
ival-pow: 415.0ms (1.3% of total)
ival-asinh: 402.0ms (1.3% of total)
ival-fabs: 329.0ms (1% of total)
ival-acosh: 295.0ms (0.9% of total)
ival-neg: 252.0ms (0.8% of total)
ival-atanh: 175.0ms (0.5% of total)
ival-cosu: 115.0ms (0.4% of total)
const: 0.0ms (0% of total)
ival-pi: 0.0ms (0% of total)
Bogosity

rewrite40.2s (23.4%)

Memory
214.9MiB live, 43 393.8MiB allocated; 14.4s collecting garbage
Stop Event
459×iter-limit
175×node-limit
15×unsound
4×saturated
Counts
28 248 → 60 395

derivations12.7s (7.4%)

Memory
-335.7MiB live, 12 327.8MiB allocated; 3.0s collecting garbage
Stop Event
36×fuel
21×done
Compiler

Compiled 7 998 to 3 985 computations (50.2% saved)

series11.8s (6.9%)

Memory
461.5MiB live, 16 776.8MiB allocated; 4.4s collecting garbage
Counts
5 175 → 23 073
Calls

1188 calls:

TimeVariablePointExpression
580.0ms
x
@0
((* (* x x) x) (* x x) x)
572.0ms
base
@inf
((/ (/ (* (log base) (atan2 im re)) (log base)) (log base)) (/ (* (log base) (atan2 im re)) (log base)) (* (log base) (atan2 im re)) (log base) base (atan2 im re) im re (/ (- (* (atan2 im re) (log base)) (* (log (sqrt (+ (* re re) (* im im)))) 0)) (+ (* (log base) (log base)) (* 0 0))) (* (/ (atan2 im re) 1) (/ 1 (log base))) (/ (atan2 im re) 1) 1 (/ 1 (log base)) (/ (- (* (log base) (atan2 im re)) 0) (exp (* (log (log base)) 2))) (- (* (log base) (atan2 im re)) 0) 0 (exp (* (log (log base)) 2)) (* (log (log base)) 2) (log (log base)) 2 (/ (- (* (exp (log (log base))) (atan2 im re)) 0) (* (log base) (log base))) (- (* (exp (log (log base))) (atan2 im re)) 0) (* (exp (log (log base))) (atan2 im re)) (exp (log (log base))) (* (log base) (log base)) (* (* (log base) (/ (atan2 im re) (pow (log base) 4))) (* (log base) (log base))) (* (log base) (/ (atan2 im re) (pow (log base) 4))) (/ (atan2 im re) (pow (log base) 4)) (pow (log base) 4) 4)
129.0ms
y.im
@0
((* (exp (- (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.re) (* (atan2 x.im x.re) y.im))) (sin (+ (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.im) (* (atan2 x.im x.re) y.re)))) (exp (- (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.re) (* (atan2 x.im x.re) y.im))) (- (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.re) (* (atan2 x.im x.re) y.im)) (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.re) (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) (sqrt (+ (* x.re x.re) (* x.im x.im))) (+ (* x.re x.re) (* x.im x.im)) (* x.re x.re) x.re (* x.im x.im) x.im y.re (* (atan2 x.im x.re) y.im) (atan2 x.im x.re) y.im (sin (+ (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.im) (* (atan2 x.im x.re) y.re))) (+ (sin (* y.re (atan2 x.im x.re))) (* y.im (* (cos (* y.re (atan2 x.im x.re))) (log (sqrt (+ (* x.im x.im) (* x.re x.re))))))) (sin (* y.re (atan2 x.im x.re))) (* y.re (atan2 x.im x.re)) (* y.im (* (cos (* y.re (atan2 x.im x.re))) (log (sqrt (+ (* x.im x.im) (* x.re x.re)))))) (* (cos (* y.re (atan2 x.im x.re))) (log (sqrt (+ (* x.im x.im) (* x.re x.re))))) (cos (* y.re (atan2 x.im x.re))) (log (sqrt (+ (* x.im x.im) (* x.re x.re)))) (sqrt (+ (* x.im x.im) (* x.re x.re))) (+ (* x.im x.im) (* x.re x.re)) (* (exp (- (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.re) (* (atan2 x.im x.re) y.im))) (sin (+ (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.im) (* (atan2 x.im x.re) y.re)))) (* (sin (* y.re (atan2 x.im x.re))) (pow (sqrt (+ (* x.im x.im) (* x.re x.re))) y.re)) (* (exp (- (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.re) (* (atan2 x.im x.re) y.im))) (sin (+ (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.im) (* (atan2 x.im x.re) y.re)))) (* (exp (- (* y.re (log x.re)) (* y.im (atan2 x.im x.re)))) (sin (+ (* y.im (log x.re)) (* y.re (atan2 x.im x.re))))) (* (exp (neg (* y.im (atan2 x.im x.re)))) (sin (* y.im (log x.re)))) (exp (neg (* y.im (atan2 x.im x.re)))) (neg (* y.im (atan2 x.im x.re))) (* y.im (atan2 x.im x.re)) (sin (* y.im (log x.re))) (* y.im (log x.re)) (log x.re) (* (exp (- (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.re) (* (atan2 x.im x.re) y.im))) (sin (+ (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.im) (* (atan2 x.im x.re) y.re)))) (exp (- (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.re) (* (atan2 x.im x.re) y.im))) (pow (sqrt (+ (* x.im x.im) (* x.re x.re))) y.re) (sin (+ (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.im) (* (atan2 x.im x.re) y.re))) (+ (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.im) (* (atan2 x.im x.re) y.re)) (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.im) (* (atan2 x.im x.re) y.re) (* (exp (- (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.re) (* (atan2 x.im x.re) y.im))) (sin (+ (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.im) (* (atan2 x.im x.re) y.re)))) (* (exp (- (* -1 (* y.re (log (/ -1 x.re)))) (* y.im (atan2 x.im x.re)))) (sin (+ (* -1 (* y.im (log (/ -1 x.re)))) (* y.re (atan2 x.im x.re))))) (exp (- (* -1 (* y.re (log (/ -1 x.re)))) (* y.im (atan2 x.im x.re)))) (- (* -1 (* y.re (log (/ -1 x.re)))) (* y.im (atan2 x.im x.re))) (* -1 (* y.re (log (/ -1 x.re)))) -1 (* y.re (log (/ -1 x.re))) (log (/ -1 x.re)) (/ -1 x.re) (sin (+ (* -1 (* y.im (log (/ -1 x.re)))) (* y.re (atan2 x.im x.re)))) (+ (* -1 (* y.im (log (/ -1 x.re)))) (* y.re (atan2 x.im x.re))) (* y.im (log (/ -1 x.re))))
119.0ms
base
@-inf
((/ (+ (* (log (sqrt (+ (* re re) (* im im)))) (log base)) (* (atan2 im re) 0)) (+ (* (log base) (log base)) (* 0 0))) (+ (* (log (sqrt (+ (* re re) (* im im)))) (log base)) (* (atan2 im re) 0)) (* (log (sqrt (+ (* re re) (* im im)))) (log base)) (log (sqrt (+ (* re re) (* im im)))) (sqrt (+ (* re re) (* im im))) re im (log base) base (* (atan2 im re) 0) (atan2 im re) 0 (+ (* (log base) (log base)) (* 0 0)) (* (log base) (log base)) (* 0 0) (/ (+ (* (log (sqrt (+ (* re re) (* im im)))) (log base)) (* (atan2 im re) 0)) (+ (* (log base) (log base)) (* 0 0))) (/ (log im) (log base)) (log im) (/ (+ (* (log (sqrt (+ (* re re) (* im im)))) (log base)) (* (atan2 im re) 0)) (+ (* (log base) (log base)) (* 0 0))) (+ (* (log (sqrt (+ (* re re) (* im im)))) (log base)) (* (atan2 im re) 0)) (* (log im) (log base)) (/ (+ (* (log (sqrt (+ (* re re) (* im im)))) (log base)) (* (atan2 im re) 0)) (+ (* (log base) (log base)) (* 0 0))) (+ (* (log (sqrt (+ (* re re) (* im im)))) (log base)) (* (atan2 im re) 0)) (+ (* (/ (* (* im im) (log base)) (* re re)) 1/2) (* (log re) (log base))) (/ (* (* im im) (log base)) (* re re)) (* (* im im) (log base)) (* im im) (* re re) 1/2 (* (log re) (log base)) (log re) (/ (+ (* (log (sqrt (+ (* re re) (* im im)))) (log base)) (* (atan2 im re) 0)) (+ (* (log base) (exp (* (log (log base)) 1))) (* 0 0))) (+ (* (log (sqrt (+ (* re re) (* im im)))) (log base)) (* (atan2 im re) 0)) (* (log (sqrt (+ (* re re) (* im im)))) (log base)) (log (sqrt (+ (* re re) (* im im)))) (sqrt (+ (* re re) (* im im))) (+ (* re re) (* im im)) (+ (* (log base) (exp (* (log (log base)) 1))) (* 0 0)) (* (log base) (exp (* (log (log base)) 1))) (exp (* (log (log base)) 1)) (* (log (log base)) 1) (log (log base)) 1)
108.0ms
y.re
@0
((* (exp (- (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.re) (* (atan2 x.im x.re) y.im))) (sin (+ (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.im) (* (atan2 x.im x.re) y.re)))) (exp (- (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.re) (* (atan2 x.im x.re) y.im))) (- (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.re) (* (atan2 x.im x.re) y.im)) (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.re) (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) (sqrt (+ (* x.re x.re) (* x.im x.im))) (+ (* x.re x.re) (* x.im x.im)) (* x.re x.re) x.re (* x.im x.im) x.im y.re (* (atan2 x.im x.re) y.im) (atan2 x.im x.re) y.im (sin (+ (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.im) (* (atan2 x.im x.re) y.re))) (+ (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.im) (* (atan2 x.im x.re) y.re)) (* (log (sqrt (+ (* x.re x.re) (* x.im x.im)))) y.im) (* (atan2 x.im x.re) y.re))

regimes10.9s (6.3%)

Memory
-109.8MiB live, 13 965.5MiB allocated; 4.9s collecting garbage
Counts
6 445 → 790
Calls

132 calls:

1.5s
x
1.1s
(sqrt.f64 (/.f64 (-.f64 #s(literal 1 binary64) x) #s(literal 2 binary64)))
546.0ms
im
381.0ms
re
365.0ms
x.im
Compiler

Compiled 10 654 to 8 760 computations (17.8% saved)

eval10.1s (5.9%)

Memory
342.7MiB live, 16 754.8MiB allocated; 3.2s collecting garbage
Compiler

Compiled 1 124 227 to 338 384 computations (69.9% saved)

preprocess8.7s (5%)

Memory
-123.8MiB live, 11 358.8MiB allocated; 3.4s collecting garbage
Stop Event
33×node-limit
24×saturated
Compiler

Compiled 41 693 to 28 160 computations (32.5% saved)

prune5.4s (3.1%)

Memory
-304.4MiB live, 8 473.3MiB allocated; 2.1s collecting garbage
Counts
69 531 → 2 821
Compiler

Compiled 174 390 to 122 868 computations (29.5% saved)

bsearch4.5s (2.6%)

Memory
-66.0MiB live, 5 840.9MiB allocated; 1.0s collecting garbage
Algorithm
254×binary-search
155×left-value
Stop Event
245×narrow-enough
9×predicate-same
Samples
1.6s16 583×0valid
917.0ms2 378×1valid
179.0ms340×2valid
60.0ms107×3valid
Compiler

Compiled 132 231 to 107 607 computations (18.6% saved)

Precisions
Click to see histograms. Total time spent on operations: 2.0s
ival-mult!: 512.0ms (26% of total)
ival-hypot: 313.0ms (15.9% of total)
ival-sin: 205.0ms (10.4% of total)
ival-log: 185.0ms (9.4% of total)
ival-atan2: 162.0ms (8.2% of total)
ival-exp: 136.0ms (6.9% of total)
adjust: 102.0ms (5.2% of total)
ival-add!: 85.0ms (4.3% of total)
ival-div!: 70.0ms (3.6% of total)
ival-sub!: 68.0ms (3.4% of total)
ival-cos: 67.0ms (3.4% of total)
ival-asin: 31.0ms (1.6% of total)
ival-sqrt: 21.0ms (1.1% of total)
ival-neg: 6.0ms (0.3% of total)
ival-fabs: 5.0ms (0.3% of total)
ival-copysign: 3.0ms (0.2% of total)
ival-pi: 0.0ms (0% of total)

analyze3.1s (1.8%)

Memory
-274.3MiB live, 3 471.4MiB allocated; 1.8s collecting garbage
Algorithm
58×search
Search
ProbabilityValidUnknownPreconditionInfiniteDomainCan'tIter
0%0%86.3%13.7%0%0%0%0
55.4%47.8%38.5%13.7%0%0%0%1
65.9%55.7%28.9%13.7%0%1.7%0%2
71.2%58.4%23.6%13.7%0%4.3%0%3
77.4%62%18.1%13.7%0%6.2%0%4
83.5%66.8%13.2%13.7%0%6.3%0%5
85.8%68.3%11.3%13.7%0%6.6%0%6
88.3%70.3%9.4%13.7%0%6.6%0%7
89.9%71.5%8%13.7%0%6.8%0%8
91.1%72.5%7.1%13.7%0%6.8%0%9
92.6%73.6%5.9%13.7%0%6.8%0%10
94%74.7%4.8%13.7%0%6.8%0%11
94.5%75.1%4.4%13.7%0%6.9%0%12
Compiler

Compiled 1 498 to 816 computations (45.5% saved)

start3.0ms (0%)

Memory
7.1MiB live, 7.0MiB allocated; 0ms collecting garbage

end0.0ms (0%)

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

Profiling

Loading profile data...