[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 .

CMakeLists.txt

@@ -398,10 +398,18 @@ set(CMAKE_INSTALL_PKGCONFIGDIR
   PATH
   "Directory to install pkgconfig files"
 )
+
+set(CMAKE_INSTALL_Z3_CMAKE_PACKAGE_DIR
+  "${CMAKE_INSTALL_LIBDIR}/cmake/z3"
+  CACHE
+  PATH
+  "Directory to install Z3 CMake package files"
+)
 message(STATUS "CMAKE_INSTALL_LIBDIR: \"${CMAKE_INSTALL_LIBDIR}\"")
 message(STATUS "CMAKE_INSTALL_BINDIR: \"${CMAKE_INSTALL_BINDIR}\"")
 message(STATUS "CMAKE_INSTALL_INCLUDEDIR: \"${CMAKE_INSTALL_INCLUDEDIR}\"")
 message(STATUS "CMAKE_INSTALL_PKGCONFIGDIR: \"${CMAKE_INSTALL_PKGCONFIGDIR}\"")
+message(STATUS "CMAKE_INSTALL_Z3_CMAKE_PACKAGE_DIR: \"${CMAKE_INSTALL_Z3_CMAKE_PACKAGE_DIR}\"")
 
 ################################################################################
 # Uninstall rule
@@ -449,6 +457,76 @@ include(${CMAKE_SOURCE_DIR}/cmake/z3_add_component.cmake)
 include(${CMAKE_SOURCE_DIR}/cmake/z3_append_linker_flag_list_to_target.cmake)
 add_subdirectory(src)
 
+################################################################################
+# Create `Z3Config.cmake` and related files for the build tree so clients can
+# use Z3 via CMake.
+################################################################################
+include(CMakePackageConfigHelpers)
+export(EXPORT Z3_EXPORTED_TARGETS
+  NAMESPACE z3::
+  FILE "${CMAKE_BINARY_DIR}/Z3Targets.cmake"
+)
+set(Z3_FIRST_PACKAGE_INCLUDE_DIR "${CMAKE_BINARY_DIR}/src/api")
+set(Z3_SECOND_PACKAGE_INCLUDE_DIR "${CMAKE_SOURCE_DIR}/src/api")
+set(Z3_CXX_PACKAGE_INCLUDE_DIR "${CMAKE_SOURCE_DIR}/src/api/c++")
+set(AUTO_GEN_MSG "Automatically generated. DO NOT EDIT")
+set(CONFIG_FILE_TYPE "build tree")
+configure_package_config_file("${CMAKE_SOURCE_DIR}/cmake/Z3Config.cmake.in"
+  "Z3Config.cmake"
+  INSTALL_DESTINATION "${CMAKE_BINARY_DIR}"
+  PATH_VARS
+    Z3_FIRST_PACKAGE_INCLUDE_DIR
+    Z3_SECOND_PACKAGE_INCLUDE_DIR
+    Z3_CXX_PACKAGE_INCLUDE_DIR
+  INSTALL_PREFIX "${CMAKE_BINARY_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)
+# TODO: Provide a `Z3Version.cmake` file so that clients can specify the version
+# of Z3 they want.
+
+################################################################################
+# 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}"
+)
+set(Z3_INSTALL_TREE_CMAKE_CONFIG_FILE "${CMAKE_BINARY_DIR}/cmake/Z3Config.cmake")
+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.
+configure_package_config_file("${CMAKE_SOURCE_DIR}/cmake/Z3Config.cmake.in"
+  "${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}"
+)
+
+# TODO: Provide a `Z3Version.cmake` file so that clients can specify the version
+# of Z3 they want.
+
 ################################################################################
 # Examples
 ################################################################################

README-CMake.md

@@ -267,6 +267,7 @@ The following useful options can be passed to CMake whilst configuring.
 * ``CMAKE_INSTALL_PREFIX`` - STRING. The install prefix to use (e.g. ``/usr/local/``).
 * ``CMAKE_INSTALL_PKGCONFIGDIR`` - STRING. The path to install pkgconfig files.
 * ``CMAKE_INSTALL_PYTHON_PKG_DIR`` - STRING. The path to install the z3 python bindings. This can be relative (to ``CMAKE_INSTALL_PREFIX``) or absolute.
+* ``CMAKE_INSTALL_Z3_CMAKE_PACKAGE_DIR`` - STRING. The path to install CMake package files (e.g. ``/usr/lib/cmake/z3``).
 * ``ENABLE_TRACING_FOR_NON_DEBUG`` - BOOL. If set to ``TRUE`` enable tracing in non-debug builds, if set to ``FALSE`` disable tracing in non-debug builds. Note in debug builds tracing is always enabled.
 * ``BUILD_LIBZ3_SHARED`` - BOOL. If set to ``TRUE`` build libz3 as a shared library otherwise build as a static library.
 * ``ENABLE_EXAMPLE_TARGETS`` - BOOL. If set to ``TRUE`` add the build targets for building the API examples.

contrib/cmake/cmake/Z3Config.cmake.in

@@ -0,0 +1,30 @@
+################################################################################
+# @AUTO_GEN_MSG@
+#
+# This file is intended to be consumed by clients who wish to use Z3 from CMake.
+# It can be use by doing `find_package(Z3 config)` from within a
+# `CMakeLists.txt` file. If CMake doesn't find this package automatically you
+# can give it a hint by passing `-DZ3_DIR=<path>` to the CMake invocation where
+# `<path>` is the path to the directory containing this file.
+#
+# This file was built for the @CONFIG_FILE_TYPE@.
+################################################################################
+
+# Exported targets
+include("${CMAKE_CURRENT_LIST_DIR}/Z3Targets.cmake")
+
+@PACKAGE_INIT@
+
+# Version information
+set(Z3_VERSION_MAJOR @Z3_VERSION_MAJOR@)
+set(Z3_VERSION_MINOR @Z3_VERSION_MINOR@)
+set(Z3_VERSION_PATCH @Z3_VERSION_PATCH@)
+set(Z3_VERSION_TWEAK @Z3_VERSION_TWEAK@)
+set(Z3_VERSION_STRING "${Z3_VERSION_MAJOR}.${Z3_VERSION_MINOR}.${Z3_VERSION_PATCH}.${Z3_VERSION_TWEAK}")
+
+# NOTE: We can't use `set_and_check()` here because this a list of paths.
+# List of include directories
+set(Z3_C_INCLUDE_DIRS @PACKAGE_Z3_FIRST_PACKAGE_INCLUDE_DIR@ @PACKAGE_Z3_SECOND_PACKAGE_INCLUDE_DIR@)
+set(Z3_CXX_INCLUDE_DIRS @PACKAGE_Z3_CXX_PACKAGE_INCLUDE_DIR@ ${Z3_C_INCLUDE_DIRS})
+# List of libraries to link against
+set(Z3_LIBRARIES "z3::libz3")

contrib/cmake/src/CMakeLists.txt

@@ -168,6 +168,7 @@ foreach (header ${libz3_public_headers})
 endforeach()
 
 install(TARGETS libz3
+  EXPORT Z3_EXPORTED_TARGETS
   LIBRARY DESTINATION "${CMAKE_INSTALL_LIBDIR}"
   ARCHIVE DESTINATION "${CMAKE_INSTALL_LIBDIR}" # On Windows this installs ``libz3.lib`` which CMake calls the "corresponding import library". Do we want this installed?
   RUNTIME DESTINATION "${CMAKE_INSTALL_LIBDIR}" # For Windows. DLLs are runtime targets for CMake