[PATCH] D54978: Move the SMT API to LLVM

[Brian Rzycki via Phabricator via cfe-commits]

brzycki added a comment.

In D54978#1392464 <https://reviews.llvm.org/D54978#1392464>, @Szelethus wrote:

> Shouldn't that be off by default?


The default for `LLVM_ENABLE_Z3_SOLVER` depends entirely on what CMake detects from `find_package()`. Here is the relevant code in `llvm/CMakeLists.txt`:

  find_package(Z3 4.7.1)
  ...
  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 `find_package()` idenfiies a suitable `Z3_FOUND` the default is to enable builds with the Z3 framework. In other words the entire Z3 feature is manual opt-out and implicit opt-in when CMake thinks a suitable Z3 library is found.

In D54978#1393552 <https://reviews.llvm.org/D54978#1393552>, @ddcc wrote:

> The likely reason for this versioning problem is that the current versioning implementation in FindZ3.cmake is best-effort only.


Thank you @ddcc for this explanation. If that's the case I'd really prefer if `LLVM_ENABLE_Z3_SOLVER` was explicit opt-in and defaulted to `OFF` regardless of what `find_package` returned.


Repository:
  rC Clang

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

https://reviews.llvm.org/D54978