Quantifier elimination in the real closed fields in Z3 (Python)

Question

Z3 now has a satisfiability engine for nonlinear real arithmetic based on cylindrical algebraic decomposition.

Is there any way to obtain the result of quantifier elimination, as opposed to mere satisfiability testing?

The following does not work:

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

I would like to get something like Or(b!=0, And(b==0, c==0)).

Thanks.

Nikolaj Bjorner Nikolaj Bjorner · Accepted Answer · 2014-09-18T21:37:10

There isn't a full blown non-linear QE in Z3 yet. There is a very partial non-linear QE that uses virtual substitutions on low order polynomials. You can use it on this example:

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

Quantifier elimination in the real closed fields in Z3 (Python)

1 Answers