Lemmas for satisfiability modulo transcendental functions via incremental linearization

Incremental linearization is a conceptually simple, yet effective, technique that we have recently proposed for solving satisfiability problems over nonlinear real arithmetic constraints, including transcendental functions. A central step in the approach is the generation of linearization lemmas, constraints that are added during search to the SMT problem and that form a piecewise-linear approximation of the nonlinear functions in the input problem. It is crucial for both the soundness and the effectiveness of the technique that these constraints are valid (to not remove solutions) and as general as possible (to improve their pruning power). In this extended abstract, we provide more details about how linearization lemmas are generated for transcendental functions, including proofs of their soundness. Such details, which were missing in previous publications, are necessary for an independent reimplementation of the method.