Integrating the SMT solver dReal to the framework JavaSMT

SMT solvers are widely utilized in computer-guided verification of computer programs and artificial intelligence. With a multitude of theories employed in these solvers, it is beneficial to have access to a diverse range of solvers and to minimize the challenge of learning a new API for each of them. Using the solver’s own API directly makes it difficult to switch to another solver without rewriting extensive parts of the application, as there is no standardized binary API for SMT solvers. Also, since these SMT solvers have varying degrees of capabilities and performance and may not accept the same input, frameworks were created, that offer a unified API to several SMT solvers. JavaSMT has exactly these attributes, a common API for SMT solvers. The framework provides access to a variety of solvers created using Java and other programming languages. Although most solvers share a common set of supported theories and features, their availability of extra theories and performance may differ. Therefore, the inclusion of additional solvers in the framework is advantageous to its users. SMT formulas over the real numbers can encode a wide range of problems in theorem proving and formal verification. Such formulas are very hard to solve when nonlinear functions are involved. For that reason, the SMT solver dReal will be implemented in JavaSMT. The SMT solver dReal is a solver that solves nonlinear formulas over the reals. The solver can handle various nonlinear real functions such as polynomials, trigonometric functions, exponential functions, etc. The goal of the project will be to integrate the SMT solver dReal into the JavaSMT framework and to include it in the existing JavaSMT tests.