Differences
This shows you the differences between two versions of the page.
Next revision | Previous revision Next revision Both sides next revision | ||
cvc4-synthesis [2015/05/24 17:25] vkuncak created |
cvc4-synthesis [2015/05/24 17:28] vkuncak |
||
---|---|---|---|
Line 6: | Line 6: | ||
We provide the following supplementary material for [[http://lara.epfl.ch/~reynolds/CAV2015-synth/smt-synth-RDKBT.pdf|this paper]]. | We provide the following supplementary material for [[http://lara.epfl.ch/~reynolds/CAV2015-synth/smt-synth-RDKBT.pdf|this paper]]. | ||
- | Solver | + | ==== Solver ==== |
- | The .tgz containing the binary of CVC4 used in our experiments can be found here: cvc4-sygus.zip | + | The zip archive containing the binary of CVC4 used in our experiments can be found here: [[http://lara.epfl.ch/~reynolds/CAV2015-synth/cvc4-sygus.zip|cvc4-sygus.zip]] |
- | Configuration cvc4+sg from the paper is enabled by command line parameters "--cegqi --dump-synth". | + | * 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-r is enabled by "--cegqi-si --dump-synth --no-cegqi-si-reconstruct" |
- | Configuration cvc4+si is enabled by "--cegqi-si --dump-synth" | + | * 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. | + | ==== Results ==== |
+ | |||
+ | The spreadsheet summarizing the results for the benchmarks considered in this paper can be accessed here: [[http://lara.epfl.ch/~reynolds/CAV2015-synth/results-cav2015-synth.xls|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: | 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 ESolver: |
- | For all three configurations of CVC4:https://www.starexec.org/starexec/secure/details/job.jsp?id=6561. | + | |
+ | 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 |