Herbie run

Date:Tuesday, December 24th, 2024
Commit:e899e8c7 on sound-simplify
Seed:2024359
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:1 784 914.0 MB

Time bar (total: 28.0min)

sample6.5min (23.2%)

Memory
3 946.1MiB live, 433 063.2MiB allocated; 2.4min collecting garbage
Samples
3.8min2 144 429×0valid
25.0s69 899×1valid
14.8s63 636×0invalid
1.8s5 912×2valid
1.5s1 633×5exit
657.0ms1 750×1invalid
183.0ms621×3valid
1.0ms3×4valid
Precisions
Click to see histograms. Total time spent on operations: 2.7min
ival-mult: 50.1s (31.1% of total)
ival-div: 22.5s (14% of total)
ival-sub: 21.2s (13.1% of total)
ival-add: 20.9s (13% of total)
ival-log: 9.1s (5.6% of total)
const: 8.3s (5.2% of total)
adjust: 6.5s (4% of total)
ival-sin: 6.4s (4% of total)
ival-sqrt: 5.8s (3.6% of total)
ival-cos: 2.8s (1.7% of total)
ival-exp: 2.0s (1.3% of total)
ival-true: 1.6s (1% of total)
exact: 1.1s (0.7% of total)
ival-assert: 879.0ms (0.5% of total)
ival-acos: 397.0ms (0.2% of total)
ival-hypot: 379.0ms (0.2% of total)
ival-fabs: 339.0ms (0.2% of total)
ival-tan: 338.0ms (0.2% of total)
ival-cosh: 283.0ms (0.2% of total)
ival-sinh: 271.0ms (0.2% of total)
ival-tanh: 84.0ms (0.1% of total)
Bogosity

simplify5.1min (18.1%)

Memory
6 088.2MiB live, 300 819.7MiB allocated; 1.1min collecting garbage
Algorithm
2 201×egg-herbie
Stop Event
2 893×iter limit
1 480×node limit
732×saturated
6×unsound
Counts
75 470 → 74 319

rewrite3.9min (14%)

Memory
-1 326.0MiB live, 246 867.6MiB allocated; 1.0min collecting garbage
Stop Event
2 020×iter limit
922×node limit
34×unsound
17×saturated
Counts
11 994 → 357 525

derivations3.4min (12.1%)

Memory
238.8MiB live, 161 794.7MiB allocated; 34.1s collecting garbage
Stop Event
1 439×iter limit
977×node limit
162×fuel
107×done
23×saturated
11×unsound
Compiler

Compiled 143 590 to 19 210 computations (86.6% saved)

localize2.0min (7.1%)

Memory
-2 090.5MiB live, 132 390.0MiB allocated; 31.6s collecting garbage
Samples
1.0min219 110×0valid
14.9s11 538×1valid
5.7s3 311×2valid
4.7s10 401×0invalid
1.2s945×5exit
743.0ms286×3valid
666.0ms1 670×0exit
55.0ms5×4valid
49.0ms30×1exit
Compiler

Compiled 154 142 to 24 006 computations (84.4% saved)

Precisions
Click to see histograms. Total time spent on operations: 1.1min
ival-mult: 22.9s (35.9% of total)
ival-add: 8.5s (13.3% of total)
ival-div: 8.1s (12.7% of total)
adjust: 5.8s (9% of total)
ival-sub: 4.3s (6.7% of total)
const: 2.7s (4.2% of total)
ival-sin: 2.1s (3.3% of total)
ival-log: 1.9s (3% of total)
ival-pow: 1.6s (2.6% of total)
ival-sqrt: 1.4s (2.1% of total)
ival-pow2: 1.1s (1.7% of total)
ival-neg: 1.0s (1.6% of total)
ival-cos: 927.0ms (1.4% of total)
ival-exp: 473.0ms (0.7% of total)
exact: 243.0ms (0.4% of total)
ival-true: 184.0ms (0.3% of total)
ival-cosh: 114.0ms (0.2% of total)
ival-hypot: 101.0ms (0.2% of total)
ival-assert: 98.0ms (0.2% of total)
ival-log1p: 52.0ms (0.1% of total)
ival-tan: 49.0ms (0.1% of total)
ival-pi: 44.0ms (0.1% of total)
ival-sinh: 33.0ms (0.1% of total)
ival-expm1: 33.0ms (0.1% of total)
ival-acos: 33.0ms (0.1% of total)
ival-fabs: 19.0ms (0% of total)
ival-tanh: 16.0ms (0% of total)
ival-sinu: 15.0ms (0% of total)
ival-asin: 13.0ms (0% of total)
ival->: 3.0ms (0% of total)
ival-then: 1.0ms (0% of total)

eval1.5min (5.3%)

Memory
1 875.1MiB live, 117 828.7MiB allocated; 24.0s collecting garbage
Compiler

Compiled 17 353 394 to 1 599 955 computations (90.8% saved)

regimes1.3min (4.6%)

Memory
-993.2MiB live, 89 426.7MiB allocated; 24.6s collecting garbage
Counts
32 765 → 4 761
Calls

510 calls:

10.2s
z
9.9s
x
9.6s
y
4.8s
t
2.6s
k
Compiler

Compiled 37 026 to 55 676 computations (-50.4% saved)

preprocess59.0s (3.5%)

Memory
2 223.6MiB live, 61 769.9MiB allocated; 14.9s collecting garbage
Algorithm
269×egg-herbie
Stop Event
536×iter limit
398×saturated
142×node limit
Compiler

Compiled 322 554 to 60 988 computations (81.1% saved)

series55.5s (3.3%)

Memory
516.9MiB live, 69 546.9MiB allocated; 15.3s collecting garbage
Counts
11 994 → 75 470
Calls

9162 calls:

TimeVariablePointExpression
394.0ms
y
@-inf
((+ (* (* (/ (pow (log y) 2) (+ (* (log y) x) z)) (neg x)) (neg x)) (- (* (/ z (+ (* (log y) x) z)) (neg z)) y)) (* (/ (pow (log y) 2) (+ (* (log y) x) z)) (neg x)) (/ (pow (log y) 2) (+ (* (log y) x) z)) (pow (log y) 2) (- (- (* x (log y)) z) y) (* (+ (* x (/ (log y) y)) (- (/ (neg z) y) 1)) y) (+ (* x (/ (log y) y)) (- (/ (neg z) y) 1)) (/ (neg z) y) (- (- (* x (log y)) z) y) (* (+ (* x (/ (log y) y)) (- (/ (neg z) y) 1)) y) (+ (* x (/ (log y) y)) (- (/ (neg z) y) 1)) (* x (/ (log y) y)) (pow (neg (sqrt x)) 2) (- (- (* x (log y)) z) y) (+ (* (log y) (pow (neg (sqrt x)) 2)) (neg y)) (log y) (+ (* (pow (pow (* x (log y)) 1/4) 2) (sqrt (* (log y) x))) (neg y)) (pow (pow (* x (log y)) 1/4) 2) (- (- (* x (log y)) z) y) (pow (* x (log y)) 1/4) (/ z (+ (* (log y) x) z)) (neg z) (/ (log y) y) (sqrt (* (log y) x)))
236.0ms
y
@0
((- (* (* y x) 3) z) (* (* y x) 3) (* y x) (- (* (* x 3) y) z) (neg z) (- (* (* y 3) x) z) (* (* y 3) x) (* y 3) (- (* (sqrt (* (* 9 (* x x)) y)) (sqrt y)) z) (* (sqrt (* (* 9 (* x x)) y)) (sqrt y)) (sqrt (* (* 9 (* x x)) y)) (* (* 9 (* x x)) y) (+ (* y (/ (* (* 9 (* x x)) y) (+ (* y (* 3 x)) z))) (* z (/ z (+ (* y (* 3 x)) z)))) (/ (* (* 9 (* x x)) y) (+ (* y (* 3 x)) z)) (* 9 (* x x)) (/ z (+ (* y (* 3 x)) z)) (* z (/ z (+ (* y (* 3 x)) z))))
235.0ms
y
@inf
((+ (* (* (/ (pow (log y) 2) (+ (* (log y) x) z)) (neg x)) (neg x)) (- (* (/ z (+ (* (log y) x) z)) (neg z)) y)) (* (/ (pow (log y) 2) (+ (* (log y) x) z)) (neg x)) (/ (pow (log y) 2) (+ (* (log y) x) z)) (pow (log y) 2) (- (- (* x (log y)) z) y) (* (+ (* x (/ (log y) y)) (- (/ (neg z) y) 1)) y) (+ (* x (/ (log y) y)) (- (/ (neg z) y) 1)) (/ (neg z) y) (- (- (* x (log y)) z) y) (* (+ (* x (/ (log y) y)) (- (/ (neg z) y) 1)) y) (+ (* x (/ (log y) y)) (- (/ (neg z) y) 1)) (* x (/ (log y) y)) (pow (neg (sqrt x)) 2) (- (- (* x (log y)) z) y) (+ (* (log y) (pow (neg (sqrt x)) 2)) (neg y)) (log y) (+ (* (pow (pow (* x (log y)) 1/4) 2) (sqrt (* (log y) x))) (neg y)) (pow (pow (* x (log y)) 1/4) 2) (- (- (* x (log y)) z) y) (pow (* x (log y)) 1/4) (/ z (+ (* (log y) x) z)) (neg z) (/ (log y) y) (sqrt (* (log y) x)))
214.0ms
a
@0
((+ (* (* 27 a) b) (+ (+ (* (* z t) (* y -9)) x) x)) (* 27 a) (+ (+ (* (* z t) (* y -9)) x) x) (+ (* (* z t) (* y -9)) x) (+ (- (* x 2) (* (* (* y 9) z) t)) (* (* a 27) b)) (+ (* 2 x) (* (* b a) 27)) (* (* b a) 27) (* b a) (+ (- (* x 2) (* (* (* y 9) z) t)) (* (* a 27) b)) (+ (* -9 (* (* t y) z)) (* (* b a) 27)) (* (* t y) z) (* t y) (+ (- (* x 2) (* (* (* y 9) z) t)) (* (* a 27) b)) (+ (* (* z -9) (* t y)) (* (* b a) 27)) (* z -9) (+ (* (* -9 (* z y)) t) (+ (* (* b 27) a) (+ x x))) (* -9 (* z y)) (* z y) (+ (* (* b 27) a) (+ x x)) (* b 27))
200.0ms
y
@0
((* x (log (pow (* y x) (/ (log (/ x y)) (log (* y x)))))) (log (pow (* y x) (/ (log (/ x y)) (log (* y x))))) (pow (* y x) (/ (log (/ x y)) (log (* y x)))) (* (neg x) (/ -1 y)) (/ 0 0) (* (/ (log (/ x y)) (log (* y x))) (* (log (* y x)) x)) (/ (log (/ x y)) (log (* y x))) (log (/ x y)) (/ x y) (/ (* (- (pow (log x) 2) (pow (log y) 2)) x) (log (* y x))) (* (- (pow (log x) 2) (pow (log y) 2)) x) (- (pow (log x) 2) (pow (log y) 2)) (pow (log x) 2) (/ (* (- (pow (log (neg x)) 3) (pow (log (neg y)) 3)) x) (+ (* (log (neg y)) (log (* (neg y) (neg x)))) (pow (log (neg x)) 2))) (* (- (pow (log (neg x)) 3) (pow (log (neg y)) 3)) x) (- (pow (log (neg x)) 3) (pow (log (neg y)) 3)) (pow (log (neg x)) 3) (neg x) (log (* y x)) (* y x) (* (log (* y x)) x) (log x) (log y) (log (neg x)) (log (neg y)) (log (* (neg y) (neg x))))

explain52.1s (3.1%)

Memory
-1 264.8MiB live, 59 976.2MiB allocated; 19.0s collecting garbage
Explanations
Click to see full explanations table
OperatorSubexpressionExplanationCount
log.f64#fsensitivity15993
/.f64#fo/n11120
sqrt.f64#foflow-rescue7710
-.f64#fcancellation5809
/.f64#fo/o5730
*.f64#fn*o5310
-.f64#fnan-rescue4850
+.f64#fnan-rescue4800
cos.f64#fsensitivity3712
+.f64#fcancellation3315
/.f64#fn/o3130
/.f64#fu/n2540
sin.f64#fsensitivity2240
*.f64#fn*u2040
/.f64#fn/u1420
cos.f64#foflow-rescue1330
/.f64#fu/u1090
log.f64#foflow-rescue930
tan.f64(tan.f64 (/.f64 x (*.f64 y #s(literal 2 binary64))))sensitivity920
log.f64#fuflow-rescue690
sqrt.f64#fuflow-rescue470
*.f64#fo*u420
sin.f64(sin.f64 (/.f64 x (*.f64 y #s(literal 2 binary64))))oflow-rescue380
↳(/.f64 x (*.f64 y #s(literal 2 binary64)))overflow38
tan.f64(tan.f64 (/.f64 x (*.f64 y #s(literal 2 binary64))))oflow-rescue380
↳(/.f64 x (*.f64 y #s(literal 2 binary64)))overflow38
exp.f64#fsensitivity273
*.f64#fu*o30
Confusion
Predicted +Predicted -
+5945196
-178460939
Precision
0.7691810065985251
Recall
0.9680833740433155
Confusion?
Predicted +Predicted MaybePredicted -
+59453193
-17842060919
Precision?
0.7672858617131063
Recall?
0.9685718938283667
Freqs
test
numberfreq
061135
16904
2746
357
418
52
62
Total Confusion?
Predicted +Predicted MaybePredicted -
+13710
-30128
Precision?
0.9787234042553191
Recall?
1.0
Samples
18.2s130 438×0valid
2.5s5 920×1valid
819.0ms1 290×2valid
43.0ms78×3valid
1.0ms2×4valid
Compiler

Compiled 24 442 to 8 402 computations (65.6% saved)

Precisions
Click to see histograms. Total time spent on operations: 10.3s
ival-mult: 3.2s (30.8% of total)
ival-sub: 1.7s (16.3% of total)
ival-div: 1.2s (11.5% of total)
ival-add: 1.1s (10.4% of total)
ival-log: 853.0ms (8.3% of total)
adjust: 747.0ms (7.3% of total)
const: 437.0ms (4.3% of total)
ival-sin: 322.0ms (3.1% of total)
ival-cos: 267.0ms (2.6% of total)
ival-sqrt: 167.0ms (1.6% of total)
ival-true: 109.0ms (1.1% of total)
ival-exp: 87.0ms (0.8% of total)
exact: 63.0ms (0.6% of total)
ival-assert: 55.0ms (0.5% of total)
ival-sinh: 28.0ms (0.3% of total)
ival-tan: 15.0ms (0.1% of total)
ival-cosh: 12.0ms (0.1% of total)
ival-fabs: 11.0ms (0.1% of total)
ival-hypot: 9.0ms (0.1% of total)
ival-tanh: 7.0ms (0.1% of total)
ival-acos: 5.0ms (0% of total)

prune37.3s (2.2%)

Memory
-68.1MiB live, 49 767.7MiB allocated; 12.8s collecting garbage
Counts
418 099 → 13 031
Compiler

Compiled 849 334 to 453 352 computations (46.6% saved)

bsearch32.6s (1.9%)

Memory
486.1MiB live, 37 088.2MiB allocated; 6.3s collecting garbage
Algorithm
1 727×binary-search
985×left-value
Stop Event
1 696×narrow-enough
31×predicate-same
Samples
17.2s137 026×0valid
1.1s3 565×1valid
224.0ms2 924×0invalid
59.0ms163×2valid
4.0ms14×3valid
2.0ms6×1invalid
Compiler

Compiled 964 135 to 691 544 computations (28.3% saved)

Precisions
Click to see histograms. Total time spent on operations: 12.4s
ival-mult: 5.5s (44.4% of total)
ival-sub: 2.0s (16.4% of total)
ival-add: 1.4s (11.1% of total)
ival-div: 856.0ms (6.9% of total)
const: 815.0ms (6.6% of total)
ival-log: 578.0ms (4.6% of total)
ival-sin: 340.0ms (2.7% of total)
adjust: 245.0ms (2% of total)
ival-cos: 182.0ms (1.5% of total)
ival-sqrt: 179.0ms (1.4% of total)
ival-true: 100.0ms (0.8% of total)
ival-assert: 55.0ms (0.4% of total)
exact: 53.0ms (0.4% of total)
ival-exp: 47.0ms (0.4% of total)
ival-tanh: 14.0ms (0.1% of total)
ival-sinh: 14.0ms (0.1% of total)
ival-cosh: 9.0ms (0.1% of total)
ival-fabs: 6.0ms (0% of total)

analyze24.0s (1.4%)

Memory
148.6MiB live, 24 548.3MiB allocated; 9.6s collecting garbage
Algorithm
269×search
Search
ProbabilityValidUnknownPreconditionInfiniteDomainCan'tIter
0%0%99.9%0.1%0%0%0%0
46.8%46.8%53.1%0.1%0%0%0%1
50.5%50.1%49.2%0.1%0%0.6%0%2
58.6%57%40.3%0.1%0%2.6%0%3
65.2%62.7%33.5%0.1%0%3.6%0%4
71.2%68.2%27.5%0.1%0%4.1%0%5
75.9%72.3%23%0.1%0%4.6%0%6
79.8%75.6%19.1%0.1%0%5.1%0%7
81.7%77%17.3%0.1%0%5.6%0%8
84.3%79.3%14.7%0.1%0%5.9%0%9
85.9%80.5%13.2%0.1%0%6.2%0%10
88.5%82.8%10.8%0.1%0%6.2%0%11
89.6%83.6%9.8%0.1%0%6.5%0%12
Compiler

Compiled 3 462 to 2 977 computations (14% saved)

start9.0ms (0%)

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

end2.0ms (0%)

Memory
5.3MiB live, 5.0MiB allocated; 0ms collecting garbage

Profiling

Loading profile data...