Differences

This shows you the differences between two versions of the page.

--- cvc4-synthesis [2015/05/24 17:25]
vkuncak created
+++ cvc4-synthesis [2015/12/02 10:56]
reynolds
@@ Line 6: / Line 6: @@
 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:
-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
+===== 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:
+For all three configurations of CVC4:
+https://www.starexec.org/starexec/secure/details/job.jsp?id=6561