please look at the questions in the google doc and reply or remove
btw: we can also use pysmt to normalize benchmarks
but restricting to only a single query will lead to a lot of duplication, for the benchmarks that already contain multiple queries
But here is a more fundamental question: do we want to require the restricted grammar from the Google document for all benchmarks in the repo, or should we rather provide a set of pre-processors that can be used to convert any (clausal) SMT-LIB benchmark into restricted form if needed?
I don't think we can come up with a grammar that will satisfy everybody (e.g., thinking about the let-binders, which are needed for some benchmarks, but hard to support for some tools)
a more pragmatic approach would be to accept benchmarks in extended form in the repository, and then let the tools simplify the benchmarks themselves (possibly using pre-processors provided by the competition) if they don't support all features
but this is equivalent to asking whether each query can be solved
- we collect all benchmarks that can potentially be converted to something the community is interested in. They leave in separate repos and are curated by the group interested in them (e.g., VMT benchmarks from Alberto). We don't worry about format. The community of interest will, since otherwise their benchmarks will not be used by tool builders.
- Each competition, we select subset of benchmarks for each category. I don't know the selection process. We will figure it out as we go. The goal is to be somewhat representative, reduce noise (i.e., similar benchmarks), while reducing running time (i.e., you should not need a huge cluster and years of cpu time to reproduce competition run for a few tools)
As such, right now, we only need to worry what format we want for the competition benchmarks. We will then ensure that during our selection process we end up only with benchmarks that fit the format. This is likely to require conversion tools, but they can be highly specialized to the benchmarks we have now (which is much easier)
single vs multi-query: it is easier to judge when solving a benchmark == solving one query
in HWMCC, there are separate tracks: single and multiple for single and multiple properties, respectively. Most tools participate in single track only. Multi-property track has more complicated rules (to address @dddejan concerns) and is geared towards solvers that do something special for multiple queries (as opposed to encode them into a single query). There is also a question of interpretation -- with multiple properties in HWMCC is to detect the subset of queries that are true. This is harder to define for CHC.
In summary, for this year, let's come up with the format(s) for the competition. Let's populate initial benchmark set for the competition. Figure out how to run everything (starexec, rules, collecting results, t-shirts for participants, sponsors?!, ) etc. And once we have everything going, next year we can discuss how to tweak things to go to the direction community is more interested in (SMT-LIB logic specification, support by other tools (i.e., pysmt), categories, tracks, etc.)
@/all thanks for commenting on the format. I've incorporated the comments and started a short discussion. The discussion requires your vote, please do so as quickly as you can. For now, I'll maintain the discussion in an ad-hoc google doc. We can use fancier technology if this will start to get out of hand.
@AdrienChampion , can you look into creating scripts to check that benchmark is in our suggested format, and a convert into that format when it is not hard
@NikolajBjorner suggested to use z3 with python bindings for that. That would be my choice. @dddejan already tried it out (there is a link to his repo somewhere here)
@/all suggestions and volunteers are welcome ;)
https://github.com/dddejan/chctranslate
Right?
According to the readme, it seems to be more than a translation as it produces a version that's not equivalent (although equi-satisfiable). Are we fine with this?
Equi-satisfiable is ok. More important is that we can guarantee the format
In the worst case, we will include the benchmark not as it was intended. This is better than including a malformed benchmark.
Note that we will not (now) try to normalize all the benchmarks. But we will only include normalized benchmarks in the competition
In other words, benchmarks that are hard to normalize simply will not make it into the competition in this round
I modified the code from @dddejan (thanks!) so that it formats the benchmarks. I think the options I use currently produce equivalent benchmarks.
Further testing is needed, but for now I'd like to put it on a repo somewhere. Should I submit a PR to @dddejan 's repo or create one on chc-comp? Or something else?
Can someone take a look at the code checking the clauses or play with it a bit to find stupid mistakes (if any)?
I ran it on all the benchmarks from https://github.com/chc-comp/hopv and it looks fine so far. I'll run on other bench repos later.
There's one problem left though, z3 prints the tail of the clause as a let binding when it's above a certain length.
I could not find a way to tell it not to do that. @/all Anyone knows whether there's a solution? Or should I just print the clauses "manually"?
(let ((a!1 (and <tail>))) (=> a!1 <head>))I could not find a way to tell it not to do that. @/all Anyone knows whether there's a solution? Or should I just print the clauses "manually"?
printing conjuncts separately is more stable
(Sorry)
chc_tail ::=
| (and (u_predicate var+)* i_formula*)
(Also note that
(u_predicate var*) needs to be changed to (u_predicate var+) everywhere.)