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

[Zhoulai]

Hello,

We would like to participate in SMT-COMP 2016, but I have two questions
regarding the rules  (Earlier, I asked the questions below using another
unregistered email address, and I am unsure whether the emails were
successfully sent. Excuse me for the duplicate, if any)

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?


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?


Thanks.

Zhoulai

Zhoulai

On Sun, Apr 24, 2016 at 3:21 AM, Tjark Weber <tjark.weber at it.uu.se> wrote:

> The revised (draft) rules for SMT-COMP 2016 are now available on the
> competition website: http://smtcomp.sourceforge.net/2016/rules16.pdf
>
> These rules are open for comment through Saturday, April 30.
>
> There are several changes from last year. Notably, we are proposing to
> incorporate a weighting scheme for benchmark families in the definition
> of division scores, and we are reintroducing the unsat-core track that
> was part of SMT-COMP 2012. Please see Section 3 of the draft rules for
> a more detailed summary of changes.
>
> Since the SMT Workshop will be slightly earlier this year than in 2015,
> we have had to adjust the timeline accordingly. Current deadlines are
>
>    May 1 for new benchmark contributions
>    May 15 for first versions of solvers
>    May 29 for final versions of solvers
>
> Earlier (non-binding) indications of intention to enter a solver in the
> competition are appreciated by the organizers.
>
> Tjark Weber
> for the organizers
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib
>