From 779af1cf7724335ba8b3cfdc2e2861e843488e27 Mon Sep 17 00:00:00 2001 From: Julian Parsert Date: Fri, 10 Feb 2023 17:41:51 +0000 Subject: [PATCH 1/3] 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* --- src/api/c++/z3++.h | 25 +++++++++++++++++++++++++ 1 file changed, 25 insertions(+) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 3f47b6637ba..ac47d7d06d1 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -359,6 +359,8 @@ namespace z3 { func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & d4, sort const & d5, sort const & range); func_decl recfun(symbol const & name, unsigned arity, sort const * domain, sort const & range); + func_decl recfun(symbol const & name, const sort_vector& domain, sort const & range); + func_decl recfun(char const * name, sort_vector const& domain, sort const & range); func_decl recfun(char const * name, unsigned arity, sort const * domain, sort const & range); 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); @@ -2710,6 +2712,16 @@ namespace z3 { void set(char const * k, double v) { params p(ctx()); p.set(k, v); set(p); } void set(char const * k, symbol const & v) { params p(ctx()); p.set(k, v); set(p); } void set(char const * k, char const* v) { params p(ctx()); p.set(k, v); set(p); } + /** + \brief Create a backtracking point. + + The solver contains a stack of assertions. + + \sa Z3_solver_get_num_scopes + \sa Z3_solver_pop + + def_API('Z3_solver_push', VOID, (_in(CONTEXT), _in(SOLVER))) + */ void push() { Z3_solver_push(ctx(), m_solver); check_error(); } void pop(unsigned n = 1) { Z3_solver_pop(ctx(), m_solver, n); check_error(); } void reset() { Z3_solver_reset(ctx(), m_solver); check_error(); } @@ -3561,6 +3573,19 @@ namespace z3 { } + inline func_decl context::recfun(symbol const & name, sort_vector const& domain, sort const & range) { + check_context(domain, range); + array domain1(domain); + Z3_func_decl f = Z3_mk_rec_func_decl(m_ctx, name, domain1.size(), domain1.ptr(), range); + check_error(); + return func_decl(*this, f); + } + + inline func_decl context::recfun(char const * name, sort_vector const& domain, sort const & range) { + return recfun(str_symbol(name), domain, range); + + } + inline func_decl context::recfun(char const * name, unsigned arity, sort const * domain, sort const & range) { return recfun(str_symbol(name), arity, domain, range); } From 9baa5867c8af8cc4352a8ffca53bad0aca058dc9 Mon Sep 17 00:00:00 2001 From: Julian Parsert Date: Mon, 13 Feb 2023 22:30:38 +0000 Subject: [PATCH 2/3] added documentation to recdef function --- src/api/c++/z3++.h | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index f2c0f3f243e..52d5e657394 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); /** From 4cb586397ae2acb4790955aad10c3660d8022822 Mon Sep 17 00:00:00 2001 From: Julian Parsert Date: Tue, 28 Feb 2023 19:12:51 +0000 Subject: [PATCH 3/3] added a section in the README-CMake.md that explains how z3 can be added to a CMake project as a dependency --- README-CMake.md | 31 +++++++++++++++++++++++++++++++ 1 file changed, 31 insertions(+) diff --git a/README-CMake.md b/README-CMake.md index 7b7381107f2..5845a52c372 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.