Herbie run

Date:Wednesday, January 15th, 2025
Commit:d270acbc on main
Seed:2025015
Parameters:256 points for 4 iterations
Flags:
localize:costslocalize:errorsreduce:regimesreduce:binary-searchreduce:branch-expressionssetup:simplifysetup:searchrules:arithmeticrules:polynomialsrules:fractionsrules:exponentsrules:trigonometryrules:hyperbolicrules:numericsrules:specialrules:boolsrules:branchesgenerate:rrgenerate:taylorgenerate:simplifygenerate:proofs
default
Memory:363 555.3 MB

Time bar (total: 5.5min)

sample1.7min (30.7%)

Memory
235.8MiB live, 112 485.5MiB allocated; 41.2s collecting garbage
Samples
53.1s434 119×0valid
10.4s26 282×1valid
4.8s9 279×2valid
2.4s4 370×0invalid
1.4s8 675×0exit
377.0ms937×3valid
Precisions
Click to see histograms. Total time spent on operations: 53.4s
ival-mult: 14.3s (26.8% of total)
ival-add: 5.3s (9.9% of total)
ival-div: 4.8s (9% of total)
const: 4.2s (7.9% of total)
ival-sub: 3.9s (7.2% of total)
ival-exp: 3.6s (6.6% of total)
ival-hypot: 2.9s (5.5% of total)
adjust: 2.2s (4.2% of total)
ival-log: 1.8s (3.4% of total)
ival-sin: 1.4s (2.7% of total)
ival-asin: 1.2s (2.3% of total)
ival-cos: 945.0ms (1.8% of total)
ival-atan2: 900.0ms (1.7% of total)
ival-sqrt: 891.0ms (1.7% of total)
ival-<=: 573.0ms (1.1% of total)
ival-asinh: 453.0ms (0.8% of total)
ival->: 447.0ms (0.8% of total)
ival-acosh: 446.0ms (0.8% of total)
ival-sinu: 414.0ms (0.8% of total)
ival-pow: 413.0ms (0.8% of total)
exact: 355.0ms (0.7% of total)
ival-pi: 343.0ms (0.6% of total)
ival-neg: 260.0ms (0.5% of total)
ival-fabs: 259.0ms (0.5% of total)
ival-true: 256.0ms (0.5% of total)
ival->=: 225.0ms (0.4% of total)
ival-assert: 198.0ms (0.4% of total)
ival-atanh: 173.0ms (0.3% of total)
ival-cosu: 92.0ms (0.2% of total)
ival-and: 82.0ms (0.2% of total)
Bogosity

simplify1.2min (21.9%)

Memory
1 362.1MiB live, 73 280.6MiB allocated; 16.3s collecting garbage
Stop Event
624×iter limit
396×node limit
71×saturated
Counts
14 569 → 14 406

localize32.6s (9.9%)

Memory
308.2MiB live, 39 325.0MiB allocated; 7.9s collecting garbage
Samples
12.1s42 264×0valid
6.1s4 914×1valid
3.9s2 037×2valid
1.2s2 363×0invalid
926.0ms105×5exit
375.0ms678×0exit
156.0ms92×3valid
49.0ms27×4valid
Compiler

Compiled 65 817 to 6 272 computations (90.5% saved)

Precisions
Click to see histograms. Total time spent on operations: 18.4s
ival-mult: 4.5s (24.2% of total)
adjust: 2.2s (11.7% of total)
ival-add: 2.1s (11.6% of total)
ival-div: 1.6s (8.8% of total)
const: 1.5s (8.3% of total)
ival-hypot: 997.0ms (5.4% of total)
ival-sub: 925.0ms (5% of total)
ival-pow: 884.0ms (4.8% of total)
ival-exp: 614.0ms (3.3% of total)
ival-log: 611.0ms (3.3% of total)
ival-sqrt: 329.0ms (1.8% of total)
ival-sin: 321.0ms (1.7% of total)
ival-cos: 280.0ms (1.5% of total)
ival-pow2: 261.0ms (1.4% of total)
ival-atan2: 258.0ms (1.4% of total)
ival-asin: 196.0ms (1.1% of total)
ival-acos: 176.0ms (1% of total)
ival-neg: 145.0ms (0.8% of total)
ival-fabs: 110.0ms (0.6% of total)
exact: 88.0ms (0.5% of total)
ival-pi: 88.0ms (0.5% of total)
ival-log1p: 51.0ms (0.3% of total)
ival-true: 40.0ms (0.2% of total)
ival-cosh: 35.0ms (0.2% of total)
ival-copysign: 27.0ms (0.1% of total)
ival-assert: 21.0ms (0.1% of total)
ival-sinh: 14.0ms (0.1% of total)
ival-sinu: 14.0ms (0.1% of total)
ival-cosu: 11.0ms (0.1% of total)
ival-acosh: 7.0ms (0% of total)
ival-asinh: 5.0ms (0% of total)
ival-cbrt: 4.0ms (0% of total)

rewrite25.2s (7.7%)

Memory
-127.8MiB live, 25 170.9MiB allocated; 6.8s collecting garbage
Stop Event
630×iter limit
156×node limit
46×unsound
saturated
Counts
2 790 → 45 853

derivations17.8s (5.4%)

Memory
-361.8MiB live, 14 048.8MiB allocated; 2.8s collecting garbage
Stop Event
35×fuel
22×done
Compiler

Compiled 32 688 to 4 240 computations (87% saved)

explain14.5s (4.4%)

Memory
22.9MiB live, 19 251.7MiB allocated; 4.2s collecting garbage
Explanations
Click to see full explanations table
OperatorSubexpressionExplanationCount
sqrt.f64#foflow-rescue11780
-.f64#fcancellation7982
/.f64#fo/o6540
/.f64#fo/n2040
+.f64#fcancellation1900
sin.f64#fsensitivity1860
cos.f64(cos.f64 (+.f64 (*.f64 (log.f64 (sqrt.f64 (+.f64 (*.f64 x.re x.re) (*.f64 x.im x.im)))) y.im) (*.f64 (atan2.f64 x.im x.re) y.re)))sensitivity1850
sqrt.f32#foflow-rescue1810
log.f64(log.f64 (+.f64 (fabs.f64 x) (sqrt.f64 (+.f64 (*.f64 x x) #s(literal 1 binary64)))))sensitivity1390
sqrt.f64#fuflow-rescue1220
log.f32(log.f32 (+.f32 (fabs.f32 x) (sqrt.f32 (+.f32 (*.f32 x x) #s(literal 1 binary32)))))sensitivity1111
/.f64#fn/o920
-.f64#fnan-rescue890
/.f64#fu/u720
*.f64#fn*u610
/.f64#fu/n450
+.f64#fnan-rescue390
*.f64#fn*o370
/.f64#fn/u50
exp.f64(exp.f64 (*.f64 (fabs.f64 x) (fabs.f64 x)))sensitivity20
cos.f64(cos.f64 (+.f64 (*.f64 (log.f64 (sqrt.f64 (+.f64 (*.f64 x.re x.re) (*.f64 x.im x.im)))) y.im) (*.f64 (atan2.f64 x.im x.re) y.re)))oflow-rescue10
(+.f64 (*.f64 (log.f64 (sqrt.f64 (+.f64 (*.f64 x.re x.re) (*.f64 x.im x.im)))) y.im) (*.f64 (atan2.f64 x.im x.re) y.re))overflow1
(*.f64 x.re x.re)overflow76
(+.f64 (*.f64 x.re x.re) (*.f64 x.im x.im))overflow117
(*.f64 (log.f64 (sqrt.f64 (+.f64 (*.f64 x.re x.re) (*.f64 x.im x.im)))) y.im)overflow1
(*.f64 x.im x.im)overflow62
log.f32(log.f32 (+.f32 x (sqrt.f32 (-.f32 (*.f32 x x) #s(literal 1 binary32)))))oflow-rescue10
(+.f32 x (sqrt.f32 (-.f32 (*.f32 x x) #s(literal 1 binary32))))overflow1
(*.f32 x x)overflow115
(-.f32 (*.f32 x x) #s(literal 1 binary32))overflow115
sin.f64(sin.f64 (+.f64 (*.f64 (log.f64 (sqrt.f64 (+.f64 (*.f64 x.re x.re) (*.f64 x.im x.im)))) y.im) (*.f64 (atan2.f64 x.im x.re) y.re)))oflow-rescue10
(+.f64 (*.f64 (log.f64 (sqrt.f64 (+.f64 (*.f64 x.re x.re) (*.f64 x.im x.im)))) y.im) (*.f64 (atan2.f64 x.im x.re) y.re))overflow1
(*.f64 x.re x.re)overflow76
(+.f64 (*.f64 x.re x.re) (*.f64 x.im x.im))overflow117
(*.f64 (log.f64 (sqrt.f64 (+.f64 (*.f64 x.re x.re) (*.f64 x.im x.im)))) y.im)overflow1
(*.f64 x.im x.im)overflow62
*.f64(*.f64 (*.f64 (sqrt.f64 (*.f64 (PI.f64) #s(literal 2 binary64))) (pow.f64 (+.f64 (+.f64 (-.f64 (-.f64 #s(literal 1 binary64) z) #s(literal 1 binary64)) #s(literal 7 binary64)) #s(literal 1/2 binary64)) (+.f64 (-.f64 (-.f64 #s(literal 1 binary64) z) #s(literal 1 binary64)) #s(literal 1/2 binary64)))) (exp.f64 (neg.f64 (+.f64 (+.f64 (-.f64 (-.f64 #s(literal 1 binary64) z) #s(literal 1 binary64)) #s(literal 7 binary64)) #s(literal 1/2 binary64)))))o*u10
(*.f64 (sqrt.f64 (*.f64 (PI.f64) #s(literal 2 binary64))) (pow.f64 (+.f64 (+.f64 (-.f64 (-.f64 #s(literal 1 binary64) z) #s(literal 1 binary64)) #s(literal 7 binary64)) #s(literal 1/2 binary64)) (+.f64 (-.f64 (-.f64 #s(literal 1 binary64) z) #s(literal 1 binary64)) #s(literal 1/2 binary64))))overflow1
(pow.f64 (+.f64 (+.f64 (-.f64 (-.f64 #s(literal 1 binary64) z) #s(literal 1 binary64)) #s(literal 7 binary64)) #s(literal 1/2 binary64)) (+.f64 (-.f64 (-.f64 #s(literal 1 binary64) z) #s(literal 1 binary64)) #s(literal 1/2 binary64)))overflow1
(exp.f64 (neg.f64 (+.f64 (+.f64 (-.f64 (-.f64 #s(literal 1 binary64) z) #s(literal 1 binary64)) #s(literal 7 binary64)) #s(literal 1/2 binary64))))underflow1
Confusion
Predicted +Predicted -
+361629
-20610741
Precision
0.946101517530089
Recall
0.9920438957475994
Confusion?
Predicted +Predicted MaybePredicted -
+3616029
-206310738
Precision?
0.945359477124183
Recall?
0.9920438957475994
Freqs
test
numberfreq
010770
13252
2568
32
Total Confusion?
Predicted +Predicted MaybePredicted -
+3800
-0019
Precision?
1.0
Recall?
1.0
Samples
3.4s25 348×0valid
1.5s2 770×1valid
768.0ms1 012×2valid
17.0ms48×3valid
3.0ms5exit
Compiler

Compiled 13 558 to 2 283 computations (83.2% saved)

Precisions
Click to see histograms. Total time spent on operations: 3.6s
ival-mult: 919.0ms (25.7% of total)
adjust: 409.0ms (11.4% of total)
ival-add: 367.0ms (10.3% of total)
ival-exp: 278.0ms (7.8% of total)
ival-log: 265.0ms (7.4% of total)
const: 247.0ms (6.9% of total)
ival-div: 225.0ms (6.3% of total)
ival-sub: 196.0ms (5.5% of total)
ival-hypot: 168.0ms (4.7% of total)
ival-sqrt: 90.0ms (2.5% of total)
ival-cos: 80.0ms (2.2% of total)
ival-asin: 67.0ms (1.9% of total)
ival-sin: 55.0ms (1.5% of total)
ival-atan2: 42.0ms (1.2% of total)
ival-fabs: 32.0ms (0.9% of total)
ival-pow: 27.0ms (0.8% of total)
ival-true: 24.0ms (0.7% of total)
exact: 20.0ms (0.6% of total)
ival-pi: 13.0ms (0.4% of total)
ival-assert: 12.0ms (0.3% of total)
ival-copysign: 12.0ms (0.3% of total)
ival-neg: 12.0ms (0.3% of total)
ival-log1p: 10.0ms (0.3% of total)
ival-sinu: 6.0ms (0.2% of total)
ival-cosu: 5.0ms (0.1% of total)

eval13.5s (4.1%)

Memory
225.7MiB live, 18 786.6MiB allocated; 3.7s collecting garbage
Compiler

Compiled 4 035 518 to 299 826 computations (92.6% saved)

preprocess13.4s (4.1%)

Memory
909.1MiB live, 13 884.3MiB allocated; 2.7s collecting garbage
Stop Event
114×iter limit
72×node limit
42×saturated
Compiler

Compiled 75 048 to 13 949 computations (81.4% saved)

regimes13.0s (4%)

Memory
-311.2MiB live, 15 723.7MiB allocated; 4.7s collecting garbage
Counts
7 755 → 854
Calls

132 calls:

1.2s
beta
967.0ms
re
891.0ms
im
859.0ms
(-.f64 (exp.f64 (neg.f64 im)) (exp.f64 im))
456.0ms
y.re
Compiler

Compiled 12 453 to 9 198 computations (26.1% saved)

series12.1s (3.7%)

Memory
-707.3MiB live, 13 615.0MiB allocated; 4.1s collecting garbage
Counts
2 790 → 14 569
Calls

1272 calls:

TimeVariablePointExpression
507.0ms
re
@-inf
((* (/ (neg (atan2 im re)) (pow (log 1/10) 2)) (log 1/10)) (/ (neg (atan2 im re)) (pow (log 1/10) 2)) (neg (atan2 im re)) (atan2 im re) (log 1/10) (pow (log 1/10) 2))
207.0ms
x
@-inf
((copysign (asinh (fabs x)) x) (asinh (fabs x)) (fabs x) (copysign (log (+ (fabs x) (sqrt (+ (* x x) 1)))) x) (log (+ (fabs x) (sqrt (+ (* x x) 1)))) (log x) (+ (* (/ (fabs x) x) x) x) (copysign (log (+ (fabs x) (sqrt (+ (* x x) 1)))) x) (log (+ (fabs x) (sqrt (+ (* x x) 1)))) (+ (fabs x) (sqrt (+ (* x x) 1))) (copysign (log (+ (fabs x) (sqrt (+ (* x x) 1)))) x) (log (+ (fabs x) (sqrt (+ (* x x) 1)))) (+ (fabs x) (sqrt (+ (* x x) 1))) (copysign (log (+ (fabs x) (sqrt (+ (* x x) 1)))) x) (log (+ (fabs x) (sqrt (+ (* x x) 1)))) (+ (fabs x) (sqrt (+ (* x x) 1))) (* (- (/ (fabs x) x) 1) x) (/ (fabs x) x) (+ (* x x) 1) (sqrt (+ (* x x) 1)))
160.0ms
x
@inf
((copysign (asinh (fabs x)) x) (asinh (fabs x)) (fabs x) (copysign (log (+ (fabs x) (sqrt (+ (* x x) 1)))) x) (log (+ (fabs x) (sqrt (+ (* x x) 1)))) (log x) (+ (* (/ (fabs x) x) x) x) (copysign (log (+ (fabs x) (sqrt (+ (* x x) 1)))) x) (log (+ (fabs x) (sqrt (+ (* x x) 1)))) (+ (fabs x) (sqrt (+ (* x x) 1))) (copysign (log (+ (fabs x) (sqrt (+ (* x x) 1)))) x) (log (+ (fabs x) (sqrt (+ (* x x) 1)))) (+ (fabs x) (sqrt (+ (* x x) 1))) (copysign (log (+ (fabs x) (sqrt (+ (* x x) 1)))) x) (log (+ (fabs x) (sqrt (+ (* x x) 1)))) (+ (fabs x) (sqrt (+ (* x x) 1))) (* (- (/ (fabs x) x) 1) x) (/ (fabs x) x) (+ (* x x) 1) (sqrt (+ (* x x) 1)))
152.0ms
u2
@inf
((+ (* (* (sqrt (* (log u1) -2)) (cos (* u2 (* (PI) 2)))) 1/6) 1/2) (* (sqrt (* (log u1) -2)) (cos (* u2 (* (PI) 2)))) (sqrt (* (log u1) -2)) (* (log u1) -2) (/ 1 6) (+ (* (* (/ 1 6) (pow (* -2 (log u1)) 1/2)) (cos (* (* 2 (PI)) u2))) 1/2) (* (* (/ 1 6) (pow (* -2 (log u1)) 1/2)) (cos (* (* 2 (PI)) u2))) (* (/ 1 6) (pow (* -2 (log u1)) 1/2)) (pow (sqrt (* -2 (log u1))) 2) (+ (* (pow (sqrt (* -2 (log u1))) 2) 1/36) -1/4) (+ (* (* (/ 1 6) (pow (* -2 (log u1)) 1/2)) (cos (* (* 2 (PI)) u2))) 1/2) (/ (+ (* (pow (sqrt (* -2 (log u1))) 2) 1/36) -1/4) (+ (* (sqrt (* -2 (log u1))) 1/6) -1/2)) (+ (* (pow (* (log u1) -2) 1/4) (* (pow (* (log u1) -2) 1/4) 1/6)) 1/2) (+ (* (* (/ 1 6) (pow (* -2 (log u1)) 1/2)) (cos (* (* 2 (PI)) u2))) 1/2) (pow (* (log u1) -2) 1/4) (exp (+ (log (sqrt (* -2 (log u1)))) (log (* (cos (* (* (PI) 2) u2)) 1/6)))) (+ (exp (+ (log (sqrt (* -2 (log u1)))) (log (* (cos (* (* (PI) 2) u2)) 1/6)))) 1/2) (+ (log (sqrt (* -2 (log u1)))) (log (* (cos (* (* (PI) 2) u2)) 1/6))) (log (sqrt (* -2 (log u1)))) (* u2 (* (PI) 2)) (cos (* (* 2 (PI)) u2)) (* (sqrt 2) (sqrt (neg (log u1)))) (sqrt (neg (log u1))) (+ (* (sqrt (* -2 (log u1))) 1/6) -1/2) (* (pow (* (log u1) -2) 1/4) 1/6) (* (* (PI) 2) u2) (sqrt (* -2 (log u1))))
145.0ms
x
@0
((copysign (asinh (fabs x)) x) (asinh (fabs x)) (fabs x) (copysign (log (+ (fabs x) (sqrt (+ (* x x) 1)))) x) (log (+ (fabs x) (sqrt (+ (* x x) 1)))) (log x) (+ (* (/ (fabs x) x) x) x) (copysign (log (+ (fabs x) (sqrt (+ (* x x) 1)))) x) (log (+ (fabs x) (sqrt (+ (* x x) 1)))) (+ (fabs x) (sqrt (+ (* x x) 1))) (copysign (log (+ (fabs x) (sqrt (+ (* x x) 1)))) x) (log (+ (fabs x) (sqrt (+ (* x x) 1)))) (+ (fabs x) (sqrt (+ (* x x) 1))) (copysign (log (+ (fabs x) (sqrt (+ (* x x) 1)))) x) (log (+ (fabs x) (sqrt (+ (* x x) 1)))) (+ (fabs x) (sqrt (+ (* x x) 1))) (* (- (/ (fabs x) x) 1) x) (/ (fabs x) x) (+ (* x x) 1) (sqrt (+ (* x x) 1)))

prune5.7s (1.7%)

Memory
-113.2MiB live, 8 828.3MiB allocated; 2.0s collecting garbage
Counts
70 541 → 2 607
Compiler

Compiled 240 111 to 103 537 computations (56.9% saved)

bsearch4.5s (1.4%)

Memory
84.1MiB live, 5 464.7MiB allocated; 899ms collecting garbage
Algorithm
247×binary-search
186×left-value
Stop Event
238×narrow-enough
predicate-same
Samples
1.9s16 076×0valid
731.0ms1 927×1valid
105.0ms172×2valid
19.0ms49×3valid
Compiler

Compiled 158 429 to 88 539 computations (44.1% saved)

Precisions
Click to see histograms. Total time spent on operations: 2.0s
ival-mult: 616.0ms (30.2% of total)
ival-hypot: 219.0ms (10.7% of total)
ival-add: 201.0ms (9.9% of total)
ival-exp: 187.0ms (9.2% of total)
const: 122.0ms (6% of total)
adjust: 117.0ms (5.7% of total)
ival-log: 109.0ms (5.3% of total)
ival-sin: 103.0ms (5% of total)
ival-sub: 93.0ms (4.6% of total)
ival-cos: 92.0ms (4.5% of total)
ival-div: 61.0ms (3% of total)
ival-atan2: 61.0ms (3% of total)
ival-sqrt: 25.0ms (1.2% of total)
ival-true: 13.0ms (0.6% of total)
ival-assert: 7.0ms (0.3% of total)
exact: 6.0ms (0.3% of total)
ival-neg: 5.0ms (0.2% of total)
ival-fabs: 3.0ms (0.1% of total)
ival-pi: 1.0ms (0% of total)

analyze3.4s (1%)

Memory
140.8MiB live, 3 681.8MiB allocated; 2.1s 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.6MiB live, 7.5MiB allocated; 0ms collecting garbage

end0.0ms (0%)

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

Profiling

Loading profile data...