SMTLIB refuses redefinition or redeclaration about dolmen HOT 9 CLOSED

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

from dolmen.

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.

from dolmen.

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?

from dolmen.

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) ?

from dolmen.

Fixed by d078da6

from dolmen.

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....

from dolmen.

These rules and exceptions are really too convoluted sometimes :/

from dolmen.

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.

from dolmen.

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

from dolmen.