The SemGuS Toolkit

TL;DR

The SemGuS Toolkit offers a flexible, standardized framework and open-source tools for defining, verifying, and solving synthesis problems across various domains, facilitating benchmarking and comparison of different solvers.

Contribution

It introduces the SemGuS format, an open-source toolkit with parser, verifier, and solvers, and provides initial benchmarks for synthesis problem evaluation.

Findings

Baseline enumerative solvers demonstrate competitive performance.

Standardized SemGuS format enables consistent problem definition.

Benchmarks facilitate solver comparison and future research.

Abstract

Semantics-Guided Synthesis (SemGuS) is a programmable framework for defining synthesis problems in a domain- and solver-agnostic way. This paper presents the standardized SemGuS format, together with an open-source toolkit that provides a parser, a verifier, and enumerative SemGuS solvers. The paper also describes an initial set of SemGuS benchmarks, which form the basis for comparing SemGuS solvers, and presents an evaluation of the baseline enumerative solvers.