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 zip archive 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
Refutation-Based Synthesis in SMT
We provide the following supplementary material for this paper.
Solver
The zip archive 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. For benchmarks with syntactic restrictions (Fig 9 and Fig 11): results-general-fmsd.xls. For the max family of benchmarks (Fig 10): results-max-fmsd.xls. For benchmarks without syntactic restrictions (Fig 12): results-clia-fmsd.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 all three configurations of CVC4:
https://www.starexec.org/starexec/secure/details/job.jsp?id=6561