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 | 735d8ea0d480cea946a1d41bfbf515a834afcebc (patch) | |
| tree | a8c5866b10ec1848793ed21591557c3fc17f85bc /llvm/lib/TableGen/TGParser.cpp | |
| parent | 9438b1594609529e6f2ed49da9b271ac3bd474f7 (diff) | |
| download | bcm5719-llvm-735d8ea0d480cea946a1d41bfbf515a834afcebc.tar.gz bcm5719-llvm-735d8ea0d480cea946a1d41bfbf515a834afcebc.zip | |
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
llvm-svn: 333899
Diffstat (limited to 'llvm/lib/TableGen/TGParser.cpp')
0 files changed, 0 insertions, 0 deletions
