Herbie run

Date:Friday, January 17th, 2025
Commit:0ed7f8bc on no-localize
Seed:2025017
Parameters:256 points for 4 iterations
Flags:
reduce:regimesreduce:binary-searchreduce:branch-expressionssetup:simplifysetup:searchrules:arithmeticrules:polynomialsrules:fractionsrules:exponentsrules:trigonometryrules:hyperbolicrules:numericsrules:specialrules:boolsrules:branchesgenerate:rrgenerate:taylorgenerate:simplifygenerate:proofs
default
Memory:221 722.2 MB

Time bar (total: 3.4min)

sample1.4min (40.4%)

Memory
954.6MiB live, 94 134.7MiB allocated; 31.1s collecting garbage
Samples
34.7s284 954×0valid
16.4s43 990×1valid
8.6s17 392×2valid
531.0ms4 348×0invalid
261.0ms202×5exit
169.0ms416×3valid
125.0ms973×0exit
Precisions
Click to see histograms. Total time spent on operations: 47.1s
ival-mult: 10.3s (21.9% of total)
adjust: 5.5s (11.6% of total)
ival-add: 5.4s (11.5% of total)
ival-pow: 4.9s (10.5% of total)
ival-div: 3.9s (8.3% of total)
const: 3.6s (7.6% of total)
ival-sub: 3.0s (6.5% of total)
ival-<=: 2.8s (5.9% of total)
ival-sin: 2.1s (4.4% of total)
ival-cos: 1.5s (3.1% of total)
ival-exp: 636.0ms (1.4% of total)
ival-sqrt: 532.0ms (1.1% of total)
exact: 453.0ms (1% of total)
ival-and: 390.0ms (0.8% of total)
ival-neg: 374.0ms (0.8% of total)
ival-==: 335.0ms (0.7% of total)
ival-pow2: 270.0ms (0.6% of total)
ival-expm1: 206.0ms (0.4% of total)
ival-<: 193.0ms (0.4% of total)
ival-log1p: 151.0ms (0.3% of total)
ival-assert: 142.0ms (0.3% of total)
ival-true: 140.0ms (0.3% of total)
ival-pi: 121.0ms (0.3% of total)
ival-atan: 112.0ms (0.2% of total)
ival-tan: 54.0ms (0.1% of total)
ival-hypot: 42.0ms (0.1% of total)
ival-fabs: 5.0ms (0% of total)
ival-if: 5.0ms (0% of total)
Bogosity

simplify34.6s (17.1%)

Memory
149.7MiB live, 32 231.2MiB allocated; 11.0s collecting garbage
Stop Event
180×node limit
147×iter limit
18×saturated
Counts
11 300 → 11 015

rewrite17.9s (8.9%)

Memory
-154.5MiB live, 16 831.3MiB allocated; 4.0s collecting garbage
Stop Event
452×iter limit
118×node limit
31×unsound
10×saturated
Counts
3 331 → 40 783

eval13.6s (6.7%)

Memory
78.7MiB live, 17 040.6MiB allocated; 5.8s collecting garbage
Compiler

Compiled 3 146 275 to 244 541 computations (92.2% saved)

derivations11.7s (5.8%)

Memory
-17.4MiB live, 8 507.7MiB allocated; 1.5s collecting garbage
Stop Event
24×fuel
18×done
Compiler

Compiled 24 184 to 2 661 computations (89% saved)

explain10.1s (5%)

Memory
-29.1MiB live, 13 790.3MiB allocated; 2.1s collecting garbage
Explanations
Click to see full explanations table
OperatorSubexpressionExplanationCount
-.f64#fcancellation13071
+.f64#fcancellation37483
sqrt.f64#foflow-rescue2400
-.f64(-.f64 (*.f64 #s(literal 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 binary64) t) #s(literal 170000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 binary64))oflow-left2230
log.f64(log.f64 (+.f64 #s(literal 1 binary64) x))sensitivity1790
/.f64#fn/o1650
/.f64#fo/o1470
pow.f64(pow.f64 (+.f64 #s(literal 1 binary64) (/.f64 i n)) n)sensitivity1040
-.f64#fnan-rescue1010
/.f64#fu/n770
/.f64#fu/u510
/.f64#fn/u500
/.f64#fo/n430
+.f64#fnan-rescue410
*.f64#fn*o360
*.f64#fn*u350
pow.f64(pow.f64 (+.f64 #s(literal 1 binary64) (/.f64 i n)) n)oflow-rescue160
(pow.f64 (+.f64 #s(literal 1 binary64) (/.f64 i n)) n)overflow36
(/.f64 i n)overflow16
(+.f64 #s(literal 1 binary64) (/.f64 i n))overflow16
sqrt.f64#fuflow-rescue140
exp.f64#fsensitivity40
Confusion
Predicted +Predicted -
+3876222
-1356519
Precision
0.9663425579655947
Recall
0.9458272327964861
Confusion?
Predicted +Predicted MaybePredicted -
+387615864
-1351826337
Precision?
0.9271431854746035
Recall?
0.984382625671059
Freqs
test
numberfreq
06741
13580
2392
338
41
Total Confusion?
Predicted +Predicted MaybePredicted -
+3010
-209
Precision?
0.9393939393939394
Recall?
1.0
Samples
1.5s16 310×0valid
1.4s3 658×1valid
689.0ms1 500×2valid
24.0ms36×3valid
Compiler

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

Precisions
Click to see histograms. Total time spent on operations: 2.5s
ival-mult: 644.0ms (25.7% of total)
ival-add: 410.0ms (16.4% of total)
adjust: 407.0ms (16.3% of total)
ival-div: 276.0ms (11% of total)
ival-pow: 224.0ms (9% of total)
ival-sub: 164.0ms (6.6% of total)
ival-sin: 96.0ms (3.8% of total)
ival-cos: 69.0ms (2.8% of total)
const: 43.0ms (1.7% of total)
ival-exp: 38.0ms (1.5% of total)
ival-pow2: 27.0ms (1.1% of total)
ival-sqrt: 21.0ms (0.8% of total)
ival-true: 19.0ms (0.8% of total)
exact: 19.0ms (0.8% of total)
ival-neg: 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-pi: 3.0ms (0.1% of total)
ival-expm1: 3.0ms (0.1% of total)

preprocess10.0s (5%)

Memory
672.4MiB live, 10 950.0MiB allocated; 2.0s collecting garbage
Stop Event
84×iter limit
62×node limit
22×saturated
Compiler

Compiled 53 869 to 8 546 computations (84.1% saved)

regimes5.5s (2.7%)

Memory
-216.4MiB live, 6 764.6MiB allocated; 1.1s collecting garbage
Counts
4 354 → 544
Calls

96 calls:

549.0ms
x
285.0ms
a
239.0ms
x1
189.0ms
b
186.0ms
d
Compiler

Compiled 9 029 to 5 544 computations (38.6% saved)

prune4.9s (2.4%)

Memory
-491.3MiB live, 7 711.7MiB allocated; 1.8s collecting garbage
Counts
60 362 → 1 883
Compiler

Compiled 149 391 to 63 127 computations (57.7% saved)

series4.4s (2.2%)

Memory
151.1MiB live, 5 743.4MiB allocated; 841ms collecting garbage
Counts
3 331 → 11 300
Calls

879 calls:

TimeVariablePointExpression
159.0ms
x
@inf
((* (/ x (- (pow x 4) 1)) (+ (* x x) -1)) (/ x (- (pow x 4) 1)) (neg x) x (+ (* x x) -1) -1 (* (/ x (+ (* (* x x) (* x x)) -1)) (- (* x x) 1)) (/ x (+ (* (* x x) (* x x)) -1)) (+ (* (* x x) (* x x)) -1) (* x x) (- (* x x) 1) 1)
103.0ms
a
@inf
((/ (- (neg b) (sqrt (+ (* (* c a) -4) (* b b)))) (+ a a)) (- (neg b) (sqrt (+ (* (* c a) -4) (* b b)))) (neg b) b (sqrt (+ (* (* c a) -4) (* b b))) (+ (* (* c a) -4) (* b b)) (* c a) c a -4 (* b b) (+ a a) (/ (- (neg b) (sqrt (- (* b b) (* 4 (* a c))))) (* 2 a)) (+ (* (/ b a) -1) (/ c b)) (/ c b) (/ (- (neg b) (sqrt (- (* b b) (* 4 (* a c))))) (* 2 a)) (- (neg b) (sqrt (- (* b b) (* 4 (* a c))))) (* (* (/ a b) -2) c) (* (/ a b) -2) (/ a b) -2 (* 2 a) 2 (- (/ b (* -2 a)) (/ (sqrt (- (* b b) (* 4 (* a c)))) (* 2 a))) (/ b (* -2 a)) (* -2 a) (/ (sqrt (- (* b b) (* 4 (* a c)))) (* 2 a)) (sqrt (- (* b b) (* 4 (* a c)))) (- (* b b) (* 4 (* a c))) (* -4 (* a c)) (* a c) (/ (- (* b b) (- (* b b) (* 4 (* a c)))) (* (+ (sqrt (- (* b b) (* 4 (* a c)))) (neg b)) (* 2 a))) (- (* b b) (- (* b b) (* 4 (* a c)))) (* (+ (sqrt (- (* b b) (* 4 (* a c)))) (neg b)) (* 2 a)) (+ (sqrt (- (* b b) (* 4 (* a c)))) (neg b)))
84.0ms
i
@-inf
((* (/ (* (- (exp (* (log (+ 1 (/ i n))) n)) 1) 100) i) n) (/ (* (- (exp (* (log (+ 1 (/ i n))) n)) 1) 100) i) (* (- (exp (* (log (+ 1 (/ i n))) n)) 1) 100) (- (exp (* (log (+ 1 (/ i n))) n)) 1) (* (log (+ 1 (/ i n))) n) (log (+ 1 (/ i n))) (/ i n) i n 100 (* (/ (- (pow (+ 1 (/ i n)) n) 1) i) (* n 100)) (/ (- (pow (+ 1 (/ i n)) n) 1) i) (- (pow (+ 1 (/ i n)) n) 1) (pow (+ 1 (/ i n)) n) 1 (* n 100) (* (/ (- (pow (+ 1 (/ i n)) n) 1) i) (* 100 n)) (/ (- (pow (+ 1 (/ i n)) n) 1) i) (- (pow (+ 1 (/ i n)) n) 1) (* (+ (* (- 1/2 (/ 1/2 n)) i) 1) i) (+ (* (- 1/2 (/ 1/2 n)) i) 1) (- 1/2 (/ 1/2 n)) 1/2 (/ 1/2 n) (* 100 n) (* 100 (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n))) (/ (- (pow (+ 1 (/ i n)) n) 1) (/ i n)) (- (pow (+ 1 (/ i n)) n) 1) (+ (* (* i i) (+ (* (- (+ (/ 1/3 (* n n)) 1/6) (/ 1/2 n)) i) (- 1/2 (/ 1/2 n)))) i) (* i i) (+ (* (- (+ (/ 1/3 (* n n)) 1/6) (/ 1/2 n)) i) (- 1/2 (/ 1/2 n))) (/ (+ (* (+ (* -1/2 i) (+ (* (+ (* 1/6 i) 1/2) n) -1/2)) n) (* 1/3 i)) (* n n)) (* (/ (+ (* (+ (* 1/6 n) -1/2) n) 1/3) n) (/ i n)) (/ (+ (* (+ (* 1/6 n) -1/2) n) 1/3) n) (+ (* (+ (* 1/6 n) -1/2) n) 1/3) (+ (* 1/6 n) -1/2) 1/6 -1/2 1/3 (* (/ (- (exp (* (log (+ 1 (/ i n))) n)) 1) (/ i n)) 100) (/ (- (exp (* (log (+ 1 (/ i n))) n)) 1) (/ i n)) (* (* (/ (log (/ i n)) i) n) n) (* (/ (log (/ i n)) i) n) (/ (log (/ i n)) i) (log (/ i n)))
81.0ms
r
@-inf
((- (- (+ 3 (/ 2 (* r r))) (/ (* (* 1/8 (- 3 (* 2 v))) (* (* (* w w) r) r)) (- 1 v))) 9/2) (- (/ 2 (* r r)) (+ (* (* (* 1/4 r) w) (* w r)) 3/2)) (/ 2 (* r r)) 2 (* r r) r (+ (* (* (* 1/4 r) w) (* w r)) 3/2) (* (* 1/4 r) w) (* 1/4 r) 1/4 w (* w r) 3/2 (- (- (+ 3 (/ 2 (* r r))) (/ (* (* 1/8 (- 3 (* 2 v))) (* (* (* w w) r) r)) (- 1 v))) 9/2) (- (/ 2 (* r r)) (+ (* (* (* w (* 1/4 r)) r) w) 3/2)) (* (* (* -1/4 (* r r)) w) w) (* (* -1/4 (* r r)) w) (* -1/4 (* r r)) -1/4 (- (- (+ 3 (/ 2 (* r r))) (/ (* (* 1/8 (- 3 (* 2 v))) (* (* (* w w) r) r)) (- 1 v))) 9/2) (- (/ 2 (* r r)) (+ (* (* (* 3/8 (* r r)) w) w) 3/2)) (+ (* (* (* 3/8 (* r r)) w) w) 3/2) (* (* 3/8 (* r r)) w) (* 3/8 (* r r)) 3/8 (- (- (+ 3 (/ 2 (* r r))) (/ (* (* 1/8 (- 3 (* 2 v))) (* (* (* w r) w) r)) (- 1 v))) 9/2) (- (+ 3 (/ 2 (* r r))) (/ (* (* 1/8 (- 3 (* 2 v))) (* (* (* w r) w) r)) (- 1 v))) (+ 3 (/ 2 (* r r))) 3 (/ (* (* 1/8 (- 3 (* 2 v))) (* (* (* w r) w) r)) (- 1 v)) (* (* (* (* w r) w) r) (+ (* v 1/8) 3/8)) (* (* (* w r) w) r) (* (* w r) w) (+ (* v 1/8) 3/8) v 1/8 9/2 (- (- (+ 3 (/ 2 (* r r))) (/ (* (* 1/8 (- 3 (* 2 v))) (* (* (* w w) r) r)) (- 1 v))) 9/2) (- (+ 3 (/ 2 (* r r))) (/ (* (* 1/8 (- 3 (* 2 v))) (* (* (* w w) r) r)) (- 1 v))) (/ (* (* 1/8 (- 3 (* 2 v))) (* (* (* w w) r) r)) (- 1 v)) (* (* 1/8 (- 3 (* 2 v))) (* (* (* w w) r) r)) (* 1/8 (- 3 (* 2 v))) (+ (* -1/4 v) 3/8) (* (* (* w w) r) r) (* (* w w) r) (* w w) (- 1 v) 1)
70.0ms
x
@inf
((- (/ (* x x) (+ (sqrt (- (* x x) eps)) x)) (/ (- (* x x) eps) (+ (sqrt (- (* x x) eps)) x))) (/ (* x x) (+ (sqrt (- (* x x) eps)) x)) (* x x) x (+ (sqrt (- (* x x) eps)) x) (sqrt (- (* x x) eps)) (- (* x x) eps) eps (/ (- (* x x) eps) (+ (sqrt (- (* x x) eps)) x)) (- x (sqrt (- (* x x) eps))) (* (/ 1/2 x) eps) (/ 1/2 x) 1/2 (- x (sqrt (- (* x x) eps))) (sqrt (- (* x x) eps)) (- (* x x) eps) (* (- (neg (/ eps (* x x))) -1) (* x x)) (- (neg (/ eps (* x x))) -1) (neg (/ eps (* x x))) (/ eps (* x x)) -1 (/ (* (+ (* x (+ (sqrt (- (* x x) eps)) x)) (- (* x x) eps)) (- x (sqrt (- (* x x) eps)))) (+ (* x x) (+ (* (sqrt (- (* x x) eps)) x) (- (* x x) eps)))) (* (+ (* x (+ (sqrt (- (* x x) eps)) x)) (- (* x x) eps)) (- x (sqrt (- (* x x) eps)))) (+ (* x (+ (sqrt (- (* x x) eps)) x)) (- (* x x) eps)) (- x (sqrt (- (* x x) eps))) (+ (* x x) (+ (* (sqrt (- (* x x) eps)) x) (- (* x x) eps))) (+ (* (sqrt (- (* x x) eps)) x) (- (* x x) eps)) (/ (+ (* (* x x) x) (* (neg (pow (- (* x x) eps) 3/4)) (pow (- (* x x) eps) 3/4))) (+ (* x x) (+ (* (sqrt (- (* x x) eps)) x) (- (* x x) eps)))) (+ (* (* x x) x) (* (neg (pow (- (* x x) eps) 3/4)) (pow (- (* x x) eps) 3/4))) (* (neg (pow (- (* x x) eps) 3/4)) (pow (- (* x x) eps) 3/4)) (neg (pow (- (* x x) eps) 3/4)) (pow (- (* x x) eps) 3/4) 3/4)

analyze4.4s (2.2%)

Memory
64.1MiB live, 5 181.3MiB allocated; 1.1s 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)

bsearch3.0s (1.5%)

Memory
-9.7MiB live, 2 828.2MiB allocated; 480ms collecting garbage
Algorithm
178×binary-search
95×left-value
Stop Event
172×narrow-enough
predicate-same
predicate-failed
Samples
1.2s9 858×0valid
407.0ms1 624×1valid
186.0ms378×2valid
68.0ms1 074×0invalid
12.0ms12×3valid
Compiler

Compiled 107 458 to 60 868 computations (43.4% saved)

Precisions
Click to see histograms. Total time spent on operations: 1.4s
ival-mult: 412.0ms (29.7% of total)
ival-pow: 245.0ms (17.6% of total)
ival-div: 186.0ms (13.4% of total)
ival-sub: 152.0ms (10.9% of total)
ival-add: 135.0ms (9.7% of total)
adjust: 87.0ms (6.3% of total)
ival-exp: 71.0ms (5.1% of total)
ival-neg: 39.0ms (2.8% of total)
ival-sqrt: 31.0ms (2.2% of total)
ival-true: 10.0ms (0.7% of total)
exact: 10.0ms (0.7% of total)
ival-assert: 5.0ms (0.4% of total)
const: 3.0ms (0.2% of total)
ival-expm1: 2.0ms (0.1% of total)
ival-pi: 1.0ms (0.1% of total)

start3.0ms (0%)

Memory
6.6MiB live, 6.5MiB allocated; 0ms collecting garbage

end0.0ms (0%)

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

Profiling

Loading profile data...