PLDI'22 Release

This version corresponds to the tool as described in the paper Recursion Synthesis with Unrelizability Witnesses submitted at PLDI'22.

The artifact has been packaged as a VM and is available on Zenodo:
https://zenodo.org/record/6329754

Version evaluated for Formal Methods in Sofware Design submission

This release identifies the version of the tool as evaluated for the submission to the Formal Methods and Software Design submission. You will find testing and result-reporting scripts in the benchmarks folder.
Experimental data is available in benchmarks/data.

Full Changelog: 0.2...fmsd22

Support for user-defined invariants

This version supports user-defined invariants, unrealizable benchmarks with feedback on possible repairs and automatic inference of invariants of the reference function.
There are many examples in the benchmarks/constraints and benchmarks/unrealizable folders.

For example, benchmarks/constraints/count_lt.ml is a synthesis task where the user has written a function counting the elements less than some parameter in a binary tree, and they want to synthesize an efficient function on binary search trees. To do that, the inputs of the target recursion skeleton are constrained to satisfy the is_bst by the attribute [@@requires is_bst].

CAV'21 Release

This release corresponds to the tool as described in the paper Counterexample-Guided Partial Bounding for Recursive Function Synthesis published at CAV'21.