PV2 ⊧ PLearnsynthesises a program conforming to a subgrammar of a given grammar

Black-box framework that runs multiple parallel instances of a SyGuS (syntax-guided synthesis) tool with different grammars

Application domain/field

• Syntax-guided synthesis (SyGuS)
• Counterexample-guided inductive synthesis (CEGIS)

Type of tool

? Synthesis tool? Metatool?

Expected input

• Synthesis tool
• SyGuS problem
• Subgrammars ${ℰ}_{1..p}$ such that ${ℰ}_i\subseteq ℰ$

Expected output

First solution that was found or $\perp$ if no solution could be found.

Internals

The idea behind the tool is that SyGuS tools are sensitive to the choice of grammar. Sometimes increasing the grammar expressiveness allows the tool to solve some problems that are unsolvable with less expressive grammars. However, it is possible that the tool can no longer solve some problems that could be solved with less expressive grammars.