This is an old revision of the document!
Synthesis within CVC4
Counterexample Guided Quantifier Instantiation for Synthesis in SMT
We provide the following supplementary material for this paper.
Solver
The .tgz containing the binary of CVC4 used in our experiments can be found here: cvc4-sygus.zip
Configuration cvc4+sg from the paper is enabled by command line parameters “–cegqi –dump-synth”. Configuration cvc4+si-r is enabled by “–cegqi-si –dump-synth –no-cegqi-si-reconstruct” Configuration cvc4+si is enabled by “–cegqi-si –dump-synth” Results
The spreadsheet summarizing the results for the benchmarks considered in this paper can be accessed here: results-cav2015-synth.xls.
Our evaluation used the StarExec cluster for evaluation https://www.starexec.org. The jobs we ran in our evaluation are publicly available, and can be accessed by logging into StarExec as a guest (click “Guest” at the bottom of the log in page). The links to the individual jobs are:
For ESolver: https://www.starexec.org/starexec/secure/details/job.jsp?id=6440. For all three configurations of CVC4:https://www.starexec.org/starexec/secure/details/job.jsp?id=6561.