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:249 794.2 MB

Time bar (total: 4.0min)

sample1.3min (33.4%)

Memory
894.3MiB live, 87 486.6MiB allocated; 27.5s collecting garbage
Samples
34.8s284 797×0valid
14.7s44 265×1valid
8.3s17 251×2valid
562.0ms4 077×0invalid
258.0ms202×5exit
255.0ms439×3valid
121.0ms933×0exit
Precisions
Click to see histograms. Total time spent on operations: 43.9s
ival-mult: 9.8s (22.4% of total)
ival-add: 5.3s (12.2% of total)
ival-pow: 4.2s (9.7% of total)
ival-div: 4.2s (9.6% of total)
adjust: 4.0s (9.1% of total)
ival-sub: 3.2s (7.3% of total)
const: 3.2s (7.2% of total)
ival-<=: 2.4s (5.4% of total)
ival-sin: 2.2s (5% of total)
ival-cos: 1.4s (3.2% of total)
ival-sqrt: 576.0ms (1.3% of total)
ival-exp: 571.0ms (1.3% of total)
ival-pow2: 550.0ms (1.3% of total)
exact: 426.0ms (1% of total)
ival-neg: 384.0ms (0.9% of total)
ival-and: 376.0ms (0.9% of total)
ival-==: 355.0ms (0.8% of total)
ival-assert: 135.0ms (0.3% of total)
ival-expm1: 134.0ms (0.3% of total)
ival-true: 130.0ms (0.3% of total)
ival-atan: 96.0ms (0.2% of total)
ival-<: 88.0ms (0.2% of total)
ival-log1p: 78.0ms (0.2% of total)
ival-tan: 65.0ms (0.1% of total)
ival-pi: 35.0ms (0.1% of total)
ival-hypot: 26.0ms (0.1% of total)
ival-if: 6.0ms (0% of total)
ival-fabs: 5.0ms (0% of total)
Bogosity

simplify57.5s (24%)

Memory
1 009.8MiB live, 53 932.5MiB allocated; 13.7s collecting garbage
Stop Event
443×iter limit
306×node limit
49×saturated
Counts
9 175 → 9 055

localize21.7s (9%)

Memory
80.0MiB live, 23 714.2MiB allocated; 4.0s collecting garbage
Samples
7.2s29 419×0valid
4.9s5 707×1valid
4.1s3 124×2valid
404.0ms203×3valid
175.0ms33×5exit
92.0ms152×0exit
12.0ms5×4valid
3.0ms13×0invalid
Compiler

Compiled 36 368 to 3 865 computations (89.4% saved)

Precisions
Click to see histograms. Total time spent on operations: 12.1s
ival-mult: 3.2s (26.2% of total)
adjust: 2.3s (19.2% of total)
ival-div: 1.5s (12.5% of total)
ival-add: 1.3s (11.1% of total)
ival-sub: 925.0ms (7.6% of total)
ival-pow: 855.0ms (7% of total)
const: 795.0ms (6.5% of total)
ival-sqrt: 229.0ms (1.9% of total)
ival-sin: 202.0ms (1.7% of total)
ival-cos: 192.0ms (1.6% of total)
ival-neg: 164.0ms (1.4% of total)
ival-pow2: 120.0ms (1% of total)
ival-exp: 112.0ms (0.9% of total)
exact: 53.0ms (0.4% of total)
ival-true: 29.0ms (0.2% of total)
ival-log1p: 24.0ms (0.2% of total)
ival-expm1: 21.0ms (0.2% of total)
ival-assert: 15.0ms (0.1% of total)
ival-log: 13.0ms (0.1% of total)
ival-tan: 7.0ms (0.1% of total)
ival-atan: 4.0ms (0% of total)
ival-pi: 4.0ms (0% of total)

rewrite17.4s (7.3%)

Memory
-612.9MiB live, 15 826.9MiB allocated; 4.0s collecting garbage
Stop Event
451×iter limit
120×node limit
29×unsound
10×saturated
Counts
1 898 → 30 184

derivations12.6s (5.3%)

Memory
-100.5MiB live, 9 378.8MiB allocated; 1.5s collecting garbage
Stop Event
24×fuel
18×done
Compiler

Compiled 27 672 to 2 842 computations (89.7% saved)

preprocess11.1s (4.6%)

Memory
317.2MiB live, 10 838.3MiB allocated; 3.4s collecting garbage
Stop Event
84×iter limit
62×node limit
22×saturated
Compiler

Compiled 60 605 to 8 824 computations (85.4% saved)

explain10.2s (4.3%)

Memory
-6.6MiB live, 13 068.4MiB allocated; 2.0s collecting garbage
Explanations
Click to see full explanations table
OperatorSubexpressionExplanationCount
-.f64#fcancellation13411
+.f64#fcancellation36190
-.f64(-.f64 (*.f64 #s(literal 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 binary64) t) #s(literal 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 binary64))oflow-left2140
sqrt.f64#foflow-rescue1980
/.f64#fo/o1850
log.f64(log.f64 (+.f64 #s(literal 1 binary64) x))sensitivity1700
/.f64#fn/o1470
pow.f64(pow.f64 (+.f64 #s(literal 1 binary64) (/.f64 i n)) n)sensitivity1190
-.f64#fnan-rescue1000
/.f64#fu/n900
/.f64#fn/u590
/.f64#fu/u520
*.f64#fn*u420
/.f64#fo/n380
+.f64#fnan-rescue370
*.f64#fn*o280
pow.f64(pow.f64 (+.f64 #s(literal 1 binary64) (/.f64 i n)) n)oflow-rescue250
↳(pow.f64 (+.f64 #s(literal 1 binary64) (/.f64 i n)) n)overflow36
↳(/.f64 i n)overflow25
↳(+.f64 #s(literal 1 binary64) (/.f64 i n))overflow25
sqrt.f64#fuflow-rescue100
Confusion
Predicted +Predicted -
+3881237
-1186516
Precision
0.970492623155789
Recall
0.9424477901894124
Confusion?
Predicted +Predicted MaybePredicted -
+388117364
-1181746342
Precision?
0.9328117809479981
Recall?
0.9844584749878582
Freqs
test
numberfreq
06753
13559
2388
352
Total Confusion?
Predicted +Predicted MaybePredicted -
+3010
-209
Precision?
0.9393939393939394
Recall?
1.0
Samples
1.7s3 762×1valid
1.5s16 270×0valid
634.0ms1 428×2valid
56.0ms2×4valid
23.0ms42×3valid
Compiler

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

Precisions
Click to see histograms. Total time spent on operations: 2.4s
ival-mult: 544.0ms (22.6% of total)
adjust: 448.0ms (18.6% of total)
ival-add: 403.0ms (16.8% of total)
ival-div: 223.0ms (9.3% of total)
ival-sub: 215.0ms (8.9% of total)
ival-pow: 211.0ms (8.8% of total)
ival-sin: 91.0ms (3.8% of total)
ival-cos: 63.0ms (2.6% of total)
const: 54.0ms (2.2% of total)
ival-exp: 26.0ms (1.1% of total)
ival-sqrt: 24.0ms (1% of total)
ival-pow2: 21.0ms (0.9% of total)
ival-neg: 18.0ms (0.7% of total)
ival-true: 18.0ms (0.7% of total)
exact: 18.0ms (0.7% 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)

eval7.8s (3.3%)

Memory
-3.9MiB live, 9 951.4MiB allocated; 2.4s collecting garbage
Compiler

Compiled 2 013 252 to 171 105 computations (91.5% saved)

regimes6.2s (2.6%)

Memory
127.0MiB live, 7 938.1MiB allocated; 922ms collecting garbage
Counts
5 249 → 580
Calls

96 calls:

565.0ms
x
363.0ms
b
259.0ms
x1
229.0ms
c
217.0ms
a
Compiler

Compiled 9 437 to 6 023 computations (36.2% saved)

analyze4.9s (2.1%)

Memory
-139.8MiB live, 5 154.8MiB allocated; 1.6s collecting garbage
Algorithm
43×search
2×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)

bsearch3.6s (1.5%)

Memory
-84.5MiB live, 3 460.3MiB allocated; 654ms collecting garbage
Algorithm
196×binary-search
84×left-value
Stop Event
179×narrow-enough
16×predicate-same
1×predicate-failed
Samples
1.3s11 044×0valid
515.0ms1 373×1valid
225.0ms1 171×0invalid
148.0ms350×2valid
15.0ms136×0exit
0.0ms1×3valid
Compiler

Compiled 170 045 to 82 947 computations (51.2% saved)

Precisions
Click to see histograms. Total time spent on operations: 1.6s
ival-mult: 401.0ms (25.5% of total)
ival-add: 241.0ms (15.3% of total)
ival-exp: 194.0ms (12.3% of total)
ival-sub: 184.0ms (11.7% of total)
ival-div: 178.0ms (11.3% of total)
ival-pow: 133.0ms (8.5% of total)
adjust: 100.0ms (6.4% of total)
ival-neg: 57.0ms (3.6% of total)
ival-sqrt: 48.0ms (3.1% of total)
ival-true: 10.0ms (0.6% of total)
exact: 10.0ms (0.6% of total)
ival-assert: 5.0ms (0.3% of total)
const: 4.0ms (0.3% of total)
ival-pi: 2.0ms (0.1% of total)
ival-expm1: 2.0ms (0.1% of total)

prune3.6s (1.5%)

Memory
-34.1MiB live, 5 261.0MiB allocated; 736ms collecting garbage
Counts
42 170 → 1 840
Compiler

Compiled 148 568 to 62 346 computations (58% saved)

series2.9s (1.2%)

Memory
-140.2MiB live, 3 772.5MiB allocated; 676ms collecting garbage
Counts
1 898 → 9 175
Calls

888 calls:

TimeVariablePointExpression
51.0ms
c
@-inf
((- (/ b (* -2 a)) (/ (sqrt (+ (* (* -4 c) a) (* b b))) (* 2 a))) (/ b (* -2 a)) (* -2 a) (/ (sqrt (+ (* (* -4 c) a) (* b b))) (* 2 a)) (+ (* (/ b a) -1) (/ c b)) (/ (- (neg b) (sqrt (- (* b b) (* 4 (* a c))))) (* 2 a)) (/ b a) (/ c b) (/ (- (neg b) (sqrt (- (* b b) (* 4 (* a c))))) (* 2 a)) (- (neg b) (sqrt (- (* b b) (* 4 (* a c))))) (neg b) (sqrt (- (* b b) (* 4 (* a c)))) (+ (sqrt (+ (* (* c a) -4) (* b b))) (neg b)) (/ (/ (- (* b b) (+ (* -4 (* c a)) (* b b))) (+ (sqrt (+ (* (* c a) -4) (* b b))) (neg b))) (* 2 a)) (/ (- (* b b) (+ (* -4 (* c a)) (* b b))) (+ (sqrt (+ (* (* c a) -4) (* b b))) (neg b))) (- (* b b) (+ (* -4 (* c a)) (* b b))) (exp (* (log (- (* b b) (* 4 (* a c)))) 1/2)) (/ (- (neg b) (exp (* (log (- (* b b) (* 4 (* a c)))) 1/2))) (* 2 a)) (- (neg b) (exp (* (log (- (* b b) (* 4 (* a c)))) 1/2))) (sqrt (+ (* (* -4 c) a) (* b b))) (+ (* (* -4 c) a) (* b b)) (- (* b b) (* 4 (* a c))) (sqrt (+ (* (* c a) -4) (* b b))) (log (- (* b b) (* 4 (* a c)))) (- (* b b) (* 4 (* a c))))
50.0ms
x
@0
((- (* x x) (- (* x x) eps)) (/ (- (* x x) (- (* x x) eps)) (+ (sqrt (- (* x x) eps)) x)) (* x x) (- (* x x) eps) (- x (sqrt (- (* x x) eps))) (sqrt (- (* x x) eps)) (neg x) (- x (sqrt (- (* x x) eps))) (* (/ 1/2 x) eps) (/ 1/2 x) (- (/ (* x x) (+ (sqrt (- (* x x) eps)) x)) (/ (- (* x x) eps) (+ (sqrt (- (* x x) eps)) x))) (/ (* x x) (+ (sqrt (- (* x x) eps)) x)) (+ (sqrt (- (* x x) eps)) x) (- x (sqrt (- (* x x) eps))) (* (+ (* (+ (* (/ eps (pow x 5)) 1/16) (/ 1/8 (pow x 3))) eps) (/ 1/2 x)) eps) (+ (* (+ (* (/ eps (pow x 5)) 1/16) (/ 1/8 (pow x 3))) eps) (/ 1/2 x)) (+ (* (/ eps (pow x 5)) 1/16) (/ 1/8 (pow x 3))) (/ (- (* x x) eps) (+ (sqrt (- (* x x) eps)) x)) (/ eps (pow x 5)))
47.0ms
x2
@inf
((+ (* (+ (* (* (* 2 x1) (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1))) (- (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1)) 3)) (* (* x1 x1) (- (* 4 (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1))) 6))) (+ (* x1 x1) 1)) (* (* (* 3 x1) x1) (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1)))) (+ (* (* (* 2 x1) (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1))) (- (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1)) 3)) (* (* x1 x1) (- (* 4 (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1))) 6))) (* (* x1 x1) x1) (+ x1 (+ (+ (+ (+ (* (+ (* (* (* 2 x1) (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1))) (- (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1)) 3)) (* (* x1 x1) (- (* 4 (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1))) 6))) (+ (* x1 x1) 1)) (* (* (* 3 x1) x1) (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1)))) (* (* x1 x1) x1)) x1) (* 3 (/ (- (- (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1))))) (- (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1)) 3) (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1)) (/ (- (- (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1)) (+ (+ (* (+ (* (* (* 2 x1) (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1))) (- (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1)) 3)) (* (* x1 x1) (- (* 4 (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1))) 6))) (+ (* x1 x1) 1)) (* (* (* 3 x1) x1) (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1)))) (* (* x1 x1) x1)))
46.0ms
t
@inf
((/ (+ (* 4 (* (/ t (- t -1)) (/ t (- t -1)))) 1) (+ (* (/ t (- t -1)) (* 4 (/ t (- t -1)))) 2)) (+ (* 4 (* (/ t (- t -1)) (/ t (- t -1)))) 1) (* (/ t (- t -1)) (/ t (- t -1))) (/ t (- t -1)) (/ (+ (* 4 (* (/ t (- t -1)) (/ t (- t -1)))) 1) (+ 2 (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t))))) (- 5/6 (/ 2/9 t)) (/ 2/9 t) (/ (+ (* 4 (* (/ t (- t -1)) (/ t (- t -1)))) 1) (+ 2 (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t))))) (- 5/6 (/ (- 2/9 (/ 1/27 t)) t)) (/ (- 2/9 (/ 1/27 t)) t) (- 2/9 (/ 1/27 t)) (/ (+ 1 (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t)))) (+ 2 (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t))))) (+ 1 (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t)))) (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t))) (* (* (+ (* (+ (* (+ (* -16 t) 12) t) -8) t) 4) t) t) (+ 1 (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t)))) (/ (+ 1 (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t)))) (+ 2 (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t))))) (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t))) (/ (* 2 t) (+ 1 t)) (/ 1/27 t) (+ 2 (* (/ (* 2 t) (+ 1 t)) (/ (* 2 t) (+ 1 t)))) (+ (* (+ (* 12 t) -8) t) 4) (+ (* (+ (* (+ (* 12 t) -8) t) 4) (* t t)) 2))
42.0ms
eps
@inf
((neg (* (- 1 eps) x)) (/ (- (* (+ 1 (/ 1 eps)) (exp (neg (* (- 1 eps) x)))) (* (- (/ 1 eps) 1) (exp (neg (* (+ 1 eps) x))))) 2) (- (* (+ 1 (/ 1 eps)) (exp (neg (* (- 1 eps) x)))) (* (- (/ 1 eps) 1) (exp (neg (* (+ 1 eps) x))))) (* (+ 1 (/ 1 eps)) (exp (neg (* (- 1 eps) x)))) (/ (- (* (+ 1 (/ 1 eps)) (exp (neg (* (- 1 eps) x)))) (* (- (/ 1 eps) 1) (exp (neg (* (+ 1 eps) x))))) 2) (+ (* (/ 1 eps) x) x) (/ (- (* (+ 1 (/ 1 eps)) (exp (neg (* (- 1 eps) x)))) (* (- (/ 1 eps) 1) (exp (neg (* (+ 1 eps) x))))) 2) (- (* (+ 1 (/ 1 eps)) (exp (neg (* (- 1 eps) x)))) (* (- (/ 1 eps) 1) (exp (neg (* (+ 1 eps) x))))) (* (+ 1 (/ 1 eps)) (exp (neg (* (- 1 eps) x)))) (/ (- (* (+ 1 (/ 1 eps)) (exp (neg (* (- 1 eps) x)))) (* (- (/ 1 eps) 1) (exp (neg (* (+ 1 eps) x))))) 2) (- (* (+ 1 (/ 1 eps)) (exp (neg (* (- 1 eps) x)))) (* (- (/ 1 eps) 1) (exp (neg (* (+ 1 eps) x))))) (* (+ 1 (/ 1 eps)) (exp (neg (* (- 1 eps) x)))) (/ (exp (neg x)) eps) (/ (- (* (+ 1 (/ 1 eps)) (exp (neg (* (- 1 eps) x)))) (* (- (/ 1 eps) 1) (exp (neg (* (+ 1 eps) x))))) 2) (- (* (+ 1 (/ 1 eps)) (exp (neg (* (- 1 eps) x)))) (* (- (/ 1 eps) 1) (exp (neg (* (+ 1 eps) x))))) (* (- (/ 1 eps) 1) (exp (neg (* (+ 1 eps) x)))) (* (- 1 eps) x) (* (- (/ 1 eps) 1) (exp (neg (* (+ 1 eps) x)))) (/ -1 (exp (+ (* x eps) x))) (* (- (/ 1 eps) 1) (exp (neg (* (+ 1 eps) x)))))

start4.0ms (0%)

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

end0.0ms (0%)

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

Profiling

Loading profile data...