Move the SMT API to LLVM

Moved everything SMT-related to LLVM and updated the cmake scripts.

Differential Revision: https://reviews.llvm.org/D54978

git-svn-id: https://llvm.org/svn/llvm-project/llvm/trunk@353373 91177308-0d34-0410-b5e6-96231b3b80d8

CMakeLists.txt

@@ -383,6 +383,32 @@ option(LLVM_ENABLE_THREADS "Use threads if available." ON)
 
 option(LLVM_ENABLE_ZLIB "Use zlib for compression/decompression if available." ON)
 
+
+set(LLVM_Z3_INSTALL_DIR "" CACHE STRING "Install directory of the Z3 solver.")
+
+find_package(Z3 4.7.1)
+
+if (LLVM_Z3_INSTALL_DIR)
+  if (NOT Z3_FOUND)
+    message(FATAL_ERROR "Z3 >= 4.7.1 has not been found in LLVM_Z3_INSTALL_DIR: ${LLVM_Z3_INSTALL_DIR}.")
+  endif()
+endif()
+
+set(LLVM_ENABLE_Z3_SOLVER_DEFAULT "${Z3_FOUND}")
+
+option(LLVM_ENABLE_Z3_SOLVER
+  "Enable Support for the Z3 constraint solver in LLVM."
+  ${LLVM_ENABLE_Z3_SOLVER_DEFAULT}
+)
+
+if (LLVM_ENABLE_Z3_SOLVER)
+  if (NOT Z3_FOUND)
+    message(FATAL_ERROR "LLVM_ENABLE_Z3_SOLVER cannot be enabled when Z3 is not available.")
+  endif()
+
+  set(LLVM_WITH_Z3 1)
+endif()
+
 if( LLVM_TARGETS_TO_BUILD STREQUAL "all" )
   set( LLVM_TARGETS_TO_BUILD ${LLVM_ALL_TARGETS} )
 endif()

cmake/modules/FindZ3.cmake

@@ -0,0 +1,51 @@
+# Looking for Z3 in LLVM_Z3_INSTALL_DIR
+find_path(Z3_INCLUDE_DIR NAMES z3.h
+   NO_DEFAULT_PATH
+   PATHS ${LLVM_Z3_INSTALL_DIR}/include
+   PATH_SUFFIXES libz3 z3
+   )
+
+find_library(Z3_LIBRARIES NAMES z3 libz3
+   NO_DEFAULT_PATH
+   PATHS ${LLVM_Z3_INSTALL_DIR}
+   PATH_SUFFIXES lib bin
+   )
+
+find_program(Z3_EXECUTABLE z3
+   NO_DEFAULT_PATH
+   PATHS ${LLVM_Z3_INSTALL_DIR}
+   PATH_SUFFIXES bin
+   )
+
+# If Z3 has not been found in LLVM_Z3_INSTALL_DIR look in the default directories
+find_path(Z3_INCLUDE_DIR NAMES z3.h
+   PATH_SUFFIXES libz3 z3
+   )
+
+find_library(Z3_LIBRARIES NAMES z3 libz3
+   PATH_SUFFIXES lib bin
+   )
+
+find_program(Z3_EXECUTABLE z3
+   PATH_SUFFIXES bin
+   )
+
+if(Z3_INCLUDE_DIR AND Z3_LIBRARIES AND Z3_EXECUTABLE)
+    execute_process (COMMAND ${Z3_EXECUTABLE} -version
+      OUTPUT_VARIABLE libz3_version_str
+      ERROR_QUIET
+      OUTPUT_STRIP_TRAILING_WHITESPACE)
+
+    string(REGEX REPLACE "^Z3 version ([0-9.]+)" "\\1"
+           Z3_VERSION_STRING "${libz3_version_str}")
+    unset(libz3_version_str)
+endif()
+
+# handle the QUIETLY and REQUIRED arguments and set Z3_FOUND to TRUE if
+# all listed variables are TRUE
+include(FindPackageHandleStandardArgs)
+FIND_PACKAGE_HANDLE_STANDARD_ARGS(Z3
+                                  REQUIRED_VARS Z3_LIBRARIES Z3_INCLUDE_DIR
+                                  VERSION_VAR Z3_VERSION_STRING)
+
+mark_as_advanced(Z3_INCLUDE_DIR Z3_LIBRARIES)

cmake/modules/LLVMConfig.cmake.in

@@ -44,6 +44,8 @@ set(LLVM_ENABLE_ZLIB @LLVM_ENABLE_ZLIB@)
 
 set(LLVM_LIBXML2_ENABLED @LLVM_LIBXML2_ENABLED@)
 
+set(LLVM_WITH_Z3 @LLVM_WITH_Z3@)
+
 set(LLVM_ENABLE_DIA_SDK @LLVM_ENABLE_DIA_SDK@)
 
 set(LLVM_NATIVE_ARCH @LLVM_NATIVE_ARCH@)

include/llvm/Config/config.h.cmake

@@ -347,6 +347,9 @@
 /* Whether GlobalISel rule coverage is being collected */
 #cmakedefine01 LLVM_GISEL_COV_ENABLED
 
+/* Define if we have z3 and want to build it */
+#cmakedefine LLVM_WITH_Z3 ${LLVM_WITH_Z3}
+
 /* Define to the default GlobalISel coverage file prefix */
 #cmakedefine LLVM_GISEL_COV_PREFIX "${LLVM_GISEL_COV_PREFIX}"