I actually don't want anything, neither as a participant for my tool or an organizer for the formatting script. Whatever the rules end up being my tool will support them (modulo bug) and I'll modify the script in consequence. I was trying to make the rules simpler.
chc_tail my point was simply that we can remove the first two variants and only keep the
The formatting script produces systems in a fragment a bit more restrictive than the one from the rules, I'll update the google doc shortly if you want to take a look.
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
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.