[cfe-dev] SMT API moved to from clang to LLVM

[Mikhail Ramalho via cfe-dev]

Hi all,

As of yesterday, the SMT API was moved to LLVM [0]. Currently, only the
clang static analyzer is using it, but its new location under LLVM makes it
easier to use it in other projects.

The SMT API only supports Z3 right now. I have a fork with other backends
(Boolector, MathSAT, Yices, and CVC4) [0], but the 5 solvers performance
was basically the same, so there was no real reason to upstream them. If
someone needs a specific solver, we can discuss submitting its backend for
review.

The SMT API is not enabled by default; you can enable it by setting the
flag -DLLVM_ENABLE_Z3_SOLVER=ON and cmake will try to find the lib Z3 in
your system. If it's not in a default location, you can pass it using the
flag LLVM_Z3_INSTALL_DIR. You also need Z3 >= 4.7.1.

The API is quite basic right now and only supports encoding bit-vectors,
floating-points, and some casts given a clang AST [2]. If anyone is
interested in using the API and needs help and/or extra features (arrays,
quantifiers, etc.), I'm happy to help.

Thank you,

[0] llvm/include/llvm/Support/SMTAPI.h
[1] https://github.com/mikhailramalho/clang
[2] clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h

-- 

Mikhail Ramalho.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20190327/533a8269/attachment.html>