Herbie run

Date:Wednesday, August 21st, 2024
Commit:1d8733fd on artem-batch-taylor
Hostname:nightly with Racket 8.11.1
Seed:2024234
Parameters:256 points for 4 iterations
Flags:
localize:costslocalize:errorsreduce:regimesreduce:avg-errorreduce:binary-searchreduce:branch-expressionssetup:simplifysetup:searchrules:arithmeticrules:polynomialsrules:fractionsrules:exponentsrules:trigonometryrules:hyperbolicrules:numericsrules:specialrules:boolsrules:branchesgenerate:rrgenerate:taylorgenerate:simplifygenerate:proofs
default

Time bar (total: 5.2min)

sample1.9min (36.3%)

Memory
368.2MiB live, 119 622.4MiB allocated
Samples
29.8s41 483×2valid
23.5s143 925×0invalid
18.9s92 055×1valid
9.4s4 898×5exit
8.9s94 623×0valid
2.2s3 006×3valid
447.0ms2 268×1exit
325.0ms4 267×0exit
30.0ms7×4exit
12.0ms5×3exit
2.0ms3×2exit
1.0ms1×4valid
Precisions
Click to see histograms. Total time spent on operations: 1.3min
ival-tan: 13.6s (17.3% of total)
ival-pow: 9.3s (11.9% of total)
ival-mult: 6.6s (8.4% of total)
adjust: 5.7s (7.3% of total)
const: 5.1s (6.5% of total)
ival-cos: 4.7s (6% of total)
ival-div: 4.1s (5.3% of total)
ival-add: 3.8s (4.8% of total)
ival-sub: 3.7s (4.7% of total)
ival-sin: 3.7s (4.7% of total)
ival-log: 3.1s (4% of total)
ival-exp: 2.3s (3% of total)
ival-fabs: 2.2s (2.8% of total)
ival-<=: 2.1s (2.7% of total)
ival-expm1: 2.0s (2.5% of total)
ival-sqrt: 1.4s (1.8% of total)
ival-log1p: 1.0s (1.3% of total)
ival-<: 876.0ms (1.1% of total)
ival-and: 603.0ms (0.8% of total)
ival-fmin: 564.0ms (0.7% of total)
ival-atan: 364.0ms (0.5% of total)
exact: 344.0ms (0.4% of total)
ival-neg: 292.0ms (0.4% of total)
ival-cbrt: 268.0ms (0.3% of total)
ival->: 252.0ms (0.3% of total)
ival-assert: 154.0ms (0.2% of total)
ival-true: 69.0ms (0.1% of total)
Bogosity

simplify54.4s (17.3%)

Memory
574.5MiB live, 57 257.2MiB allocated
Algorithm
246×egg-herbie
Rules
2 153 612×lower-fma.f32
2 153 016×lower-fma.f64
758 748×lower-*.f32
757 712×lower-*.f64
471 024×lower-+.f32
Stop Event
324×iter limit
171×node limit
78×saturated
Counts
29 472 → 28 998

rewrite36.0s (11.4%)

Memory
-236.7MiB live, 40 387.0MiB allocated
Rules
482 124×lower-fma.f32
481 528×lower-fma.f64
441 862×lower-*.f32
440 834×lower-*.f64
401 628×lower-/.f32
Stop Event
219×iter limit
108×node limit
3×saturated
Counts
1 703 → 61 986

soundness29.4s (9.3%)

Memory
165.0MiB live, 17 871.5MiB allocated
Rules
1 082 036×lower-fma.f32
1 081 772×lower-fma.f64
551 726×lower-*.f32
551 248×lower-*.f64
310 930×lower-+.f32
Stop Event
188×iter limit
124×node limit
22×fuel
6×done
2×saturated
Compiler

Compiled 10 547 to 5 027 computations (52.3% saved)

localize24.0s (7.6%)

Memory
-483.8MiB live, 26 933.6MiB allocated
Samples
7.8s5 356×2valid
6.8s10 458×1valid
3.2s11 565×0valid
387.0ms371×3valid
118.0ms28×5exit
45.0ms111×0exit
15.0ms15×1exit
Compiler

Compiled 23 955 to 3 414 computations (85.7% saved)

Precisions
Click to see histograms. Total time spent on operations: 14.5s
ival-mult: 2.7s (18.7% of total)
ival-div: 1.7s (11.8% of total)
ival-tan: 1.7s (11.7% of total)
adjust: 1.5s (10.3% of total)
ival-add: 1.4s (9.9% of total)
const: 960.0ms (6.6% of total)
ival-sin: 790.0ms (5.5% of total)
ival-pow: 609.0ms (4.2% of total)
ival-cos: 573.0ms (4% of total)
ival-sub: 560.0ms (3.9% of total)
ival-log: 556.0ms (3.8% of total)
ival-exp: 498.0ms (3.4% of total)
ival-sqrt: 280.0ms (1.9% of total)
ival-log1p: 152.0ms (1% of total)
ival-neg: 89.0ms (0.6% of total)
ival-pow2: 80.0ms (0.6% of total)
ival-expm1: 66.0ms (0.5% of total)
ival-cosh: 59.0ms (0.4% of total)
ival-cbrt: 56.0ms (0.4% of total)
exact: 42.0ms (0.3% of total)
ival-true: 24.0ms (0.2% of total)
ival-atan2: 22.0ms (0.2% of total)
ival-assert: 12.0ms (0.1% of total)
ival-atan: 12.0ms (0.1% of total)
ival-copysign: 3.0ms (0% of total)
ival-fabs: 3.0ms (0% of total)

eval18.1s (5.8%)

Memory
724.9MiB live, 24 561.3MiB allocated
Compiler

Compiled 2 997 767 to 240 645 computations (92% saved)

prune17.0s (5.4%)

Memory
-345.4MiB live, 24 296.5MiB allocated
Counts
106 058 → 2 109
Compiler

Compiled 79 391 to 37 255 computations (53.1% saved)

explain6.0s (1.9%)

Memory
-84.5MiB live, 7 744.6MiB allocated
Explanations
Click to see full explanations table
OperatorSubexpressionExplanationCount
-.f64#fcancellation409337
log.f64#fsensitivity7594
/.f64#fu/u4470
sqrt.f64#foflow-rescue4440
+.f64#fcancellation3421
/.f64#fu/n1210
pow.f64(pow.f64 (+.f64 x #s(literal 1 binary64)) (/.f64 #s(literal 1 binary64) n))sensitivity780
/.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/u250
↳(*.f64 b eps)underflow152
↳(-.f64 (exp.f64 (*.f64 a eps)) #s(literal 1 binary64))underflow140
↳(-.f64 (exp.f64 (*.f64 b eps)) #s(literal 1 binary64))underflow152
↳(*.f64 (-.f64 (exp.f64 (*.f64 a eps)) #s(literal 1 binary64)) (-.f64 (exp.f64 (*.f64 b eps)) #s(literal 1 binary64)))underflow234
↳(*.f64 a eps)underflow140
sqrt.f64#fuflow-rescue180
-.f64#fnan-rescue80
exp.f64(exp.f64 (*.f64 #s(literal 2 binary64) x))sensitivity30
/.f64(/.f64 (-.f64 #s(literal 1 binary64) (cos.f64 x)) (*.f64 x x))n/o20
↳(*.f64 x x)overflow67
/.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
cos.f64(cos.f64 (+.f64 x eps))sensitivity10
Confusion
Predicted +Predicted -
+519215
-1701791
Precision
0.9682954121596419
Recall
0.997119262531208
Confusion?
Predicted +Predicted MaybePredicted -
+5192150
-170251766
Precision?
0.9639022584228064
Recall?
1.0
Freqs
test
numberfreq
01806
14582
2636
387
457
Total Confusion?
Predicted +Predicted MaybePredicted -
+2800
-000
Precision?
1.0
Recall?
1.0
Samples
1.7s2 536×2valid
1.2s5 794×1valid
468.0ms5 818×0valid
132.0ms188×3valid
Compiler

Compiled 2 197 to 763 computations (65.3% saved)

Precisions
Click to see histograms. Total time spent on operations: 2.8s
ival-tan: 762.0ms (27.2% of total)
adjust: 258.0ms (9.2% of total)
ival-sub: 218.0ms (7.8% of total)
ival-log1p: 210.0ms (7.5% of total)
ival-cos: 202.0ms (7.2% of total)
ival-log: 186.0ms (6.6% of total)
ival-mult: 163.0ms (5.8% of total)
ival-sin: 158.0ms (5.6% of total)
ival-exp: 148.0ms (5.3% of total)
ival-div: 142.0ms (5.1% of total)
ival-add: 109.0ms (3.9% of total)
ival-pow: 85.0ms (3% of total)
ival-sqrt: 58.0ms (2.1% of total)
ival-atan: 24.0ms (0.9% of total)
ival-expm1: 24.0ms (0.9% of total)
ival-cbrt: 16.0ms (0.6% of total)
ival-neg: 13.0ms (0.5% of total)
ival-true: 12.0ms (0.4% of total)
exact: 8.0ms (0.3% of total)
ival-assert: 6.0ms (0.2% of total)

preprocess4.7s (1.5%)

Memory
88.1MiB live, 5 332.9MiB allocated
Algorithm
28×egg-herbie
Rules
27 478×lower-fma.f64
27 478×lower-fma.f32
10 768×div-sub
10 444×sub-neg
9 190×lower-*.f32
Stop Event
56×iter limit
50×saturated
6×node limit
Compiler

Compiled 11 453 to 3 917 computations (65.8% saved)

regimes4.4s (1.4%)

Memory
-93.0MiB live, 5 655.1MiB allocated
Counts
4 125 → 329
Calls

43 calls:

1.2s
x
385.0ms
eps
231.0ms
N
168.0ms
a
167.0ms
(/.f64 (-.f64 #s(literal 1 binary64) (cos.f64 x)) (*.f64 x x))
Compiler

Compiled 3 114 to 2 071 computations (33.5% saved)

series3.6s (1.1%)

Memory
55.3MiB live, 4 559.3MiB allocated
Counts
1 703 → 29 472
Calls

504 calls:

TimeVariablePointExpression
85.0ms
x
@0
((- (cbrt (+ x 1)) (cbrt x)) (* 1/3 (cbrt (/ 1 (* x x)))) (cbrt (/ 1 (* x x))) (/ 1 (* x x)) (- (cbrt (+ x 1)) (cbrt x)) (cbrt (+ x 1)) (cbrt x) (- (/ 1 (cbrt (/ 1 (+ x 1)))) (cbrt x)) (/ 1 (cbrt (/ 1 (+ x 1)))) (cbrt (/ 1 (+ x 1))) (/ 1 (+ x 1)) (+ (* (pow x 1/6) (neg (pow x 1/6))) (cbrt (+ x 1))) (pow x 1/6) (neg (pow x 1/6)) (cbrt (+ x 1)) (- (cbrt (+ (* (pow x 5/6) (pow x 1/6)) 1)) (cbrt x)) (cbrt (+ (* (pow x 5/6) (pow x 1/6)) 1)) (+ (* (pow x 5/6) (pow x 1/6)) 1) (pow x 5/6))
84.0ms
n
@0
((log (+ n 1)) (- (- (* (+ n 1) (log (+ n 1))) (* n (log n))) 1) (- (* (+ n 1) (log (+ n 1))) (* n (log n))) (* (+ n 1) (log (+ n 1))) (* n (log n)))
75.0ms
x
@-inf
((/ (/ (- x (+ 1 x)) (+ 1 x)) x) (/ (- x (+ 1 x)) (+ 1 x)) (- x (+ 1 x)) (+ 1 x) (/ (/ (- x (+ 1 x)) (+ 1 x)) x) (* (+ -1 x) (+ x (/ 1 x))) (+ -1 x) (+ x (/ 1 x)) (/ (/ (- x (+ 1 x)) (+ 1 x)) x) (/ (- x (+ 1 x)) (+ 1 x)) (/ -1 x) (- x (+ x 1)) (/ (- x (+ x 1)) (+ (* x x) x)) (+ x 1) (+ (* x x) x) (/ (- 1 (* x x)) (* (* x (* x x)) (+ 1 x))) (* (* x (* x x)) (+ 1 x)) (- (/ 1 (+ x 1)) (/ 1 x)) (- 1 (* x x)) (* x (* x x)))
64.0ms
x
@-inf
((* eps (+ 1/2 (/ x eps))) (+ eps 0) (* (* (sin (* (+ eps 0) 1/2)) (cos (* (+ (* x 2) eps) 1/2))) 2) (* (sin (* (+ eps 0) 1/2)) (cos (* (+ (* x 2) eps) 1/2))) (- (sin (+ x eps)) (sin x)) (* eps (+ (* eps (* -1/2 (sin x))) (* (+ (* eps (* eps -1/6)) 1) (cos x)))) (+ (* eps (* -1/6 (* eps eps))) eps) (* -1/6 (* eps eps)) (+ (* x (+ -1/2 (* (* eps 1/12) (+ x eps)))) (* eps -1/2)) (+ -1/2 (* (* eps 1/12) (+ x eps))) (- (sin (+ x eps)) (sin x)) (* eps (+ (* eps (* -1/2 (sin x))) (* (+ (* eps (* eps -1/6)) 1) (cos x)))) (- (sin (+ x eps)) (sin x)) (* eps (+ (* eps (* -1/2 (sin x))) (* (+ (* eps (* eps -1/6)) 1) (cos x)))) (+ (* eps (* -1/2 (sin x))) (* (+ (* eps (* eps -1/6)) 1) (cos x))) (* -1/2 (sin x)) (* (+ (* x 2) eps) 1/2) (* (* (sin (* (+ eps 0) 1/2)) (cos (* (+ (* x 2) eps) 1/2))) 2) (* (sin (* (+ eps 0) 1/2)) (cos (* (+ (* x 2) eps) 1/2))) (sin (* (+ eps 0) 1/2)) (cos (* (+ (* x 2) eps) 1/2)) (+ 1/2 (/ x eps)) (* eps eps) (+ (* eps (* -1/2 (sin x))) (* (+ (* eps (* eps -1/6)) 1) (cos x))) (* eps -1/6) (* eps 1/12) (* (* eps 1/12) (+ x eps)) (* eps (+ (* (* eps eps) -1/645120) 1/3840)) (cos (* (+ (* x 2) eps) 1/2)) (+ (* eps (* eps (+ (* (* eps eps) -1/645120) 1/3840))) -1/48))
59.0ms
x
@-inf
((+ (- (/ 1 (+ x 1)) (/ 2 x)) (/ 1 (- x 1))) (/ (+ 2 (/ (+ 2 (/ 2 (* x x))) (* x x))) (* x (* x x))) (+ 2 (/ (+ 2 (/ 2 (* x x))) (* x x))) (/ (+ 2 (/ 2 (* x x))) (* x x)) (+ (- (/ 1 (+ x 1)) (/ 2 x)) (/ 1 (- x 1))) (/ -2 x) (+ (- (/ 1 (+ x 1)) (/ 2 x)) (/ 1 (- x 1))) (/ (+ 2 (/ 2 (* x x))) (* x (* x x))) (+ 2 (/ 2 (* x x))) (/ 2 (* x x)) (- x (* (+ 1 x) 2)) (+ (* (- x (* (+ 1 x) 2)) (/ 1 (* x (+ 1 x)))) (/ 1 (+ x -1))) (* (+ 1 x) 2) (* x (+ 1 x)) (+ (* 1 (* x (+ 1 x))) (* (+ x -1) (- x (* (+ 1 x) 2)))) (* (+ x -1) (* x (+ 1 x))) (* x (* x x)) (/ 1 (* x (+ 1 x))) (/ (+ (* 1 (* x (+ 1 x))) (* (+ x -1) (- x (* (+ 1 x) 2)))) (* (+ x -1) (* x (+ 1 x)))))

analyze1.7s (0.5%)

Memory
63.2MiB live, 2 063.0MiB 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)

bsearch943.0ms (0.3%)

Memory
-68.8MiB live, 1 022.5MiB allocated
Algorithm
64×binary-search
44×left-value
Stop Event
62×narrow-enough
2×predicate-same
Samples
441.0ms4 094×0valid
70.0ms222×2valid
53.0ms648×0invalid
51.0ms292×1valid
2.0ms24×0exit
0.0ms1×1exit
Compiler

Compiled 14 271 to 9 619 computations (32.6% saved)

Precisions
Click to see histograms. Total time spent on operations: 438.0ms
ival-cos: 119.0ms (27.2% of total)
ival-pow: 71.0ms (16.2% of total)
ival-mult: 67.0ms (15.3% of total)
ival-div: 57.0ms (13% of total)
ival-sub: 33.0ms (7.5% of total)
ival-sqrt: 24.0ms (5.5% of total)
ival-add: 16.0ms (3.7% of total)
adjust: 15.0ms (3.4% of total)
ival-neg: 14.0ms (3.2% of total)
ival-expm1: 6.0ms (1.4% of total)
ival-sin: 6.0ms (1.4% of total)
ival-true: 4.0ms (0.9% of total)
ival-exp: 3.0ms (0.7% of total)
exact: 3.0ms (0.7% of total)
ival-assert: 2.0ms (0.5% of total)

start0.0ms (0%)

Memory
1.0MiB live, 1.0MiB allocated

end0.0ms (0%)

Memory
0.4MiB live, 0.4MiB allocated

Profiling

Loading profile data...