Differences

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

--- cvc4-synthesis [2015/12/02 10:54]
reynolds
+++ cvc4-synthesis [2015/12/02 11:04]
reynolds
@@ Line 45: / Line 45: @@
 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-fmsd2015-general.xls|results-fmsd2015-general.xls]].
+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-fmsd2015-max.xls|results-fmsd2015-max.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-fmsd2015-clia.xls|results-fmsd2015-clia.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:
+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 three configurations of CVC4:
+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
-https://www.starexec.org/starexec/secure/details/job.jsp?id=6561