We present a novel approach for the synthesis of recursive programs from relational, mixed-quantifier first-order logic properties. We solve this problem using a sketching-based, enumerative, counterexample-guided approach. Our algorithm learns syntactic constraints from counterexamples to prune the candidate space and employs a prophylactic pruning technique to avoid enumerating invalid candidates altogether. We implement our technique in a tool called Cataclyst and evaluate it on a suite of 60 benchmarks. We demonstrate that both counterexample generalization and prophylactic pruning significantly improve performance. Cataclyst solves 59/60 benchmarks, while variants of Cataclyst without counterexample generalization or prophylactic pruning solve fewer benchmarks. No existing tool can directly handle the entire class of synthesis problems that our tool can. A portfolio of existing state-of-the-art tools solves 30/60 of our benchmarks.

翻译：暂无翻译