Z3中真實封閉場中的量詞消除（Python）

Question

Z3現在基於圓柱代數分解的非線性實數算法具有可滿足性引擎。

有沒有什麼方法可以獲得量詞消除的結果，而不僅僅是可滿足性測試？

下不起作用：

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

我想獲得類似或（！B = 0，和（b == 0，C == 0））。

謝謝。

Answer 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();