search

nunchaku-inria / nunchaku

Model finder for higher-order logic
https://nunchaku-inria.github.io/nunchaku/
BSD 2-Clause "Simplified" License
42 stars 3 forks source link

Parse error on TIP input #35

Open mikkelmilo opened 5 years ago

mikkelmilo commented 5 years ago

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 commented 5 years ago

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

mikkelmilo commented 5 years ago

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

c-cube commented 5 years ago

Yes, and an issue with TIP changing its format without proper versioning :man_shrugging:

mikkelmilo commented 5 years ago

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 commented 5 years ago

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 commented 5 years ago

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.