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.

翻译：我们提出了一种用于求解包含超越函数（如指数函数和三角函数）的非线性实数算术（NRA）的（不可判定）扩展中的无量词公式的框架。该框架扩展了模型构造可满足演算（MCSAT），并利用了NRA求解过程和实分析中的方法。其核心在于，我们的过程将输入公式抽象为NRA形式，并让MCSAT和NRA插件逐步构建抽象公式的部分模型。一个作为MCSAT与NRA插件中间层的超越实数算术插件，用于确保部分模型的一致性，并负责对抽象公式进行精化。我们在Yices2 SMT求解器中实现了针对正弦函数和指数函数的求解过程，并进行了广泛的实证评估。结果表明，我们的原型在SAT和UNSAT实例上均优于现有最先进的求解器。