Why3 as input language about dolmen HOT 4 CLOSED

Yes it'd be very interesting !
I'm not sur about what exactly you're proposing when mentioning linking with the why library, but like other languages, supporting why3 in dolmen would mean adding a (likely functorized) parser, and a structure that matches its interface (either by extending the current untyped terms, or by adding a new structure), and potentially typechecker etc... On that matter, I will very soon re-organize a bit the dolmen_std part to better namespace the various structures in it to more easily allow new classes of languages to be added (for instance why3, which likely need a few more constructions than untyped and first-order formulas).

from dolmen.

I mean linking with the Why3 OCaml library. Letting Why3 do the parsing and perhaps typing then puting it back in Dolmen functorized parser, or expression.

from dolmen.

The dependency on why3 would be a bit of a problem for a few reasons:
First, the parser part of dolmen currently has very few dependencies, and that's why it can be used in some projects without too many worries (i know for instance that @c-cube uses it (or plans to use it), and probably wouldn't if it depended on why3).
Second, it would quite wasteful to wrap why3's interface to fit into the functorized interface of dolmen. One of the reasons for the functorized interface is to try and be as efficient as possible while being adaptable into any codebase.

from dolmen.

Ok, smtlib v3 is perhaps simpler and more important

from dolmen.