Recursion Synthesis with Unrealizability Witnesses (Software Artifact)

We propose SE2GIS, a novel inductive recursion synthesis approach with the ability to both synthesize code and declare the problem unsolvable. SE2GIS combines a symbolic variant of counterexample-guided inductive synthesis (CEGIS) with a new dual inductive procedure, which focuses on proving a synthesis problem unsolvable rather than finding a solution for it. A vital component of this procedure is a new algorithm with the capability of producing a witness, a set of concrete assignments to relevant variables, as proof that the synthesis instance is not solvable. Witnesses in the dual inductive procedure play the same role that solutions do in classic CEGIS; that is, they ensure progress. Given a reference function, invariants on the input recursive data types and a target family of recursive functions, SE2GIS synthesizes an implementation in this family that is equivalent to the reference implementation, or declares the problem unsolvable and produces a witness for it. We demonstrate that SE2GIS is effective in both cases; that is, for interesting data types with complex invariants, it can synthesize non-trivial recursive functions or output witnesses that contain useful feedback for the user.This software artifact is provided to support the experimental claims made in the conference paper Recursion Synthesis with Unrealizability Witnesses to appear at PLDI'22