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

Merge pull request #4665 from mattaereal/cmake-patch-solver

Browse Source 
cmake option added to make solvers optional
This commit is contained in:
Alex Beregszaszi 2018-08-08 17:58:01 +01:00 committed by GitHub
commit 551343ae3e
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
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

@ -159,6 +159,10 @@ if(COVERAGE)
add_compile_options(-g --coverage)
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"))
option(USE_LD_GOLD "Use GNU gold linker" ON)
if (USE_LD_GOLD)

12
cmake/FindCVC4.cmake
View File

@ -1,4 +1,8 @@
find_path(CVC4_INCLUDE_DIR cvc4/cvc4.h)
find_library(CVC4_LIBRARY NAMES cvc4 )
include(FindPackageHandleStandardArgs)
find_package_handle_standard_args(CVC4 DEFAULT_MSG CVC4_LIBRARY CVC4_INCLUDE_DIR)
if (USE_CVC4)
find_path(CVC4_INCLUDE_DIR cvc4/cvc4.h)
find_library(CVC4_LIBRARY NAMES cvc4 )
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)
find_library(Z3_LIBRARY NAMES z3 )
include(FindPackageHandleStandardArgs)
find_package_handle_standard_args(Z3 DEFAULT_MSG Z3_LIBRARY Z3_INCLUDE_DIR)
if (USE_Z3)
find_path(Z3_INCLUDE_DIR z3++.h)
find_library(Z3_LIBRARY NAMES z3 )
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.

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``.
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
============================

3
libsolidity/CMakeLists.txt
View File

@ -27,7 +27,8 @@ else()
endif()
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()
add_library(solidity ${sources} ${headers})