<html><head><meta http-equiv="Content-Type" content="text/html; charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><br class=""><div><br class=""><blockquote type="cite" class=""><div class="">On Mar 9, 2018, at 7:22 AM, Ashish Gahlot via cfe-dev <<a href="mailto:cfe-dev@lists.llvm.org" class="">cfe-dev@lists.llvm.org</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div dir="ltr" class=""><div class="">Hello,<br class=""><br class=""></div>Thank you for the detailed explanation.<br class=""><div class=""><div class=""><div class="gmail_extra"><br class=""><div class="gmail_quote">On Fri, Mar 9, 2018 at 3:16 AM, Dan Liew <span dir="ltr" class=""><<a href="mailto:dan@su-root.co.uk" target="_blank" class="">dan@su-root.co.uk</a>></span> wrote:<br class=""><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><br class="">
@Dominic: On a related note. If you remember, a while back we spoke<br class="">
about `Z3_mk_simple_solver()` vs `Z3_mk_solver()` and how their<br class="">
performance characteristics and radically different (Z3_mk_solver()<br class="">
being much faster most of the time for us in KLEE [1]).<br class="">
I've just noticed that you're using `Z3_solver_push()` and<br class="">
`Z3_solver_pop()`. We don't use that in KLEE and that might be we why<br class="">
you had performance regressions when you tried switching to<br class="">
`Z3_mk_solver()`. When you use Z3_solver_push(),<br class="">
Z3 switches to a slower incremental solver internally [2,3]. You might<br class="">
find that if you remove the pushes and pops and use `Z3_mk_solver()`<br class="">
that things work better.<br class=""></blockquote><div class=""> </div><div class="">I read the issue [2] and it explains that it when we use (push), z3 tries to<br class=""></div><div class="">use the second solver. I think it would be a good idea to remove Solver.push()<br class=""></div><div class="">from Z3ConstraintManager.<br class=""></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<br class="">
[1] <a href="https://github.com/Z3Prover/z3/issues/1035" rel="noreferrer" target="_blank" class="">https://github.com/Z3Prover/<wbr class="">z3/issues/1035</a><br class="">
[2] <a href="https://github.com/Z3Prover/z3/issues/1459" rel="noreferrer" target="_blank" class="">https://github.com/Z3Prover/<wbr class="">z3/issues/1459</a><br class="">
[3] <a href="https://github.com/Z3Prover/z3/issues/1053" rel="noreferrer" target="_blank" class="">https://github.com/Z3Prover/<wbr class="">z3/issues/1053</a><br class="">
</blockquote></div><br class=""></div><div class="gmail_extra">Sorry for a noob question but is it possible to test the changes that I make to <br class=""></div><div class="gmail_extra">Z3ConstraintManager.cpp without having to compile the whole clang every time?<br class=""></div></div></div></div></div></blockquote><div><br class=""></div><div>It does not recompile everything, whenever you type “ninja clang” (or “make clang”)</div><div>from the build folder it only recompiles the changed file and does the relinking.</div><div>Headers are a different story — then it has to recompile all the files that transitively include that header,</div><div>unfortunately, nothing that can be done there.</div><br class=""><blockquote type="cite" class=""><div class=""><div dir="ltr" class=""><div class=""><div class=""><div class="gmail_extra"><br class="">Thank you very much,<br class="">Ashish Kumar Gahlot</div><div class="gmail_extra"><br class="">-- <br class=""><div class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr" class=""><div class=""><div dir="ltr" class=""><div class="">Ashish Kumar Gahlot</div><div class="">IV year, UG</div><div class="">Govt. Engg. College, Ajmer, India</div></div></div></div></div>
</div></div></div></div>
_______________________________________________<br class="">cfe-dev mailing list<br class=""><a href="mailto:cfe-dev@lists.llvm.org" class="">cfe-dev@lists.llvm.org</a><br class="">http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev<br class=""></div></blockquote></div><br class=""></body></html>