pysmt z3 решает сбой?

Question

У меня проблемы с решателями pysmt.Я получаю следующее сообщение об ошибке:

AttributeError: 'module' object has no attribute 'Z3_mk_and'

всякий раз, когда я пытаюсь выполнить оба действия: (1) Создание экземпляра решателя с помощью Solver() и (2) Выполнение pysmt-install --check

Вотполная трассировка стека, вызванная методом 1:

Traceback (most recent call last):
  File "ex.py", line 15, in <module>
    solver = s.Solver()
  File "/Users/harper/anaconda2/lib/python2.7/site-packages/pysmt/shortcuts.py", line 910, in Solver
    return get_env().factory.Solver(name=name,
  File "/Users/harper/anaconda2/lib/python2.7/site-packages/pysmt/environment.py", line 158, in factory
    self._factory = pysmt.factory.Factory(self)
  File "/Users/harper/anaconda2/lib/python2.7/site-packages/pysmt/factory.py", line 86, in __init__
    self._get_available_solvers()
  File "/Users/harper/anaconda2/lib/python2.7/site-packages/pysmt/factory.py", line 222, in _get_available_solvers
    from pysmt.solvers.z3 import Z3Solver
  File "/Users/harper/anaconda2/lib/python2.7/site-packages/pysmt/solvers/z3.py", line 295, in <module>
    class Z3Converter(Converter, DagWalker):
  File "/Users/harper/anaconda2/lib/python2.7/site-packages/pysmt/solvers/z3.py", line 859, in Z3Converter
    walk_and     = make_walk_nary(z3.Z3_mk_and)
AttributeError: 'module' object has no attribute 'Z3_mk_and'

Я так много пытался это исправить, как удаление и переустановка z3 (предположительно успешно), установка pip z3-solver (что не удалось) иЯ не могу понять, что не так.

Answer 1

Обратите внимание, что правильный способ установки решателя для pysmt - через pysmt-install.Это гарантирует, что версия решателя была протестирована.

Answer 2

Это не имеет ничего общего с z3;а точнее непосредственно с pysmt.Скорее всего, pysmt не в курсе изменений в z3.Вы должны подать заявку прямо на их сайте: https://github.com/pysmt/pysmt/issues