Synthesizing Recursive Programs through Dataflow Constraints

Despite great progress in algorithms for synthesizing recur- sive programs, state of the art approaches continue to have several limitations. Principal among these is their inability to “invent” auxiliary functions. This makes them sensitive to the available set of primitive components. In this paper, we present an alternative approach to recover recursive pro- grams. We develop a system of constraints that characterizes patterns of data flow in the unrollings of a recursive program. Combined with a generator of seed nonrecursive circuits and a constraint solver, these constraints naturally form the basis of a general algorithm to synthesize recursive circuits.