\xHH 字符表示在 z3 4.8.11 之后是否已过时？

Question

我在 z3@4.8.10 和 z3@4.8.11 中分别找到了以下代码结果 sat 和 unsat。

(assert (= (str.len "\x4a") 1))
(check-sat)

我认为这是因为 4.8.11 中对 unicode 默认支持的更改。

现在的问题是：

是否有一个开关可以恢复以前的行为？
（如果不是）“\u{HH}”是非 ascii 字符的正确表示吗？

编辑：我注意到也不能使用通常的转义序列（如“\n”）。会比较不方便...

Answer 1

没错。 Z3 现在支持新的 SMTLib 字符串理论，记录在这里：

http://smtlib.cs.uiowa.edu/theories-UnicodeStrings.shtml

据我所知，没有“切换到以前的行为”开关。

您关于转义序列的具体问题已在上述文档中得到解答。作为参考，下面是它的内容：

The restriction to printable US ASCII characters in string constants is for simplicity since that set is universally supported. Arbitrary Unicode characters can be represented with escape sequences which can have one of the following forms
  \ud₃d₂d₁d₀  
  \u{d₀} 
  \u{d₁d₀}
  \u{d₂d₁d₀}
  \u{d₃d₂d₁d₀}
  \u{d₄d₃d₂d₁d₀}   
where each dᵢ is a hexadecimal digit and d₄ is restricted to the range 0-2.

These are the only escape sequences in this theory. See later. In a later version, the restrictions above on the digits may be extended to allow characters from all 17 Unicode planes. Observe that the first form, \ud₃d₂d₁d₀, has exactly 4 hexadecimal digit, following the common use of this form in some programming languages. Unicode characters outside the range covered by \ud₃d₂d₁d₀ can be represented with the long form \u{d₄d₃d₂d₁d₀}.

Also observe that programming language-specific escape sequences, such as \n, \b, \r and so on, are not escape sequences in this theory as they are not fully standard across languages.

正如它在最后一段中明确指出的那样，\n、\r 等序列无效并且不会被解释为转义序列。相反，您应该使用 \u{a} 表示 \n，等等，因为 \n 的 ASCII 码是 10。

\xHH 字符表示在 z3 4.8.11 之后是否已过时？

Is \xHH character representation obsoleted after z3 4.8.11?

z3