Hi all,
we are planning to have CHC-COMP’20 affiliated with HCVS at ETAPS (April 26), and as far as I know the HCVS chairs are reserving a slot for us to present the results.
Here are some questions for everybody in the forum:
(i) deadline for submitting solvers? My current plan would be to put the deadline in the second half of March, and to send out a call within the next 2 weeks;
(ii) should we add any tracks? In 2019 we had LRA, LIA, LIA+array, and LIA-nonlinear. We could consider to add a BV track;
(iii) benchmarks; if you have any benchmarks that can be made public, and are not yet available on github, please put them online. As deadline for this I propose March 15.
(iv) which teams are tentatively interested in participating?
Regards, Philipp
As announced yesterday, ETAPS has been postponed due to the virus situation, it is unclear when it will take place. This also means that HCVS, which is affiliated with ETAPS, will not take place on April 26. We are still discussing the implications for CHC-COMP.
Best wishes, Philipp
in the context of categorizing benchmarks I have also cleaned up the CHC-COMP SMT-LIB dialect a bit. I believe all changes capture points where the previous format definition was too restrictive or imprecise, so should not require modifications in the tools; please speak up if I am wrong here.
The updated format is here:
https://chc-comp.github.io/format2020.html
Changes are:
(1) allow set-info to specify, e.g., SMT-LIB format version or origin of benchmarks. Those commands can be safely ignored.
(2) de facto all benchmarks already end with an (exit); this command can be safely ignored as well.
(3) quantified facts, and cleaned up the case of facts without arguments or quantifiers.
(4) explicitly allow nullary predicates as well. As I interpret the outcome of the discussion a while ago, all tools are fine with nullary predicates already now.
Please let me know if any of the modifications might cause trouble!
My StarExec profile is https://www.starexec.org/starexec/secure/details/user.jsp?id=72 (i.e, my user ID is probably 72).
Here is the list of submissions I have received for the test runs:
Spacer: all tracks
PCSat: LIA, LIA-Lin
Ultimate Tree Automizer: all tracks
Ultimate Unihorn Automizer: all tracks
Sally: LRA-TS
Eldarica-abs: LIA, LIA-lin
prophic3: LIA-lin-arrays
ic3ia: LIA-lin, LIA-lin-arrays, LRA-TS
Hors Concours: Eldarica: LIA, LIA-lin, LIA-lin-arrays
The main question is whether we should impose a limit on
(1) wall-clock time, with each job running on a separate CPU with four cores, which might or might not be utilized by a solver.
(2) CPU time, which means that a solver utilizing multiple cores will eat up its time budget more quickly than a sequential solver.
Obviously, (1) will lead to parallel solvers getting more computation resources. (2) leads to a (smaller) advantage for sequential solvers, which do not have any overhead due to communication/synchronisation.
My preference is to go for (2) this year, and to add a dedicated track for parallel solvers next year that applies only a limit on wall-clock time.
Opinions?
Hi all!
We have now put online information about the next edition of the competition, CHC-COMP 2021:
https://chc-comp.github.io/
The web page in particular lists the tracks we are planning to evaluate, and tentative deadlines for submitting benchmarks, tools, and competition results.
If you are interested in joining CHC-COMP this year, please contact the organizers within the next couple of days, and provide the following pieces of information:
- Name of the solver(s) you are planning to submit
- Names of the people submitting
- Tracks you want to join (in particular, concerning the new tracks we are considering for this year)
[* Further comments or suggestions you might have]
Or feel free to provide this information in this forum.
Of course we hope for a similar number of participants as in the last years, and maybe a couple of new tools as well; please submit in large numbers and make sure that CHC-COMP stays alive!
Best wishes, Grigory & Philipp
ALL category? With non linear clauses and quantifier free clause bodies