x <= y and y <= x + head [0,1,2] and P (f x - f y) and not (P 0) is unsatisfiable over these background theories (why?). Due to substantial performance improvements in recent years, SMT solvers have become valuable tools for verification, optimization and many other applications.
Today, many different SMT solvers have been developed, based on different algorithms that vary considerably in performance. A regular competition evaluates the performance of SMT solvers on a large set of benchmark problems.
In this project, you will identify features of these benchmark problems that allow to predict which SMT solver(s) will perform well on a given problem. Based on your performance predictions, you will implement a strategy-parallel solver that briefly analyzes a problem and applies those SMT solvers that are likely to perform well.