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

[George Karpenkov via cfe-dev]

> On Mar 9, 2018, at 7:22 AM, Ashish Gahlot via cfe-dev <cfe-dev at lists.llvm.org> wrote:
> 
> Hello,
> 
> Thank you for the detailed explanation.
> 
> On Fri, Mar 9, 2018 at 3:16 AM, Dan Liew <dan at su-root.co.uk <mailto:dan at su-root.co.uk>> wrote:
> 
> @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.
>  
> I read the issue [2] and it explains that it when we use (push), z3 tries to
> use the second solver. I think it would be a good idea to remove Solver.push()
> from Z3ConstraintManager.
> 
> [1] https://github.com/Z3Prover/z3/issues/1035 <https://github.com/Z3Prover/z3/issues/1035>
> [2] https://github.com/Z3Prover/z3/issues/1459 <https://github.com/Z3Prover/z3/issues/1459>
> [3] https://github.com/Z3Prover/z3/issues/1053 <https://github.com/Z3Prover/z3/issues/1053>
> 
> Sorry for a noob question but is it possible to test the changes that I make to 
> Z3ConstraintManager.cpp without having to compile the whole clang every time?

It does not recompile everything, whenever you type “ninja clang” (or “make clang”)
from the build folder it only recompiles the changed file and does the relinking.
Headers are a different story — then it has to recompile all the files that transitively include that header,
unfortunately, nothing that can be done there.

> 
> Thank you very much,
> Ashish Kumar Gahlot
> 
> -- 
> Ashish Kumar Gahlot
> IV year, UG
> Govt. Engg. College, Ajmer, India
> _______________________________________________
> cfe-dev mailing list
> cfe-dev at lists.llvm.org
> http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20180309/23d4c53c/attachment.html>