cmake flags to make solvers optional. Implementation of #4651

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