[PATCH] D54978: Move the SMT API to LLVM

[Brian Rzycki via Phabricator via llvm-commits]

brzycki added a comment.

Here's my proposed logic as actual CMake code. @mikhail.ramalho if you can get your code to emit the version string I made a `TODO` placeholder for it in the 3rd block below.

  diff --git a/llvm/cmake/modules/FindZ3.cmake b/llvm/cmake/modules/FindZ3.cmake
  index 5c6d3f0..f913686 100644
  --- a/llvm/cmake/modules/FindZ3.cmake
  +++ b/llvm/cmake/modules/FindZ3.cmake
  @@ -30,7 +30,23 @@ find_program(Z3_EXECUTABLE z3
      PATH_SUFFIXES bin
      )
   
  -if(Z3_INCLUDE_DIR AND Z3_LIBRARIES AND Z3_EXECUTABLE)
  +# Searching for the version of the Z3 library is a best-effort task. The version
  +# is only recently added to a public header.
  +unset(Z3_VERSION_STRING)
  +
  +if(Z3_INCLUDE_DIR AND EXISTS "${Z3_INCLUDE_DIR}/z3_version.h")
  +    # Z3 4.8.1+ has the version is in a public header.
  +    file(STRINGS "${Z3_INCLUDE_DIR}/z3_version.h"
  +         z3_version_str REGEX "^#define[\t ]+Z3_FULL_VERSION[\t ]+\".*\"")
  +
  +    string(REGEX REPLACE "^.*Z3_FULL_VERSION[\t ]+\"Z3 ([0-9\.]+)\".*$" "\\1"
  +         Z3_VERSION_STRING "${z3_version_str}")
  +    unset(z3_version_str)
  +endif()
  +
  +if(NOT Z3_VERSION_STRING AND (Z3_INCLUDE_DIR AND Z3_LIBRARIES AND
  +                              Z3_EXECUTABLE))
  +    # Run the found z3 executable and parse the version string output.
       execute_process (COMMAND ${Z3_EXECUTABLE} -version
         OUTPUT_VARIABLE libz3_version_str
         ERROR_QUIET
  @@ -41,6 +57,20 @@ if(Z3_INCLUDE_DIR AND Z3_LIBRARIES AND Z3_EXECUTABLE)
       unset(libz3_version_str)
   endif()
   
  +if(NOT Z3_VERSION_STRING AND (Z3_INCLUDE_DIR AND Z3_LIBRARIES))
  +    # We do not have the Z3 binary to query for a version. Try to use
  +    # a small C++ program to detect it via the Z3_get_version() API call.
  +    # TODO: add code from Mikhail Ramalho to obtain the version.
  +    # TODO: set(Z3_VERSION_STRING) if successful.
  +endif()
  +
  +if(NOT Z3_VERSION_STRING)
  +    # Give up: we are unable to obtain a version of the Z3 library. Be
  +    # conservative and force the found version to 0.0.0 to make version
  +    # checks always fail.
  +    set(Z3_VERSION_STRING "0.0.0")
  +endif()
  +


CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D54978/new/

https://reviews.llvm.org/D54978