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

[Ashish Gahlot via cfe-dev]

Hello,

Thank you for the detailed explanation.

On Fri, Mar 9, 2018 at 3:16 AM, Dan Liew <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
> [2] https://github.com/Z3Prover/z3/issues/1459
> [3] 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?

Thank you very much,
Ashish Kumar Gahlot

-- 
Ashish Kumar Gahlot
IV year, UG
Govt. Engg. College, Ajmer, India
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20180309/f4b2aa5f/attachment.html>