Skip to content
Commit 5c3d032e authored by Mikhail R. Gadelha's avatar Mikhail R. Gadelha
Browse files

[analyzer] Removed API used by the Refutation Manager from...

[analyzer] Removed API used by the Refutation Manager from SMTConstraintManager and replace by proper calls to SMTSolver

Summary:
Third patch in the refactoring series, to decouple the SMT Solver from the Refutation Manager (1st: D49668, 2nd: D49767).

The refutation API in the `SMTConstraintManager` was a hack to allow us to create an SMT solver and verify the constraints; it was conceptually wrong from the start. Now, we don't actually need to use the `SMTConstraintManager` and can create an SMT object directly, add the constraints and check them.

While updating the Falsification visitor, I inlined the two functions that were used to collect the constraints and add them to the solver.

As a result of this patch, we could move the SMT API elsewhere and as it's not really dependent on the CSA anymore. Maybe we can create a new dir (utils/smt) for Z3 and future solvers?

Reviewers: NoQ, george.karpenkov

Reviewed By: george.karpenkov

Subscribers: xazax.hun, szepet, a.sidorin

Differential Revision: https://reviews.llvm.org/D49768

llvm-svn: 337922
parent 8628e2cd
Loading
Loading
Loading
Loading
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please to comment