Date:	Friday, May 12th, 2023
Commit:	471e4502 on rr-proofs
Hostname:	nightly with Racket 8.6
Seed:	2023131
Parameters:	256 points for 4 iterations
Flags:	`reduce:regimesreduce:avg-errorreduce:binary-searchreduce:branch-expressionssetup:simplifysetup:searchrules:arithmeticrules:polynomialsrules:fractionsrules:exponentsrules:trigonometryrules:hyperbolicrules:numericsrules:specialrules:boolsrules:branchesgenerate:rrgenerate:taylorgenerate:simplify` default

Details

sample9.5min (32.5%)

Results

2.7min	16921×	body	8192	exit
1.8min	69908×	body	1024	valid
1.2min	8881×	body	4096	valid
1.2min	294832×	body	256	valid
43.8s	14730×	body	2048	valid
34.5s	1648×	body	8192	valid
28.4s	34656×	body	512	valid
12.1s	6357×	body	1024	infinite
7.3s	21580×	body	256	infinite
7.3s	833×	body	4096	infinite
7.2s	1263×	body	2048	infinite
5.7s	17013×	body	256	unsamplable
4.6s	21848×	body	256	invalid
3.5s	3300×	body	512	infinite
1.3s	1225×	body	2048	invalid
1.2s	1678×	body	1024	invalid
589.0ms	1163×	body	512	invalid
540.0ms	31×	body	8192	infinite
139.0ms	892×	body	256	precondition
6.0ms	9×	body	512	unsamplable
4.0ms	3×	body	1024	unsamplable

Bogosity

eval4.6min (15.5%)

Compiler: Compiled 11074435 to 6214952 computations (43.9% saved)

regimes4.3min (14.6%)

Counts

24988 → 1039

Calls

143 calls:

13.9s	B
13.8s	phi2
13.3s	phi1
12.4s	C
12.0s	lambda2

Results

Compiler

Compiled 657083 to 352715 computations (46.3% saved)

soundness2.1min (7.3%)

Rules

77402×	`associate-/r*`
74016×	`*-commutative`
72734×	`associate-r`
71090×	`associate-+r+`
69428×	`+-commutative`

Stop Event

2×	unsound
8×	saturated
157×	node limit

Compiler

Compiled 26307 to 14993 computations (43% saved)

simplify2.0min (6.9%)

Algorithm

798×	egg-herbie

Rules

478726×	`associate-r`
440096×	`*-commutative`
432056×	`associate-/l*`
400944×	`distribute-lft-in`
396682×	`associate-l`

Stop Event

1×	unsound
68×	saturated
6×	done
42×	fuel
729×	node limit

Counts

128479 → 155486

Compiler

Compiled 17673 to 11003 computations (37.7% saved)

prune1.8min (6.2%)

Counts: 214061 → 8862
Compiler: Compiled 496314 to 344532 computations (30.6% saved)

rewrite1.8min (6.1%)

Algorithm

699×	batch-egg-rewrite

Rules

431506×	`add-sqr-sqrt`
422714×	`*-un-lft-identity`
397902×	`add-cube-cbrt`
393916×	`add-cbrt-cube`
282132×	`add-exp-log`

Stop Event

7×	unsound
692×	node limit

Counts

1784 → 87540

bsearch1.1min (3.7%)

Algorithm

541×	binary-search
34×	left-value

Stop Event

527×	narrow-enough
14×	predicate-same

Results

22.9s	14503×	body	1024	valid
12.8s	39210×	body	256	valid
8.6s	1619×	body	4096	valid
7.9s	3640×	body	2048	valid
5.9s	6106×	body	512	valid
2.8s	141×	body	8192	valid
834.0ms	63×	body	4096	infinite
727.0ms	3278×	body	256	invalid
249.0ms	57×	body	2048	infinite
226.0ms	79×	body	1024	infinite
182.0ms	453×	body	256	infinite
166.0ms	41×	body	512	infinite
30.0ms	51×	body	1024	invalid
20.0ms	49×	body	512	invalid
13.0ms	1×	body	8192	infinite
7.0ms	8×	body	2048	invalid

Compiler

Compiled 187491 to 134081 computations (28.5% saved)

localize49.6s (2.8%)

Compiler: Compiled 96462 to 48397 computations (49.8% saved)

analyze48.4s (2.7%)

Algorithm

53×

Search

Probability	Valid	Unknown	Precondition	Infinite	Domain	Can't	Iter
0%	0%	79.4%	20.6%	0%	0%	0%	0
2.4%	1.9%	77.5%	20.6%	0%	0%	0%	1
5.1%	4%	75%	21%	0%	0%	0%	2
12.7%	9.8%	67.2%	21.2%	0.5%	1.4%	0%	3
20.5%	15.3%	59.4%	21.2%	1.1%	2.6%	0.5%	4
26.8%	19.7%	53.7%	21.2%	1.3%	3.4%	0.7%	5
32.2%	23.1%	48.7%	21.2%	1.7%	4.2%	1.1%	6
35%	24.7%	45.9%	21.2%	2%	4.9%	1.2%	7
37.7%	26.3%	43.5%	21.3%	2.3%	5.3%	1.4%	8
41.6%	28.6%	40.1%	21.3%	2.7%	6%	1.5%	9
43.1%	29.4%	38.8%	21.3%	2.7%	6.3%	1.6%	10
45.8%	31%	36.7%	21.3%	2.8%	6.6%	1.6%	11
48.4%	32.6%	34.7%	21.3%	2.8%	7%	1.7%	12

Compiler

Compiled 1919 to 1338 computations (30.3% saved)

series18.7s (1.1%)

Counts

1784 → 40888

Calls

11346 calls:

Time	Variable		Point	Expression
1.7s	phi2	@	0	(pow.f64 (cbrt.f64 (.f64 R (hypot.f64 (.f64 (cos.f64 (*.f64 (+.f64 phi1 phi2) 1/2)) (-.f64 lambda1 lambda2)) (-.f64 phi1 phi2)))) 3)
347.0ms	lambda2	@	-inf	(-.f64 (exp.f64 (log1p.f64 (*.f64 (sin.f64 (-.f64 lambda1 lambda2)) (cos.f64 phi2)))) 1)
326.0ms	delta	@	-inf	(pow.f64 (cbrt.f64 (.f64 (sin.f64 delta) (.f64 (cos.f64 phi1) (sin.f64 theta)))) 3)
113.0ms	b	@	-inf	(exp.f64 (log1p.f64 (.f64 (.f64 1/4 (sqrt.f64 8)) (.f64 (.f64 (sqrt.f64 2) b) y-scale))))
109.0ms	theta	@	-inf	(log.f64 (.f64 (sin.f64 delta) (.f64 (cos.f64 phi1) (sin.f64 theta))))

end6.7s (0.4%)

Compiler: Compiled 16705 to 7471 computations (55.3% saved)

preprocess5.9s (0.3%)

Algorithm

102×	egg-herbie

Rules

32198×	`fma-def`
26296×	`*-commutative`
22918×	`+-commutative`
19502×	`distribute-lft-in`
19386×	`associate-/r*`

Stop Event

60×	saturated
5×	unsound
37×	node limit

Compiler

Compiled 1762 to 1250 computations (29.1% saved)

Details

sample9.5min (32.5%)

eval4.6min (15.5%)

regimes4.3min (14.6%)

soundness2.1min (7.3%)

simplify2.0min (6.9%)

prune1.8min (6.2%)

rewrite1.8min (6.1%)

bsearch1.1min (3.7%)

localize49.6s (2.8%)

analyze48.4s (2.7%)

series18.7s (1.1%)

end6.7s (0.4%)

preprocess5.9s (0.3%)

Profiling