z3 - 如何使用 Z3 的 Python API 执行量词消除

Question

如何使用 Z3 的 Python API 执行量词消除？尽管我检查了教程和 API，但无法做到。

我有一个具有存在量词的公式，我希望 Z3 给我一个新公式，这样这个量词就被消除了。我本质上想做与此相同的事情:

How to hide variable with Z3

但使用 Python 接口(interface)。我的公式也是线性算术。

谢谢!

添加:
完成量词消除后，我将“添加”另一个无量词公式。因此，如果我使用策略，有没有办法将子目标(即策略的输出)转换为线性算术表达式？

Answer 1

您可以为此使用量词消除策略(请参阅 Tactic.apply 文档字符串):

from z3 import Ints, Tactic, Exists, And
x, t1, t2 = Ints('x t1 t2')
t = Tactic('qe')
print t(Exists(x, And(t1 < x, x < t2)))