More efficient ways to use Z3 via its C API in the context of symbolic execution

delcypher commented 8 years ago

This is a set of questions rather than an actual issue with Z3.

I currently have basic support for using Z3 via its C API implemented in the KLEE symbolic execution engine. But I suspect how I'm using the API is sub-optimal so I'd like to discuss how Z3 is being currently used and how I can improve how I'm using it.

For reference you can find the code in KLEE to uses Z3 at

@ccadar @MartinNowack the answers here will likely be of interest to you.

So my questions currently are

What solver should I be using? I'm currently using Z3_mk_simple_solver() but I noticed there are also Z3_mk_solver(), Z3_mk_solver_for_logic() and Z3_mk_solver_from_tactic() functions. The documentation doesn't really make it clear what the differences are between the these calls. For example the documentation for Z3_mk_simple_solver() seems to talk about Z3_solver_get_model() and not much about what the solver being created actually does? In KLEE the logic is currently QF_ABV so would specifying this help?
Currently in KLEE a new solver is created and destroyed for every query. Is this adding unnecessary overhead compared to having a persistent solver and just pushing and popping assertions? I was wary of doing that due to observing in the the past that the use of push and pop can drastically change the performance on some queries. Am I loosing anything (e.g. some sort of internal caching inside Z3) by not having a persistent solver? Note that in KLEE path exploration is not necessarily depth-first which means that queries given to Z3 are not guaranteed to be incremental which means that I might have to clear the entire stack of assertions every time a query is made (I suspect this might negate any advantages offered by having a persistent solver).
Z3 has many parameters that control its behaviour. Are there any you would suggest setting in this context?

If any of these questions are unclear please let me know and I'll attempt to clarify.

delcypher commented 8 years ago

@wintersteiger @NikolajBjorner ping.

Perhaps these questions are too broad. Here's a simpler one

What is the difference between

Z3_mk_simpler_solver()
Z3_mk_solver()

The docs don't make this very clear. Currently they say

`Z3_solver Z3_API Z3_mk_simple_solver(Z3_context c )`

Create a new (incremental) solver.

The function Z3_solver_get_model retrieves a model if the assertions is satisfiable (i.e., the result is Z3_L_TRUE) and model construction is enabled. The function Z3_solver_get_model can also be used even if the result is Z3_L_UNDEF, but the returned model is not guaranteed to satisfy quantified assertions.

`Z3_solver Z3_API Z3_mk_solver (Z3_context c)`

Create a new (incremental) solver. This solver also uses a set of builtin tactics for handling the first check-sat command, and check-sat commands that take more than a given number of milliseconds to be solved.

Are the docs trying to say that Z3_mk_simple_solver() does not do This solver also uses a set of builtin tactics for handling the first...? If so then this is not clear. It would also be helpful to know why the "set of builtin tactics for handling the first check-sat command, and..." might be useful.

MartinNowack commented 8 years ago

I had some experiments a couple of weeks ago. The results are mixed.

I can put the code online. On Apr 11, 2016 12:59 PM, "Dan Liew" notifications@github.com wrote:

@wintersteiger https://github.com/wintersteiger @NikolajBjorner https://github.com/NikolajBjorner ping.

Perhaps these questions are too broad. Here's a simpler one

What is the difference between

Z3_mk_simpler_solver()

Z3_mk_solver()

The docs don't make this very clear. Currently they say

Z3_solver Z3_API Z3_mk_simple_solver(Z3_context c )

Create a new (incremental) solver.

The function Z3_solver_get_model retrieves a model if the assertions is satisfiable (i.e., the result is Z3_L_TRUE) and model construction is enabled. The function Z3_solver_get_model can also be used even if the result is Z3_L_UNDEF, but the returned model is not guaranteed to satisfy quantified assertions. Z3_solver Z3_API Z3_mk_solver (Z3_context c)

Create a new (incremental) solver. This solver also uses a set of builtin tactics for handling the first check-sat command, and check-sat commands

that take more than a given number of milliseconds to be solved.

Are the docs trying to say that Z3_mk_simple_solver() does not do This solver also uses a set of builtin tactics for handling the first...? If so then this is not clear. It would also be helpful to know why the "set of builtin tactics for handling the first check-sat command, and..." might be useful.

— You are receiving this because you were mentioned. Reply to this email directly or view it on GitHub https://github.com/Z3Prover/z3/issues/546#issuecomment-208285671

agurfinkel commented 8 years ago

Z3_mk_simple_solver creates the incremental SMT solver (smt::solver). Z3_mk_solver creates a combined solver that applies non-incremental simplification tactics before passing control to smt::solver. The tactics are chosen based on the logic. See mk_tactic_for_logic for details.

The use of pre-processing is very conservative. Z3_mk_solver behaves more or less exactly like Z3_mk_simple_solver if any incrementality is detected (push, pop, assert after check_sat, check_sat with assumptions, etc.). See combined_solver::check_sat for the exact logic.

As far as I understand, all of this behavior is subject to change, hence it is not documented. You should use Z3_mk_solver unless you know that pre-processing will never be used, in which case use Z3_mk_simple_solver. If you want to control pre-processing at a more fine grained level, apply tactics using the tactic API and use Z3_mk_simple_solver.

Hope this helps, arie

delcypher commented 8 years ago

@agurfinkel Thanks this is helpful! Are all "tactics" pre-processing steps or are there "tactics" that do more than just pre-processing?

agurfinkel commented 8 years ago

This is not a well-formed question. A tactic takes a goal and reduces it to subgoals. A tactic can reduce a goal to sat/unsat or to other sub-goals. Everything is a tactic. The core smt solver is a tactic called smt. Usually, smt is the last tactic in a chain of tactics returned by mk_tactic_for_logic.

delcypher commented 8 years ago

@agurfinkel Thank you for explaining. I'm (as you can probably tell) not familiar with how Z3 works internally. Although for better or worse I have recently become very familiar with how it is compiled.

NikolajBjorner commented 8 years ago

I thought the question is well-formed, just not informed, but that is the reason for asking questions. So, the answer to your question is yes: there are tactics that do more than just pre-processing, such as the smt tactic. In general, tactics are one-shot functions. They don't work with pus/pop, which are what you want when performing incremental checks.

agurfinkel commented 8 years ago

I meant that I cannot give a meaningful yes/no answer :)

NikolajBjorner commented 8 years ago

updated my answer with "yes". The question contained a disjunction, the second disjunct is true when interpreted in the context of Z3.

delcypher commented 8 years ago

@agurfinkel @NikolajBjorner

This is not a well-formed question. A tactic takes a goal and reduces it to subgoals. A tactic can reduce a goal to sat/unsat or to other sub-goals. Everything is a tactic. The core smt solver is a tactic called smt. Usually, smt is the last tactic in a chain of tactics returned by mk_tactic_for_logic.

Based on your description is it correct for me to assume that the smt tactic does not produce externally visible (from the perspective of Z3's public API) sub-goals and always returns sat/unsat/unknown?

Is there any documentation that explains the role that tactics play in Z3? I took a look at

http://research.microsoft.com/en-us/um/redmond/projects/z3/z3.pdf

But this doesn't seem to (explicitly) mention tactics.

NikolajBjorner commented 8 years ago

Tactics were put in after 2008 (the paper you mention). There is a paper by Leo and Grant Passmore in the volume for McCune on tactics. The online tutorial on http://rise4fun.com/z3 also explains tactics from the point of view of the SMT2 interface.

NikolajBjorner commented 7 years ago

is this possible to close?

delcypher commented 7 years ago

@NikolajBjorner Sure. The question is a bit too broad really. Over time I've figured out that tactics really do help quite a lot.

Z3Prover / z3