我已通过运行以下命令在我的计算机（带有 m1 芯片的 Mac）上安装了 Z3：
brew install z3
我正在尝试为 Haskell 安装 z3 绑定。
图书馆网站上写着：
Installation:
1) Install a Z3 4.x release. (Support for Z3 3.x is provided by the 0.3.2 version of these bindings.)
2) Just type cabal install z3 if you used the standard locations for dynamic libraries (/usr/lib) and header files (/usr/include).
Otherwise use the --extra-lib-dirs and --extra-include-dirs Cabal flags when installing.
所以我已经完成了步骤 1，在步骤 2 中，我输入 cabal install z3 ，但出现错误。我在终端中运行“find /opt/homebrew -name "z3.h" 2>/dev/null”并得到以下内容
/opt/homebrew/include/z3.h
/opt/homebrew/Cellar/z3/4.12.2/include/z3.h
说实话，我不知道为什么我有两个标头，同样我也得到了库的路径
/opt/homebrew/lib/libz3.4.12.dylib
/opt/homebrew/lib/libz3.4.12.2.0.dylib
/opt/homebrew/lib/libz3.dylib
/opt/homebrew/Cellar/z3/4.12.2/lib/libz3.4.12.dylib
/opt/homebrew/Cellar/z3/4.12.2/lib/libz3.4.12.2.0.dylib
/opt/homebrew/Cellar/z3/4.12.2/lib/libz3.dylib
所以当我尝试以下任一操作时
stack install z3 --extra-lib-dirs=/opt/homebrew/lib --extra-include-dirs=/opt/homebrew/include
OR
stack install z3 --extra-lib-dirs=/opt/homebrew/Cellar/z3/4.12.2/lib --extra-include-dirs=/opt/homebrew/Cellar/z3/4.12.2/include
我收到错误：
z3> configure
z3> Configuring z3-408.2...
z3> build
z3> Preprocessing library for z3-408.2..
z3> compiling .stack-work/dist/aarch64-osx/Cabal-3.8.1.0/build/Z3/Base/C_hsc_make.c failed (exit code 1)
z3> rsp file was: ".stack-work/dist/aarch64-osx/Cabal-3.8.1.0/build/Z3/Base/hsc2hscall47771-0.rsp"
z3> command was: /usr/bin/gcc -c .stack-work/dist/aarch64-osx/Cabal-3.8.1.0/build/Z3/Base/C_hsc_make.c -o .stack-work/dist/aarch64-osx/Cabal-3.8.1.0/build/Z3/Base/C_hsc_make.o --target=arm64-apple-darwin --target=arm64-apple-darwin -Wl,-no_fixup_chains -D__GLASGOW_HASKELL__=904 -Ddarwin_BUILD_OS=1 -Daarch64_BUILD_ARCH=1 -Ddarwin_HOST_OS=1 -Daarch64_HOST_ARCH=1 -I/opt/homebrew/include -I/opt/homebrew/include -I.stack-work/dist/aarch64-osx/Cabal-3.8.1.0/build/autogen -I.stack-work/dist/aarch64-osx/Cabal-3.8.1.0/build/global-autogen -include .stack-work/dist/aarch64-osx/Cabal-3.8.1.0/build/autogen/cabal_macros.h -I/Users/mehradhq/.ghcup/ghc/9.4.7/lib/ghc-9.4.7/lib/../lib/aarch64-osx-ghc-9.4.7/base-4.17.2.0/include -I/Users/mehradhq/.ghcup/ghc/9.4.7/lib/ghc-9.4.7/lib/../lib/aarch64-osx-ghc-9.4.7/ghc-bignum-1.3/include -I/Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/ffi -I/Users/mehradhq/.ghcup/ghc/9.4.7/lib/ghc-9.4.7/lib/../lib/aarch64-osx-ghc-9.4.7/rts-1.0.2/include -I/Users/mehradhq/.ghcup/ghc/9.4.7/include/
z3> error: clang: warning: -Wl,-no_fixup_chains: 'linker' input unused [-Wunused-command-line-argument]
z3> /private/var/folders/jr/fkn85rwj2l78jxbdpgdz7j840000gn/T/stack-cb61378bcfe38b26/z3-408.2/C.hsc:97:16: error: use of undeclared identifier 'Z3_TRUE'; did you mean 'Z3_L_TRUE'?
z3> hsc_const (Z3_TRUE);
z3> ^~~~~~~
z3> Z3_L_TRUE
z3> /Users/mehradhq/.ghcup/ghc/9.4.7/lib/ghc-9.4.7/lib/template-hsc.h:45:10: note: expanded from macro 'hsc_const'
z3> if ((x) < 0) \
z3> ^
z3> /opt/homebrew/Cellar/z3/4.12.2/include/z3_api.h:94:5: note: 'Z3_L_TRUE' declared here
z3> Z3_L_TRUE
z3> ^
z3> /private/var/folders/jr/fkn85rwj2l78jxbdpgdz7j840000gn/T/stack-cb61378bcfe38b26/z3-408.2/C.hsc:97:16: error: use of undeclared identifier 'Z3_TRUE'; did you mean 'Z3_L_TRUE'?
z3> hsc_const (Z3_TRUE);
z3> ^~~~~~~
z3> Z3_L_TRUE
z3> /Users/mehradhq/.ghcup/ghc/9.4.7/lib/ghc-9.4.7/lib/template-hsc.h:46:41: note: expanded from macro 'hsc_const'
z3> hsc_printf ("%lld", (long long)(x)); \
z3> ^
z3> /opt/homebrew/Cellar/z3/4.12.2/include/z3_api.h:94:5: note: 'Z3_L_TRUE' declared here
z3> Z3_L_TRUE
z3> ^
z3> /private/var/folders/jr/fkn85rwj2l78jxbdpgdz7j840000gn/T/stack-cb61378bcfe38b26/z3-408.2/C.hsc:97:16: error: use of undeclared identifier 'Z3_TRUE'; did you mean 'Z3_L_TRUE'?
z3> hsc_const (Z3_TRUE);
z3> ^~~~~~~
z3> Z3_L_TRUE
z3> /Users/mehradhq/.ghcup/ghc/9.4.7/lib/ghc-9.4.7/lib/template-hsc.h:48:50: note: expanded from macro 'hsc_const'
z3> hsc_printf ("%llu", (unsigned long long)(x));
z3> ^
z3> /opt/homebrew/Cellar/z3/4.12.2/include/z3_api.h:94:5: note: 'Z3_L_TRUE' declared here
z3> Z3_L_TRUE
z3> ^
z3> /private/var/folders/jr/fkn85rwj2l78jxbdpgdz7j840000gn/T/stack-cb61378bcfe38b26/z3-408.2/C.hsc:99:16: error: use of undeclared identifier 'Z3_FALSE'; did you mean 'Z3_L_FALSE'?
z3> hsc_const (Z3_FALSE);
z3> ^~~~~~~~
z3> Z3_L_FALSE
z3> /Users/mehradhq/.ghcup/ghc/9.4.7/lib/ghc-9.4.7/lib/template-hsc.h:45:10: note: expanded from macro 'hsc_const'
z3> if ((x) < 0) \
z3> ^
z3> /opt/homebrew/Cellar/z3/4.12.2/include/z3_api.h:92:5: note: 'Z3_L_FALSE' declared here
z3> Z3_L_FALSE = -1,
z3> ^
z3> /private/var/folders/jr/fkn85rwj2l78jxbdpgdz7j840000gn/T/stack-cb61378bcfe38b26/z3-408.2/C.hsc:99:16: error: use of undeclared identifier 'Z3_FALSE'; did you mean 'Z3_L_FALSE'?
z3> hsc_const (Z3_FALSE);
z3> ^~~~~~~~
z3> Z3_L_FALSE
z3> /Users/mehradhq/.ghcup/ghc/9.4.7/lib/ghc-9.4.7/lib/template-hsc.h:46:41: note: expanded from macro 'hsc_const'
z3> hsc_printf ("%lld", (long long)(x)); \
z3> ^
z3> /opt/homebrew/Cellar/z3/4.12.2/include/z3_api.h:92:5: note: 'Z3_L_FALSE' declared here
z3> Z3_L_FALSE = -1,
z3> ^
z3> /private/var/folders/jr/fkn85rwj2l78jxbdpgdz7j840000gn/T/stack-cb61378bcfe38b26/z3-408.2/C.hsc:99:16: error: use of undeclared identifier 'Z3_FALSE'; did you mean 'Z3_L_FALSE'?
z3> hsc_const (Z3_FALSE);
z3> ^~~~~~~~
z3> Z3_L_FALSE
z3> /Users/mehradhq/.ghcup/ghc/9.4.7/lib/ghc-9.4.7/lib/template-hsc.h:48:50: note: expanded from macro 'hsc_const'
z3> hsc_printf ("%llu", (unsigned long long)(x));
z3> ^
z3> /opt/homebrew/Cellar/z3/4.12.2/include/z3_api.h:92:5: note: 'Z3_L_FALSE' declared here
z3> Z3_L_FALSE = -1,
z3> ^
z3> 6 errors generated.
z3>
Error: [S-7282]
Stack failed to execute the build plan.
While executing the build plan, Stack encountered the error:
[S-7011]
While building package z3-408.2 (scroll up to its section to see the
error) using:
/Users/mehradhq/.stack/setup-exe-cache/aarch64-osx/Cabal-simple_6HauvNHV_3.8.1.0_ghc-9.4.7 --verbose=1 --builddir=.stack-work/dist/aarch64-osx/Cabal-3.8.1.0 build --ghc-options " -fdiagnostics-color=always"
Process exited with code: ExitFailure 1
我不知道这在说什么。我还用 cabal 运行它只是为了看看它是否有效，但再次出现以下错误：
Warning: Unknown/unsupported 'ghc' version detected (Cabal 3.6.2.0 supports
'ghc' version < 9.4): /Users/mehradhq/.ghcup/bin/ghc is version 9.4.7
Warning: Unknown/unsupported 'ghc' version detected (Cabal 3.6.2.0 supports
'ghc' version < 9.4): /Users/mehradhq/.ghcup/bin/ghc is version 9.4.7
Resolving dependencies...
Build profile: -w ghc-9.4.7 -O1
In order, the following will be built (use -v for more details):
- hsc2hs-0.68.10 (exe:hsc2hs) (requires download & build)
- z3-408.2 (lib) (requires download & build)
Downloading hsc2hs-0.68.10
Downloaded hsc2hs-0.68.10
Downloading z3-408.2
Starting hsc2hs-0.68.10 (exe:hsc2hs)
Downloaded z3-408.2
Building hsc2hs-0.68.10 (exe:hsc2hs)
Installing hsc2hs-0.68.10 (exe:hsc2hs)
Completed hsc2hs-0.68.10 (exe:hsc2hs)
Starting z3-408.2 (lib)
Failed to build z3-408.2. The failure occurred during the configure step.
Build log ( /Users/mehradhq/.cabal/logs/ghc-9.4.7/z3-408.2-f9eabcb0.log ):
Configuring library for z3-408.2..
cabal-3.6.2.0: Missing dependency on a foreign library:
* Missing (or bad) header file: z3.h
* Missing (or bad) C library: z3
This problem can usually be solved by installing the system package that
provides this library (you may need the "-dev" version). If the library is
already installed but in a non-standard location then you can use the flags
--extra-include-dirs= and --extra-lib-dirs= to specify where it is.If the
library file does exist, it may contain errors that are caught by the C
compiler at the preprocessing stage. In this case you can re-run configure
with the verbosity flag -v3 to see the error messages.
If the header file does exist, it may contain errors that are caught by the C
compiler at the preprocessing stage. In this case you can re-run configure
with the verbosity flag -v3 to see the error messages.
cabal: Failed to build z3-408.2. See the build log above for details.
错误消息更清晰，但我已经安装了所有内容并定义了路径。我还查看了 Z3 (Haskell) 中的分段错误问题。我尝试了回复中提出的两种方法，但都不起作用。我也在跑步：
The Glorious Glasgow Haskell Compilation System, version 9.4.7
The GHCup Haskell installer, version 0.1.19.4
stack Version 2.11.1
cabal-install version 3.6.2.0
有人可以解释一下问题是什么以及如何解决吗？预先感谢您。
只是为了其他人尝试在 Mac（使用 Arm 处理器）上使用 Haskell 运行 Z3 绑定并得到相同的错误，我将在这里发布对我有用的解决方案。所以基本上，通过执行以下命令来安装 Z3
brew install Z3
在终端中将为您安装 Z3 - 您可以通过运行 Z3 --version 来验证这一点。然而，问题是 Z3 版本是 4.12.*，而 Haskell 的 Z3 绑定仅接受 4.8. 的 Z3 版本。所以这对 Haskell 和 Z3 的绑定不起作用。不幸的是，brew 没有安装 4.8. 版本的 Z3，因此您不能使用brew 来安装。在继续之前，您可以运行 brew uninstall Z3 来卸载 Z3。现在访问网站 https://github.com/Z3Prover/z3/releases/tag/z3-4.8.17 并下载 https://z3-4.8.17-arm64-osx-10.16。邮编/。然后运行“cabal install z3”，其标志 --extra-include-dirs 和 --extra-lib-dirs 分别引用 z3 标头和 libz3.* 目录。 （对我来说，这是 cabal install z3 -v3 --extra-include-dirs=/Users/PATH/z3-4.8.17-arm64-osx-10.16/include --extra-lib-dirs=/Users/PATH/ z3-4.8.17-arm64-osx-10.16/bin）即使当我运行此命令时，我也收到错误警告：检测到未知/不支持的“ghc”版本（Cabal 3.6.2.0 支持 “ghc”版本< 9.4因此我昨天问了这个问题。如果您安装了 ghcup，则只需使用 ghcup install ghc X*。在占位符 X 中指定 ghc 的版本，然后使用 ghc setup ghc X 使该版本成为 ghc 的工作版本。原因是您需要比 9.4 更旧的 ghc 版本才能安装 z3。执行此操作后，再次运行带有标志的命令 cabal install z3 ，如果它有效，那么它就有效。对我来说，它没有记录错误，我必须使用brew更改我的LLVM版本。我的版本是 17，但 cabal install z3 想要 9-13 之间的版本。所以我安装了版本12（要安装，您需要使用brew。您需要进一步取消链接并链接新版本。您可以google它或只是问Chatgpt）。然后，如果您运行 cabal install z3 但它仍然无法像我一样工作，请执行以下操作： !!!!!!
sudo cp /Users/PATH/z3-4.8.17-arm64-osx-10.16/bin/libz3.dylib /usr/local/lib/
!!!!! 好吧，我不会建议这样做，也不建议出于安全原因将其手动复制到 lib。然而，这有效（而且我真的需要它）。再次运行 cabal install z3 -v3 --extra-include-dirs=/Users/PATH/z3-4.8.17-arm64-osx-10.16/include 一切都应该可以工作。请注意，最后一个问题是由于 --extra-lib-dirs 标志显然无法识别该目录造成的。所以我手动将文件放到lib目录下。我希望这对某人有帮助，因为我花了很长时间才让 z3 与 haskell 绑定工作。 SBV 库是一个很好的选择，但我被告知它不能很好地对数组进行量化。不过我自己还没实验过。