Missing value for option --input for polymorphic SMT syntax

[claudemarche]

With the Dolmen frontend of Alt-Ergo, it is possible to give an input file in the SMT syntax. It even supports the upcoming 3.0 version of the syntax which allows one to add prenex type quantification on hypotheses. Yet, Alt-Ergo will accepts the polymorphic syntax only if the given file has the .psmt2 extension.

It should be possible though to use this frontend parser even of the input file has another extension, or if input is taken from standard input, say, by passing the option --input. Unfortunately there does not seem to have a possible value for this option corresponding to psmt2. Please add it!

[bclement-ocp]

Thanks for the report!

With the legacy frontend, Alt-Ergo only supported psmt2 (so with the legacy frontend we actually parse all smt2 files as psmt2). Hence, historically, the --input smtlib2 for Alt-Ergo actually meant "psmt2".

When writing the Dolmen frontend we interpreted --input smtlib2 as requesting "plain" smt2, not "psmt2". But given that "psmt2" is an extension of smt2, all valid smt2 files should also be valid psmt2 files. I would prefer interpreting "smtlib2" as requesting psmt2 format, like was done in the legacy frontend: I am not sure there are benefits of having a strict adherence to the standard here, and it would streamline things a bit.

@claudemarche would that solution be acceptable for you, or is having separate --input options for "polymorphic smt2" and "non-polymorphic smt2" useful?

[claudemarche]

In fact I don't understand anymore. At first, it seemed to me that Alt-Ergo was behaving differently on f.smt2 and f.psmt2 with the same contents for these files. Now I cannot see the difference anymore.
Is it the case that it may behave differently?
If it makes no difference at all, then we should just forget about all that and just get rid of this extension 'psmt2' which is meaningless to me

[bclement-ocp]

Alt-Ergo should behave identically on .smt2 and .psmt2 files that do not use polymorphism; if it doesn't, that is a bug (either on our end or in Dolmen) and we will fix it.

If the file uses polymorphism, it currently depends on the frontend:

• With the (deprecated) legacy frontend, it should behave identically
• With the Dolmen frontend, polymorphic syntax in a .smt2 file should be rejected

We can make the Dolmen frontend behave like the legacy frontend and accept polymorphic syntax in .smt2 files, effectively treating .smt2 files (and the --input smtlib2 option) as if they were .psmt2 files, which I think aligns with your last suggestion.

[claudemarche]

My mistake, I tested without passing the --frontend dolmen option. Indeed, when using polymorphism in a .smt2 (not .psmt2) then it complains I'm using the reserved keyword par where I'm not allowed to.

To my point of view, I don't see any use of Alt-Ergo rejecting the polymorphic syntax in a .smt2 file, but if you need to keep this feature then I believe you need to have two separate values for the --input option.

[claudemarche]

By the way, it is confusing to me that Alt-Ergo accepts to parse a .smt2 file without the --frontend=dolmen option. Are you really maintaining two different parsers? 8-/

[bclement-ocp]

To my point of view, I don't see any use of Alt-Ergo rejecting the polymorphic syntax in a .smt2 file, but if you need to keep this feature then I believe you need to have two separate values for the --input option.

I agree — one of those two need to happen. We will discuss internally and pick one of these for the next release.

By the way, it is confusing to me that Alt-Ergo accepts to parse a .smt2 file without the --frontend=dolmen option. Are you really maintaining two different parsers? 8-/

We are not maintaining the legacy one ;) The support for SMT-LIB input in the legacy frontend has always been experimental and was never officially supported; it will be dropped entirely when we switch to using Dolmen by default. It is provided by psmt2-frontend whose integration into Alt-Ergo suffers from design issues (it targets the wrong internal representation, essentially) that make it hard to support SMT-LIB features natively. Official support for SMT-LIB input is through the Dolmen frontend only.

[bclement-ocp]

At the dev meeting today we chose to always use psmt2 as was done in the previous frontend.