Skip to content
Commit 456ecffe authored by Mikhail R. Gadelha's avatar Mikhail R. Gadelha
Browse files

[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
parent 635378b7
Loading
Loading
Loading
Loading
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please to comment