Page MenuHomePhabricator

[analyzer] Got rid of the `Z3ConstraintManager` class

Authored by mikhail.ramalho on Nov 27 2018, 2:33 PM.



Now, instead of passing the reference to a shared_ptr, we pass the shared_ptr instead.

I've also removed the check if Z3 is present in CreateZ3ConstraintManager as this function already calls CreateZ3Solver that performs the exactly same check.

Diff Detail

rC Clang

Event Timeline

Moved CreateZ3Solver to SMTConstraintManager.

In the future, CreateZ3Solver should be renamed CreateSMTSolver to handle all backends.

NoQ accepted this revision.Nov 30 2018, 5:27 PM

Makes perfect sense to me.

834 ↗(On Diff #176119)

Why are we even passing StMgr into this callback when it can be easily retrieved from Eng? :)

This revision is now accepted and ready to land.Nov 30 2018, 5:27 PM
mikhail.ramalho marked an inline comment as done.Dec 10 2018, 12:20 PM
mikhail.ramalho added inline comments.
834 ↗(On Diff #176119)

I guess I simply copied it from RangeConstraintManager.cpp:311...

I can send another patch to remove the parameter from both functions. They are declared in ConstraintManager.h:200 and ConstraintManager.h:204.

This revision was automatically updated to reflect the committed changes.
Herald added a project: Restricted Project. · View Herald TranscriptFeb 6 2019, 7:18 PM
Herald added a subscriber: cfe-commits. · View Herald Transcript