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

[yangky11]

Please fix the code format issue.

[irene622]

Oh, I done black prover/evaluate.py.

[yangky11]

looks good to me, thx!