Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Can't parse TIP v0.3 #88

Open
TpmKranz opened this issue May 6, 2022 · 4 comments
Open

Can't parse TIP v0.3 #88

TpmKranz opened this issue May 6, 2022 · 4 comments

Comments

@TpmKranz
Copy link
Contributor

TpmKranz commented May 6, 2022 •
edited
Loading

Apparently, the TIP language has incorporated SMT-LIB 2.6 changes (tip-org/tools@2995668) 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 (spechub/Hets#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
Copy link
Member

c-cube commented May 6, 2022

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
Copy link
Collaborator

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
Copy link
Contributor Author

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
Copy link
Collaborator

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
3 participants
@c-cube @TpmKranz @abentkamp