Can't parse TIP v0.3

[TpmKranz]

Apparently, the TIP language has incorporated SMT-LIB 2.6 changes (https://github.com/tip-org/tools/commit/2995668c6e0d3fb68ec71a494992f74f3c96b877) and is therefore no longer compatible with zipperposition's current parser:

$ zipperposition benchmarks/tip2015/list_elem_map.smt2
parse error at at file 'benchmarks/tip2015/list_elem_map.smt2': line 1, col 1 to 17:
expected statement

Since BNFC claims to be able to output Menhir files and the lbnf file is available, I suppose it would be little effort to update the parser, although I don't know anything about menhir and the way its output is used in zipperposition (otherwise I would've made a quick PR myself). Do you think this is feasible?

To give a little background: I'd like to add TIP support to Hets (https://github.com/spechub/Hets/issues/1502) to enable it to eventually talk to several induction-capable provers with relatively little translation effort of its own, using the TIP-provided tools instead. I plan on testing the implementation by connecting a prover that already talks TIP natively (e.g. zipperposition). Since the generated TIP should eventually be fed into TIP's (up-to-date) translator, I want to avoid implementing an old version of the language if possible.

[c-cube]

Depending on how complicated the changes are, you might have an easier time just adapting the current parser to follow TIP 3. It's nice that they got closer to smtlib, I must say.

I don't have any time to work on this personally, though.

[abentkamp]

I've adapted the grammar and pushed it directly to master. I've tried a couple of problems from the TIP library and they can be parsed now. Let me know if you find any issues that I've missed.

The example list_elem_map.smt2 you mention above still throws an error, but at least it can be parsed now.

[TpmKranz]

Thank you very much for the swift responses and the quick implementation!

Regarding issues, the following archive contains all the files from tip-benchmarks-0.3 that still throw parse errors, accompanied by zipperposition's respective outputs describing the error: parse_errors.tar.gz In every single case, zipperposition's parser apparently expected term, while tip has no problems reading (and translating) them.

Furthermore, here is an archive of all the files that throw the same error you noticed with list_elem_map.smt2, again accompanied by the output: ApplyError.tar.gz Interestingly, tip has problems converting most of these to Isabelle format, except for list_elem_map.smt2 (and list_nat_elem_map.smt2).

Once again, thank you for your help!

[abentkamp]

I've fixed the parsing issue and pushed it to master.

The ApplyError is more difficult to fix. The issue is a clash of variable names in the induction module and I am not sure how the induction module works at all. It seems that all the variables of a form in Test_prop.ml are supposed to live in the same namespace. But then, via Libzipperposition.Cut_form.normalize_form, RW.Lit.normalize_clause is called, and it may rename variables in a single clause of a form, which can then cause variable name clashes.

A workaround would be to replace let cs = c |> rw_terms |> rw_clause |> rm_trivial in by let cs = c |> rw_terms |> (fun c -> [c]) |> rm_trivial in in Cut_form.ml. This prevents the error, but probably takes out some important functionality from the induction module.