How to perform quantifier elimination using Python API of Z3

Question

How can I perform quantifier elimination using the Python API of Z3? Although I checked the tutorial and API, couldn't manage to do it.

I have a formula that has an existential quantifier and I want Z3 to give me a new formula, such that this quantifier is eliminated. I essentially want to do the same thing as this:

How to hide variable with Z3

but with the Python interface. Also my formula is in linear arithmetic.

Thanks!

Addition: After doing the quantifier elimination I will "add" the quantifier-free formula with another one. So if I make use of the Tactic, is there a way to convert a subgoal (which is the output of the tactic) to an expression in linear arithmetic?

Answer 1

You may use the quantifier elimination tactic for this (see the Tactic.apply docstring):

from z3 import Ints, Tactic, Exists, And
x, t1, t2 = Ints('x t1 t2')
t = Tactic('qe')
print t(Exists(x, And(t1 < x, x < t2)))

Answer 2

Possible solution using Z3Py online:

x, t1, t2 = Reals('x t1 t2')
g = Goal()
g.add(Exists(x, And(t1 < x, x < t2)))
t = Tactic('qe')
print t(g)

Output:

[[¬(0 ≤ t1 + -1·t2)]]

Run this example online here

Answer 3

Possible solution using Redlog of reduce: