Z3/SMT：我应该什么时候推/推重置？

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

有没有人有任何经验可以分享，或有关Z3内部保存的状态（引理等）的一些迹象，这有助于阐明其行为？那么其他SMT解算器的行为呢？

来源

2013-01-11 Pietro Braione

下一版本（v4.3.2）将公开可能对您有用的功能。在Z3中，默认求解器组合了一个非增量求解器和一个增量求解器。当使用push/pop（或使用多个check而不调用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-13 18:24:59

谢谢你的回答，并对迟到的反馈抱歉。这只能部分回答我的问题，因为它没有提供给出一系列查询来确定使用求解器的最佳方式的基本原理，这个问题在我们的案例中可能至关重要。顺便说一句，push + reset（没有弹出）触发增量求解器吗？ –

Z3/SMT：我应该什么时候推/推重置？

回答

相关问题