z3 - 在 Z3 Python 中使用量词消除

Question

g = And(ForAll([i, j, k], Implies(And(k <= 0, A * i + B * j + C * k + D <= 0), k + i - j <= 0)),Not(And(A==0,B==0,C==0))) 我尝试使用找到满足公式的 A、B、C、D 的值solve(g) 。这有很多可能的解决方案，一个是A=1,B=-1,C=D=0但 Z3 似乎无法做到这一点（solve(g)不会终止）。

Z3 可以做这种非线性（但简单）的公式吗？也许我可以为此指定一些量化宽松策略或其他东西？

Answer 1

Z3 有一个量词消除策略。我们可以通过使用以下方法创建求解器来启用它：

s = Then('qe', 'smt').solver()

此命令将创建一个求解器，该求解器首先应用量词消除，然后调用 SMT 求解器。但是，Z3 对非线性公式的量词消除的支持非常有限。您的示例是非线性的，因为它包含：A * i + B * j + C * k + D <= 0. 因此，该qe策略将无法消除量词。

如果您可以为非线性算术实现更好的 QE 支持，那就太好了。