Z3（Python）中实封闭域中的量词消除

【问题标题】：Quantifier elimination in the real closed fields in Z3 (Python)Z3（Python）中实封闭域中的量词消除
【发布时间】：2014-09-18 20:43:20
【问题描述】：

Z3 现在有一个基于圆柱代数分解的非线性实数算术可满足性引擎。

有什么方法可以得到量词消除的结果，而不是单纯的可满足性测试？

以下不起作用：

from z3 import *
b,c,x = Reals('b c x')
f = Exists(x, b*x+c==0);
print Tactic('qe')(f).as_expr();

我想得到类似 Or(b!=0, And(b==0, c==0)) 的东西。

谢谢。

【问题讨论】：

标签： z3 z3py

【解决方案1】：

Z3 中还没有全面的非线性 QE。有一个非常部分的非线性 QE，它在低阶多项式上使用虚拟替换。您可以在此示例中使用它：

from z3 import *
b,c,x = Reals('b c x')
f = Exists(x, b*x+c==0);
tac = Tactic('qe')
tac = With(tac, qe_nonlinear=True)
print tac.param_descrs() 
print tac(f).as_expr();

【讨论】：