Z3/SMT:我应该什么时候更喜欢 push/pop 重置? [英] Z3/SMT: When should I prefer push/pop to reset?

问题描述

我使用 Z3 来解决符号执行器产生的路径条件，它以深度优先顺序探索状态空间，与 CUTE、DART 或(可能)SAGE 非常相似.我们正在试验使用 Z3 的不同方式.在一个极端情况下，我们将每个查询发送到 Z3 并在之后立即(重置)它.另一方面，我们(推送)每个额外的分支约束，并在回溯时(弹出)(弹出)正确削弱路径条件所需的最小值.问题是，在所有情况下，似乎没有任何策略比任何其他策略更有效.推送似乎提供了最好的优势，但我们遇到了一些情况，在每次查询后重置 Z3 比执行推送/弹出快一个数量级以上.请注意，通信开销可以忽略不计:几乎所有时间都花在 check-sat 内.

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.

有没有人有任何经验可以分享，或者关于 Z3 内部保存的状态(引理等)的一些迹象，这可以帮助澄清其行为?那么其他 SMT 求解器的行为呢?

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?

推荐答案

下一个版本 (v4.3.2) 将公开一个可能对您有用的功能.在 Z3 中，默认求解器结合了非增量求解器和增量求解器.当使用push/pop(或使用多个check而不调用reset)时，Z3将使用增量求解器.在下一个版本中，我们可以为增量求解器提供超时.如果增量求解器在给定的超时时间内无法解决问题，Z3 将自动切换到非增量求解器.也许，如果您使用此功能，您将能够两全其美".要获取下一个候选版本的源代码，您应该使用

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

为了编译它，我们使用

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>

如果您使用的是编程 API，则可以使用新 API:

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

Z3_global_param_set(Z3_string param_id, Z3_string param_value)

请注意，下一个版本将有一个新的参数设置框架.它允许用户设置内部 Z3 模块的参数.

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

这篇关于Z3/SMT:我应该什么时候更喜欢 push/pop 重置?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！