sgatev added a comment. In D120289#3338262 <https://reviews.llvm.org/D120289#3338262>, @xazax.hun wrote:
> 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 very easily switch to Z3 any time.) Let me clarify 1) because I see two options there as well: 1.a) We replace the `BoolValue` hierarchy in the dataflow framework with `SMTExprRef`. This feels too committal. The dataflow interfaces are still not sufficiently developed and there isn't a clear benefit (e.g. performance) with this approach so I'd rather not couple them for now. There might also be benefits to having a structured representation (as opposed to using opaque values such as `SMTExprRef`) that we need to consider. I think this is a viable long-term option, though. 1.b) We add an `SMTExprRef` member to each boolean value (atom, conjunction, disjunction, and negation) in the dataflow framework. I like this better than 1.a). The main disadvantage I see is that `SMTSolver` is a huge interface and on the surface it seems tailored to the Z3 API. From that perspective it also feels more committal than necessary, given that we can make do with a simple one-method interface for now. I think this is a good long-term option if we think the SMT API is the most appropriate solver interface. I find 2) least committal as it keeps the dataflow framework and the solver separate. For a simple integration with Z3 I can provide an implementation of `clang::dataflow::Solver` using the SMT API. That should boil down to translating dataflow types to SMT types. What do you think about this? Any other options we should consider? Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D120289/new/ https://reviews.llvm.org/D120289 _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
