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