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

[Nuno Lopes via cfe-dev]

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

On 3/8/2018 4:46 PM, Dan Liew wrote:
> Hi,
>
> On 8 March 2018 at 19:00, Dominic Chen via cfe-dev
> <cfe-dev at lists.llvm.org> wrote:
>> I’m not sure what you mean by letting Z3 manage memory. Unless something 
>> has
>> changed significantly since I looked at the source, the Z3 C++ API simply
>> wraps memory management functions from the lower-level Z3 C API using C++
>> objects. Since the constraint manager is using the C API, due to
>> compatibility issues with RTTI and exceptions, it needs to call the
>> appropriate memory management functions.
> I think he probably means the reference counting Z3_context. Z3
> provides two ways to create a context.
> `Z3_mk_context()` makes a context where the reference counting of
> Z3_ast objects is done automatically, but the reference counting of
> other objects (e.g. Z3_model) still need to be done manually.
> `Z3_mk_context_rc()` makes a context where everything (including
> `Z3_ast` objects) must be manually reference counted.
>
> The Z3 C++ API actually now supports being used with exceptions and
> RTTI. However I still think the C API is the better choice because its
> more stable.
>
> In KLEE we use `Z3_mk_context_rc()` because we want to be able to
> cache expressions but we don't want to do so indefinitely (i.e. we
> want to control when the reference counts goes to zero and memory gets
> freed).
>
>> Likewise, I’m not sure what cache memory you’re referring to. There was 
>> some
>> discussion of a SMT query cache in CSA, but I don’t believe that was ever
>> implemented.
> @Ashish: I'm not sure what you mean either. Perhaps you mean Z3's
> internal expression cache that it uses when `Z3_mk_context()`? is
> used. This gets cleared when the created expressions go out of scope
> when `Z3_solver_pop()` gets used.
>
>
> @Dominic: On a related note. If you remember, a while back we spoke
> about `Z3_mk_simple_solver()` vs `Z3_mk_solver()` and how their
> performance characteristics and radically different (Z3_mk_solver()
> being much faster most of the time for us in KLEE [1]).
> I've just noticed that you're using `Z3_solver_push()` and
> `Z3_solver_pop()`. We don't use that in KLEE and that might be we why
> you had performance regressions when you tried switching to
> `Z3_mk_solver()`. When you use Z3_solver_push(),
> Z3 switches to a slower incremental solver internally [2,3]. You might
> find that if you remove the pushes and pops and use `Z3_mk_solver()`
> that things work better.
>
> Actually there is a third way... If you create your own custom tactic
> you will by-pass Z3's internal logic for trying to set up own solving
> strategy. I think if you use push/pop with a custom tactic you'll
> by-pass incremental solving
> and likely get better performance.
>
> Note in KLEE we end up creating a new `Z3_solver()` object for every
> solver query. This isn't great but you have to do this (or use
> `Z3_solver_reset()`) to clear the assertion stack without using
> push/pop.
> Because we don't use push/pop this necessitates that we do reference
> counting manually (otherwise we'd never free Z3_asts until the
> Z3_context gets destroyed).
>
> [1] https://github.com/Z3Prover/z3/issues/1035
> [2] https://github.com/Z3Prover/z3/issues/1459
> [3] https://github.com/Z3Prover/z3/issues/1053
>
> Thanks,
> Dan.