在Mac上使用Haskell安装Z3绑定

ezykj2lf  于 2023-10-19  发布在  Mac
关注(0)|答案(1)|浏览(204)

我已经在我的电脑上安装了Z3（带有m1芯片的Mac），运行：

  1. brew install z3

我正在尝试安装Haskell的z3绑定。
图书馆网站上写着：

  1. Installation:
  3. 1) Install a Z3 4.x release. (Support for Z3 3.x is provided by the 0.3.2 version of these bindings.)
  5. 2) Just type cabal install z3 if you used the standard locations for dynamic libraries (/usr/lib) and header files (/usr/include).
  7. 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”，得到以下结果

  1. /opt/homebrew/include/z3.h
  2. /opt/homebrew/Cellar/z3/4.12.2/include/z3.h

我不知道为什么我有两个标题是诚实的，同样，我得到了路径的库

  1. /opt/homebrew/lib/libz3.4.12.dylib
  2. /opt/homebrew/lib/libz3.4.12.2.0.dylib
  3. /opt/homebrew/lib/libz3.dylib
  4. /opt/homebrew/Cellar/z3/4.12.2/lib/libz3.4.12.dylib
  5. /opt/homebrew/Cellar/z3/4.12.2/lib/libz3.4.12.2.0.dylib
  6. /opt/homebrew/Cellar/z3/4.12.2/lib/libz3.dylib

所以当我尝试以下任何一种

  1. stack install z3 --extra-lib-dirs=/opt/homebrew/lib --extra-include-dirs=/opt/homebrew/include
  3. OR
  5. 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

我得到一个错误：

  1. z3> configure
  2. z3> Configuring z3-408.2...
  3. z3> build
  4. z3> Preprocessing library for z3-408.2..
  5. z3> compiling .stack-work/dist/aarch64-osx/Cabal-3.8.1.0/build/Z3/Base/C_hsc_make.c failed (exit code 1)
  6. z3> rsp file was: ".stack-work/dist/aarch64-osx/Cabal-3.8.1.0/build/Z3/Base/hsc2hscall47771-0.rsp"
  7. 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/
  8. z3> error: clang: warning: -Wl,-no_fixup_chains: 'linker' input unused [-Wunused-command-line-argument]
  9. 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'?
  10. z3>     hsc_const (Z3_TRUE);
  11. z3>                ^~~~~~~
  12. z3>                Z3_L_TRUE
  13. 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'
  14. z3>     if ((x) < 0)                                      \
  15. z3>          ^
  16. z3> /opt/homebrew/Cellar/z3/4.12.2/include/z3_api.h:94:5: note: 'Z3_L_TRUE' declared here
  17. z3>     Z3_L_TRUE
  18. z3>     ^
  19. 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'?
  20. z3>     hsc_const (Z3_TRUE);
  21. z3>                ^~~~~~~
  22. z3>                Z3_L_TRUE
  23. 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'
  24. z3>         hsc_printf ("%lld", (long long)(x));          \
  25. z3>                                         ^
  26. z3> /opt/homebrew/Cellar/z3/4.12.2/include/z3_api.h:94:5: note: 'Z3_L_TRUE' declared here
  27. z3>     Z3_L_TRUE
  28. z3>     ^
  29. 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'?
  30. z3>     hsc_const (Z3_TRUE);
  31. z3>                ^~~~~~~
  32. z3>                Z3_L_TRUE
  33. 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'
  34. z3>         hsc_printf ("%llu", (unsigned long long)(x));
  35. z3>                                                  ^
  36. z3> /opt/homebrew/Cellar/z3/4.12.2/include/z3_api.h:94:5: note: 'Z3_L_TRUE' declared here
  37. z3>     Z3_L_TRUE
  38. z3>     ^
  39. 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'?
  40. z3>     hsc_const (Z3_FALSE);
  41. z3>                ^~~~~~~~
  42. z3>                Z3_L_FALSE
  43. 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'
  44. z3>     if ((x) < 0)                                      \
  45. z3>          ^
  46. z3> /opt/homebrew/Cellar/z3/4.12.2/include/z3_api.h:92:5: note: 'Z3_L_FALSE' declared here
  47. z3>     Z3_L_FALSE = -1,
  48. z3>     ^
  49. 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'?
  50. z3>     hsc_const (Z3_FALSE);
  51. z3>                ^~~~~~~~
  52. z3>                Z3_L_FALSE
  53. 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'
  54. z3>         hsc_printf ("%lld", (long long)(x));          \
  55. z3>                                         ^
  56. z3> /opt/homebrew/Cellar/z3/4.12.2/include/z3_api.h:92:5: note: 'Z3_L_FALSE' declared here
  57. z3>     Z3_L_FALSE = -1,
  58. z3>     ^
  59. 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'?
  60. z3>     hsc_const (Z3_FALSE);
  61. z3>                ^~~~~~~~
  62. z3>                Z3_L_FALSE
  63. 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'
  64. z3>         hsc_printf ("%llu", (unsigned long long)(x));
  65. z3>                                                  ^
  66. z3> /opt/homebrew/Cellar/z3/4.12.2/include/z3_api.h:92:5: note: 'Z3_L_FALSE' declared here
  67. z3>     Z3_L_FALSE = -1,
  68. z3>     ^
  69. z3> 6 errors generated.
  70. z3> 
  72. Error: [S-7282]
  73.        Stack failed to execute the build plan.
  74.        
  75.        While executing the build plan, Stack encountered the error:
  76.        
  77.        [S-7011]
  78.        While building package z3-408.2 (scroll up to its section to see the
  79.        error) using:
  80.        /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"
  81.        Process exited with code: ExitFailure 1

我不知道这是什么意思。我也用cabal运行了它，只是想看看它是否有效，但又得到了以下错误：

  1. Warning: Unknown/unsupported 'ghc' version detected (Cabal 3.6.2.0 supports
  2. 'ghc' version < 9.4): /Users/mehradhq/.ghcup/bin/ghc is version 9.4.7
  3. Warning: Unknown/unsupported 'ghc' version detected (Cabal 3.6.2.0 supports
  4. 'ghc' version < 9.4): /Users/mehradhq/.ghcup/bin/ghc is version 9.4.7
  5. Resolving dependencies...
  6. Build profile: -w ghc-9.4.7 -O1
  7. In order, the following will be built (use -v for more details):
  8.  - hsc2hs-0.68.10 (exe:hsc2hs) (requires download & build)
  9.  - z3-408.2 (lib) (requires download & build)
  10. Downloading  hsc2hs-0.68.10
  11. Downloaded   hsc2hs-0.68.10
  12. Downloading  z3-408.2
  13. Starting     hsc2hs-0.68.10 (exe:hsc2hs)
  14. Downloaded   z3-408.2
  15. Building     hsc2hs-0.68.10 (exe:hsc2hs)
  16. Installing   hsc2hs-0.68.10 (exe:hsc2hs)
  17. Completed    hsc2hs-0.68.10 (exe:hsc2hs)
  18. Starting     z3-408.2 (lib)
  20. Failed to build z3-408.2. The failure occurred during the configure step.
  21. Build log ( /Users/mehradhq/.cabal/logs/ghc-9.4.7/z3-408.2-f9eabcb0.log ):
  22. Configuring library for z3-408.2..
  23. cabal-3.6.2.0: Missing dependency on a foreign library:
  24. * Missing (or bad) header file: z3.h
  25. * Missing (or bad) C library: z3
  26. This problem can usually be solved by installing the system package that
  27. provides this library (you may need the "-dev" version). If the library is
  28. already installed but in a non-standard location then you can use the flags
  29. --extra-include-dirs= and --extra-lib-dirs= to specify where it is.If the
  30. library file does exist, it may contain errors that are caught by the C
  31. compiler at the preprocessing stage. In this case you can re-run configure
  32. with the verbosity flag -v3 to see the error messages.
  33. If the header file does exist, it may contain errors that are caught by the C
  34. compiler at the preprocessing stage. In this case you can re-run configure
  35. with the verbosity flag -v3 to see the error messages.
  37. cabal: Failed to build z3-408.2. See the build log above for details.

错误信息更清楚，但我已经安装了所有东西并定义了路径。我也看了Segmentation fault in Z3 (Haskell)的问题。我尝试了两种方法提出的回应，没有一个工作。我也在跑步：

  1. The Glorious Glasgow Haskell Compilation System, version 9.4.7
  2. The GHCup Haskell installer, version 0.1.19.4
  3. stack Version 2.11.1
  4. cabal-install version 3.6.2.0
  • 有人能解释一下问题是什么以及如何解决吗？谢谢你提前。*
haskell

1条答案

按热度按时间
hfsqlsce

hfsqlsce1#

只是为了其他人试图在mac上（使用arm处理器）运行Z3与haskell的绑定，并得到相同的错误，我将在这里发布对我有效的解决方案。基本上，通过执行以下命令安装Z3

  1. 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.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，它仍然不像我这样工作，请执行以下操作：！！！！！

  1. 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库是一个很好的选择，但我被告知，它不能很好地与数组量化。但我自己没有做过实验。

展开查看全部
赞(0）分享  回复(0）举报  2023-10-19
我来回答

相关问题

    查看更多

    热门标签

    更多
    JavaquerypythonNode开发语言requestUtil数据库Table后端算法LoggerMessageElementParser

    最新问答

    更多
    • 蜀ICP备13028337号-1 大数据知识库 https://www.saoniuhuo.com © All rights reserved
    • 本站内容来源互联网,如果侵犯您的权益请联系我们删除, 联系方式：448109455@qq.com