parse_logic does not recognize QF_FPBV

[christophejunke]

Some benchmarks and solvers apparently support the syntax QF_FPBV (in that order) for QF_BVFP. For example, the following repository has a lot of examples of this: https://github.com/florianschanda/smtlib_schanda

The code in typecheck/logic.ml seems to require BV to appear first: https://github.com/Gbury/dolmen/blob/ec32e34a95d21f71b985dc747507ff9db0db32da/src/typecheck/logic.ml#L145

I couldn't find an explicit rule about how logics should be named, but I guess that since this variation occurs in the wild, it might be preferable to support it if possible.

[Gbury]

That's a good question, I think i'll try and raise it on the SMT-LIB2 spec repo to see what the SMT-LIB maintainers think about that.

That being said, once I finish the work on "printers" (or rather the ability to export problems to the SMT-LIB format), I expect that the "good" solution will be to just ask dolmen to reformat the problem so that it becomes correct.

[Gbury]

After a bit of discussion with other people in the SMT community, it seems that having a canonical unique name for each logic is a desirable property. Therefore, for now I'd propose to keep the order imposed by dolmen (note that solvers are always allowed to support more than the standard/spec, and very often do so), and if/when the SMT-LIB maintainers come to a decision about https://github.com/SMT-LIB/SMT-LIB-2/issues/39 we can revisit the issue ?

That being said, this might be annoying/problematic for users of the dolmen API (i.e. colibri2 and alt-ergo)... I'll try and add a fallback option for when logic detection fails, so that users can default to the ALL logic if needed.

[Gbury]

So actually, this is already done, you just need to make the warning non-fatal and typing will go on and use the ALL logic, which can be done by modifying the Dolmen_loop.Report.Conf.t value that is given to the State.init function in the following way:

(* creation of the `reports` value *)
let reports = Dolmen_loop.Report.mk ~default:Enabled in
...
(* make the unknown logic non fatal *)
let reports = Dolmen_loop.Report.Conf.set_enabled reports Dolmen_loop.Typer.unknown_logic in
...

Dolmen_loop.State.init ... ~reports

I'll therefore close this issue, but feel free to re-open if you still experience problems with this, ^^

[christophejunke]

Thank you