diff options
| -rw-r--r-- | cmake/FindCLN.cmake | 3 | ||||
| -rw-r--r-- | cmake/FindCVC4.cmake | 22 | ||||
| -rw-r--r-- | libsolidity/CMakeLists.txt | 15 |
3 files changed, 23 insertions, 17 deletions
diff --git a/cmake/FindCLN.cmake b/cmake/FindCLN.cmake new file mode 100644 index 00000000..f2234bb4 --- /dev/null +++ b/cmake/FindCLN.cmake @@ -0,0 +1,3 @@ +find_library(CLN_LIBRARY NAMES cln) +include(FindPackageHandleStandardArgs) +find_package_handle_standard_args(CLN DEFAULT_MSG CLN_LIBRARY) diff --git a/cmake/FindCVC4.cmake b/cmake/FindCVC4.cmake index 900a123e..2649d7c7 100644 --- a/cmake/FindCVC4.cmake +++ b/cmake/FindCVC4.cmake @@ -4,12 +4,22 @@ if (USE_CVC4) include(FindPackageHandleStandardArgs) find_package_handle_standard_args(CVC4 DEFAULT_MSG CVC4_LIBRARY CVC4_INCLUDE_DIR) if(CVC4_FOUND) - find_library(CLN_LIBRARY NAMES cln) - if(CLN_LIBRARY) - set(CVC4_LIBRARIES ${CVC4_LIBRARY} ${CLN_LIBRARY}) - else() - set(CVC4_LIBRARIES ${CVC4_LIBRARY}) - endif() + # CVC4 may depend on either CLN or GMP. + # We can assume that the one it requires is present on the system, + # so we quietly try to find both and link against them, if they are + # present. + find_package(CLN QUIET) + find_package(GMP QUIET) + + set(CVC4_LIBRARIES ${CVC4_LIBRARY}) + + if (CLN_FOUND) + set(CVC4_LIBRARIES ${CVC4_LIBRARIES} ${CLN_LIBRARY}) + endif () + + if (GMP_FOUND) + set(CVC4_LIBRARIES ${CVC4_LIBRARIES} ${GMP_LIBRARY}) + endif () endif() else() set(CVC4_FOUND FALSE) diff --git a/libsolidity/CMakeLists.txt b/libsolidity/CMakeLists.txt index 872504f3..91a4678a 100644 --- a/libsolidity/CMakeLists.txt +++ b/libsolidity/CMakeLists.txt @@ -11,17 +11,11 @@ else() list(REMOVE_ITEM sources "${CMAKE_CURRENT_SOURCE_DIR}/formal/Z3Interface.cpp") endif() -find_package(GMP QUIET) find_package(CVC4 QUIET) if (${CVC4_FOUND}) - if (${GMP_FOUND}) - include_directories(${CVC4_INCLUDE_DIR}) - add_definitions(-DHAVE_CVC4) - message("CVC4 SMT solver and GMP found. This enables optional SMT checking with CVC4.") - else() - message("CVC4 SMT solver found but its dependency GMP was NOT found. Optional SMT checking with CVC4 will not be available. Please install GMP if it is desired.") - list(REMOVE_ITEM sources "${CMAKE_CURRENT_SOURCE_DIR}/formal/CVC4Interface.cpp") - endif() + include_directories(${CVC4_INCLUDE_DIR}) + add_definitions(-DHAVE_CVC4) + message("CVC4 SMT solver found. This enables optional SMT checking with CVC4.") else() list(REMOVE_ITEM sources "${CMAKE_CURRENT_SOURCE_DIR}/formal/CVC4Interface.cpp") endif() @@ -38,7 +32,6 @@ if (${Z3_FOUND}) target_link_libraries(solidity PUBLIC ${Z3_LIBRARY}) endif() -if (${CVC4_FOUND} AND ${GMP_FOUND}) +if (${CVC4_FOUND}) target_link_libraries(solidity PUBLIC ${CVC4_LIBRARIES}) - target_link_libraries(solidity PUBLIC ${GMP_LIBRARY}) endif() |