时间戳

首页 > 解决方案 > pysmt z3求解器崩溃？

python - pysmt z3求解器崩溃？

问题描述

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

标签： pythonz3smtpysmt

解决方案

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

推荐阅读