<div dir="ltr">Hi,<div><br></div><div>In our experiments (we convert about 9000 C program to SMT almost daily), disabling relevancy gives a massive speed up in the verification time (we, however, don't use the incremental mode); maybe that's something to try on clang.</div><div><br></div><div>Thank you,</div></div><div class="gmail_extra"><br><div class="gmail_quote">2018-03-11 12:57 GMT+00:00 Nuno Lopes via cfe-dev <span dir="ltr"><<a href="mailto:cfe-dev@lists.llvm.org" target="_blank">cfe-dev@lists.llvm.org</a>></span>:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">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.<br>
BTW, there's a 3rd option which is to reset the solver.<br>
<br>
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.<br>
<br>
Nuno<div class="HOEnZb"><div class="h5"><br>
<br>
-----Original Message-----<br>
From: Dominic Chen via cfe-dev<br>
Sent: Thursday, March 8, 2018 10:13 PM<br>
Subject: Re: [cfe-dev] [GSOC 2018] Integrate with Z3 SMT solver<br>
<br>
Yes, I recall Nuno Lopes made a similar comment about the effect of<br>
pushes and pops on the internal solver state, and that the performance<br>
can differ depending on the workload. In fact, the initial<br>
implementation did recreate the solver for each satisfiability query,<br>
but it ended up being slower than the current version that reuses the<br>
solver state.<br>
<br>
Dominic<br>
<br>
On 3/8/2018 4:46 PM, Dan Liew wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Hi,<br>
<br>
On 8 March 2018 at 19:00, Dominic Chen via cfe-dev<br>
<<a href="mailto:cfe-dev@lists.llvm.org" target="_blank">cfe-dev@lists.llvm.org</a>> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
I’m not sure what you mean by letting Z3 manage memory. Unless something has<br>
changed significantly since I looked at the source, the Z3 C++ API simply<br>
wraps memory management functions from the lower-level Z3 C API using C++<br>
objects. Since the constraint manager is using the C API, due to<br>
compatibility issues with RTTI and exceptions, it needs to call the<br>
appropriate memory management functions.<br>
</blockquote>
I think he probably means the reference counting Z3_context. Z3<br>
provides two ways to create a context.<br>
`Z3_mk_context()` makes a context where the reference counting of<br>
Z3_ast objects is done automatically, but the reference counting of<br>
other objects (e.g. Z3_model) still need to be done manually.<br>
`Z3_mk_context_rc()` makes a context where everything (including<br>
`Z3_ast` objects) must be manually reference counted.<br>
<br>
The Z3 C++ API actually now supports being used with exceptions and<br>
RTTI. However I still think the C API is the better choice because its<br>
more stable.<br>
<br>
In KLEE we use `Z3_mk_context_rc()` because we want to be able to<br>
cache expressions but we don't want to do so indefinitely (i.e. we<br>
want to control when the reference counts goes to zero and memory gets<br>
freed).<br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Likewise, I’m not sure what cache memory you’re referring to. There was some<br>
discussion of a SMT query cache in CSA, but I don’t believe that was ever<br>
implemented.<br>
</blockquote>
@Ashish: I'm not sure what you mean either. Perhaps you mean Z3's<br>
internal expression cache that it uses when `Z3_mk_context()`? is<br>
used. This gets cleared when the created expressions go out of scope<br>
when `Z3_solver_pop()` gets used.<br>
<br>
<br>
@Dominic: On a related note. If you remember, a while back we spoke<br>
about `Z3_mk_simple_solver()` vs `Z3_mk_solver()` and how their<br>
performance characteristics and radically different (Z3_mk_solver()<br>
being much faster most of the time for us in KLEE [1]).<br>
I've just noticed that you're using `Z3_solver_push()` and<br>
`Z3_solver_pop()`. We don't use that in KLEE and that might be we why<br>
you had performance regressions when you tried switching to<br>
`Z3_mk_solver()`. When you use Z3_solver_push(),<br>
Z3 switches to a slower incremental solver internally [2,3]. You might<br>
find that if you remove the pushes and pops and use `Z3_mk_solver()`<br>
that things work better.<br>
<br>
Actually there is a third way... If you create your own custom tactic<br>
you will by-pass Z3's internal logic for trying to set up own solving<br>
strategy. I think if you use push/pop with a custom tactic you'll<br>
by-pass incremental solving<br>
and likely get better performance.<br>
<br>
Note in KLEE we end up creating a new `Z3_solver()` object for every<br>
solver query. This isn't great but you have to do this (or use<br>
`Z3_solver_reset()`) to clear the assertion stack without using<br>
push/pop.<br>
Because we don't use push/pop this necessitates that we do reference<br>
counting manually (otherwise we'd never free Z3_asts until the<br>
Z3_context gets destroyed).<br>
<br>
[1] <a href="https://github.com/Z3Prover/z3/issues/1035" rel="noreferrer" target="_blank">https://github.com/Z3Prover/z3<wbr>/issues/1035</a><br>
[2] <a href="https://github.com/Z3Prover/z3/issues/1459" rel="noreferrer" target="_blank">https://github.com/Z3Prover/z3<wbr>/issues/1459</a><br>
[3] <a href="https://github.com/Z3Prover/z3/issues/1053" rel="noreferrer" target="_blank">https://github.com/Z3Prover/z3<wbr>/issues/1053</a><br>
<br>
Thanks,<br>
Dan. <br>
</blockquote>
<br>
______________________________<wbr>_________________<br>
cfe-dev mailing list<br>
<a href="mailto:cfe-dev@lists.llvm.org" target="_blank">cfe-dev@lists.llvm.org</a><br>
<a href="http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev" rel="noreferrer" target="_blank">http://lists.llvm.org/cgi-bin/<wbr>mailman/listinfo/cfe-dev</a><br>
</div></div></blockquote></div><br><br clear="all"><div><br></div>-- <br><div class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div><br></div><div>Mikhail Ramalho.</div></div></div>
</div>