SMT solvers have recently been extended with techniques for finding models of universally quantified formulas in some restricted fragments of first-order logic. This paper introduces a translation that reduces axioms specifying a large class of recursive functions, including terminating functions, to universally quantified formulas for which these techniques are applicable. An evaluation confirms that the approach improves the performance of existing solvers on benchmarks from three sources. The translation is implemented as a preprocessor in the CVC4 solver and in a new higher-order model finder called Nunchaku.
CITATION STYLE
Reynolds, A., Blanchette, J., Cruanes, S., & Tinelli, C. (2016). Model finding for recursive functions in SMT. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9706, pp. 133–151). Springer Verlag. https://doi.org/10.1007/978-3-319-40229-1_10
Mendeley helps you to discover research relevant for your work.