[SMT-LIB] Benchmark Conformance: log in AUFLIRA/nasa/

[Cesare Tinelli]

Hi Tjark, David, and all,

On 3 Nov 2010, at 06:42, Tjark Weber wrote:

> On Wed, 2010-11-03 at 07:21 +0000, cok at frontiernet.net wrote:
>> - We should however keep what can be done in a theory consistent
>> with what can be done in other commands.  The fact that overloading
>> (with different ranks) can happen in one place and not the other is
>> a nuisance in parsing and inconvenient for the user.
> 
> I agree that overloading with different ranks -- since it can happen in
> theories -- should perhaps be allowed for user-declared symbols as well.
> 
There was an extensive discussion on this issue in the past, both at SMT-LIB panels in a couple of SMT workshop and in the SMT-LOGIC workgroup that worked of the underlying logic of SMT-LIB2.

At the end, the consensus was in essence that the convenience for a SMT solver user to have overloaded user-defined symbols did not justify the burden that such a feature would impose on SMT solver developers.


> However, if overloading is allowed, the standard needs to specify the
> behavior in case the user attempts to overload a polymorphic symbol
> (such as 'store').

Yes, but it gets worse. If we allow overloading of user-defined function symbols it would make sense to allow parametric polymorphism (such as with list append, say), not just the ad-hoc variety (where a symbol can have several, but only finitely many, ranks). For that, you really need full blown support of parametric types, both at the type checking and at the inference level. Again, most solver writers involved in the discussions on the SMT-LIB2 format have been so far against that, and with reason.

So the overloading of user-defined symbols is out of the question, at least for Version 2.



>  (Probably, it should be allowed if and only if the
> new rank is not an instance of the polymorphic rank.)
> 
>> - The overloading on return type with the 'as' construct appears to
>> have limited utility and also complicates the bottom up typechecking.
> 
> My understanding is that 'as' is used if (and only if) there are symbols
> 
>  f: t_1 ... t_n t  and  f: t_1 ... t_n t'
> 
> with t <> t'.  In the absence of overloading, I am not sure how one
> would declare these -- only as theory symbols?  But assuming they exist,
> 'as' is a highly useful feature: without it, straightforward bottom-up
> type checking would no longer be possible.
> 
> The (as nil (List Int)) example (on page 24) motivates 'as' well, in my
> opinion.
> 
Glad to hear that :)  That was the goal.


Cheers,


Cesare


> Regards,
> Tjark
> 
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib