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

[Stanislav Gatev via Phabricator via cfe-commits]

sgatev added a comment.

> Did you look into reusing existing SAT solvers like miniSAT? What was the main reason for rolling our own instead of picking something up off the shelves?

Mainly to provide a lightweight out-of-the-box alternative. The solver interface is simple so one should be able to roll out an implementation for their favorite solver with little effort. One concrete use case that I have in mind for this solver implementation is unit tests, but we've also used it successfully to analyze a large codebase.

> 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). For 2) we can simply provide an adapter that implements the dataflow solver API using the SMT API. This way the dataflow framework can be used with SMT API-compatible solvers. What do you think?


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D120289