[cfe-dev] [GSOC 2018] Integrate with Z3 SMT solver

[Dominic Chen via cfe-dev]

Interesting, thanks for the update. I'm not actively working on
Z3ConstraintManager, so anyone interested should go for it. There's
plenty of room for performance improvements.

Dominic

On 3/11/2018 8:57 AM, Nuno Lopes wrote:
> The implementation of the incremental stuff has improved in Z3 in the
> past year. Now the "fast" SAT solver supports a bit of incrementally.
> So the major difference now is that with push() you switch to the SMT
> solver that does lazy bit-blasting and the new solver does it eagerly
> for the whole formula.
> BTW, there's a 3rd option which is to reset the solver.
>
> I agree that going with a custom tactic is the way to go. Otherwise
> you are exposed to changes in the internals of Z3 and you never know
> what's running underneath. Also, you can tune the set of tactics for
> the formulas that clang generates.  I can help with this if there's
> interest.
>
> Nuno
>
> -----Original Message-----
> From: Dominic Chen via cfe-dev
> Sent: Thursday, March 8, 2018 10:13 PM
> Subject: Re: [cfe-dev] [GSOC 2018] Integrate with Z3 SMT solver
>
> Yes, I recall Nuno Lopes made a similar comment about the effect of
> pushes and pops on the internal solver state, and that the performance
> can differ depending on the workload. In fact, the initial
> implementation did recreate the solver for each satisfiability query,
> but it ended up being slower than the current version that reuses the
> solver state.
>
> Dominic