Details

analyze123.0ms (5.3%)

Algorithm

1×

Search

True	Other	False	Iter
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
49.9%	49.9%	0.1%	5
74.9%	25%	0.1%	6
74.9%	25%	0.1%	7
74.9%	25%	0.1%	8
81.1%	18.7%	0.1%	9
81.1%	18.7%	0.1%	10
81.1%	15.6%	3.3%	11
84.3%	10.9%	4.8%	12
84.3%	10.9%	4.8%	13
84.3%	8.6%	7.2%	14

Compiler

Compiled 10 to 10 computations (0% saved)

sample17.0ms (0.7%)

Algorithm

1×

intervals

Results

7.0ms	256×	body	128	valid
0.0ms	15×	body	128	invalid

Compiler

Compiled 19 to 22 computations (-15.8% saved)

simplify687.0ms (29.5%)

Algorithm

1×	egg-herbie

Rules

841×	`exp-prod_binary64_10019`
760×	`associate-/l/_binary64_9914`
328×	`*-commutative_binary64_9898`
307×	`swap-sqr_binary64_9934`
286×	`times-frac_binary64_9973`
284×	`associate-/r*_binary64_9911`
254×	`cancel-sign-sub-inv_binary64_9933`
179×	`associate-/r/_binary64_9913`
146×	`distribute-rgt1-in_binary64_9923`
145×	`associate-+l+_binary64_9900`
134×	`distribute-lft-neg-in_binary64_9924`
129×	`associate--l+_binary64_9904`
124×	`associate-+r+_binary64_9899`
115×	`distribute-rgt-neg-in_binary64_9925`
108×	`associate--r+_binary64_9903`
97×	`associate-+l-_binary64_9902`
92×	`associate-+r-_binary64_9901`
91×	`associate--l-_binary64_9905`
85×	`distribute-neg-frac_binary64_9931`
76×	`pow-plus_binary64_10030`
71×	`sub-neg_binary64_9960`
69×	`associate--r-_binary64_9906`
67×	`unsub-neg_binary64_9961`
65×	`distribute-frac-neg_binary64_9930`
63×	`exp-sum_binary64_10013`
61×	`distribute-neg-in_binary64_9928`
53×	`neg-mul-1_binary64_9963`
50×	`neg-sub0_binary64_9962`
49×	`distribute-rgt-in_binary64_9917`
44×	`distribute-rgt-neg-out_binary64_9927`
38×	`distribute-lft-neg-out_binary64_9926`
33×	`associate-/l*_binary64_9912`
30×	`associate-r_binary64_9907`
28×	`+-commutative_binary64_9897`
25×	`distribute-lft-in_binary64_9916`
23×	`*-rgt-identity_binary64_9957`
22×	`exp-sqrt_binary64_10020` `exp-diff_binary64_10015` `*-lft-identity_binary64_9956`
20×	`sqr-pow_binary64_9939`
19×	`distribute-rgt-out_binary64_9920`
17×	`div-sub_binary64_9972`
15×	`pow-sqr_binary64_9940`
14×	`remove-double-neg_binary64_9955`
13×	`pow-base-1_binary64_10027`
10×	`exp-lft-sqr_binary64_10022` `mul0-lft_binary64_9949` `distribute-rgt-out--_binary64_9921`
9×	`cube-unmult_binary64_10004` `div0_binary64_9948` `associate-l_binary64_9908`
8×	`sub0-neg_binary64_9954` `distribute-neg-out_binary64_9929` `associate-*l/_binary64_9910`
7×	`mul0-rgt_binary64_9950` `unswap-sqr_binary64_9935`
6×	`+-lft-identity_binary64_9951` `count-2_binary64_9915`
5×	`+-rgt-identity_binary64_9952` `associate-*r/_binary64_9909`
4×	`--rgt-identity_binary64_9953` `distribute-lft1-in_binary64_9922`
3×	`+-inverses_binary64_9946` `distribute-lft-out--_binary64_9919` `distribute-lft-out_binary64_9918`
2×	`exp-neg_binary64_10014` `cube-prod_binary64_9995` `sqr-neg_binary64_9981`
1×	`unpow3_binary64_10033` `1-exp_binary64_10011` `cube-neg_binary64_9994` `rem-sqrt-square_binary64_9980` `*-inverses_binary64_9947` `lft-mult-inverse_binary64_9945` `rgt-mult-inverse_binary64_9944` `difference-of-sqr--1_binary64_9938` `difference-of-squares_binary64_9936`
0×	`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_10230` `erf-erfc_binary64_10229` `erf-odd_binary64_10228` `if-if-and-not_binary64_10227` `if-if-and_binary64_10226` `if-if-or-not_binary64_10225` `if-if-or_binary64_10224` `if-not_binary64_10223` `if-same_binary64_10222` `if-false_binary64_10221` `if-true_binary64_10220` `not-gte_binary64_10219` `not-lte_binary64_10218` `not-gt_binary64_10217` `not-lt_binary64_10216` `gte-same_binary64_10215` `lte-same_binary64_10214` `gt-same_binary64_10213` `lt-same_binary64_10212` `sinh---cosh_binary64_10159` `sinh-+-cosh_binary64_10158` `sinh-cosh_binary64_10157` `tanh-def-c_binary64_10156` `tanh-def-b_binary64_10155` `tanh-def-a_binary64_10154` `cosh-def_binary64_10153` `sinh-def_binary64_10152` `tan-neg_binary64_10099` `cos-neg_binary64_10098` `sin-neg_binary64_10097` `tan-0_binary64_10096` `cos-0_binary64_10095` `sin-0_binary64_10094` `hang-m-tan_binary64_10093` `hang-p-tan_binary64_10092` `hang-m0-tan_binary64_10091` `hang-p0-tan_binary64_10090` `hang-0m-tan_binary64_10089` `hang-0p-tan_binary64_10088` `tan-+PI/2_binary64_10087` `tan-+PI_binary64_10086` `tan-PI_binary64_10085` `tan-PI/3_binary64_10084` `tan-PI/4_binary64_10083` `tan-PI/6_binary64_10082` `cos-+PI/2_binary64_10081` `cos-+PI_binary64_10080` `cos-PI_binary64_10079` `cos-PI/2_binary64_10078` `cos-PI/3_binary64_10077` `cos-PI/4_binary64_10076` `cos-PI/6_binary64_10075` `sin-+PI/2_binary64_10074` `sin-+PI_binary64_10073` `sin-PI_binary64_10072` `sin-PI/2_binary64_10071` `sin-PI/3_binary64_10070` `sin-PI/4_binary64_10069` `sin-PI/6_binary64_10068` `sub-1-sin_binary64_10067` `sub-1-cos_binary64_10066` `-1-add-sin_binary64_10065` `-1-add-cos_binary64_10064` `1-sub-sin_binary64_10063` `1-sub-cos_binary64_10062` `cos-sin-sum_binary64_10061` `log-E_binary64_10057` `log-pow_binary64_10056` `log-rec_binary64_10055` `log-div_binary64_10054` `log-prod_binary64_10053` `pow-base-0_binary64_10051` `unpow1/3_binary64_10034` `unpow2_binary64_10032` `unpow1/2_binary64_10031` `exp-to-pow_binary64_10029` `unpow0_binary64_10026` `unpow1_binary64_10025` `unpow-1_binary64_10024` `exp-lft-cube_binary64_10023` `exp-cbrt_binary64_10021` `div-exp_binary64_10018` `rec-exp_binary64_10017` `prod-exp_binary64_10016` `e-exp-1_binary64_10012` `exp-1-e_binary64_10010` `exp-0_binary64_10009` `rem-log-exp_binary64_10008` `rem-exp-log_binary64_10007` `cube-mult_binary64_9997` `cube-div_binary64_9996` `rem-3cbrt-rft_binary64_9993` `rem-3cbrt-lft_binary64_9992` `rem-cbrt-cube_binary64_9991` `rem-cube-cbrt_binary64_9990` `sqr-abs_binary64_9982` `rem-square-sqrt_binary64_9979` `mul-1-neg_binary64_9959` `/-rgt-identity_binary64_9958` `remove-double-div_binary64_9943` `difference-of-sqr-1_binary64_9937` `cancel-sign-sub_binary64_9932`

Counts

1 → 4

Iterations

Useful iterations: 0 (0.0ms)

Iter	Nodes	Cost
0	10	13
1	15	13
2	26	13
3	37	13
4	61	13
5	96	13
6	191	13
7	455	13
8	2325	13
9	4641	13

prune4.0ms (0.2%)

Pruning

1 alts after pruning (1 fresh and 0 done)

	Pruned	Kept	Total
New	4	0	4
Fresh	0	1	1
Picked	0	0	0
Done	0	0	0
Total	4	1	5

Error

0.0b

Counts

5 → 1

Compiler

Compiled 45 to 36 computations (20% saved)

localize6.0ms (0.3%)

Local error

Found 2 expressions with local error:

0.0b	(/.f64 (*.f64 x y) 2)
0.0b	(-.f64 (/.f64 (*.f64 x y) 2) (/.f64 z 8))

rewrite69.0ms (3%)

Algorithm

1×	rewrite-expression-head

Error

0.0b

Rules

16×	`add-sqr-sqrt_binary64_9989`
13×	`*-un-lft-identity_binary64_9967` `times-frac_binary64_9973` `cancel-sign-sub-inv_binary64_9933`
11×	`add-cube-cbrt_binary64_10002`
7×	`add-exp-log_binary64_10005` `add-cbrt-cube_binary64_10003`
4×	`add-log-exp_binary64_10006`
3×	`associate-/r*_binary64_9911`
2×	`pow1_binary64_10028` `difference-of-squares_binary64_9936` `div-inv_binary64_9964` `div-exp_binary64_10018` `cbrt-undiv_binary64_10001`
1×	`diff-log_binary64_10059` `frac-sub_binary64_9976` `flip3--_binary64_9971` `sub-neg_binary64_9960` `flip--_binary64_9942` `distribute-lft-out--_binary64_9919` `prod-exp_binary64_10016` `cbrt-unprod_binary64_10000` `frac-2neg_binary64_9978` `clear-num_binary64_9966` `associate-/l*_binary64_9912`

Counts

2 → 49

Calls

2 calls:

11.0ms	(-.f64 (/.f64 (*.f64 x y) 2) (/.f64 z 8))
4.0ms	(/.f64 (*.f64 x y) 2)

Compiler

Compiled 820 to 532 computations (35.1% saved)

series305.0ms (13.1%)

Error

0.0b

Counts

2 → 24

Calls

2 calls:

214.0ms	(-.f64 (/.f64 (*.f64 x y) 2) (/.f64 z 8))
78.0ms	(/.f64 (*.f64 x y) 2)

Compiler

Compiled 479 to 417 computations (12.9% saved)

simplify212.0ms (9.1%)

Algorithm

1×	egg-herbie

Rules

645×	`associate-/l*_binary64_9912`
587×	`times-frac_binary64_9973`
399×	`associate-l_binary64_9908`
355×	`associate-*l/_binary64_9910`
297×	`div-sub_binary64_9972`
275×	`associate-r_binary64_9907`
243×	`associate-*r/_binary64_9909`
241×	`associate-/l/_binary64_9914`
166×	`associate-/r*_binary64_9911`
141×	`exp-prod_binary64_10019`
134×	`associate-/r/_binary64_9913`
133×	`*-commutative_binary64_9898`
79×	`distribute-rgt-in_binary64_9917`
77×	`distribute-lft-in_binary64_9916`
70×	`distribute-lft-neg-out_binary64_9926`
58×	`cube-prod_binary64_9995`
57×	`neg-sub0_binary64_9962`
54×	`distribute-neg-frac_binary64_9931`
51×	`sub-neg_binary64_9960`
50×	`neg-mul-1_binary64_9963`
45×	`exp-sum_binary64_10013` `cube-div_binary64_9996`
39×	`distribute-rgt-neg-in_binary64_9925`
37×	`+-commutative_binary64_9897`
35×	`distribute-rgt-neg-out_binary64_9927`
28×	`log-div_binary64_10054`
25×	`log-prod_binary64_10053` `cancel-sign-sub-inv_binary64_9933`
24×	`sqr-pow_binary64_9939`
23×	`distribute-lft-neg-in_binary64_9924`
19×	`distribute-frac-neg_binary64_9930`
16×	`*-rgt-identity_binary64_9957`
14×	`unpow3_binary64_10033` `exp-diff_binary64_10015`
13×	`associate-+l-_binary64_9902`
11×	`cube-unmult_binary64_10004`
10×	`div-exp_binary64_10018` `/-rgt-identity_binary64_9958` `associate-+r-_binary64_9901`
9×	`prod-exp_binary64_10016` `swap-sqr_binary64_9934`
8×	`pow-sqr_binary64_9940`
7×	`cube-mult_binary64_9997` `rem-sqrt-square_binary64_9980` `associate-+l+_binary64_9900`
6×	`exp-neg_binary64_10014` `*-lft-identity_binary64_9956` `associate--l-_binary64_9905`
4×	`log-rec_binary64_10055` `unswap-sqr_binary64_9935` `associate-+r+_binary64_9899`
3×	`rec-exp_binary64_10017` `rem-square-sqrt_binary64_9979` `div0_binary64_9948` `difference-of-squares_binary64_9936` `distribute-rgt-out_binary64_9920` `associate--l+_binary64_9904`
2×	`pow-plus_binary64_10030` `exp-sqrt_binary64_10020` `rem-3cbrt-lft_binary64_9992` `unsub-neg_binary64_9961` `+-rgt-identity_binary64_9952`
1×	`log-pow_binary64_10056` `exp-to-pow_binary64_10029` `pow-base-1_binary64_10027` `1-exp_binary64_10011` `exp-1-e_binary64_10010` `rem-log-exp_binary64_10008` `rem-3cbrt-rft_binary64_9993` `sqr-neg_binary64_9981`
0×	`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_10230` `erf-erfc_binary64_10229` `erf-odd_binary64_10228` `if-if-and-not_binary64_10227` `if-if-and_binary64_10226` `if-if-or-not_binary64_10225` `if-if-or_binary64_10224` `if-not_binary64_10223` `if-same_binary64_10222` `if-false_binary64_10221` `if-true_binary64_10220` `not-gte_binary64_10219` `not-lte_binary64_10218` `not-gt_binary64_10217` `not-lt_binary64_10216` `gte-same_binary64_10215` `lte-same_binary64_10214` `gt-same_binary64_10213` `lt-same_binary64_10212` `sinh---cosh_binary64_10159` `sinh-+-cosh_binary64_10158` `sinh-cosh_binary64_10157` `tanh-def-c_binary64_10156` `tanh-def-b_binary64_10155` `tanh-def-a_binary64_10154` `cosh-def_binary64_10153` `sinh-def_binary64_10152` `tan-neg_binary64_10099` `cos-neg_binary64_10098` `sin-neg_binary64_10097` `tan-0_binary64_10096` `cos-0_binary64_10095` `sin-0_binary64_10094` `hang-m-tan_binary64_10093` `hang-p-tan_binary64_10092` `hang-m0-tan_binary64_10091` `hang-p0-tan_binary64_10090` `hang-0m-tan_binary64_10089` `hang-0p-tan_binary64_10088` `tan-+PI/2_binary64_10087` `tan-+PI_binary64_10086` `tan-PI_binary64_10085` `tan-PI/3_binary64_10084` `tan-PI/4_binary64_10083` `tan-PI/6_binary64_10082` `cos-+PI/2_binary64_10081` `cos-+PI_binary64_10080` `cos-PI_binary64_10079` `cos-PI/2_binary64_10078` `cos-PI/3_binary64_10077` `cos-PI/4_binary64_10076` `cos-PI/6_binary64_10075` `sin-+PI/2_binary64_10074` `sin-+PI_binary64_10073` `sin-PI_binary64_10072` `sin-PI/2_binary64_10071` `sin-PI/3_binary64_10070` `sin-PI/4_binary64_10069` `sin-PI/6_binary64_10068` `sub-1-sin_binary64_10067` `sub-1-cos_binary64_10066` `-1-add-sin_binary64_10065` `-1-add-cos_binary64_10064` `1-sub-sin_binary64_10063` `1-sub-cos_binary64_10062` `cos-sin-sum_binary64_10061` `log-E_binary64_10057` `pow-base-0_binary64_10051` `unpow1/3_binary64_10034` `unpow2_binary64_10032` `unpow1/2_binary64_10031` `unpow0_binary64_10026` `unpow1_binary64_10025` `unpow-1_binary64_10024` `exp-lft-cube_binary64_10023` `exp-lft-sqr_binary64_10022` `exp-cbrt_binary64_10021` `e-exp-1_binary64_10012` `exp-0_binary64_10009` `rem-exp-log_binary64_10007` `cube-neg_binary64_9994` `rem-cbrt-cube_binary64_9991` `rem-cube-cbrt_binary64_9990` `sqr-abs_binary64_9982` `mul-1-neg_binary64_9959` `remove-double-neg_binary64_9955` `sub0-neg_binary64_9954` `--rgt-identity_binary64_9953` `+-lft-identity_binary64_9951` `mul0-rgt_binary64_9950` `mul0-lft_binary64_9949` `*-inverses_binary64_9947` `+-inverses_binary64_9946` `lft-mult-inverse_binary64_9945` `rgt-mult-inverse_binary64_9944` `remove-double-div_binary64_9943` `difference-of-sqr--1_binary64_9938` `difference-of-sqr-1_binary64_9937` `cancel-sign-sub_binary64_9932` `distribute-neg-out_binary64_9929` `distribute-neg-in_binary64_9928` `distribute-rgt1-in_binary64_9923` `distribute-lft1-in_binary64_9922` `distribute-rgt-out--_binary64_9921` `distribute-lft-out--_binary64_9919` `distribute-lft-out_binary64_9918` `count-2_binary64_9915` `associate--r-_binary64_9906` `associate--r+_binary64_9903`

Counts

73 → 207

Iterations

Useful iterations: 2 (0.0ms)

Iter	Nodes	Cost
0	140	855
1	373	828
2	1141	825
3	4355	825

prune250.0ms (10.7%)

Pruning

1 alts after pruning (0 fresh and 1 done)

	Pruned	Kept	Total
New	207	0	207
Fresh	0	0	0
Picked	0	1	1
Done	0	0	0
Total	207	1	208

Error

0.0b

Counts

208 → 1

Compiler

Compiled 4058 to 2783 computations (31.4% saved)

regimes73.0ms (3.1%)

Accuracy

Total 0.0b remaining (80.2%)

Threshold costs 0.0b (80.2%)

Compiler

Compiled 200 to 248 computations (-24% saved)

bsearch0.0ms (0%)

simplify5.0ms (0.2%)

Algorithm

1×	egg-herbie

Rules

3×	`sub-neg_binary64_9960` `*-commutative_binary64_9898` `+-commutative_binary64_9897`
2×	`neg-mul-1_binary64_9963` `neg-sub0_binary64_9962`
1×	`distribute-neg-frac_binary64_9931`
0×	`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_10227` `if-if-and_binary64_10226` `if-if-or-not_binary64_10225` `if-if-or_binary64_10224` `if-not_binary64_10223` `if-same_binary64_10222` `if-false_binary64_10221` `if-true_binary64_10220` `tan-0_binary64_10096` `cos-0_binary64_10095` `sin-0_binary64_10094` `unpow1_binary64_10025` `e-exp-1_binary64_10012` `1-exp_binary64_10011` `exp-1-e_binary64_10010` `exp-0_binary64_10009` `sqr-abs_binary64_9982` `sqr-neg_binary64_9981` `unsub-neg_binary64_9961` `mul-1-neg_binary64_9959` `/-rgt-identity_binary64_9958` `-rgt-identity_binary64_9957` `-lft-identity_binary64_9956` `remove-double-neg_binary64_9955` `sub0-neg_binary64_9954` `--rgt-identity_binary64_9953` `+-rgt-identity_binary64_9952` `+-lft-identity_binary64_9951` `cancel-sign-sub-inv_binary64_9933` `cancel-sign-sub_binary64_9932` `distribute-frac-neg_binary64_9930` `distribute-neg-out_binary64_9929` `distribute-neg-in_binary64_9928` `distribute-rgt-neg-out_binary64_9927` `distribute-lft-neg-out_binary64_9926` `distribute-rgt-neg-in_binary64_9925` `distribute-lft-neg-in_binary64_9924`

Iterations

Useful iterations: 0 (0.0ms)

Iter	Nodes	Cost
0	10	13
1	13	13
2	20	13
3	24	13
4	27	13
5	28	13

Proof

(- f64 (/ f64 (* f64 h0 h1) 2) (/ f64 h2 8))

end0.0ms (0%)

sample577.0ms (24.8%)

Algorithm

1×

intervals

Results

239.0ms	8000×	body	128	valid
13.0ms	471×	body	128	invalid

Compiler

Compiled 41 to 48 computations (-17.1% saved)

Details

analyze123.0ms (5.3%)

sample17.0ms (0.7%)

simplify687.0ms (29.5%)

prune4.0ms (0.2%)

localize6.0ms (0.3%)

rewrite69.0ms (3%)

series305.0ms (13.1%)

simplify212.0ms (9.1%)

prune250.0ms (10.7%)

regimes73.0ms (3.1%)

bsearch0.0ms (0%)

simplify5.0ms (0.2%)

end0.0ms (0%)

sample577.0ms (24.8%)

Profiling