ok
do you want to further restrict that a variable can appear in at most one predicate in any clause
That is, rule out
(=> (Inv x y) (Bar x y))
and
(=> (and (Inv1 x y) (Inv2 x z)) (Inv3 u w))
Here is something I think I would prefer:
- heads over distinct variables only
- only one interpreted formula
This would simplify inlining and identification of variables somewhat (in my head).
benchmark ::=
| (assert chc_assert)* (assert chc_query)
chc_assert ::=
| (forall (vars) (=> chc_tail[vars] chc_head[vars])
chc_query ::=
| (forall (vars) (=> chc_tail[vars] i_formula[vars])
chc_head[vars] :=
| uninterpreted predicate over distinct vars as arguments (e.g., vars = [x, x'] and (inv x'), (inv x x) not allowed)
chc_tail[vars] ::=
| u_predicate[vars] | i_formula[vars]
| (and u_predicate[vars]+ i_formula[vars]?)
u_predicate[vars] ::=
| uninterpreted predicate over vars (e.g., vars = [x, x'] and (inv (+ x 1))
i_formula[vars] ::=
| formula with only interpreted functions/predicates (e.g., vars = [x, x'] and x' = x + 1)
I'm ok with it overall. See a few questions in the doc.
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)
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?