Herbie run

Date:Wednesday, October 2nd, 2024
Commit:913204d2 on artem-batch-finish-rewrite
Hostname:nightly with Racket 8.10
Seed:2024276
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: 4.5min)

sample2.0min (43.4%)

Memory
810.2MiB live, 115 919.0MiB allocated
Samples
28.2s41 545×2valid
24.9s143 368×0invalid
19.9s92 032×1valid
9.9s4 838×5exit
9.6s94 538×0valid
2.2s3 051×3valid
623.0ms2 354×1exit
448.0ms4 125×0exit
10.0ms4exit
5.0ms3exit
3.0ms2exit
2.0ms4valid
Precisions
Click to see histograms. Total time spent on operations: 1.3min
ival-tan: 12.9s (16.2% of total)
ival-pow: 9.9s (12.5% of total)
ival-mult: 6.8s (8.5% of total)
adjust: 5.4s (6.8% of total)
const: 5.2s (6.6% of total)
ival-div: 4.8s (6% of total)
ival-sub: 4.2s (5.3% of total)
ival-cos: 4.2s (5.3% of total)
ival-add: 3.9s (4.9% of total)
ival-log: 3.5s (4.4% of total)
ival-sin: 3.4s (4.2% of total)
ival-exp: 2.4s (3.1% of total)
ival-expm1: 2.3s (2.9% of total)
ival-fabs: 2.3s (2.9% of total)
ival-<=: 2.0s (2.5% of total)
ival-log1p: 1.2s (1.6% of total)
ival-sqrt: 1.2s (1.5% of total)
ival-<: 1.0s (1.3% of total)
ival-and: 625.0ms (0.8% of total)
ival-fmin: 520.0ms (0.7% of total)
exact: 368.0ms (0.5% of total)
ival-atan: 352.0ms (0.4% of total)
ival-neg: 288.0ms (0.4% of total)
ival-cbrt: 260.0ms (0.3% of total)
ival->: 235.0ms (0.3% of total)
ival-assert: 159.0ms (0.2% of total)
ival-true: 72.0ms (0.1% of total)
Bogosity

simplify34.1s (12.6%)

Memory
457.4MiB live, 30 071.2MiB allocated
Algorithm
238×egg-herbie
Stop Event
315×iter limit
164×node limit
74×saturated
Counts
28 464 → 28 016

soundness27.3s (10.1%)

Memory
171.3MiB live, 15 659.0MiB allocated
Stop Event
185×iter limit
125×node limit
21×fuel
done
saturated
Compiler

Compiled 13 865 to 6 211 computations (55.2% saved)

rewrite21.7s (8%)

Memory
42.6MiB live, 22 019.9MiB allocated
Stop Event
212×iter limit
105×node limit
Counts
1 612 → 67 026

eval21.3s (7.9%)

Memory
138.9MiB live, 27 444.5MiB allocated
Compiler

Compiled 3 978 284 to 305 095 computations (92.3% saved)

localize20.8s (7.6%)

Memory
-211.8MiB live, 21 171.7MiB allocated
Samples
6.6s5 598×2valid
6.1s9 671×1valid
3.0s10 222×0valid
397.0ms1 041×0invalid
311.0ms331×3valid
30.0ms16×5exit
2.0ms4valid
Compiler

Compiled 47 248 to 6 735 computations (85.7% saved)

Precisions
Click to see histograms. Total time spent on operations: 13.2s
ival-mult: 2.0s (14.9% of total)
ival-div: 1.6s (12.3% of total)
adjust: 1.5s (11.6% of total)
ival-add: 1.3s (10% of total)
ival-tan: 1.3s (9.5% of total)
const: 782.0ms (5.9% of total)
ival-pow: 750.0ms (5.7% of total)
ival-sub: 696.0ms (5.3% of total)
ival-cos: 642.0ms (4.9% of total)
ival-log: 426.0ms (3.2% of total)
ival-exp: 392.0ms (3% of total)
ival-sin: 282.0ms (2.1% of total)
ival-sqrt: 280.0ms (2.1% of total)
ival-sinh: 243.0ms (1.8% of total)
ival-pow2: 230.0ms (1.7% of total)
ival-log1p: 178.0ms (1.3% of total)
ival-neg: 169.0ms (1.3% of total)
ival-expm1: 148.0ms (1.1% of total)
exact: 62.0ms (0.5% of total)
ival-cbrt: 51.0ms (0.4% of total)
ival-hypot: 40.0ms (0.3% of total)
ival-atan2: 33.0ms (0.2% of total)
ival-cosh: 30.0ms (0.2% of total)
ival-true: 24.0ms (0.2% of total)
ival-atan: 20.0ms (0.2% of total)
ival-assert: 12.0ms (0.1% of total)
ival-copysign: 11.0ms (0.1% of total)
ival-fabs: 11.0ms (0.1% of total)

explain6.3s (2.3%)

Memory
-97.8MiB live, 6 519.0MiB allocated
Explanations
Click to see full explanations table
OperatorSubexpressionExplanationCount
-.f64#fcancellation424035
log.f64#fsensitivity7612
/.f64#fu/u4220
sqrt.f64#foflow-rescue4060
+.f64#fcancellation3191
/.f64#fu/n1350
pow.f64#fsensitivity710
/.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/u270
(*.f64 b eps)underflow142
(-.f64 (exp.f64 (*.f64 a eps)) #s(literal 1 binary64))underflow152
(-.f64 (exp.f64 (*.f64 b eps)) #s(literal 1 binary64))underflow142
(*.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)underflow152
sqrt.f64#fuflow-rescue240
-.f64#fnan-rescue110
/.f64(/.f64 (-.f64 #s(literal 1 binary64) (cos.f64 x)) (*.f64 x x))n/o50
(*.f64 x x)overflow53
/.f64(/.f64 (-.f64 (exp.f64 (*.f64 #s(literal 2 binary64) x)) #s(literal 1 binary64)) (-.f64 (exp.f64 x) #s(literal 1 binary64)))o/n20
(exp.f64 (*.f64 #s(literal 2 binary64) x))overflow3
(-.f64 (exp.f64 (*.f64 #s(literal 2 binary64) x)) #s(literal 1 binary64))overflow3
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/o10
(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)overflow1
(-.f64 (exp.f64 x) #s(literal 1 binary64))overflow1
sin.f64(sin.f64 (+.f64 x eps))sensitivity10
tan.f64(tan.f64 (+.f64 x eps))sensitivity10
Confusion
Predicted +Predicted -
+527114
-1341749
Precision
0.9752081406105458
Recall
0.9973509933774835
Confusion?
Predicted +Predicted MaybePredicted -
+5271113
-134261723
Precision?
0.9705990444689453
Recall?
0.9994323557237464
Freqs
test
numberfreq
01763
14584
2672
397
452
Total Confusion?
Predicted +Predicted MaybePredicted -
+2800
-000
Precision?
1.0
Recall?
1.0
Samples
1.9s2 632×2valid
1.2s5 740×1valid
541.0ms5 754×0valid
139.0ms210×3valid
Compiler

Compiled 3 034 to 980 computations (67.7% saved)

Precisions
Click to see histograms. Total time spent on operations: 2.9s
ival-tan: 843.0ms (29.1% of total)
ival-div: 380.0ms (13.1% of total)
adjust: 232.0ms (8% of total)
ival-log: 225.0ms (7.8% of total)
ival-cos: 215.0ms (7.4% of total)
ival-sub: 192.0ms (6.6% of total)
ival-sin: 147.0ms (5.1% of total)
ival-exp: 135.0ms (4.7% of total)
ival-mult: 106.0ms (3.7% of total)
ival-pow: 87.0ms (3% of total)
ival-add: 85.0ms (2.9% of total)
ival-log1p: 83.0ms (2.9% of total)
ival-sqrt: 68.0ms (2.3% of total)
ival-expm1: 23.0ms (0.8% of total)
ival-atan: 19.0ms (0.7% of total)
ival-cbrt: 15.0ms (0.5% of total)
ival-neg: 15.0ms (0.5% of total)
ival-true: 13.0ms (0.4% of total)
exact: 9.0ms (0.3% of total)
ival-assert: 6.0ms (0.2% of total)

prune6.2s (2.3%)

Memory
-402.2MiB live, 10 062.1MiB allocated
Counts
110 339 → 1 846
Compiler

Compiled 97 532 to 50 963 computations (47.7% saved)

series4.7s (1.7%)

Memory
22.3MiB live, 5 848.8MiB allocated
Counts
1 612 → 28 464
Calls

489 calls:

TimeVariablePointExpression
105.0ms
x
@inf
((/ (- (* (- (pow (log x) 3) (pow (log (+ 1 x)) 3)) n) (* (+ (* (log (+ 1 x)) (+ (log (+ 1 x)) (log x))) (pow (log x) 2)) (+ (* 1/2 (- (pow (log (+ 1 x)) 2) (pow (log x) 2))) (/ (+ (* -1/6 (- (pow (log (+ 1 x)) 3) (pow (log x) 3))) (* (/ (- (pow (log (+ 1 x)) 4) (pow (log x) 4)) n) -1/24)) (neg n))))) (* (+ (* (log (+ 1 x)) (+ (log (+ 1 x)) (log x))) (pow (log x) 2)) n)) (/ (/ (- (* (- (pow (log x) 3) (pow (log (+ 1 x)) 3)) n) (* (+ (* (log (+ 1 x)) (+ (log (+ 1 x)) (log x))) (pow (log x) 2)) (+ (* 1/2 (- (pow (log (+ 1 x)) 2) (pow (log x) 2))) (/ (+ (* -1/6 (- (pow (log (+ 1 x)) 3) (pow (log x) 3))) (* (/ (- (pow (log (+ 1 x)) 4) (pow (log x) 4)) n) -1/24)) (neg n))))) (* (+ (* (log (+ 1 x)) (+ (log (+ 1 x)) (log x))) (pow (log x) 2)) n)) (neg n)) (- (* (- (pow (log x) 3) (pow (log (+ 1 x)) 3)) n) (* (+ (* (log (+ 1 x)) (+ (log (+ 1 x)) (log x))) (pow (log x) 2)) (+ (* 1/2 (- (pow (log (+ 1 x)) 2) (pow (log x) 2))) (/ (+ (* -1/6 (- (pow (log (+ 1 x)) 3) (pow (log x) 3))) (* (/ (- (pow (log (+ 1 x)) 4) (pow (log x) 4)) n) -1/24)) (neg n))))) (/ (+ (* -1/6 (- (pow (log (+ 1 x)) 3) (pow (log x) 3))) (* (/ (- (pow (log (+ 1 x)) 4) (pow (log x) 4)) n) -1/24)) (neg n)) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n)) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (pow (+ x 1) (/ 1 n)) (+ (/ x n) 1) (/ x n) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (/ (pow x (pow n -1)) (* n x)) (pow x (pow n -1)) (pow n -1) (exp (* (log (/ n (log x))) -1)) (* (log (/ n (log x))) -1) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (- (/ x n) (- (exp (exp (* (log (/ n (log x))) -1))) 1)) (- (pow (log (+ 1 x)) 2) (pow (log x) 2)) (- (pow (log x) 3) (pow (log (+ 1 x)) 3)) (- (pow (log (+ 1 x)) 3) (pow (log x) 3)) (- (pow (log (+ 1 x)) 4) (pow (log x) 4)) (pow x (/ 1 n)) (* n x) (/ n (log x)) (- (exp (exp (* (log (/ n (log x))) -1))) 1))
77.0ms
x
@-inf
((/ (- (* (- (pow (log x) 3) (pow (log (+ 1 x)) 3)) n) (* (+ (* (log (+ 1 x)) (+ (log (+ 1 x)) (log x))) (pow (log x) 2)) (+ (* 1/2 (- (pow (log (+ 1 x)) 2) (pow (log x) 2))) (/ (+ (* -1/6 (- (pow (log (+ 1 x)) 3) (pow (log x) 3))) (* (/ (- (pow (log (+ 1 x)) 4) (pow (log x) 4)) n) -1/24)) (neg n))))) (* (+ (* (log (+ 1 x)) (+ (log (+ 1 x)) (log x))) (pow (log x) 2)) n)) (/ (/ (- (* (- (pow (log x) 3) (pow (log (+ 1 x)) 3)) n) (* (+ (* (log (+ 1 x)) (+ (log (+ 1 x)) (log x))) (pow (log x) 2)) (+ (* 1/2 (- (pow (log (+ 1 x)) 2) (pow (log x) 2))) (/ (+ (* -1/6 (- (pow (log (+ 1 x)) 3) (pow (log x) 3))) (* (/ (- (pow (log (+ 1 x)) 4) (pow (log x) 4)) n) -1/24)) (neg n))))) (* (+ (* (log (+ 1 x)) (+ (log (+ 1 x)) (log x))) (pow (log x) 2)) n)) (neg n)) (- (* (- (pow (log x) 3) (pow (log (+ 1 x)) 3)) n) (* (+ (* (log (+ 1 x)) (+ (log (+ 1 x)) (log x))) (pow (log x) 2)) (+ (* 1/2 (- (pow (log (+ 1 x)) 2) (pow (log x) 2))) (/ (+ (* -1/6 (- (pow (log (+ 1 x)) 3) (pow (log x) 3))) (* (/ (- (pow (log (+ 1 x)) 4) (pow (log x) 4)) n) -1/24)) (neg n))))) (/ (+ (* -1/6 (- (pow (log (+ 1 x)) 3) (pow (log x) 3))) (* (/ (- (pow (log (+ 1 x)) 4) (pow (log x) 4)) n) -1/24)) (neg n)) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n)) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (pow (+ x 1) (/ 1 n)) (+ (/ x n) 1) (/ x n) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (/ (pow x (pow n -1)) (* n x)) (pow x (pow n -1)) (pow n -1) (exp (* (log (/ n (log x))) -1)) (* (log (/ n (log x))) -1) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (- (/ x n) (- (exp (exp (* (log (/ n (log x))) -1))) 1)) (- (pow (log (+ 1 x)) 2) (pow (log x) 2)) (- (pow (log x) 3) (pow (log (+ 1 x)) 3)) (- (pow (log (+ 1 x)) 3) (pow (log x) 3)) (- (pow (log (+ 1 x)) 4) (pow (log x) 4)) (pow x (/ 1 n)) (* n x) (/ n (log x)) (- (exp (exp (* (log (/ n (log x))) -1))) 1))
58.0ms
n
@0
((- (- (log x) (log (+ 1 x))) (/ (+ (* (- (pow (log (+ 1 x)) 2) (pow (log x) 2)) 1/2) (/ (+ (* (- (pow (log (+ 1 x)) 3) (pow (log x) 3)) -1/6) (* -1/24 (/ (- (pow (log (+ 1 x)) 4) (pow (log x) 4)) n))) (neg n))) n)) (/ (+ (* (- (pow (log (+ 1 x)) 3) (pow (log x) 3)) -1/6) (* -1/24 (/ (- (pow (log (+ 1 x)) 4) (pow (log x) 4)) n))) (neg n)) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (- (log x) (log (+ 1 x))) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n)) (/ 1 n) (/ (/ (pow x (/ 1 n)) x) n) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (/ (pow x (/ 1 n)) x) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (- (/ x n) (- (exp (/ (log x) n)) 1)) (/ x n) (- (exp (/ (log x) n)) 1) (- (exp (/ (log (+ 1 x)) n)) (pow x (/ 1 n))) (exp (/ (log (+ 1 x)) n)) (/ (log (+ 1 x)) n) (log (+ 1 x)) (- (pow (log (+ 1 x)) 3) (pow (log x) 3)) (- (pow (log (+ 1 x)) 2) (pow (log x) 2)) (- (pow (log (+ 1 x)) 4) (pow (log x) 4)) (/ (log x) n))
56.0ms
x
@0
((- (cbrt (+ x 1)) (cbrt x)) (* (cbrt (/ (/ 1 x) x)) 1/3) (cbrt (/ (/ 1 x) x)) (/ (/ 1 x) x) (- (cbrt (+ x 1)) (cbrt x)) (cbrt (+ x 1)) (cbrt x) (pow (pow x 1/6) 2) (- (cbrt (+ x 1)) (pow (pow x 1/6) 2)) (cbrt (+ x 1)) (+ x 1) (pow (exp (neg (log (+ 1 x)))) -1/3) (exp (neg (log (+ 1 x)))) (neg (log (+ 1 x))) (log (+ 1 x)) (exp 1) (- (cbrt (pow (exp 1) (log (+ 1 x)))) (cbrt x)) (cbrt (pow (exp 1) (log (+ 1 x)))) (pow (exp 1) (log (+ 1 x))) (pow x 1/6) (- (pow (exp (neg (log (+ 1 x)))) -1/3) (cbrt x)))
51.0ms
x
@-inf
((- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (pow (+ x 1) (/ 1 n)) (+ x 1) (/ 1 n) (pow x (/ 1 n)))

preprocess4.6s (1.7%)

Memory
-485.1MiB live, 4 801.5MiB allocated
Algorithm
28×egg-herbie
Stop Event
56×iter limit
50×saturated
node limit
Compiler

Compiled 17 096 to 5 071 computations (70.3% saved)

regimes3.8s (1.4%)

Memory
-18.2MiB live, 4 714.9MiB allocated
Counts
3 583 → 294
Calls

43 calls:

1.2s
x
294.0ms
eps
175.0ms
b
173.0ms
a
126.0ms
(exp.f64 x)
Compiler

Compiled 2 085 to 1 929 computations (7.5% saved)

analyze1.9s (0.7%)

Memory
81.3MiB live, 1 998.3MiB 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.1s (0.4%)

Memory
-52.1MiB live, 1 377.4MiB allocated
Algorithm
67×binary-search
21×left-value
Stop Event
65×narrow-enough
predicate-same
Samples
396.0ms3 300×0valid
129.0ms602×1valid
69.0ms253×2valid
56.0ms700×0invalid
1.0ms3valid
1.0ms0exit
Compiler

Compiled 20 783 to 16 130 computations (22.4% saved)

Precisions
Click to see histograms. Total time spent on operations: 470.0ms
ival-mult: 129.0ms (27.4% of total)
ival-sub: 96.0ms (20.4% of total)
ival-pow: 76.0ms (16.2% of total)
ival-div: 38.0ms (8.1% of total)
ival-sqrt: 30.0ms (6.4% of total)
adjust: 24.0ms (5.1% of total)
ival-add: 19.0ms (4% of total)
ival-neg: 19.0ms (4% of total)
ival-cos: 13.0ms (2.8% of total)
ival-cbrt: 6.0ms (1.3% of total)
ival-sin: 6.0ms (1.3% of total)
ival-true: 4.0ms (0.9% of total)
ival-expm1: 3.0ms (0.6% of total)
exact: 3.0ms (0.6% of total)
ival-exp: 2.0ms (0.4% of total)
ival-assert: 2.0ms (0.4% of total)

start1.0ms (0%)

Memory
1.9MiB live, 1.8MiB allocated

end0.0ms (0%)

Memory
0.4MiB live, 0.3MiB allocated

Profiling

Loading profile data...