使用 Python-API 进行推送/弹出的 Z3 问题答案

【问题标题】：Z3 Problems with push/pop with Python-API使用 Python-API 进行推送/弹出的 Z3 问题
【发布时间】：2013-06-18 11:58:38
【问题描述】：

我正在使用带有 Python-API 的 Z3。我正在设置一组相当大的线性算术约束。

但是，push/pop 导致 check() 无限运行。

如果我不使用任何push/pop，一切正常。但是当我插入一个

s.push()

s.pop()

s.check() 之前的某处，然后s.check() 无限运行。仅使用 push 而不使用 pop 可以正常工作。

是否有任何已知问题和解决方法？我在 MacOS 10.7.5 上使用 Z3 [版本 4.3.1 - 64 位]。

非常感谢和问候，克劳斯

【问题讨论】：

您能否提供一个指向显示所描述行为的rise4fun-example 的链接？
亲爱的 Malte，您可以在这里找到一个示例：rise4fun.com/Z3Py/UATh 使用给定的 NUM_A 和 NUM_B 值，当我不使用任何 push() 和 Pop() 时，它解决了问题，但它当我在第 23 行添加 push() 时出现超时。使用 NUM_B = 10 而不是 NUM_B = 3，这种效果要高得多。然后 Z3py 在适当的时间解决了问题，但它需要更长的时间。添加 push() 时无穷无尽。我不明白为什么运行时仅仅因为 push() 和 pop() 就如此不同！？谢谢，克劳斯 PS。是否可以在 python 脚本中定义超时？

标签： z3 z3py

【解决方案1】：

Z3 是求解器的集合。但是，其中只有一个是增量的。非增量求解器对您的问题更有效。当您使用s.push() 时，Z3“猜测”您想要增量解决问题，并切换到增量（通用）求解器。

如果我们在文件开头添加以下命令，Z3 将显示几条消息。请注意，当我们使用s.push() 时，消息完全不同。

    set_option(verbose=10)

我们可以强制 Z3 使用特定的求解器。例如，如果我们替换

  s = Solver()

与

  s = Tactic('qflia').solver()

然后，即使使用s.push()，Z3 也会使用高效求解器。但是，它将从头开始每个check() 命令。我认为这不是您的问题的问题，因为非增量和增量之间的性能差异非常大。

【讨论】：

亲爱的莱昂纳多，谢谢！ qflia 策略对我来说很好用。但是，我的代码中有一个“s.reset()”，这会强制出现“分段错误：11”。一个'c.py（39）：错误：异常：访问冲突读取0x00000008'。我删除了“s.reset()”，现在它可以工作了。 qflia 是否不允许 reset() 或者这是一个错误？
还有一个问题 ;) 是否有任何rise4fun 示例，我可以在其中看到如何在从 python API 调用 s.check() 时设置超时？谢谢
Segfault 已在 unstable (work-in-progress) 分支中修复。该修复程序也可用于夜间构建 (research.microsoft.com/en-us/um/people/leonardo/blog/2013/02/15/…)。