[PATCH] D54978: Move the SMT API to LLVM

[Dominic Chen via Phabricator via llvm-commits]

ddcc added a comment.

In D54978#1395425 <https://reviews.llvm.org/D54978#1395425>, @brzycki wrote:

> This works for everything I could throw at it. If you think it's reasonable I can open another ticket and have the code reviewed as a separate fix.


Sounds good to me, although I think it'd be good to emit a warning or at least a message about assuming the version due to a missing executable.

In D54978#1395561 <https://reviews.llvm.org/D54978#1395561>, @brzycki wrote:

> I looked at the Z3 source and they do have a `z3_version.h` file now and was added in version 4.4.2.0. You may be able to use the header directly, but I'm not sure how `find_package()` parses for library versions and if this is useful or not.  The generated header is named `src/util/version.h` in this initial commit:
>  https://github.com/Z3Prover/z3/commit/251527603df01904f70ed884f8695fedab5caed9


You're right, it looks like it was originally internal-only, but them became exposed as part of the interface with the second commit, starting around the release of z3 4.8.1. It's been a while since I've used CMake, but perhaps something like this:

  if(Z3_INCLUDE_DIR AND EXISTS "${Z3_INCLUDE_DIR }/z3_version.h")
    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()



In D54978#1395476 <https://reviews.llvm.org/D54978#1395476>, @mikhail.ramalho wrote:

> I'm wondering if we can remove the binary requirement all together: is it possible to run a small program that would return EXIT_SUCCESS if the library is the correct version?


I see other projects do something similar; e.g. https://github.com/SRI-CSL/sally/blob/master/cmake/FindZ3.cmake#L20 . I'm less fond of that approach because it involves even more moving parts, but then again, parsing C header files with regular expressions isn't particularly robust either.


Repository:
  rC Clang

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

https://reviews.llvm.org/D54978