[PATCH] D28952: [analyzer] Add new Z3 constraint manager backend

[Dan Liew via Phabricator via cfe-commits]

delcypher added a comment.

I'm a little late to the review but hopefully I'll have useful comments. Nice work @ddc

> I looked around for a generic smt-lib interface earlier, but couldn't find much available, and since I wanted floating-point arithmetic support, I ended up just directly using the Z3 C interface (the C++ interface uses exceptions, which causes problems). As far as I know, CVC4 doesn't have built-in floating-point support. But longer term, I'd agree that this backend should be made more generic.

FYI I've been working on floating point support in KLEE and have extended it to support floating point (note however only the Z3 backend actually supports consuming floating point constraints). I've not yet open sourced what I've done as I'm not entirely happy with the design but if there is interest we could see if we could figure out a way of pulling `klee::Expr` (and the solver bits) out of KLEE to make a standalone library. Note there is a project called `metaSMT` that uses template meta programming to give the same interface to multiple solvers. KLEE does support it but I'm not familiar with it.

Also using Z3's C interface is the way to go. We also use this in KLEE.


https://reviews.llvm.org/D28952