[SMT-LIB] Fwd: New draft of Version 2.5 of SMT-LIB released

[Jochen Hoenicke]

Hello all,

although it's good to have extended characters in SMT-LIB restricting these
explicitly to ISO-8859-1 is bad (it does not even allow for using greek
letters in your formula :).  Why don't we allow any extended character from
128 and beyond and treat it as opaque?  I think most common encodings based
on 8-bit characters use only 128..255 for encoding extended characters.
You could say that this is just an "encoding" and the input sequence is
really the decoded character sequence, but then you should allow codepoints
beyond 255.  In this way you can see UTF-16 as using characters from
128..65535(..0x110000?) as extended characters.

I don't want a big change, just define printable characters to include all
characters starting from 128 and reword the section 3.1 such that it is not
specific to a single encoding.  There could be a footnote that these
characters are not interpreted by the solver in any way, e.g.
|U+006EU+0303| (n◌̃) is different from |U+00F1| (ñ).

So I would suggest the following rewording of second and third paragaraph
in 3.1:

SMT-LIB source files consist of Extended ASCII characters, specifically it
allows 8-bit extensions like ISO 8859-1 and UTF-8 of the original 7-bit
US-ASCII set.(3)

Most lexical tokens defined below are limited to US-ASCII printable
characters, namely, characters 32dec to 126dec. The remaining printable
characters, characters 128dec and beyond, mostly used for non-English
alphabet letters, are allowed in string literals, quoted symbols,
and comments.



Also you should replace all occurrences of "160 to 255" with "128 and
beyond"

I'm not sure if it is a good idea to have 160 as white-space character.
Note that in UTF-8 it is encoded as two bytes (although the decoded code
point is also 160).  If we start allowing this, then the next person wants
to add en-space, em-space or ideographic cjk whitespace.

Regards,
  Jochen