mirror of
https://github.com/Z3Prover/z3
synced 2025-09-14 13:41:27 +00:00
Add hybrid approach documentation for CMake
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
parent
25ff5d1446
commit
6a356f78c1
1 changed files with 71 additions and 12 deletions
|
@ -98,26 +98,32 @@ of z3 is required that may not match with the system version. With the following
|
||||||
cmake file of your project, z3 version 4.12.1 is downloaded to the build directory and the
|
cmake file of your project, z3 version 4.12.1 is downloaded to the build directory and the
|
||||||
cmake targets are added to the project:
|
cmake targets are added to the project:
|
||||||
|
|
||||||
```
|
```cmake
|
||||||
FetchContent_Declare(z3
|
include(FetchContent)
|
||||||
|
FetchContent_Declare(Z3
|
||||||
GIT_REPOSITORY https://github.com/Z3Prover/z3
|
GIT_REPOSITORY https://github.com/Z3Prover/z3
|
||||||
GIT_TAG z3-4.12.1
|
GIT_TAG z3-4.12.1
|
||||||
)
|
)
|
||||||
FetchContent_MakeAvailable(z3)
|
FetchContent_MakeAvailable(Z3)
|
||||||
```
|
```
|
||||||
|
|
||||||
The header files can be added to the included directories as follows:
|
Once fetched, you can link the z3 library to your target:
|
||||||
|
|
||||||
```
|
```cmake
|
||||||
include_directories( ${z3_SOURCE_DIR}/src/api )
|
target_link_libraries(yourTarget PRIVATE libz3)
|
||||||
```
|
```
|
||||||
|
|
||||||
Finally, the z3 library can be linked to a `yourTarget` using
|
**Note**: The target name is `libz3` (referring to the library target from `src/CMakeLists.txt`). The target automatically provides the necessary include directories, so no manual `include_directories()` call is needed.
|
||||||
|
|
||||||
|
**Alternative using target alias** (for consistency with system installs):
|
||||||
|
|
||||||
|
```cmake
|
||||||
|
# Create an alias for consistency with system install
|
||||||
|
if(NOT TARGET z3::libz3)
|
||||||
|
add_library(z3::libz3 ALIAS libz3)
|
||||||
|
endif()
|
||||||
|
target_link_libraries(yourTarget PRIVATE z3::libz3)
|
||||||
```
|
```
|
||||||
target_link_libraries(yourTarget libz3)
|
|
||||||
```
|
|
||||||
Note that this is `libz3` not `z3` (`libz3` refers to the library target from `src/CMakeLists.txt`).
|
|
||||||
|
|
||||||
#### Using system-installed Z3
|
#### Using system-installed Z3
|
||||||
|
|
||||||
|
@ -127,7 +133,13 @@ If you have Z3 installed on your system (e.g., via package manager or by buildin
|
||||||
find_package(Z3 REQUIRED CONFIG)
|
find_package(Z3 REQUIRED CONFIG)
|
||||||
```
|
```
|
||||||
|
|
||||||
Once found, you can use the Z3 include directories and libraries:
|
Once found, you can link to Z3 using the exported target (recommended):
|
||||||
|
|
||||||
|
```cmake
|
||||||
|
target_link_libraries(yourTarget PRIVATE z3::libz3)
|
||||||
|
```
|
||||||
|
|
||||||
|
**Alternative using variables** (for compatibility with older CMake code):
|
||||||
|
|
||||||
```cmake
|
```cmake
|
||||||
# For C projects
|
# For C projects
|
||||||
|
@ -141,8 +153,55 @@ target_link_libraries(yourTarget PRIVATE ${Z3_LIBRARIES})
|
||||||
|
|
||||||
The `find_package(Z3 CONFIG)` approach uses Z3's provided `Z3Config.cmake` file, which is installed to a standard location (typically `<prefix>/lib/cmake/z3/`). If CMake cannot automatically find Z3, you can help it by setting `-DZ3_DIR=<path>` where `<path>` is the directory containing the `Z3Config.cmake` file.
|
The `find_package(Z3 CONFIG)` approach uses Z3's provided `Z3Config.cmake` file, which is installed to a standard location (typically `<prefix>/lib/cmake/z3/`). If CMake cannot automatically find Z3, you can help it by setting `-DZ3_DIR=<path>` where `<path>` is the directory containing the `Z3Config.cmake` file.
|
||||||
|
|
||||||
**Note**: This approach requires that Z3 was built and installed using CMake. Z3 installations from the Python build system may not provide the necessary CMake configuration files.
|
**Note**: This approach requires that Z3 was built and installed using CMake. Z3 installations from the Python build system may not provide the necessary CMake configuration files. The exported target `z3::libz3` automatically provides the correct include directories and linking flags.
|
||||||
|
|
||||||
|
#### Using system-installed Z3 with FetchContent fallback
|
||||||
|
|
||||||
|
This approach combines the benefits of both methods above: it uses a system-installed Z3 if available and meets the minimum version requirement, otherwise falls back to fetching Z3 from the repository. This is often the most practical approach for projects.
|
||||||
|
|
||||||
|
```cmake
|
||||||
|
set(Z3_MIN_VERSION "4.12.1")
|
||||||
|
|
||||||
|
# First, try to find Z3 on the system
|
||||||
|
find_package(Z3 ${Z3_MIN_VERSION} CONFIG QUIET)
|
||||||
|
|
||||||
|
if(Z3_FOUND)
|
||||||
|
message(STATUS "Found system Z3 version ${Z3_VERSION_STRING}")
|
||||||
|
# Z3_LIBRARIES will contain z3::libz3
|
||||||
|
else()
|
||||||
|
message(STATUS "System Z3 not found or version too old, fetching Z3 ${Z3_MIN_VERSION}")
|
||||||
|
|
||||||
|
# Fallback to FetchContent
|
||||||
|
include(FetchContent)
|
||||||
|
FetchContent_Declare(Z3
|
||||||
|
GIT_REPOSITORY https://github.com/Z3Prover/z3
|
||||||
|
GIT_TAG z3-${Z3_MIN_VERSION}
|
||||||
|
)
|
||||||
|
FetchContent_MakeAvailable(Z3)
|
||||||
|
|
||||||
|
# Create an alias to match the system install target name
|
||||||
|
if(NOT TARGET z3::libz3)
|
||||||
|
add_library(z3::libz3 ALIAS libz3)
|
||||||
|
endif()
|
||||||
|
endif()
|
||||||
|
|
||||||
|
# Now use Z3 consistently regardless of how it was found
|
||||||
|
target_link_libraries(yourTarget PRIVATE z3::libz3)
|
||||||
|
```
|
||||||
|
|
||||||
|
**Key benefits of this approach:**
|
||||||
|
|
||||||
|
- **Consistent interface**: Both paths result in the same `z3::libz3` target
|
||||||
|
- **Version control**: Ensures minimum version requirements are met
|
||||||
|
- **Flexible deployment**: Works whether Z3 is pre-installed or not
|
||||||
|
- **Proper linking**: Uses CMake targets which handle include directories and linking automatically
|
||||||
|
|
||||||
|
**Important notes:**
|
||||||
|
|
||||||
|
- Use `z3::libz3` target instead of raw library names for better CMake integration
|
||||||
|
- The target automatically provides the correct include directories, so no need for manual `target_include_directories`
|
||||||
|
- When using FetchContent, an alias is created to ensure target name consistency
|
||||||
|
- Set `QUIET` in `find_package` to avoid error messages when Z3 isn't found
|
||||||
|
|
||||||
|
|
||||||
### Ninja
|
### Ninja
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue