Efficient Term-ITE Conversion for Satisfiability Modulo Theories

This paper describes how term-if-then-else ( term-ITE ) is handled in Satisfiability Modulo Theories (SMT) and to decide Linear Arithmetic Logic ( LA ) in particular. Term-ITEs allow one to conveniently express verification conditions; hence, they are very common in practice. However, the theory provers of SMT solvers are usually designed to work on conjunctions of literals; therefore, the input formulae are rewritten so as to eliminate term-ITEs. The challenge in rewriting is to avoid introducing too many new variables, while avoiding as often as possible the exponential explosion that is frequent when a naive approach is applied. We propose a solution that is based on cofactoring and theory propagation, which often produces orders-of-magnitude speedups in several SMT solvers for LA problems.