Herbie run

Date:Sunday, December 29th, 2024
Commit:fbbe2c7d on main
Seed:2024364
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:241 869.3 MB

Time bar (total: 4.5min)

sample2.1min (47.1%)

Memory
657.3MiB live, 117 957.6MiB allocated; 38.2s collecting garbage
Samples
29.3s43 862×2valid
24.2s148 999×0invalid
21.4s96 553×1valid
17.8s7 075×5exit
8.0s87 361×0valid
2.9s3 389×3valid
332.0ms4 263×0exit
4.0ms4valid
Precisions
Click to see histograms. Total time spent on operations: 1.5min
ival-pow: 16.9s (19.3% of total)
ival-tan: 12.9s (14.7% of total)
adjust: 8.7s (10% of total)
ival-mult: 6.5s (7.4% of total)
const: 5.3s (6.1% of total)
ival-cos: 4.4s (5.1% of total)
ival-div: 4.3s (4.9% of total)
ival-log: 3.9s (4.4% of total)
ival-sub: 3.7s (4.2% of total)
ival-sin: 3.3s (3.8% of total)
ival-add: 3.0s (3.4% of total)
ival-<=: 2.4s (2.8% of total)
ival-exp: 2.3s (2.6% of total)
ival-fabs: 2.1s (2.4% of total)
ival-expm1: 1.8s (2% of total)
ival-sqrt: 1.3s (1.5% of total)
ival-log1p: 1.2s (1.4% of total)
ival-<: 724.0ms (0.8% of total)
ival-and: 627.0ms (0.7% of total)
ival-fmin: 484.0ms (0.6% of total)
ival-neg: 357.0ms (0.4% of total)
exact: 347.0ms (0.4% of total)
ival-atan: 331.0ms (0.4% of total)
ival->: 257.0ms (0.3% of total)
ival-cbrt: 232.0ms (0.3% of total)
ival-assert: 161.0ms (0.2% of total)
ival-true: 69.0ms (0.1% of total)
Bogosity

simplify34.9s (13%)

Memory
302.9MiB live, 28 740.2MiB allocated; 7.3s collecting garbage
Stop Event
328×iter limit
219×node limit
27×saturated
Counts
8 925 → 8 828

localize25.5s (9.5%)

Memory
341.0MiB live, 23 241.2MiB allocated; 5.3s collecting garbage
Samples
9.0s6 009×2valid
8.5s10 958×1valid
2.9s10 150×0valid
886.0ms487×3valid
126.0ms56×5exit
84.0ms142×0invalid
75.0ms78×0exit
36.0ms24×1exit
Compiler

Compiled 23 145 to 3 478 computations (85% saved)

Precisions
Click to see histograms. Total time spent on operations: 17.7s
adjust: 3.7s (21.1% of total)
ival-mult: 2.6s (14.6% of total)
ival-tan: 2.5s (14.3% of total)
ival-div: 1.5s (8.6% of total)
ival-add: 1.0s (5.7% of total)
ival-sub: 973.0ms (5.5% of total)
ival-log: 971.0ms (5.5% of total)
ival-pow: 880.0ms (5% of total)
ival-sin: 806.0ms (4.5% of total)
const: 674.0ms (3.8% of total)
ival-cos: 555.0ms (3.1% of total)
ival-exp: 318.0ms (1.8% of total)
ival-sqrt: 269.0ms (1.5% of total)
ival-neg: 225.0ms (1.3% of total)
ival-log1p: 196.0ms (1.1% of total)
ival-pow2: 128.0ms (0.7% of total)
ival-cosh: 55.0ms (0.3% of total)
ival-cbrt: 55.0ms (0.3% of total)
ival-expm1: 52.0ms (0.3% of total)
exact: 45.0ms (0.3% of total)
ival-pi: 23.0ms (0.1% of total)
ival-true: 22.0ms (0.1% of total)
ival-hypot: 19.0ms (0.1% of total)
ival-atan2: 13.0ms (0.1% of total)
ival-assert: 12.0ms (0.1% of total)
ival-atan: 10.0ms (0.1% of total)
ival-fabs: 10.0ms (0.1% of total)
ival-sinh: 7.0ms (0% of total)
ival->: 1.0ms (0% of total)
ival-then: 0.0ms (0% of total)

rewrite22.6s (8.4%)

Memory
194.8MiB live, 20 610.7MiB allocated; 5.4s collecting garbage
Stop Event
221×iter limit
109×node limit
Counts
1 731 → 49 663

derivations22.6s (8.4%)

Memory
454.1MiB live, 12 890.6MiB allocated; 2.0s collecting garbage
Stop Event
204×iter limit
139×node limit
25×fuel
done
Compiler

Compiled 7 824 to 2 020 computations (74.2% saved)

eval11.4s (4.2%)

Memory
-761.9MiB live, 12 129.0MiB allocated; 6.0s collecting garbage
Compiler

Compiled 2 282 853 to 242 159 computations (89.4% saved)

explain6.1s (2.3%)

Memory
-41.7MiB live, 6 444.5MiB allocated; 1.2s collecting garbage
Explanations
Click to see full explanations table
OperatorSubexpressionExplanationCount
-.f64#fcancellation412440
log.f64#fsensitivity7633
/.f64#fu/u4420
sqrt.f64#foflow-rescue3840
+.f64#fcancellation3421
/.f64#fu/n1080
pow.f64(pow.f64 (+.f64 x #s(literal 1 binary64)) (/.f64 #s(literal 1 binary64) n))sensitivity640
/.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/u210
(*.f64 b eps)underflow142
(-.f64 (exp.f64 (*.f64 a eps)) #s(literal 1 binary64))underflow145
(-.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)))underflow227
(*.f64 a eps)underflow145
sqrt.f64#fuflow-rescue200
-.f64#fnan-rescue190
cos.f64(cos.f64 (+.f64 x eps))sensitivity80
tan.f64(tan.f64 (+.f64 x eps))sensitivity71
sin.f64(sin.f64 (+.f64 x eps))sensitivity61
exp.f64(exp.f64 (neg.f64 x))sensitivity32
/.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
Confusion
Predicted +Predicted -
+521622
-1161814
Precision
0.978244561140285
Recall
0.9957999236349752
Confusion?
Predicted +Predicted MaybePredicted -
+5216184
-116281786
Precision?
0.973224246931945
Recall?
0.9992363497518136
Freqs
test
numberfreq
01836
14553
2629
396
454
Total Confusion?
Predicted +Predicted MaybePredicted -
+2800
-000
Precision?
1.0
Recall?
1.0
Samples
1.9s2 764×2valid
1.3s6 044×1valid
479.0ms5 328×0valid
169.0ms200×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: 881.0ms (28.7% of total)
adjust: 444.0ms (14.5% of total)
ival-log: 259.0ms (8.4% of total)
ival-cos: 226.0ms (7.4% of total)
ival-sin: 183.0ms (6% of total)
ival-div: 172.0ms (5.6% of total)
ival-sub: 165.0ms (5.4% of total)
ival-exp: 145.0ms (4.7% of total)
ival-pow: 143.0ms (4.7% of total)
ival-add: 107.0ms (3.5% of total)
ival-mult: 98.0ms (3.2% of total)
ival-log1p: 62.0ms (2% of total)
ival-sqrt: 56.0ms (1.8% of total)
ival-cbrt: 37.0ms (1.2% of total)
ival-expm1: 27.0ms (0.9% of total)
ival-atan: 24.0ms (0.8% of total)
ival-neg: 15.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)

preprocess5.0s (1.9%)

Memory
316.3MiB live, 4 223.7MiB allocated; 792ms collecting garbage
Stop Event
56×iter limit
33×saturated
23×node limit
Compiler

Compiled 18 262 to 5 601 computations (69.3% saved)

series3.9s (1.5%)

Memory
83.9MiB live, 3 854.8MiB allocated; 736ms collecting garbage
Counts
1 731 → 8 925
Calls

507 calls:

TimeVariablePointExpression
149.0ms
b_2
@-inf
((* (- 1 (* (/ (/ c b_2) b_2) a)) b_2) (* (* (- 1 (* (/ (/ c b_2) b_2) a)) b_2) b_2) (/ (- (neg b_2) (sqrt (- (* b_2 b_2) (* a c)))) a) (- (neg b_2) (sqrt (- (* b_2 b_2) (* a c)))) (/ (- (neg b_2) (sqrt (- (* b_2 b_2) (* a c)))) a) (* -1/2 (/ c b_2)) (/ c b_2) (/ (- (neg b_2) (sqrt (- (* b_2 b_2) (* a c)))) a) (- (neg b_2) (sqrt (- (* b_2 b_2) (* a c)))) (neg b_2) (sqrt (- (* 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)))) (sqrt (- (* b_2 b_2) (* a c))) (/ (- (neg b_2) (pow (pow (+ (* c a) (* b_2 b_2)) 2) 1/4)) a) (- (neg b_2) (pow (pow (+ (* c a) (* b_2 b_2)) 2) 1/4)) (pow (pow (+ (* c a) (* b_2 b_2)) 2) 1/4) (sqrt (- (* b_2 b_2) (* a c))) (* (/ (/ c b_2) b_2) a) (- (* b_2 b_2) (* a c)) (- (* b_2 b_2) (* a c)) (+ (* c a) (* b_2 b_2)))
90.0ms
b_2
@0
((/ (+ (* (pow (- (* b_2 b_2) (* a c)) 1/8) (sqrt (pow (- (* b_2 b_2) (* a c)) 3/4))) (neg b_2)) a) (+ (* (pow (- (* b_2 b_2) (* a c)) 1/8) (sqrt (pow (- (* b_2 b_2) (* a c)) 3/4))) (neg b_2)) (pow (- (* b_2 b_2) (* a c)) 1/8) (- (* b_2 b_2) (* a c)) (/ (+ (* (sqrt (sqrt (- (* b_2 b_2) (* a c)))) (sqrt (sqrt (- (* b_2 b_2) (* a c))))) (neg b_2)) a) (+ (* (sqrt (sqrt (- (* b_2 b_2) (* a c)))) (sqrt (sqrt (- (* b_2 b_2) (* a c))))) (neg b_2)) (* -2 b_2) (* (+ (* (/ (/ c b_2) b_2) -1/2) (/ 2 a)) (neg b_2)) (/ (+ (neg b_2) (sqrt (- (* b_2 b_2) (* a c)))) a) (+ (* (/ (/ c b_2) b_2) -1/2) (/ 2 a)) (/ (/ c b_2) b_2) (+ (* (* (/ (* c c) b_2) (/ a (* b_2 b_2))) -1/8) (* (/ c b_2) -1/2)) (* (/ (* c c) b_2) (/ a (* b_2 b_2))) (/ (+ (neg b_2) (sqrt (- (* b_2 b_2) (* a c)))) a) (/ (* c c) b_2) (/ (+ (* (sqrt (sqrt (- (* b_2 b_2) (* a c)))) (sqrt (sqrt (- (* b_2 b_2) (* a c))))) (neg b_2)) a) (+ (* (sqrt (sqrt (- (* b_2 b_2) (* a c)))) (sqrt (sqrt (- (* b_2 b_2) (* a c))))) (neg b_2)) (sqrt (sqrt (- (* b_2 b_2) (* a c)))) (sqrt (- (* b_2 b_2) (* a c))) (sqrt (pow (- (* b_2 b_2) (* a c)) 3/4)) (pow (- (* b_2 b_2) (* a c)) 3/4) (/ a (* b_2 b_2)) (sqrt (- (* b_2 b_2) (* a c))) (* (/ c b_2) a))
75.0ms
a
@0
((/ (+ (* (pow (- (* b_2 b_2) (* a c)) 1/8) (sqrt (pow (- (* b_2 b_2) (* a c)) 3/4))) (neg b_2)) a) (+ (* (pow (- (* b_2 b_2) (* a c)) 1/8) (sqrt (pow (- (* b_2 b_2) (* a c)) 3/4))) (neg b_2)) (pow (- (* b_2 b_2) (* a c)) 1/8) (- (* b_2 b_2) (* a c)) (/ (+ (* (sqrt (sqrt (- (* b_2 b_2) (* a c)))) (sqrt (sqrt (- (* b_2 b_2) (* a c))))) (neg b_2)) a) (+ (* (sqrt (sqrt (- (* b_2 b_2) (* a c)))) (sqrt (sqrt (- (* b_2 b_2) (* a c))))) (neg b_2)) (* -2 b_2) (* (+ (* (/ (/ c b_2) b_2) -1/2) (/ 2 a)) (neg b_2)) (/ (+ (neg b_2) (sqrt (- (* b_2 b_2) (* a c)))) a) (+ (* (/ (/ c b_2) b_2) -1/2) (/ 2 a)) (/ (/ c b_2) b_2) (+ (* (* (/ (* c c) b_2) (/ a (* b_2 b_2))) -1/8) (* (/ c b_2) -1/2)) (* (/ (* c c) b_2) (/ a (* b_2 b_2))) (/ (+ (neg b_2) (sqrt (- (* b_2 b_2) (* a c)))) a) (/ (* c c) b_2) (/ (+ (* (sqrt (sqrt (- (* b_2 b_2) (* a c)))) (sqrt (sqrt (- (* b_2 b_2) (* a c))))) (neg b_2)) a) (+ (* (sqrt (sqrt (- (* b_2 b_2) (* a c)))) (sqrt (sqrt (- (* b_2 b_2) (* a c))))) (neg b_2)) (sqrt (sqrt (- (* b_2 b_2) (* a c)))) (sqrt (- (* b_2 b_2) (* a c))) (sqrt (pow (- (* b_2 b_2) (* a c)) 3/4)) (pow (- (* b_2 b_2) (* a c)) 3/4) (/ a (* b_2 b_2)) (sqrt (- (* b_2 b_2) (* a c))) (* (/ c b_2) a))
62.0ms
a
@inf
((/ (* eps (- (exp (* (+ a b) eps)) 1)) (* (- (exp (* a eps)) 1) (- (exp (* b eps)) 1))) (/ 1 a) (/ (* eps (- (exp (* (+ a b) eps)) 1)) (* (- (exp (* a eps)) 1) (- (exp (* b eps)) 1))) (/ 1 b) (/ (* eps (- (exp (* (+ a b) eps)) 1)) (* (- (exp (* a eps)) 1) (- (exp (* b eps)) 1))) (/ (/ (+ b a) b) a) (/ (+ b a) b) (+ b a) (/ (+ (* (* eps (+ -1/2 (/ (pow (exp a) eps) (- (exp (* eps a)) 1)))) b) 1) b) (/ (* eps (- (exp (* (+ a b) eps)) 1)) (* (- (exp (* a eps)) 1) (- (exp (* b eps)) 1))) (+ (* (* eps (+ -1/2 (/ (pow (exp a) eps) (- (exp (* eps a)) 1)))) b) 1) (* eps (+ -1/2 (/ (pow (exp a) eps) (- (exp (* eps a)) 1)))) (/ (pow (exp a) eps) (- (exp (* eps a)) 1)))
56.0ms
x
@inf
((/ (+ (* -1/24 (/ (- (pow (log (+ 1 x)) 4) (pow (log x) 4)) n)) (* (- (pow (log (+ 1 x)) 3) (pow (log x) 3)) -1/6)) (neg n)) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (/ (+ (- (neg (log (+ 1 x))) (/ (+ (* (- (pow (log (+ 1 x)) 2) (pow (log x) 2)) 1/2) (/ (+ (* -1/24 (/ (- (pow (log (+ 1 x)) 4) (pow (log x) 4)) n)) (* (- (pow (log (+ 1 x)) 3) (pow (log x) 3)) -1/6)) (neg n))) n)) (log x)) (neg n)) (+ (- (neg (log (+ 1 x))) (/ (+ (* (- (pow (log (+ 1 x)) 2) (pow (log x) 2)) 1/2) (/ (+ (* -1/24 (/ (- (pow (log (+ 1 x)) 4) (pow (log x) 4)) n)) (* (- (pow (log (+ 1 x)) 3) (pow (log x) 3)) -1/6)) (neg n))) n)) (log x)) (- (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)) x) n) (/ (exp (/ (log x) n)) x) (exp (/ (log x) n)) (+ (* (+ (* (neg x) (- (/ 1/2 n) (/ 1/2 (* n n)))) (/ 1 n)) x) (/ (neg (+ (* (/ (pow (log x) 2) n) 1/2) (log x))) n)) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (/ (neg (+ (* 1/2 (/ (- (pow (log (+ 1 x)) 2) (pow (log x) 2)) n)) (- (log (+ 1 x)) (log x)))) (neg n)) (+ (* (neg x) (- (/ 1/2 n) (/ 1/2 (* n n)))) (/ 1 n)) (* (/ (/ 2 n) 4) 4) (/ (/ 2 n) 4) (pow (pow x (pow n -1)) 2) (/ (- (pow (+ 1 x) (* (/ (/ 2 n) 4) 4)) (pow (pow x (pow n -1)) 2)) (+ (pow (pow (+ 1 x) 2) (/ (/ 2 n) 4)) (pow x (pow n -1)))) (- (pow (log (+ 1 x)) 4) (pow (log x) 4)) (- (pow (log (+ 1 x)) 3) (pow (log x) 3)) (- (pow (log (+ 1 x)) 2) (pow (log x) 2)) (/ (log x) n) (/ 1/2 (* n n)) (- (pow (+ 1 x) (* (/ (/ 2 n) 4) 4)) (pow (pow x (pow n -1)) 2)) (pow (pow (+ 1 x) 2) (/ (/ 2 n) 4)) (pow (+ 1 x) (* (/ (/ 2 n) 4) 4)))

prune3.3s (1.2%)

Memory
-12.4MiB live, 4 876.4MiB allocated; 666ms collecting garbage
Counts
59 203 → 1 831
Compiler

Compiled 103 105 to 54 395 computations (47.2% saved)

regimes3.2s (1.2%)

Memory
-11.8MiB live, 3 970.8MiB allocated; 523ms collecting garbage
Counts
3 709 → 302
Calls

43 calls:

864.0ms
x
365.0ms
eps
132.0ms
(-.f64 (tan.f64 (+.f64 x eps)) (tan.f64 x))
131.0ms
n
115.0ms
b
Compiler

Compiled 2 285 to 2 124 computations (7% saved)

analyze2.2s (0.8%)

Memory
49.5MiB live, 2 006.6MiB allocated; 1.2s collecting garbage
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)

bsearch908.0ms (0.3%)

Memory
-71.4MiB live, 921.3MiB allocated; 119ms collecting garbage
Algorithm
69×binary-search
15×left-value
Stop Event
64×narrow-enough
predicate-same
Samples
326.0ms4 110×0valid
79.0ms572×1valid
77.0ms776×0invalid
60.0ms228×2valid
1.0ms15×0exit
1.0ms3valid
Compiler

Compiled 23 219 to 17 617 computations (24.1% saved)

Precisions
Click to see histograms. Total time spent on operations: 367.0ms
ival-mult: 91.0ms (24.8% of total)
ival-neg: 46.0ms (12.5% of total)
ival-div: 41.0ms (11.2% of total)
ival-sub: 35.0ms (9.5% of total)
ival-sqrt: 32.0ms (8.7% of total)
adjust: 29.0ms (7.9% of total)
ival-pow: 29.0ms (7.9% of total)
ival-add: 25.0ms (6.8% of total)
ival-cos: 10.0ms (2.7% of total)
ival-expm1: 8.0ms (2.2% of total)
ival-exp: 6.0ms (1.6% of total)
ival-cbrt: 5.0ms (1.4% of total)
ival-true: 4.0ms (1.1% of total)
exact: 3.0ms (0.8% of total)
ival-assert: 2.0ms (0.5% of total)
ival-tan: 1.0ms (0.3% of total)

start1.0ms (0%)

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

end0.0ms (0%)

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

Profiling

Loading profile data...