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安装。这保证了解算器的版本已经过测试。你知道吗

Answer 2

这实际上与z3无关，而是直接与pysmt本身有关。很可能pysmt没有及时了解z3的变化。你应该直接在他们的网站上提交一张罚单：https://github.com/pysmt/pysmt/issues