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.