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

[Tjark Weber]

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.

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').  (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.

Regards,
Tjark