When evaluation done, add case which all theorem is discarded. Modify num_gpus in ray.init

[irene622]

Hi, I experiment your code, I think the some of code would be good if it is changed.

1. After evaluation is done, in my experiment, all theorem are discarded, so I meet ZeroDivisionError. Hence, by using if, adding the case of all theorem are discarded can avoid the ZeroDivisionError.

2. When evaluating with gpus and cpus more than 2 respectively, ray.init takes the argument num_gpus as num_cpus. It cause the error in case of num gpus and num cpus are not equal. I think it is typo, because it is easy to confuse num_cpus and num_gpus. So, add torch.cuda.device_count() to find num_gpus instead of getting num_gpus as arguments.

Thank you for spending your time, I hope to merge my modification soon. :)

[yangky11]

Thank you for the PR! Please see my comments in the code.

[irene622]

Thanks, I change them! Please merge them. :)

[yangky11]

@irene622 The black code formatter failed. Could you please fix it (black prover/evaluate.py)? Thx

[irene622]

Oh, I done black prover/evaluate.py.