Semantics-Guided Synthesis Benchmarks

This repository contains benchmark files for SemGuS. For more information about the benchmark format, please refer to the SemGuS format specification document.

Overview

The benchmarks are in the benchmarks folder and organized into directories based on the domain of the benchmark. These names are somewhat arbitrary, as we do not have set "tracks" for SemGuS benchmarks at this time. There are five overall categories:

• Bitvector benchmarks
• Boolean formula benchmarks
• Regular expression benchmarks
• Benchmarks from Messy (mostly unrealizable)
• Samples in other domains (integer arithmetic, datatypes, and imperative programs)

Benchmark Contributions

Contributions of new benchmarks are welcome. Open a pull request that adds the new benchmarks, and a maintainer will review the submission.

• Benchmarks must be categorized into appropriate folders, e.g. non-deterministic or imperative. If an appropriate folder does not exist, feel free to create it in your pull request.
• All contributed benchmarks must pass a syntax check before being approved, based on the current release of the SemGuS Parser. To test a benchmark locally, install the parser and verify the benchmark: semgus-parser --format verify -- <your-benchmark.sl>
• Feel free to create discussion posts with any questions, or issues about potential bugs in existing benchmarks.