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 _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
