Sibyl: Improving Software Engineering Tools with SMT Selection

SMT solvers are often used in the back end of different software engineering tools-e.g., program verifiers, test generators, or program synthesizers. There are a plethora of algorithmic techniques for solving SMT queries. Among the available SMT solvers, each employs its own combination of algorithmic techniques that are optimized for different fragments of logics and problem types. The most efficient solver can change with small changes in the SMT query, which makes it nontrivial to decide which solver to use. Consequently, designers of software engineering tools often select a single solver, based on familiarity or convenience, and tailor their tool towards it. Choosing an SMT solver at design time misses the opportunity to optimize query solve times and, for tools where SMT solving is a bottleneck, the performance loss can be significant. In this work, we present Sibyl, an automated SMT selector based on graph neural networks (GNNs). Sibyl creates a graph representation of a given SMT query and uses GNNs to predict how each solver in a suite of SMT solvers would perform on said query. Sibyl learns to predict based on features of SMT queries that are specific to the population on which it is trained - avoiding the need for manual feature engineering. Once trained, Sibyl makes fast and accurate predictions which can substantially reduce the time needed to solve a set of SMT queries. We evaluate Sibyl in four scenarios in which SMT solvers are used: in competition, in a symbolic execution engine, in a bounded model checker, and in a program synthesis tool. We find that Sibyl improves upon the state of the art in nearly every case and provide evidence that it generalizes better than existing techniques. Further, we evaluate Sibyl's overhead and demonstrate that it has the potential to speedup a variety of different software engineering tools.