Details

Time bar (total: 23.3s)

analyze250.0ms (1.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
0%99.9%0.1%4
0%99.9%0.1%5
12.5%87.4%0.1%6
28.1%71.8%0.1%7
42.1%57.7%0.1%8
43.7%56.2%0.1%9
64.4%35.5%0.1%10
71.6%28.3%0.1%11
72.2%27.7%0.1%12
81.6%18.2%0.2%13
84.9%14.9%0.2%14
Compiler

Compiled 13 to 9 computations (30.8% saved)

sample19.0ms (0.1%)

Algorithm
intervals
Results
8.0ms256×body128valid
0.0ms10×body128invalid
Compiler

Compiled 25 to 20 computations (20% saved)

simplify472.0ms (2%)

Algorithm
egg-herbie
Rules
912×cancel-sign-sub-inv_binary64_44
845×distribute-rgt-out_binary64_31
629×distribute-rgt-in_binary64_28
607×distribute-lft-in_binary64_27
283×associate-/l/_binary64_25
251×distribute-neg-frac_binary64_42
224×associate-/l*_binary64_23
159×distribute-rgt-neg-in_binary64_36
79×distribute-lft-out_binary64_29
74×associate-*l*_binary64_19
59×times-frac_binary64_84
49×associate-/r/_binary64_24
37×div-sub_binary64_83
33×distribute-rgt1-in_binary64_34
26×distribute-lft-neg-in_binary64_35 associate-*r/_binary64_20
25×associate-*r*_binary64_18
24×swap-sqr_binary64_45 associate-*l/_binary64_21 associate-+l+_binary64_11 *-commutative_binary64_9
20×sub-neg_binary64_71 associate-/r*_binary64_22
15×distribute-frac-neg_binary64_41 associate-+r+_binary64_10
12×neg-mul-1_binary64_74 neg-sub0_binary64_73
11×distribute-neg-in_binary64_39
mul0-rgt_binary64_61 +-commutative_binary64_8
unsub-neg_binary64_72 distribute-lft-neg-out_binary64_37 distribute-lft1-in_binary64_33
div0_binary64_59 distribute-rgt-neg-out_binary64_38 distribute-rgt-out--_binary64_32 associate-+l-_binary64_13
cube-unmult_binary64_115 unswap-sqr_binary64_46 count-2_binary64_26
sub0-neg_binary64_65 --rgt-identity_binary64_64 mul0-lft_binary64_60
1-exp_binary64_122 mul-1-neg_binary64_70 +-rgt-identity_binary64_63 +-lft-identity_binary64_62 associate-+r-_binary64_12
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_341 erf-erfc_binary64_340 erf-odd_binary64_339 if-if-and-not_binary64_338 if-if-and_binary64_337 if-if-or-not_binary64_336 if-if-or_binary64_335 if-not_binary64_334 if-same_binary64_333 if-false_binary64_332 if-true_binary64_331 not-gte_binary64_330 not-lte_binary64_329 not-gt_binary64_328 not-lt_binary64_327 gte-same_binary64_326 lte-same_binary64_325 gt-same_binary64_324 lt-same_binary64_323 sinh---cosh_binary64_270 sinh-+-cosh_binary64_269 sinh-cosh_binary64_268 tanh-def-c_binary64_267 tanh-def-b_binary64_266 tanh-def-a_binary64_265 cosh-def_binary64_264 sinh-def_binary64_263 tan-neg_binary64_210 cos-neg_binary64_209 sin-neg_binary64_208 tan-0_binary64_207 cos-0_binary64_206 sin-0_binary64_205 hang-m-tan_binary64_204 hang-p-tan_binary64_203 hang-m0-tan_binary64_202 hang-p0-tan_binary64_201 hang-0m-tan_binary64_200 hang-0p-tan_binary64_199 tan-+PI/2_binary64_198 tan-+PI_binary64_197 tan-PI_binary64_196 tan-PI/3_binary64_195 tan-PI/4_binary64_194 tan-PI/6_binary64_193 cos-+PI/2_binary64_192 cos-+PI_binary64_191 cos-PI_binary64_190 cos-PI/2_binary64_189 cos-PI/3_binary64_188 cos-PI/4_binary64_187 cos-PI/6_binary64_186 sin-+PI/2_binary64_185 sin-+PI_binary64_184 sin-PI_binary64_183 sin-PI/2_binary64_182 sin-PI/3_binary64_181 sin-PI/4_binary64_180 sin-PI/6_binary64_179 sub-1-sin_binary64_178 sub-1-cos_binary64_177 -1-add-sin_binary64_176 -1-add-cos_binary64_175 1-sub-sin_binary64_174 1-sub-cos_binary64_173 cos-sin-sum_binary64_172 log-E_binary64_168 log-pow_binary64_167 log-rec_binary64_166 log-div_binary64_165 log-prod_binary64_164 pow-base-0_binary64_162 unpow1/3_binary64_145 unpow3_binary64_144 unpow2_binary64_143 unpow1/2_binary64_142 pow-plus_binary64_141 exp-to-pow_binary64_140 pow-base-1_binary64_138 unpow0_binary64_137 unpow1_binary64_136 unpow-1_binary64_135 exp-lft-cube_binary64_134 exp-lft-sqr_binary64_133 exp-cbrt_binary64_132 exp-sqrt_binary64_131 exp-prod_binary64_130 div-exp_binary64_129 rec-exp_binary64_128 prod-exp_binary64_127 exp-diff_binary64_126 exp-neg_binary64_125 exp-sum_binary64_124 e-exp-1_binary64_123 exp-1-e_binary64_121 exp-0_binary64_120 rem-log-exp_binary64_119 rem-exp-log_binary64_118 cube-mult_binary64_108 cube-div_binary64_107 cube-prod_binary64_106 cube-neg_binary64_105 rem-3cbrt-rft_binary64_104 rem-3cbrt-lft_binary64_103 rem-cbrt-cube_binary64_102 rem-cube-cbrt_binary64_101 sqr-abs_binary64_93 sqr-neg_binary64_92 rem-sqrt-square_binary64_91 rem-square-sqrt_binary64_90 /-rgt-identity_binary64_69 *-rgt-identity_binary64_68 *-lft-identity_binary64_67 remove-double-neg_binary64_66 *-inverses_binary64_58 +-inverses_binary64_57 lft-mult-inverse_binary64_56 rgt-mult-inverse_binary64_55 remove-double-div_binary64_54 pow-sqr_binary64_51 sqr-pow_binary64_50 difference-of-sqr--1_binary64_49 difference-of-sqr-1_binary64_48 difference-of-squares_binary64_47 cancel-sign-sub_binary64_43 distribute-neg-out_binary64_40 distribute-lft-out--_binary64_30 associate--r-_binary64_17 associate--l-_binary64_16 associate--l+_binary64_15 associate--r+_binary64_14
Counts
1 → 5
Iterations

Useful iterations: 0 (0.0ms)

IterNodesCost
0918
13018
28318
318718
433718
5129018

prune13.0ms (0.1%)

Pruning

6 alts after pruning (6 fresh and 0 done)

PrunedKeptTotal
New055
Fresh011
Picked000
Done000
Total066
Error
0.0b
Counts
6 → 6
Compiler

Compiled 132 to 67 computations (49.2% saved)

localize11.0ms (0%)

Local error

Found 3 expressions with local error:

0.0b
(/.f64 (neg.f64 v) (+.f64 t1 u))
0.0b
(/.f64 (+.f64 t1 u) t1)
1.4b
(/.f64 (/.f64 (neg.f64 v) (+.f64 t1 u)) (/.f64 (+.f64 t1 u) t1))

rewrite1.3s (5.5%)

Algorithm
rewrite-expression-head
Error
0b
Rules
2032×times-frac_binary64_84
1457×*-un-lft-identity_binary64_78
805×add-cube-cbrt_binary64_113 add-sqr-sqrt_binary64_100
326×distribute-lft-out_binary64_29
219×distribute-rgt-neg-in_binary64_36 distribute-lft-neg-in_binary64_35
73×neg-mul-1_binary64_74
67×div-inv_binary64_75
60×associate-/l*_binary64_23
37×associate-/r/_binary64_24
23×associate-/r*_binary64_22
19×add-exp-log_binary64_116 add-cbrt-cube_binary64_114 flip3-+_binary64_81 flip-+_binary64_52
10×div-exp_binary64_129 cbrt-undiv_binary64_112
pow1_binary64_139 add-log-exp_binary64_117 frac-2neg_binary64_89 div-sub_binary64_83 clear-num_binary64_77 distribute-frac-neg_binary64_41 associate-/l/_binary64_25
neg-sub0_binary64_73
Counts
3 → 923
Calls

3 calls:

32.0ms
(/.f64 (/.f64 (neg.f64 v) (+.f64 t1 u)) (/.f64 (+.f64 t1 u) t1))
6.0ms
(/.f64 (neg.f64 v) (+.f64 t1 u))
5.0ms
(/.f64 (+.f64 t1 u) t1)
Compiler

Compiled 26169 to 4726 computations (81.9% saved)

series506.0ms (2.2%)

Error
0.0b
Counts
3 → 39
Calls

3 calls:

240.0ms
(/.f64 (/.f64 (neg.f64 v) (+.f64 t1 u)) (/.f64 (+.f64 t1 u) t1))
137.0ms
(/.f64 (neg.f64 v) (+.f64 t1 u))
99.0ms
(/.f64 (+.f64 t1 u) t1)
Compiler

Compiled 1380 to 894 computations (35.2% saved)

simplify1.9s (8.2%)

Algorithm
egg-herbie
Rules
745×associate-/r*_binary64_22
684×associate-/l/_binary64_25
568×associate-/r/_binary64_24
406×div-sub_binary64_83
367×distribute-frac-neg_binary64_41
121×distribute-rgt-in_binary64_28
114×distribute-lft-in_binary64_27
68×/-rgt-identity_binary64_69
48×distribute-lft-neg-out_binary64_37
47×neg-sub0_binary64_73
44×neg-mul-1_binary64_74
35×sub-neg_binary64_71
29×associate-/l*_binary64_23
23×distribute-rgt-neg-out_binary64_38
18×distribute-rgt-neg-in_binary64_36
17×unswap-sqr_binary64_46
14×*-commutative_binary64_9
12×cancel-sign-sub-inv_binary64_44 associate-*r/_binary64_20
11×*-rgt-identity_binary64_68 distribute-neg-frac_binary64_42 distribute-lft-neg-in_binary64_35
10×sqr-pow_binary64_50
mul-1-neg_binary64_70
log-div_binary64_165
times-frac_binary64_84
log-prod_binary64_164 cube-unmult_binary64_115 swap-sqr_binary64_45 +-commutative_binary64_8
*-lft-identity_binary64_67 pow-sqr_binary64_51 associate-*l*_binary64_19
exp-prod_binary64_130 difference-of-squares_binary64_47 associate-*l/_binary64_21
unpow2_binary64_143 pow-plus_binary64_141 sqr-neg_binary64_92 cancel-sign-sub_binary64_43 distribute-neg-in_binary64_39
unpow3_binary64_144 cube-mult_binary64_108 remove-double-div_binary64_54
div-exp_binary64_129 rec-exp_binary64_128 prod-exp_binary64_127 exp-neg_binary64_125 1-exp_binary64_122 rem-square-sqrt_binary64_90 unsub-neg_binary64_72 remove-double-neg_binary64_66 mul0-lft_binary64_60 div0_binary64_59 *-inverses_binary64_58 distribute-rgt-out--_binary64_32 associate-*r*_binary64_18 associate--r-_binary64_17 associate--l-_binary64_16 associate-+r-_binary64_12 associate-+r+_binary64_10
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_341 erf-erfc_binary64_340 erf-odd_binary64_339 if-if-and-not_binary64_338 if-if-and_binary64_337 if-if-or-not_binary64_336 if-if-or_binary64_335 if-not_binary64_334 if-same_binary64_333 if-false_binary64_332 if-true_binary64_331 not-gte_binary64_330 not-lte_binary64_329 not-gt_binary64_328 not-lt_binary64_327 gte-same_binary64_326 lte-same_binary64_325 gt-same_binary64_324 lt-same_binary64_323 sinh---cosh_binary64_270 sinh-+-cosh_binary64_269 sinh-cosh_binary64_268 tanh-def-c_binary64_267 tanh-def-b_binary64_266 tanh-def-a_binary64_265 cosh-def_binary64_264 sinh-def_binary64_263 tan-neg_binary64_210 cos-neg_binary64_209 sin-neg_binary64_208 tan-0_binary64_207 cos-0_binary64_206 sin-0_binary64_205 hang-m-tan_binary64_204 hang-p-tan_binary64_203 hang-m0-tan_binary64_202 hang-p0-tan_binary64_201 hang-0m-tan_binary64_200 hang-0p-tan_binary64_199 tan-+PI/2_binary64_198 tan-+PI_binary64_197 tan-PI_binary64_196 tan-PI/3_binary64_195 tan-PI/4_binary64_194 tan-PI/6_binary64_193 cos-+PI/2_binary64_192 cos-+PI_binary64_191 cos-PI_binary64_190 cos-PI/2_binary64_189 cos-PI/3_binary64_188 cos-PI/4_binary64_187 cos-PI/6_binary64_186 sin-+PI/2_binary64_185 sin-+PI_binary64_184 sin-PI_binary64_183 sin-PI/2_binary64_182 sin-PI/3_binary64_181 sin-PI/4_binary64_180 sin-PI/6_binary64_179 sub-1-sin_binary64_178 sub-1-cos_binary64_177 -1-add-sin_binary64_176 -1-add-cos_binary64_175 1-sub-sin_binary64_174 1-sub-cos_binary64_173 cos-sin-sum_binary64_172 log-E_binary64_168 log-pow_binary64_167 log-rec_binary64_166 pow-base-0_binary64_162 unpow1/3_binary64_145 unpow1/2_binary64_142 exp-to-pow_binary64_140 pow-base-1_binary64_138 unpow0_binary64_137 unpow1_binary64_136 unpow-1_binary64_135 exp-lft-cube_binary64_134 exp-lft-sqr_binary64_133 exp-cbrt_binary64_132 exp-sqrt_binary64_131 exp-diff_binary64_126 exp-sum_binary64_124 e-exp-1_binary64_123 exp-1-e_binary64_121 exp-0_binary64_120 rem-log-exp_binary64_119 rem-exp-log_binary64_118 cube-div_binary64_107 cube-prod_binary64_106 cube-neg_binary64_105 rem-3cbrt-rft_binary64_104 rem-3cbrt-lft_binary64_103 rem-cbrt-cube_binary64_102 rem-cube-cbrt_binary64_101 sqr-abs_binary64_93 rem-sqrt-square_binary64_91 sub0-neg_binary64_65 --rgt-identity_binary64_64 +-rgt-identity_binary64_63 +-lft-identity_binary64_62 mul0-rgt_binary64_61 +-inverses_binary64_57 lft-mult-inverse_binary64_56 rgt-mult-inverse_binary64_55 difference-of-sqr--1_binary64_49 difference-of-sqr-1_binary64_48 distribute-neg-out_binary64_40 distribute-rgt1-in_binary64_34 distribute-lft1-in_binary64_33 distribute-rgt-out_binary64_31 distribute-lft-out--_binary64_30 distribute-lft-out_binary64_29 count-2_binary64_26 associate--l+_binary64_15 associate--r+_binary64_14 associate-+l-_binary64_13 associate-+l+_binary64_11
Counts
962 → 3529
Iterations

Useful iterations: 1 (0.0ms)

IterNodesCost
0100335067
1267133841

prune4.1s (17.4%)

Pruning

8 alts after pruning (7 fresh and 1 done)

PrunedKeptTotal
New352453529
Fresh325
Picked011
Done000
Total352783535
Error
0b
Counts
3535 → 8
Compiler

Compiled 99886 to 11083 computations (88.9% saved)

localize9.0ms (0%)

Local error

Found 4 expressions with local error:

0.0b
(/.f64 -1 (+.f64 t1 u))
0.0b
(/.f64 v (+.f64 t1 u))
0.2b
(*.f64 (/.f64 -1 (+.f64 t1 u)) (/.f64 (/.f64 v (+.f64 t1 u)) (/.f64 1 t1)))
6.8b
(/.f64 (/.f64 v (+.f64 t1 u)) (/.f64 1 t1))

rewrite1.5s (6.4%)

Algorithm
rewrite-expression-head
Error
0b
Rules
1194×times-frac_binary64_84
694×*-un-lft-identity_binary64_78
563×add-sqr-sqrt_binary64_100
506×add-cube-cbrt_binary64_113
239×associate-*r*_binary64_18
103×add-exp-log_binary64_116
92×distribute-lft-out_binary64_29
69×div-inv_binary64_75
62×associate-/r/_binary64_24
61×add-cbrt-cube_binary64_114
59×div-exp_binary64_129
31×cbrt-undiv_binary64_112
30×flip3-+_binary64_81 flip-+_binary64_52
24×associate-/l*_binary64_23
21×associate-/r*_binary64_22
18×prod-exp_binary64_127 associate-*l*_binary64_19
14×unswap-sqr_binary64_46
10×cbrt-unprod_binary64_111
pow1_binary64_139 1-exp_binary64_122 rec-exp_binary64_128
add-log-exp_binary64_117
frac-2neg_binary64_89 clear-num_binary64_77
associate-/l/_binary64_25 pow-prod-down_binary64_149 frac-times_binary64_88 associate-*l/_binary64_21 associate-*r/_binary64_20 *-commutative_binary64_9
Counts
4 → 666
Calls

4 calls:

113.0ms
(*.f64 (/.f64 -1 (+.f64 t1 u)) (/.f64 (/.f64 v (+.f64 t1 u)) (/.f64 1 t1)))
15.0ms
(/.f64 (/.f64 v (+.f64 t1 u)) (/.f64 1 t1))
5.0ms
(/.f64 v (+.f64 t1 u))
5.0ms
(/.f64 -1 (+.f64 t1 u))
Compiler

Compiled 19851 to 8561 computations (56.9% saved)

series648.0ms (2.8%)

Error
0b
Counts
4 → 57
Calls

4 calls:

226.0ms
(*.f64 (/.f64 -1 (+.f64 t1 u)) (/.f64 (/.f64 v (+.f64 t1 u)) (/.f64 1 t1)))
156.0ms
(/.f64 (/.f64 v (+.f64 t1 u)) (/.f64 1 t1))
130.0ms
(/.f64 v (+.f64 t1 u))
88.0ms
(/.f64 -1 (+.f64 t1 u))
Compiler

Compiled 2493 to 1703 computations (31.7% saved)

simplify1.5s (6.4%)

Algorithm
egg-herbie
Rules
682×associate-/r/_binary64_24
528×associate-*l*_binary64_19
498×times-frac_binary64_84
402×associate-/r*_binary64_22
249×associate-/l/_binary64_25
208×*-commutative_binary64_9
204×associate-*r/_binary64_20
184×associate-*l/_binary64_21
162×mul-1-neg_binary64_70
99×distribute-rgt-in_binary64_28
93×distribute-lft-in_binary64_27
45×div-sub_binary64_83
39×sub-neg_binary64_71
37×/-rgt-identity_binary64_69
33×associate-/l*_binary64_23
22×neg-sub0_binary64_73
18×neg-mul-1_binary64_74
16×*-rgt-identity_binary64_68 distribute-neg-frac_binary64_42 distribute-frac-neg_binary64_41
15×log-div_binary64_165
14×unswap-sqr_binary64_46
11×sqr-pow_binary64_50
10×cancel-sign-sub-inv_binary64_44
cube-unmult_binary64_115
swap-sqr_binary64_45 distribute-rgt-neg-in_binary64_36
log-prod_binary64_164 +-commutative_binary64_8
exp-prod_binary64_130 *-lft-identity_binary64_67 distribute-lft-neg-in_binary64_35 associate-*r*_binary64_18
pow-sqr_binary64_51
difference-of-squares_binary64_47 distribute-neg-in_binary64_39
log-rec_binary64_166 unpow2_binary64_143 pow-plus_binary64_141 remove-double-div_binary64_54
unpow3_binary64_144 cube-mult_binary64_108 unsub-neg_binary64_72 lft-mult-inverse_binary64_56 distribute-lft-neg-out_binary64_37 associate--r-_binary64_17 associate-+r-_binary64_12
div-exp_binary64_129 rec-exp_binary64_128 prod-exp_binary64_127 1-exp_binary64_122 rem-log-exp_binary64_119 cube-div_binary64_107 cube-prod_binary64_106 rem-sqrt-square_binary64_91 *-inverses_binary64_58 distribute-rgt-out--_binary64_32 associate--l-_binary64_16 associate--r+_binary64_14 associate-+l-_binary64_13 associate-+r+_binary64_10
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_341 erf-erfc_binary64_340 erf-odd_binary64_339 if-if-and-not_binary64_338 if-if-and_binary64_337 if-if-or-not_binary64_336 if-if-or_binary64_335 if-not_binary64_334 if-same_binary64_333 if-false_binary64_332 if-true_binary64_331 not-gte_binary64_330 not-lte_binary64_329 not-gt_binary64_328 not-lt_binary64_327 gte-same_binary64_326 lte-same_binary64_325 gt-same_binary64_324 lt-same_binary64_323 sinh---cosh_binary64_270 sinh-+-cosh_binary64_269 sinh-cosh_binary64_268 tanh-def-c_binary64_267 tanh-def-b_binary64_266 tanh-def-a_binary64_265 cosh-def_binary64_264 sinh-def_binary64_263 tan-neg_binary64_210 cos-neg_binary64_209 sin-neg_binary64_208 tan-0_binary64_207 cos-0_binary64_206 sin-0_binary64_205 hang-m-tan_binary64_204 hang-p-tan_binary64_203 hang-m0-tan_binary64_202 hang-p0-tan_binary64_201 hang-0m-tan_binary64_200 hang-0p-tan_binary64_199 tan-+PI/2_binary64_198 tan-+PI_binary64_197 tan-PI_binary64_196 tan-PI/3_binary64_195 tan-PI/4_binary64_194 tan-PI/6_binary64_193 cos-+PI/2_binary64_192 cos-+PI_binary64_191 cos-PI_binary64_190 cos-PI/2_binary64_189 cos-PI/3_binary64_188 cos-PI/4_binary64_187 cos-PI/6_binary64_186 sin-+PI/2_binary64_185 sin-+PI_binary64_184 sin-PI_binary64_183 sin-PI/2_binary64_182 sin-PI/3_binary64_181 sin-PI/4_binary64_180 sin-PI/6_binary64_179 sub-1-sin_binary64_178 sub-1-cos_binary64_177 -1-add-sin_binary64_176 -1-add-cos_binary64_175 1-sub-sin_binary64_174 1-sub-cos_binary64_173 cos-sin-sum_binary64_172 log-E_binary64_168 log-pow_binary64_167 pow-base-0_binary64_162 unpow1/3_binary64_145 unpow1/2_binary64_142 exp-to-pow_binary64_140 pow-base-1_binary64_138 unpow0_binary64_137 unpow1_binary64_136 unpow-1_binary64_135 exp-lft-cube_binary64_134 exp-lft-sqr_binary64_133 exp-cbrt_binary64_132 exp-sqrt_binary64_131 exp-diff_binary64_126 exp-neg_binary64_125 exp-sum_binary64_124 e-exp-1_binary64_123 exp-1-e_binary64_121 exp-0_binary64_120 rem-exp-log_binary64_118 cube-neg_binary64_105 rem-3cbrt-rft_binary64_104 rem-3cbrt-lft_binary64_103 rem-cbrt-cube_binary64_102 rem-cube-cbrt_binary64_101 sqr-abs_binary64_93 sqr-neg_binary64_92 rem-square-sqrt_binary64_90 remove-double-neg_binary64_66 sub0-neg_binary64_65 --rgt-identity_binary64_64 +-rgt-identity_binary64_63 +-lft-identity_binary64_62 mul0-rgt_binary64_61 mul0-lft_binary64_60 div0_binary64_59 +-inverses_binary64_57 rgt-mult-inverse_binary64_55 difference-of-sqr--1_binary64_49 difference-of-sqr-1_binary64_48 cancel-sign-sub_binary64_43 distribute-neg-out_binary64_40 distribute-rgt-neg-out_binary64_38 distribute-rgt1-in_binary64_34 distribute-lft1-in_binary64_33 distribute-rgt-out_binary64_31 distribute-lft-out--_binary64_30 distribute-lft-out_binary64_29 count-2_binary64_26 associate--l+_binary64_15 associate-+l+_binary64_11
Counts
723 → 1927
Iterations

Useful iterations: 1 (0.0ms)

IterNodesCost
080319518
1248518440

prune4.0s (17.2%)

Pruning

8 alts after pruning (6 fresh and 2 done)

PrunedKeptTotal
New192701927
Fresh066
Picked011
Done011
Total192781935
Error
0b
Counts
1935 → 8
Compiler

Compiled 56261 to 21128 computations (62.4% saved)

localize7.0ms (0%)

Local error

Found 3 expressions with local error:

0.0b
(/.f64 (neg.f64 t1) (+.f64 t1 u))
0.0b
(/.f64 v (+.f64 t1 u))
1.5b
(*.f64 (/.f64 (neg.f64 t1) (+.f64 t1 u)) (/.f64 v (+.f64 t1 u)))

rewrite215.0ms (0.9%)

Algorithm
rewrite-expression-head
Error
0b
Rules
125×*-un-lft-identity_binary64_78
108×times-frac_binary64_84
81×add-sqr-sqrt_binary64_100
69×add-cube-cbrt_binary64_113
46×associate-*l*_binary64_19
28×distribute-lft-out_binary64_29
27×distribute-rgt-neg-in_binary64_36 distribute-lft-neg-in_binary64_35
19×add-exp-log_binary64_116 add-cbrt-cube_binary64_114
18×associate-*r*_binary64_18
13×associate-/l*_binary64_23
neg-mul-1_binary64_74
associate-/r/_binary64_24 associate-/r*_binary64_22
div-exp_binary64_129 cbrt-undiv_binary64_112
pow1_binary64_139
prod-exp_binary64_127 cbrt-unprod_binary64_111 unswap-sqr_binary64_46 div-inv_binary64_75 flip3-+_binary64_81 flip-+_binary64_52
add-log-exp_binary64_117
distribute-frac-neg_binary64_41 frac-2neg_binary64_89 clear-num_binary64_77
pow-prod-down_binary64_149 frac-times_binary64_88 distribute-lft-neg-out_binary64_37 associate-*l/_binary64_21 associate-*r/_binary64_20 *-commutative_binary64_9 neg-sub0_binary64_73 div-sub_binary64_83
Counts
3 → 192
Calls

3 calls:

30.0ms
(*.f64 (/.f64 (neg.f64 t1) (+.f64 t1 u)) (/.f64 v (+.f64 t1 u)))
7.0ms
(/.f64 (neg.f64 t1) (+.f64 t1 u))
5.0ms
(/.f64 v (+.f64 t1 u))
Compiler

Compiled 3974 to 711 computations (82.1% saved)

series477.0ms (2%)

Error
0b
Counts
3 → 42
Calls

3 calls:

235.0ms
(*.f64 (/.f64 (neg.f64 t1) (+.f64 t1 u)) (/.f64 v (+.f64 t1 u)))
124.0ms
(/.f64 v (+.f64 t1 u))
89.0ms
(/.f64 (neg.f64 t1) (+.f64 t1 u))
Compiler

Compiled 1599 to 1028 computations (35.7% saved)

simplify448.0ms (1.9%)

Algorithm
egg-herbie
Rules
599×associate-/r/_binary64_24
487×div-sub_binary64_83
292×distribute-lft-neg-out_binary64_37
264×distribute-frac-neg_binary64_41
239×distribute-rgt-neg-out_binary64_38
212×associate-/l*_binary64_23 associate-*l/_binary64_21
185×associate-*r/_binary64_20
157×distribute-rgt-in_binary64_28
146×neg-sub0_binary64_73
142×*-commutative_binary64_9
141×distribute-lft-in_binary64_27
126×neg-mul-1_binary64_74
110×distribute-rgt-neg-in_binary64_36
108×sub-neg_binary64_71
106×associate-*l*_binary64_19
101×associate-/l/_binary64_25
99×distribute-lft-neg-in_binary64_35
85×associate-*r*_binary64_18
83×times-frac_binary64_84
76×cancel-sign-sub-inv_binary64_44
74×distribute-neg-frac_binary64_42
63×associate-/r*_binary64_22
37×log-prod_binary64_164
33×log-div_binary64_165
32×sqr-pow_binary64_50
27×*-rgt-identity_binary64_68
25×unsub-neg_binary64_72
24×cube-prod_binary64_106
21×/-rgt-identity_binary64_69 *-lft-identity_binary64_67
20×cube-div_binary64_107 +-commutative_binary64_8
15×exp-prod_binary64_130
14×swap-sqr_binary64_45
11×div-exp_binary64_129 div0_binary64_59 pow-sqr_binary64_51
10×distribute-neg-out_binary64_40
pow-plus_binary64_141 prod-exp_binary64_127 distribute-neg-in_binary64_39 distribute-rgt-out_binary64_31
cube-unmult_binary64_115 sqr-neg_binary64_92
difference-of-squares_binary64_47 distribute-lft-out_binary64_29 associate-+l-_binary64_13
cube-neg_binary64_105 unswap-sqr_binary64_46 associate-+l+_binary64_11
mul-1-neg_binary64_70 associate-+r-_binary64_12
exp-neg_binary64_125 distribute-rgt-out--_binary64_32 distribute-lft-out--_binary64_30 associate--r-_binary64_17 associate--r+_binary64_14
unpow3_binary64_144 unpow2_binary64_143 unpow1_binary64_136 rec-exp_binary64_128 cube-mult_binary64_108 remove-double-neg_binary64_66 sub0-neg_binary64_65 associate-+r+_binary64_10
log-rec_binary64_166 exp-diff_binary64_126 *-inverses_binary64_58 cancel-sign-sub_binary64_43
exp-sqrt_binary64_131 1-exp_binary64_122 exp-1-e_binary64_121 rem-log-exp_binary64_119 --rgt-identity_binary64_64 +-rgt-identity_binary64_63 distribute-rgt1-in_binary64_34 associate--l-_binary64_16
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_341 erf-erfc_binary64_340 erf-odd_binary64_339 if-if-and-not_binary64_338 if-if-and_binary64_337 if-if-or-not_binary64_336 if-if-or_binary64_335 if-not_binary64_334 if-same_binary64_333 if-false_binary64_332 if-true_binary64_331 not-gte_binary64_330 not-lte_binary64_329 not-gt_binary64_328 not-lt_binary64_327 gte-same_binary64_326 lte-same_binary64_325 gt-same_binary64_324 lt-same_binary64_323 sinh---cosh_binary64_270 sinh-+-cosh_binary64_269 sinh-cosh_binary64_268 tanh-def-c_binary64_267 tanh-def-b_binary64_266 tanh-def-a_binary64_265 cosh-def_binary64_264 sinh-def_binary64_263 tan-neg_binary64_210 cos-neg_binary64_209 sin-neg_binary64_208 tan-0_binary64_207 cos-0_binary64_206 sin-0_binary64_205 hang-m-tan_binary64_204 hang-p-tan_binary64_203 hang-m0-tan_binary64_202 hang-p0-tan_binary64_201 hang-0m-tan_binary64_200 hang-0p-tan_binary64_199 tan-+PI/2_binary64_198 tan-+PI_binary64_197 tan-PI_binary64_196 tan-PI/3_binary64_195 tan-PI/4_binary64_194 tan-PI/6_binary64_193 cos-+PI/2_binary64_192 cos-+PI_binary64_191 cos-PI_binary64_190 cos-PI/2_binary64_189 cos-PI/3_binary64_188 cos-PI/4_binary64_187 cos-PI/6_binary64_186 sin-+PI/2_binary64_185 sin-+PI_binary64_184 sin-PI_binary64_183 sin-PI/2_binary64_182 sin-PI/3_binary64_181 sin-PI/4_binary64_180 sin-PI/6_binary64_179 sub-1-sin_binary64_178 sub-1-cos_binary64_177 -1-add-sin_binary64_176 -1-add-cos_binary64_175 1-sub-sin_binary64_174 1-sub-cos_binary64_173 cos-sin-sum_binary64_172 log-E_binary64_168 log-pow_binary64_167 pow-base-0_binary64_162 unpow1/3_binary64_145 unpow1/2_binary64_142 exp-to-pow_binary64_140 pow-base-1_binary64_138 unpow0_binary64_137 unpow-1_binary64_135 exp-lft-cube_binary64_134 exp-lft-sqr_binary64_133 exp-cbrt_binary64_132 exp-sum_binary64_124 e-exp-1_binary64_123 exp-0_binary64_120 rem-exp-log_binary64_118 rem-3cbrt-rft_binary64_104 rem-3cbrt-lft_binary64_103 rem-cbrt-cube_binary64_102 rem-cube-cbrt_binary64_101 sqr-abs_binary64_93 rem-sqrt-square_binary64_91 rem-square-sqrt_binary64_90 +-lft-identity_binary64_62 mul0-rgt_binary64_61 mul0-lft_binary64_60 +-inverses_binary64_57 lft-mult-inverse_binary64_56 rgt-mult-inverse_binary64_55 remove-double-div_binary64_54 difference-of-sqr--1_binary64_49 difference-of-sqr-1_binary64_48 distribute-lft1-in_binary64_33 count-2_binary64_26 associate--l+_binary64_15
Counts
234 → 341
Iterations

Useful iterations: 2 (0.0ms)

IterNodesCost
02464122
16783764
223183749

prune285.0ms (1.2%)

Pruning

7 alts after pruning (4 fresh and 3 done)

PrunedKeptTotal
New3401341
Fresh235
Picked011
Done022
Total3427349
Error
0b
Counts
349 → 7
Compiler

Compiled 6512 to 1381 computations (78.8% saved)

localize8.0ms (0%)

Local error

Found 3 expressions with local error:

0.0b
(pow.f64 (+.f64 t1 u) 2)
4.4b
(/.f64 v (/.f64 (pow.f64 (+.f64 t1 u) 2) t1))
16.7b
(/.f64 (pow.f64 (+.f64 t1 u) 2) t1)

rewrite275.0ms (1.2%)

Algorithm
rewrite-expression-head
Error
0b
Rules
228×times-frac_binary64_84
153×*-un-lft-identity_binary64_78
119×add-cube-cbrt_binary64_113 add-sqr-sqrt_binary64_100
68×unpow-prod-down_binary64_157
34×associate-/r*_binary64_22
19×add-exp-log_binary64_116
17×distribute-lft-out_binary64_29 unpow2_binary64_143 sqr-pow_binary64_50
12×associate-/l*_binary64_23
10×div-exp_binary64_129 add-cbrt-cube_binary64_114
div-inv_binary64_75
pow1_binary64_139 cbrt-undiv_binary64_112
pow-to-exp_binary64_147 pow-exp_binary64_146 add-log-exp_binary64_117 pow-unpow_binary64_155
frac-2neg_binary64_89 clear-num_binary64_77
associate-/r/_binary64_24 pow-pow_binary64_150
Counts
3 → 216
Calls

3 calls:

14.0ms
(/.f64 v (/.f64 (pow.f64 (+.f64 t1 u) 2) t1))
7.0ms
(/.f64 (pow.f64 (+.f64 t1 u) 2) t1)
4.0ms
(pow.f64 (+.f64 t1 u) 2)
Compiler

Compiled 4679 to 2233 computations (52.3% saved)

series541.0ms (2.3%)

Error
0b
Counts
3 → 48
Calls

3 calls:

198.0ms
(/.f64 v (/.f64 (pow.f64 (+.f64 t1 u) 2) t1))
189.0ms
(/.f64 (pow.f64 (+.f64 t1 u) 2) t1)
123.0ms
(pow.f64 (+.f64 t1 u) 2)
Compiler

Compiled 1464 to 1125 computations (23.2% saved)

simplify888.0ms (3.8%)

Algorithm
egg-herbie
Rules
477×distribute-rgt-in_binary64_28
452×*-commutative_binary64_9
396×distribute-lft-in_binary64_27
237×associate-/r/_binary64_24
218×associate-/l/_binary64_25
195×associate-/l*_binary64_23
146×cancel-sign-sub-inv_binary64_44
125×associate-*l/_binary64_21
109×sqr-pow_binary64_50
108×log-prod_binary64_164 distribute-rgt-neg-in_binary64_36
102×times-frac_binary64_84
99×unswap-sqr_binary64_46 distribute-lft-neg-in_binary64_35
96×associate-*r/_binary64_20
95×cube-prod_binary64_106
90×exp-prod_binary64_130
77×associate-/r*_binary64_22
62×distribute-rgt-out_binary64_31
60×*-rgt-identity_binary64_68
59×swap-sqr_binary64_45
57×log-div_binary64_165
53×/-rgt-identity_binary64_69
52×cube-div_binary64_107
51×pow-sqr_binary64_51 associate-*r*_binary64_18
44×sub-neg_binary64_71 associate-*l*_binary64_19
41×distribute-neg-frac_binary64_42
39×neg-mul-1_binary64_74
37×neg-sub0_binary64_73 distribute-rgt-out--_binary64_32
36×pow-plus_binary64_141
31×distribute-neg-in_binary64_39
27×log-pow_binary64_167
23×div-sub_binary64_83
21×+-commutative_binary64_8
20×*-lft-identity_binary64_67
18×prod-exp_binary64_127
17×distribute-lft-out_binary64_29
16×unpow3_binary64_144 div-exp_binary64_129 exp-sum_binary64_124 rem-sqrt-square_binary64_91
14×cube-unmult_binary64_115 cube-mult_binary64_108 unsub-neg_binary64_72
10×distribute-neg-out_binary64_40
distribute-lft-neg-out_binary64_37 distribute-rgt1-in_binary64_34
associate--r+_binary64_14 associate-+l+_binary64_11
unpow2_binary64_143 distribute-lft-out--_binary64_30 associate-+r+_binary64_10
log-rec_binary64_166 pow-base-1_binary64_138 unpow1_binary64_136 associate-+l-_binary64_13
distribute-rgt-neg-out_binary64_38
rec-exp_binary64_128 sub0-neg_binary64_65 distribute-lft1-in_binary64_33 associate-+r-_binary64_12
exp-sqrt_binary64_131 remove-double-div_binary64_54 associate--r-_binary64_17 associate--l-_binary64_16
exp-lft-sqr_binary64_133 count-2_binary64_26 associate--l+_binary64_15
exp-diff_binary64_126 1-exp_binary64_122 rem-log-exp_binary64_119 rem-3cbrt-rft_binary64_104 rem-3cbrt-lft_binary64_103 rem-square-sqrt_binary64_90 remove-double-neg_binary64_66 +-rgt-identity_binary64_63 div0_binary64_59 *-inverses_binary64_58 cancel-sign-sub_binary64_43
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_341 erf-erfc_binary64_340 erf-odd_binary64_339 if-if-and-not_binary64_338 if-if-and_binary64_337 if-if-or-not_binary64_336 if-if-or_binary64_335 if-not_binary64_334 if-same_binary64_333 if-false_binary64_332 if-true_binary64_331 not-gte_binary64_330 not-lte_binary64_329 not-gt_binary64_328 not-lt_binary64_327 gte-same_binary64_326 lte-same_binary64_325 gt-same_binary64_324 lt-same_binary64_323 sinh---cosh_binary64_270 sinh-+-cosh_binary64_269 sinh-cosh_binary64_268 tanh-def-c_binary64_267 tanh-def-b_binary64_266 tanh-def-a_binary64_265 cosh-def_binary64_264 sinh-def_binary64_263 tan-neg_binary64_210 cos-neg_binary64_209 sin-neg_binary64_208 tan-0_binary64_207 cos-0_binary64_206 sin-0_binary64_205 hang-m-tan_binary64_204 hang-p-tan_binary64_203 hang-m0-tan_binary64_202 hang-p0-tan_binary64_201 hang-0m-tan_binary64_200 hang-0p-tan_binary64_199 tan-+PI/2_binary64_198 tan-+PI_binary64_197 tan-PI_binary64_196 tan-PI/3_binary64_195 tan-PI/4_binary64_194 tan-PI/6_binary64_193 cos-+PI/2_binary64_192 cos-+PI_binary64_191 cos-PI_binary64_190 cos-PI/2_binary64_189 cos-PI/3_binary64_188 cos-PI/4_binary64_187 cos-PI/6_binary64_186 sin-+PI/2_binary64_185 sin-+PI_binary64_184 sin-PI_binary64_183 sin-PI/2_binary64_182 sin-PI/3_binary64_181 sin-PI/4_binary64_180 sin-PI/6_binary64_179 sub-1-sin_binary64_178 sub-1-cos_binary64_177 -1-add-sin_binary64_176 -1-add-cos_binary64_175 1-sub-sin_binary64_174 1-sub-cos_binary64_173 cos-sin-sum_binary64_172 log-E_binary64_168 pow-base-0_binary64_162 unpow1/3_binary64_145 unpow1/2_binary64_142 exp-to-pow_binary64_140 unpow0_binary64_137 unpow-1_binary64_135 exp-lft-cube_binary64_134 exp-cbrt_binary64_132 exp-neg_binary64_125 e-exp-1_binary64_123 exp-1-e_binary64_121 exp-0_binary64_120 rem-exp-log_binary64_118 cube-neg_binary64_105 rem-cbrt-cube_binary64_102 rem-cube-cbrt_binary64_101 sqr-abs_binary64_93 sqr-neg_binary64_92 mul-1-neg_binary64_70 --rgt-identity_binary64_64 +-lft-identity_binary64_62 mul0-rgt_binary64_61 mul0-lft_binary64_60 +-inverses_binary64_57 lft-mult-inverse_binary64_56 rgt-mult-inverse_binary64_55 difference-of-sqr--1_binary64_49 difference-of-sqr-1_binary64_48 difference-of-squares_binary64_47 distribute-frac-neg_binary64_41
Counts
264 → 1575
Iterations

Useful iterations: 2 (0.0ms)

IterNodesCost
03205823
15905084
220015075
328755075

prune2.1s (9.1%)

Pruning

7 alts after pruning (3 fresh and 4 done)

PrunedKeptTotal
New157501575
Fresh033
Picked011
Done033
Total157571582
Error
0b
Counts
1582 → 7
Compiler

Compiled 35038 to 12800 computations (63.5% saved)

regimes466.0ms (2%)

Accuracy

Total 1.3b remaining (99.8%)

Threshold costs 0b (0%)

Compiler

Compiled 5038 to 3058 computations (39.3% saved)

bsearch0.0ms (0%)

simplify3.0ms (0%)

Algorithm
egg-herbie
Rules
1-exp_binary64_122 /-rgt-identity_binary64_69 *-commutative_binary64_9 +-commutative_binary64_8
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_338 if-if-and_binary64_337 if-if-or-not_binary64_336 if-if-or_binary64_335 if-not_binary64_334 if-same_binary64_333 if-false_binary64_332 if-true_binary64_331 tan-0_binary64_207 cos-0_binary64_206 sin-0_binary64_205 unpow1_binary64_136 e-exp-1_binary64_123 exp-1-e_binary64_121 exp-0_binary64_120 sqr-abs_binary64_93 sqr-neg_binary64_92 neg-mul-1_binary64_74 neg-sub0_binary64_73 unsub-neg_binary64_72 sub-neg_binary64_71 mul-1-neg_binary64_70 *-rgt-identity_binary64_68 *-lft-identity_binary64_67 remove-double-neg_binary64_66 sub0-neg_binary64_65 --rgt-identity_binary64_64 +-rgt-identity_binary64_63 +-lft-identity_binary64_62 cancel-sign-sub-inv_binary64_44 cancel-sign-sub_binary64_43 distribute-neg-frac_binary64_42 distribute-frac-neg_binary64_41 distribute-neg-out_binary64_40 distribute-neg-in_binary64_39 distribute-rgt-neg-out_binary64_38 distribute-lft-neg-out_binary64_37 distribute-rgt-neg-in_binary64_36 distribute-lft-neg-in_binary64_35
Iterations

Useful iterations: 0 (0.0ms)

IterNodesCost
01322
11722
Proof
(* f64 (/ f64 (=> (/ f64 -1 1)) (+ f64 h0 h1)) (/ f64 (/ f64 h2 (+ f64 h0 h1)) (/ f64 1 h0))) /-rgt-identity_binary64_69 => (* f64 (/ f64 -1 (+ f64 h0 h1)) (/ f64 (/ f64 h2 (+ f64 h0 h1)) (/ f64 1 h0)))

end0.0ms (0%)

sample1.4s (6.1%)

Algorithm
intervals
Results
262.0ms8000×body128valid
9.0ms278×body128invalid
Compiler

Compiled 1280 to 779 computations (39.1% saved)

Profiling

Loading profile data...