SemGuS Solvers and Benchmarks

Two solvers for SemGuS problems are initially available: Messy and Bless.


Messy is a constraint-based Semgus solver that reduces synthesis into solving a set of CHCs, as described in the Semantics-Guided Synthesis paper. One key feature of Messy is that it can also prove unrealizability: that is, identify when synthesis problems do not have a solution.

View Messy on GitHub. Questions? Contact Jinwoo Kim.


Bless is an enumerative Semgus solver for example-based problems. It performs standard bottom-up enumeration of terms in the user’s language, optionally incorporating observational equivalence reduction to prune the search space. Bless is packaged with an interpreter for Semgus; we provide a command-line interface for both interpretation and synthesis tasks.

View Bless on GitHub. Questions? Contact Wiley Corning.


Some preliminary SemGuS benchmarks are initially available, including basic examples and regular expression benchmarks.

View SemGuS benchmarks on GitHub. Questions? Contact Wiley Corning.