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

[Gábor Horváth via Phabricator via cfe-commits]

xazax.hun added a comment.

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

>> I wonder if it would make sense to have a SAT base class for the SMT API and reuse that here?
>
> I think that on a high level we can either 1) integrate the SMT API types deeply into the dataflow framework and use that solver interface directly or 2) have a layer that translates from the dataflow `BoolValue` types to the SMT API types. At this point I'm not convinced that we should go for 1).

Could you elaborate on what would be the main disadvantage of using 1)? (The advantage would be that we could switch to Z3 any time.)


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D120289