Herbie run

Date:Tuesday, April 1st, 2025
Commit:7427b81e on no-initial-simplify
Seed:2025091
Parameters:256 points for 4 iterations
Flags:
reduce:regimesreduce:binary-searchreduce:branch-expressionsreduce:simplifysetup:searchrules:arithmeticrules:polynomialsrules:fractionsrules:exponentsrules:trigonometryrules:hyperbolicrules:numericsrules:specialrules:boolsrules:branchesgenerate:rrgenerate:taylorgenerate:simplifygenerate:proofs
default
Memory:78 484.6 MB

Time bar (total: 1.4min)

sample42.2s (51.8%)

Memory
769.2MiB live, 41 526.4MiB allocated; 11.2s collecting garbage
Samples
11.6s16 548×5exit
8.4s39 780×1valid
7.3s108 429×0valid
6.0s16 911×2valid
456.0ms4 132×0invalid
174.0ms1 424×0exit
Precisions
Click to see histograms. Total time spent on operations: 26.4s
ival-exp: 4.0s (15.1% of total)
ival-pow: 3.6s (13.8% of total)
adjust: 3.0s (11.5% of total)
ival-cos: 2.3s (8.6% of total)
ival-log: 2.2s (8.2% of total)
ival-tan: 1.8s (6.8% of total)
ival-mult!: 1.6s (6% of total)
ival-sqrt: 1.5s (5.7% of total)
ival-sinh: 930.0ms (3.5% of total)
ival-fmod: 905.0ms (3.4% of total)
ival-sin: 876.0ms (3.3% of total)
ival-div!: 794.0ms (3% of total)
ival-pow2: 703.0ms (2.7% of total)
ival-acos: 651.0ms (2.5% of total)
ival-sub!: 483.0ms (1.8% of total)
ival-add!: 371.0ms (1.4% of total)
ival-neg: 201.0ms (0.8% of total)
ival-hypot: 182.0ms (0.7% of total)
ival-atan: 147.0ms (0.6% of total)
ival-<=: 105.0ms (0.4% of total)
ival-and: 40.0ms (0.2% of total)
ival-or: 18.0ms (0.1% of total)
ival-assert: 4.0ms (0% of total)
ival->: 2.0ms (0% of total)
ival-<: 2.0ms (0% of total)
Bogosity

rewrite11.5s (14.1%)

Memory
227.3MiB live, 9 876.7MiB allocated; 2.4s collecting garbage
Stop Event
189×iter limit
52×node limit
15×unsound
4×saturated
Counts
7 461 → 16 261

regimes5.7s (7%)

Memory
-114.2MiB live, 5 867.5MiB allocated; 780ms collecting garbage
Counts
3 728 → 199
Calls

53 calls:

987.0ms
x
445.0ms
a
350.0ms
r
321.0ms
b
235.0ms
c
Compiler

Compiled 1 703 to 2 030 computations (-19.2% saved)

derivations3.9s (4.8%)

Memory
-119.3MiB live, 2 681.7MiB allocated; 418ms collecting garbage
Stop Event
12×fuel
8×done
Compiler

Compiled 4 117 to 1 003 computations (75.6% saved)

eval3.4s (4.2%)

Memory
149.3MiB live, 3 756.1MiB allocated; 797ms collecting garbage
Compiler

Compiled 621 181 to 75 998 computations (87.8% saved)

series3.2s (4%)

Memory
300.4MiB live, 3 165.2MiB allocated; 1.3s collecting garbage
Counts
1 497 → 5 964
Calls

390 calls:

TimeVariablePointExpression
540.0ms
x
@0
((/ (cos (+ x x)) (* (* (* c x) (neg s)) (* (* c x) (neg s)))) (cos (+ x x)) (+ x x) x (* (* (* c x) (neg s)) (* (* c x) (neg s))) (* (* c x) (neg s)) (* c x) c (neg s) s (/ (cos (* -2 x)) (* (* s (* (* (* s c) x) c)) x)) (cos (* -2 x)) 1 (* (* s (* (* (* s c) x) c)) x) (* s (* (* (* s c) x) c)) (* (* (* s c) x) c) (* (* s c) x) (* s c) (/ (/ (cos (* -2 x)) (* (* s c) x)) (* (* s c) x)) (/ (cos (* -2 x)) (* (* s c) x)) (/ (/ (cos (* -2 x)) (* (pow (* c x) 2) s)) s) (/ (cos (* -2 x)) (* (pow (* c x) 2) s)) (* (pow (* c x) 2) s) (pow (* c x) 2) 2 (/ (cos (* 2 x)) (* (* (* (* c x) x) c) (* s s))) (cos (* 2 x)) (* 2 x) (* (* (* (* c x) x) c) (* s s)) (* (* (* c x) x) c) (* (* c x) x) (* s s))
95.0ms
x
@inf
((+ (* (/ (pow (/ (PI) 2) 2) (+ (pow (asin (- 1 x)) 3) (pow (/ (PI) 2) 3))) (+ (* (asin (- 1 x)) (- (asin (- 1 x)) (/ (PI) 2))) (pow (/ (PI) 2) 2))) (/ (neg (pow (asin (+ -1 x)) 2)) (+ (asin (- 1 x)) (/ (PI) 2)))) (/ (pow (/ (PI) 2) 2) (+ (pow (asin (- 1 x)) 3) (pow (/ (PI) 2) 3))) (pow (/ (PI) 2) 2) (/ (PI) 2) (PI) 2 (+ (pow (asin (- 1 x)) 3) (pow (/ (PI) 2) 3)) (pow (asin (- 1 x)) 3) (asin (- 1 x)) (- 1 x) 1 x 3 (pow (/ (PI) 2) 3) (+ (* (asin (- 1 x)) (- (asin (- 1 x)) (/ (PI) 2))) (pow (/ (PI) 2) 2)) (- (asin (- 1 x)) (/ (PI) 2)) (/ (neg (pow (asin (+ -1 x)) 2)) (+ (asin (- 1 x)) (/ (PI) 2))) (neg (pow (asin (+ -1 x)) 2)) (pow (asin (+ -1 x)) 2) (asin (+ -1 x)) (+ -1 x) -1 (+ (asin (- 1 x)) (/ (PI) 2)) (- (/ (PI) 2) (asin (- 1 x))) (- (* 1/2 (PI)) (asin (- 1 x))) (* 1/2 (PI)) 1/2 (acos (- 1 x)) (- 1 x) (* (- (exp (* (log x) -1)) 1) x) (- (exp (* (log x) -1)) 1) (* (log x) -1) (log x) (* (+ (asin (- 1 x)) (/ (PI) 2)) (/ (acos (- 1 x)) (+ (asin (- 1 x)) (/ (PI) 2)))) (/ (acos (- 1 x)) (+ (asin (- 1 x)) (/ (PI) 2))) (acos (- 1 x)) (- (/ (PI) 2) (* (pow (asin (- 1 x)) 1/2) (pow (asin (- 1 x)) 1/2))) (* (pow (asin (- 1 x)) 1/2) (pow (asin (- 1 x)) 1/2)) (pow (asin (- 1 x)) 1/2))
88.0ms
x
@inf
((log (/ (sinh x) x)) (* (+ (* 1/6 x) (* (* (* (- (* (* x x) 1/2835) 1/180) x) x) x)) x) (+ (* 1/6 x) (* (* (* (- (* (* x x) 1/2835) 1/180) x) x) x)) (* 1/6 x) 1/6 x (* (* (* (- (* (* x x) 1/2835) 1/180) x) x) x) (* (* (- (* (* x x) 1/2835) 1/180) x) x) (* (- (* (* x x) 1/2835) 1/180) x) (- (* (* x x) 1/2835) 1/180) (* (* x x) 1/2835) (* x x) 1/2835 1/180 (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)) (/ (sinh x) x) (+ (* (+ (* 1/120 (* x x)) 1/6) (* x x)) 1) (+ (* 1/120 (* x x)) 1/6) (* (* x x) 1/120) 1/120 1 (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) (* (pow x 5) (- (+ (/ 1/6 (pow x 4)) 1/2835) (* (pow x -2) 1/180))) (pow x 5) 5 (- (+ (/ 1/6 (pow x 4)) 1/2835) (* (pow x -2) 1/180)) (+ (/ 1/6 (pow x 4)) 1/2835) (/ 1/6 (pow x 4)) (pow x 4) 4 (* (pow x -2) 1/180) (pow x -2) -2 (/ (- (* (log (sinh x)) (log (sinh x))) (* (log x) (log x))) (+ (log (sinh x)) (log x))) (- (* (log (sinh x)) (log (sinh x))) (* (log x) (log x))) (* (+ (* (+ (* -1/90 (log x)) 1/36) (* x x)) (log (cbrt x))) (* x x)) (+ (* (+ (* -1/90 (log x)) 1/36) (* x x)) (log (cbrt x))) (+ (* -1/90 (log x)) 1/36) -1/90 (log x) 1/36 (log (cbrt x)) (cbrt x) (+ (log (sinh x)) (log x)) (log (sinh x)) (sinh x))
86.0ms
x
@-inf
((log (/ (sinh x) x)) (* (+ (* 1/6 x) (* (* (* (- (* (* x x) 1/2835) 1/180) x) x) x)) x) (+ (* 1/6 x) (* (* (* (- (* (* x x) 1/2835) 1/180) x) x) x)) (* 1/6 x) 1/6 x (* (* (* (- (* (* x x) 1/2835) 1/180) x) x) x) (* (* (- (* (* x x) 1/2835) 1/180) x) x) (* (- (* (* x x) 1/2835) 1/180) x) (- (* (* x x) 1/2835) 1/180) (* (* x x) 1/2835) (* x x) 1/2835 1/180 (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)) (/ (sinh x) x) (+ (* (+ (* 1/120 (* x x)) 1/6) (* x x)) 1) (+ (* 1/120 (* x x)) 1/6) (* (* x x) 1/120) 1/120 1 (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) (* (pow x 5) (- (+ (/ 1/6 (pow x 4)) 1/2835) (* (pow x -2) 1/180))) (pow x 5) 5 (- (+ (/ 1/6 (pow x 4)) 1/2835) (* (pow x -2) 1/180)) (+ (/ 1/6 (pow x 4)) 1/2835) (/ 1/6 (pow x 4)) (pow x 4) 4 (* (pow x -2) 1/180) (pow x -2) -2 (/ (- (* (log (sinh x)) (log (sinh x))) (* (log x) (log x))) (+ (log (sinh x)) (log x))) (- (* (log (sinh x)) (log (sinh x))) (* (log x) (log x))) (* (+ (* (+ (* -1/90 (log x)) 1/36) (* x x)) (log (cbrt x))) (* x x)) (+ (* (+ (* -1/90 (log x)) 1/36) (* x x)) (log (cbrt x))) (+ (* -1/90 (log x)) 1/36) -1/90 (log x) 1/36 (log (cbrt x)) (cbrt x) (+ (log (sinh x)) (log x)) (log (sinh x)) (sinh x))
77.0ms
x
@-inf
((log (/ (sinh x) x)) (+ (* (* x x) 1/6) (* (* (* (- (* (* x x) 1/2835) 1/180) x) x) (* x x))) (* (* x x) 1/6) (* x x) x 1/6 (* (* (* (- (* (* x x) 1/2835) 1/180) x) x) (* x x)) (* (* (- (* (* x x) 1/2835) 1/180) x) x) (* (- (* (* x x) 1/2835) 1/180) x) (- (* (* x x) 1/2835) 1/180) (* (* x x) 1/2835) 1/2835 1/180 (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) (- (* (* (+ (* -1/37800 (* x x)) 1/2835) x) x) 1/180) -1/180 (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) (* (pow x 5) (- (+ (/ 1/6 (pow x 4)) 1/2835) (* (pow x -2) 1/180))) (pow x 5) 5 (- (+ (/ 1/6 (pow x 4)) 1/2835) (* (pow x -2) 1/180)) (/ 1/6 (pow x 4)) (pow x 4) 4 (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) (* (+ (* (pow x -4) 1/6) (- 1/2835 (* (pow x -2) 1/180))) (pow x 4)) (+ (* (pow x -4) 1/6) (- 1/2835 (* (pow x -2) 1/180))) (pow x -4) -4 (- 1/2835 (* (pow x -2) 1/180)) (* (pow x -2) 1/180) (pow x -2) -2 (/ (- (pow (log (sinh x)) 2) (pow (log x) 2)) (log (* x (sinh x)))) (- (pow (log (sinh x)) 2) (pow (log x) 2)) (pow (log (sinh x)) 2) (log (sinh x)) (sinh x) 2 (pow (log x) 2) (log x) (log (* x (sinh x))) (* x (sinh x)))

explain2.7s (3.3%)

Memory
-134.4MiB live, 2 743.2MiB allocated; 462ms collecting garbage
Explanations
Click to see full explanations table
OperatorSubexpressionExplanationCount
sqrt.f64#foflow-rescue5730
cos.f64#fsensitivity5180
-.f64#fcancellation3281
sqrt.f64#fuflow-rescue3240
/.f64#fn/o2560
acos.f64(acos.f64 (-.f64 #s(literal 1 binary64) x))sensitivity2511
log.f64(log.f64 (/.f64 (sinh.f64 x) x))sensitivity2501
tan.f64(tan.f64 (+.f64 y z))sensitivity1911
pow.f64(pow.f64 l (exp.f64 w))sensitivity11618
*.f64#fn*o420
*.f64#fn*u410
*.f64(*.f64 (pow.f64 c #s(literal 2 binary64)) (*.f64 (*.f64 x (pow.f64 s #s(literal 2 binary64))) x))o*u190
↳(pow.f64 c #s(literal 2 binary64))overflow70
↳(*.f64 (*.f64 x (pow.f64 s #s(literal 2 binary64))) x)underflow75
↳(*.f64 x (pow.f64 s #s(literal 2 binary64)))underflow66
↳(pow.f64 s #s(literal 2 binary64))underflow72
*.f64(*.f64 (pow.f64 c #s(literal 2 binary64)) (*.f64 (*.f64 x (pow.f64 s #s(literal 2 binary64))) x))u*o150
↳(pow.f64 c #s(literal 2 binary64))underflow55
↳(*.f64 (*.f64 x (pow.f64 s #s(literal 2 binary64))) x)overflow71
↳(*.f64 x (pow.f64 s #s(literal 2 binary64)))overflow58
↳(pow.f64 s #s(literal 2 binary64))overflow65
-.f64(-.f64 (*.f64 a a) (*.f64 b b))nan-rescue110
↳(*.f64 a a)overflow117
↳(*.f64 b b)overflow11
log.f64(log.f64 (/.f64 (sinh.f64 x) x))oflow-rescue30
↳(sinh.f64 x)overflow3
↳(/.f64 (sinh.f64 x) x)overflow3
/.f64(/.f64 (-.f64 x lo) (-.f64 hi lo))o/o10
↳(-.f64 x lo)overflow1
↳(-.f64 hi lo)overflow256
Confusion
Predicted +Predicted -
+2171274
-6921983
Precision
0.7582954942368145
Recall
0.8879345603271984
Confusion?
Predicted +Predicted MaybePredicted -
+21714270
-692191964
Precision?
0.7536382536382537
Recall?
0.8895705521472392
Freqs
test
numberfreq
02257
12790
270
33
Total Confusion?
Predicted +Predicted MaybePredicted -
+1701
-002
Precision?
1.0
Recall?
0.9444444444444444
Samples
511.0ms2 490×1valid
395.0ms6 612×0valid
362.0ms1 036×2valid
15.0ms102×1exit
Compiler

Compiled 1 067 to 440 computations (58.8% saved)

Precisions
Click to see histograms. Total time spent on operations: 925.0ms
adjust: 145.0ms (15.7% of total)
ival-sin: 82.0ms (8.9% of total)
ival-tan: 81.0ms (8.8% of total)
ival-cos: 80.0ms (8.6% of total)
ival-sqrt: 72.0ms (7.8% of total)
ival-mult!: 67.0ms (7.2% of total)
ival-log: 66.0ms (7.1% of total)
ival-acos: 62.0ms (6.7% of total)
ival-sub!: 53.0ms (5.7% of total)
ival-sinh: 43.0ms (4.6% of total)
ival-exp: 41.0ms (4.4% of total)
ival-fmod: 31.0ms (3.4% of total)
ival-pow2: 30.0ms (3.2% of total)
ival-div!: 26.0ms (2.8% of total)
ival-add!: 21.0ms (2.3% of total)
ival-hypot: 9.0ms (1% of total)
ival-pow: 8.0ms (0.9% of total)
ival-neg: 5.0ms (0.5% of total)
ival-atan: 3.0ms (0.3% of total)

preprocess2.7s (3.3%)

Memory
-84.1MiB live, 2 232.0MiB allocated; 471ms collecting garbage
Stop Event
15×node limit
5×saturated
Compiler

Compiled 20 297 to 9 058 computations (55.4% saved)

analyze2.5s (3%)

Memory
-4.8MiB live, 2 655.0MiB allocated; 589ms 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)

prune2.2s (2.7%)

Memory
-173.6MiB live, 3 035.3MiB allocated; 561ms collecting garbage
Counts
19 803 → 1 397
Compiler

Compiled 75 251 to 39 533 computations (47.5% saved)

bsearch1.4s (1.7%)

Memory
102.5MiB live, 943.5MiB allocated; 889ms collecting garbage
Algorithm
54×binary-search
13×left-value
Stop Event
49×narrow-enough
5×predicate-same
Samples
336.0ms1 454×1valid
194.0ms2 258×0valid
149.0ms160×2valid
Compiler

Compiled 16 608 to 13 697 computations (17.5% saved)

Precisions
Click to see histograms. Total time spent on operations: 562.0ms
ival-exp: 140.0ms (24.9% of total)
ival-cos: 83.0ms (14.8% of total)
ival-tan: 76.0ms (13.5% of total)
ival-sin: 70.0ms (12.5% of total)
adjust: 39.0ms (6.9% of total)
ival-div!: 34.0ms (6.1% of total)
ival-mult!: 34.0ms (6.1% of total)
ival-fmod: 19.0ms (3.4% of total)
ival-pow2: 16.0ms (2.8% of total)
ival-pow: 15.0ms (2.7% of total)
ival-neg: 15.0ms (2.7% of total)
ival-add!: 13.0ms (2.3% of total)
ival-sqrt: 7.0ms (1.2% of total)
ival-sub!: 3.0ms (0.5% 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...