The tool works on virtually all the benchmarks on the chc-comp organization.
Please take a look at
test/check_err/*.smt2 (and scripts/check.sh), if you come up with illegal benchmarks that these test files do not cover let me know or submit a PR :D
(Illegal in the sense that z3 fails to parse them.)
it should include everything from our discussions
a script to translate arbitrary files to this format is: https://github.com/chc-comp/scripts
it should not be too difficult to extend the script to convert to prolog-like format. I believe @jpgallagher has a z3-based converter from SMT-LIB constraints to prolog
if you have benchmarks (in any format) please let me know so that I can include them. The best way is either a link to an archive or a github repo
Fantastic! Given that this is our first time organizing the competition, there are no strict deadlines. We are waiting for comments until April 2nd. Throughout April, I'll start going over the rules again and getting people to try their tools and benchmarks on StarExec. Provided that everything works smoothly, we can wait until the last minute to finalize competition benchmarks and run the tools.
Of course, earlier is better, especially if your benchmarks are in your format and will require conversion to smt-lib
Please let me know if there are any issues for you with our current format. We have tried to make it as simple and as inclusive as possible. But since all of our tools are smt-lib based, we are not sure what complications others might encounter.
Now looking at let-binders. Reading the gdrive doc it seems that all participants use them... are there any further specs about their format and occurrence?
According to the current grammar they can be used in i_formulas only, right? do let-binders occur at top-level only? can they be nested ?
According to the current grammar they can be used in i_formulas only, right? do let-binders occur at top-level only? can they be nested ?
the syntax and semantics follows the one in SMT-LIB, p27 in http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf
let binders are very commonly nested when they occur
Hi Philipp. Thanks for your answer.
Can we make some assumptions on the variables occurring in let-binders?
For example, given the term (let ((x1 t1)...(xn tn)) t )
the SMT-LIB standard requires that x1...xn are distinct variables but does not say anything about their occurrence in t1...tn.
Thus a term (let ((x y) (y x)) (> x y)) is legal and equivalent to (> y x).
Can we assume that variables x1...xn do not occur in t1...tn?
This would simplify the management of let-binders
and allow us to manage the parallel bindings in a sequential manner.
I suppose one could add the simplification in the format that identifiers are not reused (the variables bound by let all have distinct and unique names)
in the more general form let-binders require a more sophisticated treatment (f.e. for assigning distinct names to the two distinct variables with the same name)
The only complication is the scope introduced by multiple let binders, but that simply means you keep a stack of {xi->ti} maps
You have two choices: (a) replace let binders by new existentially quantified variables. That is, rewrite each
let as an equality. and (b) write a parser that keeps track of current binding while building the expressions
(b) seems easier and more robust in presence of nested let binders
if you want to flatten the formula to remove let binders you can probably use one of many smt-lib parsers to do that.
but, again, this would explode the size of the formula dramatically
SMT-LIB does not support lists directly, this is an extension of Z3, and I think we should not have lists as a pre-defined theory. Where relevant, we can define lists as an ADT.