在定义 z3 变量和类型时使用非 ascii 字符串

如何解决在定义 z3 变量和类型时使用非 ascii 字符串

我在 z3 中定义 z3py 变量和类型，例如 X=Int('X') 或 X=EnumSort('X',['Y',...])，以防 X,Y,... 是非 ascii 字符串，就我而言，日语。

我的系统在 Python3.7.6 上是 z3py 4.8.7.0 和 MacOs 10.15.7。系统的响应是，

File "/usr/local/lib/python3.7/site-packages/z3/z3core.py",line 1588,in Z3_mk_string_symbol
    r = _elems.f(a0,_str_to_bytes(a1))
ctypes.ArgumentError: argument 2: <class 'TypeError'>: wrong type

我该如何解决这个问题？对于可变情况，我发现了一个技巧 X=Int('X'.encode())，尽管这对 EnumSort 不起作用。

解决方法

以下似乎有效，但您可能必须在终端上设置适当的编码设置才能正确打印字符。

（另外，如果这些字符有不恰当的含义，请提前道歉！不幸的是我不会说中文，我只是从网上复制了它们。）

# coding=utf-8

from z3 import *

E,_ = EnumSort('的',['是','不'])

s = Solver()
a = Const('X',E)
b = Const('Y',E)
s.add(a != b)

if s.check() == sat:
   m = s.model()
   for i in [a,b]:
     print(repr(m[i]))

,

我有类似的问题：'utf-8' codec can't decode byte 0xe9 in position 2: invalid continuation byte。

z3core.py（第 69 行）中的以下代码对我来说非常可疑：

def _str_to_bytes(s):
  if isinstance(s,str):
    try:
      return s.encode('latin-1')
    except:
      # kick the bucket down the road.  :-J
      return s
  else:
    return s

也许是python2的遗留物。如果我将 latin-1 更改为 utf-8，它似乎有效……但这与其说是一个好的解决方案，不如说是一种破解。也许我们需要提交一个补丁。我在 Z3 github 存储库上提出了 an issue。