[PATCH] D54978: Move the SMT API to LLVM

[Mikhail Ramalho via llvm-commits]

Hi,

Thank you for the discussion, I was finally able to reproduce the error.


> Hello @ddcc.
> I agree with your reasoning here and developed a patch based on this line
> of thought:
>
>   diff --git a/llvm/cmake/modules/FindZ3.cmake
> b/llvm/cmake/modules/FindZ3.cmake
>   index 5c6d3f0b427..b213342df37 100644
>   --- a/llvm/cmake/modules/FindZ3.cmake
>   +++ b/llvm/cmake/modules/FindZ3.cmake
>   @@ -39,6 +39,11 @@ if(Z3_INCLUDE_DIR AND Z3_LIBRARIES AND Z3_EXECUTABLE)
>        string(REGEX REPLACE "^Z3 version ([0-9.]+)" "\\1"
>               Z3_VERSION_STRING "${libz3_version_str}")
>        unset(libz3_version_str)
>   +else()
>   +    # The version could not be determined from running Z3_EXECUTABLE.
> Set the
>   +    # version Z3 to the lowest possible value such that all checks for a
>   +    # minimum version will fail.
>   +    set(Z3_VERSION_STRING "0.0.0")
>    endif()
>
>    # handle the QUIETLY and REQUIRED arguments and set Z3_FOUND to TRUE if
>
> 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.
>
>
This seems fine but 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?

Something like:
```
#include <z3.h>

int main()
{
  unsigned int major, minor, build, revision;
  Z3_get_version(&major, &minor, &build, &revision);

  if(major >= 4 && minor >= 7 && build >= 1)
    return EXIT_SUCCESS;

  return EXIT_FAILURE;
}
```

This would be part of FindZ3.cmake and would set Z3_FOUND.

Do you guys think it's possible? I'm almost certain it can be done with
autotools, but I'm clueless when it comes to cmake.

-- 

Mikhail Ramalho.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/llvm-commits/attachments/20190212/f5144ee4/attachment.html>