[PATCH] D120289: [clang][dataflow] Add SAT solver interface and implementation

Gábor Horváth via Phabricator via cfe-commits cfe-commits at lists.llvm.org
Wed Feb 23 16:07:16 PST 2022


xazax.hun added a comment.

In D120289#3341008 <https://reviews.llvm.org/D120289#3341008>, @sgatev wrote:

> it seems tailored to the Z3 API.

As far as I understand, there were downstream patches that used the same API with other SMT solvers. The authors did not upstream it because they did not see any major improvement on Z3 for any of the use cases.

> What do you think about this? Any other options we should consider?

After reading your analysis, I'm fine with the current approach.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D120289



More information about the cfe-commits mailing list