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?
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?
(let ((a!1 (and <tail>))) (=> a!1 <head>))
chc_tail ::= | (and (u_predicate var+)* i_formula*)
(u_predicate var*)needs to be changed to
u_predicateshould either always or never be required to be over distinct variables. (I'm fine either way.) I think it would make the rules simpler and less confusing thanks to uniformity.
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.