如何在 Z3py 中激活部分模式？

Question

我正在使用 Z3 的 Python 绑定，我很好奇部分模式是否会加速我的模型。然而，似乎没有办法在 Python 中做到这一点。 （set_param(...) 似乎没有参数）

我考虑迁移到 pySMT，因为它声称支持 Z3 的部分模式，但我更愿意保留 Z3Py。

额外问题：部分模式真的对我有什么好处吗？我正在模拟数组中的计算机内存，并希望 Z3 忽略从未引用的条目。

Answer 1

这是设置部分模型的方法：

from z3 import *

print get_param('model.partial')
set_param('model.partial', True)
print get_param('model.partial')

打印出来：

false
true

关于你的额外问题：我怀疑部分模型会为你买任何东西。 SMT 求解器通常会在 sat 的情况下找到模型，然后根据需要完成模型。 “寻找模型”部分通常是代价高昂的行动，而不是完成模型。但这当然取决于您的特定问题；所以尝试一下不会有什么坏处。