Add support for running multiple solvers in parallel #4
Description
The PolicyEquivalenceChecker class can currently be instantiated with a backend attribute, which can take the value of "z3" or "cvc5" currently. It would be nice if this could be changed so that a list of backends could be requested, or backend="*" could be specified (a shorthand for "all backends installed"). Then, the solver attribute on the PolicyEquivalenceChecker would be changed to a list of solvers (one for each backend). Finally, the methods encode, p_implies_q and q_implies_p would all be changed to make use of multiple solvers. The have_encoded attribute would need to be moved to the solver level. Each call to the solver's proof methods (e.g., return self.solver.p_implies_q would ideally happen in a new thread so that the using multiple solvers would run concurrently.