[PATCH] D54978: Move the SMT API to LLVM

Sat Mar 16 06:33:37 PDT 2019

delcypher added a comment.

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

> The only relevant commit that I can find is https://github.com/Z3Prover/z3/commit/2cb4223979cc94e2ebc4e49a9e83adbdcd2b6979 , but it first landed in z3 4.6.0. It looks like it's specific to CMake though, so is it different if you use the python build? I haven't tried the CMake build.

Hmm this looks like there are some bugs in the different Z3 build systems.

So for the CMake build the value of `Z3_FULL_VERSION_STR` is used to populate the `Z3_FULL_VERSION` macro in the header file. Initially this is `"${Z3_VERSION_MAJOR}.${Z3_VERSION_MINOR}.${Z3_VERSION_PATCH}.${Z3_VERSION_TWEAK}"` but then
If the git has is available we append to it https://github.com/Z3Prover/z3/blob/c0f7afacc497e7e2e1a2a28bcebf1173933f5bab/CMakeLists.txt#L96
and if the git description is available we append to it https://github.com/Z3Prover/z3/blob/c0f7afacc497e7e2e1a2a28bcebf1173933f5bab/CMakeLists.txt#L109
This was my attempt at mimicking the `get_full_version_string()` function ( https://github.com/Z3Prover/z3/blob/038f992ff485d0bf93f962dc9e45330ff1e2e47d/scripts/mk_util.py#L3065 ) when I added Z3's CMake build system.

Unfortunately this doesn't quite match what Z3's python build system does.

- In the python build system the `VER_REVISION` global (used to set `Z3_REVISION_NUMBER` macro and is the forth integer in `Z3_FULL_VERSION`, i.e. `d` in `a.b.c.d`)  tries to count the number of commits reachable from the current git `HEAD` (see https://github.com/Z3Prover/z3/blob/038f992ff485d0bf93f962dc9e45330ff1e2e47d/scripts/mk_util.py#L561 ). The CMake build system doesn't mimic this. Personally I don't think the python build system makes sense here at all given that this integer goes in the 4th position in the version output (i.e. `d` in `a.b.c.d`).

- In the CMake build system the 4th integer in `Z3_FULL_VERSION` is always whatever `Z3_VERSION_TWEAK` is set to in the root `CMakeLists.txt` file. So far, I think has always been `0`.

So the bug here is that the CMake and python build systems don't agree on the meaning of the 4th version field. Personally I think the implementation of Z3's CMake build system makes more sense given where it is placed in the version string but that means the name `Z3_REVISION_NUMBER` macro name isn't very appropriate.

None of this really mattered until the version header file became public

Would one of you be able to file a bug against Z3 to fix this? I am no longer in a position to contribute to Z3 so I can't do this.

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

https://reviews.llvm.org/D54978