aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--cmake/EthCompilerSettings.cmake4
-rw-r--r--cmake/FindCVC4.cmake12
-rw-r--r--cmake/FindZ3.cmake14
-rw-r--r--docs/installing-solidity.rst21
-rw-r--r--libsolidity/CMakeLists.txt3
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})