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.
The
PolicyEquivalenceCheckerclass can currently be instantiated with abackendattribute, 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, orbackend="*"could be specified (a shorthand for "all backends installed"). Then, thesolverattribute on thePolicyEquivalenceCheckerwould be changed to a list of solvers (one for each backend). Finally, the methodsencode,p_implies_qandq_implies_pwould all be changed to make use of multiple solvers. Thehave_encodedattribute would need to be moved to the solver level. Each call to the solver's proof methods (e.g.,return self.solver.p_implies_qwould ideally happen in a new thread so that the using multiple solvers would run concurrently.