cerc-io/solidity
16
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Do not force GMP to be present as dependency of CVC4, but also allow CLN instead.

Browse Source
This commit is contained in:
Daniel Kirchner 2018-08-08 17:23:15 +02:00
parent 9b4546c487
commit c7a0f44159
3 changed files with 23 additions and 17 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
cmake/FindCLN.cmake Normal file
View File

@ -0,0 +1,3 @@
find_library(CLN_LIBRARY NAMES cln)
include(FindPackageHandleStandardArgs)
find_package_handle_standard_args(CLN DEFAULT_MSG CLN_LIBRARY)

22
cmake/FindCVC4.cmake
View File

@ -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)

15
libsolidity/CMakeLists.txt
View File

@ -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()