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

Question

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

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

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

s.push()

s.pop()

之前的某个地方s.check()，然后s.check()运行无穷无尽。只有使用pushwithout才能pop正常工作。

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

非常感谢和问候，克劳斯

Answer 1

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

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

    set_option(verbose=10)

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

  s = Solver()

和

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

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