Использование многобайтового символа для функции и имени сортировки в Z3py - PullRequest
Новая
       6

Использование многобайтового символа для функции и имени сортировки в Z3py

1 голос
/ 28 февраля 2020

Это может быть незнакомый вопрос для говорящего на английском языке sh.

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 или нет. В Inte rnet я видел несколько случаев, когда 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

1 Ответ

0 голосов
/ 28 февраля 2020

Я копался в методе _to_ascii(), на который ссылается ваша трассировка, который содержит этот код (из последней версии Z3Prover / z3, 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 вы заметите, что он выполняет кодировку ascii для s (где 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 :))

...