如何使用 Z3 的 Python API 执行量词消除？虽然我检查了教程和 API，但无法做到。
我有一个公式，它有一个存在量词，我希望 Z3 给我一个新公式，这样这个量词就被消除了。我基本上想做与此相同的事情：
但使用 Python 接口。我的公式也是线性算术。
谢谢！
添加：在进行量词消除后，我将用另一个“添加”无量词公式。因此，如果我使用 Tactic，是否可以将子目标（即策略的输出）转换为线性算术表达式？
您可以为此使用量词消除策略（请参阅 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)))