Parse error on TIP input

[mikkelmilo]

Whenever I try to use a TIP file as input i get a parse error. For example, if I run nunchaku --input tip cfg5_unambig.smt2 on this file from the TIP-benchmarks repository, I get the error:

could not parse cfg5_unambig.smt2: parsing error: expected statement at file 'cfg5_unambig.smt2': line 1, col 1 to 17

This seems to happen for any TIP I give as input.

[c-cube]

The TIP format seems to have changed (probably to become closer to SMTLIB 2.6).

[mikkelmilo]

So this is really an issue in the tip-parser ocaml library?

[c-cube]

Yes, and an issue with TIP changing its format without proper versioning 🤷‍♂️

[mikkelmilo]

Indeed, the format has changed. I found a (seemingly) up-to-date definition of the BNF. Is this something you think is easily fixable in tip-parser? I would like to help, but unfortunately I am not very proficient in OCaml nor the parser generator tool tip-parser uses.

[c-cube]

It could be reasonable easy to fix if it's changes in the datatypes syntax. the parser generator, menhir, is awesome (and hopefully the file is reasonably readable; you can ask questions if you need, here or on IRC on freenode, I'm companion_cube). There is this tip_cat executable in the repo that can be used to parse and print files, when it passes on the whole new set of benchmarks you'll know it works :)

That being said, I wish the tip org would version their syntax (with a statement at the beginning maybe)…

[mikkelmilo]

Unfortunately, it doesn't seem to be only the syntax. They have added new statement constructs 'lemma' and 'prove', which means the converter to the internal representation in nunchaku also needs to be updated. Also, I'm not sure but I think the semantics of polymorphic function/types may also have changed... This is not something I can fix...

Edit: Oh yeah, and they added attributes syntax, but the parser could just discard these attributes since they have no semantics - I suppose they are purely for propagating useful information when doing many translations between formats.