PV2 QuaSitries to solve a SyGuS problem with quantitative objectives

Application domain/field

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
Synthesis

Links

Repository: Cannot find one in the paper or on the first author's website.

Related papers

Syntax-Guided Synthesis with Quantitative Syntactic Objectives

Last publication date

18 July 2018

ProVerB specific



ProVerB is a part of SLEBoK. Last updated: February 2023.