Details

Time bar (total: 1.5s)

analyze63.0ms (4.1%)

Algorithm
search
Search
TrueOtherFalseIter
0%99.9%0.1%0
0%99.9%0.1%1
0%99.9%0.1%2
0%99.9%0.1%3
12.5%87.4%0.1%4
31.2%68.7%0.1%5
43.7%56.2%0.1%6
54.6%42.1%3.2%7
63.2%30.4%6.3%8
69.9%21.5%8.7%9
75.3%15.2%9.5%10
79%10.1%10.8%11
82%7%11%12
83.9%4.4%11.8%13
84.7%3.5%11.8%14
Compiler

Compiled 10 to 9 computations (10% saved)

sample23.0ms (1.5%)

Algorithm
intervals
Results
5.0ms201×body128valid
2.0ms23×body1024valid
1.0ms17×body512valid
1.0ms15×body256valid
0.0msbody128invalid
Compiler

Compiled 19 to 19 computations (0% saved)

simplify510.0ms (33%)

Algorithm
egg-herbie
Rules
1131×unsub-neg_binary64_24965
724×exp-prod_binary64_25023
386×cube-prod_binary64_24999
245×exp-sum_binary64_25017
233×sub-neg_binary64_24964
215×exp-diff_binary64_25019
206×neg-sub0_binary64_24966
202×neg-mul-1_binary64_24967
201×swap-sqr_binary64_24938
161×div-sub_binary64_24976
156×distribute-rgt-neg-out_binary64_24931
136×associate-+l-_binary64_24906
124×distribute-rgt-in_binary64_24921
117×distribute-neg-out_binary64_24933
114×associate-+l+_binary64_24904
112×associate--r+_binary64_24907
111×associate-*r*_binary64_24911
107×exp-neg_binary64_25018
104×distribute-lft-in_binary64_24920
100×distribute-lft-neg-out_binary64_24930
97×associate-+r+_binary64_24903
96×sqr-neg_binary64_24985
95×distribute-rgt1-in_binary64_24927
89×associate-*l*_binary64_24912
86×distribute-neg-in_binary64_24932
83×associate--l+_binary64_24908
82×pow-plus_binary64_25034
78×*-commutative_binary64_24902
72×distribute-rgt-out_binary64_24924
71×associate-+r-_binary64_24905
66×+-commutative_binary64_24901
65×cancel-sign-sub-inv_binary64_24937
56×associate--r-_binary64_24910
51×distribute-rgt-neg-in_binary64_24929
41×associate--l-_binary64_24909
39×associate-*l/_binary64_24914
35×sub0-neg_binary64_24958
30×distribute-rgt-out--_binary64_24925
23×+-rgt-identity_binary64_24956
21×sqr-pow_binary64_24943 distribute-lft-neg-in_binary64_24928
18×*-rgt-identity_binary64_24961
17×remove-double-neg_binary64_24959
16×exp-lft-sqr_binary64_25026
13×mul0-rgt_binary64_24954
12×pow-base-1_binary64_25031 mul0-lft_binary64_24953
11×pow-sqr_binary64_24944
10×distribute-lft1-in_binary64_24926
*-lft-identity_binary64_24960
cube-neg_binary64_24998 distribute-lft-out_binary64_24922
prod-exp_binary64_25020 cube-div_binary64_25000 cancel-sign-sub_binary64_24936 count-2_binary64_24919
cube-unmult_binary64_25008 times-frac_binary64_24977 mul-1-neg_binary64_24963
--rgt-identity_binary64_24957 +-lft-identity_binary64_24955 +-inverses_binary64_24950 distribute-lft-out--_binary64_24923
1-exp_binary64_25015 exp-1-e_binary64_25014 difference-of-squares_binary64_24940 distribute-neg-frac_binary64_24935 associate-/l*_binary64_24916 associate-/r*_binary64_24915
not-true not-false not-not not-and not-or and-true-l and-true-r and-false-l and-false-r and-same or-true-l or-true-r or-false-l or-false-r or-same erfc-erf_binary64_25234 erf-erfc_binary64_25233 erf-odd_binary64_25232 if-if-and-not_binary64_25231 if-if-and_binary64_25230 if-if-or-not_binary64_25229 if-if-or_binary64_25228 if-not_binary64_25227 if-same_binary64_25226 if-false_binary64_25225 if-true_binary64_25224 not-gte_binary64_25223 not-lte_binary64_25222 not-gt_binary64_25221 not-lt_binary64_25220 gte-same_binary64_25219 lte-same_binary64_25218 gt-same_binary64_25217 lt-same_binary64_25216 sinh---cosh_binary64_25163 sinh-+-cosh_binary64_25162 sinh-cosh_binary64_25161 tanh-def-c_binary64_25160 tanh-def-b_binary64_25159 tanh-def-a_binary64_25158 cosh-def_binary64_25157 sinh-def_binary64_25156 tan-neg_binary64_25103 cos-neg_binary64_25102 sin-neg_binary64_25101 tan-0_binary64_25100 cos-0_binary64_25099 sin-0_binary64_25098 hang-m-tan_binary64_25097 hang-p-tan_binary64_25096 hang-m0-tan_binary64_25095 hang-p0-tan_binary64_25094 hang-0m-tan_binary64_25093 hang-0p-tan_binary64_25092 tan-+PI/2_binary64_25091 tan-+PI_binary64_25090 tan-PI_binary64_25089 tan-PI/3_binary64_25088 tan-PI/4_binary64_25087 tan-PI/6_binary64_25086 cos-+PI/2_binary64_25085 cos-+PI_binary64_25084 cos-PI_binary64_25083 cos-PI/2_binary64_25082 cos-PI/3_binary64_25081 cos-PI/4_binary64_25080 cos-PI/6_binary64_25079 sin-+PI/2_binary64_25078 sin-+PI_binary64_25077 sin-PI_binary64_25076 sin-PI/2_binary64_25075 sin-PI/3_binary64_25074 sin-PI/4_binary64_25073 sin-PI/6_binary64_25072 sub-1-sin_binary64_25071 sub-1-cos_binary64_25070 -1-add-sin_binary64_25069 -1-add-cos_binary64_25068 1-sub-sin_binary64_25067 1-sub-cos_binary64_25066 cos-sin-sum_binary64_25065 log-E_binary64_25061 log-pow_binary64_25060 log-rec_binary64_25059 log-div_binary64_25058 log-prod_binary64_25057 pow-base-0_binary64_25055 unpow1/3_binary64_25038 unpow3_binary64_25037 unpow2_binary64_25036 unpow1/2_binary64_25035 exp-to-pow_binary64_25033 unpow0_binary64_25030 unpow1_binary64_25029 unpow-1_binary64_25028 exp-lft-cube_binary64_25027 exp-cbrt_binary64_25025 exp-sqrt_binary64_25024 div-exp_binary64_25022 rec-exp_binary64_25021 e-exp-1_binary64_25016 exp-0_binary64_25013 rem-log-exp_binary64_25012 rem-exp-log_binary64_25011 cube-mult_binary64_25001 rem-3cbrt-rft_binary64_24997 rem-3cbrt-lft_binary64_24996 rem-cbrt-cube_binary64_24995 rem-cube-cbrt_binary64_24994 sqr-abs_binary64_24986 rem-sqrt-square_binary64_24984 rem-square-sqrt_binary64_24983 /-rgt-identity_binary64_24962 div0_binary64_24952 *-inverses_binary64_24951 lft-mult-inverse_binary64_24949 rgt-mult-inverse_binary64_24948 remove-double-div_binary64_24947 difference-of-sqr--1_binary64_24942 difference-of-sqr-1_binary64_24941 unswap-sqr_binary64_24939 distribute-frac-neg_binary64_24934 associate-/l/_binary64_24918 associate-/r/_binary64_24917 associate-*r/_binary64_24913
Counts
1 → 2
Iterations

Useful iterations: 5 (0.0ms)

IterNodesCost
0813
11613
23513
39113
429413
581410
6146510
7234610

prune4.0ms (0.3%)

Pruning

1 alts after pruning (1 fresh and 0 done)

PrunedKeptTotal
New112
Fresh101
Picked000
Done000
Total213
Error
0.0b
Counts
3 → 1
Compiler

Compiled 21 to 17 computations (19% saved)

localize4.0ms (0.3%)

Local error

Found 1 expressions with local error:

0.0b
(-.f64 (*.f64 x y) y)

rewrite21.0ms (1.3%)

Algorithm
rewrite-expression-head
Error
0.0b
Rules
add-log-exp_binary64_25010 *-un-lft-identity_binary64_24971 cancel-sign-sub-inv_binary64_24937
add-cube-cbrt_binary64_25006 add-sqr-sqrt_binary64_24993
diff-log_binary64_25063 pow1_binary64_25032 add-exp-log_binary64_25009 add-cbrt-cube_binary64_25007 flip3--_binary64_24975 sub-neg_binary64_24964 flip--_binary64_24946 distribute-rgt-out--_binary64_24925
Counts
1 → 15
Calls

1 calls:

4.0ms
(-.f64 (*.f64 x y) y)
Compiler

Compiled 203 to 86 computations (57.6% saved)

series92.0ms (5.9%)

Error
0.0b
Counts
1 → 9
Calls

1 calls:

86.0ms
(-.f64 (*.f64 x y) y)
Compiler

Compiled 162 to 133 computations (17.9% saved)

simplify119.0ms (7.7%)

Algorithm
egg-herbie
Rules
476×unswap-sqr_binary64_24939
412×unsub-neg_binary64_24965
395×cancel-sign-sub-inv_binary64_24937
248×associate-*l*_binary64_24912
235×exp-prod_binary64_25023
219×associate-*r*_binary64_24911
200×*-commutative_binary64_24902
178×distribute-rgt-out_binary64_24924
165×neg-sub0_binary64_24966
152×sqr-pow_binary64_24943
148×neg-mul-1_binary64_24967 difference-of-squares_binary64_24940
146×cube-prod_binary64_24999
135×log-prod_binary64_25057
116×distribute-lft-out_binary64_24922
100×distribute-rgt-neg-out_binary64_24931
91×distribute-lft-neg-out_binary64_24930
78×sub-neg_binary64_24964
73×times-frac_binary64_24977
72×exp-sum_binary64_25017
64×swap-sqr_binary64_24938
55×pow-sqr_binary64_24944 associate-+r+_binary64_24903
53×distribute-rgt-out--_binary64_24925
48×distribute-rgt-in_binary64_24921 associate-+l+_binary64_24904
44×distribute-lft-in_binary64_24920
39×+-commutative_binary64_24901
34×exp-diff_binary64_25019
29×distribute-rgt-neg-in_binary64_24929
28×distribute-lft-out--_binary64_24923
24×remove-double-neg_binary64_24959
23×unpow3_binary64_25037 distribute-lft-neg-in_binary64_24928
20×+-rgt-identity_binary64_24956
19×sqr-neg_binary64_24985 *-rgt-identity_binary64_24961 associate-+l-_binary64_24906
18×cube-mult_binary64_25001 associate-+r-_binary64_24905
16×exp-neg_binary64_25018
15×*-lft-identity_binary64_24960
13×div-sub_binary64_24976 sub0-neg_binary64_24958
12×distribute-neg-in_binary64_24932 associate-/l*_binary64_24916
11×cube-neg_binary64_24998 mul0-rgt_binary64_24954 mul0-lft_binary64_24953
10×associate--r+_binary64_24907
cube-unmult_binary64_25008 associate-/l/_binary64_24918
associate-*r/_binary64_24913
pow-plus_binary64_25034 mul-1-neg_binary64_24963 +-lft-identity_binary64_24955
associate-/r/_binary64_24917 associate-/r*_binary64_24915
distribute-rgt1-in_binary64_24927 distribute-lft1-in_binary64_24926
--rgt-identity_binary64_24957
log-pow_binary64_25060 pow-base-1_binary64_25031 rem-sqrt-square_binary64_24984 difference-of-sqr--1_binary64_24942 associate--r-_binary64_24910
div-exp_binary64_25022 prod-exp_binary64_25020 1-exp_binary64_25015 exp-1-e_binary64_25014 rem-log-exp_binary64_25012 rem-3cbrt-lft_binary64_24996 rem-square-sqrt_binary64_24983 /-rgt-identity_binary64_24962 *-inverses_binary64_24951 difference-of-sqr-1_binary64_24941 count-2_binary64_24919 associate-*l/_binary64_24914
not-true not-false not-not not-and not-or and-true-l and-true-r and-false-l and-false-r and-same or-true-l or-true-r or-false-l or-false-r or-same erfc-erf_binary64_25234 erf-erfc_binary64_25233 erf-odd_binary64_25232 if-if-and-not_binary64_25231 if-if-and_binary64_25230 if-if-or-not_binary64_25229 if-if-or_binary64_25228 if-not_binary64_25227 if-same_binary64_25226 if-false_binary64_25225 if-true_binary64_25224 not-gte_binary64_25223 not-lte_binary64_25222 not-gt_binary64_25221 not-lt_binary64_25220 gte-same_binary64_25219 lte-same_binary64_25218 gt-same_binary64_25217 lt-same_binary64_25216 sinh---cosh_binary64_25163 sinh-+-cosh_binary64_25162 sinh-cosh_binary64_25161 tanh-def-c_binary64_25160 tanh-def-b_binary64_25159 tanh-def-a_binary64_25158 cosh-def_binary64_25157 sinh-def_binary64_25156 tan-neg_binary64_25103 cos-neg_binary64_25102 sin-neg_binary64_25101 tan-0_binary64_25100 cos-0_binary64_25099 sin-0_binary64_25098 hang-m-tan_binary64_25097 hang-p-tan_binary64_25096 hang-m0-tan_binary64_25095 hang-p0-tan_binary64_25094 hang-0m-tan_binary64_25093 hang-0p-tan_binary64_25092 tan-+PI/2_binary64_25091 tan-+PI_binary64_25090 tan-PI_binary64_25089 tan-PI/3_binary64_25088 tan-PI/4_binary64_25087 tan-PI/6_binary64_25086 cos-+PI/2_binary64_25085 cos-+PI_binary64_25084 cos-PI_binary64_25083 cos-PI/2_binary64_25082 cos-PI/3_binary64_25081 cos-PI/4_binary64_25080 cos-PI/6_binary64_25079 sin-+PI/2_binary64_25078 sin-+PI_binary64_25077 sin-PI_binary64_25076 sin-PI/2_binary64_25075 sin-PI/3_binary64_25074 sin-PI/4_binary64_25073 sin-PI/6_binary64_25072 sub-1-sin_binary64_25071 sub-1-cos_binary64_25070 -1-add-sin_binary64_25069 -1-add-cos_binary64_25068 1-sub-sin_binary64_25067 1-sub-cos_binary64_25066 cos-sin-sum_binary64_25065 log-E_binary64_25061 log-rec_binary64_25059 log-div_binary64_25058 pow-base-0_binary64_25055 unpow1/3_binary64_25038 unpow2_binary64_25036 unpow1/2_binary64_25035 exp-to-pow_binary64_25033 unpow0_binary64_25030 unpow1_binary64_25029 unpow-1_binary64_25028 exp-lft-cube_binary64_25027 exp-lft-sqr_binary64_25026 exp-cbrt_binary64_25025 exp-sqrt_binary64_25024 rec-exp_binary64_25021 e-exp-1_binary64_25016 exp-0_binary64_25013 rem-exp-log_binary64_25011 cube-div_binary64_25000 rem-3cbrt-rft_binary64_24997 rem-cbrt-cube_binary64_24995 rem-cube-cbrt_binary64_24994 sqr-abs_binary64_24986 div0_binary64_24952 +-inverses_binary64_24950 lft-mult-inverse_binary64_24949 rgt-mult-inverse_binary64_24948 remove-double-div_binary64_24947 cancel-sign-sub_binary64_24936 distribute-neg-frac_binary64_24935 distribute-frac-neg_binary64_24934 distribute-neg-out_binary64_24933 associate--l-_binary64_24909 associate--l+_binary64_24908
Counts
24 → 69
Iterations

Useful iterations: 2 (0.0ms)

IterNodesCost
044226
1114208
2255202
31197202
42483202

prune56.0ms (3.6%)

Pruning

1 alts after pruning (0 fresh and 1 done)

PrunedKeptTotal
New69069
Fresh000
Picked011
Done000
Total69170
Error
0.0b
Counts
70 → 1
Compiler

Compiled 1042 to 442 computations (57.6% saved)

regimes46.0ms (3%)

Accuracy

Total 0.0b remaining (66.7%)

Threshold costs 0.0b (66.7%)

Compiler

Compiled 168 to 172 computations (-2.4% saved)

bsearch0.0ms (0%)

simplify3.0ms (0.2%)

Algorithm
egg-herbie
Rules
+-commutative_binary64_24901
sub-neg_binary64_24964 *-commutative_binary64_24902
1-exp_binary64_25015 neg-mul-1_binary64_24967 neg-sub0_binary64_24966
not-true not-false not-not not-and not-or and-true-l and-true-r and-false-l and-false-r and-same or-true-l or-true-r or-false-l or-false-r or-same if-if-and-not_binary64_25231 if-if-and_binary64_25230 if-if-or-not_binary64_25229 if-if-or_binary64_25228 if-not_binary64_25227 if-same_binary64_25226 if-false_binary64_25225 if-true_binary64_25224 tan-0_binary64_25100 cos-0_binary64_25099 sin-0_binary64_25098 unpow1_binary64_25029 e-exp-1_binary64_25016 exp-1-e_binary64_25014 exp-0_binary64_25013 sqr-abs_binary64_24986 sqr-neg_binary64_24985 unsub-neg_binary64_24965 mul-1-neg_binary64_24963 /-rgt-identity_binary64_24962 *-rgt-identity_binary64_24961 *-lft-identity_binary64_24960 remove-double-neg_binary64_24959 sub0-neg_binary64_24958 --rgt-identity_binary64_24957 +-rgt-identity_binary64_24956 +-lft-identity_binary64_24955 cancel-sign-sub-inv_binary64_24937 cancel-sign-sub_binary64_24936 distribute-neg-frac_binary64_24935 distribute-frac-neg_binary64_24934 distribute-neg-out_binary64_24933 distribute-neg-in_binary64_24932 distribute-rgt-neg-out_binary64_24931 distribute-lft-neg-out_binary64_24930 distribute-rgt-neg-in_binary64_24929 distribute-lft-neg-in_binary64_24928
Iterations

Useful iterations: 0 (0.0ms)

IterNodesCost
0710
11310
21710
31910
42010
Proof
(+ f64 1 (- f64 (* f64 h0 h1) h1))

end0.0ms (0%)

sample605.0ms (39.1%)

Algorithm
intervals
Results
153.0ms6031×body128valid
62.0ms679×body1024valid
51.0ms800×body512valid
21.0ms481×body256valid
2.0ms69×body128invalid
1.0msbody2048valid
Compiler

Compiled 59 to 58 computations (1.7% saved)

Profiling

Loading profile data...