Smt.ml: A Multi-Backend Frontend for SMT Solvers in OCaml
摘要
SMT solvers are essential for applications in artificial intelligence, software verification, and optimisation. However, no single solver excels across all formula types, and different applications may require the use of different solvers. While the SMT-LIB language enables multi-solver support, it also incurs heavy I/O overhead. To address this, we introduce Smt.ml, an SMT-solver frontend for OCaml that simplifies integration with various solvers through a consistent interface. Its parametric encoding facilitates the easy addition of new solver backends, while optimisations like formula simplification, result caching, and detailed error feedback enhance performance and usability. Furthermore, Smt.ml is the only SMT frontend that includes a simplification-management engine for streamlining the integration of new formula simplifications and the verification of their correctness. Our evaluation demonstrates that Smt.ml ’s results are consistent with those of its backend solvers and that its optimisations are highly effective on formulas generated from the symbolic execution of an extensive program-analysis benchmark.