Quoted identifiers can be keywords

[bclement-ocp]

According to my reading of 3.2

[Gbury]

I think that's correct, i'll fix that.

[bclement-ocp]

That being said, after a bit more thinking, this is really weird, and maybe should not be done. Using reserved words as identifiers, even quoted, just seems prone to confusion, and doesn't seem to be supported in a consistent way by existing solvers.

For instance, Z3 supports (declare-const |forall| Int) but CVC5 doesn't; on the other hand CVC5 supports (declare-const |_| Int) while Z3 doesn't, and both support (declare-const |!| Int). All of these are part of the set of reserved words.

It is probably fine to take the lax interpretation of "Following Common Lisp’s conventions, enclosing a simple symbol in vertical bars does not produce a new symbol." as implying that assert and |assert| are the same "pseudo-symbol" and hence neither is valid as a symbol.

[Gbury]

It's not easy to determine indeed, but first let me state that for most things related to the spec, the behaviour of solvers is not really a good indication (sadly enough). Basically, the problem boils down to the following two choices:

• quoted symbols allow to quote reserved words and turn them into symbols, allowing for instance the following statement

  (declare-fun |assert| () Bool)

• on the other hand, if the quoting mechanism is completely transparent, and quoted reserved words behave as reserved words, then the following statement should be legal:

  (|assert| false)

So basically, this is the choice we have: exactly one of the two statements above should be legal (and the other not). I would say that for now my reading of the specification would make me go towards the first solution (i.e. quoting allows to use usually reserved names as symbol names), but I agree it's not really clear.

[bclement-ocp]

I think there is a third reading, which is the one I was going for: quoted reserved words behave as reserved words in contexts where a quoted symbol is allowed by the grammar.

• (declare-fun |assert| () Bool) is rejected, because (declare-fun <symbol> () Bool) is allowed and the symbol is assert, which is a reserved word;
• (|assert| false) is accepted, because the syntax is (assert <term>), not (<symbol> <term>)

[bclement-ocp]

In fact there is a weird discrepancy in the way that the standard excludes reserved words versus symbols starting with @ or . from being used. From a strict reading of the spec:

• Reserved words are not simple symbols;
• Simple symbols starting with @ or . are "reserved for solver use";
• "Enclosing a simple symbol in vertical bars does not produce a new symbol" (emphasis mine)

So |assert| is OK, even though assert is a reserved word, because assert is not a simple symbol, |assert| is not "enclosing a simple symbol in vertical bars"; but |@assert| is reserved, because @assert is a simple symbol, and so |@assert| and @assert are the same symbol.

On the other hand, |@é| is technically allowed, since it is not a "simple symbol starting with @ or ." (and yet I believe it is rejected after #185 ).

[Gbury]

Your understanding is probably the one that matches the (quite fuzzy) specification of the smtlib spec. That being said, I'd argue for a slightly different semantics for a few reasons.

So first, my proposition:

• in my proposed semantics: |assert| would act as a symbol (and not a reserved word), so you can define/declare/let-bind it
• any symbol (whether it be quoted or simple in the source) would be reserved if it starts with an @ or a .

Now for a few reasons:

• first: simplicity. At least for the aspects of the spec that are not specific enough, I'd argue that the simpler and most intuitive/coherent behaviour should be used
• second: usability/intent. At least in my opinion quoting is there to.. well quote things, so my interpretation of quoted symbols is to allow users to quote symbols that otherwise may not be accepted as simple symbols. Reasons for not being accepted as simple symbols are mainly tied to the syntax, so these reasons can be for instance whitespace-related (as the examples in the spec show), but it can also be that the symbol that one wanted to use is a reserved word. In that case, it makes sens to me to allow users to not have to rename their symbols, and therefore to allow quoted reserved word as symbols.
• lastly, about |@é| and the like, here I'd argue for simplicity and predictability of the syntax, as well as separation of the syntax and typing/name resolving parts of the language: quoting is a syntax mechanism to overcome some difficulty related to the syntax of symbols/identifiers, as well as the usefullness of reserved word for parsing (which would make it extremely annoying/complex to try and support assert as both a reserved word or a symbol depending on its position in the source). On the other hand symbols reserved for solver use is a typing/name resolution thing: the restriction is not enforced during parsing, and the rules that drives it are more closely related to name resolution, and name shadowing than, the syntax.

That way quoting is only relevant in the parser, and the information of what was quoted disappears afterwards, and not used during typing, because it makes more sense for quoting to be a syntax solution to a syntax problem, and typing can then simply not care about the syntax.

[bclement-ocp]

Yeah, I also think that this is the most reasonable implementation.

That said, if quoted keywords are allowed, it would be really useful for Dolmen to provide quoting printers so that users don't have to manage the list of keywords on their own when printing models.

[Gbury]

Yup, such functions will be part of the printing functionality of Dolmen (which I should really get to soon..).

[bclement-ocp]

My point is that even without the full printing functionality having only these functions would be very helpful, and probably easier to implement than the full printing functionality (but maybe not that much?).

[Gbury]

Well, it's more that these functions solve one very particular problem, which is to ensure that what you print is likely to be parseable, however, it doesn't ensure that what is parsed is what you want (e.g. that you didn't accidentally shadow some variables or definitions).

[bclement-ocp]

True, but for my specific use case (which is model printing in Alt-Ergo), having just those functions should be enough :)

[Gbury]

Hm.. right, I'll add those functions as soon as I have the time.