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

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

xazax.hun added a comment.

Hi!

Just a quick high level question. 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 selves?

Also, LLVM already has a SMT API (https://github.com/llvm/llvm-project/blob/main/llvm/include/llvm/Support/SMTAPI.h). I wonder if it would make sense to have a SAT base class for the SMT API and reuse that here? Specifically, because solvers could be useful for all of the frontends and also optimizations in the backends, it would be great to make sure everyone can benefit from these features. What do you think?


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D120289