PV2 ⊧ QuaSitries to solve a SyGuS problem with quantitative objectives

Application domain/field

• Syntax-guided synthesis (SyGuS)
• Program synthesis
• Quantitative objectives

Type of tool

Synthesis tool

Expected input

QSyGuS problem (SyGuS problem with quantitative objectives)

Format:

Extension of the SyGuS format

Expected output

It times out or presents the solution to the QSyGuS problem. A solution to the QSyGuS problem is a term, in the language of the provided grammar, such that the Boolean formula constraining the semantic behavior is satisfied, and such that the constraints over the weight $w$ of the synthesized program is true.

Internals

Quasi is a tool for specifying and solving QSyGuS problems. QSyGuS: "syntax-guided synthesis problems with quantitative objectives over the syntax of the synthesized program, e.g. find the most likely program with respect to a given probability distribution" Uses CVC4, ESolver, EUSolver