HomePhabricator

Generalised the SMT state constraints

Description

Generalised the SMT state constraints

This patch moves the ConstraintSMT definition to the SMTConstraintManager header to make it easier to move the Z3 backend around.

We achieve this by not using shared_ptr anymore, as llvm::ImmutableSet doesn't seem to like it.

The solver specific exprs and sorts are cached in the Z3Solver object now and we move pointers to those objects around.

As a nice side-effect, SMTConstraintManager doesn't have to be a template anymore. Yay!

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

Details

Committed
mramalhoFeb 6 2019, 7:17 PM
Differential Revision
D54975: [analyzer] Generalised the SMT state constraints
Branches
Unknown
Tags
Unknown