MCSAT Modulo Transcendental Arithmetics
This work addresses the undecidable problem of SMT with transcendental functions, providing a practical solving method that outperforms existing solvers.
The paper proposes a framework for solving quantifier-free formulas in non-linear real arithmetic with transcendental functions, extending the MCSAT calculus. The prototype in Yices2 outperforms state-of-the-art solvers on both SAT and UNSAT instances.
We propose a framework for solving quantifier-free formulas from (undecidable) extensions of non-linear real arithmetic (NRA) with transcendental functions, such as exponential and trigonometric ones. The framework extends the Model Constructive Satisfiability calculus (MCSAT), and leverages procedures for NRA and methods from real analysis. At its core, our procedure abstracts the input formula to NRA, and lets MCSAT and an NRA plugin incrementally build a partial model of the abstracted formula. A Transcendental Real Arithmetic plugin, acting as an intermediary between MCSAT and the NRA plugin, ensures the consistency of the partial model and is responsible for refining the abstracted formula. We implemented our procedure in the Yices2 SMT solver for the sine and exponential functions, and conducted an extensive empirical evaluation that shows that our prototype outperforms state-of-the-art solvers on both SAT and UNSAT instances.