Herbie run

Date:Sunday, December 29th, 2024
Commit:fbbe2c7d on main
Seed:2024364
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:294 728.0 MB

Time bar (total: 4.7min)

sample1.3min (27.1%)

Memory
1 145.0MiB live, 87 889.8MiB allocated; 28.3s collecting garbage
Samples
32.9s285 022×0valid
14.6s44 079×1valid
8.4s17 246×2valid
486.0ms4 462×0invalid
226.0ms405×3valid
213.0ms202×5exit
157.0ms974×0exit
Precisions
Click to see histograms. Total time spent on operations: 44.3s
ival-mult: 9.2s (20.7% of total)
ival-pow: 5.1s (11.4% of total)
ival-add: 4.8s (10.8% of total)
adjust: 4.2s (9.5% of total)
const: 4.0s (9% of total)
ival-div: 3.8s (8.6% of total)
ival-sub: 3.4s (7.6% of total)
ival-<=: 2.3s (5.3% of total)
ival-sin: 1.9s (4.2% of total)
ival-cos: 1.5s (3.3% of total)
ival-pow2: 939.0ms (2.1% of total)
ival-exp: 511.0ms (1.2% of total)
ival-sqrt: 466.0ms (1.1% of total)
ival-neg: 453.0ms (1% of total)
exact: 453.0ms (1% of total)
ival-and: 375.0ms (0.8% of total)
ival-==: 224.0ms (0.5% of total)
ival-assert: 142.0ms (0.3% of total)
ival-true: 142.0ms (0.3% of total)
ival-pi: 125.0ms (0.3% of total)
ival-tan: 124.0ms (0.3% of total)
ival-log1p: 79.0ms (0.2% of total)
ival-atan: 75.0ms (0.2% of total)
ival-expm1: 72.0ms (0.2% of total)
ival-<: 59.0ms (0.1% of total)
ival-hypot: 24.0ms (0.1% of total)
ival-fabs: 5.0ms (0% of total)
ival-if: 5.0ms (0% of total)
Bogosity

simplify52.3s (18.4%)

Memory
947.4MiB live, 49 878.2MiB allocated; 12.1s collecting garbage
Stop Event
448×iter limit
276×node limit
84×saturated
Counts
10 441 → 10 299

rewrite35.9s (12.6%)

Memory
-225.4MiB live, 36 267.2MiB allocated; 8.5s collecting garbage
Stop Event
305×iter limit
149×node limit
11×saturated
Counts
2 046 → 72 517

derivations33.6s (11.8%)

Memory
-236.2MiB live, 21 568.5MiB allocated; 7.2s collecting garbage
Stop Event
264×iter limit
175×node limit
26×fuel
16×done
saturated
Compiler

Compiled 27 868 to 2 820 computations (89.9% saved)

localize22.5s (7.9%)

Memory
216.8MiB live, 26 197.6MiB allocated; 4.3s collecting garbage
Samples
7.7s30 339×0valid
4.5s2 813×2valid
4.2s5 206×1valid
364.0ms107×3valid
180.0ms449×0invalid
133.0ms225×0exit
131.0ms4valid
62.0ms20×5exit
Compiler

Compiled 37 276 to 4 268 computations (88.6% saved)

Precisions
Click to see histograms. Total time spent on operations: 13.2s
ival-mult: 3.7s (27.9% of total)
adjust: 2.0s (14.9% of total)
ival-div: 1.9s (14% of total)
ival-add: 1.5s (11.3% of total)
ival-sub: 1.3s (10% of total)
ival-pow: 685.0ms (5.2% of total)
const: 482.0ms (3.6% of total)
ival-tan: 469.0ms (3.6% of total)
ival-sin: 256.0ms (1.9% of total)
ival-cos: 234.0ms (1.8% of total)
ival-exp: 156.0ms (1.2% of total)
ival-pow2: 121.0ms (0.9% of total)
ival-sqrt: 115.0ms (0.9% of total)
ival-neg: 114.0ms (0.9% of total)
exact: 59.0ms (0.4% of total)
ival-log: 32.0ms (0.2% of total)
ival-true: 31.0ms (0.2% of total)
ival-cosh: 23.0ms (0.2% of total)
ival-log1p: 23.0ms (0.2% of total)
ival-atan: 20.0ms (0.2% of total)
ival-expm1: 19.0ms (0.1% of total)
ival-pi: 18.0ms (0.1% of total)
ival-assert: 16.0ms (0.1% of total)
ival-hypot: 10.0ms (0.1% of total)
ival-sinh: 8.0ms (0.1% of total)
ival-fabs: 1.0ms (0% of total)

eval18.5s (6.5%)

Memory
103.1MiB live, 21 264.3MiB allocated; 4.4s collecting garbage
Compiler

Compiled 3 890 018 to 314 230 computations (91.9% saved)

explain9.9s (3.5%)

Memory
-63.1MiB live, 12 938.0MiB allocated; 2.1s collecting garbage
Explanations
Click to see full explanations table
OperatorSubexpressionExplanationCount
-.f64#fcancellation12673
+.f64#fcancellation36684
-.f64(-.f64 (*.f64 #s(literal 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 binary64) t) #s(literal 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 binary64))oflow-left2170
sqrt.f64#foflow-rescue1840
/.f64#fo/o1740
/.f64#fn/o1600
log.f64(log.f64 (+.f64 #s(literal 1 binary64) x))sensitivity1581
pow.f64(pow.f64 (+.f64 #s(literal 1 binary64) (/.f64 i n)) n)sensitivity1162
-.f64#fnan-rescue1090
/.f64#fu/n750
+.f64#fnan-rescue550
/.f64#fn/u510
*.f64#fn*u470
/.f64#fu/u410
/.f64#fo/n380
*.f64#fn*o190
pow.f64(pow.f64 (+.f64 #s(literal 1 binary64) (/.f64 i n)) n)oflow-rescue170
(pow.f64 (+.f64 #s(literal 1 binary64) (/.f64 i n)) n)overflow35
(/.f64 i n)overflow17
(+.f64 #s(literal 1 binary64) (/.f64 i n))overflow17
sqrt.f64#fuflow-rescue100
Confusion
Predicted +Predicted -
+3827220
-936612
Precision
0.9762755102040817
Recall
0.945638744749197
Confusion?
Predicted +Predicted MaybePredicted -
+382715565
-931896423
Precision?
0.9338649155722326
Recall?
0.9839387200395354
Freqs
test
numberfreq
06832
13503
2375
342
Total Confusion?
Predicted +Predicted MaybePredicted -
+3010
-209
Precision?
0.9393939393939394
Recall?
1.0
Samples
1.5s16 424×0valid
1.2s3 620×1valid
628.0ms1 442×2valid
12.0ms18×3valid
Compiler

Compiled 7 535 to 1 486 computations (80.3% saved)

Precisions
Click to see histograms. Total time spent on operations: 2.3s
ival-mult: 561.0ms (24.5% of total)
adjust: 399.0ms (17.4% of total)
ival-add: 299.0ms (13.1% of total)
ival-div: 241.0ms (10.5% of total)
ival-pow: 229.0ms (10% of total)
ival-sub: 181.0ms (7.9% of total)
ival-sin: 99.0ms (4.3% of total)
ival-cos: 69.0ms (3% of total)
const: 44.0ms (1.9% of total)
ival-sqrt: 40.0ms (1.7% of total)
ival-exp: 36.0ms (1.6% of total)
exact: 19.0ms (0.8% of total)
ival-true: 18.0ms (0.8% of total)
ival-neg: 15.0ms (0.7% of total)
ival-pow2: 14.0ms (0.6% of total)
ival-assert: 9.0ms (0.4% of total)
ival-atan: 5.0ms (0.2% of total)
ival-log1p: 5.0ms (0.2% of total)
ival-tan: 4.0ms (0.2% of total)
ival-expm1: 3.0ms (0.1% of total)
ival-pi: 2.0ms (0.1% of total)

preprocess9.4s (3.3%)

Memory
94.7MiB live, 8 598.5MiB allocated; 2.3s collecting garbage
Stop Event
82×iter limit
53×saturated
33×node limit
Compiler

Compiled 61 957 to 8 762 computations (85.9% saved)

regimes7.1s (2.5%)

Memory
-32.6MiB live, 8 293.1MiB allocated; 1.1s collecting garbage
Counts
6 069 → 593
Calls

96 calls:

1.1s
x
534.0ms
(*.f64 (cos.f64 x) (exp.f64 (*.f64 #s(literal 10 binary64) (*.f64 x x))))
377.0ms
b
298.0ms
a
283.0ms
c
Compiler

Compiled 8 485 to 5 434 computations (36% saved)

prune5.5s (1.9%)

Memory
48.6MiB live, 8 356.5MiB allocated; 1.1s collecting garbage
Counts
83 456 → 2 094
Compiler

Compiled 163 603 to 67 755 computations (58.6% saved)

analyze4.5s (1.6%)

Memory
-187.1MiB live, 5 095.4MiB allocated; 2.0s collecting garbage
Algorithm
43×search
random
Search
ProbabilityValidUnknownPreconditionInfiniteDomainCan'tIter
0%0%54.5%45.5%0%0%0%0
21.4%11.7%42.9%45.5%0%0%0%1
37.4%20.4%34.1%45.5%0%0%0%2
48.7%26.2%27.7%45.5%0%0.6%0%3
57.7%30.7%22.6%45.5%0%1.2%0%4
71.2%37.7%15.3%45.5%0%1.6%0%5
72.9%38.4%14.3%45.5%0%1.8%0%6
77.9%40.7%11.6%45.5%0%2.2%0%7
81.5%42.6%9.7%45.5%0%2.3%0%8
84.1%43.8%8.3%45.5%0%2.5%0%9
86.2%44.6%7.2%45.5%0%2.7%0%10
88.2%45.6%6.1%45.5%0%2.8%0%11
89.1%45.9%5.6%45.5%0%2.9%0%12
Compiler

Compiled 1 402 to 721 computations (48.6% saved)

series4.1s (1.4%)

Memory
-176.3MiB live, 4 903.1MiB allocated; 1.1s collecting garbage
Counts
2 046 → 10 441
Calls

885 calls:

TimeVariablePointExpression
153.0ms
t
@inf
((- (* 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 t) 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) (* t 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) (- (* 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 t) 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) (* (neg t) (- (* (sqrt 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) (sqrt (/ (/ 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 t) t))) 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000)) (neg t) (- (* (sqrt 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) (sqrt (/ (/ 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 t) t))) 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) (* (sqrt (/ 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 t)) (sqrt (/ 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 t))) (- (* 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 t) 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) (* (neg t) (- (* (sqrt (/ 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 t)) (sqrt (/ 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 t))) 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000)) (sqrt 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) (* (sqrt 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) (sqrt (/ (/ 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 t) t))) (/ 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 t) (- (* (sqrt (/ 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 t)) (sqrt (/ 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 t))) 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000))
84.0ms
i
@inf
((* (/ (* 100 (- (exp (* (log (+ 1 (/ i n))) n)) 1)) i) n) (/ (* 100 (- (exp (* (log (+ 1 (/ i n))) n)) 1)) i) (* 100 (- (exp (* (log (+ 1 (/ i n))) n)) 1)) (- (exp (* (log (+ 1 (/ i n))) n)) 1) (/ (* 0 n) i) (* 0 n) (* 100 (+ (* (/ (pow (+ (/ i n) 1) n) i) n) (* (/ -1 i) n))) (+ (* (/ (pow (+ (/ i n) 1) n) i) n) (* (/ -1 i) n)) (* (/ (- (exp (* (log (+ 1 (/ i n))) n)) 1) i) (* n 100)) (/ (- (exp (* (log (+ 1 (/ i n))) n)) 1) i) (+ (* (- 1/2 (/ 1/2 n)) i) 1) (- 1/2 (/ 1/2 n)) (* (* (- (exp (* (log (+ 1 (/ i n))) n)) 1) (/ 100 i)) n) (* (- (exp (* (log (+ 1 (/ i n))) n)) 1) (/ 100 i)) (+ (* (* 100 (+ (* (- (+ (/ 1/3 (* n n)) 1/6) (/ 1/2 n)) i) (- 1/2 (/ 1/2 n)))) i) 100) (* 100 (+ (* (- (+ (/ 1/3 (* n n)) 1/6) (/ 1/2 n)) i) (- 1/2 (/ 1/2 n)))) (* 100 (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n))) (* (* 100 (* n n)) (/ (- (log i) (log n)) i)) (* 100 (* n n)) (* n n) (log (+ 1 (/ i n))) (* (log (+ 1 (/ i n))) n) (+ (* (- (+ (/ 1/3 (* n n)) 1/6) (/ 1/2 n)) i) (- 1/2 (/ 1/2 n))) (/ 1/3 (* n n)) (- (log i) (log n)))
65.0ms
u
@inf
((/ (/ (* v t1) (- t1 u)) (- u t1)) (/ (* v t1) (- t1 u)) (* v t1) (- t1 u) (* (neg v) (/ t1 (pow (- u t1) 2))) (neg v) (/ t1 (pow (- u t1) 2)) (/ 1 t1) (* (/ v (* (+ t1 u) (+ t1 u))) (neg t1)) (/ v (* (+ t1 u) (+ t1 u))) (* (+ t1 u) (+ t1 u)) (* u u) (/ (* (neg t1) v) (* (+ t1 u) (+ t1 u))) (* t1 (/ (/ (neg v) u) u)) (/ (/ (neg v) u) u) (/ (neg v) u) (* (/ t1 (sqrt (- u t1))) (/ (/ v (- t1 u)) (sqrt (- u t1)))) (/ t1 (sqrt (- u t1))) (sqrt (- u t1)) (- u t1) (neg t1) (/ (/ v (- t1 u)) (sqrt (- u t1))))
51.0ms
t
@inf
((+ (* (+ 1 (* t 1/5000000000000000)) (+ 1 (* t 1/5000000000000000))) (- -1 (* 2 (* t 1/5000000000000000)))) (* (+ 1 (* t 1/5000000000000000)) (+ 1 (* t 1/5000000000000000))) (* 2 (* t 1/5000000000000000)) (+ 1 (* t 1/5000000000000000)) (* t 1/5000000000000000))
50.0ms
i
@0
((* (/ (* 100 (- (exp (* (log (+ 1 (/ i n))) n)) 1)) i) n) (/ (* 100 (- (exp (* (log (+ 1 (/ i n))) n)) 1)) i) (* 100 (- (exp (* (log (+ 1 (/ i n))) n)) 1)) (- (exp (* (log (+ 1 (/ i n))) n)) 1) (/ (* 0 n) i) (* 0 n) (* 100 (+ (* (/ (pow (+ (/ i n) 1) n) i) n) (* (/ -1 i) n))) (+ (* (/ (pow (+ (/ i n) 1) n) i) n) (* (/ -1 i) n)) (* (/ (- (exp (* (log (+ 1 (/ i n))) n)) 1) i) (* n 100)) (/ (- (exp (* (log (+ 1 (/ i n))) n)) 1) i) (+ (* (- 1/2 (/ 1/2 n)) i) 1) (- 1/2 (/ 1/2 n)) (* (* (- (exp (* (log (+ 1 (/ i n))) n)) 1) (/ 100 i)) n) (* (- (exp (* (log (+ 1 (/ i n))) n)) 1) (/ 100 i)) (+ (* (* 100 (+ (* (- (+ (/ 1/3 (* n n)) 1/6) (/ 1/2 n)) i) (- 1/2 (/ 1/2 n)))) i) 100) (* 100 (+ (* (- (+ (/ 1/3 (* n n)) 1/6) (/ 1/2 n)) i) (- 1/2 (/ 1/2 n)))) (* 100 (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n))) (* (* 100 (* n n)) (/ (- (log i) (log n)) i)) (* 100 (* n n)) (* n n) (log (+ 1 (/ i n))) (* (log (+ 1 (/ i n))) n) (+ (* (- (+ (/ 1/3 (* n n)) 1/6) (/ 1/2 n)) i) (- 1/2 (/ 1/2 n))) (/ 1/3 (* n n)) (- (log i) (log n)))

bsearch3.8s (1.3%)

Memory
11.4MiB live, 3 471.0MiB allocated; 555ms collecting garbage
Algorithm
219×binary-search
80×left-value
Stop Event
208×narrow-enough
11×predicate-same
Samples
1.3s10 644×0valid
554.0ms1 535×1valid
297.0ms598×2valid
111.0ms1 243×0invalid
14.0ms23×3valid
3.0ms28×0exit
Compiler

Compiled 132 964 to 78 375 computations (41.1% saved)

Precisions
Click to see histograms. Total time spent on operations: 1.8s
ival-mult: 595.0ms (33.7% of total)
adjust: 219.0ms (12.4% of total)
ival-pow: 196.0ms (11.1% of total)
ival-div: 188.0ms (10.6% of total)
ival-exp: 178.0ms (10.1% of total)
ival-sub: 157.0ms (8.9% of total)
ival-add: 119.0ms (6.7% of total)
ival-neg: 43.0ms (2.4% of total)
ival-sqrt: 23.0ms (1.3% of total)
const: 17.0ms (1% of total)
ival-true: 11.0ms (0.6% of total)
exact: 11.0ms (0.6% of total)
ival-assert: 6.0ms (0.3% of total)
ival-pi: 5.0ms (0.3% of total)
ival-expm1: 2.0ms (0.1% of total)

start2.0ms (0%)

Memory
6.0MiB live, 6.1MiB allocated; 0ms collecting garbage

end0.0ms (0%)

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

Profiling

Loading profile data...