Z3 для pysmt не работает в MacOS с ошибкой «libz3.dylib не найден»

Question

Я пытался использовать z3 в pysmt и установил z3 как через доморощенный, так и черезpysmt-install --z3команда. Однако, когда я пытаюсь проверить статус решателей черезpysmt-install --check, он возвращает следующее сообщение

      Could not find libz3.dylib; consider adding the directory containing it to
  - your system's PATH environment variable,
  - the Z3_LIBRARY_PATH environment variable, or 
  - to the custom Z3_LIBRARY_DIRS Python-builtin before importing the z3 module, e.g. via
    import builtins
    builtins.Z3_LIB_DIRS = [ '/path/to/libz3.dylib' ] 
Traceback (most recent call last):
  File "/Library/Frameworks/Python.framework/Versions/3.12/bin/pysmt-install", line 5, in <module>
    from pysmt.cmd.install import main
  File "/Library/Frameworks/Python.framework/Versions/3.12/lib/python3.12/site-packages/pysmt/cmd/install.py", line 27, in <module>
    from pysmt.environment import get_env
  File "/Library/Frameworks/Python.framework/Versions/3.12/lib/python3.12/site-packages/pysmt/environment.py", line 24, in <module>
    import pysmt.simplifier
  File "/Library/Frameworks/Python.framework/Versions/3.12/lib/python3.12/site-packages/pysmt/simplifier.py", line 26, in <module>
    from pysmt.fnode import FNode
  File "/Library/Frameworks/Python.framework/Versions/3.12/lib/python3.12/site-packages/pysmt/fnode.py", line 57, in <module>
    from pysmt.constants import (Fraction, is_python_integer,
  File "/Library/Frameworks/Python.framework/Versions/3.12/lib/python3.12/site-packages/pysmt/constants.py", line 174, in <module>
    import z3.z3num
  File "/Users/local_user/Library/Python/3.12/lib/python/site-packages/z3/__init__.py", line 1, in <module>
    from .z3 import *
  File "/Users/local_user/Library/Python/3.12/lib/python/site-packages/z3/z3.py", line 43, in <module>
    from . import z3core
  File "/Users/local_user/Library/Python/3.12/lib/python/site-packages/z3/z3core.py", line 67, in <module>
    raise Z3Exception("libz3.%s not found." % _ext)
z3.z3types.Z3Exception: libz3.dylib not found.

Я последовал комментариям в сообщении об ошибке и добавил путь к libz3.dylib в PATH, но это не помогло. Я также пытался установить z3 через доморощенный, но pysmt не может найти правильный путь к z3 и вернуть сообщение об ошибке.

      ModuleNotFoundError: No module named 'pysmt.solvers.z3'

Как мне установить z3 в pysmt?

Answer 1

Попробуйте установить:

      DYLD_LIBRARY_PATH=$DYLD_LIBRARY_PATH:/Applications/z3/bin
PYTHONPATH=/Applications/z3/bin/python

используя правильные пути для вашей системы.