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:121 856.1 MB

Time bar (total: 2.1min)

sample52.6s (41.7%)

Memory
486.1MiB live, 49 776.6MiB allocated; 15.9s collecting garbage
Samples
14.6s16 424×5exit
11.6s39 858×1valid
10.3s108 898×0valid
6.0s16 364×2valid
480.0ms3 991×0invalid
128.0ms1 380×0exit
Precisions
Click to see histograms. Total time spent on operations: 34.7s
ival-exp: 4.4s (12.8% of total)
adjust: 4.0s (11.5% of total)
ival-pow: 3.9s (11.3% of total)
ival-log: 3.2s (9.1% of total)
const: 2.6s (7.5% of total)
ival-cos: 2.3s (6.5% of total)
ival-mult: 1.7s (5% of total)
ival-tan: 1.7s (4.8% of total)
ival-sinh: 1.3s (3.9% of total)
ival-div: 1.3s (3.7% of total)
ival-sin: 1.2s (3.5% of total)
ival-sqrt: 1.0s (3% of total)
ival-fmod: 1.0s (3% of total)
ival-add: 886.0ms (2.6% of total)
ival-sub: 878.0ms (2.5% of total)
ival-pow2: 669.0ms (1.9% of total)
ival-<=: 621.0ms (1.8% of total)
ival-acos: 533.0ms (1.5% of total)
ival-hypot: 248.0ms (0.7% of total)
ival-neg: 244.0ms (0.7% of total)
ival-<: 228.0ms (0.7% of total)
ival-==: 198.0ms (0.6% of total)
ival-and: 121.0ms (0.3% of total)
ival-true: 115.0ms (0.3% of total)
ival-assert: 90.0ms (0.3% of total)
exact: 81.0ms (0.2% of total)
ival-atan: 46.0ms (0.1% of total)
ival-or: 42.0ms (0.1% of total)
ival->=: 27.0ms (0.1% of total)
ival->: 18.0ms (0.1% of total)
Bogosity

simplify22.1s (17.5%)

Memory
-180.8MiB live, 19 876.5MiB allocated; 3.5s collecting garbage
Stop Event
218×iter limit
136×node limit
19×saturated
unsound
Counts
4 972 → 4 972

localize13.0s (10.3%)

Memory
24.2MiB live, 13 478.0MiB allocated; 2.2s collecting garbage
Samples
5.1s5 442×1valid
2.1s1 767×2valid
2.0s9 786×0valid
1.4s198×5exit
75.0ms393×0invalid
25.0ms70×0exit
10.0ms3valid
Compiler

Compiled 11 798 to 1 769 computations (85% saved)

Precisions
Click to see histograms. Total time spent on operations: 8.7s
adjust: 1.6s (18.8% of total)
ival-mult: 1.4s (15.8% of total)
ival-cos: 1.3s (15% of total)
ival-div: 673.0ms (7.7% of total)
ival-tan: 631.0ms (7.3% of total)
ival-add: 570.0ms (6.6% of total)
ival-sin: 442.0ms (5.1% of total)
ival-sqrt: 330.0ms (3.8% of total)
ival-sub: 295.0ms (3.4% of total)
ival-log: 291.0ms (3.4% of total)
const: 288.0ms (3.3% of total)
ival-pow2: 148.0ms (1.7% of total)
ival-exp: 132.0ms (1.5% of total)
ival-pow: 119.0ms (1.4% of total)
ival-sinh: 111.0ms (1.3% of total)
ival-fmod: 99.0ms (1.1% of total)
ival-asin: 67.0ms (0.8% of total)
ival-neg: 42.0ms (0.5% of total)
ival-acos: 37.0ms (0.4% of total)
ival-hypot: 25.0ms (0.3% of total)
ival-pi: 23.0ms (0.3% of total)
exact: 20.0ms (0.2% of total)
ival-true: 14.0ms (0.2% of total)
ival-assert: 8.0ms (0.1% of total)
ival-cbrt: 5.0ms (0.1% of total)
ival-atan: 1.0ms (0% of total)

rewrite6.7s (5.3%)

Memory
682.7MiB live, 6 584.2MiB allocated; 864ms collecting garbage
Stop Event
208×iter limit
46×node limit
21×unsound
saturated
Counts
949 → 15 275

preprocess5.0s (3.9%)

Memory
31.5MiB live, 4 048.0MiB allocated; 1.9s collecting garbage
Stop Event
38×iter limit
29×node limit
13×saturated
Compiler

Compiled 8 931 to 3 064 computations (65.7% saved)

derivations4.7s (3.7%)

Memory
-93.6MiB live, 2 925.6MiB allocated; 470ms collecting garbage
Stop Event
12×fuel
done
Compiler

Compiled 3 744 to 1 018 computations (72.8% saved)

regimes4.4s (3.5%)

Memory
-0.8MiB live, 5 335.5MiB allocated; 889ms collecting garbage
Counts
3 045 → 188
Calls

53 calls:

617.0ms
x
405.0ms
a
349.0ms
b
290.0ms
r
247.0ms
(/.f64 (sin.f64 b) (cos.f64 (+.f64 a b)))
Compiler

Compiled 1 785 to 2 051 computations (-14.9% saved)

analyze4.1s (3.2%)

Memory
31.0MiB live, 4 105.4MiB allocated; 1.6s collecting garbage
Algorithm
20×search
Search
ProbabilityValidUnknownPreconditionInfiniteDomainCan'tIter
0%0%73.7%26.3%0%0%0%0
28.8%21.3%52.5%26.3%0%0%0%1
44.1%32.5%41.2%26.3%0%0%0%2
52.6%38.7%35%26.3%0%0%0%3
61.9%45.6%28.1%26.3%0%0%0%4
65.2%47.5%25.3%26.3%0%0.9%0%5
66.8%48.4%24%26.3%0%1.2%0%6
71.1%51.1%20.8%26.3%0%1.9%0%7
72.1%51.6%20%26.3%0%2.1%0%8
74.4%53%18.2%26.3%0%2.5%0%9
75.8%53.9%17.2%26.3%0%2.6%0%10
76.6%54.3%16.6%26.3%0%2.8%0%11
77.3%54.8%16.1%26.3%0%2.9%0%12
Compiler

Compiled 279 to 216 computations (22.6% saved)

explain3.8s (3%)

Memory
-44.8MiB live, 3 532.4MiB allocated; 1.9s collecting garbage
Explanations
Click to see full explanations table
OperatorSubexpressionExplanationCount
sqrt.f64#foflow-rescue6310
cos.f64#fsensitivity4860
-.f64#fcancellation3462
sqrt.f64#fuflow-rescue3040
/.f64#fn/o2580
acos.f64(acos.f64 (-.f64 #s(literal 1 binary64) x))sensitivity2540
log.f64(log.f64 (/.f64 (sinh.f64 x) x))sensitivity2450
tan.f64(tan.f64 (+.f64 y z))sensitivity2000
pow.f64(pow.f64 l (exp.f64 w))sensitivity13112
*.f64#fn*o380
*.f64#fn*u280
*.f64#fu*o190
-.f64(-.f64 (*.f64 a a) (*.f64 b b))nan-rescue130
(*.f64 a a)overflow111
(*.f64 b b)overflow13
*.f64(*.f64 (pow.f64 c #s(literal 2 binary64)) (*.f64 (*.f64 x (pow.f64 s #s(literal 2 binary64))) x))o*u130
(pow.f64 c #s(literal 2 binary64))overflow58
(*.f64 (*.f64 x (pow.f64 s #s(literal 2 binary64))) x)underflow75
(*.f64 x (pow.f64 s #s(literal 2 binary64)))underflow63
(pow.f64 s #s(literal 2 binary64))underflow58
log.f64(log.f64 (/.f64 (sinh.f64 x) x))oflow-rescue80
(sinh.f64 x)overflow8
(/.f64 (sinh.f64 x) x)overflow8
exp.f64(exp.f64 (neg.f64 w))sensitivity21
Confusion
Predicted +Predicted -
+2236267
-6791938
Precision
0.7670668953687821
Recall
0.8933280063923292
Confusion?
Predicted +Predicted MaybePredicted -
+22362265
-679131925
Precision?
0.7638225255972696
Recall?
0.8941270475429485
Freqs
test
numberfreq
02205
12854
261
Total Confusion?
Predicted +Predicted MaybePredicted -
+1800
-002
Precision?
1.0
Recall?
1.0
Samples
552.0ms98×5exit
493.0ms2 466×1valid
435.0ms6 682×0valid
304.0ms994×2valid
Compiler

Compiled 1 067 to 440 computations (58.8% saved)

Precisions
Click to see histograms. Total time spent on operations: 1.4s
ival-cos: 504.0ms (35.4% of total)
adjust: 173.0ms (12.2% of total)
ival-mult: 110.0ms (7.7% of total)
ival-sqrt: 98.0ms (6.9% of total)
ival-tan: 82.0ms (5.8% of total)
ival-exp: 60.0ms (4.2% of total)
ival-log: 58.0ms (4.1% of total)
ival-div: 44.0ms (3.1% of total)
ival-add: 40.0ms (2.8% of total)
ival-fmod: 40.0ms (2.8% of total)
ival-sinh: 39.0ms (2.7% of total)
ival-sin: 37.0ms (2.6% of total)
ival-sub: 36.0ms (2.5% of total)
ival-pow2: 30.0ms (2.1% of total)
ival-acos: 30.0ms (2.1% of total)
ival-hypot: 9.0ms (0.6% of total)
ival-true: 8.0ms (0.6% of total)
ival-pow: 8.0ms (0.6% of total)
ival-neg: 7.0ms (0.5% of total)
ival-assert: 4.0ms (0.3% of total)
ival-atan: 3.0ms (0.2% of total)
exact: 2.0ms (0.1% of total)

series3.4s (2.7%)

Memory
173.4MiB live, 3 667.6MiB allocated; 1.6s collecting garbage
Counts
949 → 4 972
Calls

387 calls:

TimeVariablePointExpression
110.0ms
hi
@0
((exp (* (log (/ (neg lo) hi)) 3)) (/ (- x lo) (- hi lo)) (/ (+ (* (/ (- x lo) hi) (+ (* lo (/ lo hi)) lo)) (- x lo)) hi) (* (log (/ (neg lo) hi)) 3) (/ (- x lo) (- hi lo)) (- 1 (/ x lo)) (/ x lo) (- (/ (+ (* (/ (- x lo) hi) lo) x) hi) (/ lo hi)) (/ (- x lo) (- hi lo)) (/ (+ (* (/ (- x lo) hi) lo) x) hi) (+ (* (/ (- x lo) hi) lo) x) (/ (- x lo) (- hi lo)) (/ (+ (* (/ (- x lo) hi) (+ (* lo (/ lo hi)) lo)) (- x lo)) hi) (+ (* (/ (- x lo) hi) (+ (* lo (/ lo hi)) lo)) (- x lo)) (+ (* (+ (* (- (/ (/ (- x lo) hi) hi) (/ 1 hi)) lo) (- (/ x hi) 1)) lo) x) (+ (* (/ (/ (+ (* -1 (/ lo hi)) -1) hi) x) x) (/ (/ x hi) hi)) (+ (* -1 (/ lo hi)) -1) (/ (- x lo) (- hi lo)) (/ (+ (* (/ (- x lo) hi) (+ (* lo (/ lo hi)) lo)) (- x lo)) hi) (log (/ (neg lo) hi)) (- (/ (/ (- x lo) hi) hi) (/ 1 hi)) (+ (* (- (/ (/ (- x lo) hi) hi) (/ 1 hi)) lo) (- (/ x hi) 1)))
90.0ms
x
@0
((* (sqrt x) (sqrt (+ x x))) (sqrt x) (sqrt (+ x x)) (+ x x) (* (pow x 1/4) (pow x 1/4)) (* (* (pow x 1/4) (pow x 1/4)) (sqrt (* 2 x))) (pow x 1/4) (sqrt (* 2 x)) (* 2 x))
77.0ms
x
@-inf
((* (* (* (+ (* (* x x) 1/2835) -1/180) x) x) x) (log (/ (sinh x) x)) (* (+ (* x 1/6) (* (* (* (+ (* (* x x) 1/2835) -1/180) x) x) x)) x) (+ (* x 1/6) (* (* (* (+ (* (* x x) 1/2835) -1/180) x) x) x)) (log (/ (sinh x) x)) (* (* (+ (* (+ (* (+ (* -1/37800 (* x x)) 1/2835) (* x x)) -1/180) (* x x)) 1/6) x) x) (* (+ (* (+ (* (+ (* -1/37800 (* x x)) 1/2835) (* x x)) -1/180) (* x x)) 1/6) x) (+ (* (+ (* (+ (* -1/37800 (* x x)) 1/2835) (* x x)) -1/180) (* x x)) 1/6) (log (/ (sinh x) x)) (/ (sinh x) x) (+ (* (* x x) 1/6) 1) (* x x) (log (/ (sinh x) x)) (* (* (+ (* (+ (* 1/2835 (* x x)) -1/180) (* x x)) 1/6) x) x) (* (- (- (/ 1/6 (pow x 4)) -1/2835) (/ 1/180 (* x x))) (pow x 6)) (- (- (/ 1/6 (pow x 4)) -1/2835) (/ 1/180 (* x x))) (- (- (log (* 2 (sinh x))) (log 2)) (log x)) (- (log (* 2 (sinh x))) (log 2)) (log (* 2 (sinh x))) (* 2 (sinh x)) (* (+ (* (* x x) 1/2835) -1/180) x) (* (* (+ (* (* x x) 1/2835) -1/180) x) x) (/ 1/180 (* x x)) (sinh x))
59.0ms
x
@-inf
((log (/ (sinh x) x)) (* (* (+ (* (+ (* 1/2835 (* x x)) -1/180) (* x x)) 1/6) x) x) (* (+ (* (+ (* 1/2835 (* x x)) -1/180) (* x x)) 1/6) x) (+ (* (+ (* 1/2835 (* x x)) -1/180) (* x x)) 1/6) (log (/ (sinh x) x)) (* (* x x) 1/6) (* x x) (log (/ (sinh x) x)) (* (* (+ (* (+ (* (+ (* -1/37800 (* x x)) 1/2835) (* x x)) -1/180) (* x x)) 1/6) x) x) (* (+ (* (+ (* (+ (* -1/37800 (* x x)) 1/2835) (* x x)) -1/180) (* x x)) 1/6) x) (+ (* (+ (* (+ (* -1/37800 (* x x)) 1/2835) (* x x)) -1/180) (* x x)) 1/6) (log (/ (sinh x) x)) (/ (sinh x) x) (+ (* (+ (* 1/120 (* x x)) 1/6) (* x x)) 1) (+ (* 1/120 (* x x)) 1/6) (- (log (sinh x)) (log x)) (log (sinh x)) (sinh x) (log x) (+ (* 1/2835 (* x x)) -1/180) (+ (* (+ (* -1/37800 (* x x)) 1/2835) (* x x)) -1/180))
56.0ms
r
@-inf
((* r (/ (sin b) (+ (* (cos b) (cos a)) (* (neg (sin a)) (sin b))))) (/ (sin b) (+ (* (cos b) (cos a)) (* (neg (sin a)) (sin b)))) (sin b) (+ (* (cos b) (cos a)) (* (neg (sin a)) (sin b))) (* r (/ (sin b) (cos (+ a b)))) (* (/ r (cos a)) b) (/ r (cos a)) (cos a) (sin (neg (+ (PI) b))) (* r (/ (sin (neg (+ (PI) b))) (cos (+ a b)))) (/ (sin (neg (+ (PI) b))) (cos (+ a b))) (neg (+ (PI) b)) (* r (/ (sin b) (cos (+ a b)))) (/ (sin b) (cos (+ a b))) (sin b) (+ (* (pow b 3) (+ (* 1/120 (* b b)) -1/6)) b) (* (/ (sin b) (* (cos (- b a)) (cos (+ a b)))) (cos (- b a))) (* r (* (/ (sin b) (* (cos (- b a)) (cos (+ a b)))) (cos (- b a)))) (/ (sin b) (* (cos (- b a)) (cos (+ a b)))) (* (neg (sin a)) (sin b)) (cos (+ a b)) (+ (* 1/120 (* b b)) -1/6) (cos (- b a)) (* (cos (- b a)) (cos (+ a b))))

eval3.4s (2.7%)

Memory
-272.7MiB live, 4 286.6MiB allocated; 720ms collecting garbage
Compiler

Compiled 758 567 to 82 797 computations (89.1% saved)

prune2.1s (1.7%)

Memory
-155.7MiB live, 3 149.0MiB allocated; 377ms collecting garbage
Counts
21 275 → 1 584
Compiler

Compiled 94 342 to 45 986 computations (51.3% saved)

bsearch1.1s (0.9%)

Memory
40.1MiB live, 1 088.8MiB allocated; 112ms collecting garbage
Algorithm
49×binary-search
11×left-value
Stop Event
42×narrow-enough
predicate-failed
predicate-same
Samples
476.0ms1 969×1valid
186.0ms2 399×0valid
70.0ms606×0invalid
2.0ms22×0exit
Compiler

Compiled 13 071 to 10 728 computations (17.9% saved)

Precisions
Click to see histograms. Total time spent on operations: 539.0ms
ival-tan: 125.0ms (23.2% of total)
ival-cos: 100.0ms (18.6% of total)
adjust: 67.0ms (12.4% of total)
ival-sin: 42.0ms (7.8% of total)
ival-mult: 40.0ms (7.4% of total)
ival-exp: 39.0ms (7.2% of total)
ival-add: 32.0ms (5.9% of total)
ival-fmod: 16.0ms (3% of total)
ival-div: 15.0ms (2.8% of total)
ival-pow2: 15.0ms (2.8% of total)
ival-pow: 12.0ms (2.2% of total)
ival-sub: 9.0ms (1.7% of total)
ival-sqrt: 9.0ms (1.7% of total)
ival-neg: 7.0ms (1.3% of total)
ival-acos: 4.0ms (0.7% of total)
ival-true: 4.0ms (0.7% of total)
ival-assert: 2.0ms (0.4% of total)
exact: 1.0ms (0.2% of total)

start1.0ms (0%)

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

end0.0ms (0%)

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

Profiling

Loading profile data...