Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
cvc4-synthesis [2015/05/24 17:27] vkuncak |
cvc4-synthesis [2015/12/02 11:04] (current) reynolds |
||
---|---|---|---|
Line 8: | Line 8: | ||
==== Solver ==== | ==== Solver ==== | ||
- | The .tgz 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]] | + | 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". | ||
Line 27: | Line 27: | ||
https://www.starexec.org/starexec/secure/details/job.jsp?id=6561 | https://www.starexec.org/starexec/secure/details/job.jsp?id=6561 | ||
+ | |||
+ | |||
+ | ===== Refutation-Based Synthesis in SMT ===== | ||
+ | |||
+ | |||
+ | We provide the following supplementary material for [[http://lara.epfl.ch/~reynolds/FMSD2015-synth/smt-synth-RDKBT.pdf|this paper]]. | ||
+ | |||
+ | ==== Solver ==== | ||
+ | |||
+ | The zip archive containing the binary of CVC4 used in our experiments can be found here: [[http://lara.epfl.ch/~reynolds/FMSD2015-synth/cvc4-sygus.zip|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): [[http://lara.epfl.ch/~reynolds/FMSD2015-synth/results-general-fmsd.xls|results-general-fmsd.xls]]. | ||
+ | For the max family of benchmarks (Fig 10): [[http://lara.epfl.ch/~reynolds/FMSD2015-synth/results-max-fmsd.xls|results-max-fmsd.xls]]. | ||
+ | For benchmarks without syntactic restrictions (Fig 12): [[http://lara.epfl.ch/~reynolds/FMSD2015-synth/results-clia-fmsd.xls|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 below, which include additional configurations not mention in this paper. | ||
+ | |||
+ | For all solvers, except the latest version of CVC4, on benchmarks with syntactic restrictions: | ||
+ | |||
+ | https://www.starexec.org/starexec/secure/details/job.jsp?id=10526 | ||
+ | |||
+ | For all configurations of CVC4 on benchmarks with syntactic restrictions: | ||
+ | |||
+ | https://www.starexec.org/starexec/secure/details/job.jsp?id=10575 | ||
+ | |||
+ | For all solvers on the max family of benchmarks: | ||
+ | |||
+ | https://www.starexec.org/starexec/secure/details/job.jsp?id=11076 | ||
+ | |||
+ | For all solvers, except the latest version of CVC4, on benchmarks without syntactic restrictions: | ||
+ | |||
+ | https://www.starexec.org/starexec/secure/details/job.jsp?id=10556 | ||
+ | |||
+ | For CVC4 on benchmarks without syntactic restrictions: | ||
+ | |||
+ | https://www.starexec.org/starexec/secure/details/job.jsp?id=10597 | ||