3

I am using Z3 to solve the path conditions produced by a symbolic executor, which explores the state space in depth-first order, quite similarly to CUTE, DART or (possibly) SAGE. We are experimenting different ways of using Z3. At one extreme, we send every query to Z3 and (reset) it right after. At the other, we (push) every additional branch constraint, and (pop) (pop) upon backtrack the minimum necessary to correctly weaken the path condition. The problem is, no strategy seems to work better than any other in all the circumstances. Pushing seems to offer the best advantage, but we met a few cases where resetting Z3 after every query is more than one order of magnitude faster than doing push/pop. Note that communication overhead is negligible: almost all the time is spent inside check-sat.

Does anyone have any experience to share, or some indication on the state kept internally by Z3 (lemmas, etc), which can help clarifying its behavior? And what about the behavior of other SMT solvers?

Pietro Braione
  • 1,123
  • 8
  • 22

1 Answers1

4

The next release (v4.3.2) will expose a feature that may be useful for you. In Z3, the default solver combines a non-incremental solver and an incremental one. When push/pop are used (or multiple checks are used without invoking reset), Z3 will use the incremental solver. In the next release, we can provide a timeout for the incremental solver. If the incremental solver can't solve the problem in the given timeout, Z3 will automatically switch to the non-incremental one. Perhaps, if you use this feature, you will be able to get the best of "both worlds". To get the source code for the next release candidate, you should use

git clone https://git01.codeplex.com/z3 -b rc

To compile it, we have use

cd z3
python scripts/mk_make.py
cd build
make

To set the timeout for the incremental solver, we have to provide the following command line option:

 combined_solver.solver2_timeout=<time in milliseconds>

If you are using the programmatic APIs, you can the new API:

Z3_global_param_set(Z3_string param_id, Z3_string param_value)

Note that, the next release will have a new framework for setting parameters. It allows the user to set parameters for internal Z3 modules.

Leonardo de Moura
  • 21,065
  • 2
  • 47
  • 53
  • Thank you for the answer and sorry for the late feedback. This answers only in part to my question, since it does not provide the rationale for establishing an optimal way to use the solver given a sequence of queries, an issue that can be critical in our case. By the way, does push + reset (without pop) trigger the incremental solver? – Pietro Braione Feb 05 '13 at 16:17