A Multi-Backend Frontend for SMT Solvers in OCaml

João Maria Henriques Madeira Pereira

Key information

Authors:

João Maria Henriques Madeira Pereira (João Maria Henriques Madeira Pereira)

Supervisors:

José Faustino Fragoso Femenin dos Santos (José Faustino Fragoso Femenin dos Santos); Pedro Miguel dos Santos Alves Madeira Adão (Pedro Miguel dos Santos Alves Madeira Adão)

Published in

November 12, 2024

Abstract

Satisfiability Modulo Theories (SMT) solvers have proven to be highly effective and helpful in various domains, including software and hardware verification and test-case generation, among others. Consequently, numerous tools need to interface with SMT solvers during their execution. With the intent of efficiently facilitating this interaction within the OCaml programming language, SMT.ml was developed as a frontend for SMT solving that allows an OCaml program to easily interact with an SMT solver. However, the current version of SMT.ml exclusively supports the Z3 SMT solver. This can pose constraints on users, as Z3 may not be the optimal solver for all theories and applications. To address this limitation, we propose an enhanced version of SMT.ml that features an additional backend for cvc5, a state-of-the-art SMT solver that outperforms Z3 in multiple theories. To achieve this, we also developed OCaml bindings that enable direct interaction between SMT.ml and the cvc5 solver. These bindings will not only benefit SMT.ml but also provide value to OCaml developers aiming to incorporate the cvc5 SMT solver into their programs and other OCaml-based tools.