Converting Z3 QBF formula directly to pcnf

Question

I'm using Z3 theorem prover (using Z3Py: the Z3 API in Python) to create QBF (Quantified Boolean formula).

Is there any way in Z3 to directly convert your qbf formula into Prenex normal form ?

Answer 1

I don't think there's a tactic to convert to Prenex, but you can surely apply the quantifier-elimination tactic and further process your formulas. Note that the transformed formulas will not really look like the originals, as they are mechanically generated.

Here's an example:

from z3 import *

f = Function('f', IntSort(), IntSort(), IntSort())
x, y = Ints('x y')
p = ForAll(x, Or(x == 2, Exists(y, f (x, y) == 0)))

print Tactic('qe')(p)

Here qe is the quantifier elimination tactic. This produces:

[[Not(Exists(x!0,
             Not(Or(x!0 == 2,
                    Exists(x!1,
                           And(f(x!0, x!1) <= 0,
                               f(x!0, x!1) >= 0))))))]]

For a nice tutorial on tactics, see here: http://ericpony.github.io/z3py-tutorial/strategies-examples.htm