[SMT-LIB] SMT-COMP 2016: Draft Rules and Timeline Available

[Tjark Weber]

Dear Zhoulai,

On Mon, 2016-05-09 at 05:16 +0800, Zhoulai wrote:
> Question 1: The first paragraph of page 7 of your rules and procedures
> draft reads: "Persistent state. Solvers may create and write to files
> and directories during the course of an execution, but they must not
> read such files back during later executions. " 
> 
> Our solver has to create a file before solving the constraint, and
> when it solves the constraint, it loads that file.  More concretely,
> we create a Python's C extension file and then compile it to a .so
> file and load it as a Python module for calculating the model. Is this
> allowable?

Yes, assuming you do this separately for each benchmark. The paragraph
that you quoted disallows using information from one benchmark to solve
other benchmarks later.

> Question 2: Following your "rules and procedures",  the benchmark will
> not be finalized until 22 May, but the solvers need to be submitted
> before that date, on 15 May.  Does it imply that the competitors are
> not supposed to know about the benchmark before the competition?  Or
> maybe will this year's benchmark be the same to those used in 2015?

The benchmarks will come from the SMT-LIB, which means that they will
largely be the same as in 2015 (but hopefully there will be some new
benchmarks as well).

Note that the deadline on May 15 is only for first versions of solvers.
It is still possible to make changes until May 29, the deadline for
final solver versions.

We intend to finalize the set of competition benchmarks before that
date, so that solver developers have at least a few days to explore all
benchmarks and tune solvers accordingly.

Best,
Tjark