diff --git a/backends/p4tools/CMakeLists.txt b/backends/p4tools/CMakeLists.txt index 4ae76cf153..2fec824d11 100644 --- a/backends/p4tools/CMakeLists.txt +++ b/backends/p4tools/CMakeLists.txt @@ -34,6 +34,19 @@ project(P4TOOLS VERSION ${P4C_SEM_VERSION_STRING}) # inherit FindLibGc. list(APPEND CMAKE_MODULE_PATH "${CMAKE_CURRENT_SOURCE_DIR}/cmake") +# We need a fairly recent version of Z3. +set(Z3_MIN_VERSION "4.8.14") +# But 4.12+ is currently broken with libGC +set(Z3_MAX_VERSION_EXCL "4.12") +find_package(Z3 ${Z3_MIN_VERSION} REQUIRED) + +if(NOT DEFINED Z3_VERSION_STRING OR ${Z3_VERSION_STRING} VERSION_LESS ${Z3_MIN_VERSION}) + message(FATAL_ERROR "The minimum required Z3 version is ${Z3_MIN_VERSION}. Has ${Z3_VERSION_STRING}.") +endif() +if (${Z3_VERSION_STRING} VERSION_GREATER_EQUAL ${Z3_MAX_VERSION_EXCL}) + message(FATAL_ERROR "The Z3 version has to be lower than ${Z3_MAX_VERSION_EXCL} (the latter currently does no work with libGC). Has ${Z3_VERSION_STRING}.") +endif() + # GSL-lite is needed for testgen. add_subdirectory(submodules/gsl-lite EXCLUDE_FROM_ALL) diff --git a/backends/p4tools/cmake/FindZ3.cmake b/backends/p4tools/cmake/FindZ3.cmake index 0895d85258..d73a2944ad 100644 --- a/backends/p4tools/cmake/FindZ3.cmake +++ b/backends/p4tools/cmake/FindZ3.cmake @@ -6,12 +6,14 @@ find_path( NAMES z3++.h HINTS ${PC_Z3_INCLUDEDIR} ${PC_Z3_INCLUDE_DIRS} PATH_SUFFIXES z3 Z3 + DOC "A path to the directory that contain Z3 include files (e.g. z3.h & z3++.h)." ) find_library( Z3_LIBRARY NAMES z3 HINTS ${PC_Z3_LIBDIR} ${PC_Z3_LIBRARY_DIRS} + DOC "A path to the library file of Z3 (i.e. libz3). This can be dynamic or static library." ) find_program( @@ -51,7 +53,7 @@ if(Z3_FOUND) endif() message(STATUS "Z3 version: ${Z3_VERSION_STRING}") -message(STATUS "Z3 lib dir: ${Z3_LIBRARY}") +message(STATUS "Z3 library: ${Z3_LIBRARY}") message(STATUS "Z3 include dir: ${Z3_INCLUDE_DIR}") # create imported target z3::z3 diff --git a/backends/p4tools/common/CMakeLists.txt b/backends/p4tools/common/CMakeLists.txt index e071df2abe..857c68ae2a 100644 --- a/backends/p4tools/common/CMakeLists.txt +++ b/backends/p4tools/common/CMakeLists.txt @@ -5,14 +5,6 @@ include(common) project(p4tools-common) -# We need a fairly recent version of Z3. -set(Z3_MIN_VERSION "4.8.14") -find_package(Z3 ${Z3_MIN_VERSION} REQUIRED) - -if(NOT DEFINED Z3_VERSION_STRING OR ${Z3_VERSION_STRING} VERSION_LESS ${Z3_MIN_VERSION}) - message(FATAL_ERROR "The minimum required Z3 version is ${Z3_MIN_VERSION}. Has ${Z3_VERSION_STRING}.") -endif() - # Boost filesystem is required for path handling. set(THREADS_PREFER_PTHREAD_FLAG ON) find_package(Threads REQUIRED) @@ -64,7 +56,7 @@ target_link_libraries( PUBLIC gsl-lite PUBLIC ${Boost_SYSTEM_LIBRARY} PUBLIC ${Boost_FILESYSTEM_LIBRARY} - PUBLIC ${Z3_LIBRARY} + PUBLIC z3::z3 ) target_include_directories(