<p>我在pysmt解算器上遇到了麻烦。我收到以下错误消息:</p>
<pre><code>AttributeError: 'module' object has no attribute 'Z3_mk_and'
</code></pre>
<p>无论何时我尝试两者:
(1) 通过<code>Solver()</code>和
(2) 运行<code>pysmt-install --check</code></p>
<p>下面是从方法1得到的完整堆栈跟踪:</p>
<pre><code>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'
</code></pre>
<p>为了解决这个问题,我做了很多尝试,比如卸载并重新安装z3(据说是成功的),pip安装z3 solver(失败的),我不知道出了什么问题。你知道吗</p>