Page MenuHomePhabricator

[analyzer] Move canReasonAbout from Z3ConstraintManager to SMTConstraintManager
ClosedPublic

Authored by mikhail.ramalho on Oct 25 2018, 5:55 AM.

Details

Summary

This patch moves the last method in Z3ConstraintManager to SMTConstraintManager: canReasonAbout().

The canReasonAbout() method checks if a given SVal can be encoded in SMT. I've added a new method to the SMT API to return true if a solver can encode floating-point arithmetics and it was enough to make canReasonAbout() solver independent.

As an annoying side-effect, Z3ConstraintManager is pretty empty now and only (1) creates the Z3 solver object by calling CreateZ3Solver() and (2) instantiates SMTConstraintManager. Maybe we can get rid of this class altogether in the future: a CreateSMTConstraintManager() method that does (1) and (2) and returns the constraint manager object?

Diff Detail

Repository
rL LLVM

Event Timeline

This revision is now accepted and ready to land.Oct 25 2018, 10:11 AM
This revision was automatically updated to reflect the committed changes.