[PATCH] D54978: Move the SMT API to LLVM

Dan Liew via Phabricator via cfe-commits cfe-commits at lists.llvm.org
Mon Mar 18 08:41:22 PDT 2019


delcypher added a comment.

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

> In D54978#1431935 <https://reviews.llvm.org/D54978#1431935>, @delcypher wrote:
>
> > 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.
>
>
> I've opened https://github.com/Z3Prover/z3/issues/2184 .


Thanks.

> In D54978#1431936 <https://reviews.llvm.org/D54978#1431936>, @delcypher wrote:
> 
>> This output means you built Z3 from source that was not in a git repository. In this case the header file should look the same for both Z3's CMake and Python build systems.
> 
> 
> That's strange, I have been building from a git repository.

Hmm I misread the python code. I inferred that because the extra text from

  def get_full_version_string(major, minor, build, revision):
      global GIT_HASH, GIT_DESCRIBE
      res = "Z3 %s.%s.%s.%s" % (major, minor, build, revision)
      if GIT_HASH:
          res += " " + GIT_HASH
      if GIT_DESCRIBE:
          branch = check_output(['git', 'rev-parse', '--abbrev-ref', 'HEAD'])
          res += " " + branch + " " + check_output(['git', 'describe'])
      return '"' + res + '"'

wasn't in your output. However, I didn't actually check to see how `GIT_HASH` and `GIT_DESCRIBE` are set. It looks like you need to pass `--githash` and `--gitdescribe` respectively to the Python build system configure scripts to get those. They are false by default.
The Z3 CMake build system is different. It will add the git hash and description by default if it detects you're using git ( see https://github.com/Z3Prover/z3/blob/057151c7a80dac44d610f5286799ad7b727b5d2c/CMakeLists.txt#L67 ). You can switch this off by passing
`-DINCLUDE_GIT_HASH=OFF -DINCLUDE_GIT_DESCRIBE=OFF` to the CMake invocation you use when configuring Z3.

> In D54978#1431430 <https://reviews.llvm.org/D54978#1431430>, @mikhail.ramalho wrote:
> 
>> 2. Instead of parsing `Z3_FULL_VERSION`, we can parse `Z3_MAJOR_VERSION`, `Z3_MINOR_VERSION` and `Z3_BUILD_NUMBER` which are also available in the same header.
> 
> 
> Since the differences in version string depending on the build system are intended behavior, it seems (2) would be preferable?

Yeah, that's the way I would go.


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

https://reviews.llvm.org/D54978





More information about the cfe-commits mailing list