On Satisfiability Modulo Computable Functions

We present a semi-decision procedure for checking satisfiability of formulas in the language of algebraic data types and integer linear arithmetic extended with user-defined terminating recursive functions. Our procedure is designed to integrate into a DPLL(T) solver loop, using blocking clauses to control function definition unfolding. The procedure can check the faithfulness of candidate counterexamples using code execution. It is sound for proofs and counterexamples. Moreover, it is terminating and thus complete for many important classes of specifications: for satisfiable specifications, for specifications whose recursive functions are sufficiently surjective, and for functions annotated with inductive postconditions. We have implemented our system in Scala, building on top of the Z3 API and Z3's plugin mechanism. Our results show our approach to be superior in practice to the alternative of encoding recursive functions as quantified axioms. Using our system, we verified detailed correctness properties for functional data structure implementations, as well as Scala syntax tree manipulations. We have found our system to be fast for both finding counterexamples and finding proofs for inductively annotated specifications. Furthermore, it can quickly enumerate many test cases satisfying a given functional precondition, which can then be used to test both functional and imperative code. Thanks to our tool, many SMT solver clients, including verifiers and synthesizers, can benefit from the expressive power of recursive function definitions within formulas.