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.
|Title of host publication||Automated Reasoning - 8th International Joint Conference|
|Subtitle of host publication||IJCAR 2016, Coimbra, Portugal, June 27 - July 2, 2016, Proceedings|
|Publication status||Published - 2016|
Reynolds, A., Blanchette, J. C., Cruanes, S., & Tinelli, C. (2016). Model Finding for Recursive Functions in SMT. In Automated Reasoning - 8th International Joint Conference: IJCAR 2016, Coimbra, Portugal, June 27 - July 2, 2016, Proceedings (pp. 133-151). Springer. https://doi.org/10.1007/978-3-319-40229-1_10