(=> (Inv x y) (Bar x y))
(=> (and (Inv1 x y) (Inv2 x z)) (Inv3 u w))
Here is something I think I would prefer:
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)
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?