SMTLIB refuses redefinition or redeclaration

[bobot]

Cf SMTLIB v6 end of §4.1.5

Overloading accepted in theory definition but not for users.

Well-sortedness checks, required for commands that use sorts or terms, are always done
with respect to the current signature. It is an error to declare or define a symbol that is already
in the current signature. This implies in particular that, contrary to theory function symbols,
user-defined function symbols cannot be overloaded.(29)

29 The motivation for not overloading user-defined symbols is to simplify their processing by a solver. This restriction is significant only for users who want to extend the signature of the theory used by a script with a new polymorphic function symbol—i.e., one whose rank would contain parametric sorts if it was a theory symbol. For instance, users who want to declare a “reverse” function on arbitrary lists, must define a different reverse function symbol for each (concrete) list sort used in the script. This restriction might be removed in future versions

[Gbury]

I'll fix that soon (probably in or along #36 ); the support is already there I just have to pass the correct option to the typechecker env to forbid shadowing of declared identifiers.

[bobot]

Currently the theories doesn't define the symbols the define. It seems that they need to give also this information in order to support that, no?

[Gbury]

ah yes, that's slightly more complex (since some theories actually define an infinite number of symbols), but I have some plans for that, ^^

[Gbury]

So, I have mostly the patch needed for that, but one last question: are bound variables allowed to shadow identifiers previously declared (whether they previously declared identifiers, identifiers declared by a theory, or other variables in scope) ?

[Gbury]

Fixed by d078da6

[Gbury]

So, I just saw the following in the standard:

Remark 5 (No shadowing of theory symbols). One exception is that binders cannot shadow
theory function symbols, that is, function symbols from the declaration (see Section 3.7) of a
theory included in the current logic (see Section 3.8 and Subsection 4.2.1). In other words,
variables and parameters cannot have the same name as a theory function symbol in the same
scope.(14)

Which is particularly annoying when variables and parameters are allowed to shadow sort symbols coming theories....

[Gbury]

These rules and exceptions are really too convoluted sometimes :/

[bobot]

Yes, they are meant to make solver implementer life easier, but not always for all of them ;). It could be discussed fo the next version of the standard.

[Gbury]

Should be definitely fixed thanks to the n-th big refactoring done in 15985f4