diff options
| author | Mikhail R. Gadelha <mikhail.ramalho@gmail.com> | 2018-07-25 12:49:29 +0000 |
|---|---|---|
| committer | Mikhail R. Gadelha <mikhail.ramalho@gmail.com> | 2018-07-25 12:49:29 +0000 |
| commit | 456ecffe112bb05ec14ef4816eb107e2d6a783ce (patch) | |
| tree | f7855ac5c9790b3b6286261d7ec478bec30110b8 /llvm/lib/CodeGen/AsmPrinter/DwarfStringPool.cpp | |
| parent | 635378b78316569c8ee30a971d6d2f2b950f2ec5 (diff) | |
| download | llvm-456ecffe112bb05ec14ef4816eb107e2d6a783ce.zip llvm-456ecffe112bb05ec14ef4816eb107e2d6a783ce.tar.gz llvm-456ecffe112bb05ec14ef4816eb107e2d6a783ce.tar.bz2 | |
[analyzer] Moved non solver specific code from Z3ConstraintManager to SMTConstraintManager
Summary:
This patch moves a lot of code from `Z3ConstraintManager` to `SMTConstraintManager`, leaving only the necessary:
* `canReasonAbout` which returns if a Solver can handle a given `SVal` (should be moved to `SMTSolver` in the future).
* `removeDeadBindings`, `assumeExpr` and `print`: methods that need to use `ConstraintZ3Ty`, can probably be moved to `SMTConstraintManager` in the future.
The patch creates a new file, `SMTConstraintManager.cpp` with the moved code. Conceptually, this is move in the right direction and needs further improvements: `SMTConstraintManager` still does a lot of things that are not required by a `ConstraintManager`.
We ought to move the unrelated to `SMTSolver` and remove everything that's not related to a `ConstraintManager`. In particular, we could remove `addRangeConstraints` and `isModelFeasible`, and make the refutation manager create an Z3Solver directly.
Reviewers: NoQ, george.karpenkov
Reviewed By: george.karpenkov
Subscribers: mgorny, xazax.hun, szepet, a.sidorin
Differential Revision: https://reviews.llvm.org/D49668
llvm-svn: 337919
Diffstat (limited to 'llvm/lib/CodeGen/AsmPrinter/DwarfStringPool.cpp')
0 files changed, 0 insertions, 0 deletions