首页 > 解决方案 > 在使用预发布版本中使用 cmake 实现 Z3

问题描述

set(Z3_DIR "../../z3-4.8.8-x64-osx-10.14.6")
include_directories(${Z3_DIR}/include)
set(Z3_LIBRARIES ${Z3_DIR}/bin/)
add_executable(exa main.cpp)
target_link_libraries(exa ${Z3_LIBRARIES})

我下载的是 Z3 的预发布版本,但文件结构与机器构建的完全不同。我如何编写包含目录以在我的 cpp 项目中使用预发布版本。树:

├── LICENSE.txt
├── bin
│   ├── Microsoft.Z3.deps.json
│   ├── Microsoft.Z3.dll
│   ├── com.microsoft.z3.jar
│   ├── libz3.a
│   ├── libz3.dylib
│   ├── libz3java.dylib
│   ├── python
│   │   ├── example.py
│   │   └── z3
│   │       ├── __init__.py
│   │       ├── __init__.pyc
│   │       ├── z3.py
│   │       ├── z3.pyc
│   │       ├── z3consts.py
│   │       ├── z3consts.pyc
│   │       ├── z3core.py
│   │       ├── z3core.pyc
│   │       ├── z3num.py
│   │       ├── z3num.pyc
│   │       ├── z3poly.py
│   │       ├── z3poly.pyc
│   │       ├── z3printer.py
│   │       ├── z3printer.pyc
│   │       ├── z3rcf.py
│   │       ├── z3rcf.pyc
│   │       ├── z3types.py
│   │       ├── z3types.pyc
│   │       ├── z3util.py
│   │       └── z3util.pyc
│   └── z3
└── include
    ├── z3++.h
    ├── z3.h
    ├── z3_algebraic.h
    ├── z3_api.h
    ├── z3_ast_containers.h
    ├── z3_fixedpoint.h
    ├── z3_fpa.h
    ├── z3_macros.h
    ├── z3_optimization.h
    ├── z3_polynomial.h
    ├── z3_rcf.h
    ├── z3_spacer.h
    ├── z3_v1.h
    └── z3_version.h

使用以下 cmakelists,致命错误:

输出在这里`/usr/local/Cellar/cmake/3.17.2/bin/cmake -S/Users/charles/guanqin/analysis/z3test -B/Users/charles/guanqin/analysis/z3test/build --check -build-system CMakeFiles/Makefile.cmake 0 /usr/local/Cellar/cmake/3.17.2/bin/cmake -E cmake_progress_start /Users/charles/guanqin/analysis/z3test/build/CMakeFiles /Users/charles/guanqin/分析/z3test/build/CMakeFiles/progress.marks /Library/Developer/CommandLineTools/usr/bin/make -f CMakeFiles/Makefile2 all /Library/Developer/CommandLineTools/usr/bin/make -f CMakeFiles/exa.dir/build .make CMakeFiles/exa.dir/depend cd /Users/charles/guanqin/analysis/z3test/build && /usr/local/Cellar/cmake/3.17.2/bin/cmake -E cmake_depends "Unix Makefiles"/Users/charles/guanqin/analysis/z3test /Users/charles/guanqin/analysis/z3test /Users/charles/guanqin/analysis/z3test/build /Users/charles/guanqin/analysis/z3test/build /Users/charles/guanqin /analysis/z3test/build/CMakeFiles/exa.dir/DependInfo.cmake --color= /Library/Developer/CommandLineTools/usr/bin/make -f CMakeFiles/exa.dir/build.make CMakeFiles/exa.dir/build [ 50%] 链接 CXX 可执行 exa

/usr/local/Cellar/cmake/3.17.2/bin/cmake -E cmake_link_script CMakeFiles/exa.dir/link.txt --verbose=1
/Library/Developer/CommandLineTools/usr/bin/c++   -isysroot /Library/Developer/CommandLineTools/SDKs/MacOSX10.15.sdk -Wl,-search_paths_first -Wl,-headerpad_max_install_names  CMakeFiles/exa.dir/main.o  -o exa   -L../z3-4.8.8-x64-osx-10.14.6/bin/libz3.dylib  -Wl,-rpath,../z3-4.8.8-x64-osx-10.14.6/bin/libz3.dylib -lz3 
ld: warning: directory not found for option '-L../z3-4.8.8-x64-osx-10.14.6/bin/libz3.dylib'
ld: library not found for -lz3
clang: error: linker command failed with exit code 1 (use -v to see invocation)
make[2]: *** [exa] Error 1
make[1]: *** [CMakeFiles/exa.dir/all] Error 2
make: *** [all] Error 2


标签: c++cmakez3

解决方案


推荐阅读