python - 在 Z3py 中使用多字节字符作为函数和排序名称

Question

对于说英语的人来说这可能是一个陌生的问题。

Python3 接受多字节字符作为变量名称。 然而，在下面的 z3py 示例中，Human -> 人间(日语)会导致错误。 我原来的Python3可以毫无问题地处理多字节字符。

from z3 import *

Object = DeclareSort('Object')

人間 = Function('人間', Object, BoolSort())
Mortal = Function('Mortal', Object, BoolSort())

# a well known philosopher 
soc= Const('socrates', Object)

# free variables used in forall must be declared Const in python
x = Const('x', Object)

axioms = [ForAll([x], Implies(人間(x), Mortal(x))), 
          人間(socrates)]

s = Solver()
s.add(axioms)

print(s.check()) # prints sat so axioms are coherent

# classical refutation
s.add(Not(Mortal(socrates)))

print(s.check()) # prints unsat so soc is Mortal

错误表示 _to_ascii() 出了问题。您知道这里发生了什么吗？请告诉我是否可以使用多字节字符并稍微重写 z3 主脚本。我在互联网上看到一些案例，z3py 与日语可以工作。所以，我认为这是可能的。

usr/lib/python3.7/site-packages/z3/z3core.py in Z3_mk_string_symbol(a0, a1, _elems)
   1526 
   1527 def Z3_mk_string_symbol(a0, a1, _elems=Elementaries(_lib.Z3_mk_string_symbol)):
-> 1528   r = _elems.f(a0, _to_ascii(a1))
   1529   _elems.Check(a0)
   1530   return r

ArgumentError: argument 2: <class 'TypeError'>: wrong type

Answer 1

我深入研究了回溯所引用的 _to_ascii() 方法，其中包含此代码(来自最新的 Z3Prover/z3 release, z3-4.8.7 ):

z3/z3core.py @ 69

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

您会注意到，在 try 中，它对 s 进行了 ascii 编码(其中 s 是您传递给 Function 构造函数的函数名称)，它与方法名称相符。显然，你的名字“人间”不能被编码为ASCII，所以这里的编码失败。最终这会冒泡，导致您看到的 ArgumentError。

查看代码，我怀疑您看到的任何表示 z3 支持日语名称的消息来源都是不正确的。您可以尝试在 z3 GitHub 上提交有关失败的错误，但由于该方法被称为 _to_ascii()，我认为它没有引起太多关注(也许是功能请求？)。

话虽如此，您可以修改此处的代码以允许您的日语函数名称:

def _to_ascii(s):
  if isinstance(s, str):
    try:
      return s.encode('utf-8') # <- Note the change in encoding here
    except:
      # kick the bucket down the road.  :-J
      return s
  else:
    return s

这样做，我能够运行您的代码(在将您的 socrates 变量重命名为 soc :) )