小编blu*_*ium的帖子

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

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

如何使用 Z3 隐藏变量

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

谢谢！

添加：在进行量词消除后，我将用另一个“添加”无量词公式。因此，如果我使用 Tactic，是否可以将子目标（即策略的输出）转换为线性算术表达式？