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

cmake flags to make solvers optional. Implementation of #4651

Browse Source
This commit is contained in:
Matías Aereal Aeón 2018-08-08 11:46:17 -03:00
parent 009a55c82d
commit 4b20708c49
5 changed files with 43 additions and 11 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
cmake/EthCompilerSettings.cmake
View File

@ -166,6 +166,10 @@ if(COVERAGE)
add_compile_options(-g --coverage) add_compile_options(-g --coverage)
endif() endif()
# SMT Solvers integration
option(USE_Z3 "Allow compiling with Z3 SMT solver integration" ON)
option(USE_CVC4 "Allow compiling with CVC4 SMT solver integration" ON)
if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU") OR ("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang")) if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU") OR ("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang"))
option(USE_LD_GOLD "Use GNU gold linker" ON) option(USE_LD_GOLD "Use GNU gold linker" ON)
if (USE_LD_GOLD) if (USE_LD_GOLD)

12
cmake/FindCVC4.cmake
View File

@ -1,4 +1,8 @@
find_path(CVC4_INCLUDE_DIR cvc4/cvc4.h) if (USE_CVC4)
find_library(CVC4_LIBRARY NAMES cvc4 ) find_path(CVC4_INCLUDE_DIR cvc4/cvc4.h)
include(FindPackageHandleStandardArgs) find_library(CVC4_LIBRARY NAMES cvc4 )
find_package_handle_standard_args(CVC4 DEFAULT_MSG CVC4_LIBRARY CVC4_INCLUDE_DIR) include(FindPackageHandleStandardArgs)
find_package_handle_standard_args(CVC4 DEFAULT_MSG CVC4_LIBRARY CVC4_INCLUDE_DIR)
else()
set(CVC4_FOUND FALSE)
endif()

14
cmake/FindZ3.cmake
View File

@ -1,7 +1,9 @@
find_path(Z3_INCLUDE_DIR z3++.h) if (USE_Z3)
find_library(Z3_LIBRARY NAMES z3 ) find_path(Z3_INCLUDE_DIR z3++.h)
include(FindPackageHandleStandardArgs) find_library(Z3_LIBRARY NAMES z3 )
find_package_handle_standard_args(Z3 DEFAULT_MSG Z3_LIBRARY Z3_INCLUDE_DIR) include(FindPackageHandleStandardArgs)
find_package_handle_standard_args(Z3 DEFAULT_MSG Z3_LIBRARY Z3_INCLUDE_DIR)
else()
set(Z3_FOUND FALSE)
endif()
# TODO: Create IMPORTED library for Z3. # TODO: Create IMPORTED library for Z3.

21
docs/installing-solidity.rst
View File

@ -300,6 +300,27 @@ CMake options
If you are interested what CMake options are available run ``cmake .. -LH``. If you are interested what CMake options are available run ``cmake .. -LH``.
SMT Solvers
-----------
Solidity can be built against SMT solvers and will do so by default if
they are found in the system. Each solver can be disabled by a `cmake` option.
*Note: In some cases, this can also be a potential workaround for build failures.*
Inside the build folder you can disable them, since they are enabled by default:
.. code:: bash
# disables only Z3 SMT Solver.
cmake .. -DUSE_Z3=OFF
# disables only CVC4 SMT Solver.
cmake .. -DUSE_CVC4=OFF
# disables both Z3 and CVC4
cmake .. -DUSE_CVC4=OFF -DUSE_Z3=OFF
The version string in detail The version string in detail
============================ ============================

3
libsolidity/CMakeLists.txt
View File

@ -27,7 +27,8 @@ else()
endif() endif()
if (NOT (${Z3_FOUND} OR ${CVC4_FOUND})) if (NOT (${Z3_FOUND} OR ${CVC4_FOUND}))
message("No SMT solver found. Optional SMT checking will not be available. Please install Z3 or CVC4 if it is desired.") message("No SMT solver found (or it has been forcefully disabled). Optional SMT checking will not be available.\
\nPlease install Z3 or CVC4 or remove the option disabling them (USE_Z3, USE_CVC4).")
endif() endif()
add_library(solidity ${sources} ${headers}) add_library(solidity ${sources} ${headers})