HomePhabricator

Generalised the SMT state constraints

Authored by mikhail.ramalho on Feb 6 2019, 7:17 PM.

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

llvm-svn: 353370

Details

Committed
mikhail.ramalhoFeb 6 2019, 7:17 PM
Differential Revision
D54975: [analyzer] Generalised the SMT state constraints
Parents
rGc449409533ba: gn build: Merge the test part of r353237.
Branches
Unknown
Tags
Unknown