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:146 470.6 MB

Time bar (total: 4.0min)

rewrite2.2min (53.6%)

Memory
414.6MiB live, 69 462.6MiB allocated; 17.7s collecting garbage
Counts
1 642 → 87 846

sample51.4s (21.2%)

Memory
213.8MiB live, 32 304.7MiB allocated; 14.4s collecting garbage
Samples
21.2s21 210×5exit
8.3s39 049×1valid
7.5s109 862×0valid
5.0s16 209×2valid
890.0ms5 812×0invalid
232.0ms1 241×1exit
108.0ms1 378×0exit
1.0ms1×4exit
Precisions
Click to see histograms. Total time spent on operations: 36.1s
ival-exp: 7.7s (21.4% of total)
ival-cos: 6.3s (17.5% of total)
ival-pow: 3.8s (10.6% of total)
adjust: 3.5s (9.6% of total)
ival-sqrt: 1.9s (5.2% of total)
ival-tan: 1.7s (4.7% of total)
ival-mult!: 1.7s (4.6% of total)
ival-log: 1.6s (4.5% of total)
ival-fmod: 1.5s (4.2% of total)
ival-sinh: 1.3s (3.5% of total)
ival-sin: 1.1s (3.1% of total)
ival-add!: 1.0s (2.9% of total)
ival-div!: 923.0ms (2.6% of total)
ival-acos: 566.0ms (1.6% of total)
ival-pow2: 551.0ms (1.5% of total)
ival-sub!: 350.0ms (1% of total)
ival-neg: 232.0ms (0.6% of total)
ival-hypot: 225.0ms (0.6% of total)
ival-<=: 49.0ms (0.1% of total)
ival-atan: 48.0ms (0.1% of total)
ival-and: 35.0ms (0.1% of total)
ival-or: 16.0ms (0% of total)
ival-assert: 4.0ms (0% of total)
ival->: 2.0ms (0% of total)
ival-<: 2.0ms (0% of total)
Bogosity

series25.9s (10.7%)

Memory
160.9MiB live, 13 591.9MiB allocated; 4.0s collecting garbage
Counts
1 642 → 4 700
Calls

402 calls:

TimeVariablePointExpression
370.0ms
w
@-inf
((* (exp (neg w)) (pow l (exp w))) (exp (neg w)) (neg w) w (pow l (exp w)) (pow (exp (neg (exp w))) (neg (log l))) (exp (neg (exp w))) (neg (exp w)) (exp w) (neg (log l)) (log l) l (/ (pow l (exp w)) (exp w)) (+ l (* w (- (* l (log l)) l))) (* w (- (* l (log l)) l)) (- (* l (log l)) l) (* l (log l)) (* (exp (neg w)) (pow l (exp w))) (exp (neg w)) (+ 1 (* w (- (* 1/2 w) 1))) 1 (* w (- (* 1/2 w) 1)) (- (* 1/2 w) 1) (* 1/2 w) 1/2 (pow l (exp w)) (+ l (* l (* w (log l)))) (* l (* w (log l))) (* w (log l)) (* (exp (neg w)) (pow l (exp w))) (exp (neg w)) (+ 1 (* -1 w)) (* -1 w) -1 (pow l (exp w)) (/ (pow l (exp w)) (exp w)) (/ (exp (* -1 (* (exp w) (log (/ 1 l))))) (exp w)) (exp (* -1 (* (exp w) (log (/ 1 l))))) (* -1 (* (exp w) (log (/ 1 l)))) (* (exp w) (log (/ 1 l))) (log (/ 1 l)) (/ 1 l))
58.0ms
l
@0
((/ (pow l (exp w)) (exp w)) (pow l (exp w)) l (exp w) w (* (exp (neg w)) (pow l (exp w))) (* (exp (neg w)) (pow l (exp w))) (exp (neg w)) (neg w) (pow l (exp w)) (+ l (* l (* w (log l)))) (* l (* w (log l))) (* w (log l)) (log l) (* (exp (neg w)) (pow l (exp w))) (pow l (exp w)) (exp w) (+ 1 w) 1 (* (exp (neg w)) (pow l (exp w))) (pow l (exp w)) (exp (* -1 (* (exp w) (log (/ 1 l))))) (* -1 (* (exp w) (log (/ 1 l)))) -1 (* (exp w) (log (/ 1 l))) (log (/ 1 l)) (/ 1 l))
47.0ms
x
@-inf
((* (fmod (exp x) (sqrt (cos (+ (* 2 (* (sin (/ (- 0 (/ (+ (fabs (PI)) (PI)) 2)) 2)) (cos (/ (/ (+ (fabs (PI)) (PI)) 2) 2)))) x)))) (exp (neg (+ (* 2 (* (sin (/ (- 0 (/ (+ (fabs (PI)) (PI)) 2)) 2)) (cos (/ (/ (+ (fabs (PI)) (PI)) 2) 2)))) x)))) (fmod (exp x) (sqrt (cos (+ (* 2 (* (sin (/ (- 0 (/ (+ (fabs (PI)) (PI)) 2)) 2)) (cos (/ (/ (+ (fabs (PI)) (PI)) 2) 2)))) x)))) (exp x) (+ 1 (+ (* 2 (* (sin (/ (- 0 (/ (+ (fabs (PI)) (PI)) 2)) 2)) (cos (/ (/ (+ (fabs (PI)) (PI)) 2) 2)))) x)) 1 (+ (* 2 (* (sin (/ (- 0 (/ (+ (fabs (PI)) (PI)) 2)) 2)) (cos (/ (/ (+ (fabs (PI)) (PI)) 2) 2)))) x) 2 (* (sin (/ (- 0 (/ (+ (fabs (PI)) (PI)) 2)) 2)) (cos (/ (/ (+ (fabs (PI)) (PI)) 2) 2))) (sin (/ (- 0 (/ (+ (fabs (PI)) (PI)) 2)) 2)) (/ (- 0 (/ (+ (fabs (PI)) (PI)) 2)) 2) (- 0 (/ (+ (fabs (PI)) (PI)) 2)) 0 (/ (+ (fabs (PI)) (PI)) 2) (+ (fabs (PI)) (PI)) (fabs (PI)) (PI) (cos (/ (/ (+ (fabs (PI)) (PI)) 2) 2)) (/ (/ (+ (fabs (PI)) (PI)) 2) 2) x (sqrt (cos (+ (* 2 (* (sin (/ (- 0 (/ (+ (fabs (PI)) (PI)) 2)) 2)) (cos (/ (/ (+ (fabs (PI)) (PI)) 2) 2)))) x))) (cos (+ (* 2 (* (sin (/ (- 0 (/ (+ (fabs (PI)) (PI)) 2)) 2)) (cos (/ (/ (+ (fabs (PI)) (PI)) 2) 2)))) x)) (exp (neg (+ (* 2 (* (sin (/ (- 0 (/ (+ (fabs (PI)) (PI)) 2)) 2)) (cos (/ (/ (+ (fabs (PI)) (PI)) 2) 2)))) x))) (neg (+ (* 2 (* (sin (/ (- 0 (/ (+ (fabs (PI)) (PI)) 2)) 2)) (cos (/ (/ (+ (fabs (PI)) (PI)) 2) 2)))) x)) (* (fmod (exp x) (sqrt (cos x))) (exp (neg x))) (fmod (exp x) (sqrt (cos x))) (exp x) (sqrt (cos x)) (+ 1 (* -1/4 (pow x 2))) (* -1/4 (pow x 2)) -1/4 (pow x 2) (* (fmod (exp x) (sqrt (cos x))) (/ 1 (exp x))) (fmod (exp x) (sqrt (cos x))) (exp x) (+ 1 x) (sqrt (cos x)) (cos x) (/ 1 (exp x)) (* (fmod (exp x) (sqrt (cos x))) (pow (exp (+ x x)) (neg 1/2))) (fmod (exp x) (sqrt (cos x))) (pow (exp (+ x x)) (neg 1/2)) (exp (+ x x)) (+ x x) (neg 1/2) 1/2 (* (fmod (exp x) (sqrt (cos x))) (exp (neg x))) (fmod (exp x) (sqrt (cos x))) (exp x) (+ (* (cosh (/ 1 2)) (cosh (/ (- 0 1) 2))) (* (sinh (/ 1 2)) (sinh (/ (- 0 1) 2)))) (cosh (/ 1 2)) (/ 1 2) (cosh (/ (- 0 1) 2)) (/ (- 0 1) 2) (- 0 1) (* (sinh (/ 1 2)) (sinh (/ (- 0 1) 2))) (sinh (/ 1 2)) (sinh (/ (- 0 1) 2)) (exp (neg x)) (neg x))
44.0ms
x
@0
((sqrt (+ (* x x) (* x x))) x (sqrt (+ (* x x) (* x x))) (* x (sqrt 2)) (sqrt 2) 2 (sqrt (* (+ x x) x)) (* (+ x x) x) (+ x x) (sqrt (+ (* x x) (* x x))) (* -1 (* x (sqrt 2))) -1 (pow (* (* (+ x x) (+ x x)) (* x x)) (/ 1/2 2)) (* (* (+ x x) (+ x x)) (* x x)) (* (+ x x) (+ x x)) (* x x) (/ 1/2 2) 1/2)
42.0ms
x
@-inf
((log (/ (sinh x) x)) (* (* (- (+ (* (* x 1/2835) (* (* x x) x)) 1/6) (* (* x 1/180) x)) x) x) (* (- (+ (* (* x 1/2835) (* (* x x) x)) 1/6) (* (* x 1/180) x)) x) (- (+ (* (* x 1/2835) (* (* x x) x)) 1/6) (* (* x 1/180) x)) (+ (* (* x 1/2835) (* (* x x) x)) 1/6) (* x 1/2835) x 1/2835 (* (* x x) x) (* x x) 1/6 (* (* x 1/180) 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) (+ (* (- (* 1/2835 (* x x)) 1/180) (* x x)) 1/6) (log (/ (sinh x) x)) (+ (* (* (* (* x -1/180) x) x) x) (* (* x 1/6) x)) (* (* (* x -1/180) x) x) (* (* x -1/180) x) (* x -1/180) -1/180 (* (* x 1/6) x) (* x 1/6) (log (/ (sinh x) x)) (* (pow x 2) (+ 1/6 (* -1/180 (pow x 2)))) (* (pow x 4) (- (* 1/6 (/ 1 (pow x 2))) 1/180)) (pow x 4) 4 (- (* 1/6 (/ 1 (pow x 2))) 1/180) (* 1/6 (/ 1 (pow x 2))) (/ 1 (pow x 2)) 1 (pow x 2) 2 (log (/ (sinh x) x)) (* (pow x 2) (+ 1/6 (* (pow x 2) (- (* 1/2835 (pow x 2)) 1/180)))) (* (pow x 6) (- (+ 1/2835 (/ 1/6 (pow x 4))) (* 1/180 (/ 1 (pow x 2))))) (pow x 6) 6 (- (+ 1/2835 (/ 1/6 (pow x 4))) (* 1/180 (/ 1 (pow x 2)))) (+ 1/2835 (/ 1/6 (pow x 4))) (/ 1/6 (pow x 4)) (* 1/180 (/ 1 (pow x 2))))

eval17.8s (7.4%)

Memory
494.2MiB live, 16 081.1MiB allocated; 6.9s collecting garbage
Compiler

Compiled 1 211 358 to 369 646 computations (69.5% saved)

regimes7.1s (2.9%)

Memory
19.2MiB live, 5 699.1MiB allocated; 1.3s collecting garbage
Counts
3 943 → 156
Calls

53 calls:

876.0ms
x
764.0ms
a
431.0ms
y
426.0ms
(tan.f64 a)
400.0ms
z
Compiler

Compiled 1 431 to 1 962 computations (-37.1% saved)

prune4.1s (1.7%)

Memory
-185.4MiB live, 4 764.0MiB allocated; 931ms collecting garbage
Counts
93 505 → 1 655
Compiler

Compiled 58 793 to 47 269 computations (19.6% saved)

preprocess3.4s (1.4%)

Memory
-134.8MiB live, 2 345.6MiB allocated; 1.3s collecting garbage
Stop Event
19×node-limit
1×saturated
Compiler

Compiled 7 821 to 6 641 computations (15.1% saved)

analyze2.0s (0.8%)

Memory
118.5MiB live, 1 623.9MiB allocated; 397ms 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)

bsearch817.0ms (0.3%)

Memory
57.2MiB live, 540.3MiB allocated; 130ms collecting garbage
Algorithm
34×binary-search
13×left-value
Stop Event
32×narrow-enough
1×predicate-same
1×predicate-failed
Samples
224.0ms1 051×1valid
171.0ms1 861×0valid
146.0ms101×5exit
5.0ms61×0exit
Compiler

Compiled 7 954 to 7 823 computations (1.6% saved)

Precisions
Click to see histograms. Total time spent on operations: 446.0ms
ival-exp: 123.0ms (27.6% of total)
ival-tan: 101.0ms (22.7% of total)
ival-cos: 57.0ms (12.8% of total)
ival-sin: 35.0ms (7.9% of total)
adjust: 34.0ms (7.6% of total)
ival-pow: 20.0ms (4.5% of total)
ival-mult!: 19.0ms (4.3% of total)
ival-add!: 10.0ms (2.2% of total)
ival-fmod: 9.0ms (2% of total)
ival-acos: 9.0ms (2% of total)
ival-div!: 7.0ms (1.6% of total)
ival-sqrt: 6.0ms (1.3% of total)
ival-pow2: 6.0ms (1.3% of total)
ival-neg: 6.0ms (1.3% of total)
ival-sub!: 4.0ms (0.9% of total)

derivations47.0ms (0%)

Memory
-6.5MiB live, 56.3MiB allocated; 11ms collecting garbage
Stop Event
15×fuel
5×done
Compiler

Compiled 1 334 to 845 computations (36.7% saved)

start1.0ms (0%)

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

end0.0ms (0%)

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

Profiling

Loading profile data...