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

https://doi.org/10.1007/978-3-319-96145-3_21

Last publication date

18 July 2018

ProVerB specific

View/edit source (Markdown)



ProVerB is a part of SLEBoK. Last updated: July 2022.