我已经在我的电脑上安装了Z3（带有m1芯片的Mac），运行：
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.错误信息更清楚，但我已经安装了所有东西并定义了路径。我也看了Segmentation fault in 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- 有人能解释一下问题是什么以及如何解决吗？谢谢你提前。*
1条答案
按热度按时间hfsqlsce1#
只是为了其他人试图在mac上（使用arm处理器）运行Z3与haskell的绑定，并得到相同的错误，我将在这里发布对我有效的解决方案。基本上，通过执行以下命令安装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.zip/。然后运行“cabal install z3”，标志--extra-include-dirs和--extra-lib-dirs分别指向z3头文件和libz 3. 目录。（对我来说，这是 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，但阴谋集团安装z3想要一个9-13之间的版本。所以我安装了版本12（安装你需要使用brew。您需要进一步取消链接并链接新版本。你可以在谷歌上搜索，或者直接问Chatgpt）。然后如果你运行cabal install z3，它仍然不像我这样工作，请执行以下操作：！！！！！
！！好吧，我不打算建议这样做，出于安全原因，不建议手动将其复制到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库是一个很好的选择，但我被告知，它不能很好地与数组量化。但我自己没有做过实验。