Herbie run

Date:Sunday, January 19th, 2025
Commit:455c599f on main
Seed:2025019
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:211 717.6 MB

Time bar (total: 4.0min)

sample2.1min (52.5%)

Memory
943.7MiB live, 114 323.6MiB allocated; 36.4s collecting garbage
Samples
29.3s43 814×2valid
24.0s145 287×0invalid
23.0s96 695×1valid
17.5s7 198×5exit
8.5s87 291×0valid
3.0s3 362×3valid
290.0ms4 079×0exit
7.0ms6×4valid
Precisions
Click to see histograms. Total time spent on operations: 1.5min
ival-pow: 16.9s (19.1% of total)
ival-tan: 12.4s (14.1% of total)
adjust: 8.7s (9.9% of total)
ival-mult: 5.8s (6.6% of total)
const: 5.4s (6.1% of total)
ival-sub: 4.5s (5.1% of total)
ival-div: 4.2s (4.7% of total)
ival-cos: 3.8s (4.4% of total)
ival-log: 3.5s (3.9% of total)
ival-sin: 3.4s (3.9% of total)
ival-add: 3.4s (3.8% of total)
ival-fabs: 2.6s (2.9% of total)
ival-expm1: 2.4s (2.7% of total)
ival-exp: 2.4s (2.7% of total)
ival-<=: 2.0s (2.2% of total)
ival-<: 1.4s (1.6% of total)
ival-log1p: 1.3s (1.5% of total)
ival-sqrt: 1.2s (1.4% of total)
ival-and: 604.0ms (0.7% of total)
ival-fmin: 440.0ms (0.5% of total)
ival-atan: 403.0ms (0.5% of total)
exact: 338.0ms (0.4% of total)
ival->: 328.0ms (0.4% of total)
ival-neg: 291.0ms (0.3% of total)
ival-cbrt: 257.0ms (0.3% of total)
ival-assert: 151.0ms (0.2% of total)
ival-true: 68.0ms (0.1% of total)
Bogosity

simplify39.1s (16.3%)

Memory
342.4MiB live, 30 793.5MiB allocated; 9.5s collecting garbage
Stop Event
330×iter limit
243×node limit
3×saturated
Counts
11 448 → 11 448

localize22.8s (9.5%)

Memory
588.3MiB live, 21 448.4MiB allocated; 3.5s collecting garbage
Samples
7.9s11 874×1valid
7.8s6 196×2valid
2.3s9 205×0valid
722.0ms456×3valid
487.0ms173×5exit
Compiler

Compiled 22 050 to 3 310 computations (85% saved)

Precisions
Click to see histograms. Total time spent on operations: 15.7s
adjust: 3.5s (22.3% of total)
ival-mult: 2.2s (13.9% of total)
ival-tan: 1.8s (11.6% of total)
ival-div: 1.8s (11.4% of total)
ival-add: 1.2s (7.5% of total)
ival-pow: 815.0ms (5.2% of total)
ival-sub: 781.0ms (5% of total)
const: 750.0ms (4.8% of total)
ival-cos: 593.0ms (3.8% of total)
ival-log: 554.0ms (3.5% of total)
ival-sin: 399.0ms (2.5% of total)
ival-exp: 290.0ms (1.9% of total)
ival-sqrt: 267.0ms (1.7% of total)
ival-pow2: 179.0ms (1.1% of total)
ival-neg: 158.0ms (1% of total)
ival-log1p: 121.0ms (0.8% of total)
ival-expm1: 75.0ms (0.5% of total)
ival-cbrt: 62.0ms (0.4% of total)
exact: 44.0ms (0.3% of total)
ival-pi: 32.0ms (0.2% of total)
ival-atan2: 27.0ms (0.2% of total)
ival-true: 21.0ms (0.1% of total)
ival-atan: 18.0ms (0.1% of total)
ival-assert: 11.0ms (0.1% of total)

rewrite11.6s (4.9%)

Memory
-799.9MiB live, 8 306.3MiB allocated; 4.5s collecting garbage
Stop Event
333×iter limit
89×node limit
20×unsound
Counts
1 655 → 22 574

derivations9.1s (3.8%)

Memory
-12.7MiB live, 4 921.0MiB allocated; 1.1s collecting garbage
Stop Event
25×fuel
3×done
Compiler

Compiled 8 290 to 1 924 computations (76.8% saved)

preprocess6.9s (2.9%)

Memory
349.1MiB live, 6 553.5MiB allocated; 1.1s collecting garbage
Stop Event
56×iter limit
51×node limit
5×saturated
Compiler

Compiled 18 930 to 5 239 computations (72.3% saved)

explain6.0s (2.5%)

Memory
106.9MiB live, 6 281.4MiB allocated; 1.6s collecting garbage
Explanations
Click to see full explanations table
OperatorSubexpressionExplanationCount
-.f64#fcancellation417431
log.f64#fsensitivity7603
/.f64#fu/u4360
sqrt.f64#foflow-rescue3880
+.f64#fcancellation3100
/.f64#fu/n1130
pow.f64(pow.f64 (+.f64 x #s(literal 1 binary64)) (/.f64 #s(literal 1 binary64) n))sensitivity780
sqrt.f64#fuflow-rescue300
/.f64(/.f64 (*.f64 eps (-.f64 (exp.f64 (*.f64 (+.f64 a b) eps)) #s(literal 1 binary64))) (*.f64 (-.f64 (exp.f64 (*.f64 a eps)) #s(literal 1 binary64)) (-.f64 (exp.f64 (*.f64 b eps)) #s(literal 1 binary64))))n/u240
↳(*.f64 b eps)underflow158
↳(-.f64 (exp.f64 (*.f64 a eps)) #s(literal 1 binary64))underflow153
↳(-.f64 (exp.f64 (*.f64 b eps)) #s(literal 1 binary64))underflow158
↳(*.f64 (-.f64 (exp.f64 (*.f64 a eps)) #s(literal 1 binary64)) (-.f64 (exp.f64 (*.f64 b eps)) #s(literal 1 binary64)))underflow236
↳(*.f64 a eps)underflow153
-.f64#fnan-rescue120
/.f64(/.f64 (-.f64 #s(literal 1 binary64) (cos.f64 x)) (*.f64 x x))n/o30
↳(*.f64 x x)overflow61
/.f64(/.f64 (-.f64 (exp.f64 (*.f64 #s(literal 2 binary64) x)) #s(literal 1 binary64)) (-.f64 (exp.f64 x) #s(literal 1 binary64)))o/o20
↳(exp.f64 (*.f64 #s(literal 2 binary64) x))overflow2
↳(-.f64 (exp.f64 (*.f64 #s(literal 2 binary64) x)) #s(literal 1 binary64))overflow2
↳(exp.f64 x)overflow2
↳(-.f64 (exp.f64 x) #s(literal 1 binary64))overflow2
*.f64#fn*u20
Confusion
Predicted +Predicted -
+523017
-1311790
Precision
0.9755642603991792
Recall
0.996760053363827
Confusion?
Predicted +Predicted MaybePredicted -
+5230143
-131181772
Precision?
0.9723715928054886
Recall?
0.9994282447112636
Freqs
test
numberfreq
01807
14574
2648
394
445
Total Confusion?
Predicted +Predicted MaybePredicted -
+2800
-000
Precision?
1.0
Recall?
1.0
Samples
2.0s2 730×2valid
1.2s6 034×1valid
472.0ms5 380×0valid
118.0ms192×3valid
Compiler

Compiled 2 154 to 763 computations (64.6% saved)

Precisions
Click to see histograms. Total time spent on operations: 2.7s
ival-tan: 714.0ms (26.6% of total)
adjust: 413.0ms (15.4% of total)
ival-log: 212.0ms (7.9% of total)
ival-cos: 211.0ms (7.9% of total)
ival-sub: 162.0ms (6% of total)
ival-div: 156.0ms (5.8% of total)
ival-exp: 155.0ms (5.8% of total)
ival-sin: 130.0ms (4.8% of total)
ival-pow: 112.0ms (4.2% of total)
ival-mult: 100.0ms (3.7% of total)
ival-add: 91.0ms (3.4% of total)
ival-sqrt: 61.0ms (2.3% of total)
ival-log1p: 57.0ms (2.1% of total)
ival-atan: 23.0ms (0.9% of total)
ival-expm1: 23.0ms (0.9% of total)
ival-cbrt: 20.0ms (0.7% of total)
ival-neg: 19.0ms (0.7% of total)
ival-true: 11.0ms (0.4% of total)
exact: 8.0ms (0.3% of total)
ival-assert: 6.0ms (0.2% of total)

eval5.1s (2.1%)

Memory
363.9MiB live, 5 943.1MiB allocated; 950ms collecting garbage
Compiler

Compiled 1 349 539 to 149 285 computations (88.9% saved)

series3.4s (1.4%)

Memory
244.2MiB live, 3 518.7MiB allocated; 837ms collecting garbage
Counts
1 655 → 11 448
Calls

507 calls:

TimeVariablePointExpression
105.0ms
n
@0
((- (* (+ n 1) (log (+ n 1))) (* n (log n))) (log (+ n 1)) (- (- (* (+ n 1) (log (+ n 1))) (* n (log n))) 1) (* (+ n 1) (log (+ n 1))) (* n (log n)) (log n))
77.0ms
x
@inf
((- (exp (* x a)) 1) (* x a) (- (exp (* a x)) 1) (exp (* a x)) (- (exp (* a x)) 1) (exp (* a x)) (+ (* x a) 1) (- (exp (* a x)) 1) (* (+ (* (* (* x x) (+ (* (* x a) 1/6) 1/2)) a) x) a) (+ (* (* (* x x) (+ (* (* x a) 1/6) 1/2)) a) x) (* (* x x) (+ (* (* x a) 1/6) 1/2)) (/ (- (exp (* (* x a) 2)) 1) (- (pow (exp x) a) -1)) (- (exp (* (* x a) 2)) 1) (* (* x a) 2) (+ (* (* x a) 1/6) 1/2) (pow (exp x) a) (- (pow (exp x) a) -1))
67.0ms
b
@-inf
((/ (* eps (- (exp (* (+ a b) eps)) 1)) (* (- (exp (* a eps)) 1) (- (exp (* b eps)) 1))) (/ (/ (+ b a) b) a) (/ (+ b a) b) (+ b a) (/ (* eps (- (exp (* (+ a b) eps)) 1)) (* (- (exp (* a eps)) 1) (- (exp (* b eps)) 1))) (/ 1 a) (/ (* eps (- (exp (* (+ a b) eps)) 1)) (* (- (exp (* a eps)) 1) (- (exp (* b eps)) 1))) (/ 1 b) (/ (* (* (+ b a) 1/2) (+ (* (* b a) b) (* (* b a) a))) (* (* (* b a) a) b)) (+ (* (* b a) b) (* (* b a) a)) (- (* (/ 1/2 b) (/ (pow (+ b a) 2) a)) (/ (* (* (+ b a) 1/2) (+ (* (* b a) b) (* (* b a) a))) (* (* (* b a) a) b))) (* (* (+ b a) 1/2) (+ (* (* b a) b) (* (* b a) a))) (/ (+ (* (* eps (- (/ (pow (exp a) eps) (- (exp (* eps a)) 1)) 1/2)) b) 1) b) (/ (* eps (- (exp (* (+ a b) eps)) 1)) (* (- (exp (* a eps)) 1) (- (exp (* b eps)) 1))) (+ (* (* eps (- (/ (pow (exp a) eps) (- (exp (* eps a)) 1)) 1/2)) b) 1) (* eps (- (/ (pow (exp a) eps) (- (exp (* eps a)) 1)) 1/2)) (/ (pow (+ b a) 2) a) (* (/ 1/2 b) (/ (pow (+ b a) 2) a)) (/ (pow (exp a) eps) (- (exp (* eps a)) 1)))
60.0ms
a
@inf
((/ (* eps (- (exp (* (+ a b) eps)) 1)) (* (- (exp (* a eps)) 1) (- (exp (* b eps)) 1))) (/ (/ (+ b a) b) a) (/ (+ b a) b) (+ b a) (/ (* eps (- (exp (* (+ a b) eps)) 1)) (* (- (exp (* a eps)) 1) (- (exp (* b eps)) 1))) (/ 1 a) (/ (* eps (- (exp (* (+ a b) eps)) 1)) (* (- (exp (* a eps)) 1) (- (exp (* b eps)) 1))) (/ 1 b) (/ (* (* (+ b a) 1/2) (+ (* (* b a) b) (* (* b a) a))) (* (* (* b a) a) b)) (+ (* (* b a) b) (* (* b a) a)) (- (* (/ 1/2 b) (/ (pow (+ b a) 2) a)) (/ (* (* (+ b a) 1/2) (+ (* (* b a) b) (* (* b a) a))) (* (* (* b a) a) b))) (* (* (+ b a) 1/2) (+ (* (* b a) b) (* (* b a) a))) (/ (+ (* (* eps (- (/ (pow (exp a) eps) (- (exp (* eps a)) 1)) 1/2)) b) 1) b) (/ (* eps (- (exp (* (+ a b) eps)) 1)) (* (- (exp (* a eps)) 1) (- (exp (* b eps)) 1))) (+ (* (* eps (- (/ (pow (exp a) eps) (- (exp (* eps a)) 1)) 1/2)) b) 1) (* eps (- (/ (pow (exp a) eps) (- (exp (* eps a)) 1)) 1/2)) (/ (pow (+ b a) 2) a) (* (/ 1/2 b) (/ (pow (+ b a) 2) a)) (/ (pow (exp a) eps) (- (exp (* eps a)) 1)))
56.0ms
x
@0
((- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (pow (+ x 1) (/ 1 n)) (+ x 1) (/ 1 n) (pow x (/ 1 n)))

prune2.9s (1.2%)

Memory
-767.5MiB live, 3 405.7MiB allocated; 1.4s collecting garbage
Counts
36 046 → 1 640
Compiler

Compiled 97 047 to 48 331 computations (50.2% saved)

regimes2.8s (1.2%)

Memory
-90.2MiB live, 3 185.5MiB allocated; 496ms collecting garbage
Counts
3 413 → 295
Calls

43 calls:

779.0ms
x
280.0ms
eps
111.0ms
a
93.0ms
(exp.f64 x)
89.0ms
b_2
Compiler

Compiled 2 187 to 2 053 computations (6.1% saved)

analyze2.8s (1.2%)

Memory
-177.2MiB live, 2 130.3MiB allocated; 1.9s collecting garbage
Algorithm
28×search
Search
ProbabilityValidUnknownPreconditionInfiniteDomainCan'tIter
0%0%61.1%38.9%0%0%0%0
7.4%4.5%56.6%38.9%0%0%0%1
22.3%13.6%47.5%38.9%0%0%0%2
40.2%23.5%34.9%38.9%0%2.7%0%3
53.4%31.1%27.2%38.9%0%2.8%0%4
63%36.3%21.3%38.9%0%3.6%0%5
65.9%37.5%19.4%38.9%0%4.2%0%6
70.4%38.8%16.3%38.9%0%6%0%7
73.6%40.2%14.4%38.9%0%6.5%0%8
76.3%40.9%12.7%38.9%0%7.5%0%9
78.4%41.4%11.4%38.9%0%8.3%0%10
81.1%42.4%9.9%38.9%0%8.8%0%11
82.3%42.7%9.2%38.9%0%9.3%0%12
Compiler

Compiled 483 to 337 computations (30.2% saved)

bsearch1.1s (0.5%)

Memory
-15.6MiB live, 904.0MiB allocated; 132ms collecting garbage
Algorithm
70×binary-search
16×left-value
Stop Event
58×narrow-enough
12×predicate-same
Samples
295.0ms4 007×0valid
228.0ms1 207×1valid
119.0ms298×2valid
79.0ms891×0invalid
4.0ms44×0exit
2.0ms8×3valid
Compiler

Compiled 31 883 to 21 213 computations (33.5% saved)

Precisions
Click to see histograms. Total time spent on operations: 537.0ms
ival-pow: 114.0ms (21.2% of total)
ival-mult: 93.0ms (17.3% of total)
ival-sub: 74.0ms (13.8% of total)
ival-div: 59.0ms (11% of total)
adjust: 55.0ms (10.3% of total)
ival-cos: 39.0ms (7.3% of total)
ival-sqrt: 30.0ms (5.6% of total)
ival-add: 27.0ms (5% of total)
ival-neg: 19.0ms (3.5% of total)
ival-cbrt: 12.0ms (2.2% of total)
ival-true: 4.0ms (0.7% of total)
exact: 3.0ms (0.6% of total)
ival-assert: 2.0ms (0.4% of total)
ival-expm1: 2.0ms (0.4% of total)
ival-log1p: 1.0ms (0.2% of total)
ival-log: 1.0ms (0.2% of total)

start1.0ms (0%)

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

end0.0ms (0%)

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

Profiling

Loading profile data...