Metrics for invcot (example 3.9)

analyze8.0ms (0%)

Algorithm

1×

Search

Probability	Valid	Unknown	Precondition	Infinite	Domain	Can't	Iter
0%	0%	49.7%	50.3%	0%	0%	0%	0
0%	0%	49.7%	50.3%	0%	0%	0%	1
0%	0%	49.7%	50.3%	0%	0%	0%	2
25%	12.4%	37.3%	50.3%	0%	0%	0%	3
62.5%	31.1%	18.6%	50.3%	0%	0%	0%	4
81.3%	40.4%	9.3%	50.3%	0%	0%	0%	5
90.6%	45%	4.7%	50.3%	0%	0%	0%	6
95.3%	47.4%	2.3%	50.3%	0%	0%	0%	7
97.7%	48.5%	1.2%	50.3%	0%	0%	0%	8
98.8%	49.1%	0.6%	50.3%	0%	0%	0%	9
99.4%	49.4%	0.3%	50.3%	0%	0%	0%	10
99.7%	49.5%	0.1%	50.3%	0%	0%	0%	11
99.9%	49.6%	0.1%	50.3%	0%	0%	0%	12

Compiler

Compiled 16 to 11 computations (31.3% saved)

sample1.1min (99.7%)

Results

7.2s	4459×	2	valid-rival
3.5s	4362×	2	valid-sollya
1.2s	2400×	1	valid-rival
337.0ms	2399×	1	valid-sollya
2.1s	1355×	3	valid-rival
946.0ms	1023×	3	valid-sollya
1.7s	332×	3	exit-sollya
485.0ms	97×	2	exit-sollya
3.0ms	42×	0	valid-sollya
11.0ms	42×	0	valid-rival
5.0ms	1×	1	exit-sollya

Bogosity

preprocess101.0ms (0.2%)

Algorithm

1×	egg-herbie

Rules

44×	`fma-neg`
21×	`fma-define`
15×	`sub-neg`
14×	`distribute-lft-neg-in`
12×	`neg-mul-1`

Iterations

Useful iterations: 1 (0.0ms)

Iter	Nodes	Cost
0	17	124
1	33	116
2	68	116
3	146	116
4	229	116
5	278	116
6	287	116

Stop Event

1×

saturated

Calls

Call 1

Inputs
(-.f64 (/.f64 #s(literal 1 binary64) x) (/.f64 #s(literal 1 binary64) (tan.f64 x)))
(-.f64 (/.f64 #s(literal 1 binary64) x) (/.f64 #s(literal 1 binary64) (tan.f64 x)))
(-.f64 (/.f64 #s(literal 1 binary64) (neg.f64 x)) (/.f64 #s(literal 1 binary64) (tan.f64 (neg.f64 x))))
(neg.f64 (-.f64 (/.f64 #s(literal 1 binary64) (neg.f64 x)) (/.f64 #s(literal 1 binary64) (tan.f64 (neg.f64 x)))))

Outputs
(-.f64 (/.f64 #s(literal 1 binary64) x) (/.f64 #s(literal 1 binary64) (tan.f64 x)))
(+.f64 (/.f64 #s(literal 1 binary64) x) (/.f64 #s(literal -1 binary64) (tan.f64 x)))
(-.f64 (/.f64 #s(literal 1 binary64) x) (/.f64 #s(literal 1 binary64) (tan.f64 x)))
(+.f64 (/.f64 #s(literal 1 binary64) x) (/.f64 #s(literal -1 binary64) (tan.f64 x)))
(-.f64 (/.f64 #s(literal 1 binary64) (neg.f64 x)) (/.f64 #s(literal 1 binary64) (tan.f64 (neg.f64 x))))
(-.f64 (/.f64 #s(literal 1 binary64) (neg.f64 x)) (/.f64 #s(literal 1 binary64) (neg.f64 (tan.f64 x))))
(-.f64 (/.f64 #s(literal -1 binary64) x) (/.f64 #s(literal -1 binary64) (tan.f64 x)))
(+.f64 (/.f64 #s(literal -1 binary64) x) (/.f64 #s(literal 1 binary64) (tan.f64 x)))
(neg.f64 (-.f64 (/.f64 #s(literal 1 binary64) (neg.f64 x)) (/.f64 #s(literal 1 binary64) (tan.f64 (neg.f64 x)))))
(-.f64 (/.f64 #s(literal 1 binary64) x) (/.f64 #s(literal 1 binary64) (tan.f64 x)))
(+.f64 (/.f64 #s(literal 1 binary64) x) (/.f64 #s(literal -1 binary64) (tan.f64 x)))

Symmetry

(negabs x)

Compiler

Compiled 9 to 6 computations (33.3% saved)

eval0.0ms (0%)

Compiler: Compiled 1 to 1 computations (0% saved)

prune2.0ms (0%)

Alt Table

Click to see full alt table

Status	Accuracy	Program
	6.2%	(-.f64 (/.f64 #s(literal 1 binary64) x) (/.f64 #s(literal 1 binary64) (tan.f64 x)))

Compiler

Compiled 18 to 12 computations (33.3% saved)

simplify4.0ms (0%)

Algorithm

1×	egg-herbie

Rules

8×	`neg-mul-1`
7×	`unsub-neg`
4×	`sub-neg`
4×	`+-commutative`
3×	`*-rgt-identity`

Iterations

Useful iterations: 0 (0.0ms)

Iter	Nodes	Cost
0	11	29
1	18	29
2	26	29
3	32	29
4	39	29
5	51	29
6	67	29

Stop Event

1×

saturated

Calls

Call 1

Inputs
(-.f64 (/.f64 #s(literal 1 binary64) x) (/.f64 #s(literal 1 binary64) (tan.f64 x)))

Outputs
(-.f64 (/.f64 #s(literal 1 binary64) x) (/.f64 #s(literal 1 binary64) (tan.f64 x)))
(+.f64 (/.f64 #s(literal 1 binary64) x) (/.f64 #s(literal -1 binary64) (tan.f64 x)))

soundness1.0ms (0%)

Stop Event

1×

fuel

Compiler

Compiled 9 to 7 computations (22.2% saved)

preprocess81.0ms (0.1%)

Remove: (negabs x)
Compiler: Compiled 122 to 88 computations (27.9% saved)

invcot (example 3.9)

analyze8.0ms (0%)

sample1.1min (99.7%)

preprocess101.0ms (0.2%)

eval0.0ms (0%)

prune2.0ms (0%)

simplify4.0ms (0%)

soundness1.0ms (0%)

preprocess81.0ms (0.1%)

end0.0ms (0%)

Profiling