Details

analyze265.0ms (13.9%)

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
0%	99.9%	0.1%	5
0%	99.9%	0.1%	6
12.5%	87.4%	0.1%	7
18.7%	81.1%	0.1%	8
36.7%	60.8%	2.5%	9
43.3%	49.9%	6.8%	10
49.7%	40.8%	9.5%	11
58.2%	30.4%	11.4%	12
61.3%	24.7%	14%	13
65%	19.9%	15.1%	14

Compiler

Compiled 8 to 7 computations (12.5% saved)

sample16.0ms (0.8%)

Algorithm

1×

intervals

Results

6.0ms	256×	body	128	valid
0.0ms	14×	body	128	invalid

Compiler

Compiled 15 to 16 computations (-6.7% saved)

simplify697.0ms (36.5%)

Algorithm

1×	egg-herbie

Rules

809×	`pow-plus_binary64_4915`
508×	`exp-prod_binary64_4904`
492×	`sqr-pow_binary64_4824`
382×	`pow-sqr_binary64_4825`
309×	`*-commutative_binary64_4783`
295×	`exp-sum_binary64_4898`
215×	`distribute-rgt1-in_binary64_4808`
200×	`associate-/r*_binary64_4796`
178×	`distribute-rgt-out_binary64_4805`
166×	`associate-/l/_binary64_4799`
153×	`associate-r_binary64_4792`
149×	`associate-+l+_binary64_4785`
134×	`+-commutative_binary64_4782`
127×	`pow-base-1_binary64_4912` `associate-l_binary64_4793`
98×	`distribute-lft-out_binary64_4803`
73×	`associate-+r+_binary64_4784`
41×	`swap-sqr_binary64_4819`
27×	`associate-/r/_binary64_4798` `associate-/l*_binary64_4797`
26×	`distribute-rgt-in_binary64_4802`
17×	`*-rgt-identity_binary64_4842`
16×	`*-lft-identity_binary64_4841` `distribute-lft-in_binary64_4801`
13×	`exp-lft-sqr_binary64_4907`
12×	`unswap-sqr_binary64_4820`
11×	`cube-unmult_binary64_4889` `distribute-lft1-in_binary64_4807`
10×	`exp-sqrt_binary64_4905`
9×	`cube-prod_binary64_4880` `count-2_binary64_4800`
4×	`prod-exp_binary64_4901`
3×	`unpow1_binary64_4910`
2×	`unpow3_binary64_4918` `cube-div_binary64_4881` `rem-sqrt-square_binary64_4865`
1×	`1-exp_binary64_4896` `exp-1-e_binary64_4895` `/-rgt-identity_binary64_4843` `+-rgt-identity_binary64_4837` `div0_binary64_4833` `-inverses_binary64_4832` `lft-mult-inverse_binary64_4830` `rgt-mult-inverse_binary64_4829` `associate-r/_binary64_4794`
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_5115` `erf-erfc_binary64_5114` `erf-odd_binary64_5113` `if-if-and-not_binary64_5112` `if-if-and_binary64_5111` `if-if-or-not_binary64_5110` `if-if-or_binary64_5109` `if-not_binary64_5108` `if-same_binary64_5107` `if-false_binary64_5106` `if-true_binary64_5105` `not-gte_binary64_5104` `not-lte_binary64_5103` `not-gt_binary64_5102` `not-lt_binary64_5101` `gte-same_binary64_5100` `lte-same_binary64_5099` `gt-same_binary64_5098` `lt-same_binary64_5097` `sinh---cosh_binary64_5044` `sinh-+-cosh_binary64_5043` `sinh-cosh_binary64_5042` `tanh-def-c_binary64_5041` `tanh-def-b_binary64_5040` `tanh-def-a_binary64_5039` `cosh-def_binary64_5038` `sinh-def_binary64_5037` `tan-neg_binary64_4984` `cos-neg_binary64_4983` `sin-neg_binary64_4982` `tan-0_binary64_4981` `cos-0_binary64_4980` `sin-0_binary64_4979` `hang-m-tan_binary64_4978` `hang-p-tan_binary64_4977` `hang-m0-tan_binary64_4976` `hang-p0-tan_binary64_4975` `hang-0m-tan_binary64_4974` `hang-0p-tan_binary64_4973` `tan-+PI/2_binary64_4972` `tan-+PI_binary64_4971` `tan-PI_binary64_4970` `tan-PI/3_binary64_4969` `tan-PI/4_binary64_4968` `tan-PI/6_binary64_4967` `cos-+PI/2_binary64_4966` `cos-+PI_binary64_4965` `cos-PI_binary64_4964` `cos-PI/2_binary64_4963` `cos-PI/3_binary64_4962` `cos-PI/4_binary64_4961` `cos-PI/6_binary64_4960` `sin-+PI/2_binary64_4959` `sin-+PI_binary64_4958` `sin-PI_binary64_4957` `sin-PI/2_binary64_4956` `sin-PI/3_binary64_4955` `sin-PI/4_binary64_4954` `sin-PI/6_binary64_4953` `sub-1-sin_binary64_4952` `sub-1-cos_binary64_4951` `-1-add-sin_binary64_4950` `-1-add-cos_binary64_4949` `1-sub-sin_binary64_4948` `1-sub-cos_binary64_4947` `cos-sin-sum_binary64_4946` `log-E_binary64_4942` `log-pow_binary64_4941` `log-rec_binary64_4940` `log-div_binary64_4939` `log-prod_binary64_4938` `pow-base-0_binary64_4936` `unpow1/3_binary64_4919` `unpow2_binary64_4917` `unpow1/2_binary64_4916` `exp-to-pow_binary64_4914` `unpow0_binary64_4911` `unpow-1_binary64_4909` `exp-lft-cube_binary64_4908` `exp-cbrt_binary64_4906` `div-exp_binary64_4903` `rec-exp_binary64_4902` `exp-diff_binary64_4900` `exp-neg_binary64_4899` `e-exp-1_binary64_4897` `exp-0_binary64_4894` `rem-log-exp_binary64_4893` `rem-exp-log_binary64_4892` `cube-mult_binary64_4882` `cube-neg_binary64_4879` `rem-3cbrt-rft_binary64_4878` `rem-3cbrt-lft_binary64_4877` `rem-cbrt-cube_binary64_4876` `rem-cube-cbrt_binary64_4875` `sqr-abs_binary64_4867` `sqr-neg_binary64_4866` `rem-square-sqrt_binary64_4864` `times-frac_binary64_4858` `div-sub_binary64_4857` `neg-mul-1_binary64_4848` `neg-sub0_binary64_4847` `unsub-neg_binary64_4846` `sub-neg_binary64_4845` `mul-1-neg_binary64_4844` `remove-double-neg_binary64_4840` `sub0-neg_binary64_4839` `--rgt-identity_binary64_4838` `+-lft-identity_binary64_4836` `mul0-rgt_binary64_4835` `mul0-lft_binary64_4834` `+-inverses_binary64_4831` `remove-double-div_binary64_4828` `difference-of-sqr--1_binary64_4823` `difference-of-sqr-1_binary64_4822` `difference-of-squares_binary64_4821` `cancel-sign-sub-inv_binary64_4818` `cancel-sign-sub_binary64_4817` `distribute-neg-frac_binary64_4816` `distribute-frac-neg_binary64_4815` `distribute-neg-out_binary64_4814` `distribute-neg-in_binary64_4813` `distribute-rgt-neg-out_binary64_4812` `distribute-lft-neg-out_binary64_4811` `distribute-rgt-neg-in_binary64_4810` `distribute-lft-neg-in_binary64_4809` `distribute-rgt-out--_binary64_4806` `distribute-lft-out--_binary64_4804` `associate-*l/_binary64_4795` `associate--r-_binary64_4791` `associate--l-_binary64_4790` `associate--l+_binary64_4789` `associate--r+_binary64_4788` `associate-+l-_binary64_4787` `associate-+r-_binary64_4786`

Counts

1 → 1

Iterations

Useful iterations: 0 (0.0ms)

Iter	Nodes	Cost
0	7	10
1	16	10
2	24	10
3	30	10
4	34	10
5	40	10
6	36	10
7	48	10
8	44	10
9	59	10
10	73	10
11	145	10
12	744	10
13	1372	10
14	2324	10
15	4531	10

prune2.0ms (0.1%)

Pruning

1 alts after pruning (1 fresh and 0 done)

	Pruned	Kept	Total
New	1	0	1
Fresh	0	1	1
Picked	0	0	0
Done	0	0	0
Total	1	1	2

Error

Counts

2 → 1

Compiler

Compiled 14 to 12 computations (14.3% saved)

localize5.0ms (0.3%)

Local error

Found 1 expressions with local error:

0.0b	(*.f64 y (+.f64 z x))

rewrite26.0ms (1.4%)

Algorithm

1×	rewrite-expression-head

Error

Rules

5×	`add-sqr-sqrt_binary64_4874` `*-un-lft-identity_binary64_4852`
4×	`associate-r_binary64_4792`
3×	`pow1_binary64_4913` `add-exp-log_binary64_4890` `add-cbrt-cube_binary64_4888` `add-cube-cbrt_binary64_4887` `associate-l_binary64_4793`
2×	`associate-*r/_binary64_4794`
1×	`pow-prod-down_binary64_4923` `prod-exp_binary64_4901` `add-log-exp_binary64_4891` `cbrt-unprod_binary64_4885` `unswap-sqr_binary64_4820` `distribute-rgt-in_binary64_4802` `distribute-lft-in_binary64_4801` `flip3-+_binary64_4855` `flip-+_binary64_4826` `distribute-lft-out_binary64_4803` `*-commutative_binary64_4783`

Counts

1 → 23

Calls

1 calls:

7.0ms

(*.f64 y (+.f64 z x))

Compiler

Compiled 295 to 103 computations (65.1% saved)

series139.0ms (7.3%)

Error

Counts

1 → 15

Calls

1 calls:

129.0ms

(*.f64 y (+.f64 z x))

Compiler

Compiled 285 to 162 computations (43.2% saved)

simplify151.0ms (7.9%)

Algorithm

1×	egg-herbie

Rules

932×	`distribute-rgt-in_binary64_4802`
923×	`distribute-lft-in_binary64_4801`
267×	`associate-l_binary64_4793`
220×	`unswap-sqr_binary64_4820`
198×	`associate-r_binary64_4792`
187×	`associate-*r/_binary64_4794`
181×	`associate-*l/_binary64_4795`
161×	`distribute-rgt-out_binary64_4805`
134×	`associate-+l+_binary64_4785`
133×	`sqr-pow_binary64_4824`
122×	`associate-+r+_binary64_4784`
117×	`*-commutative_binary64_4783`
100×	`*-rgt-identity_binary64_4842`
98×	`*-lft-identity_binary64_4841`
92×	`associate-/l/_binary64_4799`
90×	`cancel-sign-sub-inv_binary64_4818`
81×	`associate-/l*_binary64_4797`
73×	`pow-sqr_binary64_4825`
67×	`exp-prod_binary64_4904`
65×	`distribute-rgt-neg-in_binary64_4810`
56×	`cube-div_binary64_4881`
55×	`distribute-lft-neg-in_binary64_4809`
52×	`neg-mul-1_binary64_4848` `associate-/r/_binary64_4798`
49×	`cube-prod_binary64_4880`
46×	`distribute-lft-out_binary64_4803`
40×	`unsub-neg_binary64_4846`
38×	`associate--r+_binary64_4788`
35×	`sub-neg_binary64_4845`
34×	`times-frac_binary64_4858`
28×	`log-div_binary64_4939`
27×	`log-prod_binary64_4938` `associate-+r-_binary64_4786`
25×	`pow-plus_binary64_4915`
24×	`distribute-neg-in_binary64_4813`
22×	`neg-sub0_binary64_4847` `associate-/r*_binary64_4796`
21×	`log-pow_binary64_4941` `distribute-lft-neg-out_binary64_4811`
20×	`exp-sqrt_binary64_4905` `associate-+l-_binary64_4787`
17×	`distribute-rgt-neg-out_binary64_4812`
15×	`distribute-rgt1-in_binary64_4808`
14×	`cube-unmult_binary64_4889` `distribute-rgt-out--_binary64_4806`
13×	`+-commutative_binary64_4782`
11×	`unpow3_binary64_4918`
9×	`exp-sum_binary64_4898` `swap-sqr_binary64_4819` `count-2_binary64_4800`
8×	`exp-to-pow_binary64_4914` `sub0-neg_binary64_4839`
7×	`associate--l+_binary64_4789`
6×	`div-sub_binary64_4857` `+-rgt-identity_binary64_4837`
5×	`mul0-rgt_binary64_4835` `mul0-lft_binary64_4834`
4×	`log-rec_binary64_4940` `pow-base-1_binary64_4912`
3×	`exp-lft-sqr_binary64_4907` `cube-mult_binary64_4882` `/-rgt-identity_binary64_4843` `associate--r-_binary64_4791`
2×	`exp-diff_binary64_4900` `rem-log-exp_binary64_4893` `--rgt-identity_binary64_4838` `difference-of-squares_binary64_4821` `cancel-sign-sub_binary64_4817`
1×	`exp-lft-cube_binary64_4908` `prod-exp_binary64_4901` `1-exp_binary64_4896` `exp-1-e_binary64_4895` `remove-double-neg_binary64_4840` `*-inverses_binary64_4832` `rgt-mult-inverse_binary64_4829` `distribute-neg-frac_binary64_4816` `distribute-lft-out--_binary64_4804`
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_5115` `erf-erfc_binary64_5114` `erf-odd_binary64_5113` `if-if-and-not_binary64_5112` `if-if-and_binary64_5111` `if-if-or-not_binary64_5110` `if-if-or_binary64_5109` `if-not_binary64_5108` `if-same_binary64_5107` `if-false_binary64_5106` `if-true_binary64_5105` `not-gte_binary64_5104` `not-lte_binary64_5103` `not-gt_binary64_5102` `not-lt_binary64_5101` `gte-same_binary64_5100` `lte-same_binary64_5099` `gt-same_binary64_5098` `lt-same_binary64_5097` `sinh---cosh_binary64_5044` `sinh-+-cosh_binary64_5043` `sinh-cosh_binary64_5042` `tanh-def-c_binary64_5041` `tanh-def-b_binary64_5040` `tanh-def-a_binary64_5039` `cosh-def_binary64_5038` `sinh-def_binary64_5037` `tan-neg_binary64_4984` `cos-neg_binary64_4983` `sin-neg_binary64_4982` `tan-0_binary64_4981` `cos-0_binary64_4980` `sin-0_binary64_4979` `hang-m-tan_binary64_4978` `hang-p-tan_binary64_4977` `hang-m0-tan_binary64_4976` `hang-p0-tan_binary64_4975` `hang-0m-tan_binary64_4974` `hang-0p-tan_binary64_4973` `tan-+PI/2_binary64_4972` `tan-+PI_binary64_4971` `tan-PI_binary64_4970` `tan-PI/3_binary64_4969` `tan-PI/4_binary64_4968` `tan-PI/6_binary64_4967` `cos-+PI/2_binary64_4966` `cos-+PI_binary64_4965` `cos-PI_binary64_4964` `cos-PI/2_binary64_4963` `cos-PI/3_binary64_4962` `cos-PI/4_binary64_4961` `cos-PI/6_binary64_4960` `sin-+PI/2_binary64_4959` `sin-+PI_binary64_4958` `sin-PI_binary64_4957` `sin-PI/2_binary64_4956` `sin-PI/3_binary64_4955` `sin-PI/4_binary64_4954` `sin-PI/6_binary64_4953` `sub-1-sin_binary64_4952` `sub-1-cos_binary64_4951` `-1-add-sin_binary64_4950` `-1-add-cos_binary64_4949` `1-sub-sin_binary64_4948` `1-sub-cos_binary64_4947` `cos-sin-sum_binary64_4946` `log-E_binary64_4942` `pow-base-0_binary64_4936` `unpow1/3_binary64_4919` `unpow2_binary64_4917` `unpow1/2_binary64_4916` `unpow0_binary64_4911` `unpow1_binary64_4910` `unpow-1_binary64_4909` `exp-cbrt_binary64_4906` `div-exp_binary64_4903` `rec-exp_binary64_4902` `exp-neg_binary64_4899` `e-exp-1_binary64_4897` `exp-0_binary64_4894` `rem-exp-log_binary64_4892` `cube-neg_binary64_4879` `rem-3cbrt-rft_binary64_4878` `rem-3cbrt-lft_binary64_4877` `rem-cbrt-cube_binary64_4876` `rem-cube-cbrt_binary64_4875` `sqr-abs_binary64_4867` `sqr-neg_binary64_4866` `rem-sqrt-square_binary64_4865` `rem-square-sqrt_binary64_4864` `mul-1-neg_binary64_4844` `+-lft-identity_binary64_4836` `div0_binary64_4833` `+-inverses_binary64_4831` `lft-mult-inverse_binary64_4830` `remove-double-div_binary64_4828` `difference-of-sqr--1_binary64_4823` `difference-of-sqr-1_binary64_4822` `distribute-frac-neg_binary64_4815` `distribute-neg-out_binary64_4814` `distribute-lft1-in_binary64_4807` `associate--l-_binary64_4790`

Counts

38 → 40

Iterations

Useful iterations: 1 (0.0ms)

Iter	Nodes	Cost
0	49	335
1	131	305
2	422	305
3	1024	305
4	3113	305
5	3351	305
6	4713	305

prune26.0ms (1.4%)

Pruning

1 alts after pruning (0 fresh and 1 done)

	Pruned	Kept	Total
New	40	0	40
Fresh	0	0	0
Picked	0	1	1
Done	0	0	0
Total	40	1	41

Error

Counts

41 → 1

Compiler

Compiled 451 to 98 computations (78.3% saved)

regimes47.0ms (2.5%)

Accuracy

Total 0.0b remaining (0%)

Threshold costs 0.0b (0%)

Compiler

Compiled 128 to 134 computations (-4.7% saved)

bsearch0.0ms (0%)

simplify3.0ms (0.1%)

Algorithm

1×	egg-herbie

Rules

2×	`+-commutative_binary64_4782`
1×	`*-commutative_binary64_4783`
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_5112` `if-if-and_binary64_5111` `if-if-or-not_binary64_5110` `if-if-or_binary64_5109` `if-not_binary64_5108` `if-same_binary64_5107` `if-false_binary64_5106` `if-true_binary64_5105` `tan-0_binary64_4981` `cos-0_binary64_4980` `sin-0_binary64_4979` `unpow1_binary64_4910` `e-exp-1_binary64_4897` `1-exp_binary64_4896` `exp-1-e_binary64_4895` `exp-0_binary64_4894` `sqr-abs_binary64_4867` `sqr-neg_binary64_4866` `neg-mul-1_binary64_4848` `neg-sub0_binary64_4847` `unsub-neg_binary64_4846` `sub-neg_binary64_4845` `mul-1-neg_binary64_4844` `/-rgt-identity_binary64_4843` `-rgt-identity_binary64_4842` `-lft-identity_binary64_4841` `remove-double-neg_binary64_4840` `sub0-neg_binary64_4839` `--rgt-identity_binary64_4838` `+-rgt-identity_binary64_4837` `+-lft-identity_binary64_4836` `cancel-sign-sub-inv_binary64_4818` `cancel-sign-sub_binary64_4817` `distribute-neg-frac_binary64_4816` `distribute-frac-neg_binary64_4815` `distribute-neg-out_binary64_4814` `distribute-neg-in_binary64_4813` `distribute-rgt-neg-out_binary64_4812` `distribute-lft-neg-out_binary64_4811` `distribute-rgt-neg-in_binary64_4810` `distribute-lft-neg-in_binary64_4809`

Iterations

Useful iterations: 0 (0.0ms)

Iter	Nodes	Cost
0	7	10
1	10	10

Proof

(+ f64 h0 (* f64 h1 (=> (+ f64 h2 h0))))
+-commutative_binary64_4782 =>
(+ f64 h0 (* f64 h1 (+ f64 h0 h2)))

end0.0ms (0%)

sample530.0ms (27.8%)

Algorithm

1×

intervals

Results

185.0ms	8000×	body	128	valid
17.0ms	590×	body	128	invalid

Compiler

Compiled 42 to 42 computations (0% saved)

Details

analyze265.0ms (13.9%)

sample16.0ms (0.8%)

simplify697.0ms (36.5%)

prune2.0ms (0.1%)

localize5.0ms (0.3%)

rewrite26.0ms (1.4%)

series139.0ms (7.3%)

simplify151.0ms (7.9%)

prune26.0ms (1.4%)

regimes47.0ms (2.5%)

bsearch0.0ms (0%)

simplify3.0ms (0.1%)

end0.0ms (0%)

sample530.0ms (27.8%)

Profiling