SMTChecker: Switch CVC4 from API to SMT-LIB2 interface

Instead of compiling `solc` itself with CVC4 support, it is now enough
to have `cvc4` executable on PATH when running the compiler.
Instead of using API of CVC4, we write the queries to temporary SMT-LIB2
files and call the solver process directly to run on the file.

Author: blishko

CMakeLists.txt

@@ -131,15 +131,15 @@ elseif (${Z3_FOUND})
   message("Z3 SMT solver found. This enables optional SMT checking with Z3.")
 endif()
 
-find_package(CVC4 QUIET)
-if (${CVC4_FOUND})
-  add_definitions(-DHAVE_CVC4)
+find_program(CVC4_PATH cvc4)
+if (CVC4_PATH)
+  add_compile_definitions(CVC4_PATH=${CVC4_PATH})
   message("CVC4 SMT solver found. This enables optional SMT checking with CVC4.")
 endif()
 
-if (NOT (${Z3_FOUND} OR ${CVC4_FOUND}))
+if (NOT (${Z3_FOUND} OR CVC4_PATH))
   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).")
+  \nPlease install Z3 or CVC4 or remove the option disabling them (USE_Z3).")
 endif()
 
 add_subdirectory(libsolutil)

cmake/EthCompilerSettings.cmake

@@ -266,7 +266,6 @@ option(USE_Z3 "Allow compiling with Z3 SMT solver integration" ON)
 if(UNIX AND NOT APPLE)
 	option(USE_Z3_DLOPEN "Dynamically load the Z3 SMT solver instead of linking against it." OFF)
 endif()
-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)

cmake/FindCVC4.cmake

@@ -336,10 +336,7 @@ The following are dependencies for all builds of Solidity:
 +-----------------------------------+-------------------------------------------------------+
 | `z3`_ (version 4.8.16+, Optional) | For use with SMT checker.                             |
 +-----------------------------------+-------------------------------------------------------+
-| `cvc4`_ (Optional)                | For use with SMT checker.                             |
-+-----------------------------------+-------------------------------------------------------+
 
-.. _cvc4: https://cvc4.cs.stanford.edu/web/
 .. _Git: https://git-scm.com/download
 .. _Boost: https://www.boost.org
 .. _CMake: https://cmake.org/download/
@@ -546,12 +543,6 @@ Inside the build folder you can disable them, since they are enabled by default:
     # 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
 ============================
 

docs/installing-solidity.rst

@@ -825,7 +825,7 @@ The user can choose which solvers should be used, if available, via the CLI
 option ``--model-checker-solvers {all,cvc4,eld,smtlib2,z3}`` or the JSON option
 ``settings.modelChecker.solvers=[smtlib2,z3]``, where:
 
-- ``cvc4`` is only available if the ``solc`` binary is compiled with it. Only BMC uses ``cvc4``.
+- ``cvc4`` is used via its binary which must be installed in the system. Only BMC uses ``cvc4``.
 - ``eld`` is used via its binary which must be installed in the system. Only CHC uses ``eld``, and only if ``z3`` is not enabled.
 - ``smtlib2`` outputs SMT/Horn queries in the `smtlib2 <http://smtlib.cs.uiowa.edu/>`_ format.
   These can be used together with the compiler's `callback mechanism <https://github.com/ethereum/solc-js>`_ so that

docs/smtchecker.rst

@@ -20,12 +20,6 @@ else()
   set(z3_SRCS)
 endif()
 
-if (${CVC4_FOUND})
-  set(cvc4_SRCS CVC4Interface.cpp CVC4Interface.h)
-else()
-  set(cvc4_SRCS)
-endif()
-
 if (${USE_Z3_DLOPEN})
   file(GLOB Z3_HEADERS ${Z3_HEADER_PATH}/z3*.h)
   set(Z3_WRAPPER ${CMAKE_CURRENT_BINARY_DIR}/z3wrapper.cpp)
@@ -38,7 +32,7 @@ if (${USE_Z3_DLOPEN})
   set(z3_SRCS ${z3_SRCS} ${Z3_WRAPPER} Z3Loader.cpp Z3Loader.h)
 endif()
 
-add_library(smtutil ${sources} ${z3_SRCS} ${cvc4_SRCS})
+add_library(smtutil ${sources} ${z3_SRCS})
 target_link_libraries(smtutil PUBLIC solutil Boost::boost)
 
 if (${USE_Z3_DLOPEN})
@@ -47,7 +41,3 @@ if (${USE_Z3_DLOPEN})
 elseif (${Z3_FOUND})
   target_link_libraries(smtutil PUBLIC z3::libz3)
 endif()
-
-if (${CVC4_FOUND})
-  target_link_libraries(smtutil PUBLIC CVC4::CVC4)
-endif()