Z3 / SMT：我什么时候应该选择push / pop来重置？-Java 学习之路

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

有没有人有任何经验可以分享，或者Z3（lemmas等）内部保留的状态有哪些迹象，这有助于澄清其行为？那么其他SMT求解器的行为呢？

1 回答

3
下一个版本（v4.3.2）将公开可能对您有用的功能 . 在Z3中，默认解算器组合了非增量求解器和增量求解器 . 当使用 push / pop （或使用多个 check 而不调用 reset ）时，Z3将使用增量解算器 . 在下一个版本中，我们可以为增量解算器提供超时 . 如果增量求解器无法解决给定超时中的问题，Z3将自动切换到非增量求解器 . 也许，如果您使用此功能，您将能够充分利用"both worlds" . 要获取下一个候选版本的源代码，您应该使用
```
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模块设置参数 .
回复于 2024-04-29T06:31:54+08:00

Z3 / SMT：我什么时候应该选择push / pop来重置？

1 回答

相关问题