Create a include folder

[illera88]

Hi,

I realized that there is no include folder in the source code tree but it does exists in the Release file.

Shouldn't a include directory with the .h be created to easy things to developers that uses z3 in their projects and compile it from the source?

Thank you

[NikolajBjorner]

Relevant include files are copied from src/api and src/api/c++
You could perhaps replace a src/include directive by using these two directory paths if you use Z3 from sources.

If you disagree, then one approach is to update the build scripts (currently we have two, one based on cmake and one based on python, the latter preferrably deprecated) to create an include directory. If you have bandwidth you are welcome add a pull request. The path of least resistance seems to me to just include src/api and src/api/c++.

[illera88]

Can you point me to the line in the CMakeLists.txt where the build script is?

I think that creating a single include directory (like in the release packages) is the best way to do so.

Actually normally that's what every C/C++ project has

[NikolajBjorner]

Line 636 in https://github.com/Z3Prover/z3/blob/master/CMakeLists.txt
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++")

I can't locate relevant locations for the legacy build system though.

[NikolajBjorner]

Here is some more detail.

We already export all the information a C/C++ project (that uses CMake) needs when Z3 is built with CMake in a file called Z3Config.cmake. The template for this file can be found at https://github.com/Z3Prover/z3/blob/master/cmake/Z3Config.cmake.in.

We generate two versions of this file. One that goes in the root of the Z3 build directory which allows an external project to use Z3 directly from a build tree (i.e. installing Z3 is not necessary). The other gets installed when Z3 gets installed (e.g. ninja install).

We have two example consumers of the Z3Config.cmake file. First the C example project https://github.com/Z3Prover/z3/blob/master/examples/c/CMakeLists.txt and the example C++ project as well. This is how the C and C++ example projects are currently tested in TravisCI.