mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-12-10 13:53:23 +00:00
Code Activity
z3/CMakeLists.txt

660 lines
28 KiB
Text
Raw Permalink Normal View History

Fix CMake configure under CMake 3.1 with MSVC under Windows.
2016-02-29 18:18:58 +00:00
# Enforce some CMake policies
cmake: Require cmake 3.16 or later. (#7015) Support for requiring cmake < 3.4 may go away soon (according to a deprecation notice when building). Ubuntu 20.04 provides cmake 3.16 and current is 3.27, so that seems like a reasonable version to require.
2023-11-26 22:30:22 +07:00
cmake_minimum_required(VERSION 3.16)
bump cmake minimum version to 3.4 as it was released 3+ years ago some misc compiler flags cleanup
2019-03-07 09:58:36 +00:00
[CMake] Override CMake's default flags for GCC/Clang as we were doing before 4cc2b292c0cc8759da7a525e63dbfefdb06d6a01. It's useful to be able to control the defaults and CMake's internal logic for GCC/Clang is simple enough that doing this makes sense. It would be nice to do the same for MSVC but CMake's internal logic is more complicated so for now it's better that we just use CMake's default.
2017-04-29 17:45:02 +01:00
set(CMAKE_USER_MAKE_RULES_OVERRIDE_CXX "${CMAKE_CURRENT_SOURCE_DIR}/cmake/cxx_compiler_flags_overrides.cmake")
Create centralized version management with VERSION.txt (#7802) * Initial plan * Create VERSION.txt and update CMakeLists.txt to read version from file Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Complete centralized version management system Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Fix version update script and finalize implementation Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Create centralized version management with VERSION.txt Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
2025-08-20 09:12:33 -07:00
# Read version from VERSION.txt file
Move VERSION.txt to scripts directory and update all references (#7811) * Initial plan * Move VERSION.txt to scripts/ and update all references Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
2025-08-24 16:36:05 -07:00
file(READ "${CMAKE_CURRENT_SOURCE_DIR}/scripts/VERSION.txt" Z3_VERSION_FROM_FILE)
Create centralized version management with VERSION.txt (#7802) * Initial plan * Create VERSION.txt and update CMakeLists.txt to read version from file Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Complete centralized version management system Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Fix version update script and finalize implementation Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Create centralized version management with VERSION.txt Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
2025-08-20 09:12:33 -07:00
string(STRIP "${Z3_VERSION_FROM_FILE}" Z3_VERSION_FROM_FILE)
project(Z3 VERSION ${Z3_VERSION_FROM_FILE} LANGUAGES CXX)
Implement a CMake build system. This is a large rework of my first attempt at this (#459). This implementation calls into the recently implemented python scripts to generate the necessary generated ``.h`` and ``.cpp`` files but is independent from Python building system otherwise. Unlike the Python build system, the generated files are emitted into the build tree to avoid polluting the source tree. The build system is setup to refuse to configure if it detects generated files in the source tree. If your source tree is dirty you can run ``git clean -fx`` to clean your working directory. Currently the build succeeds on Linux using CMake 3.4.3 using the "Unix Makefiles" generator with gcc or clang. The following notable features are implemented: * Building of the C and C++ examples and the ``test-z3`` executable. These are included from the ``all`` target so you have to tell the build system (e.g. make) to build them manually. * Install (``make install``) and uninstall (``make uninstall``) of libz3 and its header files. This supports ``DESTDIR`` out of the box because CMake supports it. * An option (``BUILD_LIBZ3_SHARED``) to build libz3 as a static or dynamic library. * Support for using/not using OpenMP (``USE_OPENMP``) * Support for using/not using libgmp (``USE_LIB_GMP``) * Setting the SOVERSION for libz3. I'm not sure if I'm setting the * number correctly though. This is required by Linux distrubtions that wills ship libz3. This needs discussion. The following notable features are currently not implemented and are left for future work. * Support for ARM. * Support for the foci2 library. * Support for creating/installing/uninstalling the dotnet, java, python and ml bindings. * Full support for MSVC. Although I've tried to write the CMake code with MSVC in mind not all the correct flags are passed to it. * Support for using the git hash. This new build system has several advantages other the old build system. * It is easier for outside contributors to contribute to Z3 when the build system is something more standard. * Incremental builds work properly. With the old build system when new code is pulled down the old build directory would need to thrown out and a new fresh build had to be performed because the build system didn't know how to correctly rebuild the project (e.g. couldn't handle new sources being added/removed, compiler flags changing, generated files changing, etc...). This is a MASSIVE boost to productivity! * We now have access rich array of features that CMake provides for building C/C++ projects. This means less time spent implementing custom build system logic in Python that is already supported by CMake. * CMake supports many IDEs out of the box so it should be fairly straight forward to build Z3 with Visual Studio (once support for MSVC is added), Xcode, Eclipse CDT, CLion, ..etc.
2016-02-20 23:21:00 +00:00
################################################################################
# Project version
################################################################################
[CMake] Support including Git hash and description into the build. CMake will automatically pick up changes in git's HEAD so that the necessary code is rebuilt when the build system is invoked. Two new options `INCLUDE_GIT_HASH` and `INCLUDE_GIT_DESCRIBE` have been added that enable/disable including the git hash and the output of `git describe` respectively. By default if the source tree is a git repository both options are on, otherwise they are false by default. To support the `Z3GITHASH` macro a different implementation is used from the old build system. In that build system the define is passed on the command line. This would not work well for CMake because CMake conservatively (and correctly) rebuilds *everything* if the flags given to the compiler change. This would result in the entire project being rebuilt everytime git's `HEAD` changed. Instead in this implementation a CMake specific version of `version.h.in` (named `version.h.cmake.in`) is added that uses the `#cmakedefine` feature of CMake's `configure_file()` command to define `Z3GITHASH` if it is available and not define it otherwise. This way only object files that depend on `version.h` get re-built rather than the whole project. It is unfortunate that the build systems now have different `version.h` file templates. However they are very simple and I don't want to modify how templates are handled in the python/Makefile build system.
2017-03-12 12:29:26 +01:00
set(Z3_FULL_VERSION_STR "${Z3_VERSION}") # Note this might be modified
Implement a CMake build system. This is a large rework of my first attempt at this (#459). This implementation calls into the recently implemented python scripts to generate the necessary generated ``.h`` and ``.cpp`` files but is independent from Python building system otherwise. Unlike the Python build system, the generated files are emitted into the build tree to avoid polluting the source tree. The build system is setup to refuse to configure if it detects generated files in the source tree. If your source tree is dirty you can run ``git clean -fx`` to clean your working directory. Currently the build succeeds on Linux using CMake 3.4.3 using the "Unix Makefiles" generator with gcc or clang. The following notable features are implemented: * Building of the C and C++ examples and the ``test-z3`` executable. These are included from the ``all`` target so you have to tell the build system (e.g. make) to build them manually. * Install (``make install``) and uninstall (``make uninstall``) of libz3 and its header files. This supports ``DESTDIR`` out of the box because CMake supports it. * An option (``BUILD_LIBZ3_SHARED``) to build libz3 as a static or dynamic library. * Support for using/not using OpenMP (``USE_OPENMP``) * Support for using/not using libgmp (``USE_LIB_GMP``) * Setting the SOVERSION for libz3. I'm not sure if I'm setting the * number correctly though. This is required by Linux distrubtions that wills ship libz3. This needs discussion. The following notable features are currently not implemented and are left for future work. * Support for ARM. * Support for the foci2 library. * Support for creating/installing/uninstalling the dotnet, java, python and ml bindings. * Full support for MSVC. Although I've tried to write the CMake code with MSVC in mind not all the correct flags are passed to it. * Support for using the git hash. This new build system has several advantages other the old build system. * It is easier for outside contributors to contribute to Z3 when the build system is something more standard. * Incremental builds work properly. With the old build system when new code is pulled down the old build directory would need to thrown out and a new fresh build had to be performed because the build system didn't know how to correctly rebuild the project (e.g. couldn't handle new sources being added/removed, compiler flags changing, generated files changing, etc...). This is a MASSIVE boost to productivity! * We now have access rich array of features that CMake provides for building C/C++ projects. This means less time spent implementing custom build system logic in Python that is already supported by CMake. * CMake supports many IDEs out of the box so it should be fairly straight forward to build Z3 with Visual Studio (once support for MSVC is added), Xcode, Eclipse CDT, CLion, ..etc.
2016-02-20 23:21:00 +00:00
message(STATUS "Z3 version ${Z3_VERSION}")
################################################################################
# Message for polluted source tree sanity checks
################################################################################
set(z3_polluted_tree_msg
" should not exist and is polluting the source tree."
" It is likely that this file came from the Python build system which"
" generates files inside the source tree. This is bad practice and the CMake"
" build system is setup to make sure that the source tree is clean during"
" its configure step. If you are using git you can remove all untracked files"
" using ``git clean -fx``. Be careful when doing this. You should probably use"
" this with ``-n`` first to check which file(s) would be removed."
)
Add sanity check to make sure in-source CMake builds are disallowed.
2016-02-29 16:28:53 +00:00
################################################################################
# Sanity check - Disallow building in source
################################################################################
clean up CMake code (#5182) * CMake: simplify FindGMP.cmake Remove printing of all the different variables, and let FPHSA output the library name. Add an imported target, which bundles the library and the include directories for easier usage. * fix build: vector::c_ptr() now is vector::data() * CMake: use Threads::Threads imported module Otherwise the setting of THREADS_PREFER_PTHREAD_FLAG has no effect. * CMake: remove needless policy setting The minimum required version is CMake 3.4, where these policies are already set to new because they were introduced earlier. * CMake: remove needless variable expansion
2021-04-14 19:29:15 +02:00
if (PROJECT_SOURCE_DIR STREQUAL PROJECT_BINARY_DIR)
Add sanity check to make sure in-source CMake builds are disallowed.
2016-02-29 16:28:53 +00:00
message(FATAL_ERROR "In source builds are not allowed. You should invoke "
"CMake from a different directory.")
endif()
Implement a CMake build system. This is a large rework of my first attempt at this (#459). This implementation calls into the recently implemented python scripts to generate the necessary generated ``.h`` and ``.cpp`` files but is independent from Python building system otherwise. Unlike the Python build system, the generated files are emitted into the build tree to avoid polluting the source tree. The build system is setup to refuse to configure if it detects generated files in the source tree. If your source tree is dirty you can run ``git clean -fx`` to clean your working directory. Currently the build succeeds on Linux using CMake 3.4.3 using the "Unix Makefiles" generator with gcc or clang. The following notable features are implemented: * Building of the C and C++ examples and the ``test-z3`` executable. These are included from the ``all`` target so you have to tell the build system (e.g. make) to build them manually. * Install (``make install``) and uninstall (``make uninstall``) of libz3 and its header files. This supports ``DESTDIR`` out of the box because CMake supports it. * An option (``BUILD_LIBZ3_SHARED``) to build libz3 as a static or dynamic library. * Support for using/not using OpenMP (``USE_OPENMP``) * Support for using/not using libgmp (``USE_LIB_GMP``) * Setting the SOVERSION for libz3. I'm not sure if I'm setting the * number correctly though. This is required by Linux distrubtions that wills ship libz3. This needs discussion. The following notable features are currently not implemented and are left for future work. * Support for ARM. * Support for the foci2 library. * Support for creating/installing/uninstalling the dotnet, java, python and ml bindings. * Full support for MSVC. Although I've tried to write the CMake code with MSVC in mind not all the correct flags are passed to it. * Support for using the git hash. This new build system has several advantages other the old build system. * It is easier for outside contributors to contribute to Z3 when the build system is something more standard. * Incremental builds work properly. With the old build system when new code is pulled down the old build directory would need to thrown out and a new fresh build had to be performed because the build system didn't know how to correctly rebuild the project (e.g. couldn't handle new sources being added/removed, compiler flags changing, generated files changing, etc...). This is a MASSIVE boost to productivity! * We now have access rich array of features that CMake provides for building C/C++ projects. This means less time spent implementing custom build system logic in Python that is already supported by CMake. * CMake supports many IDEs out of the box so it should be fairly straight forward to build Z3 with Visual Studio (once support for MSVC is added), Xcode, Eclipse CDT, CLion, ..etc.
2016-02-20 23:21:00 +00:00
################################################################################
# Add our CMake module directory to the list of module search directories
################################################################################
Change from BINARY_DIR to PROJECT_BINARY_DIR
2019-05-15 11:25:40 -07:00
list(APPEND CMAKE_MODULE_PATH "${PROJECT_SOURCE_DIR}/cmake/modules")
Implement a CMake build system. This is a large rework of my first attempt at this (#459). This implementation calls into the recently implemented python scripts to generate the necessary generated ``.h`` and ``.cpp`` files but is independent from Python building system otherwise. Unlike the Python build system, the generated files are emitted into the build tree to avoid polluting the source tree. The build system is setup to refuse to configure if it detects generated files in the source tree. If your source tree is dirty you can run ``git clean -fx`` to clean your working directory. Currently the build succeeds on Linux using CMake 3.4.3 using the "Unix Makefiles" generator with gcc or clang. The following notable features are implemented: * Building of the C and C++ examples and the ``test-z3`` executable. These are included from the ``all`` target so you have to tell the build system (e.g. make) to build them manually. * Install (``make install``) and uninstall (``make uninstall``) of libz3 and its header files. This supports ``DESTDIR`` out of the box because CMake supports it. * An option (``BUILD_LIBZ3_SHARED``) to build libz3 as a static or dynamic library. * Support for using/not using OpenMP (``USE_OPENMP``) * Support for using/not using libgmp (``USE_LIB_GMP``) * Setting the SOVERSION for libz3. I'm not sure if I'm setting the * number correctly though. This is required by Linux distrubtions that wills ship libz3. This needs discussion. The following notable features are currently not implemented and are left for future work. * Support for ARM. * Support for the foci2 library. * Support for creating/installing/uninstalling the dotnet, java, python and ml bindings. * Full support for MSVC. Although I've tried to write the CMake code with MSVC in mind not all the correct flags are passed to it. * Support for using the git hash. This new build system has several advantages other the old build system. * It is easier for outside contributors to contribute to Z3 when the build system is something more standard. * Incremental builds work properly. With the old build system when new code is pulled down the old build directory would need to thrown out and a new fresh build had to be performed because the build system didn't know how to correctly rebuild the project (e.g. couldn't handle new sources being added/removed, compiler flags changing, generated files changing, etc...). This is a MASSIVE boost to productivity! * We now have access rich array of features that CMake provides for building C/C++ projects. This means less time spent implementing custom build system logic in Python that is already supported by CMake. * CMake supports many IDEs out of the box so it should be fairly straight forward to build Z3 with Visual Studio (once support for MSVC is added), Xcode, Eclipse CDT, CLion, ..etc.
2016-02-20 23:21:00 +00:00
################################################################################
[CMake] Support including Git hash and description into the build. CMake will automatically pick up changes in git's HEAD so that the necessary code is rebuilt when the build system is invoked. Two new options `INCLUDE_GIT_HASH` and `INCLUDE_GIT_DESCRIBE` have been added that enable/disable including the git hash and the output of `git describe` respectively. By default if the source tree is a git repository both options are on, otherwise they are false by default. To support the `Z3GITHASH` macro a different implementation is used from the old build system. In that build system the define is passed on the command line. This would not work well for CMake because CMake conservatively (and correctly) rebuilds *everything* if the flags given to the compiler change. This would result in the entire project being rebuilt everytime git's `HEAD` changed. Instead in this implementation a CMake specific version of `version.h.in` (named `version.h.cmake.in`) is added that uses the `#cmakedefine` feature of CMake's `configure_file()` command to define `Z3GITHASH` if it is available and not define it otherwise. This way only object files that depend on `version.h` get re-built rather than the whole project. It is unfortunate that the build systems now have different `version.h` file templates. However they are very simple and I don't want to modify how templates are handled in the python/Makefile build system.
2017-03-12 12:29:26 +01:00
# Handle git hash and description
################################################################################
Change from BINARY_DIR to PROJECT_BINARY_DIR
2019-05-15 11:25:40 -07:00
include(${PROJECT_SOURCE_DIR}/cmake/git_utils.cmake)
[CMake] Support including Git hash and description into the build. CMake will automatically pick up changes in git's HEAD so that the necessary code is rebuilt when the build system is invoked. Two new options `INCLUDE_GIT_HASH` and `INCLUDE_GIT_DESCRIBE` have been added that enable/disable including the git hash and the output of `git describe` respectively. By default if the source tree is a git repository both options are on, otherwise they are false by default. To support the `Z3GITHASH` macro a different implementation is used from the old build system. In that build system the define is passed on the command line. This would not work well for CMake because CMake conservatively (and correctly) rebuilds *everything* if the flags given to the compiler change. This would result in the entire project being rebuilt everytime git's `HEAD` changed. Instead in this implementation a CMake specific version of `version.h.in` (named `version.h.cmake.in`) is added that uses the `#cmakedefine` feature of CMake's `configure_file()` command to define `Z3GITHASH` if it is available and not define it otherwise. This way only object files that depend on `version.h` get re-built rather than the whole project. It is unfortunate that the build systems now have different `version.h` file templates. However they are very simple and I don't want to modify how templates are handled in the python/Makefile build system.
2017-03-12 12:29:26 +01:00
macro(disable_git_describe)
CMake: Improve handling of git hash/describe (#7028) Only check for and depend on the .git folder if requested. Only warn about disabling when enabled. Only add git hash to version if valid.
2023-12-02 18:47:57 +01:00
if(Z3_INCLUDE_GIT_DESCRIBE)
message(WARNING "Disabling Z3_INCLUDE_GIT_DESCRIBE")
set(Z3_INCLUDE_GIT_DESCRIBE OFF CACHE BOOL "Include git describe output in version output" FORCE)
endif()
[CMake] Support including Git hash and description into the build. CMake will automatically pick up changes in git's HEAD so that the necessary code is rebuilt when the build system is invoked. Two new options `INCLUDE_GIT_HASH` and `INCLUDE_GIT_DESCRIBE` have been added that enable/disable including the git hash and the output of `git describe` respectively. By default if the source tree is a git repository both options are on, otherwise they are false by default. To support the `Z3GITHASH` macro a different implementation is used from the old build system. In that build system the define is passed on the command line. This would not work well for CMake because CMake conservatively (and correctly) rebuilds *everything* if the flags given to the compiler change. This would result in the entire project being rebuilt everytime git's `HEAD` changed. Instead in this implementation a CMake specific version of `version.h.in` (named `version.h.cmake.in`) is added that uses the `#cmakedefine` feature of CMake's `configure_file()` command to define `Z3GITHASH` if it is available and not define it otherwise. This way only object files that depend on `version.h` get re-built rather than the whole project. It is unfortunate that the build systems now have different `version.h` file templates. However they are very simple and I don't want to modify how templates are handled in the python/Makefile build system.
2017-03-12 12:29:26 +01:00
endmacro()
macro(disable_git_hash)
CMake: Improve handling of git hash/describe (#7028) Only check for and depend on the .git folder if requested. Only warn about disabling when enabled. Only add git hash to version if valid.
2023-12-02 18:47:57 +01:00
if(Z3_INCLUDE_GIT_HASH)
message(WARNING "Disabling Z3_INCLUDE_GIT_HASH")
set(Z3_INCLUDE_GIT_HASH OFF CACHE BOOL "Include git hash in version output" FORCE)
endif()
[CMake] Support including Git hash and description into the build. CMake will automatically pick up changes in git's HEAD so that the necessary code is rebuilt when the build system is invoked. Two new options `INCLUDE_GIT_HASH` and `INCLUDE_GIT_DESCRIBE` have been added that enable/disable including the git hash and the output of `git describe` respectively. By default if the source tree is a git repository both options are on, otherwise they are false by default. To support the `Z3GITHASH` macro a different implementation is used from the old build system. In that build system the define is passed on the command line. This would not work well for CMake because CMake conservatively (and correctly) rebuilds *everything* if the flags given to the compiler change. This would result in the entire project being rebuilt everytime git's `HEAD` changed. Instead in this implementation a CMake specific version of `version.h.in` (named `version.h.cmake.in`) is added that uses the `#cmakedefine` feature of CMake's `configure_file()` command to define `Z3GITHASH` if it is available and not define it otherwise. This way only object files that depend on `version.h` get re-built rather than the whole project. It is unfortunate that the build systems now have different `version.h` file templates. However they are very simple and I don't want to modify how templates are handled in the python/Makefile build system.
2017-03-12 12:29:26 +01:00
endmacro()
rename additional build options #2709 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-11-18 20:39:04 -08:00
option(Z3_INCLUDE_GIT_HASH "Include git hash in version output" ON)
option(Z3_INCLUDE_GIT_DESCRIBE "Include git describe output in version output" ON)
[CMake] Support including Git hash and description into the build. CMake will automatically pick up changes in git's HEAD so that the necessary code is rebuilt when the build system is invoked. Two new options `INCLUDE_GIT_HASH` and `INCLUDE_GIT_DESCRIBE` have been added that enable/disable including the git hash and the output of `git describe` respectively. By default if the source tree is a git repository both options are on, otherwise they are false by default. To support the `Z3GITHASH` macro a different implementation is used from the old build system. In that build system the define is passed on the command line. This would not work well for CMake because CMake conservatively (and correctly) rebuilds *everything* if the flags given to the compiler change. This would result in the entire project being rebuilt everytime git's `HEAD` changed. Instead in this implementation a CMake specific version of `version.h.in` (named `version.h.cmake.in`) is added that uses the `#cmakedefine` feature of CMake's `configure_file()` command to define `Z3GITHASH` if it is available and not define it otherwise. This way only object files that depend on `version.h` get re-built rather than the whole project. It is unfortunate that the build systems now have different `version.h` file templates. However they are very simple and I don't want to modify how templates are handled in the python/Makefile build system.
2017-03-12 12:29:26 +01:00
Change from BINARY_DIR to PROJECT_BINARY_DIR
2019-05-15 11:25:40 -07:00
set(GIT_DIR "${PROJECT_SOURCE_DIR}/.git")
CMake: Improve handling of git hash/describe (#7028) Only check for and depend on the .git folder if requested. Only warn about disabling when enabled. Only add git hash to version if valid.
2023-12-02 18:47:57 +01:00
if ((Z3_INCLUDE_GIT_HASH OR Z3_INCLUDE_GIT_HASH) AND EXISTS "${GIT_DIR}")
[CMake] Support including Git hash and description into the build. CMake will automatically pick up changes in git's HEAD so that the necessary code is rebuilt when the build system is invoked. Two new options `INCLUDE_GIT_HASH` and `INCLUDE_GIT_DESCRIBE` have been added that enable/disable including the git hash and the output of `git describe` respectively. By default if the source tree is a git repository both options are on, otherwise they are false by default. To support the `Z3GITHASH` macro a different implementation is used from the old build system. In that build system the define is passed on the command line. This would not work well for CMake because CMake conservatively (and correctly) rebuilds *everything* if the flags given to the compiler change. This would result in the entire project being rebuilt everytime git's `HEAD` changed. Instead in this implementation a CMake specific version of `version.h.in` (named `version.h.cmake.in`) is added that uses the `#cmakedefine` feature of CMake's `configure_file()` command to define `Z3GITHASH` if it is available and not define it otherwise. This way only object files that depend on `version.h` get re-built rather than the whole project. It is unfortunate that the build systems now have different `version.h` file templates. However they are very simple and I don't want to modify how templates are handled in the python/Makefile build system.
2017-03-12 12:29:26 +01:00
# Try to make CMake configure depend on the current git HEAD so that
# a re-configure is triggered when the HEAD changes.
fix git dir for git-dependency in cmake (#4759) This is not fixed as #1993 stated. Co-authored-by: Ding Fei <fei.ding@ustchcs.com>
2020-10-29 01:08:13 +08:00
add_git_dir_dependency("${GIT_DIR}" ADD_GIT_DEP_SUCCESS)
[CMake] Support including Git hash and description into the build. CMake will automatically pick up changes in git's HEAD so that the necessary code is rebuilt when the build system is invoked. Two new options `INCLUDE_GIT_HASH` and `INCLUDE_GIT_DESCRIBE` have been added that enable/disable including the git hash and the output of `git describe` respectively. By default if the source tree is a git repository both options are on, otherwise they are false by default. To support the `Z3GITHASH` macro a different implementation is used from the old build system. In that build system the define is passed on the command line. This would not work well for CMake because CMake conservatively (and correctly) rebuilds *everything* if the flags given to the compiler change. This would result in the entire project being rebuilt everytime git's `HEAD` changed. Instead in this implementation a CMake specific version of `version.h.in` (named `version.h.cmake.in`) is added that uses the `#cmakedefine` feature of CMake's `configure_file()` command to define `Z3GITHASH` if it is available and not define it otherwise. This way only object files that depend on `version.h` get re-built rather than the whole project. It is unfortunate that the build systems now have different `version.h` file templates. However they are very simple and I don't want to modify how templates are handled in the python/Makefile build system.
2017-03-12 12:29:26 +01:00
if (ADD_GIT_DEP_SUCCESS)
rename additional build options #2709 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-11-18 20:39:04 -08:00
if (Z3_INCLUDE_GIT_HASH)
[CMake] Support including Git hash and description into the build. CMake will automatically pick up changes in git's HEAD so that the necessary code is rebuilt when the build system is invoked. Two new options `INCLUDE_GIT_HASH` and `INCLUDE_GIT_DESCRIBE` have been added that enable/disable including the git hash and the output of `git describe` respectively. By default if the source tree is a git repository both options are on, otherwise they are false by default. To support the `Z3GITHASH` macro a different implementation is used from the old build system. In that build system the define is passed on the command line. This would not work well for CMake because CMake conservatively (and correctly) rebuilds *everything* if the flags given to the compiler change. This would result in the entire project being rebuilt everytime git's `HEAD` changed. Instead in this implementation a CMake specific version of `version.h.in` (named `version.h.cmake.in`) is added that uses the `#cmakedefine` feature of CMake's `configure_file()` command to define `Z3GITHASH` if it is available and not define it otherwise. This way only object files that depend on `version.h` get re-built rather than the whole project. It is unfortunate that the build systems now have different `version.h` file templates. However they are very simple and I don't want to modify how templates are handled in the python/Makefile build system.
2017-03-12 12:29:26 +01:00
get_git_head_hash("${GIT_DIR}" Z3GITHASH)
if (NOT Z3GITHASH)
message(WARNING "Failed to get Git hash")
disable_git_hash()
CMake: Improve handling of git hash/describe (#7028) Only check for and depend on the .git folder if requested. Only warn about disabling when enabled. Only add git hash to version if valid.
2023-12-02 18:47:57 +01:00
else()
message(STATUS "Using Git hash in version output: ${Z3GITHASH}")
# This mimics the behaviour of the old build system.
set(Z3_FULL_VERSION_STR "${Z3_FULL_VERSION_STR} ${Z3GITHASH}")
[CMake] Support including Git hash and description into the build. CMake will automatically pick up changes in git's HEAD so that the necessary code is rebuilt when the build system is invoked. Two new options `INCLUDE_GIT_HASH` and `INCLUDE_GIT_DESCRIBE` have been added that enable/disable including the git hash and the output of `git describe` respectively. By default if the source tree is a git repository both options are on, otherwise they are false by default. To support the `Z3GITHASH` macro a different implementation is used from the old build system. In that build system the define is passed on the command line. This would not work well for CMake because CMake conservatively (and correctly) rebuilds *everything* if the flags given to the compiler change. This would result in the entire project being rebuilt everytime git's `HEAD` changed. Instead in this implementation a CMake specific version of `version.h.in` (named `version.h.cmake.in`) is added that uses the `#cmakedefine` feature of CMake's `configure_file()` command to define `Z3GITHASH` if it is available and not define it otherwise. This way only object files that depend on `version.h` get re-built rather than the whole project. It is unfortunate that the build systems now have different `version.h` file templates. However they are very simple and I don't want to modify how templates are handled in the python/Makefile build system.
2017-03-12 12:29:26 +01:00
endif()
else()
message(STATUS "Not using Git hash in version output")
endif()
rename additional build options #2709 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-11-18 20:39:04 -08:00
if (Z3_INCLUDE_GIT_DESCRIBE)
[CMake] Support including Git hash and description into the build. CMake will automatically pick up changes in git's HEAD so that the necessary code is rebuilt when the build system is invoked. Two new options `INCLUDE_GIT_HASH` and `INCLUDE_GIT_DESCRIBE` have been added that enable/disable including the git hash and the output of `git describe` respectively. By default if the source tree is a git repository both options are on, otherwise they are false by default. To support the `Z3GITHASH` macro a different implementation is used from the old build system. In that build system the define is passed on the command line. This would not work well for CMake because CMake conservatively (and correctly) rebuilds *everything* if the flags given to the compiler change. This would result in the entire project being rebuilt everytime git's `HEAD` changed. Instead in this implementation a CMake specific version of `version.h.in` (named `version.h.cmake.in`) is added that uses the `#cmakedefine` feature of CMake's `configure_file()` command to define `Z3GITHASH` if it is available and not define it otherwise. This way only object files that depend on `version.h` get re-built rather than the whole project. It is unfortunate that the build systems now have different `version.h` file templates. However they are very simple and I don't want to modify how templates are handled in the python/Makefile build system.
2017-03-12 12:29:26 +01:00
get_git_head_describe("${GIT_DIR}" Z3_GIT_DESCRIPTION)
if (NOT Z3_GIT_DESCRIPTION)
message(WARNING "Failed to get Git description")
disable_git_describe()
endif()
message(STATUS "Using Git description in version output: ${Z3_GIT_DESCRIPTION}")
# This mimics the behaviour of the old build system.
[CMake] Fix detection of git description and hash for CMake 2.8.12
2017-06-24 15:15:27 +01:00
set(Z3_FULL_VERSION_STR "${Z3_FULL_VERSION_STR} ${Z3_GIT_DESCRIPTION}")
[CMake] Support including Git hash and description into the build. CMake will automatically pick up changes in git's HEAD so that the necessary code is rebuilt when the build system is invoked. Two new options `INCLUDE_GIT_HASH` and `INCLUDE_GIT_DESCRIBE` have been added that enable/disable including the git hash and the output of `git describe` respectively. By default if the source tree is a git repository both options are on, otherwise they are false by default. To support the `Z3GITHASH` macro a different implementation is used from the old build system. In that build system the define is passed on the command line. This would not work well for CMake because CMake conservatively (and correctly) rebuilds *everything* if the flags given to the compiler change. This would result in the entire project being rebuilt everytime git's `HEAD` changed. Instead in this implementation a CMake specific version of `version.h.in` (named `version.h.cmake.in`) is added that uses the `#cmakedefine` feature of CMake's `configure_file()` command to define `Z3GITHASH` if it is available and not define it otherwise. This way only object files that depend on `version.h` get re-built rather than the whole project. It is unfortunate that the build systems now have different `version.h` file templates. However they are very simple and I don't want to modify how templates are handled in the python/Makefile build system.
2017-03-12 12:29:26 +01:00
else()
Typo Fixes (#6803)
2023-07-09 14:56:10 -04:00
message(STATUS "Not including git description in version")
[CMake] Support including Git hash and description into the build. CMake will automatically pick up changes in git's HEAD so that the necessary code is rebuilt when the build system is invoked. Two new options `INCLUDE_GIT_HASH` and `INCLUDE_GIT_DESCRIBE` have been added that enable/disable including the git hash and the output of `git describe` respectively. By default if the source tree is a git repository both options are on, otherwise they are false by default. To support the `Z3GITHASH` macro a different implementation is used from the old build system. In that build system the define is passed on the command line. This would not work well for CMake because CMake conservatively (and correctly) rebuilds *everything* if the flags given to the compiler change. This would result in the entire project being rebuilt everytime git's `HEAD` changed. Instead in this implementation a CMake specific version of `version.h.in` (named `version.h.cmake.in`) is added that uses the `#cmakedefine` feature of CMake's `configure_file()` command to define `Z3GITHASH` if it is available and not define it otherwise. This way only object files that depend on `version.h` get re-built rather than the whole project. It is unfortunate that the build systems now have different `version.h` file templates. However they are very simple and I don't want to modify how templates are handled in the python/Makefile build system.
2017-03-12 12:29:26 +01:00
endif()
else()
message(WARNING "Failed to add git dependency.")
disable_git_describe()
disable_git_hash()
endif()
else()
message(STATUS "Failed to find git directory.")
disable_git_describe()
disable_git_hash()
endif()
CMake: Improve handling of git hash/describe (#7028) Only check for and depend on the .git folder if requested. Only warn about disabling when enabled. Only add git hash to version if valid.
2023-12-02 18:47:57 +01:00
if(NOT Z3_INCLUDE_GIT_HASH)
unset(Z3GITHASH) # Used in configure_file()
endif()
[CMake] Support including Git hash and description into the build. CMake will automatically pick up changes in git's HEAD so that the necessary code is rebuilt when the build system is invoked. Two new options `INCLUDE_GIT_HASH` and `INCLUDE_GIT_DESCRIBE` have been added that enable/disable including the git hash and the output of `git describe` respectively. By default if the source tree is a git repository both options are on, otherwise they are false by default. To support the `Z3GITHASH` macro a different implementation is used from the old build system. In that build system the define is passed on the command line. This would not work well for CMake because CMake conservatively (and correctly) rebuilds *everything* if the flags given to the compiler change. This would result in the entire project being rebuilt everytime git's `HEAD` changed. Instead in this implementation a CMake specific version of `version.h.in` (named `version.h.cmake.in`) is added that uses the `#cmakedefine` feature of CMake's `configure_file()` command to define `Z3GITHASH` if it is available and not define it otherwise. This way only object files that depend on `version.h` get re-built rather than the whole project. It is unfortunate that the build systems now have different `version.h` file templates. However they are very simple and I don't want to modify how templates are handled in the python/Makefile build system.
2017-03-12 12:29:26 +01:00
################################################################################
Implement a CMake build system. This is a large rework of my first attempt at this (#459). This implementation calls into the recently implemented python scripts to generate the necessary generated ``.h`` and ``.cpp`` files but is independent from Python building system otherwise. Unlike the Python build system, the generated files are emitted into the build tree to avoid polluting the source tree. The build system is setup to refuse to configure if it detects generated files in the source tree. If your source tree is dirty you can run ``git clean -fx`` to clean your working directory. Currently the build succeeds on Linux using CMake 3.4.3 using the "Unix Makefiles" generator with gcc or clang. The following notable features are implemented: * Building of the C and C++ examples and the ``test-z3`` executable. These are included from the ``all`` target so you have to tell the build system (e.g. make) to build them manually. * Install (``make install``) and uninstall (``make uninstall``) of libz3 and its header files. This supports ``DESTDIR`` out of the box because CMake supports it. * An option (``BUILD_LIBZ3_SHARED``) to build libz3 as a static or dynamic library. * Support for using/not using OpenMP (``USE_OPENMP``) * Support for using/not using libgmp (``USE_LIB_GMP``) * Setting the SOVERSION for libz3. I'm not sure if I'm setting the * number correctly though. This is required by Linux distrubtions that wills ship libz3. This needs discussion. The following notable features are currently not implemented and are left for future work. * Support for ARM. * Support for the foci2 library. * Support for creating/installing/uninstalling the dotnet, java, python and ml bindings. * Full support for MSVC. Although I've tried to write the CMake code with MSVC in mind not all the correct flags are passed to it. * Support for using the git hash. This new build system has several advantages other the old build system. * It is easier for outside contributors to contribute to Z3 when the build system is something more standard. * Incremental builds work properly. With the old build system when new code is pulled down the old build directory would need to thrown out and a new fresh build had to be performed because the build system didn't know how to correctly rebuild the project (e.g. couldn't handle new sources being added/removed, compiler flags changing, generated files changing, etc...). This is a MASSIVE boost to productivity! * We now have access rich array of features that CMake provides for building C/C++ projects. This means less time spent implementing custom build system logic in Python that is already supported by CMake. * CMake supports many IDEs out of the box so it should be fairly straight forward to build Z3 with Visual Studio (once support for MSVC is added), Xcode, Eclipse CDT, CLion, ..etc.
2016-02-20 23:21:00 +00:00
# Useful CMake functions/Macros
################################################################################
include(CheckCXXSourceCompiles)
fix #2708 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-11-19 21:36:13 -08:00
include(CMakeDependentOption)
Implement a CMake build system. This is a large rework of my first attempt at this (#459). This implementation calls into the recently implemented python scripts to generate the necessary generated ``.h`` and ``.cpp`` files but is independent from Python building system otherwise. Unlike the Python build system, the generated files are emitted into the build tree to avoid polluting the source tree. The build system is setup to refuse to configure if it detects generated files in the source tree. If your source tree is dirty you can run ``git clean -fx`` to clean your working directory. Currently the build succeeds on Linux using CMake 3.4.3 using the "Unix Makefiles" generator with gcc or clang. The following notable features are implemented: * Building of the C and C++ examples and the ``test-z3`` executable. These are included from the ``all`` target so you have to tell the build system (e.g. make) to build them manually. * Install (``make install``) and uninstall (``make uninstall``) of libz3 and its header files. This supports ``DESTDIR`` out of the box because CMake supports it. * An option (``BUILD_LIBZ3_SHARED``) to build libz3 as a static or dynamic library. * Support for using/not using OpenMP (``USE_OPENMP``) * Support for using/not using libgmp (``USE_LIB_GMP``) * Setting the SOVERSION for libz3. I'm not sure if I'm setting the * number correctly though. This is required by Linux distrubtions that wills ship libz3. This needs discussion. The following notable features are currently not implemented and are left for future work. * Support for ARM. * Support for the foci2 library. * Support for creating/installing/uninstalling the dotnet, java, python and ml bindings. * Full support for MSVC. Although I've tried to write the CMake code with MSVC in mind not all the correct flags are passed to it. * Support for using the git hash. This new build system has several advantages other the old build system. * It is easier for outside contributors to contribute to Z3 when the build system is something more standard. * Incremental builds work properly. With the old build system when new code is pulled down the old build directory would need to thrown out and a new fresh build had to be performed because the build system didn't know how to correctly rebuild the project (e.g. couldn't handle new sources being added/removed, compiler flags changing, generated files changing, etc...). This is a MASSIVE boost to productivity! * We now have access rich array of features that CMake provides for building C/C++ projects. This means less time spent implementing custom build system logic in Python that is already supported by CMake. * CMake supports many IDEs out of the box so it should be fairly straight forward to build Z3 with Visual Studio (once support for MSVC is added), Xcode, Eclipse CDT, CLion, ..etc.
2016-02-20 23:21:00 +00:00
################################################################################
# Compiler flags for Z3 components.
# Subsequent commands will append to this
################################################################################
set(Z3_COMPONENT_CXX_DEFINES "")
set(Z3_COMPONENT_CXX_FLAGS "")
set(Z3_COMPONENT_EXTRA_INCLUDE_DIRS "")
set(Z3_DEPENDENT_LIBS "")
Don't append ${OpenMP_CXX_FLAGS} to Z3_DEPENDENT_LIBS. This is wrong because this is passed to ``target_link_libraries()``. It just so happens that ``target_link_libraries()`` will interpret arguments starting with a dash as a flag to pass to the linker (i.e. in this case ``-fopenmp``). However in the case of MSVC that flag is ``/openmp`` which is the interpreted as a file path which will lead to a linker failure later because the linker can't find the file ``\openmp.obj``.
2016-02-29 20:53:57 +00:00
set(Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS "")
Implement a CMake build system. This is a large rework of my first attempt at this (#459). This implementation calls into the recently implemented python scripts to generate the necessary generated ``.h`` and ``.cpp`` files but is independent from Python building system otherwise. Unlike the Python build system, the generated files are emitted into the build tree to avoid polluting the source tree. The build system is setup to refuse to configure if it detects generated files in the source tree. If your source tree is dirty you can run ``git clean -fx`` to clean your working directory. Currently the build succeeds on Linux using CMake 3.4.3 using the "Unix Makefiles" generator with gcc or clang. The following notable features are implemented: * Building of the C and C++ examples and the ``test-z3`` executable. These are included from the ``all`` target so you have to tell the build system (e.g. make) to build them manually. * Install (``make install``) and uninstall (``make uninstall``) of libz3 and its header files. This supports ``DESTDIR`` out of the box because CMake supports it. * An option (``BUILD_LIBZ3_SHARED``) to build libz3 as a static or dynamic library. * Support for using/not using OpenMP (``USE_OPENMP``) * Support for using/not using libgmp (``USE_LIB_GMP``) * Setting the SOVERSION for libz3. I'm not sure if I'm setting the * number correctly though. This is required by Linux distrubtions that wills ship libz3. This needs discussion. The following notable features are currently not implemented and are left for future work. * Support for ARM. * Support for the foci2 library. * Support for creating/installing/uninstalling the dotnet, java, python and ml bindings. * Full support for MSVC. Although I've tried to write the CMake code with MSVC in mind not all the correct flags are passed to it. * Support for using the git hash. This new build system has several advantages other the old build system. * It is easier for outside contributors to contribute to Z3 when the build system is something more standard. * Incremental builds work properly. With the old build system when new code is pulled down the old build directory would need to thrown out and a new fresh build had to be performed because the build system didn't know how to correctly rebuild the project (e.g. couldn't handle new sources being added/removed, compiler flags changing, generated files changing, etc...). This is a MASSIVE boost to productivity! * We now have access rich array of features that CMake provides for building C/C++ projects. This means less time spent implementing custom build system logic in Python that is already supported by CMake. * CMake supports many IDEs out of the box so it should be fairly straight forward to build Z3 with Visual Studio (once support for MSVC is added), Xcode, Eclipse CDT, CLion, ..etc.
2016-02-20 23:21:00 +00:00
################################################################################
# Build type
################################################################################
message(STATUS "CMake generator: ${CMAKE_GENERATOR}")
[CMake] Report the various values of CMAKE_CXX_FLAGS, CMAKE_CXX_FLAGS_<CONFIG>, CMAKE_<TYPE>_LINKER_FLAGS, and CMAKE_<TYPE>_LINKER_FLAGS_<CONFIG>. This is useful for debugging where some flags come from. Now that we don't explicitly set the defaults it useful to see which default values we are getting from CMake.
2017-04-28 21:30:36 +01:00
set(available_build_types Debug Release RelWithDebInfo MinSizeRel)
Implement a CMake build system. This is a large rework of my first attempt at this (#459). This implementation calls into the recently implemented python scripts to generate the necessary generated ``.h`` and ``.cpp`` files but is independent from Python building system otherwise. Unlike the Python build system, the generated files are emitted into the build tree to avoid polluting the source tree. The build system is setup to refuse to configure if it detects generated files in the source tree. If your source tree is dirty you can run ``git clean -fx`` to clean your working directory. Currently the build succeeds on Linux using CMake 3.4.3 using the "Unix Makefiles" generator with gcc or clang. The following notable features are implemented: * Building of the C and C++ examples and the ``test-z3`` executable. These are included from the ``all`` target so you have to tell the build system (e.g. make) to build them manually. * Install (``make install``) and uninstall (``make uninstall``) of libz3 and its header files. This supports ``DESTDIR`` out of the box because CMake supports it. * An option (``BUILD_LIBZ3_SHARED``) to build libz3 as a static or dynamic library. * Support for using/not using OpenMP (``USE_OPENMP``) * Support for using/not using libgmp (``USE_LIB_GMP``) * Setting the SOVERSION for libz3. I'm not sure if I'm setting the * number correctly though. This is required by Linux distrubtions that wills ship libz3. This needs discussion. The following notable features are currently not implemented and are left for future work. * Support for ARM. * Support for the foci2 library. * Support for creating/installing/uninstalling the dotnet, java, python and ml bindings. * Full support for MSVC. Although I've tried to write the CMake code with MSVC in mind not all the correct flags are passed to it. * Support for using the git hash. This new build system has several advantages other the old build system. * It is easier for outside contributors to contribute to Z3 when the build system is something more standard. * Incremental builds work properly. With the old build system when new code is pulled down the old build directory would need to thrown out and a new fresh build had to be performed because the build system didn't know how to correctly rebuild the project (e.g. couldn't handle new sources being added/removed, compiler flags changing, generated files changing, etc...). This is a MASSIVE boost to productivity! * We now have access rich array of features that CMake provides for building C/C++ projects. This means less time spent implementing custom build system logic in Python that is already supported by CMake. * CMake supports many IDEs out of the box so it should be fairly straight forward to build Z3 with Visual Studio (once support for MSVC is added), Xcode, Eclipse CDT, CLion, ..etc.
2016-02-20 23:21:00 +00:00
if (DEFINED CMAKE_CONFIGURATION_TYPES)
# Multi-configuration build (e.g. Visual Studio and Xcode). Here
# CMAKE_BUILD_TYPE doesn't matter
message(STATUS "Available configurations: ${CMAKE_CONFIGURATION_TYPES}")
else()
# Single configuration generator (e.g. Unix Makefiles, Ninja)
if(NOT CMAKE_BUILD_TYPE)
message(STATUS "CMAKE_BUILD_TYPE is not set. Setting default")
message(STATUS "The available build types are: ${available_build_types}")
Correcting 'String' to 'STRING' to resolve CMake warning (#5091) Signed-off-by: Andrew V. Jones <andrewvaughanj@gmail.com>
2021-03-09 23:14:57 +00:00
set(CMAKE_BUILD_TYPE RelWithDebInfo CACHE STRING
[CMake] Fix incorrect variable name.
2016-03-08 16:14:18 +00:00
"Options are ${available_build_types}"
Implement a CMake build system. This is a large rework of my first attempt at this (#459). This implementation calls into the recently implemented python scripts to generate the necessary generated ``.h`` and ``.cpp`` files but is independent from Python building system otherwise. Unlike the Python build system, the generated files are emitted into the build tree to avoid polluting the source tree. The build system is setup to refuse to configure if it detects generated files in the source tree. If your source tree is dirty you can run ``git clean -fx`` to clean your working directory. Currently the build succeeds on Linux using CMake 3.4.3 using the "Unix Makefiles" generator with gcc or clang. The following notable features are implemented: * Building of the C and C++ examples and the ``test-z3`` executable. These are included from the ``all`` target so you have to tell the build system (e.g. make) to build them manually. * Install (``make install``) and uninstall (``make uninstall``) of libz3 and its header files. This supports ``DESTDIR`` out of the box because CMake supports it. * An option (``BUILD_LIBZ3_SHARED``) to build libz3 as a static or dynamic library. * Support for using/not using OpenMP (``USE_OPENMP``) * Support for using/not using libgmp (``USE_LIB_GMP``) * Setting the SOVERSION for libz3. I'm not sure if I'm setting the * number correctly though. This is required by Linux distrubtions that wills ship libz3. This needs discussion. The following notable features are currently not implemented and are left for future work. * Support for ARM. * Support for the foci2 library. * Support for creating/installing/uninstalling the dotnet, java, python and ml bindings. * Full support for MSVC. Although I've tried to write the CMake code with MSVC in mind not all the correct flags are passed to it. * Support for using the git hash. This new build system has several advantages other the old build system. * It is easier for outside contributors to contribute to Z3 when the build system is something more standard. * Incremental builds work properly. With the old build system when new code is pulled down the old build directory would need to thrown out and a new fresh build had to be performed because the build system didn't know how to correctly rebuild the project (e.g. couldn't handle new sources being added/removed, compiler flags changing, generated files changing, etc...). This is a MASSIVE boost to productivity! * We now have access rich array of features that CMake provides for building C/C++ projects. This means less time spent implementing custom build system logic in Python that is already supported by CMake. * CMake supports many IDEs out of the box so it should be fairly straight forward to build Z3 with Visual Studio (once support for MSVC is added), Xcode, Eclipse CDT, CLion, ..etc.
2016-02-20 23:21:00 +00:00
FORCE)
# Provide drop down menu options in cmake-gui
set_property(CACHE CMAKE_BUILD_TYPE PROPERTY STRINGS ${available_build_types})
endif()
message(STATUS "Build type: ${CMAKE_BUILD_TYPE}")
[CMake] For single configuration generators only allow `CMAKE_BUILD_TYPE` to be one of the pre-defined build configurations that we support.
2017-03-02 21:18:54 +00:00
# Check the selected build type is valid
list(FIND available_build_types "${CMAKE_BUILD_TYPE}" _build_type_index)
if ("${_build_type_index}" EQUAL "-1")
message(FATAL_ERROR "\"${CMAKE_BUILD_TYPE}\" is an invalid build type.\n"
"Use one of the following build types ${available_build_types}")
endif()
Implement a CMake build system. This is a large rework of my first attempt at this (#459). This implementation calls into the recently implemented python scripts to generate the necessary generated ``.h`` and ``.cpp`` files but is independent from Python building system otherwise. Unlike the Python build system, the generated files are emitted into the build tree to avoid polluting the source tree. The build system is setup to refuse to configure if it detects generated files in the source tree. If your source tree is dirty you can run ``git clean -fx`` to clean your working directory. Currently the build succeeds on Linux using CMake 3.4.3 using the "Unix Makefiles" generator with gcc or clang. The following notable features are implemented: * Building of the C and C++ examples and the ``test-z3`` executable. These are included from the ``all`` target so you have to tell the build system (e.g. make) to build them manually. * Install (``make install``) and uninstall (``make uninstall``) of libz3 and its header files. This supports ``DESTDIR`` out of the box because CMake supports it. * An option (``BUILD_LIBZ3_SHARED``) to build libz3 as a static or dynamic library. * Support for using/not using OpenMP (``USE_OPENMP``) * Support for using/not using libgmp (``USE_LIB_GMP``) * Setting the SOVERSION for libz3. I'm not sure if I'm setting the * number correctly though. This is required by Linux distrubtions that wills ship libz3. This needs discussion. The following notable features are currently not implemented and are left for future work. * Support for ARM. * Support for the foci2 library. * Support for creating/installing/uninstalling the dotnet, java, python and ml bindings. * Full support for MSVC. Although I've tried to write the CMake code with MSVC in mind not all the correct flags are passed to it. * Support for using the git hash. This new build system has several advantages other the old build system. * It is easier for outside contributors to contribute to Z3 when the build system is something more standard. * Incremental builds work properly. With the old build system when new code is pulled down the old build directory would need to thrown out and a new fresh build had to be performed because the build system didn't know how to correctly rebuild the project (e.g. couldn't handle new sources being added/removed, compiler flags changing, generated files changing, etc...). This is a MASSIVE boost to productivity! * We now have access rich array of features that CMake provides for building C/C++ projects. This means less time spent implementing custom build system logic in Python that is already supported by CMake. * CMake supports many IDEs out of the box so it should be fairly straight forward to build Z3 with Visual Studio (once support for MSVC is added), Xcode, Eclipse CDT, CLion, ..etc.
2016-02-20 23:21:00 +00:00
endif()
# CMAKE_BUILD_TYPE has no meaning for multi-configuration generators
# (e.g. Visual Studio) so use generator expressions instead to add
# the right definitions when doing a particular build type.
#
# Note for some reason we have to leave off ``-D`` here otherwise
# we get ``-D-DZ3DEBUG`` passed to the compiler
list(APPEND Z3_COMPONENT_CXX_DEFINES $<$<CONFIG:Debug>:Z3DEBUG>)
list(APPEND Z3_COMPONENT_CXX_DEFINES $<$<CONFIG:Release>:_EXTERNAL_RELEASE>)
list(APPEND Z3_COMPONENT_CXX_DEFINES $<$<CONFIG:RelWithDebInfo>:_EXTERNAL_RELEASE>)
################################################################################
# Find Python
################################################################################
cmake: Use `FindPython3`. (#7019) `FindPythonInterp` has been deprecated for a long time and is more verbal about that deprecation now. The build system no longer uses `PYTHON_EXECUTABLE` but instead uses `Python3_EXECUTABLE`.
2023-11-27 17:20:21 +07:00
find_package(Python3 REQUIRED COMPONENTS Interpreter)
message(STATUS "Python3_EXECUTABLE: ${Python3_EXECUTABLE}")
Implement a CMake build system. This is a large rework of my first attempt at this (#459). This implementation calls into the recently implemented python scripts to generate the necessary generated ``.h`` and ``.cpp`` files but is independent from Python building system otherwise. Unlike the Python build system, the generated files are emitted into the build tree to avoid polluting the source tree. The build system is setup to refuse to configure if it detects generated files in the source tree. If your source tree is dirty you can run ``git clean -fx`` to clean your working directory. Currently the build succeeds on Linux using CMake 3.4.3 using the "Unix Makefiles" generator with gcc or clang. The following notable features are implemented: * Building of the C and C++ examples and the ``test-z3`` executable. These are included from the ``all`` target so you have to tell the build system (e.g. make) to build them manually. * Install (``make install``) and uninstall (``make uninstall``) of libz3 and its header files. This supports ``DESTDIR`` out of the box because CMake supports it. * An option (``BUILD_LIBZ3_SHARED``) to build libz3 as a static or dynamic library. * Support for using/not using OpenMP (``USE_OPENMP``) * Support for using/not using libgmp (``USE_LIB_GMP``) * Setting the SOVERSION for libz3. I'm not sure if I'm setting the * number correctly though. This is required by Linux distrubtions that wills ship libz3. This needs discussion. The following notable features are currently not implemented and are left for future work. * Support for ARM. * Support for the foci2 library. * Support for creating/installing/uninstalling the dotnet, java, python and ml bindings. * Full support for MSVC. Although I've tried to write the CMake code with MSVC in mind not all the correct flags are passed to it. * Support for using the git hash. This new build system has several advantages other the old build system. * It is easier for outside contributors to contribute to Z3 when the build system is something more standard. * Incremental builds work properly. With the old build system when new code is pulled down the old build directory would need to thrown out and a new fresh build had to be performed because the build system didn't know how to correctly rebuild the project (e.g. couldn't handle new sources being added/removed, compiler flags changing, generated files changing, etc...). This is a MASSIVE boost to productivity! * We now have access rich array of features that CMake provides for building C/C++ projects. This means less time spent implementing custom build system logic in Python that is already supported by CMake. * CMake supports many IDEs out of the box so it should be fairly straight forward to build Z3 with Visual Studio (once support for MSVC is added), Xcode, Eclipse CDT, CLion, ..etc.
2016-02-20 23:21:00 +00:00
################################################################################
# Target architecture detection
################################################################################
Change from BINARY_DIR to PROJECT_BINARY_DIR
2019-05-15 11:25:40 -07:00
include(${PROJECT_SOURCE_DIR}/cmake/target_arch_detect.cmake)
Implement a CMake build system. This is a large rework of my first attempt at this (#459). This implementation calls into the recently implemented python scripts to generate the necessary generated ``.h`` and ``.cpp`` files but is independent from Python building system otherwise. Unlike the Python build system, the generated files are emitted into the build tree to avoid polluting the source tree. The build system is setup to refuse to configure if it detects generated files in the source tree. If your source tree is dirty you can run ``git clean -fx`` to clean your working directory. Currently the build succeeds on Linux using CMake 3.4.3 using the "Unix Makefiles" generator with gcc or clang. The following notable features are implemented: * Building of the C and C++ examples and the ``test-z3`` executable. These are included from the ``all`` target so you have to tell the build system (e.g. make) to build them manually. * Install (``make install``) and uninstall (``make uninstall``) of libz3 and its header files. This supports ``DESTDIR`` out of the box because CMake supports it. * An option (``BUILD_LIBZ3_SHARED``) to build libz3 as a static or dynamic library. * Support for using/not using OpenMP (``USE_OPENMP``) * Support for using/not using libgmp (``USE_LIB_GMP``) * Setting the SOVERSION for libz3. I'm not sure if I'm setting the * number correctly though. This is required by Linux distrubtions that wills ship libz3. This needs discussion. The following notable features are currently not implemented and are left for future work. * Support for ARM. * Support for the foci2 library. * Support for creating/installing/uninstalling the dotnet, java, python and ml bindings. * Full support for MSVC. Although I've tried to write the CMake code with MSVC in mind not all the correct flags are passed to it. * Support for using the git hash. This new build system has several advantages other the old build system. * It is easier for outside contributors to contribute to Z3 when the build system is something more standard. * Incremental builds work properly. With the old build system when new code is pulled down the old build directory would need to thrown out and a new fresh build had to be performed because the build system didn't know how to correctly rebuild the project (e.g. couldn't handle new sources being added/removed, compiler flags changing, generated files changing, etc...). This is a MASSIVE boost to productivity! * We now have access rich array of features that CMake provides for building C/C++ projects. This means less time spent implementing custom build system logic in Python that is already supported by CMake. * CMake supports many IDEs out of the box so it should be fairly straight forward to build Z3 with Visual Studio (once support for MSVC is added), Xcode, Eclipse CDT, CLion, ..etc.
2016-02-20 23:21:00 +00:00
detect_target_architecture(TARGET_ARCHITECTURE)
message(STATUS "Detected target architecture: ${TARGET_ARCHITECTURE}")
################################################################################
# Function for detecting C++ compiler flag support
################################################################################
Change from BINARY_DIR to PROJECT_BINARY_DIR
2019-05-15 11:25:40 -07:00
include(${PROJECT_SOURCE_DIR}/cmake/z3_add_cxx_flag.cmake)
Implement a CMake build system. This is a large rework of my first attempt at this (#459). This implementation calls into the recently implemented python scripts to generate the necessary generated ``.h`` and ``.cpp`` files but is independent from Python building system otherwise. Unlike the Python build system, the generated files are emitted into the build tree to avoid polluting the source tree. The build system is setup to refuse to configure if it detects generated files in the source tree. If your source tree is dirty you can run ``git clean -fx`` to clean your working directory. Currently the build succeeds on Linux using CMake 3.4.3 using the "Unix Makefiles" generator with gcc or clang. The following notable features are implemented: * Building of the C and C++ examples and the ``test-z3`` executable. These are included from the ``all`` target so you have to tell the build system (e.g. make) to build them manually. * Install (``make install``) and uninstall (``make uninstall``) of libz3 and its header files. This supports ``DESTDIR`` out of the box because CMake supports it. * An option (``BUILD_LIBZ3_SHARED``) to build libz3 as a static or dynamic library. * Support for using/not using OpenMP (``USE_OPENMP``) * Support for using/not using libgmp (``USE_LIB_GMP``) * Setting the SOVERSION for libz3. I'm not sure if I'm setting the * number correctly though. This is required by Linux distrubtions that wills ship libz3. This needs discussion. The following notable features are currently not implemented and are left for future work. * Support for ARM. * Support for the foci2 library. * Support for creating/installing/uninstalling the dotnet, java, python and ml bindings. * Full support for MSVC. Although I've tried to write the CMake code with MSVC in mind not all the correct flags are passed to it. * Support for using the git hash. This new build system has several advantages other the old build system. * It is easier for outside contributors to contribute to Z3 when the build system is something more standard. * Incremental builds work properly. With the old build system when new code is pulled down the old build directory would need to thrown out and a new fresh build had to be performed because the build system didn't know how to correctly rebuild the project (e.g. couldn't handle new sources being added/removed, compiler flags changing, generated files changing, etc...). This is a MASSIVE boost to productivity! * We now have access rich array of features that CMake provides for building C/C++ projects. This means less time spent implementing custom build system logic in Python that is already supported by CMake. * CMake supports many IDEs out of the box so it should be fairly straight forward to build Z3 with Visual Studio (once support for MSVC is added), Xcode, Eclipse CDT, CLion, ..etc.
2016-02-20 23:21:00 +00:00
add configuration per Dan Liew's comment Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-08 10:02:09 -07:00
################################################################################
# C++ language version
################################################################################
update to c++20, remove debug output Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-09-22 21:30:44 +01:00
set(CMAKE_CXX_STANDARD 20)
remove stale config #2318 thanks @ekpyron Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-07 17:08:22 -07:00
set(CMAKE_CXX_STANDARD_REQUIRED ON)
add configuration per Dan Liew's comment Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-08 10:02:09 -07:00
Implement a CMake build system. This is a large rework of my first attempt at this (#459). This implementation calls into the recently implemented python scripts to generate the necessary generated ``.h`` and ``.cpp`` files but is independent from Python building system otherwise. Unlike the Python build system, the generated files are emitted into the build tree to avoid polluting the source tree. The build system is setup to refuse to configure if it detects generated files in the source tree. If your source tree is dirty you can run ``git clean -fx`` to clean your working directory. Currently the build succeeds on Linux using CMake 3.4.3 using the "Unix Makefiles" generator with gcc or clang. The following notable features are implemented: * Building of the C and C++ examples and the ``test-z3`` executable. These are included from the ``all`` target so you have to tell the build system (e.g. make) to build them manually. * Install (``make install``) and uninstall (``make uninstall``) of libz3 and its header files. This supports ``DESTDIR`` out of the box because CMake supports it. * An option (``BUILD_LIBZ3_SHARED``) to build libz3 as a static or dynamic library. * Support for using/not using OpenMP (``USE_OPENMP``) * Support for using/not using libgmp (``USE_LIB_GMP``) * Setting the SOVERSION for libz3. I'm not sure if I'm setting the * number correctly though. This is required by Linux distrubtions that wills ship libz3. This needs discussion. The following notable features are currently not implemented and are left for future work. * Support for ARM. * Support for the foci2 library. * Support for creating/installing/uninstalling the dotnet, java, python and ml bindings. * Full support for MSVC. Although I've tried to write the CMake code with MSVC in mind not all the correct flags are passed to it. * Support for using the git hash. This new build system has several advantages other the old build system. * It is easier for outside contributors to contribute to Z3 when the build system is something more standard. * Incremental builds work properly. With the old build system when new code is pulled down the old build directory would need to thrown out and a new fresh build had to be performed because the build system didn't know how to correctly rebuild the project (e.g. couldn't handle new sources being added/removed, compiler flags changing, generated files changing, etc...). This is a MASSIVE boost to productivity! * We now have access rich array of features that CMake provides for building C/C++ projects. This means less time spent implementing custom build system logic in Python that is already supported by CMake. * CMake supports many IDEs out of the box so it should be fairly straight forward to build Z3 with Visual Studio (once support for MSVC is added), Xcode, Eclipse CDT, CLion, ..etc.
2016-02-20 23:21:00 +00:00
################################################################################
# Platform detection
################################################################################
Remove all per-OS defines apart from _WINDOWS. These are all unused and shouldn't be needed. Mostly we need something for differentiating between POSIX and non-POSIX (until we can reduce some of those differences as well). We shouldn't need to modify the build system to build on a new OS if it is basically a Unix and is supported by cmake.
2022-08-03 15:21:23 +07:00
if (CMAKE_SYSTEM_NAME STREQUAL "Darwin")
set ARM64 if detected under OSX
2022-04-07 08:35:45 +02:00
if (TARGET_ARCHITECTURE STREQUAL "arm64")
set(CMAKE_OSX_ARCHITECTURES "arm64")
endif()
Implement a CMake build system. This is a large rework of my first attempt at this (#459). This implementation calls into the recently implemented python scripts to generate the necessary generated ``.h`` and ``.cpp`` files but is independent from Python building system otherwise. Unlike the Python build system, the generated files are emitted into the build tree to avoid polluting the source tree. The build system is setup to refuse to configure if it detects generated files in the source tree. If your source tree is dirty you can run ``git clean -fx`` to clean your working directory. Currently the build succeeds on Linux using CMake 3.4.3 using the "Unix Makefiles" generator with gcc or clang. The following notable features are implemented: * Building of the C and C++ examples and the ``test-z3`` executable. These are included from the ``all`` target so you have to tell the build system (e.g. make) to build them manually. * Install (``make install``) and uninstall (``make uninstall``) of libz3 and its header files. This supports ``DESTDIR`` out of the box because CMake supports it. * An option (``BUILD_LIBZ3_SHARED``) to build libz3 as a static or dynamic library. * Support for using/not using OpenMP (``USE_OPENMP``) * Support for using/not using libgmp (``USE_LIB_GMP``) * Setting the SOVERSION for libz3. I'm not sure if I'm setting the * number correctly though. This is required by Linux distrubtions that wills ship libz3. This needs discussion. The following notable features are currently not implemented and are left for future work. * Support for ARM. * Support for the foci2 library. * Support for creating/installing/uninstalling the dotnet, java, python and ml bindings. * Full support for MSVC. Although I've tried to write the CMake code with MSVC in mind not all the correct flags are passed to it. * Support for using the git hash. This new build system has several advantages other the old build system. * It is easier for outside contributors to contribute to Z3 when the build system is something more standard. * Incremental builds work properly. With the old build system when new code is pulled down the old build directory would need to thrown out and a new fresh build had to be performed because the build system didn't know how to correctly rebuild the project (e.g. couldn't handle new sources being added/removed, compiler flags changing, generated files changing, etc...). This is a MASSIVE boost to productivity! * We now have access rich array of features that CMake provides for building C/C++ projects. This means less time spent implementing custom build system logic in Python that is already supported by CMake. * CMake supports many IDEs out of the box so it should be fairly straight forward to build Z3 with Visual Studio (once support for MSVC is added), Xcode, Eclipse CDT, CLion, ..etc.
2016-02-20 23:21:00 +00:00
elseif (WIN32)
message(STATUS "Platform: Windows")
list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_WINDOWS")
fixes for #7420 #7405
2024-10-13 15:52:13 -07:00
# workaround for #7420
list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_DISABLE_CONSTEXPR_MUTEX_CONSTRUCTOR")
Allow emscripten builds.
2018-12-26 23:01:20 -05:00
elseif (EMSCRIPTEN)
message(STATUS "Platform: Emscripten")
list(APPEND Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS
"-Os"
"-s ALLOW_MEMORY_GROWTH=1"
"-s ASSERTIONS=0"
"-s DISABLE_EXCEPTION_CATCHING=0"
"-s ERROR_ON_UNDEFINED_SYMBOLS=1"
)
Implement a CMake build system. This is a large rework of my first attempt at this (#459). This implementation calls into the recently implemented python scripts to generate the necessary generated ``.h`` and ``.cpp`` files but is independent from Python building system otherwise. Unlike the Python build system, the generated files are emitted into the build tree to avoid polluting the source tree. The build system is setup to refuse to configure if it detects generated files in the source tree. If your source tree is dirty you can run ``git clean -fx`` to clean your working directory. Currently the build succeeds on Linux using CMake 3.4.3 using the "Unix Makefiles" generator with gcc or clang. The following notable features are implemented: * Building of the C and C++ examples and the ``test-z3`` executable. These are included from the ``all`` target so you have to tell the build system (e.g. make) to build them manually. * Install (``make install``) and uninstall (``make uninstall``) of libz3 and its header files. This supports ``DESTDIR`` out of the box because CMake supports it. * An option (``BUILD_LIBZ3_SHARED``) to build libz3 as a static or dynamic library. * Support for using/not using OpenMP (``USE_OPENMP``) * Support for using/not using libgmp (``USE_LIB_GMP``) * Setting the SOVERSION for libz3. I'm not sure if I'm setting the * number correctly though. This is required by Linux distrubtions that wills ship libz3. This needs discussion. The following notable features are currently not implemented and are left for future work. * Support for ARM. * Support for the foci2 library. * Support for creating/installing/uninstalling the dotnet, java, python and ml bindings. * Full support for MSVC. Although I've tried to write the CMake code with MSVC in mind not all the correct flags are passed to it. * Support for using the git hash. This new build system has several advantages other the old build system. * It is easier for outside contributors to contribute to Z3 when the build system is something more standard. * Incremental builds work properly. With the old build system when new code is pulled down the old build directory would need to thrown out and a new fresh build had to be performed because the build system didn't know how to correctly rebuild the project (e.g. couldn't handle new sources being added/removed, compiler flags changing, generated files changing, etc...). This is a MASSIVE boost to productivity! * We now have access rich array of features that CMake provides for building C/C++ projects. This means less time spent implementing custom build system logic in Python that is already supported by CMake. * CMake supports many IDEs out of the box so it should be fairly straight forward to build Z3 with Visual Studio (once support for MSVC is added), Xcode, Eclipse CDT, CLion, ..etc.
2016-02-20 23:21:00 +00:00
endif()
Fix build on Mac (#6146) * Fix finding Python on Mac On Mac you have to specify the version. It also works well on other platforms this way. * Ignore CMake build directories from index * Fix warning about unused variable in release The variable is used in debug only, but it's legit that the compiler does not warn us for that in release.
2022-07-11 18:46:23 +02:00
list(APPEND Z3_COMPONENT_EXTRA_INCLUDE_DIRS
Change from BINARY_DIR to PROJECT_BINARY_DIR
2019-05-15 11:25:40 -07:00
"${PROJECT_BINARY_DIR}/src"
"${PROJECT_SOURCE_DIR}/src"
updated include directives Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-08-01 10:51:47 -07:00
)
[CMake] Fix #1437. The `clock_gettime()` function in glibc < 2.17 required linking against librt. Until #1437 nobody had tried using the CMake build system with a really old version of glibc (in this case 2.12). The python build system always linked against librt but the CMake build system never tried to link against it leading to link failures. This patch teaches the CMake build system to detect if librt is required when linking against `clock_gettime()` and adds `rt` as a link dependency if necessary.
2018-01-03 12:42:43 +00:00
Implement a CMake build system. This is a large rework of my first attempt at this (#459). This implementation calls into the recently implemented python scripts to generate the necessary generated ``.h`` and ``.cpp`` files but is independent from Python building system otherwise. Unlike the Python build system, the generated files are emitted into the build tree to avoid polluting the source tree. The build system is setup to refuse to configure if it detects generated files in the source tree. If your source tree is dirty you can run ``git clean -fx`` to clean your working directory. Currently the build succeeds on Linux using CMake 3.4.3 using the "Unix Makefiles" generator with gcc or clang. The following notable features are implemented: * Building of the C and C++ examples and the ``test-z3`` executable. These are included from the ``all`` target so you have to tell the build system (e.g. make) to build them manually. * Install (``make install``) and uninstall (``make uninstall``) of libz3 and its header files. This supports ``DESTDIR`` out of the box because CMake supports it. * An option (``BUILD_LIBZ3_SHARED``) to build libz3 as a static or dynamic library. * Support for using/not using OpenMP (``USE_OPENMP``) * Support for using/not using libgmp (``USE_LIB_GMP``) * Setting the SOVERSION for libz3. I'm not sure if I'm setting the * number correctly though. This is required by Linux distrubtions that wills ship libz3. This needs discussion. The following notable features are currently not implemented and are left for future work. * Support for ARM. * Support for the foci2 library. * Support for creating/installing/uninstalling the dotnet, java, python and ml bindings. * Full support for MSVC. Although I've tried to write the CMake code with MSVC in mind not all the correct flags are passed to it. * Support for using the git hash. This new build system has several advantages other the old build system. * It is easier for outside contributors to contribute to Z3 when the build system is something more standard. * Incremental builds work properly. With the old build system when new code is pulled down the old build directory would need to thrown out and a new fresh build had to be performed because the build system didn't know how to correctly rebuild the project (e.g. couldn't handle new sources being added/removed, compiler flags changing, generated files changing, etc...). This is a MASSIVE boost to productivity! * We now have access rich array of features that CMake provides for building C/C++ projects. This means less time spent implementing custom build system logic in Python that is already supported by CMake. * CMake supports many IDEs out of the box so it should be fairly straight forward to build Z3 with Visual Studio (once support for MSVC is added), Xcode, Eclipse CDT, CLion, ..etc.
2016-02-20 23:21:00 +00:00
################################################################################
# GNU multiple precision library support
################################################################################
rename additional build options #2709 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-11-18 21:07:12 -08:00
option(Z3_USE_LIB_GMP "Use GNU Multiple Precision Library" OFF)
if (Z3_USE_LIB_GMP)
Implement a CMake build system. This is a large rework of my first attempt at this (#459). This implementation calls into the recently implemented python scripts to generate the necessary generated ``.h`` and ``.cpp`` files but is independent from Python building system otherwise. Unlike the Python build system, the generated files are emitted into the build tree to avoid polluting the source tree. The build system is setup to refuse to configure if it detects generated files in the source tree. If your source tree is dirty you can run ``git clean -fx`` to clean your working directory. Currently the build succeeds on Linux using CMake 3.4.3 using the "Unix Makefiles" generator with gcc or clang. The following notable features are implemented: * Building of the C and C++ examples and the ``test-z3`` executable. These are included from the ``all`` target so you have to tell the build system (e.g. make) to build them manually. * Install (``make install``) and uninstall (``make uninstall``) of libz3 and its header files. This supports ``DESTDIR`` out of the box because CMake supports it. * An option (``BUILD_LIBZ3_SHARED``) to build libz3 as a static or dynamic library. * Support for using/not using OpenMP (``USE_OPENMP``) * Support for using/not using libgmp (``USE_LIB_GMP``) * Setting the SOVERSION for libz3. I'm not sure if I'm setting the * number correctly though. This is required by Linux distrubtions that wills ship libz3. This needs discussion. The following notable features are currently not implemented and are left for future work. * Support for ARM. * Support for the foci2 library. * Support for creating/installing/uninstalling the dotnet, java, python and ml bindings. * Full support for MSVC. Although I've tried to write the CMake code with MSVC in mind not all the correct flags are passed to it. * Support for using the git hash. This new build system has several advantages other the old build system. * It is easier for outside contributors to contribute to Z3 when the build system is something more standard. * Incremental builds work properly. With the old build system when new code is pulled down the old build directory would need to thrown out and a new fresh build had to be performed because the build system didn't know how to correctly rebuild the project (e.g. couldn't handle new sources being added/removed, compiler flags changing, generated files changing, etc...). This is a MASSIVE boost to productivity! * We now have access rich array of features that CMake provides for building C/C++ projects. This means less time spent implementing custom build system logic in Python that is already supported by CMake. * CMake supports many IDEs out of the box so it should be fairly straight forward to build Z3 with Visual Studio (once support for MSVC is added), Xcode, Eclipse CDT, CLion, ..etc.
2016-02-20 23:21:00 +00:00
# Because this is off by default we will make the configure fail if libgmp
# can't be found
find_package(GMP REQUIRED)
message(STATUS "Using libgmp")
clean up CMake code (#5182) * CMake: simplify FindGMP.cmake Remove printing of all the different variables, and let FPHSA output the library name. Add an imported target, which bundles the library and the include directories for easier usage. * fix build: vector::c_ptr() now is vector::data() * CMake: use Threads::Threads imported module Otherwise the setting of THREADS_PREFER_PTHREAD_FLAG has no effect. * CMake: remove needless policy setting The minimum required version is CMake 3.4, where these policies are already set to new because they were introduced earlier. * CMake: remove needless variable expansion
2021-04-14 19:29:15 +02:00
list(APPEND Z3_DEPENDENT_LIBS GMP::GMP)
Implement a CMake build system. This is a large rework of my first attempt at this (#459). This implementation calls into the recently implemented python scripts to generate the necessary generated ``.h`` and ``.cpp`` files but is independent from Python building system otherwise. Unlike the Python build system, the generated files are emitted into the build tree to avoid polluting the source tree. The build system is setup to refuse to configure if it detects generated files in the source tree. If your source tree is dirty you can run ``git clean -fx`` to clean your working directory. Currently the build succeeds on Linux using CMake 3.4.3 using the "Unix Makefiles" generator with gcc or clang. The following notable features are implemented: * Building of the C and C++ examples and the ``test-z3`` executable. These are included from the ``all`` target so you have to tell the build system (e.g. make) to build them manually. * Install (``make install``) and uninstall (``make uninstall``) of libz3 and its header files. This supports ``DESTDIR`` out of the box because CMake supports it. * An option (``BUILD_LIBZ3_SHARED``) to build libz3 as a static or dynamic library. * Support for using/not using OpenMP (``USE_OPENMP``) * Support for using/not using libgmp (``USE_LIB_GMP``) * Setting the SOVERSION for libz3. I'm not sure if I'm setting the * number correctly though. This is required by Linux distrubtions that wills ship libz3. This needs discussion. The following notable features are currently not implemented and are left for future work. * Support for ARM. * Support for the foci2 library. * Support for creating/installing/uninstalling the dotnet, java, python and ml bindings. * Full support for MSVC. Although I've tried to write the CMake code with MSVC in mind not all the correct flags are passed to it. * Support for using the git hash. This new build system has several advantages other the old build system. * It is easier for outside contributors to contribute to Z3 when the build system is something more standard. * Incremental builds work properly. With the old build system when new code is pulled down the old build directory would need to thrown out and a new fresh build had to be performed because the build system didn't know how to correctly rebuild the project (e.g. couldn't handle new sources being added/removed, compiler flags changing, generated files changing, etc...). This is a MASSIVE boost to productivity! * We now have access rich array of features that CMake provides for building C/C++ projects. This means less time spent implementing custom build system logic in Python that is already supported by CMake. * CMake supports many IDEs out of the box so it should be fairly straight forward to build Z3 with Visual Studio (once support for MSVC is added), Xcode, Eclipse CDT, CLion, ..etc.
2016-02-20 23:21:00 +00:00
list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_MP_GMP")
else()
list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_MP_INTERNAL")
message(STATUS "Not using libgmp")
endif()
################################################################################
[CMake] Add CMake option `API_LOG_SYNC` that corresponds to the `--log-sync` option added to the python/Makefile build system added in dee7c29b19ade620d66cb8f49f3ccb8b688530ea .
2017-05-22 17:11:25 +01:00
# API Log sync
################################################################################
remove deprecated USE_OPENMP, rename API_LOG_SYNC to Z3_API_LOG_SYNC (tiny part of #2709) Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-11-18 20:24:29 -08:00
option(Z3_API_LOG_SYNC
[CMake] Add CMake option `API_LOG_SYNC` that corresponds to the `--log-sync` option added to the python/Makefile build system added in dee7c29b19ade620d66cb8f49f3ccb8b688530ea .
2017-05-22 17:11:25 +01:00
"Use locking when logging Z3 API calls (experimental)"
OFF
)
remove deprecated USE_OPENMP, rename API_LOG_SYNC to Z3_API_LOG_SYNC (tiny part of #2709) Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-11-18 20:24:29 -08:00
if (Z3_API_LOG_SYNC)
[CMake] Add CMake option `API_LOG_SYNC` that corresponds to the `--log-sync` option added to the python/Makefile build system added in dee7c29b19ade620d66cb8f49f3ccb8b688530ea .
2017-05-22 17:11:25 +01:00
list(APPEND Z3_COMPONENT_CXX_DEFINES "-DZ3_LOG_SYNC")
remove deprecated USE_OPENMP, rename API_LOG_SYNC to Z3_API_LOG_SYNC (tiny part of #2709) Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-11-18 20:24:29 -08:00
message(STATUS "Using Z3_API_LOG_SYNC")
[CMake] Add CMake option `API_LOG_SYNC` that corresponds to the `--log-sync` option added to the python/Makefile build system added in dee7c29b19ade620d66cb8f49f3ccb8b688530ea .
2017-05-22 17:11:25 +01:00
else()
rename additional build options #2709 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-11-18 20:39:04 -08:00
message(STATUS "Not using Z3_API_LOG_SYNC")
[CMake] Add CMake option `API_LOG_SYNC` that corresponds to the `--log-sync` option added to the python/Makefile build system added in dee7c29b19ade620d66cb8f49f3ccb8b688530ea .
2017-05-22 17:11:25 +01:00
endif()
cmake: addd SINGLE_THREADED option
2019-06-05 15:44:25 +01:00
################################################################################
# Thread safe or not?
################################################################################
follow up on #2737 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-11-25 08:35:28 -08:00
option(Z3_SINGLE_THREADED
cmake: addd SINGLE_THREADED option
2019-06-05 15:44:25 +01:00
"Non-thread-safe build"
OFF
)
follow up on #2737 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-11-25 08:35:28 -08:00
if (Z3_SINGLE_THREADED)
cmake: addd SINGLE_THREADED option
2019-06-05 15:44:25 +01:00
list(APPEND Z3_COMPONENT_CXX_DEFINES "-DSINGLE_THREAD")
message(STATUS "Non-thread-safe build")
else()
message(STATUS "Thread-safe build")
endif()
#7418 - circumvent use of timer threads to make WASM integration of z3 easier The scoped_timer uses a std::therad. Spawning this thread fails in cases of WASM. Instead of adapting builds and using async features at the level of WASM and the client, we expose a specialized version of z3 that doesn't use threads at all, neither for solvers nor for timers. The tradeoff is that the periodic poll that checks for timeout directly queries the global clock each time. We characterize it as based on polling.
2024-11-21 11:20:05 -08:00
################################################################################
# Use polling based timeout. This avoids spawning threads for timer tasks
################################################################################
option(Z3_POLLING_TIMER
"Use polling based timeout checks"
OFF
)
if (Z3_POLLING_TIMER)
list(APPEND Z3_COMPONENT_CXX_DEFINES "-DPOLLING_TIMER")
message(STATUS "Polling based timer")
endif()
[CMake] Add CMake option `API_LOG_SYNC` that corresponds to the `--log-sync` option added to the python/Makefile build system added in dee7c29b19ade620d66cb8f49f3ccb8b688530ea .
2017-05-22 17:11:25 +01:00
################################################################################
Implement a CMake build system. This is a large rework of my first attempt at this (#459). This implementation calls into the recently implemented python scripts to generate the necessary generated ``.h`` and ``.cpp`` files but is independent from Python building system otherwise. Unlike the Python build system, the generated files are emitted into the build tree to avoid polluting the source tree. The build system is setup to refuse to configure if it detects generated files in the source tree. If your source tree is dirty you can run ``git clean -fx`` to clean your working directory. Currently the build succeeds on Linux using CMake 3.4.3 using the "Unix Makefiles" generator with gcc or clang. The following notable features are implemented: * Building of the C and C++ examples and the ``test-z3`` executable. These are included from the ``all`` target so you have to tell the build system (e.g. make) to build them manually. * Install (``make install``) and uninstall (``make uninstall``) of libz3 and its header files. This supports ``DESTDIR`` out of the box because CMake supports it. * An option (``BUILD_LIBZ3_SHARED``) to build libz3 as a static or dynamic library. * Support for using/not using OpenMP (``USE_OPENMP``) * Support for using/not using libgmp (``USE_LIB_GMP``) * Setting the SOVERSION for libz3. I'm not sure if I'm setting the * number correctly though. This is required by Linux distrubtions that wills ship libz3. This needs discussion. The following notable features are currently not implemented and are left for future work. * Support for ARM. * Support for the foci2 library. * Support for creating/installing/uninstalling the dotnet, java, python and ml bindings. * Full support for MSVC. Although I've tried to write the CMake code with MSVC in mind not all the correct flags are passed to it. * Support for using the git hash. This new build system has several advantages other the old build system. * It is easier for outside contributors to contribute to Z3 when the build system is something more standard. * Incremental builds work properly. With the old build system when new code is pulled down the old build directory would need to thrown out and a new fresh build had to be performed because the build system didn't know how to correctly rebuild the project (e.g. couldn't handle new sources being added/removed, compiler flags changing, generated files changing, etc...). This is a MASSIVE boost to productivity! * We now have access rich array of features that CMake provides for building C/C++ projects. This means less time spent implementing custom build system logic in Python that is already supported by CMake. * CMake supports many IDEs out of the box so it should be fairly straight forward to build Z3 with Visual Studio (once support for MSVC is added), Xcode, Eclipse CDT, CLion, ..etc.
2016-02-20 23:21:00 +00:00
# FP math
################################################################################
# FIXME: Support ARM "-mfpu=vfp -mfloat-abi=hard"
clean up CMake code (#5182) * CMake: simplify FindGMP.cmake Remove printing of all the different variables, and let FPHSA output the library name. Add an imported target, which bundles the library and the include directories for easier usage. * fix build: vector::c_ptr() now is vector::data() * CMake: use Threads::Threads imported module Otherwise the setting of THREADS_PREFER_PTHREAD_FLAG has no effect. * CMake: remove needless policy setting The minimum required version is CMake 3.4, where these policies are already set to new because they were introduced earlier. * CMake: remove needless variable expansion
2021-04-14 19:29:15 +02:00
if ((TARGET_ARCHITECTURE STREQUAL "x86_64") OR (TARGET_ARCHITECTURE STREQUAL "i686"))
if ((CMAKE_CXX_COMPILER_ID MATCHES "GNU") OR (CMAKE_CXX_COMPILER_ID MATCHES "Clang") OR (CMAKE_CXX_COMPILER_ID MATCHES "Intel"))
incorporate #1854 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-10-01 19:49:18 -07:00
set(SSE_FLAGS "-mfpmath=sse" "-msse" "-msse2")
clean up CMake code (#5182) * CMake: simplify FindGMP.cmake Remove printing of all the different variables, and let FPHSA output the library name. Add an imported target, which bundles the library and the include directories for easier usage. * fix build: vector::c_ptr() now is vector::data() * CMake: use Threads::Threads imported module Otherwise the setting of THREADS_PREFER_PTHREAD_FLAG has no effect. * CMake: remove needless policy setting The minimum required version is CMake 3.4, where these policies are already set to new because they were introduced earlier. * CMake: remove needless variable expansion
2021-04-14 19:29:15 +02:00
elseif (CMAKE_CXX_COMPILER_ID STREQUAL "MSVC")
Implement a CMake build system. This is a large rework of my first attempt at this (#459). This implementation calls into the recently implemented python scripts to generate the necessary generated ``.h`` and ``.cpp`` files but is independent from Python building system otherwise. Unlike the Python build system, the generated files are emitted into the build tree to avoid polluting the source tree. The build system is setup to refuse to configure if it detects generated files in the source tree. If your source tree is dirty you can run ``git clean -fx`` to clean your working directory. Currently the build succeeds on Linux using CMake 3.4.3 using the "Unix Makefiles" generator with gcc or clang. The following notable features are implemented: * Building of the C and C++ examples and the ``test-z3`` executable. These are included from the ``all`` target so you have to tell the build system (e.g. make) to build them manually. * Install (``make install``) and uninstall (``make uninstall``) of libz3 and its header files. This supports ``DESTDIR`` out of the box because CMake supports it. * An option (``BUILD_LIBZ3_SHARED``) to build libz3 as a static or dynamic library. * Support for using/not using OpenMP (``USE_OPENMP``) * Support for using/not using libgmp (``USE_LIB_GMP``) * Setting the SOVERSION for libz3. I'm not sure if I'm setting the * number correctly though. This is required by Linux distrubtions that wills ship libz3. This needs discussion. The following notable features are currently not implemented and are left for future work. * Support for ARM. * Support for the foci2 library. * Support for creating/installing/uninstalling the dotnet, java, python and ml bindings. * Full support for MSVC. Although I've tried to write the CMake code with MSVC in mind not all the correct flags are passed to it. * Support for using the git hash. This new build system has several advantages other the old build system. * It is easier for outside contributors to contribute to Z3 when the build system is something more standard. * Incremental builds work properly. With the old build system when new code is pulled down the old build directory would need to thrown out and a new fresh build had to be performed because the build system didn't know how to correctly rebuild the project (e.g. couldn't handle new sources being added/removed, compiler flags changing, generated files changing, etc...). This is a MASSIVE boost to productivity! * We now have access rich array of features that CMake provides for building C/C++ projects. This means less time spent implementing custom build system logic in Python that is already supported by CMake. * CMake supports many IDEs out of the box so it should be fairly straight forward to build Z3 with Visual Studio (once support for MSVC is added), Xcode, Eclipse CDT, CLion, ..etc.
2016-02-20 23:21:00 +00:00
set(SSE_FLAGS "/arch:SSE2")
else()
message(FATAL_ERROR "Unknown compiler ${CMAKE_CXX_COMPILER_ID}")
endif()
CHECK_CXX_COMPILER_FLAG("${SSE_FLAGS}" HAS_SSE2)
if (HAS_SSE2)
list(APPEND Z3_COMPONENT_CXX_FLAGS ${SSE_FLAGS})
endif()
unset(SSE_FLAGS)
endif()
Try to fix the freebsd build by linking against the system's threading library.
2016-03-03 19:30:18 +00:00
################################################################################
# Threading support
################################################################################
Fix build failure on riscv64 (#4506)
2020-06-07 21:27:54 +02:00
set(THREADS_PREFER_PTHREAD_FLAG TRUE)
Try to fix the freebsd build by linking against the system's threading library.
2016-03-03 19:30:18 +00:00
find_package(Threads)
clean up CMake code (#5182) * CMake: simplify FindGMP.cmake Remove printing of all the different variables, and let FPHSA output the library name. Add an imported target, which bundles the library and the include directories for easier usage. * fix build: vector::c_ptr() now is vector::data() * CMake: use Threads::Threads imported module Otherwise the setting of THREADS_PREFER_PTHREAD_FLAG has no effect. * CMake: remove needless policy setting The minimum required version is CMake 3.4, where these policies are already set to new because they were introduced earlier. * CMake: remove needless variable expansion
2021-04-14 19:29:15 +02:00
list(APPEND Z3_DEPENDENT_LIBS Threads::Threads)
Try to fix the freebsd build by linking against the system's threading library.
2016-03-03 19:30:18 +00:00
Implement a CMake build system. This is a large rework of my first attempt at this (#459). This implementation calls into the recently implemented python scripts to generate the necessary generated ``.h`` and ``.cpp`` files but is independent from Python building system otherwise. Unlike the Python build system, the generated files are emitted into the build tree to avoid polluting the source tree. The build system is setup to refuse to configure if it detects generated files in the source tree. If your source tree is dirty you can run ``git clean -fx`` to clean your working directory. Currently the build succeeds on Linux using CMake 3.4.3 using the "Unix Makefiles" generator with gcc or clang. The following notable features are implemented: * Building of the C and C++ examples and the ``test-z3`` executable. These are included from the ``all`` target so you have to tell the build system (e.g. make) to build them manually. * Install (``make install``) and uninstall (``make uninstall``) of libz3 and its header files. This supports ``DESTDIR`` out of the box because CMake supports it. * An option (``BUILD_LIBZ3_SHARED``) to build libz3 as a static or dynamic library. * Support for using/not using OpenMP (``USE_OPENMP``) * Support for using/not using libgmp (``USE_LIB_GMP``) * Setting the SOVERSION for libz3. I'm not sure if I'm setting the * number correctly though. This is required by Linux distrubtions that wills ship libz3. This needs discussion. The following notable features are currently not implemented and are left for future work. * Support for ARM. * Support for the foci2 library. * Support for creating/installing/uninstalling the dotnet, java, python and ml bindings. * Full support for MSVC. Although I've tried to write the CMake code with MSVC in mind not all the correct flags are passed to it. * Support for using the git hash. This new build system has several advantages other the old build system. * It is easier for outside contributors to contribute to Z3 when the build system is something more standard. * Incremental builds work properly. With the old build system when new code is pulled down the old build directory would need to thrown out and a new fresh build had to be performed because the build system didn't know how to correctly rebuild the project (e.g. couldn't handle new sources being added/removed, compiler flags changing, generated files changing, etc...). This is a MASSIVE boost to productivity! * We now have access rich array of features that CMake provides for building C/C++ projects. This means less time spent implementing custom build system logic in Python that is already supported by CMake. * CMake supports many IDEs out of the box so it should be fairly straight forward to build Z3 with Visual Studio (once support for MSVC is added), Xcode, Eclipse CDT, CLion, ..etc.
2016-02-20 23:21:00 +00:00
################################################################################
# Compiler warnings
################################################################################
Change from BINARY_DIR to PROJECT_BINARY_DIR
2019-05-15 11:25:40 -07:00
include(${PROJECT_SOURCE_DIR}/cmake/compiler_warnings.cmake)
Implement a CMake build system. This is a large rework of my first attempt at this (#459). This implementation calls into the recently implemented python scripts to generate the necessary generated ``.h`` and ``.cpp`` files but is independent from Python building system otherwise. Unlike the Python build system, the generated files are emitted into the build tree to avoid polluting the source tree. The build system is setup to refuse to configure if it detects generated files in the source tree. If your source tree is dirty you can run ``git clean -fx`` to clean your working directory. Currently the build succeeds on Linux using CMake 3.4.3 using the "Unix Makefiles" generator with gcc or clang. The following notable features are implemented: * Building of the C and C++ examples and the ``test-z3`` executable. These are included from the ``all`` target so you have to tell the build system (e.g. make) to build them manually. * Install (``make install``) and uninstall (``make uninstall``) of libz3 and its header files. This supports ``DESTDIR`` out of the box because CMake supports it. * An option (``BUILD_LIBZ3_SHARED``) to build libz3 as a static or dynamic library. * Support for using/not using OpenMP (``USE_OPENMP``) * Support for using/not using libgmp (``USE_LIB_GMP``) * Setting the SOVERSION for libz3. I'm not sure if I'm setting the * number correctly though. This is required by Linux distrubtions that wills ship libz3. This needs discussion. The following notable features are currently not implemented and are left for future work. * Support for ARM. * Support for the foci2 library. * Support for creating/installing/uninstalling the dotnet, java, python and ml bindings. * Full support for MSVC. Although I've tried to write the CMake code with MSVC in mind not all the correct flags are passed to it. * Support for using the git hash. This new build system has several advantages other the old build system. * It is easier for outside contributors to contribute to Z3 when the build system is something more standard. * Incremental builds work properly. With the old build system when new code is pulled down the old build directory would need to thrown out and a new fresh build had to be performed because the build system didn't know how to correctly rebuild the project (e.g. couldn't handle new sources being added/removed, compiler flags changing, generated files changing, etc...). This is a MASSIVE boost to productivity! * We now have access rich array of features that CMake provides for building C/C++ projects. This means less time spent implementing custom build system logic in Python that is already supported by CMake. * CMake supports many IDEs out of the box so it should be fairly straight forward to build Z3 with Visual Studio (once support for MSVC is added), Xcode, Eclipse CDT, CLion, ..etc.
2016-02-20 23:21:00 +00:00
add cmake option to turn on asan
2025-01-28 15:01:31 -08:00
################################################################################
# Address sanitization
################################################################################
option(Z3_ADDRESS_SANITIZE "Set address sanitization." OFF)
if (Z3_ADDRESS_SANITIZE)
z3_add_cxx_flag("-fsanitize=address" REQUIRED)
endif()
cmake: Allow saving clang's optimization records. This gives some insight into what the compiler has decided to do or not do.
2018-11-30 19:52:57 +07:00
################################################################################
# Save Clang optimization records
################################################################################
follow up on #2737 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-11-25 08:35:28 -08:00
option(Z3_SAVE_CLANG_OPTIMIZATION_RECORDS "Enable saving Clang optimization records." OFF)
cmake: Allow saving clang's optimization records. This gives some insight into what the compiler has decided to do or not do.
2018-11-30 19:52:57 +07:00
follow up on #2737 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-11-25 08:35:28 -08:00
if (Z3_SAVE_CLANG_OPTIMIZATION_RECORDS)
cmake: Allow saving clang's optimization records. This gives some insight into what the compiler has decided to do or not do.
2018-11-30 19:52:57 +07:00
z3_add_cxx_flag("-fsave-optimization-record" REQUIRED)
endif()
Implement a CMake build system. This is a large rework of my first attempt at this (#459). This implementation calls into the recently implemented python scripts to generate the necessary generated ``.h`` and ``.cpp`` files but is independent from Python building system otherwise. Unlike the Python build system, the generated files are emitted into the build tree to avoid polluting the source tree. The build system is setup to refuse to configure if it detects generated files in the source tree. If your source tree is dirty you can run ``git clean -fx`` to clean your working directory. Currently the build succeeds on Linux using CMake 3.4.3 using the "Unix Makefiles" generator with gcc or clang. The following notable features are implemented: * Building of the C and C++ examples and the ``test-z3`` executable. These are included from the ``all`` target so you have to tell the build system (e.g. make) to build them manually. * Install (``make install``) and uninstall (``make uninstall``) of libz3 and its header files. This supports ``DESTDIR`` out of the box because CMake supports it. * An option (``BUILD_LIBZ3_SHARED``) to build libz3 as a static or dynamic library. * Support for using/not using OpenMP (``USE_OPENMP``) * Support for using/not using libgmp (``USE_LIB_GMP``) * Setting the SOVERSION for libz3. I'm not sure if I'm setting the * number correctly though. This is required by Linux distrubtions that wills ship libz3. This needs discussion. The following notable features are currently not implemented and are left for future work. * Support for ARM. * Support for the foci2 library. * Support for creating/installing/uninstalling the dotnet, java, python and ml bindings. * Full support for MSVC. Although I've tried to write the CMake code with MSVC in mind not all the correct flags are passed to it. * Support for using the git hash. This new build system has several advantages other the old build system. * It is easier for outside contributors to contribute to Z3 when the build system is something more standard. * Incremental builds work properly. With the old build system when new code is pulled down the old build directory would need to thrown out and a new fresh build had to be performed because the build system didn't know how to correctly rebuild the project (e.g. couldn't handle new sources being added/removed, compiler flags changing, generated files changing, etc...). This is a MASSIVE boost to productivity! * We now have access rich array of features that CMake provides for building C/C++ projects. This means less time spent implementing custom build system logic in Python that is already supported by CMake. * CMake supports many IDEs out of the box so it should be fairly straight forward to build Z3 with Visual Studio (once support for MSVC is added), Xcode, Eclipse CDT, CLion, ..etc.
2016-02-20 23:21:00 +00:00
################################################################################
disable GCC flag change to see if this affects build Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-09 15:40:35 -05:00
# If using Ninja, force color output for Clang (and gcc, disabled to check build).
Force color output with Ninja.
2018-03-07 13:29:13 +07:00
################################################################################
if (UNIX AND CMAKE_GENERATOR STREQUAL "Ninja")
if (CMAKE_CXX_COMPILER_ID STREQUAL "Clang")
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fcolor-diagnostics")
set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -fcolor-diagnostics")
endif()
disable GCC flag change to see if this affects build Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-09 15:40:35 -05:00
# if (CMAKE_CXX_COMPILER_ID STREQUAL "GNU")
# set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fdiagnostics-color")
# set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -fdiagnostics-color")
# endif()
Force color output with Ninja.
2018-03-07 13:29:13 +07:00
endif()
################################################################################
Implement a CMake build system. This is a large rework of my first attempt at this (#459). This implementation calls into the recently implemented python scripts to generate the necessary generated ``.h`` and ``.cpp`` files but is independent from Python building system otherwise. Unlike the Python build system, the generated files are emitted into the build tree to avoid polluting the source tree. The build system is setup to refuse to configure if it detects generated files in the source tree. If your source tree is dirty you can run ``git clean -fx`` to clean your working directory. Currently the build succeeds on Linux using CMake 3.4.3 using the "Unix Makefiles" generator with gcc or clang. The following notable features are implemented: * Building of the C and C++ examples and the ``test-z3`` executable. These are included from the ``all`` target so you have to tell the build system (e.g. make) to build them manually. * Install (``make install``) and uninstall (``make uninstall``) of libz3 and its header files. This supports ``DESTDIR`` out of the box because CMake supports it. * An option (``BUILD_LIBZ3_SHARED``) to build libz3 as a static or dynamic library. * Support for using/not using OpenMP (``USE_OPENMP``) * Support for using/not using libgmp (``USE_LIB_GMP``) * Setting the SOVERSION for libz3. I'm not sure if I'm setting the * number correctly though. This is required by Linux distrubtions that wills ship libz3. This needs discussion. The following notable features are currently not implemented and are left for future work. * Support for ARM. * Support for the foci2 library. * Support for creating/installing/uninstalling the dotnet, java, python and ml bindings. * Full support for MSVC. Although I've tried to write the CMake code with MSVC in mind not all the correct flags are passed to it. * Support for using the git hash. This new build system has several advantages other the old build system. * It is easier for outside contributors to contribute to Z3 when the build system is something more standard. * Incremental builds work properly. With the old build system when new code is pulled down the old build directory would need to thrown out and a new fresh build had to be performed because the build system didn't know how to correctly rebuild the project (e.g. couldn't handle new sources being added/removed, compiler flags changing, generated files changing, etc...). This is a MASSIVE boost to productivity! * We now have access rich array of features that CMake provides for building C/C++ projects. This means less time spent implementing custom build system logic in Python that is already supported by CMake. * CMake supports many IDEs out of the box so it should be fairly straight forward to build Z3 with Visual Studio (once support for MSVC is added), Xcode, Eclipse CDT, CLion, ..etc.
2016-02-20 23:21:00 +00:00
# Option to control what type of library we build
################################################################################
rename additional build options #2709 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-11-18 23:06:48 -08:00
option(Z3_BUILD_LIBZ3_SHARED "Build libz3 as a shared library if true, otherwise build a static library" ON)
Add option 'MSVC_STATIC' (#6358) * Add option 'MSVC_STATIC' * Update CMakeLists.txt * Update CMakeLists.txt * Upload msvc-static-build.yml
2022-09-23 04:55:40 +08:00
option(Z3_BUILD_LIBZ3_MSVC_STATIC "Build libz3 as a statically-linked runtime library" OFF)
Implement a CMake build system. This is a large rework of my first attempt at this (#459). This implementation calls into the recently implemented python scripts to generate the necessary generated ``.h`` and ``.cpp`` files but is independent from Python building system otherwise. Unlike the Python build system, the generated files are emitted into the build tree to avoid polluting the source tree. The build system is setup to refuse to configure if it detects generated files in the source tree. If your source tree is dirty you can run ``git clean -fx`` to clean your working directory. Currently the build succeeds on Linux using CMake 3.4.3 using the "Unix Makefiles" generator with gcc or clang. The following notable features are implemented: * Building of the C and C++ examples and the ``test-z3`` executable. These are included from the ``all`` target so you have to tell the build system (e.g. make) to build them manually. * Install (``make install``) and uninstall (``make uninstall``) of libz3 and its header files. This supports ``DESTDIR`` out of the box because CMake supports it. * An option (``BUILD_LIBZ3_SHARED``) to build libz3 as a static or dynamic library. * Support for using/not using OpenMP (``USE_OPENMP``) * Support for using/not using libgmp (``USE_LIB_GMP``) * Setting the SOVERSION for libz3. I'm not sure if I'm setting the * number correctly though. This is required by Linux distrubtions that wills ship libz3. This needs discussion. The following notable features are currently not implemented and are left for future work. * Support for ARM. * Support for the foci2 library. * Support for creating/installing/uninstalling the dotnet, java, python and ml bindings. * Full support for MSVC. Although I've tried to write the CMake code with MSVC in mind not all the correct flags are passed to it. * Support for using the git hash. This new build system has several advantages other the old build system. * It is easier for outside contributors to contribute to Z3 when the build system is something more standard. * Incremental builds work properly. With the old build system when new code is pulled down the old build directory would need to thrown out and a new fresh build had to be performed because the build system didn't know how to correctly rebuild the project (e.g. couldn't handle new sources being added/removed, compiler flags changing, generated files changing, etc...). This is a MASSIVE boost to productivity! * We now have access rich array of features that CMake provides for building C/C++ projects. This means less time spent implementing custom build system logic in Python that is already supported by CMake. * CMake supports many IDEs out of the box so it should be fairly straight forward to build Z3 with Visual Studio (once support for MSVC is added), Xcode, Eclipse CDT, CLion, ..etc.
2016-02-20 23:21:00 +00:00
################################################################################
# Tracing
################################################################################
rename additional build options #2709 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-11-18 20:39:04 -08:00
option(Z3_ENABLE_TRACING_FOR_NON_DEBUG "Enable tracing in non-debug builds." OFF)
if (Z3_ENABLE_TRACING_FOR_NON_DEBUG)
Implement a CMake build system. This is a large rework of my first attempt at this (#459). This implementation calls into the recently implemented python scripts to generate the necessary generated ``.h`` and ``.cpp`` files but is independent from Python building system otherwise. Unlike the Python build system, the generated files are emitted into the build tree to avoid polluting the source tree. The build system is setup to refuse to configure if it detects generated files in the source tree. If your source tree is dirty you can run ``git clean -fx`` to clean your working directory. Currently the build succeeds on Linux using CMake 3.4.3 using the "Unix Makefiles" generator with gcc or clang. The following notable features are implemented: * Building of the C and C++ examples and the ``test-z3`` executable. These are included from the ``all`` target so you have to tell the build system (e.g. make) to build them manually. * Install (``make install``) and uninstall (``make uninstall``) of libz3 and its header files. This supports ``DESTDIR`` out of the box because CMake supports it. * An option (``BUILD_LIBZ3_SHARED``) to build libz3 as a static or dynamic library. * Support for using/not using OpenMP (``USE_OPENMP``) * Support for using/not using libgmp (``USE_LIB_GMP``) * Setting the SOVERSION for libz3. I'm not sure if I'm setting the * number correctly though. This is required by Linux distrubtions that wills ship libz3. This needs discussion. The following notable features are currently not implemented and are left for future work. * Support for ARM. * Support for the foci2 library. * Support for creating/installing/uninstalling the dotnet, java, python and ml bindings. * Full support for MSVC. Although I've tried to write the CMake code with MSVC in mind not all the correct flags are passed to it. * Support for using the git hash. This new build system has several advantages other the old build system. * It is easier for outside contributors to contribute to Z3 when the build system is something more standard. * Incremental builds work properly. With the old build system when new code is pulled down the old build directory would need to thrown out and a new fresh build had to be performed because the build system didn't know how to correctly rebuild the project (e.g. couldn't handle new sources being added/removed, compiler flags changing, generated files changing, etc...). This is a MASSIVE boost to productivity! * We now have access rich array of features that CMake provides for building C/C++ projects. This means less time spent implementing custom build system logic in Python that is already supported by CMake. * CMake supports many IDEs out of the box so it should be fairly straight forward to build Z3 with Visual Studio (once support for MSVC is added), Xcode, Eclipse CDT, CLion, ..etc.
2016-02-20 23:21:00 +00:00
list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_TRACE")
[CMake] Fix issue #522 Previously tracing could be disabled and was not enabled by default in a debug build. This isn't desirable but I had avoided fixing it because enabling tracing in debug mode would be confusing because ``ENABLE_TRACING`` could be set to off but tracing would be enabled anyway. I have resolved this by renaming the option from ``ENABLE_TRACING`` to ``ENABLE_TRACING_FOR_NON_DEBUG``. The semantics of the optiona are now that it will enable tracing in non-debug builds. I have also added code to ensure that tracing is always enabled in debug builds. Whilst I was here I also fixed how ``option()`` was being used. The default value and comment were in the wrong order.
2016-03-21 19:33:50 +00:00
else()
# Tracing is always enabled in debug builds
list(APPEND Z3_COMPONENT_CXX_DEFINES $<$<CONFIG:Debug>:_TRACE>)
Implement a CMake build system. This is a large rework of my first attempt at this (#459). This implementation calls into the recently implemented python scripts to generate the necessary generated ``.h`` and ``.cpp`` files but is independent from Python building system otherwise. Unlike the Python build system, the generated files are emitted into the build tree to avoid polluting the source tree. The build system is setup to refuse to configure if it detects generated files in the source tree. If your source tree is dirty you can run ``git clean -fx`` to clean your working directory. Currently the build succeeds on Linux using CMake 3.4.3 using the "Unix Makefiles" generator with gcc or clang. The following notable features are implemented: * Building of the C and C++ examples and the ``test-z3`` executable. These are included from the ``all`` target so you have to tell the build system (e.g. make) to build them manually. * Install (``make install``) and uninstall (``make uninstall``) of libz3 and its header files. This supports ``DESTDIR`` out of the box because CMake supports it. * An option (``BUILD_LIBZ3_SHARED``) to build libz3 as a static or dynamic library. * Support for using/not using OpenMP (``USE_OPENMP``) * Support for using/not using libgmp (``USE_LIB_GMP``) * Setting the SOVERSION for libz3. I'm not sure if I'm setting the * number correctly though. This is required by Linux distrubtions that wills ship libz3. This needs discussion. The following notable features are currently not implemented and are left for future work. * Support for ARM. * Support for the foci2 library. * Support for creating/installing/uninstalling the dotnet, java, python and ml bindings. * Full support for MSVC. Although I've tried to write the CMake code with MSVC in mind not all the correct flags are passed to it. * Support for using the git hash. This new build system has several advantages other the old build system. * It is easier for outside contributors to contribute to Z3 when the build system is something more standard. * Incremental builds work properly. With the old build system when new code is pulled down the old build directory would need to thrown out and a new fresh build had to be performed because the build system didn't know how to correctly rebuild the project (e.g. couldn't handle new sources being added/removed, compiler flags changing, generated files changing, etc...). This is a MASSIVE boost to productivity! * We now have access rich array of features that CMake provides for building C/C++ projects. This means less time spent implementing custom build system logic in Python that is already supported by CMake. * CMake supports many IDEs out of the box so it should be fairly straight forward to build Z3 with Visual Studio (once support for MSVC is added), Xcode, Eclipse CDT, CLion, ..etc.
2016-02-20 23:21:00 +00:00
endif()
[CMake] Report the various values of CMAKE_CXX_FLAGS, CMAKE_CXX_FLAGS_<CONFIG>, CMAKE_<TYPE>_LINKER_FLAGS, and CMAKE_<TYPE>_LINKER_FLAGS_<CONFIG>. This is useful for debugging where some flags come from. Now that we don't explicitly set the defaults it useful to see which default values we are getting from CMake.
2017-04-28 21:30:36 +01:00
################################################################################
[CMake] Add support for link time optimization (LTO). This analogous to the `--optimize` flag in the Python/Makefile build system except that we now support doing LTO with Clang/GCC as well. However it is probably best to avoid doing LTO with Clang or GCC for now because I see a bunch of warnings about ODR violations when building with LTO. LTO can be enabled with the new `LINK_TIME_OPTIMIZATION` option which is off by default.
2017-04-29 01:21:49 +01:00
# Link time optimization
################################################################################
Change from BINARY_DIR to PROJECT_BINARY_DIR
2019-05-15 11:25:40 -07:00
include(${PROJECT_SOURCE_DIR}/cmake/compiler_lto.cmake)
[CMake] Add support for link time optimization (LTO). This analogous to the `--optimize` flag in the Python/Makefile build system except that we now support doing LTO with Clang/GCC as well. However it is probably best to avoid doing LTO with Clang or GCC for now because I see a bunch of warnings about ODR violations when building with LTO. LTO can be enabled with the new `LINK_TIME_OPTIMIZATION` option which is off by default.
2017-04-29 01:21:49 +01:00
Adding ENABLE_CFI flag to CMake.
2017-07-24 15:53:37 -07:00
################################################################################
Enabling Control Flow Guard (CFG) by default for MSVC on Windows, with options to disable CFG. (#7988) * Enabling Control Flow Guard by default for MSVC on Windows, with options to disable it. * Fix configuration error for non-MSVC compilers. * Reviewed and updated configuration for Python build and added comment for CFG.
2025-10-22 05:18:25 -07:00
# Control flow integrity (Clang only)
Adding ENABLE_CFI flag to CMake.
2017-07-24 15:53:37 -07:00
################################################################################
Enabling Control Flow Guard (CFG) by default for MSVC on Windows, with options to disable CFG. (#7988) * Enabling Control Flow Guard by default for MSVC on Windows, with options to disable it. * Fix configuration error for non-MSVC compilers. * Reviewed and updated configuration for Python build and added comment for CFG.
2025-10-22 05:18:25 -07:00
option(Z3_ENABLE_CFI "Enable Control Flow Integrity security checks" OFF)
rename additional build options #2709 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-11-18 20:50:53 -08:00
if (Z3_ENABLE_CFI)
Enabling Control Flow Guard (CFG) by default for MSVC on Windows, with options to disable CFG. (#7988) * Enabling Control Flow Guard by default for MSVC on Windows, with options to disable it. * Fix configuration error for non-MSVC compilers. * Reviewed and updated configuration for Python build and added comment for CFG.
2025-10-22 05:18:25 -07:00
if (NOT CMAKE_CXX_COMPILER_ID MATCHES "Clang")
message(FATAL_ERROR "Z3_ENABLE_CFI is only supported with Clang compiler. "
"Current compiler: ${CMAKE_CXX_COMPILER_ID}. "
"You should set Z3_ENABLE_CFI to OFF or use Clang to compile.")
endif()
rename additional build options #2709 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-11-18 20:50:53 -08:00
if (NOT Z3_LINK_TIME_OPTIMIZATION)
Enabling Control Flow Guard (CFG) by default for MSVC on Windows, with options to disable CFG. (#7988) * Enabling Control Flow Guard by default for MSVC on Windows, with options to disable it. * Fix configuration error for non-MSVC compilers. * Reviewed and updated configuration for Python build and added comment for CFG.
2025-10-22 05:18:25 -07:00
message(FATAL_ERROR "Cannot enable Control Flow Integrity without link-time optimization. "
rename additional build options #2709 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-11-18 20:50:53 -08:00
"You should set Z3_LINK_TIME_OPTIMIZATION to ON or Z3_ENABLE_CFI to OFF.")
Adding ENABLE_CFI flag to CMake.
2017-07-24 15:53:37 -07:00
endif()
Enabling Control Flow Guard (CFG) by default for MSVC on Windows, with options to disable CFG. (#7988) * Enabling Control Flow Guard by default for MSVC on Windows, with options to disable it. * Fix configuration error for non-MSVC compilers. * Reviewed and updated configuration for Python build and added comment for CFG.
2025-10-22 05:18:25 -07:00
set(build_types_with_cfi "RELEASE" "RELWITHDEBINFO")
Adding ENABLE_CFI flag to CMake.
2017-07-24 15:53:37 -07:00
if (DEFINED CMAKE_CONFIGURATION_TYPES)
# Multi configuration generator
message(STATUS "Note CFI is only enabled for the following configurations: ${build_types_with_cfi}")
# No need for else because this is the same as the set that LTO requires.
endif()
Enabling Control Flow Guard (CFG) by default for MSVC on Windows, with options to disable CFG. (#7988) * Enabling Control Flow Guard by default for MSVC on Windows, with options to disable it. * Fix configuration error for non-MSVC compilers. * Reviewed and updated configuration for Python build and added comment for CFG.
2025-10-22 05:18:25 -07:00
message(STATUS "Enabling Control Flow Integrity (CFI) for Clang")
z3_add_cxx_flag("-fsanitize=cfi" REQUIRED)
z3_add_cxx_flag("-fsanitize-cfi-cross-dso" REQUIRED)
endif()
# End CFI section
################################################################################
# Control Flow Guard (MSVC only)
################################################################################
# Default CFG to ON for MSVC, OFF for other compilers.
if (CMAKE_CXX_COMPILER_ID STREQUAL "MSVC")
option(Z3_ENABLE_CFG "Enable Control Flow Guard security checks" ON)
else()
option(Z3_ENABLE_CFG "Enable Control Flow Guard security checks" OFF)
endif()
if (Z3_ENABLE_CFG)
if (NOT CMAKE_CXX_COMPILER_ID STREQUAL "MSVC")
message(FATAL_ERROR "Z3_ENABLE_CFG is only supported with MSVC compiler. "
"Current compiler: ${CMAKE_CXX_COMPILER_ID}. "
"You should remove Z3_ENABLE_CFG or set it to OFF or use MSVC to compile.")
endif()
# Check for incompatible options (handle both / and - forms for robustness)
string(REGEX MATCH "[-/]ZI" _has_ZI "${CMAKE_CXX_FLAGS} ${CMAKE_CXX_FLAGS_DEBUG} ${CMAKE_CXX_FLAGS_RELEASE} ${CMAKE_CXX_FLAGS_RELWITHDEBINFO} ${CMAKE_CXX_FLAGS_MINSIZEREL}")
string(REGEX MATCH "[-/]clr" _has_clr "${CMAKE_CXX_FLAGS} ${CMAKE_CXX_FLAGS_DEBUG} ${CMAKE_CXX_FLAGS_RELEASE} ${CMAKE_CXX_FLAGS_RELWITHDEBINFO} ${CMAKE_CXX_FLAGS_MINSIZEREL}")
if(_has_ZI)
message(WARNING "/guard:cf is incompatible with /ZI (Edit and Continue debug information). "
"Control Flow Guard will be disabled due to /ZI option.")
elseif(_has_clr)
message(WARNING "/guard:cf is incompatible with /clr (Common Language Runtime compilation). "
"Control Flow Guard will be disabled due to /clr option.")
Adding ENABLE_CFI flag to CMake.
2017-07-24 15:53:37 -07:00
else()
Enabling Control Flow Guard (CFG) by default for MSVC on Windows, with options to disable CFG. (#7988) * Enabling Control Flow Guard by default for MSVC on Windows, with options to disable it. * Fix configuration error for non-MSVC compilers. * Reviewed and updated configuration for Python build and added comment for CFG.
2025-10-22 05:18:25 -07:00
# Enable Control Flow Guard if no incompatible options are present
message(STATUS "Enabling Control Flow Guard (/guard:cf) and ASLR (/DYNAMICBASE) for MSVC")
z3_add_cxx_flag("/guard:cf" REQUIRED)
string(APPEND CMAKE_EXE_LINKER_FLAGS " /GUARD:CF /DYNAMICBASE")
string(APPEND CMAKE_SHARED_LINKER_FLAGS " /GUARD:CF /DYNAMICBASE")
endif()
else()
if (CMAKE_CXX_COMPILER_ID STREQUAL "MSVC")
# Explicitly disable Control Flow Guard when Z3_ENABLE_CFG is OFF
message(STATUS "Disabling Control Flow Guard (/guard:cf-) for MSVC")
z3_add_cxx_flag("/guard:cf-" REQUIRED)
string(APPEND CMAKE_EXE_LINKER_FLAGS " /GUARD:NO")
string(APPEND CMAKE_SHARED_LINKER_FLAGS " /GUARD:NO")
Adding ENABLE_CFI flag to CMake.
2017-07-24 15:53:37 -07:00
endif()
endif()
[CMake] Add support for link time optimization (LTO). This analogous to the `--optimize` flag in the Python/Makefile build system except that we now support doing LTO with Clang/GCC as well. However it is probably best to avoid doing LTO with Clang or GCC for now because I see a bunch of warnings about ODR violations when building with LTO. LTO can be enabled with the new `LINK_TIME_OPTIMIZATION` option which is off by default.
2017-04-29 01:21:49 +01:00
################################################################################
[CMake] Try to do a better job of matching the old build system's compiler defines and flags when using MSVC. There are lots of defines and flags that I'm unsure about so in some cases I've changed the behaviour slightly (if I'm confident the behaviour in the old build system is wrong) or not added the flag/define at all but just left comments noting what the old build system did and why I disagree with the old build system's choices.
2017-04-29 11:00:27 +01:00
# MSVC specific flags inherited from old build system
################################################################################
clean up CMake code (#5182) * CMake: simplify FindGMP.cmake Remove printing of all the different variables, and let FPHSA output the library name. Add an imported target, which bundles the library and the include directories for easier usage. * fix build: vector::c_ptr() now is vector::data() * CMake: use Threads::Threads imported module Otherwise the setting of THREADS_PREFER_PTHREAD_FLAG has no effect. * CMake: remove needless policy setting The minimum required version is CMake 3.4, where these policies are already set to new because they were introduced earlier. * CMake: remove needless variable expansion
2021-04-14 19:29:15 +02:00
if (CMAKE_CXX_COMPILER_ID STREQUAL "MSVC")
Change from BINARY_DIR to PROJECT_BINARY_DIR
2019-05-15 11:25:40 -07:00
include(${PROJECT_SOURCE_DIR}/cmake/msvc_legacy_quirks.cmake)
[CMake] Try to do a better job of matching the old build system's compiler defines and flags when using MSVC. There are lots of defines and flags that I'm unsure about so in some cases I've changed the behaviour slightly (if I'm confident the behaviour in the old build system is wrong) or not added the flag/define at all but just left comments noting what the old build system did and why I disagree with the old build system's choices.
2017-04-29 11:00:27 +01:00
endif()
Pass /RELEASE to MSVC linker Without /RELEASE passed to MSVC linker, the checksum field in exe/dll is not calculated. When you load the exe/dll in windbg (e.g., windbg -z libz3.dll), a warning "Unable to verify checksum" will show. With /RELEASE passed to linker, the warning will be gone.
2019-07-04 08:08:32 -07:00
################################################################################
# Pass /RELEASE to the linker so that checksums in PE files are calculated.
################################################################################
clean up CMake code (#5182) * CMake: simplify FindGMP.cmake Remove printing of all the different variables, and let FPHSA output the library name. Add an imported target, which bundles the library and the include directories for easier usage. * fix build: vector::c_ptr() now is vector::data() * CMake: use Threads::Threads imported module Otherwise the setting of THREADS_PREFER_PTHREAD_FLAG has no effect. * CMake: remove needless policy setting The minimum required version is CMake 3.4, where these policies are already set to new because they were introduced earlier. * CMake: remove needless variable expansion
2021-04-14 19:29:15 +02:00
if (CMAKE_CXX_COMPILER_ID STREQUAL "MSVC")
Pass /RELEASE to MSVC linker Without /RELEASE passed to MSVC linker, the checksum field in exe/dll is not calculated. When you load the exe/dll in windbg (e.g., windbg -z libz3.dll), a warning "Unable to verify checksum" will show. With /RELEASE passed to linker, the warning will be gone.
2019-07-04 08:08:32 -07:00
string(APPEND CMAKE_EXE_LINKER_FLAGS " /RELEASE")
string(APPEND CMAKE_SHARED_LINKER_FLAGS " /RELEASE")
endif()
github action: add riscv64/aarch64/powerpc64 cross compile (#5897) * github action: add riscv64/aarch64/powerpc64 cross compile Signed-off-by: Han Gao <rabenda.cn@gmail.com> * fix: build on non-x86 platform Signed-off-by: Revy <rabenda.cn@gmail.com>
2022-03-16 22:30:20 +08:00
################################################################################
# Check atomic linking as needed
################################################################################
include(${PROJECT_SOURCE_DIR}/cmake/check_link_atomic.cmake)
[CMake] Try to do a better job of matching the old build system's compiler defines and flags when using MSVC. There are lots of defines and flags that I'm unsure about so in some cases I've changed the behaviour slightly (if I'm confident the behaviour in the old build system is wrong) or not added the flag/define at all but just left comments noting what the old build system did and why I disagree with the old build system's choices.
2017-04-29 11:00:27 +01:00
################################################################################
[CMake] Report the various values of CMAKE_CXX_FLAGS, CMAKE_CXX_FLAGS_<CONFIG>, CMAKE_<TYPE>_LINKER_FLAGS, and CMAKE_<TYPE>_LINKER_FLAGS_<CONFIG>. This is useful for debugging where some flags come from. Now that we don't explicitly set the defaults it useful to see which default values we are getting from CMake.
2017-04-28 21:30:36 +01:00
# Report default CMake flags
################################################################################
# This is mainly for debugging.
message(STATUS "CMAKE_CXX_FLAGS: \"${CMAKE_CXX_FLAGS}\"")
message(STATUS "CMAKE_EXE_LINKER_FLAGS: \"${CMAKE_EXE_LINKER_FLAGS}\"")
message(STATUS "CMAKE_STATIC_LINKER_FLAGS: \"${CMAKE_STATIC_LINKER_FLAGS}\"")
message(STATUS "CMAKE_SHARED_LINKER_FLAGS: \"${CMAKE_SHARED_LINKER_FLAGS}\"")
if (DEFINED CMAKE_CONFIGURATION_TYPES)
# Multi configuration generator
string(TOUPPER "${available_build_types}" build_types_to_report)
else()
# Single configuration generator
string(TOUPPER "${CMAKE_BUILD_TYPE}" build_types_to_report)
endif()
foreach (_build_type ${build_types_to_report})
message(STATUS "CMAKE_CXX_FLAGS_${_build_type}: \"${CMAKE_CXX_FLAGS_${_build_type}}\"")
message(STATUS "CMAKE_EXE_LINKER_FLAGS_${_build_type}: \"${CMAKE_EXE_LINKER_FLAGS_${_build_type}}\"")
message(STATUS "CMAKE_SHARED_LINKER_FLAGS_${_build_type}: \"${CMAKE_SHARED_LINKER_FLAGS_${_build_type}}\"")
message(STATUS "CMAKE_STATIC_LINKER_FLAGS_${_build_type}: \"${CMAKE_STATIC_LINKER_FLAGS_${_build_type}}\"")
endforeach()
Implement a CMake build system. This is a large rework of my first attempt at this (#459). This implementation calls into the recently implemented python scripts to generate the necessary generated ``.h`` and ``.cpp`` files but is independent from Python building system otherwise. Unlike the Python build system, the generated files are emitted into the build tree to avoid polluting the source tree. The build system is setup to refuse to configure if it detects generated files in the source tree. If your source tree is dirty you can run ``git clean -fx`` to clean your working directory. Currently the build succeeds on Linux using CMake 3.4.3 using the "Unix Makefiles" generator with gcc or clang. The following notable features are implemented: * Building of the C and C++ examples and the ``test-z3`` executable. These are included from the ``all`` target so you have to tell the build system (e.g. make) to build them manually. * Install (``make install``) and uninstall (``make uninstall``) of libz3 and its header files. This supports ``DESTDIR`` out of the box because CMake supports it. * An option (``BUILD_LIBZ3_SHARED``) to build libz3 as a static or dynamic library. * Support for using/not using OpenMP (``USE_OPENMP``) * Support for using/not using libgmp (``USE_LIB_GMP``) * Setting the SOVERSION for libz3. I'm not sure if I'm setting the * number correctly though. This is required by Linux distrubtions that wills ship libz3. This needs discussion. The following notable features are currently not implemented and are left for future work. * Support for ARM. * Support for the foci2 library. * Support for creating/installing/uninstalling the dotnet, java, python and ml bindings. * Full support for MSVC. Although I've tried to write the CMake code with MSVC in mind not all the correct flags are passed to it. * Support for using the git hash. This new build system has several advantages other the old build system. * It is easier for outside contributors to contribute to Z3 when the build system is something more standard. * Incremental builds work properly. With the old build system when new code is pulled down the old build directory would need to thrown out and a new fresh build had to be performed because the build system didn't know how to correctly rebuild the project (e.g. couldn't handle new sources being added/removed, compiler flags changing, generated files changing, etc...). This is a MASSIVE boost to productivity! * We now have access rich array of features that CMake provides for building C/C++ projects. This means less time spent implementing custom build system logic in Python that is already supported by CMake. * CMake supports many IDEs out of the box so it should be fairly straight forward to build Z3 with Visual Studio (once support for MSVC is added), Xcode, Eclipse CDT, CLion, ..etc.
2016-02-20 23:21:00 +00:00
################################################################################
# Report Z3_COMPONENT flags
################################################################################
message(STATUS "Z3_COMPONENT_CXX_DEFINES: ${Z3_COMPONENT_CXX_DEFINES}")
message(STATUS "Z3_COMPONENT_CXX_FLAGS: ${Z3_COMPONENT_CXX_FLAGS}")
message(STATUS "Z3_DEPENDENT_LIBS: ${Z3_DEPENDENT_LIBS}")
message(STATUS "Z3_COMPONENT_EXTRA_INCLUDE_DIRS: ${Z3_COMPONENT_EXTRA_INCLUDE_DIRS}")
Don't append ${OpenMP_CXX_FLAGS} to Z3_DEPENDENT_LIBS. This is wrong because this is passed to ``target_link_libraries()``. It just so happens that ``target_link_libraries()`` will interpret arguments starting with a dash as a flag to pass to the linker (i.e. in this case ``-fopenmp``). However in the case of MSVC that flag is ``/openmp`` which is the interpreted as a file path which will lead to a linker failure later because the linker can't find the file ``\openmp.obj``.
2016-02-29 20:53:57 +00:00
message(STATUS "Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS: ${Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS}")
Implement a CMake build system. This is a large rework of my first attempt at this (#459). This implementation calls into the recently implemented python scripts to generate the necessary generated ``.h`` and ``.cpp`` files but is independent from Python building system otherwise. Unlike the Python build system, the generated files are emitted into the build tree to avoid polluting the source tree. The build system is setup to refuse to configure if it detects generated files in the source tree. If your source tree is dirty you can run ``git clean -fx`` to clean your working directory. Currently the build succeeds on Linux using CMake 3.4.3 using the "Unix Makefiles" generator with gcc or clang. The following notable features are implemented: * Building of the C and C++ examples and the ``test-z3`` executable. These are included from the ``all`` target so you have to tell the build system (e.g. make) to build them manually. * Install (``make install``) and uninstall (``make uninstall``) of libz3 and its header files. This supports ``DESTDIR`` out of the box because CMake supports it. * An option (``BUILD_LIBZ3_SHARED``) to build libz3 as a static or dynamic library. * Support for using/not using OpenMP (``USE_OPENMP``) * Support for using/not using libgmp (``USE_LIB_GMP``) * Setting the SOVERSION for libz3. I'm not sure if I'm setting the * number correctly though. This is required by Linux distrubtions that wills ship libz3. This needs discussion. The following notable features are currently not implemented and are left for future work. * Support for ARM. * Support for the foci2 library. * Support for creating/installing/uninstalling the dotnet, java, python and ml bindings. * Full support for MSVC. Although I've tried to write the CMake code with MSVC in mind not all the correct flags are passed to it. * Support for using the git hash. This new build system has several advantages other the old build system. * It is easier for outside contributors to contribute to Z3 when the build system is something more standard. * Incremental builds work properly. With the old build system when new code is pulled down the old build directory would need to thrown out and a new fresh build had to be performed because the build system didn't know how to correctly rebuild the project (e.g. couldn't handle new sources being added/removed, compiler flags changing, generated files changing, etc...). This is a MASSIVE boost to productivity! * We now have access rich array of features that CMake provides for building C/C++ projects. This means less time spent implementing custom build system logic in Python that is already supported by CMake. * CMake supports many IDEs out of the box so it should be fairly straight forward to build Z3 with Visual Studio (once support for MSVC is added), Xcode, Eclipse CDT, CLion, ..etc.
2016-02-20 23:21:00 +00:00
################################################################################
# Z3 installation locations
################################################################################
[CMake] Provide a way to customise the install directories used for executables, include files and libraries. We use ``GNUInstallDirs.cmake`` which ships with CMake to do the difficult work of setting a sensible default and setting up CMake cache variables. These can be overriden when running CMake by setting the ``CMAKE_INSTALL_BINDIR``, ``CMAKE_INSTALL_INCLUDEDIR`` and ``CMAKE_INSTALL_LIBDIR`` cache variables.
2016-03-09 14:09:29 +00:00
include(GNUInstallDirs)
[CMake] Implement support for building the .NET bindings. When using Mono support for installing/uninstalling the bindings is also implemented. For Windows install/uninstall is not implemented because the python build system does not implement it and Microsoft's documentation (https://msdn.microsoft.com/en-us/library/dkkx7f79.aspx) says that the gacutil should only be used for development and not for production. For now a warning is just emitted if ``INSTALL_DOTNET_BINDINGS`` is enabled and the .NET toolchain is native Windows. Someone with better knowledge of how to correctly install assemblies under Windows should implement this or remove this message. A notable difference from the Python build system is the ``/linkresource:`` flag is not passed to the C# compiler. This means a user of the .NET bindings will have to copy the Z3 library (i.e. ``libz3.dll``) to their application directory manually. The reason for this difference is that using this flag requires the working directory to be the directory containing the Z3 library (i.e. ``libz3.dll``) but setting this up with multi-configuration generators doesn't currently seem possible.
2016-03-24 23:54:44 +00:00
set(CMAKE_INSTALL_PKGCONFIGDIR
"${CMAKE_INSTALL_LIBDIR}/pkgconfig"
CACHE
PATH
"Directory to install pkgconfig files"
)
[CMake] Implement generation of `Z3Config.cmake` and `Z3Target.cmake` file for the build and install tree. These files allow users of CMake to use Z3 via a CMake config package. Clients can do `find_package(Z3 CONFIG)` to get use the package from their projects. When generating the files for the install tree we try to generate the files so that they are relocatable so that it shouldn't matter if the installed files aren't in the CMAKE_INSTALL_PREFIX when a user consumes them. As long as the relative locations of the files aren't changed things should still work. A new CMake cache variable `CMAKE_INSTALL_Z3_CMAKE_PACKAGE_DIR` has been added so that the install location of the Z3 CMake package files can be controlled. This addresses #915 .
2017-03-03 19:39:53 +00:00
set(CMAKE_INSTALL_Z3_CMAKE_PACKAGE_DIR
"${CMAKE_INSTALL_LIBDIR}/cmake/z3"
CACHE
PATH
"Directory to install Z3 CMake package files"
)
[CMake] Provide a way to customise the install directories used for executables, include files and libraries. We use ``GNUInstallDirs.cmake`` which ships with CMake to do the difficult work of setting a sensible default and setting up CMake cache variables. These can be overriden when running CMake by setting the ``CMAKE_INSTALL_BINDIR``, ``CMAKE_INSTALL_INCLUDEDIR`` and ``CMAKE_INSTALL_LIBDIR`` cache variables.
2016-03-09 14:09:29 +00:00
message(STATUS "CMAKE_INSTALL_LIBDIR: \"${CMAKE_INSTALL_LIBDIR}\"")
message(STATUS "CMAKE_INSTALL_BINDIR: \"${CMAKE_INSTALL_BINDIR}\"")
message(STATUS "CMAKE_INSTALL_INCLUDEDIR: \"${CMAKE_INSTALL_INCLUDEDIR}\"")
[CMake] Implement support for building the .NET bindings. When using Mono support for installing/uninstalling the bindings is also implemented. For Windows install/uninstall is not implemented because the python build system does not implement it and Microsoft's documentation (https://msdn.microsoft.com/en-us/library/dkkx7f79.aspx) says that the gacutil should only be used for development and not for production. For now a warning is just emitted if ``INSTALL_DOTNET_BINDINGS`` is enabled and the .NET toolchain is native Windows. Someone with better knowledge of how to correctly install assemblies under Windows should implement this or remove this message. A notable difference from the Python build system is the ``/linkresource:`` flag is not passed to the C# compiler. This means a user of the .NET bindings will have to copy the Z3 library (i.e. ``libz3.dll``) to their application directory manually. The reason for this difference is that using this flag requires the working directory to be the directory containing the Z3 library (i.e. ``libz3.dll``) but setting this up with multi-configuration generators doesn't currently seem possible.
2016-03-24 23:54:44 +00:00
message(STATUS "CMAKE_INSTALL_PKGCONFIGDIR: \"${CMAKE_INSTALL_PKGCONFIGDIR}\"")
[CMake] Implement generation of `Z3Config.cmake` and `Z3Target.cmake` file for the build and install tree. These files allow users of CMake to use Z3 via a CMake config package. Clients can do `find_package(Z3 CONFIG)` to get use the package from their projects. When generating the files for the install tree we try to generate the files so that they are relocatable so that it shouldn't matter if the installed files aren't in the CMAKE_INSTALL_PREFIX when a user consumes them. As long as the relative locations of the files aren't changed things should still work. A new CMake cache variable `CMAKE_INSTALL_Z3_CMAKE_PACKAGE_DIR` has been added so that the install location of the Z3 CMake package files can be controlled. This addresses #915 .
2017-03-03 19:39:53 +00:00
message(STATUS "CMAKE_INSTALL_Z3_CMAKE_PACKAGE_DIR: \"${CMAKE_INSTALL_Z3_CMAKE_PACKAGE_DIR}\"")
Implement a CMake build system. This is a large rework of my first attempt at this (#459). This implementation calls into the recently implemented python scripts to generate the necessary generated ``.h`` and ``.cpp`` files but is independent from Python building system otherwise. Unlike the Python build system, the generated files are emitted into the build tree to avoid polluting the source tree. The build system is setup to refuse to configure if it detects generated files in the source tree. If your source tree is dirty you can run ``git clean -fx`` to clean your working directory. Currently the build succeeds on Linux using CMake 3.4.3 using the "Unix Makefiles" generator with gcc or clang. The following notable features are implemented: * Building of the C and C++ examples and the ``test-z3`` executable. These are included from the ``all`` target so you have to tell the build system (e.g. make) to build them manually. * Install (``make install``) and uninstall (``make uninstall``) of libz3 and its header files. This supports ``DESTDIR`` out of the box because CMake supports it. * An option (``BUILD_LIBZ3_SHARED``) to build libz3 as a static or dynamic library. * Support for using/not using OpenMP (``USE_OPENMP``) * Support for using/not using libgmp (``USE_LIB_GMP``) * Setting the SOVERSION for libz3. I'm not sure if I'm setting the * number correctly though. This is required by Linux distrubtions that wills ship libz3. This needs discussion. The following notable features are currently not implemented and are left for future work. * Support for ARM. * Support for the foci2 library. * Support for creating/installing/uninstalling the dotnet, java, python and ml bindings. * Full support for MSVC. Although I've tried to write the CMake code with MSVC in mind not all the correct flags are passed to it. * Support for using the git hash. This new build system has several advantages other the old build system. * It is easier for outside contributors to contribute to Z3 when the build system is something more standard. * Incremental builds work properly. With the old build system when new code is pulled down the old build directory would need to thrown out and a new fresh build had to be performed because the build system didn't know how to correctly rebuild the project (e.g. couldn't handle new sources being added/removed, compiler flags changing, generated files changing, etc...). This is a MASSIVE boost to productivity! * We now have access rich array of features that CMake provides for building C/C++ projects. This means less time spent implementing custom build system logic in Python that is already supported by CMake. * CMake supports many IDEs out of the box so it should be fairly straight forward to build Z3 with Visual Studio (once support for MSVC is added), Xcode, Eclipse CDT, CLion, ..etc.
2016-02-20 23:21:00 +00:00
[CMake] Declare uninstall rule before the components so that they can add dependencies to the rule for their own custom uninstall logic.
2016-03-26 17:08:24 +00:00
################################################################################
# Uninstall rule
################################################################################
configure_file(
Change from BINARY_DIR to PROJECT_BINARY_DIR
2019-05-15 11:25:40 -07:00
"${PROJECT_SOURCE_DIR}/cmake/cmake_uninstall.cmake.in"
[CMake] Declare uninstall rule before the components so that they can add dependencies to the rule for their own custom uninstall logic.
2016-03-26 17:08:24 +00:00
"${CMAKE_CURRENT_BINARY_DIR}/cmake_uninstall.cmake"
@ONLY
)
# Target needs to be declared before the components so that they can add
# dependencies to this target so they can run their own custom uninstall rules.
add_custom_target(uninstall
COMMAND
"${CMAKE_COMMAND}" -P "${CMAKE_CURRENT_BINARY_DIR}/cmake_uninstall.cmake"
COMMENT "Uninstalling..."
cmake: Cleanup remnants of workaround for USES_TERMINAL. In older versions, this was dependent upon the version of cmake, but when it was updated for newer cmake, these remnants were left.
2022-07-02 21:04:20 +07:00
USES_TERMINAL
[CMake] Declare uninstall rule before the components so that they can add dependencies to the rule for their own custom uninstall logic.
2016-03-26 17:08:24 +00:00
VERBATIM
)
Implement a CMake build system. This is a large rework of my first attempt at this (#459). This implementation calls into the recently implemented python scripts to generate the necessary generated ``.h`` and ``.cpp`` files but is independent from Python building system otherwise. Unlike the Python build system, the generated files are emitted into the build tree to avoid polluting the source tree. The build system is setup to refuse to configure if it detects generated files in the source tree. If your source tree is dirty you can run ``git clean -fx`` to clean your working directory. Currently the build succeeds on Linux using CMake 3.4.3 using the "Unix Makefiles" generator with gcc or clang. The following notable features are implemented: * Building of the C and C++ examples and the ``test-z3`` executable. These are included from the ``all`` target so you have to tell the build system (e.g. make) to build them manually. * Install (``make install``) and uninstall (``make uninstall``) of libz3 and its header files. This supports ``DESTDIR`` out of the box because CMake supports it. * An option (``BUILD_LIBZ3_SHARED``) to build libz3 as a static or dynamic library. * Support for using/not using OpenMP (``USE_OPENMP``) * Support for using/not using libgmp (``USE_LIB_GMP``) * Setting the SOVERSION for libz3. I'm not sure if I'm setting the * number correctly though. This is required by Linux distrubtions that wills ship libz3. This needs discussion. The following notable features are currently not implemented and are left for future work. * Support for ARM. * Support for the foci2 library. * Support for creating/installing/uninstalling the dotnet, java, python and ml bindings. * Full support for MSVC. Although I've tried to write the CMake code with MSVC in mind not all the correct flags are passed to it. * Support for using the git hash. This new build system has several advantages other the old build system. * It is easier for outside contributors to contribute to Z3 when the build system is something more standard. * Incremental builds work properly. With the old build system when new code is pulled down the old build directory would need to thrown out and a new fresh build had to be performed because the build system didn't know how to correctly rebuild the project (e.g. couldn't handle new sources being added/removed, compiler flags changing, generated files changing, etc...). This is a MASSIVE boost to productivity! * We now have access rich array of features that CMake provides for building C/C++ projects. This means less time spent implementing custom build system logic in Python that is already supported by CMake. * CMake supports many IDEs out of the box so it should be fairly straight forward to build Z3 with Visual Studio (once support for MSVC is added), Xcode, Eclipse CDT, CLion, ..etc.
2016-02-20 23:21:00 +00:00
################################################################################
# CMake build file locations
################################################################################
# To mimic the python build system output these into the root of the build
# directory
Change from BINARY_DIR to PROJECT_BINARY_DIR
2019-05-15 11:25:40 -07:00
set(CMAKE_LIBRARY_OUTPUT_DIRECTORY "${PROJECT_BINARY_DIR}")
set(CMAKE_ARCHIVE_OUTPUT_DIRECTORY "${PROJECT_BINARY_DIR}")
set(CMAKE_RUNTIME_OUTPUT_DIRECTORY "${PROJECT_BINARY_DIR}")
Implement a CMake build system. This is a large rework of my first attempt at this (#459). This implementation calls into the recently implemented python scripts to generate the necessary generated ``.h`` and ``.cpp`` files but is independent from Python building system otherwise. Unlike the Python build system, the generated files are emitted into the build tree to avoid polluting the source tree. The build system is setup to refuse to configure if it detects generated files in the source tree. If your source tree is dirty you can run ``git clean -fx`` to clean your working directory. Currently the build succeeds on Linux using CMake 3.4.3 using the "Unix Makefiles" generator with gcc or clang. The following notable features are implemented: * Building of the C and C++ examples and the ``test-z3`` executable. These are included from the ``all`` target so you have to tell the build system (e.g. make) to build them manually. * Install (``make install``) and uninstall (``make uninstall``) of libz3 and its header files. This supports ``DESTDIR`` out of the box because CMake supports it. * An option (``BUILD_LIBZ3_SHARED``) to build libz3 as a static or dynamic library. * Support for using/not using OpenMP (``USE_OPENMP``) * Support for using/not using libgmp (``USE_LIB_GMP``) * Setting the SOVERSION for libz3. I'm not sure if I'm setting the * number correctly though. This is required by Linux distrubtions that wills ship libz3. This needs discussion. The following notable features are currently not implemented and are left for future work. * Support for ARM. * Support for the foci2 library. * Support for creating/installing/uninstalling the dotnet, java, python and ml bindings. * Full support for MSVC. Although I've tried to write the CMake code with MSVC in mind not all the correct flags are passed to it. * Support for using the git hash. This new build system has several advantages other the old build system. * It is easier for outside contributors to contribute to Z3 when the build system is something more standard. * Incremental builds work properly. With the old build system when new code is pulled down the old build directory would need to thrown out and a new fresh build had to be performed because the build system didn't know how to correctly rebuild the project (e.g. couldn't handle new sources being added/removed, compiler flags changing, generated files changing, etc...). This is a MASSIVE boost to productivity! * We now have access rich array of features that CMake provides for building C/C++ projects. This means less time spent implementing custom build system logic in Python that is already supported by CMake. * CMake supports many IDEs out of the box so it should be fairly straight forward to build Z3 with Visual Studio (once support for MSVC is added), Xcode, Eclipse CDT, CLion, ..etc.
2016-02-20 23:21:00 +00:00
[CMake] Refactor the dependency on ``scripts/mk_util.py`` into a list ``Z3_GENERATED_FILE_EXTRA_DEPENDENCIES`` that is used by the ``add_custom_command()`` declarations. This will let us easily change the common dependencies for generating build files in the future.
2016-03-08 18:23:51 +00:00
################################################################################
# Extra dependencies for build rules that use the Python infrastructure to
# generate files used for Z3's build. Changes to these files will trigger
# a rebuild of all the generated files.
################################################################################
Typo Fixes (#6803)
2023-07-09 14:56:10 -04:00
# Note: ``update_api.py`` is deliberately not here because it is not used
[CMake] Refactor the dependency on ``scripts/mk_util.py`` into a list ``Z3_GENERATED_FILE_EXTRA_DEPENDENCIES`` that is used by the ``add_custom_command()`` declarations. This will let us easily change the common dependencies for generating build files in the future.
2016-03-08 18:23:51 +00:00
# to generate every generated file. The targets that need it list it explicitly.
set(Z3_GENERATED_FILE_EXTRA_DEPENDENCIES
Change from BINARY_DIR to PROJECT_BINARY_DIR
2019-05-15 11:25:40 -07:00
"${PROJECT_SOURCE_DIR}/scripts/mk_genfile_common.py"
[CMake] Refactor the dependency on ``scripts/mk_util.py`` into a list ``Z3_GENERATED_FILE_EXTRA_DEPENDENCIES`` that is used by the ``add_custom_command()`` declarations. This will let us easily change the common dependencies for generating build files in the future.
2016-03-08 18:23:51 +00:00
)
Implement a CMake build system. This is a large rework of my first attempt at this (#459). This implementation calls into the recently implemented python scripts to generate the necessary generated ``.h`` and ``.cpp`` files but is independent from Python building system otherwise. Unlike the Python build system, the generated files are emitted into the build tree to avoid polluting the source tree. The build system is setup to refuse to configure if it detects generated files in the source tree. If your source tree is dirty you can run ``git clean -fx`` to clean your working directory. Currently the build succeeds on Linux using CMake 3.4.3 using the "Unix Makefiles" generator with gcc or clang. The following notable features are implemented: * Building of the C and C++ examples and the ``test-z3`` executable. These are included from the ``all`` target so you have to tell the build system (e.g. make) to build them manually. * Install (``make install``) and uninstall (``make uninstall``) of libz3 and its header files. This supports ``DESTDIR`` out of the box because CMake supports it. * An option (``BUILD_LIBZ3_SHARED``) to build libz3 as a static or dynamic library. * Support for using/not using OpenMP (``USE_OPENMP``) * Support for using/not using libgmp (``USE_LIB_GMP``) * Setting the SOVERSION for libz3. I'm not sure if I'm setting the * number correctly though. This is required by Linux distrubtions that wills ship libz3. This needs discussion. The following notable features are currently not implemented and are left for future work. * Support for ARM. * Support for the foci2 library. * Support for creating/installing/uninstalling the dotnet, java, python and ml bindings. * Full support for MSVC. Although I've tried to write the CMake code with MSVC in mind not all the correct flags are passed to it. * Support for using the git hash. This new build system has several advantages other the old build system. * It is easier for outside contributors to contribute to Z3 when the build system is something more standard. * Incremental builds work properly. With the old build system when new code is pulled down the old build directory would need to thrown out and a new fresh build had to be performed because the build system didn't know how to correctly rebuild the project (e.g. couldn't handle new sources being added/removed, compiler flags changing, generated files changing, etc...). This is a MASSIVE boost to productivity! * We now have access rich array of features that CMake provides for building C/C++ projects. This means less time spent implementing custom build system logic in Python that is already supported by CMake. * CMake supports many IDEs out of the box so it should be fairly straight forward to build Z3 with Visual Studio (once support for MSVC is added), Xcode, Eclipse CDT, CLion, ..etc.
2016-02-20 23:21:00 +00:00
################################################################################
# Z3 components, library and executables
################################################################################
Change from BINARY_DIR to PROJECT_BINARY_DIR
2019-05-15 11:25:40 -07:00
include(${PROJECT_SOURCE_DIR}/cmake/z3_add_component.cmake)
include(${PROJECT_SOURCE_DIR}/cmake/z3_append_linker_flag_list_to_target.cmake)
Implement a CMake build system. This is a large rework of my first attempt at this (#459). This implementation calls into the recently implemented python scripts to generate the necessary generated ``.h`` and ``.cpp`` files but is independent from Python building system otherwise. Unlike the Python build system, the generated files are emitted into the build tree to avoid polluting the source tree. The build system is setup to refuse to configure if it detects generated files in the source tree. If your source tree is dirty you can run ``git clean -fx`` to clean your working directory. Currently the build succeeds on Linux using CMake 3.4.3 using the "Unix Makefiles" generator with gcc or clang. The following notable features are implemented: * Building of the C and C++ examples and the ``test-z3`` executable. These are included from the ``all`` target so you have to tell the build system (e.g. make) to build them manually. * Install (``make install``) and uninstall (``make uninstall``) of libz3 and its header files. This supports ``DESTDIR`` out of the box because CMake supports it. * An option (``BUILD_LIBZ3_SHARED``) to build libz3 as a static or dynamic library. * Support for using/not using OpenMP (``USE_OPENMP``) * Support for using/not using libgmp (``USE_LIB_GMP``) * Setting the SOVERSION for libz3. I'm not sure if I'm setting the * number correctly though. This is required by Linux distrubtions that wills ship libz3. This needs discussion. The following notable features are currently not implemented and are left for future work. * Support for ARM. * Support for the foci2 library. * Support for creating/installing/uninstalling the dotnet, java, python and ml bindings. * Full support for MSVC. Although I've tried to write the CMake code with MSVC in mind not all the correct flags are passed to it. * Support for using the git hash. This new build system has several advantages other the old build system. * It is easier for outside contributors to contribute to Z3 when the build system is something more standard. * Incremental builds work properly. With the old build system when new code is pulled down the old build directory would need to thrown out and a new fresh build had to be performed because the build system didn't know how to correctly rebuild the project (e.g. couldn't handle new sources being added/removed, compiler flags changing, generated files changing, etc...). This is a MASSIVE boost to productivity! * We now have access rich array of features that CMake provides for building C/C++ projects. This means less time spent implementing custom build system logic in Python that is already supported by CMake. * CMake supports many IDEs out of the box so it should be fairly straight forward to build Z3 with Visual Studio (once support for MSVC is added), Xcode, Eclipse CDT, CLion, ..etc.
2016-02-20 23:21:00 +00:00
add_subdirectory(src)
[CMake] Implement generation of `Z3Config.cmake` and `Z3Target.cmake` file for the build and install tree. These files allow users of CMake to use Z3 via a CMake config package. Clients can do `find_package(Z3 CONFIG)` to get use the package from their projects. When generating the files for the install tree we try to generate the files so that they are relocatable so that it shouldn't matter if the installed files aren't in the CMAKE_INSTALL_PREFIX when a user consumes them. As long as the relative locations of the files aren't changed things should still work. A new CMake cache variable `CMAKE_INSTALL_Z3_CMAKE_PACKAGE_DIR` has been added so that the install location of the Z3 CMake package files can be controlled. This addresses #915 .
2017-03-03 19:39:53 +00:00
################################################################################
# Create `Z3Config.cmake` and related files for the build tree so clients can
# use Z3 via CMake.
################################################################################
include(CMakePackageConfigHelpers)
remove stale config #2318 thanks @ekpyron Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-07 17:08:22 -07:00
export(EXPORT Z3_EXPORTED_TARGETS
NAMESPACE z3::
FILE "${PROJECT_BINARY_DIR}/Z3Targets.cmake"
)
Change from BINARY_DIR to PROJECT_BINARY_DIR
2019-05-15 11:25:40 -07:00
set(Z3_FIRST_PACKAGE_INCLUDE_DIR "${PROJECT_BINARY_DIR}/src/api")
set(Z3_SECOND_PACKAGE_INCLUDE_DIR "${PROJECT_SOURCE_DIR}/src/api")
set(Z3_CXX_PACKAGE_INCLUDE_DIR "${PROJECT_SOURCE_DIR}/src/api/c++")
[CMake] Implement generation of `Z3Config.cmake` and `Z3Target.cmake` file for the build and install tree. These files allow users of CMake to use Z3 via a CMake config package. Clients can do `find_package(Z3 CONFIG)` to get use the package from their projects. When generating the files for the install tree we try to generate the files so that they are relocatable so that it shouldn't matter if the installed files aren't in the CMAKE_INSTALL_PREFIX when a user consumes them. As long as the relative locations of the files aren't changed things should still work. A new CMake cache variable `CMAKE_INSTALL_Z3_CMAKE_PACKAGE_DIR` has been added so that the install location of the Z3 CMake package files can be controlled. This addresses #915 .
2017-03-03 19:39:53 +00:00
set(AUTO_GEN_MSG "Automatically generated. DO NOT EDIT")
set(CONFIG_FILE_TYPE "build tree")
Change from BINARY_DIR to PROJECT_BINARY_DIR
2019-05-15 11:25:40 -07:00
configure_package_config_file("${PROJECT_SOURCE_DIR}/cmake/Z3Config.cmake.in"
[CMake] Implement generation of `Z3Config.cmake` and `Z3Target.cmake` file for the build and install tree. These files allow users of CMake to use Z3 via a CMake config package. Clients can do `find_package(Z3 CONFIG)` to get use the package from their projects. When generating the files for the install tree we try to generate the files so that they are relocatable so that it shouldn't matter if the installed files aren't in the CMAKE_INSTALL_PREFIX when a user consumes them. As long as the relative locations of the files aren't changed things should still work. A new CMake cache variable `CMAKE_INSTALL_Z3_CMAKE_PACKAGE_DIR` has been added so that the install location of the Z3 CMake package files can be controlled. This addresses #915 .
2017-03-03 19:39:53 +00:00
"Z3Config.cmake"
Change from BINARY_DIR to PROJECT_BINARY_DIR
2019-05-15 11:25:40 -07:00
INSTALL_DESTINATION "${PROJECT_BINARY_DIR}"
[CMake] Implement generation of `Z3Config.cmake` and `Z3Target.cmake` file for the build and install tree. These files allow users of CMake to use Z3 via a CMake config package. Clients can do `find_package(Z3 CONFIG)` to get use the package from their projects. When generating the files for the install tree we try to generate the files so that they are relocatable so that it shouldn't matter if the installed files aren't in the CMAKE_INSTALL_PREFIX when a user consumes them. As long as the relative locations of the files aren't changed things should still work. A new CMake cache variable `CMAKE_INSTALL_Z3_CMAKE_PACKAGE_DIR` has been added so that the install location of the Z3 CMake package files can be controlled. This addresses #915 .
2017-03-03 19:39:53 +00:00
PATH_VARS
Z3_FIRST_PACKAGE_INCLUDE_DIR
Z3_SECOND_PACKAGE_INCLUDE_DIR
Z3_CXX_PACKAGE_INCLUDE_DIR
)
unset(Z3_FIRST_PACKAGE_INCLUDE_DIR)
unset(Z3_SECOND_PACKAGE_INCLUDE_DIR)
unset(Z3_CXX_PACKAGE_INCLUDE_DIR)
unset(AUTO_GEN_MSG)
unset(CONFIG_FILE_TYPE)
Generate Z3ConfigVersion.cmake.
2019-06-08 02:28:36 +02:00
write_basic_package_version_file("${PROJECT_BINARY_DIR}/Z3ConfigVersion.cmake"
COMPATIBILITY SameMajorVersion
)
[CMake] Implement generation of `Z3Config.cmake` and `Z3Target.cmake` file for the build and install tree. These files allow users of CMake to use Z3 via a CMake config package. Clients can do `find_package(Z3 CONFIG)` to get use the package from their projects. When generating the files for the install tree we try to generate the files so that they are relocatable so that it shouldn't matter if the installed files aren't in the CMAKE_INSTALL_PREFIX when a user consumes them. As long as the relative locations of the files aren't changed things should still work. A new CMake cache variable `CMAKE_INSTALL_Z3_CMAKE_PACKAGE_DIR` has been added so that the install location of the Z3 CMake package files can be controlled. This addresses #915 .
2017-03-03 19:39:53 +00:00
Add pkg-config file (#4368) * Add pkg-config file * Copy z3.cmake.in to the Docker for CI
2020-05-22 00:10:41 +08:00
configure_file("${CMAKE_CURRENT_SOURCE_DIR}/z3.pc.cmake.in"
"${CMAKE_CURRENT_BINARY_DIR}/z3.pc" @ONLY)
[CMake] Implement generation of `Z3Config.cmake` and `Z3Target.cmake` file for the build and install tree. These files allow users of CMake to use Z3 via a CMake config package. Clients can do `find_package(Z3 CONFIG)` to get use the package from their projects. When generating the files for the install tree we try to generate the files so that they are relocatable so that it shouldn't matter if the installed files aren't in the CMAKE_INSTALL_PREFIX when a user consumes them. As long as the relative locations of the files aren't changed things should still work. A new CMake cache variable `CMAKE_INSTALL_Z3_CMAKE_PACKAGE_DIR` has been added so that the install location of the Z3 CMake package files can be controlled. This addresses #915 .
2017-03-03 19:39:53 +00:00
################################################################################
# Create `Z3Config.cmake` and related files for install tree so clients can use
# Z3 via CMake.
################################################################################
install(EXPORT
Z3_EXPORTED_TARGETS
FILE "Z3Targets.cmake"
NAMESPACE z3::
DESTINATION "${CMAKE_INSTALL_Z3_CMAKE_PACKAGE_DIR}"
)
Change from BINARY_DIR to PROJECT_BINARY_DIR
2019-05-15 11:25:40 -07:00
set(Z3_INSTALL_TREE_CMAKE_CONFIG_FILE "${PROJECT_BINARY_DIR}/cmake/Z3Config.cmake")
[CMake] Implement generation of `Z3Config.cmake` and `Z3Target.cmake` file for the build and install tree. These files allow users of CMake to use Z3 via a CMake config package. Clients can do `find_package(Z3 CONFIG)` to get use the package from their projects. When generating the files for the install tree we try to generate the files so that they are relocatable so that it shouldn't matter if the installed files aren't in the CMAKE_INSTALL_PREFIX when a user consumes them. As long as the relative locations of the files aren't changed things should still work. A new CMake cache variable `CMAKE_INSTALL_Z3_CMAKE_PACKAGE_DIR` has been added so that the install location of the Z3 CMake package files can be controlled. This addresses #915 .
2017-03-03 19:39:53 +00:00
set(Z3_FIRST_PACKAGE_INCLUDE_DIR "${CMAKE_INSTALL_INCLUDEDIR}")
set(Z3_SECOND_INCLUDE_DIR "")
set(Z3_CXX_PACKAGE_INCLUDE_DIR "")
set(AUTO_GEN_MSG "Automatically generated. DO NOT EDIT")
set(CONFIG_FILE_TYPE "install tree")
# We use `configure_package_config_file()` to try and create CMake files
# that are re-locatable so that it doesn't matter if the files aren't placed
# in the original install prefix.
Change from BINARY_DIR to PROJECT_BINARY_DIR
2019-05-15 11:25:40 -07:00
configure_package_config_file("${PROJECT_SOURCE_DIR}/cmake/Z3Config.cmake.in"
[CMake] Implement generation of `Z3Config.cmake` and `Z3Target.cmake` file for the build and install tree. These files allow users of CMake to use Z3 via a CMake config package. Clients can do `find_package(Z3 CONFIG)` to get use the package from their projects. When generating the files for the install tree we try to generate the files so that they are relocatable so that it shouldn't matter if the installed files aren't in the CMAKE_INSTALL_PREFIX when a user consumes them. As long as the relative locations of the files aren't changed things should still work. A new CMake cache variable `CMAKE_INSTALL_Z3_CMAKE_PACKAGE_DIR` has been added so that the install location of the Z3 CMake package files can be controlled. This addresses #915 .
2017-03-03 19:39:53 +00:00
"${Z3_INSTALL_TREE_CMAKE_CONFIG_FILE}"
INSTALL_DESTINATION "${CMAKE_INSTALL_Z3_CMAKE_PACKAGE_DIR}"
PATH_VARS Z3_FIRST_PACKAGE_INCLUDE_DIR
)
unset(Z3_FIRST_PACKAGE_INCLUDE_DIR)
unset(Z3_SECOND_PACKAGE_INCLUDE_DIR)
unset(Z3_CXX_PACKAGE_INCLUDE_DIR)
unset(AUTO_GEN_MSG)
unset(CONFIG_FILE_TYPE)
# Add install rule to install ${Z3_INSTALL_TREE_CMAKE_CONFIG_FILE}
install(
FILES "${Z3_INSTALL_TREE_CMAKE_CONFIG_FILE}"
DESTINATION "${CMAKE_INSTALL_Z3_CMAKE_PACKAGE_DIR}"
)
Generate Z3ConfigVersion.cmake.
2019-06-08 02:28:36 +02:00
# Add install rule to install ${PROJECT_BINARY_DIR}/Z3ConfigVersion.cmake
install(
FILES "${PROJECT_BINARY_DIR}/Z3ConfigVersion.cmake"
DESTINATION "${CMAKE_INSTALL_Z3_CMAKE_PACKAGE_DIR}"
)
[CMake] Implement generation of `Z3Config.cmake` and `Z3Target.cmake` file for the build and install tree. These files allow users of CMake to use Z3 via a CMake config package. Clients can do `find_package(Z3 CONFIG)` to get use the package from their projects. When generating the files for the install tree we try to generate the files so that they are relocatable so that it shouldn't matter if the installed files aren't in the CMAKE_INSTALL_PREFIX when a user consumes them. As long as the relative locations of the files aren't changed things should still work. A new CMake cache variable `CMAKE_INSTALL_Z3_CMAKE_PACKAGE_DIR` has been added so that the install location of the Z3 CMake package files can be controlled. This addresses #915 .
2017-03-03 19:39:53 +00:00
Add pkg-config file (#4368) * Add pkg-config file * Copy z3.cmake.in to the Docker for CI
2020-05-22 00:10:41 +08:00
# Add install rule to install ${PROJECT_BINARY_DIR}/z3.pc
install(
FILES "${PROJECT_BINARY_DIR}/z3.pc"
DESTINATION "${CMAKE_INSTALL_PKGCONFIGDIR}"
)
Implement a CMake build system. This is a large rework of my first attempt at this (#459). This implementation calls into the recently implemented python scripts to generate the necessary generated ``.h`` and ``.cpp`` files but is independent from Python building system otherwise. Unlike the Python build system, the generated files are emitted into the build tree to avoid polluting the source tree. The build system is setup to refuse to configure if it detects generated files in the source tree. If your source tree is dirty you can run ``git clean -fx`` to clean your working directory. Currently the build succeeds on Linux using CMake 3.4.3 using the "Unix Makefiles" generator with gcc or clang. The following notable features are implemented: * Building of the C and C++ examples and the ``test-z3`` executable. These are included from the ``all`` target so you have to tell the build system (e.g. make) to build them manually. * Install (``make install``) and uninstall (``make uninstall``) of libz3 and its header files. This supports ``DESTDIR`` out of the box because CMake supports it. * An option (``BUILD_LIBZ3_SHARED``) to build libz3 as a static or dynamic library. * Support for using/not using OpenMP (``USE_OPENMP``) * Support for using/not using libgmp (``USE_LIB_GMP``) * Setting the SOVERSION for libz3. I'm not sure if I'm setting the * number correctly though. This is required by Linux distrubtions that wills ship libz3. This needs discussion. The following notable features are currently not implemented and are left for future work. * Support for ARM. * Support for the foci2 library. * Support for creating/installing/uninstalling the dotnet, java, python and ml bindings. * Full support for MSVC. Although I've tried to write the CMake code with MSVC in mind not all the correct flags are passed to it. * Support for using the git hash. This new build system has several advantages other the old build system. * It is easier for outside contributors to contribute to Z3 when the build system is something more standard. * Incremental builds work properly. With the old build system when new code is pulled down the old build directory would need to thrown out and a new fresh build had to be performed because the build system didn't know how to correctly rebuild the project (e.g. couldn't handle new sources being added/removed, compiler flags changing, generated files changing, etc...). This is a MASSIVE boost to productivity! * We now have access rich array of features that CMake provides for building C/C++ projects. This means less time spent implementing custom build system logic in Python that is already supported by CMake. * CMake supports many IDEs out of the box so it should be fairly straight forward to build Z3 with Visual Studio (once support for MSVC is added), Xcode, Eclipse CDT, CLion, ..etc.
2016-02-20 23:21:00 +00:00
################################################################################
# Examples
################################################################################
Fix build on Mac (#6146) * Fix finding Python on Mac On Mac you have to specify the version. It also works well on other platforms this way. * Ignore CMake build directories from index * Fix warning about unused variable in release The variable is used in debug only, but it's legit that the compiler does not warn us for that in release.
2022-07-11 18:46:23 +02:00
cmake_dependent_option(Z3_ENABLE_EXAMPLE_TARGETS
follow up on #2737 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-11-25 08:35:28 -08:00
"Build Z3 api examples" ON
"CMAKE_SOURCE_DIR STREQUAL PROJECT_SOURCE_DIR" OFF)
rename additional build options #2709 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-11-18 20:39:04 -08:00
if (Z3_ENABLE_EXAMPLE_TARGETS)
Implement a CMake build system. This is a large rework of my first attempt at this (#459). This implementation calls into the recently implemented python scripts to generate the necessary generated ``.h`` and ``.cpp`` files but is independent from Python building system otherwise. Unlike the Python build system, the generated files are emitted into the build tree to avoid polluting the source tree. The build system is setup to refuse to configure if it detects generated files in the source tree. If your source tree is dirty you can run ``git clean -fx`` to clean your working directory. Currently the build succeeds on Linux using CMake 3.4.3 using the "Unix Makefiles" generator with gcc or clang. The following notable features are implemented: * Building of the C and C++ examples and the ``test-z3`` executable. These are included from the ``all`` target so you have to tell the build system (e.g. make) to build them manually. * Install (``make install``) and uninstall (``make uninstall``) of libz3 and its header files. This supports ``DESTDIR`` out of the box because CMake supports it. * An option (``BUILD_LIBZ3_SHARED``) to build libz3 as a static or dynamic library. * Support for using/not using OpenMP (``USE_OPENMP``) * Support for using/not using libgmp (``USE_LIB_GMP``) * Setting the SOVERSION for libz3. I'm not sure if I'm setting the * number correctly though. This is required by Linux distrubtions that wills ship libz3. This needs discussion. The following notable features are currently not implemented and are left for future work. * Support for ARM. * Support for the foci2 library. * Support for creating/installing/uninstalling the dotnet, java, python and ml bindings. * Full support for MSVC. Although I've tried to write the CMake code with MSVC in mind not all the correct flags are passed to it. * Support for using the git hash. This new build system has several advantages other the old build system. * It is easier for outside contributors to contribute to Z3 when the build system is something more standard. * Incremental builds work properly. With the old build system when new code is pulled down the old build directory would need to thrown out and a new fresh build had to be performed because the build system didn't know how to correctly rebuild the project (e.g. couldn't handle new sources being added/removed, compiler flags changing, generated files changing, etc...). This is a MASSIVE boost to productivity! * We now have access rich array of features that CMake provides for building C/C++ projects. This means less time spent implementing custom build system logic in Python that is already supported by CMake. * CMake supports many IDEs out of the box so it should be fairly straight forward to build Z3 with Visual Studio (once support for MSVC is added), Xcode, Eclipse CDT, CLion, ..etc.
2016-02-20 23:21:00 +00:00
add_subdirectory(examples)
endif()
[CMake] Teach CMake to build the documentation for the API bindings and install them. The target for building the documentation is `api_docs`. This is off by default but can be enabled with the `BUILD_DOCUMENTATION` option. The C and C++ API documentation is always built but the Python, ".NET", and Java documentation are only built if they are enabled in the build system. The rationale for this is that it would be confusing to install documentation for API bindings that are not installed. By default `ALWAYS_BUILD_DOCS` is on which will slow down builds significantly but will ensure that when the `install` target is invoked the documentation is up-to-date. Unfortunately I couldn't find a better way to do this. `ALWAYS_BUILD_DOCS` can be disabled to get faster builds and still have the `api_docs` target available.
2017-04-25 14:16:14 +01:00
################################################################################
# Documentation
################################################################################
rename additional build options #2709 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-11-18 20:39:04 -08:00
option(Z3_BUILD_DOCUMENTATION "Build API documentation" OFF)
if (Z3_BUILD_DOCUMENTATION)
[CMake] Teach CMake to build the documentation for the API bindings and install them. The target for building the documentation is `api_docs`. This is off by default but can be enabled with the `BUILD_DOCUMENTATION` option. The C and C++ API documentation is always built but the Python, ".NET", and Java documentation are only built if they are enabled in the build system. The rationale for this is that it would be confusing to install documentation for API bindings that are not installed. By default `ALWAYS_BUILD_DOCS` is on which will slow down builds significantly but will ensure that when the `install` target is invoked the documentation is up-to-date. Unfortunately I couldn't find a better way to do this. `ALWAYS_BUILD_DOCS` can be disabled to get faster builds and still have the `api_docs` target available.
2017-04-25 14:16:14 +01:00
message(STATUS "Building documentation enabled")
add_subdirectory(doc)
else()
message(STATUS "Building documentation disabled")
endif()
Copy permalink