DryadSynth

Dryad Synthesizer for SyGuS competition.

For a complete description on methods, please see docs/pldi2020.pdf for CLIA and docs/popl2024.ppsx for bitvector.

Publications

• Reconciling enumerative and deductive program synthesis. Kangjing Huang, Xiaokang Qiu, Peiyuan Shen, and Yanjun Wang. In Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '20), pp. 1159-1174. 2020. author version.
• Enhanced Enumeration of Techniques for Syntax-Guided Synthesis of Bit-Vector Manipulations Yuantian Ding, Xiaokang Qiu, In Proc. 51st ACM SIGPLAN Symposium on Principles of Programming Languages (POPL '24), 2024. author version.
• A Concurrent Approach to String Transformation Synthesis. Yuantian Ding, Xiaokang Qiu, In Proc. Proc. 46th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '25), 2025. author version.

Installation and Running

Install the Synthesizer

To install DryadSynth, you need:

• Basic Linux Utilities:
  • gcc, g++, glibc-dev, zlib-dev, zlib-static, libstdc++-static for GraalVM compilation,
  • libssl-dev, pkg-config for OpenAI API,
  • cmake, python3, python3-pip for Z3 compilation,
  • See Dockerfile for more details about dependencies.
• Rust toolchain: rustup, cargo, rustc, rust-std installed.
• For bit-vector solver, make sure bitwuzla command installed in PATH.

And then simply install DryadSynth by

cargo +nightly-2025-03-13 install dryadsynth dryadsynth-bv synthphonia-rs

Then all executables will be put in ~/.cargo/bin directory. Note that you can also build DryadSynth using this repo. Simply run:

git clone https://github.com/purdue-cap/DryadSynth --recursive
cd DryadSynth && cargo build --release

Then all executables will be available in target/release directory. The executable depends on each other, so make sure target/release is in your path when you run dryadsynth:

PATH=$(pwd)/target/release:$PATH dryadsynth

Supported Platform

Platform	Test	Notes
linux-x64-glibc	Passed	See Dockerfile
macos-x64	Passed	Must use release mode, debug mode no bitvec support.

Run the Synthesizer

Once DryadSynth in installed in your system. The following command will be available in your environment:

• dryadsynth the main entry of the general solver, only general solving strategy options for SyGuS-IF (.sl) format supported, will call the sub-solvers in settings restricted in sygus-if2 format.
• dryadsynth-bv the bit-vector sub-solver, used to specify bit-vector specific options in our POPL'24 paper.
• synthphonia the string sub-solver, used to specify the string-related grammar and options. Use this command to obtain the result in our PLDI'25 paper.

Note: Some problems run in multithread by default. If you don't specify the number of threads, the CPU core count on your system would be used. This may cause unexpected behavior when the size of the CPU pool is large.