[PATCH] D88198: Hints CMake where to find Z3 with LLVM_Z3_INSTALL_DIR.

[Ella Ma via Phabricator via llvm-commits]

OikawaKirie abandoned this revision.
OikawaKirie added a comment.

> Yes, it's being used in the FindZ3.cmaks script.

I think I probably have been misled by the configuration method I previously used. In addition, the output notice of "Found Z3: /path/to/libz3.so (xxx)" makes me think I need to set the variable `LLVM_Z3_INSTALL_DIR` to the path of `libz3.so` rather than the path of both libraries and the headers. Especially when I set the variable to the path of `libz3.so` of a higher version but CMake reports that the lower version of Z3 found from the system directory cannot be used, I will become confused about whether the variable is correctly set and used to find Z3.

Maybe it could be better if the variable is documented in `llvm/docs/CMake.rst` after the variable `LLVM_ENABLE_Z3_SOLVER`. Do think the documentation is needed?

> The issue here is that the z3 zip file does not include the cmake scripts, that's why you're unable to configure it by only setting the Z3 directory.

You are correct. In the file `llvm/cmake/modules/FindZ3.cmake`, only file `z3.h` and `libz3.{so|a}` are used, but the directories I tested without the patch has none of these files included. Besides, when I set `LLVM_Z3_INSTALL_DIR` to `/tmp/ella.z3-patch/z3-4.8.9/z3-4.8.9-x64-ubuntu-16.04` directly, which is the directory where the Z3 zip file is unzipped to, the project can also be correctly configured without the patch. There is no problem with the official pre-build Z3 solver binaries and the original LLVM code. It is the problem of the patch. I misled myself.

Thank you for the comments. I will abandon this revision. And if you think the document for the variable `LLVM_Z3_INSTALL_DIR` is required, I will add create another review for the document.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D88198