I have an implementation in Python that makes use of theorem proving. I would like to know if there is a possibility to speed up the SMT solving part, which is currently using Z3.
I am trying to discover different solvers, and have found cvc4/cvc5 and Yices as multiple-theory (arithmetics, equality, bitvectors...) solvers. I also found dReal and MetiTarski (this one seems to be out to date) for the concrete case of real arithmetics.
My intention is to test my implementation with those tools' APIs to see whether I can use one or other solver depending on the sort I want to solve.
However, I would like to know in advance if there is some kind of comparison between these solvers in order to have a more useful foundation for my findings. I am interested in both standard benchmarks or user-tests out there in GitHub or Stack.
I only found this paper of cvc5 (https://www-cs.stanford.edu/~preiner/publications/2022/BarbosaBBKLMMMN-TACAS22.pdf), which, obviously suggests it as the best option. I also found this minimal comparison (https://lemire.me/blog/2020/11/08/benchmarking-theorem-provers-for-programming-tasks-yices-vs-z3/) that tells us Yices is 15 times faster than Z3 for a concrete example.
Any advise?
You can always look at the results of SMT competition: https://smt-comp.github.io
Having said that, I think it’s a fool’s errand to look for the “best.” There isn’t a good yard stick to compare all solvers in a meaningful way: it all depends on your particular application.
If your system allows for using multiple backend solvers, why not take advantage of the many cores on modern machines: spawn all of them and take the result of first to complete. Any a priori selection of the solver will suffer from a case where another will perform better. At this point, running all available and taking the fastest result is the best option to utilize your hardware.