From 6e7d80633da849da13633ca000a05e1573ad509a Mon Sep 17 00:00:00 2001 From: Julian Parsert Date: Tue, 28 Feb 2023 19:44:21 +0000 Subject: [PATCH] Documentation on how to add z3 to CMake project using FetchContent and documentation to recdef function. (#6613) * Added overloaded versions of context::recfun in the c++ api that allow for the declaration of recursive functions where the domain is given by a z3::sort_vector instead of an arity and sort* * added documentation to recdef function * added a section in the README-CMake.md that explains how z3 can be added to a CMake project as a dependency --------- Co-authored-by: Julian Parsert --- README-CMake.md | 31 +++++++++++++++++++++++++++++++ src/api/c++/z3++.h | 8 +++++++- 2 files changed, 38 insertions(+), 1 deletion(-) diff --git a/README-CMake.md b/README-CMake.md index 7b7381107..5845a52c3 100644 --- a/README-CMake.md +++ b/README-CMake.md @@ -90,6 +90,37 @@ CFLAGS="-m32" CXXFLAGS="-m32" CC=gcc CXX=g++ cmake ../ Note like with the ``CC`` and ``CXX`` flags this must be done on the very first invocation to CMake in the build directory. +### Adding Z3 as a dependency to a CMAKE Project + +CMake's [FetchContent](https://cmake.org/cmake/help/latest/module/FetchContent.html) allows +the fetching and populating of an external project. This is useful when a certain version +of z3 is required that may not match with the system version. With the following code in the +cmake file of your project, z3 version 4.12.1 is downloaded to the build directory and the +cmake targets are added to the project: + +``` +FetchContent_Declare(z3 + GIT_REPOSITORY https://github.com/Z3Prover/z3 + GIT_TAG z3-4.12.1 +) +FetchContent_MakeAvailable(z3) +``` + +The header files can be added to the included directories as follows: + +``` +include_directories( ${z3_SOURCE_DIR}/src/api ) +``` + +Finally, the z3 library can be linked to a `yourTarget` using + +``` +target_link_libraries(yourTarget libz3) +``` +Note that this is `libz3` not `z3` (`libz3` refers to the library target from `src/CMakeLists.txt`). + + + ### Ninja [Ninja](https://ninja-build.org/) is a simple build system that is built for speed. diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index f2c0f3f24..52d5e6573 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -366,7 +366,13 @@ namespace z3 { func_decl recfun(char const * name, sort const & domain, sort const & range); func_decl recfun(char const * name, sort const & d1, sort const & d2, sort const & range); - void recdef(func_decl, expr_vector const& args, expr const& body); + /** + * \brief add function definition body to declaration decl. decl needs to be declared using context::. + * @param decl + * @param args + * @param body + */ + void recdef(func_decl decl, expr_vector const& args, expr const& body); func_decl user_propagate_function(symbol const& name, sort_vector const& domain, sort const& range); /**