diff options
| author | Mikhail R. Gadelha <mikhail.ramalho@gmail.com> | 2018-06-04 14:25:58 +0000 |
|---|---|---|
| committer | Mikhail R. Gadelha <mikhail.ramalho@gmail.com> | 2018-06-04 14:25:58 +0000 |
| commit | 9aed45542a597d01c4dcd48ced335ba28bb6063d (patch) | |
| tree | 2fdb45d658ab842c38168643c5246ce2925eeecf /lib/Frontend/CompilerInvocation.cpp | |
| parent | 049a3e3d0cda2ceece1650e3809e7148fc365e9d (diff) | |
| download | clang-9aed45542a597d01c4dcd48ced335ba28bb6063d.tar.gz | |
Created a tiny SMT interface and make Z3ConstraintManager implement it
Summary:
This patch implements a simple SMTConstraintManager API, and requires the implementation of two methods for now: `addRangeConstraints` and `isModelFeasible`.
Update Z3ConstraintManager to inherit it and implement required methods.
I also moved the method to dump the SMT formula from D45517 to this patch.
This patch was created based on the reviews from D47640.
Reviewers: george.karpenkov, NoQ, ddcc, dcoughlin
Reviewed By: george.karpenkov
Differential Revision: https://reviews.llvm.org/D47689
git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@333899 91177308-0d34-0410-b5e6-96231b3b80d8
Diffstat (limited to 'lib/Frontend/CompilerInvocation.cpp')
0 files changed, 0 insertions, 0 deletions