3

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

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

4

1 回答 1

4

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

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

为了编译它，我们使用

cd z3
python scripts/mk_make.py
cd build
make

要为增量求解器设置超时，我们必须提供以下命令行选项：

 combined_solver.solver2_timeout=<time in milliseconds>

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

Z3_global_param_set(Z3_string param_id, Z3_string param_value)

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

于 2013-01-13T18:24:59.203 回答