pysmt z3求解器崩溃？答案

【问题标题】：pysmt z3 solver crashing?pysmt z3求解器崩溃？
【发布时间】：2018-11-20 19:20:10
【问题描述】：

我在使用 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（失败），但我不知道出了什么问题。

【问题讨论】：

标签： python z3 smt pysmt

【解决方案1】：

请注意，为 pysmt 安装求解器的正确方法是通过 pysmt-install。这保证了求解器的版本已经过测试。

【讨论】：

【解决方案2】：

这与z3 无关；而是直接使用pysmt 本身。很可能pysmt 没有跟上z3 的变化。您应该直接在他们的网站上提交票证：https://github.com/pysmt/pysmt/issues

【讨论】：