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

[Dan Liew via cfe-dev]

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.