CODEWITHSUNDEEP
z3smtz3py
blurium
blurium

Reputation: 43

How to perform quantifier elimination using Python API of Z3

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?

Upvotes: 4

Views: 1993

Answers (3)

tbormer
tbormer

Reputation: 76

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

Upvotes: 6

Juan Ospina
Juan Ospina

Reputation: 1347

Possible solution using Redlog of reduce:

enter image description here

Upvotes: 0

Juan Ospina
Juan Ospina

Reputation: 1347

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

Upvotes: 0

Related Questions