This is an archive of the discontinued LLVM Phabricator instance.

[analyzer] Moved all CSA code from the SMT API to a new header, `SMTConv.h`. NFC.
ClosedPublic

Authored by mikhail.ramalho on Aug 15 2018, 5:29 AM.

Details

Summary

With this patch, the SMT backend is almost completely detached from the CSA.

Unfortunate consequence is that we missed the ConditionTruthVal from the CSA and had to use Optional<bool>.

The Z3 solver implementation is still in the same file as the Z3ConstraintManager, in lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp though, but except for that, the SMT API can be moved to anywhere in the codebase.

Diff Detail

Event Timeline

Makes sense. Another approach would have been to add state to SMTConv and have it reference the solver, but your way also works.

This revision is now accepted and ready to land.Aug 21 2018, 10:59 AM
This revision was automatically updated to reflect the committed changes.