Built-in Treatment of an Axiomatic Floating-Point Theory for SMT Solvers

The treatment of the axiomatic theory of oating-point numbers is out of reach of current SMT solvers, especially when it comes to automatic reasoning on approximation errors. In this paper, we describe a dedicated procedure for such a theory, which provides an interface akin to the instantiation mechanism of an SMT solver. This procedure is based on the approach of the Gappa tool: it performs saturation of consequences of the axioms, in order to rene bounds on expressions. In addition to the original approach, bounds are further rened by a constraint solver for linear arithmetic. Combined with the natural support for equalities provided by SMT solvers, our approach improves the treatment of goals coming from deductive verication of numerical programs. We have implemented it in the Alt-Ergo SMT solver.