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

Question

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

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

如何用 Z3 隐藏变量

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

谢谢！

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

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)))

Answer 2

在线使用 Z3Py 的可能解决方案：

x, t1, t2 = Reals('x t1 t2')
g = Goal()
g.add(Exists(x, And(t1 < x, x < t2)))
t = Tactic('qe')
print t(g)

输出：

[[¬(0 ≤ t1 + -1·t2)]]

在此处在线运行此示例

Answer 3

使用redlog of reduce的可能解决方案：