Smtlib v3

[bobot]

The proposal is becoming more tangible http://smtlib.cs.uiowa.edu/version3.shtml. I believe it could give good feedback to try to implement it in dolmen. I can give a hand, but I would certainly need your help @Gbury to know the best way to encode namespace and filters for example. Do you think it is a difficult task?

[Gbury]

Typing smtlib3 is going to be a non-trivial task indeed. I've already started to think about the changes that would be required to properly handle it. Currently the main points that will requires changes are:

• modules (this is not really that complex, rather it requires a bit of thinking about the design and import/open/lookup complexity tradeoffs in terms of performance): dolmen untyped ids already support module name/paths, but some native support will have to be added to the core typechecker to support modules import/open.
• overloading of user-defined operators: this is going to be annoying as it will most certainly require to support overloading in the core typechecker (rather than support it in the builtins as done currently), and I think it might require the typechecker to inspect (or rather unify) types in order to be able to resolve a name to the correct typed symbol, which I don't like because it basically breaks the abstraction between the typer and the expressions, :/
• qualified imports with restrictions to only some instances of polymorphic type constructors: as far as I can tell this is the real problem, and might require a lot to correctly work, depending on the exact specification of such import restrictions (e.g. what happens if functions imported by this module can produce some values of types not imported, would this have to be checked and rejected by the type-checker or would it be the user's responsibility to import a coherent subset of a module, what happens with imports from other modules which can produce values of not imported types, what happens if the same module is imported multiple times with different type instances allowed, etc...)
• upgrading the Expr module (and the core typechecker) to higher-order (this one should be fairly easy).

So quite a lot of non-trivial work. I'll try and work on that as soon as possible. Do you have any idea of the timeframe of the v3 release ?

[bobot]

At least 1 year for a final version, I believe. I think you could express your difficulty on the SMTLIB mailing list if you think that some part are too complicated or not precise enough. For example overloading can be accepted only if an as is provided (and it is now with the correct type of the function not only the result) or all the argument have a type without non-user type variable. Or overloading of polymorphic function can be completely forbidden: perhaps polymorphism or overloading not both, for defining the family of a particular function symbol!

At the end it is just a first public draft. Once available you should listen to @tinelli talk at SMTLIB: one important point is that it should not be a too big burden for solver implementor. So you can choose your own restrictions if you think they make sense and they help you to implement a possible/simpler v3, then we can propose them as amendment to the draft.

[Gbury]

I'll try and post something on the SMTLIB google group soon to raise my concerns (primarily about overloading + polymorphism as an infinite family of overloaded functions, which makes resolving a symbol non-local in my opinion).

[Gbury]

Dolmen now has support for higher-order typing, which is a first step towards supporting smtlibv3.