Herbie run

Date:Thursday, December 5th, 2024
Commit:4b098aa3 on Unsound-rule-removal
Hostname:nightly with Racket 8.10
Seed:2024340
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:240 044.5 MB

Time bar (total: 4.4min)

sample2.0min (44.4%)

Memory
1 162.6MiB live, 109 864.3MiB allocated
Samples
31.2s41 333×2valid
24.0s144 319×0invalid
19.8s92 265×1valid
9.9s4 796×5exit
9.1s94 611×0valid
2.4s2 956×3valid
551.0ms2 304×1exit
380.0ms4 118×0exit
17.0ms6×4exit
3.0ms3×4valid
3.0ms2×3exit
3.0ms4×2exit
Precisions
Click to see histograms. Total time spent on operations: 1.4min
ival-tan: 14.2s (17.3% of total)
ival-pow: 10.2s (12.4% of total)
ival-mult: 6.0s (7.3% of total)
adjust: 5.8s (7.1% of total)
const: 5.4s (6.5% of total)
ival-cos: 5.0s (6.1% of total)
ival-div: 4.4s (5.3% of total)
ival-sub: 4.3s (5.2% of total)
ival-log: 3.8s (4.6% of total)
ival-sin: 3.5s (4.3% of total)
ival-add: 3.3s (4% of total)
ival-fabs: 2.6s (3.1% of total)
ival-exp: 2.3s (2.8% of total)
ival-<=: 2.2s (2.7% of total)
ival-expm1: 1.6s (2% of total)
ival-sqrt: 1.3s (1.6% of total)
ival-log1p: 1.1s (1.4% of total)
ival-cbrt: 953.0ms (1.2% of total)
ival-<: 949.0ms (1.2% of total)
ival-fmin: 891.0ms (1.1% of total)
ival-and: 617.0ms (0.8% of total)
ival-atan: 476.0ms (0.6% of total)
exact: 349.0ms (0.4% of total)
ival-neg: 333.0ms (0.4% of total)
ival->: 269.0ms (0.3% of total)
ival-assert: 154.0ms (0.2% of total)
ival-true: 68.0ms (0.1% of total)
Bogosity

simplify36.3s (13.6%)

Memory
112.9MiB live, 30 824.4MiB allocated
Algorithm
248×egg-herbie
Stop Event
331×iter limit
215×node limit
33×saturated
Counts
8 176 → 8 083

soundness27.4s (10.3%)

Memory
106.2MiB live, 16 845.0MiB allocated
Stop Event
204×iter limit
137×node limit
24×fuel
4×done
Compiler

Compiled 13 732 to 6 163 computations (55.1% saved)

localize23.6s (8.9%)

Memory
536.5MiB live, 23 075.1MiB allocated
Samples
7.8s6 123×2valid
7.7s10 902×1valid
2.5s10 489×0valid
1.0s581×3valid
122.0ms63×5exit
2.0ms2×3exit
Compiler

Compiled 22 893 to 3 385 computations (85.2% saved)

Precisions
Click to see histograms. Total time spent on operations: 15.7s
ival-div: 2.4s (15.3% of total)
ival-mult: 2.4s (15% of total)
adjust: 2.1s (13.3% of total)
ival-tan: 1.7s (11% of total)
ival-add: 1.4s (8.6% of total)
ival-sub: 982.0ms (6.2% of total)
ival-pow: 735.0ms (4.7% of total)
ival-cos: 706.0ms (4.5% of total)
ival-log: 603.0ms (3.8% of total)
const: 587.0ms (3.7% of total)
ival-sin: 449.0ms (2.9% of total)
ival-exp: 396.0ms (2.5% of total)
ival-sqrt: 295.0ms (1.9% of total)
ival-pow2: 266.0ms (1.7% of total)
ival-log1p: 251.0ms (1.6% of total)
ival-neg: 117.0ms (0.7% of total)
ival-cosh: 94.0ms (0.6% of total)
ival-cbrt: 82.0ms (0.5% of total)
ival-expm1: 78.0ms (0.5% of total)
exact: 47.0ms (0.3% of total)
ival-true: 24.0ms (0.2% of total)
ival-hypot: 18.0ms (0.1% of total)
ival-atan2: 15.0ms (0.1% of total)
ival-assert: 12.0ms (0.1% of total)
ival-atan: 9.0ms (0.1% of total)
ival-pi: 8.0ms (0.1% of total)
ival-acosh: 7.0ms (0% of total)
ival-sinh: 5.0ms (0% of total)
ival-fabs: 4.0ms (0% of total)

rewrite23.1s (8.7%)

Memory
290.0MiB live, 20 507.0MiB allocated
Stop Event
222×iter limit
110×node limit
Counts
1 682 → 47 707

eval12.2s (4.6%)

Memory
-840.3MiB live, 12 145.9MiB allocated
Compiler

Compiled 2 311 482 to 246 786 computations (89.3% saved)

explain6.6s (2.5%)

Memory
-195.9MiB live, 6 355.8MiB allocated
Explanations
Click to see full explanations table
OperatorSubexpressionExplanationCount
-.f64#fcancellation414422
log.f64#fsensitivity7670
/.f64#fu/u4280
sqrt.f64#foflow-rescue3860
+.f64#fcancellation3400
/.f64#fu/n1140
pow.f64(pow.f64 (+.f64 x #s(literal 1 binary64)) (/.f64 #s(literal 1 binary64) n))sensitivity731
/.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/u260
↳(*.f64 b eps)underflow148
↳(-.f64 (exp.f64 (*.f64 a eps)) #s(literal 1 binary64))underflow152
↳(-.f64 (exp.f64 (*.f64 b eps)) #s(literal 1 binary64))underflow148
↳(*.f64 (-.f64 (exp.f64 (*.f64 a eps)) #s(literal 1 binary64)) (-.f64 (exp.f64 (*.f64 b eps)) #s(literal 1 binary64)))underflow237
↳(*.f64 a eps)underflow152
sqrt.f64#fuflow-rescue160
-.f64#fnan-rescue100
exp.f64#fsensitivity30
/.f64(/.f64 (-.f64 #s(literal 1 binary64) (cos.f64 x)) (*.f64 x x))n/o20
↳(*.f64 x x)overflow63
/.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))overflow3
↳(-.f64 (exp.f64 (*.f64 #s(literal 2 binary64) x)) #s(literal 1 binary64))overflow3
↳(exp.f64 x)overflow2
↳(-.f64 (exp.f64 x) #s(literal 1 binary64))overflow2
sin.f64(sin.f64 (+.f64 x eps))sensitivity10
tan.f64(tan.f64 (+.f64 x eps))sensitivity10
cos.f64(cos.f64 (+.f64 x eps))sensitivity10
/.f64(/.f64 (-.f64 (exp.f64 (*.f64 #s(literal 2 binary64) x)) #s(literal 1 binary64)) (-.f64 (exp.f64 x) #s(literal 1 binary64)))o/n10
↳(exp.f64 (*.f64 #s(literal 2 binary64) x))overflow3
↳(-.f64 (exp.f64 (*.f64 #s(literal 2 binary64) x)) #s(literal 1 binary64))overflow3
Confusion
Predicted +Predicted -
+515010
-1651843
Precision
0.9689557855126999
Recall
0.998062015503876
Confusion?
Predicted +Predicted MaybePredicted -
+515073
-165161827
Precision?
0.9660921693518172
Recall?
0.9994186046511628
Freqs
test
numberfreq
01853
14512
2656
397
450
Total Confusion?
Predicted +Predicted MaybePredicted -
+2800
-000
Precision?
1.0
Recall?
1.0
Samples
2.0s2 542×2valid
1.2s5 738×1valid
560.0ms5 846×0valid
222.0ms210×3valid
Compiler

Compiled 2 154 to 763 computations (64.6% saved)

Precisions
Click to see histograms. Total time spent on operations: 3.1s
ival-tan: 790.0ms (25.4% of total)
ival-mult: 463.0ms (14.9% of total)
adjust: 302.0ms (9.7% of total)
ival-log: 219.0ms (7% of total)
ival-sin: 213.0ms (6.8% of total)
ival-cos: 209.0ms (6.7% of total)
ival-div: 180.0ms (5.8% of total)
ival-sub: 166.0ms (5.3% of total)
ival-exp: 127.0ms (4.1% of total)
ival-add: 99.0ms (3.2% of total)
ival-pow: 93.0ms (3% of total)
ival-sqrt: 82.0ms (2.6% of total)
ival-log1p: 55.0ms (1.8% of total)
ival-atan: 38.0ms (1.2% of total)
ival-expm1: 22.0ms (0.7% of total)
ival-cbrt: 15.0ms (0.5% of total)
ival-true: 13.0ms (0.4% of total)
ival-neg: 11.0ms (0.4% of total)
exact: 8.0ms (0.3% of total)
ival-assert: 6.0ms (0.2% of total)

preprocess5.2s (2%)

Memory
432.4MiB live, 5 016.6MiB allocated
Algorithm
28×egg-herbie
Stop Event
56×iter limit
33×saturated
23×node limit
Compiler

Compiled 18 642 to 5 263 computations (71.8% saved)

series4.0s (1.5%)

Memory
-224.9MiB live, 3 914.9MiB allocated
Counts
1 682 → 8 176
Calls

504 calls:

TimeVariablePointExpression
164.0ms
a
@inf
((+ (/ (sqrt (- (* b_2 b_2) (* a c))) a) (/ (neg b_2) a)) (/ (sqrt (- (* b_2 b_2) (* a c))) a) (sqrt (- (* b_2 b_2) (* a c))) (- (* b_2 b_2) (* a c)) (/ (+ (neg b_2) (sqrt (- (* b_2 b_2) (* a c)))) a) (+ (neg b_2) (sqrt (- (* b_2 b_2) (* a c)))) (* -2 b_2) (/ (+ (* (sqrt (- (* b_2 b_2) (* a c))) a) (* a (neg b_2))) (* a a)) (+ (* (sqrt (- (* b_2 b_2) (* a c))) a) (* a (neg b_2))) (sqrt (- (* b_2 b_2) (* a c))) (- (* b_2 b_2) (* a c)) (/ (- (* b_2 b_2) (- (* b_2 b_2) (* a c))) (- (neg b_2) (sqrt (- (* b_2 b_2) (* a c))))) (/ (/ (- (* b_2 b_2) (- (* b_2 b_2) (* a c))) (- (neg b_2) (sqrt (- (* b_2 b_2) (* a c))))) a) (- (* b_2 b_2) (- (* b_2 b_2) (* a c))) (* b_2 b_2) (+ (/ (* b_2 b_2) (* (- (neg b_2) (sqrt (- (* b_2 b_2) (* a c)))) a)) (/ (* (neg (sqrt (- (* b_2 b_2) (* a c)))) (sqrt (- (* b_2 b_2) (* a c)))) (* (- (neg b_2) (sqrt (- (* b_2 b_2) (* a c)))) a))) (* (neg (sqrt (- (* b_2 b_2) (* a c)))) (sqrt (- (* b_2 b_2) (* a c)))) (/ (* (neg (sqrt (- (* b_2 b_2) (* a c)))) (sqrt (- (* b_2 b_2) (* a c)))) (* (- (neg b_2) (sqrt (- (* b_2 b_2) (* a c)))) a)) (/ (* b_2 b_2) (* (- (neg b_2) (sqrt (- (* b_2 b_2) (* a c)))) a)) (* (/ c b_2) a) (* (* (- 1 (/ (* (/ c b_2) a) b_2)) b_2) b_2) (- (neg b_2) (sqrt (- (* b_2 b_2) (* a c)))))
99.0ms
x
@inf
((/ 1 (pow (cbrt x) 2)) (- (cbrt (+ x 1)) (cbrt x)) (* (/ 1 (pow (cbrt x) 2)) 1/3) (pow (cbrt x) 2) (- (cbrt (+ x 1)) (cbrt x)) (* (pow x -2/3) 1/3) (pow x -2/3) (- (cbrt (+ x 1)) (cbrt x)) (* (/ (cbrt (/ -1 x)) (cbrt (neg x))) 1/3) (/ (cbrt (/ -1 x)) (cbrt (neg x))) (cbrt (/ -1 x)) (pow (exp -2) (log (cbrt x))) (- (cbrt (+ x 1)) (cbrt x)) (* (pow (exp -2) (log (cbrt x))) 1/3) (exp -2) (* (pow (/ -1 x) 2) 1/3) (- (cbrt (+ x 1)) (cbrt x)) (* (exp (neg (* (log (cbrt x)) 2))) 1/3) (* (pow (* (cbrt -1) (cbrt (pow x -2))) -2) (* (pow (/ -1 x) 2) 1/3)) (cbrt x) (cbrt (neg x)) (cbrt (pow x -2)) (pow (* (cbrt -1) (cbrt (pow x -2))) -2))
83.0ms
x
@0
((/ 1 (pow (cbrt x) 2)) (- (cbrt (+ x 1)) (cbrt x)) (* (/ 1 (pow (cbrt x) 2)) 1/3) (pow (cbrt x) 2) (- (cbrt (+ x 1)) (cbrt x)) (* (pow x -2/3) 1/3) (pow x -2/3) (- (cbrt (+ x 1)) (cbrt x)) (* (/ (cbrt (/ -1 x)) (cbrt (neg x))) 1/3) (/ (cbrt (/ -1 x)) (cbrt (neg x))) (cbrt (/ -1 x)) (pow (exp -2) (log (cbrt x))) (- (cbrt (+ x 1)) (cbrt x)) (* (pow (exp -2) (log (cbrt x))) 1/3) (exp -2) (* (pow (/ -1 x) 2) 1/3) (- (cbrt (+ x 1)) (cbrt x)) (* (exp (neg (* (log (cbrt x)) 2))) 1/3) (* (pow (* (cbrt -1) (cbrt (pow x -2))) -2) (* (pow (/ -1 x) 2) 1/3)) (cbrt x) (cbrt (neg x)) (cbrt (pow x -2)) (pow (* (cbrt -1) (cbrt (pow x -2))) -2))
79.0ms
x
@inf
((sin (+ (/ (+ (* x 2) eps) 2) (/ (PI) 2))) (+ (/ (+ (* x 2) eps) 2) (/ (PI) 2)) (- (* 1/3840 (* eps eps)) 1/48) (/ (+ (* x 2) eps) 2) (- (sin (+ x eps)) (sin x)) (* (cos x) eps) (+ (* (* (* -1/2 x) x) eps) eps) (* (* -1/2 x) x) (- (* 1/12 (* x eps)) 1/2) (- (sin (+ x eps)) (sin x)) (* (+ (* (* (sin x) eps) -1/2) (cos x)) eps) (+ (* (* (sin x) eps) -1/2) (cos x)) (sin (+ (/ (PI) 2) x)) (- (sin (+ x eps)) (sin x)) (* (sin (+ (/ (PI) 2) x)) eps) (+ (/ (PI) 2) x) (- (sin (+ x eps)) (sin x)) (* (+ (* (+ (* (* (cos x) eps) -1/6) (* (sin x) -1/2)) eps) (cos x)) eps) (+ (* (+ (* (* (cos x) eps) -1/6) (* (sin x) -1/2)) eps) (cos x)) (+ (* (* (cos x) eps) -1/6) (* (sin x) -1/2)) (PI) (* 1/3840 (* eps eps)) (* -1/2 x) (* 1/12 (* x eps)) (+ (* (- (* 1/12 (* x eps)) 1/2) x) (* -1/2 eps)) (* (+ x eps) 1/12) (* -1/6 eps) (* 1/12 x))
71.0ms
x
@-inf
((/ (+ (* (- (pow (log (+ 1 x)) 2) (pow (log x) 2)) n) (* (+ (log (+ 1 x)) (log x)) (* (- (pow (log (+ 1 x)) 2) (pow (log x) 2)) 1/2))) (* (+ (log (+ 1 x)) (log x)) n)) (+ (* (- (pow (log (+ 1 x)) 2) (pow (log x) 2)) n) (* (+ (log (+ 1 x)) (log x)) (* (- (pow (log (+ 1 x)) 2) (pow (log x) 2)) 1/2))) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (/ (/ (+ (* (- (pow (log (+ 1 x)) 2) (pow (log x) 2)) n) (* (+ (log (+ 1 x)) (log x)) (* (- (pow (log (+ 1 x)) 2) (pow (log x) 2)) 1/2))) (* (+ (log (+ 1 x)) (log x)) n)) n) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (/ (exp (/ (log x) n)) (* n x)) (/ (/ 1 n) x) (/ 1 n) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (/ (exp (/ (log x) n)) (* n x)) (/ (- (/ (/ (log x) n) (neg x)) (/ 1 x)) (neg n)) (- (/ (/ (log x) n) (neg x)) (/ 1 x)) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (/ (- (log (+ 1 x)) (log x)) n) (- (log (+ 1 x)) (log x)) (log (+ 1 x)) (+ (* (/ -1/2 n) (/ (pow (log x) 2) n)) (- (/ x n) (/ (log x) n))) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (/ (- (+ (* 1/2 (/ (- (pow (log (+ 1 x)) 2) (pow (log x) 2)) n)) (log (+ 1 x))) (log x)) n) (/ -1/2 n) (- (pow (log (+ 1 x)) 2) (pow (log x) 2)) (pow (log x) 2) (* (+ (log (+ 1 x)) (log x)) (* (- (pow (log (+ 1 x)) 2) (pow (log x) 2)) 1/2)) (/ (/ (log x) n) (neg x)) (/ (log x) n) (log x))

prune3.1s (1.2%)

Memory
385.1MiB live, 4 689.4MiB allocated
Counts
58 371 → 1 592
Compiler

Compiled 86 536 to 45 165 computations (47.8% saved)

regimes2.8s (1.1%)

Memory
-202.0MiB live, 3 455.9MiB allocated
Counts
2 825 → 300
Calls

43 calls:

726.0ms
x
202.0ms
eps
201.0ms
(/.f64 (-.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 #s(literal 4 binary64) (*.f64 a c))))) (*.f64 #s(literal 2 binary64) a))
143.0ms
b
110.0ms
a
Compiler

Compiled 2 131 to 2 006 computations (5.9% saved)

analyze2.5s (0.9%)

Memory
-60.0MiB live, 2 212.9MiB allocated
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.2s (0.4%)

Memory
125.9MiB live, 1 134.9MiB allocated
Algorithm
68×binary-search
25×left-value
Stop Event
62×narrow-enough
6×predicate-same
Samples
324.0ms3 878×0valid
159.0ms481×2valid
137.0ms818×1valid
60.0ms716×0invalid
5.0ms23×3valid
4.0ms43×0exit
Compiler

Compiled 23 966 to 17 955 computations (25.1% saved)

Precisions
Click to see histograms. Total time spent on operations: 499.0ms
ival-pow: 114.0ms (22.9% of total)
ival-mult: 93.0ms (18.6% of total)
ival-div: 65.0ms (13% of total)
adjust: 60.0ms (12% of total)
ival-sub: 43.0ms (8.6% of total)
ival-sqrt: 28.0ms (5.6% of total)
ival-neg: 28.0ms (5.6% of total)
ival-add: 27.0ms (5.4% of total)
ival-cos: 14.0ms (2.8% of total)
ival-cbrt: 7.0ms (1.4% of total)
ival-expm1: 6.0ms (1.2% of total)
ival-true: 4.0ms (0.8% of total)
ival-exp: 3.0ms (0.6% of total)
exact: 3.0ms (0.6% of total)
ival-assert: 2.0ms (0.4% of total)

start1.0ms (0%)

Memory
2.1MiB live, 2.1MiB allocated

end0.0ms (0%)

Memory
0.4MiB live, 0.4MiB allocated

Profiling

Loading profile data...