Herbie run

Date:Monday, June 2nd, 2025
Commit:c64524ab on sound-egglog
Seed:2025153
Parameters:256 points for 4 iterations
Flags:
reduce:regimesreduce:binary-searchreduce:branch-expressionssetup:searchrules:arithmeticrules:polynomialsrules:fractionsrules:exponentsrules:trigonometryrules:hyperbolicrules:numericsrules:specialrules:boolsrules:branchesgenerate:rrgenerate:taylorgenerate:proofsgenerate:egglog
default
Memory:234 215.6 MB

Time bar (total: 6.7min)

rewrite3.5min (53%)

Memory
-23.0MiB live, 105 439.2MiB allocated; 38.6s collecting garbage
Counts
2 498 → 162 508

sample1.7min (25.3%)

Memory
1 579.1MiB live, 68 989.4MiB allocated; 27.5s collecting garbage
Samples
26.3s44 526×2valid
16.9s96 992×1valid
16.5s146 246×0invalid
12.0s6 276×5exit
7.0s86 071×0valid
3.5s3 573×3valid
813.0ms4 221×0exit
202.0ms1 109×1exit
127.0ms137×4exit
11.0ms6×4valid
Precisions
Click to see histograms. Total time spent on operations: 1.1min
ival-tan: 12.4s (18.5% of total)
ival-pow: 12.2s (18.2% of total)
adjust: 6.6s (9.9% of total)
ival-cos: 5.0s (7.5% of total)
ival-log: 4.6s (6.8% of total)
ival-sin: 4.0s (6% of total)
ival-mult!: 4.0s (6% of total)
ival-div!: 3.5s (5.2% of total)
ival-expm1: 2.3s (3.4% of total)
ival-sub!: 2.0s (3% of total)
ival-exp: 1.8s (2.7% of total)
ival-add!: 1.7s (2.6% of total)
ival-sqrt: 1.5s (2.3% of total)
ival-fabs: 1.4s (2.1% of total)
ival-log1p: 1.3s (2% of total)
ival-<: 500.0ms (0.7% of total)
ival-atan: 424.0ms (0.6% of total)
ival-<=: 416.0ms (0.6% of total)
ival-and: 378.0ms (0.6% of total)
ival-neg: 365.0ms (0.5% of total)
ival-cbrt: 258.0ms (0.4% of total)
ival-assert: 79.0ms (0.1% of total)
ival-fmin: 64.0ms (0.1% of total)
ival->: 2.0ms (0% of total)
exact: 0.0ms (0% of total)
Bogosity

series38.0s (9.5%)

Memory
644.5MiB live, 18 077.3MiB allocated; 4.7s collecting garbage
Counts
2 498 → 7 902
Calls

501 calls:

TimeVariablePointExpression
163.0ms
n
@0
((- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (/ (log (+ 1 (/ 1 x))) n) (log (+ 1 (/ 1 x))) (/ 1 x) 1 x n (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (/ (- (log (+ 1 x)) (log x)) n) (/ 1 (* n x)) (* n x) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (/ (neg (log (/ x (+ 1 x)))) n) (neg (log (/ x (+ 1 x)))) (log (/ x (+ 1 x))) (/ x (+ 1 x)) (+ 1 x) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (/ (- (+ (log (+ 1 x)) (* 1/2 (/ (pow (log (+ 1 x)) 2) n))) (+ (log x) (* 1/2 (/ (pow (log x) 2) n)))) n) (/ (+ 1 (* -1 (/ (log (/ 1 x)) n))) (* n x)) (+ 1 (* -1 (/ (log (/ 1 x)) n))) (* -1 (/ (log (/ 1 x)) n)) -1 (/ (log (/ 1 x)) n) (log (/ 1 x)) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (/ (exp (* -1 (/ (log (/ 1 x)) n))) (* n x)) (exp (* -1 (/ (log (/ 1 x)) n))))
93.0ms
x
@-inf
((- (tan (+ x eps)) (tan x)) (+ (* (+ (* (+ (* (neg (+ (* (+ (* (+ (+ (* -1/2 (+ (* (tan x) (tan x)) 1)) (* 1/6 (* (tan x) (tan x)))) (- 1/6 (* (+ (* (tan x) (tan x)) 1) (* (tan x) (tan x))))) (tan x)) (* (* (+ (* (tan x) (tan x)) 1) (tan x)) (+ -1/2 1/6))) eps) (+ (+ (* -1/2 (+ (* (tan x) (tan x)) 1)) (* 1/6 (* (tan x) (tan x)))) (- 1/6 (* (+ (* (tan x) (tan x)) 1) (* (tan x) (tan x))))))) eps) (* (+ (* (tan x) (tan x)) 1) (tan x))) eps) 1) eps) (* (* (tan x) (tan x)) eps)) (+ (* (+ (* (neg (+ (* (+ (* (+ (+ (* -1/2 (+ (* (tan x) (tan x)) 1)) (* 1/6 (* (tan x) (tan x)))) (- 1/6 (* (+ (* (tan x) (tan x)) 1) (* (tan x) (tan x))))) (tan x)) (* (* (+ (* (tan x) (tan x)) 1) (tan x)) (+ -1/2 1/6))) eps) (+ (+ (* -1/2 (+ (* (tan x) (tan x)) 1)) (* 1/6 (* (tan x) (tan x)))) (- 1/6 (* (+ (* (tan x) (tan x)) 1) (* (tan x) (tan x))))))) eps) (* (+ (* (tan x) (tan x)) 1) (tan x))) eps) 1) (+ (* (neg (+ (* (+ (* (+ (+ (* -1/2 (+ (* (tan x) (tan x)) 1)) (* 1/6 (* (tan x) (tan x)))) (- 1/6 (* (+ (* (tan x) (tan x)) 1) (* (tan x) (tan x))))) (tan x)) (* (* (+ (* (tan x) (tan x)) 1) (tan x)) (+ -1/2 1/6))) eps) (+ (+ (* -1/2 (+ (* (tan x) (tan x)) 1)) (* 1/6 (* (tan x) (tan x)))) (- 1/6 (* (+ (* (tan x) (tan x)) 1) (* (tan x) (tan x))))))) eps) (* (+ (* (tan x) (tan x)) 1) (tan x))) (neg (+ (* (+ (* (+ (+ (* -1/2 (+ (* (tan x) (tan x)) 1)) (* 1/6 (* (tan x) (tan x)))) (- 1/6 (* (+ (* (tan x) (tan x)) 1) (* (tan x) (tan x))))) (tan x)) (* (* (+ (* (tan x) (tan x)) 1) (tan x)) (+ -1/2 1/6))) eps) (+ (+ (* -1/2 (+ (* (tan x) (tan x)) 1)) (* 1/6 (* (tan x) (tan x)))) (- 1/6 (* (+ (* (tan x) (tan x)) 1) (* (tan x) (tan x))))))) (+ (* (+ (* (+ (+ (* -1/2 (+ (* (tan x) (tan x)) 1)) (* 1/6 (* (tan x) (tan x)))) (- 1/6 (* (+ (* (tan x) (tan x)) 1) (* (tan x) (tan x))))) (tan x)) (* (* (+ (* (tan x) (tan x)) 1) (tan x)) (+ -1/2 1/6))) eps) (+ (+ (* -1/2 (+ (* (tan x) (tan x)) 1)) (* 1/6 (* (tan x) (tan x)))) (- 1/6 (* (+ (* (tan x) (tan x)) 1) (* (tan x) (tan x)))))) (+ (* (+ (+ (* -1/2 (+ (* (tan x) (tan x)) 1)) (* 1/6 (* (tan x) (tan x)))) (- 1/6 (* (+ (* (tan x) (tan x)) 1) (* (tan x) (tan x))))) (tan x)) (* (* (+ (* (tan x) (tan x)) 1) (tan x)) (+ -1/2 1/6))) (+ (+ (* -1/2 (+ (* (tan x) (tan x)) 1)) (* 1/6 (* (tan x) (tan x)))) (- 1/6 (* (+ (* (tan x) (tan x)) 1) (* (tan x) (tan x))))) (+ (* -1/2 (+ (* (tan x) (tan x)) 1)) (* 1/6 (* (tan x) (tan x)))) -1/2 (+ (* (tan x) (tan x)) 1) (tan x) x 1 (* 1/6 (* (tan x) (tan x))) 1/6 (* (tan x) (tan x)) (- 1/6 (* (+ (* (tan x) (tan x)) 1) (* (tan x) (tan x)))) (* (+ (* (tan x) (tan x)) 1) (* (tan x) (tan x))) (* (* (+ (* (tan x) (tan x)) 1) (tan x)) (+ -1/2 1/6)) (* (+ (* (tan x) (tan x)) 1) (tan x)) (+ -1/2 1/6) eps (* (* (tan x) (tan x)) eps) (- (tan (+ x eps)) (tan x)) (* eps (- (+ 1 (* eps (- (* eps (- (* -1 (* eps (+ (* -1/2 (/ (* (sin x) (- 1 (* -1 (/ (pow (sin x) 2) (pow (cos x) 2))))) (cos x))) (+ (* 1/6 (/ (* (sin x) (- 1 (* -1 (/ (pow (sin x) 2) (pow (cos x) 2))))) (cos x))) (/ (* (sin x) (+ 1/6 (+ (* -1 (/ (* (pow (sin x) 2) (- 1 (* -1 (/ (pow (sin x) 2) (pow (cos x) 2))))) (pow (cos x) 2))) (+ (* -1/2 (- 1 (* -1 (/ (pow (sin x) 2) (pow (cos x) 2))))) (* 1/6 (/ (pow (sin x) 2) (pow (cos x) 2))))))) (cos x)))))) (+ 1/6 (+ (* -1 (/ (* (pow (sin x) 2) (- 1 (* -1 (/ (pow (sin x) 2) (pow (cos x) 2))))) (pow (cos x) 2))) (+ (* -1/2 (- 1 (* -1 (/ (pow (sin x) 2) (pow (cos x) 2))))) (* 1/6 (/ (pow (sin x) 2) (pow (cos x) 2)))))))) (* -1 (/ (* (sin x) (- 1 (* -1 (/ (pow (sin x) 2) (pow (cos x) 2))))) (cos x)))))) (* -1 (/ (pow (sin x) 2) (pow (cos x) 2))))) (- (+ 1 (* eps (- (* eps (- (* -1 (* eps (+ (* -1/2 (/ (* (sin x) (- 1 (* -1 (/ (pow (sin x) 2) (pow (cos x) 2))))) (cos x))) (+ (* 1/6 (/ (* (sin x) (- 1 (* -1 (/ (pow (sin x) 2) (pow (cos x) 2))))) (cos x))) (/ (* (sin x) (+ 1/6 (+ (* -1 (/ (* (pow (sin x) 2) (- 1 (* -1 (/ (pow (sin x) 2) (pow (cos x) 2))))) (pow (cos x) 2))) (+ (* -1/2 (- 1 (* -1 (/ (pow (sin x) 2) (pow (cos x) 2))))) (* 1/6 (/ (pow (sin x) 2) (pow (cos x) 2))))))) (cos x)))))) (+ 1/6 (+ (* -1 (/ (* (pow (sin x) 2) (- 1 (* -1 (/ (pow (sin x) 2) (pow (cos x) 2))))) (pow (cos x) 2))) (+ (* -1/2 (- 1 (* -1 (/ (pow (sin x) 2) (pow (cos x) 2))))) (* 1/6 (/ (pow (sin x) 2) (pow (cos x) 2)))))))) (* -1 (/ (* (sin x) (- 1 (* -1 (/ (pow (sin x) 2) (pow (cos x) 2))))) (cos x)))))) (* -1 (/ (pow (sin x) 2) (pow (cos x) 2)))) (+ 1 (* 1/3 (pow eps 2))) (* 1/3 (pow eps 2)) 1/3 (pow eps 2) 2 (- (tan (+ (* 2 (PI)) (+ x eps))) (tan x)) (tan (+ (* 2 (PI)) (+ x eps))) (+ (* 2 (PI)) (+ x eps)) (PI) (+ x eps) (tan x) (* x (+ 1 (* 1/3 (pow x 2)))) (+ 1 (* 1/3 (pow x 2))) (* 1/3 (pow x 2)) (pow x 2) (- (tan (+ x eps)) (tan x)) (* eps (- 1 (* -1 (/ (pow (sin x) 2) (pow (cos x) 2))))) (- 1 (* -1 (/ (pow (sin x) 2) (pow (cos x) 2)))) (* -1 (/ (pow (sin x) 2) (pow (cos x) 2))) -1 (/ (pow (sin x) 2) (pow (cos x) 2)) (pow (sin x) 2) (sin x) (pow (cos x) 2) (cos x) (/ (+ (* (tan (+ x eps)) (neg (cos x))) (sin x)) (neg (cos x))) (+ (* (tan (+ x eps)) (neg (cos x))) (sin x)) (tan (+ x eps)) (neg (cos x)))
80.0ms
n
@-inf
((- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (/ (neg (log (/ x (+ (* (* (/ 1 (* n x)) n) x) x)))) n) (neg (log (/ x (+ (* (* (/ 1 (* n x)) n) x) x)))) (log (/ x (+ (* (* (/ 1 (* n x)) n) x) x))) (/ x (+ (* (* (/ 1 (* n x)) n) x) x)) x (+ (* (* (/ 1 (* n x)) n) x) x) (* (/ 1 (* n x)) n) (/ 1 (* n x)) 1 (* n x) n (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (/ (- (log (+ 1 x)) (log x)) n) (/ (/ 1 n) x) (/ 1 n) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (/ (log (/ (+ 1 x) x)) n) (log (/ (+ 1 x) x)) (/ (+ 1 x) x) (+ 1 x) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (/ (- (log (+ 1 x)) (log x)) n) (/ (/ (* (/ 1 x) (* n x)) n) (* n x)) (/ (* (/ 1 x) (* n x)) n) (* (/ 1 x) (* n x)) (/ 1 x) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (/ (pow x (/ 1 n)) (* n x)) (pow x (/ 1 n)))
80.0ms
n
@inf
((- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (/ (log (+ 1 (/ 1 x))) n) (log (+ 1 (/ 1 x))) (/ 1 x) 1 x n (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (/ (- (log (+ 1 x)) (log x)) n) (/ 1 (* n x)) (* n x) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (/ (neg (log (/ x (+ 1 x)))) n) (neg (log (/ x (+ 1 x)))) (log (/ x (+ 1 x))) (/ x (+ 1 x)) (+ 1 x) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (/ (- (+ (log (+ 1 x)) (* 1/2 (/ (pow (log (+ 1 x)) 2) n))) (+ (log x) (* 1/2 (/ (pow (log x) 2) n)))) n) (/ (+ 1 (* -1 (/ (log (/ 1 x)) n))) (* n x)) (+ 1 (* -1 (/ (log (/ 1 x)) n))) (* -1 (/ (log (/ 1 x)) n)) -1 (/ (log (/ 1 x)) n) (log (/ 1 x)) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (/ (exp (* -1 (/ (log (/ 1 x)) n))) (* n x)) (exp (* -1 (/ (log (/ 1 x)) n))))
71.0ms
n
@-inf
((- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (* -1 (/ (- (+ (* -1 (log (+ 1 x))) (* -1 (/ (- (+ (* -1 (/ (- (* -1/6 (pow (log (+ 1 x)) 3)) (* -1/6 (pow (log x) 3))) n)) (* 1/2 (pow (log (+ 1 x)) 2))) (* 1/2 (pow (log x) 2))) n))) (* -1 (log x))) n)) -1 (/ (- (+ (* -1 (log (+ 1 x))) (* -1 (/ (- (+ (* -1 (/ (- (* -1/6 (pow (log (+ 1 x)) 3)) (* -1/6 (pow (log x) 3))) n)) (* 1/2 (pow (log (+ 1 x)) 2))) (* 1/2 (pow (log x) 2))) n))) (* -1 (log x))) n) (- (+ (* -1 (log (+ 1 x))) (* -1 (/ (- (+ (* -1 (/ (- (* -1/6 (pow (log (+ 1 x)) 3)) (* -1/6 (pow (log x) 3))) n)) (* 1/2 (pow (log (+ 1 x)) 2))) (* 1/2 (pow (log x) 2))) n))) (* -1 (log x))) (+ (* -1 (log (+ 1 x))) (* -1 (/ (- (+ (* -1 (/ (- (* -1/6 (pow (log (+ 1 x)) 3)) (* -1/6 (pow (log x) 3))) n)) (* 1/2 (pow (log (+ 1 x)) 2))) (* 1/2 (pow (log x) 2))) n))) (log (+ 1 x)) (+ 1 x) 1 x (* -1 (/ (- (+ (* -1 (/ (- (* -1/6 (pow (log (+ 1 x)) 3)) (* -1/6 (pow (log x) 3))) n)) (* 1/2 (pow (log (+ 1 x)) 2))) (* 1/2 (pow (log x) 2))) n)) (/ (- (+ (* -1 (/ (- (* -1/6 (pow (log (+ 1 x)) 3)) (* -1/6 (pow (log x) 3))) n)) (* 1/2 (pow (log (+ 1 x)) 2))) (* 1/2 (pow (log x) 2))) n) (- (+ (* -1 (/ (- (* -1/6 (pow (log (+ 1 x)) 3)) (* -1/6 (pow (log x) 3))) n)) (* 1/2 (pow (log (+ 1 x)) 2))) (* 1/2 (pow (log x) 2))) (+ (* -1 (/ (- (* -1/6 (pow (log (+ 1 x)) 3)) (* -1/6 (pow (log x) 3))) n)) (* 1/2 (pow (log (+ 1 x)) 2))) (/ (- (* -1/6 (pow (log (+ 1 x)) 3)) (* -1/6 (pow (log x) 3))) n) (- (* -1/6 (pow (log (+ 1 x)) 3)) (* -1/6 (pow (log x) 3))) (* -1/6 (pow (log (+ 1 x)) 3)) -1/6 (pow (log (+ 1 x)) 3) 3 (* -1/6 (pow (log x) 3)) (pow (log x) 3) (log x) n (* 1/2 (pow (log (+ 1 x)) 2)) 1/2 (pow (log (+ 1 x)) 2) 2 (* 1/2 (pow (log x) 2)) (pow (log x) 2) (* -1 (log x)) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (/ (- (log (+ 1 x)) (log x)) n) (- (log (+ 1 x)) (log x)) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (pow (+ x 1) (/ 1 n)) (+ 1 (/ x n)) (/ x n) (pow x (/ 1 n)) (/ 1 n) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (pow (+ x 1) (/ 1 n)) (+ x 1) (pow x (/ 1 n)) (+ 1 (/ (log x) n)) (/ (log x) n) (- (pow (+ x 1) (/ 1 n)) (pow x (/ 1 n))) (/ (- (+ (log (+ 1 x)) (* 1/2 (/ (pow (log (+ 1 x)) 2) n))) (+ (log x) (* 1/2 (/ (pow (log x) 2) n)))) n) (- (+ (log (+ 1 x)) (* 1/2 (/ (pow (log (+ 1 x)) 2) n))) (+ (log x) (* 1/2 (/ (pow (log x) 2) n)))) (+ (log (+ 1 x)) (* 1/2 (/ (pow (log (+ 1 x)) 2) n))) (* 1/2 (/ (pow (log (+ 1 x)) 2) n)) (/ (pow (log (+ 1 x)) 2) n) (+ (log x) (* 1/2 (/ (pow (log x) 2) n))) (* 1/2 (/ (pow (log x) 2) n)) (/ (pow (log x) 2) n))

eval30.9s (7.7%)

Memory
720.2MiB live, 26 558.5MiB allocated; 11.7s collecting garbage
Compiler

Compiled 2 382 187 to 739 417 computations (69% saved)

prune7.6s (1.9%)

Memory
-667.9MiB live, 7 242.0MiB allocated; 3.5s collecting garbage
Counts
190 775 → 1 703
Compiler

Compiled 57 910 to 46 623 computations (19.5% saved)

preprocess4.5s (1.1%)

Memory
-529.8MiB live, 3 150.7MiB allocated; 935ms collecting garbage
Stop Event
28×node-limit
Compiler

Compiled 5 403 to 4 227 computations (21.8% saved)

regimes3.1s (0.8%)

Memory
-135.6MiB live, 2 568.0MiB allocated; 452ms collecting garbage
Counts
3 099 → 277
Calls

43 calls:

688.0ms
x
225.0ms
(/.f64 #s(literal 1 binary64) n)
216.0ms
eps
197.0ms
b
144.0ms
n
Compiler

Compiled 1 440 to 1 572 computations (-9.2% saved)

analyze1.7s (0.4%)

Memory
73.9MiB live, 1 216.1MiB allocated; 284ms 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)

bsearch1.3s (0.3%)

Memory
-70.5MiB live, 915.0MiB allocated; 316ms collecting garbage
Algorithm
80×binary-search
24×left-value
Stop Event
73×narrow-enough
7×predicate-same
Samples
429.0ms4 574×0valid
115.0ms556×1valid
99.0ms1 005×0invalid
74.0ms230×2valid
3.0ms34×0exit
Compiler

Compiled 22 237 to 23 291 computations (-4.7% saved)

Precisions
Click to see histograms. Total time spent on operations: 480.0ms
ival-mult!: 154.0ms (32.1% of total)
ival-pow: 52.0ms (10.8% of total)
ival-neg: 50.0ms (10.4% of total)
ival-div!: 43.0ms (9% of total)
ival-sqrt: 42.0ms (8.7% of total)
ival-cos: 36.0ms (7.5% of total)
adjust: 24.0ms (5% of total)
ival-sub!: 24.0ms (5% of total)
ival-log1p: 23.0ms (4.8% of total)
ival-add!: 13.0ms (2.7% of total)
ival-expm1: 9.0ms (1.9% of total)
ival-exp: 5.0ms (1% of total)
ival-log: 5.0ms (1% of total)

derivations109.0ms (0%)

Memory
-18.6MiB live, 57.4MiB allocated; 126ms collecting garbage
Stop Event
23×fuel
5×done
Compiler

Compiled 2 229 to 1 474 computations (33.9% saved)

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...