diff options
| -rw-r--r-- | cmake/EthCompilerSettings.cmake | 4 | ||||
| -rw-r--r-- | cmake/FindCVC4.cmake | 12 | ||||
| -rw-r--r-- | cmake/FindZ3.cmake | 14 | ||||
| -rw-r--r-- | docs/installing-solidity.rst | 21 | ||||
| -rw-r--r-- | libsolidity/CMakeLists.txt | 3 |
5 files changed, 43 insertions, 11 deletions
diff --git a/cmake/EthCompilerSettings.cmake b/cmake/EthCompilerSettings.cmake index 515057fa..76268626 100644 --- a/cmake/EthCompilerSettings.cmake +++ b/cmake/EthCompilerSettings.cmake @@ -166,6 +166,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) diff --git a/cmake/FindCVC4.cmake b/cmake/FindCVC4.cmake index 0fb13196..90b7ebd5 100644 --- a/cmake/FindCVC4.cmake +++ b/cmake/FindCVC4.cmake @@ -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() diff --git a/cmake/FindZ3.cmake b/cmake/FindZ3.cmake index 971d3b4b..704f367e 100644 --- a/cmake/FindZ3.cmake +++ b/cmake/FindZ3.cmake @@ -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. - diff --git a/docs/installing-solidity.rst b/docs/installing-solidity.rst index 5b3fdf87..41204bba 100644 --- a/docs/installing-solidity.rst +++ b/docs/installing-solidity.rst @@ -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 ============================ diff --git a/libsolidity/CMakeLists.txt b/libsolidity/CMakeLists.txt index 706b3b08..49095fff 100644 --- a/libsolidity/CMakeLists.txt +++ b/libsolidity/CMakeLists.txt @@ -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}) |