Synthesizing Recursive Programs Through Dataflow Constraints
Despite great progress in recursive program synthesis, state of the art approaches continue to have several limitations. Current recursive synthesizers are unable to invent auxiliary functions, resulting in (a) the inability to synthesize mutually recursive functions, (b) sensitivity to the provided auxiliary functions, and (c) occasionally producing asymptotically sub-optimal implementations. In this paper, we present an alternative approach where we recover a recursive program from a non-recursive implementation. We develop a system of constraints that characterizes patterns of data flow in recursive program unrollings. Combined with a generator of seed non-recursive circuits and an appropriate constraint solver, these constraints will naturally form the basis of a general algorithm to synthesize recursive circuits.